/*********************                                           -*- C++ -*-  */
/** pl.ypp
 ** This file is part of the CVC4 prototype.
 ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
 ** Courant Institute of Mathematical Sciences
 ** New York University
 ** See the file COPYING in the top-level source directory for licensing
 ** information.
 **
 ** This file contains the bison code for the parser that reads in CVC
 ** commands in the presentation language (hence "PL").
 **/

%{


#include <list>
#include <vector>
#include <string>

#include "smt/smt_engine.h"
#include "parser/parser_exception.h"
#include "parser/parser_state.h"
#include "expr/expr.h"
#include "expr/expr_builder.h"
#include "expr/expr_manager.h"
#include "util/command.h"
//#include "rational.h"

// Exported shared data
namespace CVC4 {
  namespace parser {
    extern ParserState* parserState;
  }/* CVC4::parser namespace */
}/* CVC4 hnamespace */

// Define shortcuts for various things
// #define TMP CVC4::parser::parserState
// #define EXPR CVC4::parser::parserState->expr
#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
// compile error)
#undef __GNUC_MINOR__

/* stuff that lives in PL.lex */
extern int PLlex(void);

int PLerror(const char *s)
{
  std::ostringstream ss;
  ss << CVC4::parser::parserState->fileName << ":" << CVC4::parser::parserState->lineNum
     << ": " << s;
  CVC4::parser::parserState->error(ss.str());
  return 0;// dead code; error() above throws an exception
}

#define YYLTYPE_IS_TRIVIAL 1
#define YYMAXDEPTH 10485760
/* Prefer YYERROR_VERBOSE over %error-verbose to avoid errors in older bison */
#define YYERROR_VERBOSE 1

using namespace CVC4;

%}

%union {
  std::string *str;
  CVC4::Expr *expr;
  CVC4::Command *cmd;
  std::vector<CVC4::Expr> *vec;
  std::list<std::string> *strlst;
  int kind;
};


%start cmd
 // %start Query

/* strings are for better error messages.  
   "_TOK" is so macros don't conflict with kind names */

%token  DISTINCT_TOK    "DISTINCT"
%token	AND_TOK			"AND"
%token	ARRAY_TOK		"ARRAY"
%token	BOOLEAN_TOK		"BOOLEAN"
%token	DATATYPE_TOK		"DATATYPE"
%token	ELSE_TOK		"ELSE"
%token	ELSIF_TOK		"ELSIF"
%token	END_TOK			"END"
%token	ENDIF_TOK		"ENDIF"
%token	EXISTS_TOK		"EXISTS"
%token	FALSELIT_TOK		"FALSE"
%token	FORALL_TOK		"FORALL"
%token	IN_TOK			"IN"
%token	IF_TOK			"IF"
%token	LAMBDA_TOK		"LAMBDA"
%token	SIMULATE_TOK		"SIMULATE"
%token	LET_TOK			"LET"
%token	NOT_TOK			"NOT"
%token	IS_INTEGER_TOK		"IS_INTEGER"
%token	OF_TOK			"OF"
%token	OR_TOK			"OR"
%token	REAL_TOK		"REAL"
%token  INT_TOK                 "INT"
%token  SUBTYPE_TOK             "SUBTYPE"
%token  BITVECTOR_TOK           "BITVECTOR"
%token	THEN_TOK		"THEN"
%token	TRUELIT_TOK		"TRUE"
%token	TYPE_TOK		"TYPE"
%token	WITH_TOK		"WITH"
%token	XOR_TOK			"XOR"
%token	TCC_TOK			"TCC"
%token	PATTERN_TOK		"PATTERN"
%token '_'
%token  DONE_TOK

