sys/src/cmd/spin/tl_parse.c

   1 /***** tl_spin: tl_parse.c *****/
   2
   3 /*
   4  * This file is part of the public release of Spin. It is subject to the
   5  * terms in the LICENSE file that is included in this source directory.
   6  * Tool documentation is available at http://spinroot.com
   7  *
   8  * Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper,
   9  * presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.
  10  */
  11
  12 #include "tl.h"
  13
  14 extern int      tl_yylex(void);
  15 extern int      tl_verbose, tl_errs;
  16
  17 int     tl_yychar = 0;
  18 YYSTYPE tl_yylval;
  19
  20 static Node     *tl_formula(void);
  21 static Node     *tl_factor(void);
  22 static Node     *tl_level(int);
  23
  24 static int      prec[2][4] = {
  25         { U_OPER,  V_OPER, 0, 0 },      /* left associative */
  26         { OR, AND, IMPLIES, EQUIV, },   /* left associative */
  27 };
  28
  29 static Node *
  30 tl_factor(void)
  31 {       Node *ptr = ZN;
  32
  33         switch (tl_yychar) {
  34         case '(':
  35                 ptr = tl_formula();
  36                 if (tl_yychar != ')')
  37                         tl_yyerror("expected ')'");
  38                 tl_yychar = tl_yylex();
  39                 break;
  40         case NOT:
  41                 ptr = tl_yylval;
  42                 tl_yychar = tl_yylex();
  43                 ptr->lft = tl_factor();
  44                 if (!ptr->lft)
  45                 {       fatal("malformed expression", (char *) 0);
  46                 }
  47                 ptr = push_negation(ptr);
  48                 break;
  49         case ALWAYS:
  50                 tl_yychar = tl_yylex();
  51                 ptr = tl_factor();
  52 #ifndef NO_OPT
  53                 if (ptr->ntyp == FALSE
  54                 ||  ptr->ntyp == TRUE)
  55                         break;  /* [] false == false */
  56
  57                 if (ptr->ntyp == V_OPER)
  58                 {       if (ptr->lft->ntyp == FALSE)
  59                                 break;  /* [][]p = []p */
  60
  61                         ptr = ptr->rgt; /* [] (p V q) = [] q */
  62                 }
  63 #endif
  64                 ptr = tl_nn(V_OPER, False, ptr);
  65                 break;
  66 #ifdef NXT
  67         case NEXT:
  68                 tl_yychar = tl_yylex();
  69                 ptr = tl_factor();
  70                 if (ptr->ntyp == TRUE)
  71                         break;  /* X true = true */
  72                 ptr = tl_nn(NEXT, ptr, ZN);
  73                 break;
  74 #endif
  75         case CEXPR:
  76                 tl_yychar = tl_yylex();
  77                 ptr = tl_factor();
  78                 if (ptr->ntyp != PREDICATE)
  79                 {       tl_yyerror("expected {...} after c_expr");
  80                 }
  81                 ptr = tl_nn(CEXPR, ptr, ZN);
  82                 break;
  83         case EVENTUALLY:
  84                 tl_yychar = tl_yylex();
  85
  86                 ptr = tl_factor();
  87 #ifndef NO_OPT
  88                 if (ptr->ntyp == TRUE
  89                 ||  ptr->ntyp == FALSE)
  90                         break;  /* <> true == true */
  91
  92                 if (ptr->ntyp == U_OPER
  93                 &&  ptr->lft->ntyp == TRUE)
  94                         break;  /* <><>p = <>p */
  95
  96                 if (ptr->ntyp == U_OPER)
  97                 {       /* <> (p U q) = <> q */
  98                         ptr = ptr->rgt;
  99                         /* fall thru */
 100                 }
 101 #endif
 102                 ptr = tl_nn(U_OPER, True, ptr);
 103
 104                 break;
 105         case PREDICATE:
 106                 ptr = tl_yylval;
 107                 tl_yychar = tl_yylex();
 108                 break;
 109         case TRUE:
 110         case FALSE:
 111                 ptr = tl_yylval;
 112                 tl_yychar = tl_yylex();
 113                 break;
 114         }
 115         if (!ptr) tl_yyerror("expected predicate");
 116 #if 0
 117         printf("factor: ");
 118         tl_explain(ptr->ntyp);
 119         printf("\n");
 120 #endif
 121         return ptr;
 122 }
 123
 124 static Node *
 125 bin_simpler(Node *ptr)
 126 {       Node *a, *b;
 127
 128         if (ptr)
 129         switch (ptr->ntyp) {
 130         case U_OPER:
 131 #ifndef NO_OPT
 132                 if (ptr->rgt->ntyp == TRUE
 133                 ||  ptr->rgt->ntyp == FALSE
 134                 ||  ptr->lft->ntyp == FALSE)
 135                 {       ptr = ptr->rgt;
 136                         break;
 137                 }
 138                 if (isequal(ptr->lft, ptr->rgt))
 139                 {       /* p U p = p */
 140                         ptr = ptr->rgt;
 141                         break;
 142                 }
 143                 if (ptr->lft->ntyp == U_OPER
 144                 &&  isequal(ptr->lft->lft, ptr->rgt))
 145                 {       /* (p U q) U p = (q U p) */
 146                         ptr->lft = ptr->lft->rgt;
 147                         break;
 148                 }
 149                 if (ptr->rgt->ntyp == U_OPER
 150                 &&  ptr->rgt->lft->ntyp == TRUE)
 151                 {       /* p U (T U q)  = (T U q) */
 152                         ptr = ptr->rgt;
 153                         break;
 154                 }
 155 #ifdef NXT
 156                 /* X p U X q == X (p U q) */
 157                 if (ptr->rgt->ntyp == NEXT
 158                 &&  ptr->lft->ntyp == NEXT)
 159                 {       ptr = tl_nn(NEXT,
 160                                 tl_nn(U_OPER,
 161                                         ptr->lft->lft,
 162                                         ptr->rgt->lft), ZN);
 163                 }
 164 #endif
 165 #endif
 166                 break;
 167         case V_OPER:
 168 #ifndef NO_OPT
 169                 if (ptr->rgt->ntyp == FALSE
 170                 ||  ptr->rgt->ntyp == TRUE
 171                 ||  ptr->lft->ntyp == TRUE)
 172                 {       ptr = ptr->rgt;
 173                         break;
 174                 }
 175                 if (isequal(ptr->lft, ptr->rgt))
 176                 {       /* p V p = p */
 177                         ptr = ptr->rgt;
 178                         break;
 179                 }
 180                 /* F V (p V q) == F V q */
 181                 if (ptr->lft->ntyp == FALSE
 182                 &&  ptr->rgt->ntyp == V_OPER)
 183                 {       ptr->rgt = ptr->rgt->rgt;
 184                         break;
 185                 }
 186                 /* p V (F V q) == F V q */
 187                 if (ptr->rgt->ntyp == V_OPER
 188                 &&  ptr->rgt->lft->ntyp == FALSE)
 189                 {       ptr->lft = False;
 190                         ptr->rgt = ptr->rgt->rgt;
 191                         break;
 192                 }
 193 #endif
 194                 break;
 195         case IMPLIES:
 196 #ifndef NO_OPT
 197                 if (isequal(ptr->lft, ptr->rgt))
 198                 {       ptr = True;
 199                         break;
 200                 }
 201 #endif
 202                 ptr = tl_nn(OR, Not(ptr->lft), ptr->rgt);
 203                 ptr = rewrite(ptr);
 204                 break;
 205         case EQUIV:
 206 #ifndef NO_OPT
 207                 if (isequal(ptr->lft, ptr->rgt))
 208                 {       ptr = True;
 209                         break;
 210                 }
 211 #endif
 212                 a = rewrite(tl_nn(AND,
 213                         dupnode(ptr->lft),
 214                         dupnode(ptr->rgt)));
 215                 b = rewrite(tl_nn(AND,
 216                         Not(ptr->lft),
 217                         Not(ptr->rgt)));
 218                 ptr = tl_nn(OR, a, b);
 219                 ptr = rewrite(ptr);
 220                 break;
 221         case AND:
 222 #ifndef NO_OPT
 223                 /* p && (q U p) = p */
 224                 if (ptr->rgt->ntyp == U_OPER
 225                 &&  isequal(ptr->rgt->rgt, ptr->lft))
 226                 {       ptr = ptr->lft;
 227                         break;
 228                 }
 229                 if (ptr->lft->ntyp == U_OPER
 230                 &&  isequal(ptr->lft->rgt, ptr->rgt))
 231                 {       ptr = ptr->rgt;
 232                         break;
 233                 }
 234
 235                 /* p && (q V p) == q V p */
 236                 if (ptr->rgt->ntyp == V_OPER
 237                 &&  isequal(ptr->rgt->rgt, ptr->lft))
 238                 {       ptr = ptr->rgt;
 239                         break;
 240                 }
 241                 if (ptr->lft->ntyp == V_OPER
 242                 &&  isequal(ptr->lft->rgt, ptr->rgt))
 243                 {       ptr = ptr->lft;
 244                         break;
 245                 }
 246
 247                 /* (p U q) && (r U q) = (p && r) U q*/
 248                 if (ptr->rgt->ntyp == U_OPER
 249                 &&  ptr->lft->ntyp == U_OPER
 250                 &&  isequal(ptr->rgt->rgt, ptr->lft->rgt))
 251                 {       ptr = tl_nn(U_OPER,
 252                                 tl_nn(AND, ptr->lft->lft, ptr->rgt->lft),
 253                                 ptr->lft->rgt);
 254                         break;
 255                 }
 256
 257                 /* (p V q) && (p V r) = p V (q && r) */
 258                 if (ptr->rgt->ntyp == V_OPER
 259                 &&  ptr->lft->ntyp == V_OPER
 260                 &&  isequal(ptr->rgt->lft, ptr->lft->lft))
 261                 {       ptr = tl_nn(V_OPER,
 262                                 ptr->rgt->lft,
 263                                 tl_nn(AND, ptr->lft->rgt, ptr->rgt->rgt));
 264                         break;
 265                 }
 266 #ifdef NXT
 267                 /* X p && X q == X (p && q) */
 268                 if (ptr->rgt->ntyp == NEXT
 269                 &&  ptr->lft->ntyp == NEXT)
 270                 {       ptr = tl_nn(NEXT,
 271                                 tl_nn(AND,
 272                                         ptr->rgt->lft,
 273                                         ptr->lft->lft), ZN);
 274                         break;
 275                 }
 276 #endif
 277
 278                 if (isequal(ptr->lft, ptr->rgt) /* (p && p) == p */
 279                 ||  ptr->rgt->ntyp == FALSE     /* (p && F) == F */
 280                 ||  ptr->lft->ntyp == TRUE)     /* (T && p) == p */
 281                 {       ptr = ptr->rgt;
 282                         break;
 283                 }
 284                 if (ptr->rgt->ntyp == TRUE      /* (p && T) == p */
 285                 ||  ptr->lft->ntyp == FALSE)    /* (F && p) == F */
 286                 {       ptr = ptr->lft;
 287                         break;
 288                 }
 289
 290                 /* (p V q) && (r U q) == p V q */
 291                 if (ptr->rgt->ntyp == U_OPER
 292                 &&  ptr->lft->ntyp == V_OPER
 293                 &&  isequal(ptr->lft->rgt, ptr->rgt->rgt))
 294                 {       ptr = ptr->lft;
 295                         break;
 296                 }
 297 #endif
 298                 break;
 299
 300         case OR:
 301 #ifndef NO_OPT
 302                 /* p || (q U p) == q U p */
 303                 if (ptr->rgt->ntyp == U_OPER
 304                 &&  isequal(ptr->rgt->rgt, ptr->lft))
 305                 {       ptr = ptr->rgt;
 306                         break;
 307                 }
 308
 309                 /* p || (q V p) == p */
 310                 if (ptr->rgt->ntyp == V_OPER
 311                 &&  isequal(ptr->rgt->rgt, ptr->lft))
 312                 {       ptr = ptr->lft;
 313                         break;
 314                 }
 315
 316                 /* (p U q) || (p U r) = p U (q || r) */
 317                 if (ptr->rgt->ntyp == U_OPER
 318                 &&  ptr->lft->ntyp == U_OPER
 319                 &&  isequal(ptr->rgt->lft, ptr->lft->lft))
 320                 {       ptr = tl_nn(U_OPER,
 321                                 ptr->rgt->lft,
 322                                 tl_nn(OR, ptr->lft->rgt, ptr->rgt->rgt));
 323                         break;
 324                 }
 325
 326                 if (isequal(ptr->lft, ptr->rgt) /* (p || p) == p */
 327                 ||  ptr->rgt->ntyp == FALSE     /* (p || F) == p */
 328                 ||  ptr->lft->ntyp == TRUE)     /* (T || p) == T */
 329                 {       ptr = ptr->lft;
 330                         break;
 331                 }
 332                 if (ptr->rgt->ntyp == TRUE      /* (p || T) == T */
 333                 ||  ptr->lft->ntyp == FALSE)    /* (F || p) == p */
 334                 {       ptr = ptr->rgt;
 335                         break;
 336                 }
 337
 338                 /* (p V q) || (r V q) = (p || r) V q */
 339                 if (ptr->rgt->ntyp == V_OPER
 340                 &&  ptr->lft->ntyp == V_OPER
 341                 &&  isequal(ptr->lft->rgt, ptr->rgt->rgt))
 342                 {       ptr = tl_nn(V_OPER,
 343                                 tl_nn(OR, ptr->lft->lft, ptr->rgt->lft),
 344                                 ptr->rgt->rgt);
 345                         break;
 346                 }
 347
 348                 /* (p V q) || (r U q) == r U q */
 349                 if (ptr->rgt->ntyp == U_OPER
 350                 &&  ptr->lft->ntyp == V_OPER
 351                 &&  isequal(ptr->lft->rgt, ptr->rgt->rgt))
 352                 {       ptr = ptr->rgt;
 353                         break;
 354                 }
 355 #endif
 356                 break;
 357         }
 358         return ptr;
 359 }
 360
 361 static Node *
 362 tl_level(int nr)
 363 {       int i; Node *ptr = ZN;
 364
 365         if (nr < 0)
 366                 return tl_factor();
 367
 368         ptr = tl_level(nr-1);
 369 again:
 370         for (i = 0; i < 4; i++)
 371                 if (tl_yychar == prec[nr][i])
 372                 {       tl_yychar = tl_yylex();
 373                         ptr = tl_nn(prec[nr][i],
 374                                 ptr, tl_level(nr-1));
 375                         ptr = bin_simpler(ptr);
 376                         goto again;
 377                 }
 378         if (!ptr) tl_yyerror("syntax error");
 379 #if 0
 380         printf("level %d:       ", nr);
 381         tl_explain(ptr->ntyp);
 382         printf("\n");
 383 #endif
 384         return ptr;
 385 }
 386
 387 static Node *
 388 tl_formula(void)
 389 {       tl_yychar = tl_yylex();
 390         return tl_level(1);     /* 2 precedence levels, 1 and 0 */
 391 }
 392
 393 void
 394 tl_parse(void)
 395 {       Node *n;
 396
 397         /* tl_verbose = 1; */
 398         n = tl_formula();
 399         if (tl_verbose)
 400         {       printf("formula: ");
 401                 dump(n);
 402                 printf("\n");
 403         }
 404         if (tl_Getchar() != -1)
 405         {       tl_yyerror("syntax error");
 406                 tl_errs++;
 407                 return;
 408         }
 409         trans(n);
 410 }