From 963a77a699432364ebabeeff4cd401ecd92b1be0 Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Tue, 24 Nov 2009 23:05:52 +0000
Subject: [PATCH] Parser should be complete for Booleans

---
 src/parser/parser_state.h |  8 +++--
 src/parser/pl.ypp         | 64 +++++++++++++++++++++++++++------------
 src/parser/pl_scanner.lpp |  3 ++
 3 files changed, 54 insertions(+), 21 deletions(-)

diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index 1d013a0b4..0fbedb958 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -21,6 +21,7 @@
 #include <sstream>
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
+#include "parser/symbol_table.h"
 #include "util/exception.h"
 
 namespace CVC4 {
@@ -40,8 +41,9 @@ private:
   // The currently used prompt
   std::string prompt;
 public:
-  SmtEngine* vc;
+  SmtEngine* smtEngine;
   ExprManager* exprManager;
+  SymbolTable* symbolTable;
   std::istream* is;
   // The current input line
   int lineNum;
@@ -66,7 +68,9 @@ public:
                   prompt1("CVC> "),
                   prompt2("- "),
                   prompt("CVC> "),
-                  vc(0),
+                  smtEngine(0),
+                  exprManager(0),
+                  symbolTable(0),
                   is(0),
                   lineNum(1),
                   fileName(),
diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index b59c7c69e..20687b783 100644
--- a/src/parser/pl.ypp
+++ b/src/parser/pl.ypp
@@ -13,6 +13,11 @@
 
 %{
 
+
+#include <vector>
+#include <list>
+#include <string>
+
 #include "smt/smt_engine.h"
 #include "parser/parser_exception.h"
 #include "parser/parser_state.h"
@@ -32,8 +37,9 @@ namespace CVC4 {
 // Define shortcuts for various things
 // #define TMP CVC4::parser::parserState
 // #define EXPR CVC4::parser::parserState->expr
-// #define VC (CVC4::parser::parserState->vc)
-#define EM (CVC4::parser::parserState->exprManager)
+#define SMT_ENGINE (CVC4::parser::parserState->smtEngine)
+#define EXPR_MANAGER (CVC4::parser::parserState->exprManager)
+#define SYMBOL_TABLE (CVC4::parser::parserState->symbolTable)
 // #define RAT(args) CVC4::newRational args
 
 // Suppress the bogus warning suppression in bison (it generates
@@ -65,6 +71,7 @@ using namespace CVC4;
   CVC4::Expr *expr;
   CVC4::Command *cmd;
   std::vector<CVC4::Expr> *vec;
+  std::list<std::string> *strlst;
   int kind;
 };
 
@@ -272,7 +279,8 @@ using namespace CVC4;
 // %type <node> TypeLetDecl TypeLetExpr TypeLetDeclsNode
 // %type <node> BoundVarDecl BoundVarDeclNode VarDecl
 // %type <node> ConstDecl TypeDecl 
- // %type <expr> Identifier // StringLiteral Numeral Binary Hex
+%type <strlst> IdentifierList // StringLiteral Numeral Binary Hex
+%type <str> Identifier // Type
 
 %type <cmd> cmd /// Assert Query Help Dbg Trace Option  
 // %type <node> Transform Print Call Echo DumpCommand
@@ -300,47 +308,65 @@ cmd:
     }
   | CHECKSAT_TOK {
       $$ = new CheckSatCommand();
-    } ;
+    } 
+  | IdentifierList ':' Type { // variable/constant declaration
+      // FIXME: assuming Type is BOOLEAN
+      SYMBOL_TABLE->defineVarList($1, (const void *)0);
+    }
 
 Expr:	
-//    Identifier { $$ = $1; }
-//  | 
-    TRUELIT_TOK {
-      $$ = new Expr(EM->mkExpr(TRUE));
+    Identifier { 
+      $$ = new Expr(SYMBOL_TABLE->lookupVar($1)); 
+    }
+  | TRUELIT_TOK {
+      $$ = new Expr(EXPR_MANAGER->mkExpr(TRUE));
     }
   | FALSELIT_TOK {
-      $$ = new Expr(EM->mkExpr(FALSE));
+      $$ = new Expr(EXPR_MANAGER->mkExpr(FALSE));
     }
   | Expr OR_TOK Expr {
-      $$ = new Expr(EM->mkExpr(OR, *$1, *$3));
+      $$ = new Expr(EXPR_MANAGER->mkExpr(OR, *$1, *$3));
       delete $1;
       delete $3;
     } 
   | Expr AND_TOK Expr {
-      $$ = new Expr(EM->mkExpr(AND, *$1, *$3));
+      $$ = new Expr(EXPR_MANAGER->mkExpr(AND, *$1, *$3));
       delete $1;
       delete $3;
     } 
   | Expr IMPLIES_TOK Expr {
-      $$ = new Expr(EM->mkExpr(IMPLIES, *$1, *$3));
+      $$ = new Expr(EXPR_MANAGER->mkExpr(IMPLIES, *$1, *$3));
       delete $1;
       delete $3;
     }
   | Expr IFF_TOK Expr {
-      $$ = new Expr(EM->mkExpr(IFF, *$1, *$3));
+      $$ = new Expr(EXPR_MANAGER->mkExpr(IFF, *$1, *$3));
       delete $1;
       delete $3;
     } 
   | NOT_TOK Expr {
-      $$ = new Expr(EM->mkExpr(NOT, *$2));
+      $$ = new Expr(EXPR_MANAGER->mkExpr(NOT, *$2));
       delete $2;
     } ;
 
+IdentifierList:
+    Identifier { 
+      $$ = new std::list<std::string>;
+      $$->push_front(*$1);
+      delete $1;
+    }
+  | Identifier ',' IdentifierList {
+      $3->push_front(*$1);
+      $$ = $3; 
+      delete $1;
+    }
+
+Identifier:
+    ID_TOK {
+      $$ = $1;
+    }
 
-// Identifier:
-//     ID_TOK {
-//         $$ = EM->mkExpr(VARIABLE, *$1);
-//         delete $1;
-//     }
+Type:	
+    BOOLEAN_TOK 
 
 %%
diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp
index 5ffd6b93b..f3b866f2d 100644
--- a/src/parser/pl_scanner.lpp
+++ b/src/parser/pl_scanner.lpp
@@ -21,6 +21,9 @@
 %{
 
 #include <iostream>
+#include <vector>
+#include <list>
+
 #include "expr/expr_manager.h" /* for the benefit of parsePL_defs.h */
 #include "util/command.h"
 #include "parser/parser_state.h"
-- 
2.30.2