%token	DOTDOT_TOK		".."
%token	ASSIGN_TOK		":="
%token	NEQ_TOK			"/="
%token	IMPLIES_TOK		"=>"
%token	IFF_TOK			"<=>"
%token	PLUS_TOK		"+"
%token	MINUS_TOK		"-"
%token	MULT_TOK		"*"
%token	POW_TOK			"^"
%token	DIV_TOK			"/"
%token	MOD_TOK			"MOD"
%token	INTDIV_TOK		"DIV"
%token	LT_TOK			"<"
%token	LE_TOK			"<="
%token	GT_TOK			">"
%token	GE_TOK			">="
%token  FLOOR_TOK               "FLOOR"
%token  LEFTSHIFT_TOK            "<<"
%token  RIGHTSHIFT_TOK           ">>"
%token  BVPLUS_TOK              "BVPLUS"
%token  BVSUB_TOK               "BVSUB"
%token  BVUDIV_TOK              "BVUDIV"
%token  BVSDIV_TOK              "BVSDIV"
%token  BVUREM_TOK              "BVUREM"
%token  BVSREM_TOK              "BVSREM"
%token  BVSMOD_TOK              "BVSMOD"
%token  BVSHL_TOK               "BVSHL"
%token  BVASHR_TOK              "BVASHR"
%token  BVLSHR_TOK              "BVLSHR"
%token  BVUMINUS_TOK            "BVUMINUS"
%token  BVMULT_TOK              "BVMULT"
%token	SQHASH_TOK		"[#"
%token	HASHSQ_TOK		"#]"
%token	PARENHASH_TOK		"(#"
%token	HASHPAREN_TOK		"#)"
%token	ARROW_TOK		"->"
%token  BVNEG_TOK               "~"
%token  BVAND_TOK               "&"
%token  MID_TOK                 "|"
%token  BVXOR_TOK               "BVXOR"
%token  BVNAND_TOK              "BVNAND"
%token  BVNOR_TOK               "BVNOR"
%token  BVCOMP_TOK              "BVCOMP"
%token  BVXNOR_TOK              "BVXNOR"
%token  CONCAT_TOK              "@"
%token  BVTOINT_TOK             "BVTOINT"
%token  INTTOBV_TOK             "INTTOBV"
%token  BOOLEXTRACT_TOK         "BOOLEXTRACT"
%token  BVLT_TOK                "BVLT"
%token  BVGT_TOK                "BVGT"
%token  BVLE_TOK                "BVLE"
%token  BVGE_TOK                "BVGE"
%token  SX_TOK                  "SX"
%token  BVZEROEXTEND_TOK        "BVZEROEXTEND"
%token  BVREPEAT_TOK            "BVREPEAT"
%token  BVROTL_TOK              "BVROTL"
%token  BVROTR_TOK              "BVROTR"
%token  BVSLT_TOK               "BVSLT"
%token  BVSGT_TOK               "BVSGT"
%token  BVSLE_TOK               "BVSLE"
%token  BVSGE_TOK               "BVSGE"


/* commands given in prefix syntax */
%token  ARITH_VAR_ORDER_TOK     "ARITH_VAR_ORDER"
%token  ASSERT_TOK              "ASSERT"
%token  QUERY_TOK               "QUERY"
%token  CHECKSAT_TOK            "CHECKSAT"
%token  CONTINUE_TOK            "CONTINUE"
%token  RESTART_TOK             "RESTART"
%token  HELP_TOK                "HELP"
%token  DBG_TOK                 "DBG"
%token  TRACE_TOK               "TRACE"
%token  UNTRACE_TOK             "UNTRACE"
%token  OPTION_TOK              "OPTION"
%token  TRANSFORM_TOK           "TRANSFORM"
%token  PRINT_TOK               "PRINT"
%token  PRINT_TYPE_TOK          "PRINT_TYPE"
%token  CALL_TOK                "CALL"
%token  ECHO_TOK                "ECHO"
%token  INCLUDE_TOK             "INCLUDE"
%token  DUMP_PROOF_TOK          "DUMP_PROOF"
%token  DUMP_ASSUMPTIONS_TOK    "DUMP_ASSUMPTIONS"
%token  DUMP_SIG_TOK            "DUMP_SIG"
%token  DUMP_TCC_TOK            "DUMP_TCC"
%token  DUMP_TCC_ASSUMPTIONS_TOK "DUMP_TCC_ASSUMPTIONS"
%token  DUMP_TCC_PROOF_TOK      "DUMP_TCC_PROOF"
%token  DUMP_CLOSURE_TOK        "DUMP_CLOSURE"
%token  DUMP_CLOSURE_PROOF_TOK  "DUMP_CLOSURE_PROOF"
%token  WHERE_TOK               "WHERE"
%token  ASSERTIONS_TOK          "ASSERTIONS"
%token  ASSUMPTIONS_TOK         "ASSUMPTIONS"
%token  COUNTEREXAMPLE_TOK      "COUNTEREXAMPLE"
%token  COUNTERMODEL_TOK        "COUNTERMODEL"
%token  PUSH_TOK                "PUSH"
%token  POP_TOK                 "POP"
%token  POPTO_TOK               "POPTO"
%token  PUSH_SCOPE_TOK          "PUSH_SCOPE"
%token  POP_SCOPE_TOK           "POP_SCOPE"
%token  POPTO_SCOPE_TOK         "POPTO_SCOPE"
%token  RESET_TOK               "RESET"
%token  CONTEXT_TOK             "CONTEXT"
%token  FORGET_TOK              "FORGET"
%token  GET_TYPE_TOK            "GET_TYPE"
%token  CHECK_TYPE_TOK          "CHECK_TYPE"
%token  GET_CHILD_TOK           "GET_CHILD"
%token  GET_OP_TOK              "GET_OP"
%token  SUBSTITUTE_TOK          "SUBSTITUTE"

%nonassoc ASSIGN_TOK IN_TOK
%nonassoc FORALL_TOK EXISTS_TOK
%left IFF_TOK
%right IMPLIES_TOK
%left OR_TOK XOR_TOK 
%left AND_TOK
%left NOT_TOK

