1 files changed, 45 insertions, 19 deletions

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 
 
 %%