%{

open Ast
open Getters
open AstUtils

let rec MyFold ee acc =
  match ee with
    | [] -> acc
    | x::rest -> BinaryAnd x (MyFold rest acc)

%}

// The start token becomes a parser function in the compiled code:
%start start

// These are the terminal tokens of the grammar along with the types of
// the data carried by each token:
%token <string> ID
%token <int> INTEGER
%token DOT
%token NOT
%token STAR DIV MOD
%token PLUS MINUS
%token OLD
%token DOTDOT DOTDOTDOT
%token EQ NEQ LESS ATMOST ATLEAST GREATER IN NOTIN
%token AND OR
%token IMPLIES
%token IFF
%token LPAREN RPAREN LBRACKET RBRACKET LCURLY RCURLY VERTBAR
%token GETS COLON COLONCOLON COMMA QMARK
%token INTERFACE DATAMODEL CODE
%token VAR CONSTRUCTOR METHOD FRAME INVARIANT RETURNS REQUIRES ENSURES FORALL
%token INTTYPE BOOLTYPE SEQTYPE SETTYPE
%token EOF

// This is the type of the data produced by a successful reduction of the 'start'
// symbol:
%type < Ast.SyntacticProgram > start

%%

// These are the rules of the grammar along with the F# code of the 
// actions executed as rules are reduced.  In this case the actions 
// produce data using F# data construction terms.
start: TopLevelDecls EOF     { SProgram($1) }

TopLevelDecls:
    |                             { [] }
    | TopLevelDecl TopLevelDecls  { $1 :: $2 }

TopLevelDecl:
    | INTERFACE ID TypeParams LCURLY Members RCURLY       { Interface($2, $3, $5) }
    | DATAMODEL ID TypeParams LCURLY FrameMembers RCURLY  { match $5 with (vv,fr,inv) -> DataModel($2, $3, vv, fr, inv) }
    | CODE ID TypeParams LCURLY RCURLY                { Code($2, $3) }

TypeParams:
    |                          { [] }
    | LBRACKET IdList RBRACKET { $2 }

IdList:
    | ID            { [$1] }
    | ID IdList     { $1 :: $2 }

Members:
    |                      { [] }
    | Member Members       { $1 :: $2 }

Signature:
    | LPAREN VarDeclList RPAREN  { Sig($2, []) }
    | LPAREN VarDeclList RPAREN RETURNS LPAREN VarDeclList RPAREN  { Sig($2, $6) }

Pre:
    |                           { TrueLiteral }
    | REQUIRES Expr Pre         { BinaryAnd $2 $3 }

Post: 
  |                           { TrueLiteral }
  | ENSURES Expr Post         { BinaryAnd $2 $3 }
  | ID GETS Expr Post         { BinaryAnd (BinaryExpr(40,"=",IdLiteral($1),$3)) $4 }

StmtList:
    |                    { [] }
    | Stmt StmtList      { $1 :: $2 }

Stmt:
    | BlockStmt          { $1 }
    | Expr GETS Expr     { Assign($1, $3) }

BlockStmt:
    | LCURLY StmtList RCURLY   { Block $2 }

Member:
    | VAR VarDecl                            { Field($2) }
    | CONSTRUCTOR ID Signature Pre Post      { Method($2, $3, RewriteVars (GetSigVars $3) $4, RewriteVars (GetSigVars $3) $5, true) }
    | METHOD ID Signature Pre Post           { Method($2, $3, RewriteVars (GetSigVars $3) $4, RewriteVars (GetSigVars $3) $5, false) }
	  | INVARIANT ExprList                     { Invariant($2) }

FrameMembers:
    |                                        { [], [], TrueLiteral }
    | VAR VarDecl FrameMembers               { match $3 with (vv,fr,inv) -> $2 :: vv, fr, inv }
    | FRAME FrameMembers                     { $2 }
    | FRAME FramePartitionList FrameMembers  { match $3 with (vv,fr,inv) -> vv, List.append $2 fr, inv }
    | INVARIANT ExprList FrameMembers        { match $3 with (vv,fr,inv) -> vv, fr, MyFold $2 inv }

FramePartitionList:
    | FramePartition                     { $1 }
    | FramePartition FramePartitionList  { List.append $1 $2 }

VarDeclList:
    |                           { [] }
    | VarDecl                   { [$1] }
    | VarDecl COMMA VarDeclList { $1 :: $3 }

VarDecl:
    | ID               { Var($1,None, false) }
    | ID COLON Type    { Var($1,Some($3), false) }

