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