%nonassoc '=' NEQ_TOK
%nonassoc LE_TOK LT_TOK GE_TOK GT_TOK FLOOR_TOK
%left PLUS_TOK MINUS_TOK
%left MULT_TOK INTDIV_TOK DIV_TOK MOD_TOK
%left POW_TOK
%left WITH_TOK
%left UMINUS_TOK
%left CONCAT_TOK
%left MID_TOK
%left BVAND_TOK
%left BVXOR_TOK
%left BVNAND_TOK
%left BVNOR_TOK BVCOMP_TOK
%left BVXNOR_TOK
%left BVNEG_TOK
%left BVUMINUS_TOK BVPLUS_TOK BVSUB_TOK 
%left BVUDIV_TOK BVSDIV_TOK BVUREM_TOK BVSREM_TOK BVSMOD_TOK BVSHL_TOK BVASHR_TOK BVLSHR_TOK
%left SX_TOK BVZEROEXTEND_TOK BVREPEAT_TOK BVROTL_TOK BVROTR_TOK
%left LEFTSHIFT_TOK RIGHTSHIFT_TOK
%nonassoc BVLT_TOK BVLE_TOK BVGT_TOK BVGE_TOK 
%nonassoc BVSLT_TOK BVSLE_TOK BVSGT_TOK BVSGE_TOK 
%right IS_INTEGER_TOK
%left ARROW_TOK

%nonassoc '[' 
%nonassoc '{' '.' '('
%nonassoc BITVECTOR_TOK

// %type <vec> FieldDecls TypeList IDs reverseIDs SingleDataTypes Constructors
// %type <vec> LetDecls TypeLetDecls BoundVarDecls ElseRest VarDecls 
// %type <vec> Exprs AndExpr OrExpr Pattern Patterns
// %type <vec> RecordEntries UpdatePosition Updates

// %type <node> Type /* IndexType */ TypeNotIdentifier TypeDef
// %type <node> DataType SingleDataType Constructor
// %type <node> FunctionType RecordType Real Int BitvectorType
// %type <node> FieldDecl TupleType
// %type <node> ArrayType ScalarType SubType BasicType SubrangeType 
// %type <node> LeftBound RightBound
%type <expr> Expr // Conditional UpdatePositionNode Update Lambda
// %type <node> QuantExpr ArrayLiteral RecordLiteral RecordEntry TupleLiteral 
// %type <node> LetDecl LetExpr LetDeclsNode 
// %type <node> TypeLetDecl TypeLetExpr TypeLetDeclsNode
// %type <node> BoundVarDecl BoundVarDeclNode VarDecl
// %type <node> ConstDecl TypeDecl 
%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
// %type <node> Include Where Push Pop PopTo
// %type <node> Context Forget Get_Child Get_Op Get_Type Check_Type Substitute
// %type <node> other_cmd
// %type <node> Arith_Var_Order

%token <str> ID_TOK STRINGLIT_TOK NUMERAL_TOK HEX_TOK BINARY_TOK

%%

cmd:       
    ASSERT_TOK Expr { 
      $$ = new AssertCommand(*$2);
      delete $2;
    } 
  | QUERY_TOK Expr { 
      $$ = new QueryCommand(*$2);
      delete $2;
    }
  | CHECKSAT_TOK Expr {
      $$ = new CheckSatCommand(*$2);
      delete $2;
    }
  | CHECKSAT_TOK {
      $$ = new CheckSatCommand();
    } 
  | IdentifierList ':' Type { // variable/constant declaration
      // FIXME: assuming Type is BOOLEAN
      SYMBOL_TABLE->defineVarList($1, (const void *)0);
    }

Expr:	
    Identifier { 
      $$ = new Expr(SYMBOL_TABLE->lookupVar($1)); 
    }
  | TRUELIT_TOK {
      $$ = new Expr(EXPR_MANAGER->mkExpr(TRUE));
    }
  | FALSELIT_TOK {
      $$ = new Expr(EXPR_MANAGER->mkExpr(FALSE));
    }
  | Expr OR_TOK Expr {
      $$ = new Expr(EXPR_MANAGER->mkExpr(OR, *$1, *$3));
      delete $1;
      delete $3;
    } 
  | Expr AND_TOK Expr {
      $$ = new Expr(EXPR_MANAGER->mkExpr(AND, *$1, *$3));
      delete $1;
      delete $3;
    } 
  | Expr IMPLIES_TOK Expr {
      $$ = new Expr(EXPR_MANAGER->mkExpr(IMPLIES, *$1, *$3));
      delete $1;
      delete $3;
    }
  | Expr IFF_TOK Expr {
      $$ = new Expr(EXPR_MANAGER->mkExpr(IFF, *$1, *$3));
      delete $1;
      delete $3;
    } 
  | NOT_TOK Expr {
      $$ = 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;
    }

Type:	
    BOOLEAN_TOK 

%%