demos/rewrite-trick5.pC

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //
   3 //  This example program performs simplification of propositional logic
   4 //  formulas using rewriting.  We'll also define a parser to parses a
   5 //  logical formula from the input.
   6 //
   7 ///////////////////////////////////////////////////////////////////////////////
   8 #include <stdlib.h>
   9 #include <iostream.h>
  10 #include <AD/strings/quark.h>
  11 #include <AD/automata/iolexerbuf.h>
  12
  13 ///////////////////////////////////////////////////////////////////////////////
  14 //
  15 //  First, we define the type Wff (Well Formed Formulas) to represent
  16 //  our logic formulas.  Identifiers (type Id) are represented as
  17 //  atomic strings so that equality testing can be done quickly.
  18 //
  19 //  We also use pretty printing annotations to
  20 //  indicate to Prop to generate a simple print routine.
  21 //
  22 ///////////////////////////////////////////////////////////////////////////////
  23 class Rewrite {
  24    int state;
  25 public:
  26    Rewrite() : state(BURS::undefined_state) {}
  27    int get_wff_state() const { return state; }
  28    void set_wff_state(int s) { state = s; }
  29 };
  30
  31 datatype Wff : public Rewrite
  32    = True
  33    | False
  34    | Var (class Quark)  =>  _
  35    | And (Wff, Wff)     => "(" _ " and " _ ")"
  36    | Or  (Wff, Wff)     => "(" _ " or " _ ")"
  37    | Not (Wff)          => "not (" _ ")"
  38
  39    ////////////////////////////////////////////////////////////////////////////
  40    //
  41    //  The following set of laws abbreviate commonly used logical connectives.
  42    //
  43    ////////////////////////////////////////////////////////////////////////////
  44 law inline Implies(a,b) = Or(Not a, b)
  45 and inline Xor(a,b)     = Or(And(Not a,b),And(a,Not b))
  46 and inline Equiv(a,b)   = Or(And(a,b),And(Not a,Not b))
  47 ;
  48
  49 instantiate datatype Wff;
  50
  51 ///////////////////////////////////////////////////////////////////////////////
  52 //
  53 //  Next, we define the set of symbols used for our Wff parser.
  54 //
  55 ///////////////////////////////////////////////////////////////////////////////
  56 datatype WffToken :: lexeme =
  57    "[" | "]" | "(" | ")" | "*" | "+" | "->" | "<->"
  58 | "not" | "and" | "or" |  "xor" | ";" | "true" | "false" | "t" | "f"
  59 |  ID /[a-zA-Z][a-zA-Z0-9]*/
  60 ;
  61
  62 ///////////////////////////////////////////////////////////////////////////////
  63 //
  64 //  Next, we declare the interface of the parser.
  65 //
  66 ///////////////////////////////////////////////////////////////////////////////
  67 syntax class WffParser
  68 {  IOLexerBuffer lexbuf;
  69 public:
  70    int get_token();      // retrieve a token
  71    void process (Wff);   // process a Wff
  72 };
  73
  74 ///////////////////////////////////////////////////////////////////////////////
  75 //
  76 //  The lexer simply returns the tokens one by one; it also skip over the
  77 //  spaces and newlines.  If any unrecognized tokens are encountered,
  78 //  the program will terminate.
  79 //
  80 ///////////////////////////////////////////////////////////////////////////////
  81 int WffParser::get_token()
  82 {  matchscan while (lexbuf)
  83    {  lexeme class WffToken:  { return ?lexeme; }
  84    |  /[ \t\n]/: // skip spaces
  85    }
  86    return EOF;
  87 }
  88
  89 ///////////////////////////////////////////////////////////////////////////////
  90 //
  91 //  The parser is defined below.  Notice that the wffs are separated
  92 //  by semi-colons.  We call process() to simplify each one.
  93 //
  94 ///////////////////////////////////////////////////////////////////////////////
  95 syntax WffParser
  96 {
  97
  98    ////////////////////////////////////////////////////////////////////////////
  99    //
 100    //  Precedences.   Note that implication associates to the right.
 101    //
 102    ////////////////////////////////////////////////////////////////////////////
 103 left:  1 "not";
 104 left:  2 "*" "and" "xor";
 105 left:  3 "+" "or";
 106 right: 4 "->";
 107 left:  5 "<->";
 108
 109 command:
 110 |       wff ";" { process($1); } command
 111 |       ? ";" command  // for error recover, just skip to the next ;
 112 ;
 113
 114 wff Wff:  wff "+" wff   { $$ = Or($1,$3); }
 115 |         wff "*" wff   { $$ = And($1,$3); }
 116 |         wff "->" wff  { $$ = Implies($1,$3); }
 117 |         wff "<->" wff { $$ = Equiv($1,$3); }
 118 |         wff "and" wff { $$ = And($1,$3); }
 119 |         wff "or" wff  { $$ = Or($1,$3); }
 120 |         wff "xor" wff { $$ = Xor($1,$3); }
 121 |         "not" wff     { $$ = Not($2); }
 122 |         "(" wff ")"   { $$ = $2; }
 123 |         "[" wff "]"   { $$ = $2; }
 124 |         ID            { $$ = Var(lexbuf.text()); }
 125 |         "true"        { $$ = True; }
 126 |         "t"           { $$ = True; }
 127 |         "false"       { $$ = False; }
 128 |         "f"           { $$ = False; }
 129 ;
 130 };
 131
 132 ///////////////////////////////////////////////////////////////////////////////
 133 //
 134 //  For processing, we just transform the input formula a bit,
 135 //  then prints it out.  The rules are by no means exhaustive.
 136 //
 137 ///////////////////////////////////////////////////////////////////////////////
 138 void WffParser::process(Wff wff)
 139 {
 140    cout << "input = " << wff << '\n';
 141
 142    rewrite (wff) type (Wff) of
 143       index: Wff = wff;
 144
 145       And(True,X):     X
 146    |  And(X,True):     X
 147    |  And(False,_):    False
 148    |  And(_,False):    False
 149    |  Or(True,_):      True
 150    |  Or(_,True):      True
 151    |  Or(False,X):     X
 152    |  Or(X,False):     X
 153    |  Not True:        False
 154    |  Not False:       True
 155    |  Not(Not X):      X
 156    |  Not(And(X,Y)):   Or(Not(X),Not(Y))
 157    |  Not(Or(X,Y)):    And(Not(X),Not(Y))
 158    |  And(And(X,Y),Z): And(X,And(Y,Z))
 159    |  Or(Or(X,Y),Z):   Or(X,Or(Y,Z))
 160    |  And(a,b) | a==b:  a
 161    |  Or(a,b)  | a==b:  a
 162    |  And(X as Var a,Var b) | a == b: X
 163    |  Or(X as Var a,Var b) | a == b:  X
 164    |  And(X as Var a,Y as Var b) | a > b: And(Y,X)
 165    |  Or(X as Var a,Y as Var b) | a > b: Or(Y,X)
 166    |  And(X as Var a,And(Y as Var b,Z)) | a > b: And(Y,And(X,Z))
 167    |  Or(X as Var a,Or(Y as Var b,Z)) | a > b: Or(Y,Or(X,Z))
 168    |  And(X as Var a,And(Y as Var b,Z)) | a == b: Or(X,Z)
 169    |  Or(X as Var a,Or(Y as Var b,Z)) | a == b: Or(X,Z)
 170    end rewrite;
 171
 172    cout << "output = " << wff << '\n';
 173 }
 174
 175
 176 ///////////////////////////////////////////////////////////////////////////////
 177 //
 178 //  Finally, the main program simply instantiates a copy of the parser,
 179 //  and invoke the parse method.   By default, the input is from
 180 //  the standard input.
 181 //
 182 ///////////////////////////////////////////////////////////////////////////////
 183 int main()
 184 {
 185    WffParser P;
 186
 187    cerr << "Enter logical expressions terminated by a semicolon.\n";
 188    cerr << "Use t for true, f for false, + for or, * for and, etc.:\n";
 189
 190    P.parse();
 191
 192    exit(0);
 193 }