Type:
    | INTTYPE                        { IntType }
    | BOOLTYPE                       { BoolType }
    | ID                             { NamedType($1, []) }
    | SEQTYPE LBRACKET Type RBRACKET { SeqType($3) }
    | SETTYPE LBRACKET Type RBRACKET { SetType($3) }
    | ID LBRACKET Type RBRACKET      { InstantiatedType($1, [$3]) }

ExprList:
    |                   { [] }
    | Expr              { [$1] }
    | Expr ExprList     { $1 :: $2 }

Expr:
    | Expr10            { $1 }

Expr10:
    | Expr20            { $1 }
    | Expr10 IFF Expr20 { BinaryExpr(10,"<==>",$1,$3) }

Expr20:
    | Expr25                { $1 }
    | Expr25 IMPLIES Expr20 { BinaryExpr(20,"==>",$1,$3) }

Expr25: 
    | Expr30                { $1 }
    | Expr30 QMARK Expr25 COLON Expr25 { IteExpr($1,$3,$5) }
Expr30:
    | Expr40                { $1 }
    | Expr40 AND Expr30and  { BinaryAnd $1 $3 }
    | Expr40 OR Expr30or    { BinaryOr  $1 $3 }
Expr30and:
    | Expr40                { $1 }
    | Expr40 AND Expr30and  { BinaryAnd $1 $3 }
Expr30or:
    | Expr40                { $1 }
    | Expr40 AND Expr30or   { BinaryOr $1 $3 }
                                           
Expr40:
    | Expr50                { $1 }
    | Expr50 EQ Expr50      { BinaryExpr(40,"=",$1,$3) }
    | Expr50 NEQ Expr50     { BinaryExpr(40,"!=",$1,$3) }
    | Expr50 LESS Expr50    { BinaryExpr(40,"<",$1,$3) }
    | Expr50 ATMOST Expr50  { BinaryExpr(40,"<=",$1,$3) }
    | Expr50 ATLEAST Expr50 { BinaryExpr(40,">=",$1,$3) }
    | Expr50 GREATER Expr50 { BinaryExpr(40,">",$1,$3) }
    | Expr50 IN Expr50      { BinaryExpr(40,"in",$1,$3) }
    | Expr50 NOTIN Expr50   { BinaryExpr(40,"!in",$1,$3) }
    
Expr50:
    | Expr55                   { $1 }
    | Expr55 DOTDOTDOT Expr55  { BinaryExpr(50,"...",$1,$3) }        

Expr55:
    | Expr60               { $1 }
    | Expr55 PLUS Expr60   { BinaryExpr(55,"+",$1,$3) }
    | Expr55 MINUS Expr60  { BinaryExpr(55,"-",$1,$3) }

Expr60:
    | Expr90              { $1 }
    | Expr60 STAR Expr90  { BinaryExpr(60,"*",$1,$3) }
    | Expr60 DIV Expr90   { BinaryExpr(60,"div",$1,$3) }
    | Expr60 MOD Expr90   { BinaryExpr(60,"mod",$1,$3) }

Expr90:
  | Expr100                  { $1 }
  | OLD LPAREN Expr90 RPAREN { OldExpr($3) }
  | NOT Expr90               { UnaryExpr("!", $2) }
  | MINUS Expr90             { UnaryExpr("-", $2) }
  | Expr90 DOTDOT            { LCIntervalExpr($1) }

Expr100:
  | INTEGER                                  { IntLiteral($1) }
  | ID                                       { if $1 = "this" then
                                                 ObjLiteral("this")
                                               elif $1 = "null" then
                                                 ObjLiteral("null")
                                               else
                                                 IdLiteral($1) }
  | Expr100 DOT ID                           { Dot($1, $3) }
  | Expr100 LBRACKET StarExpr RBRACKET       { SelectExpr($1, $3) }
  | Expr100 LBRACKET Expr GETS Expr RBRACKET { UpdateExpr($1, $3, $5) }
  | LPAREN Expr RPAREN                       { $2 }
  | LBRACKET ExprList RBRACKET               { SequenceExpr($2) }
  | LCURLY ExprList RCURLY                   { SetExpr($2) }
  | VERTBAR Expr VERTBAR                     { SeqLength($2) }
  | FORALL VarDeclList COLONCOLON Expr       { ForallExpr($2, RewriteVars $2 $4) }

StarExpr:
  | STAR                  { Star }
  | Expr                  { $1 }

FramePartition:
  | Expr100                     { [$1] }
  | Expr100 STAR FramePartition { $1 :: $3 }