%{

open Forro

exception ParseError of string

let StringsToVariables ss = [ for s in ss -> Var(s) ]

let IdToField id =
    match id with
    | "head" -> Field.Head
    | "tail" -> Field.Tail
    | "valid" -> Field.Valid
    | _ -> raise (ParseError ("illegal field selector: '" + id + "' (legal selectors are 'head', 'tail', and 'valid')"))

%}

// 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 <System.Int32> INT32
%token NULL
%token DOT
%token NOT
%token STAR
%token PLUS MINUS
%token EQ NEQ LESS ATMOST
%token AND OR
%token OLD LPAREN RPAREN LCURLY RCURLY SEMI COMMA ASSIGN
%token PROCEDURE REQUIRES ENSURES DO END
%token NEW IF THEN ELSE WHILE INVARIANT CALL ASSERT
%token EOF

// This is the type of the data produced by a successful reduction of the 'start'
// symbol:
%type < Forro.Program > 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: Prog EOF { Prog(List.rev($1)) }

Prog: Proc { [$1] }
    | Prog Proc { $2 :: $1  }

Proc:
    PROCEDURE Signature ProcedureSpec
    DO StmtList END SEMI
    { match $2, $3 with (outs,id,ins), (req,ens) -> Proc(id, StringsToVariables ins, StringsToVariables outs, req, ens, $5) }

ProcedureSpec:
      REQUIRES Expression ENSURES Expression { $2, $4 }

Signature:
      ID LPAREN IdList RPAREN                { [], $1, $3 }
    | ID LPAREN RPAREN                       { [], $1, [] }
    | IdList ASSIGN ID LPAREN IdList RPAREN  { $1, $3, $5 }
    | IdList ASSIGN ID LPAREN RPAREN         { $1, $3, [] }

IdList: ID      { [$1] }
    | ID COMMA IdList { $1 :: $3 }

Expression:
      AtomicExpr { $1 }
    | NOT Expression { Not($2) }
    | Expression PLUS Expression { Binary(Operator.Plus, $1, $3) }
    | Expression MINUS Expression { Binary(Operator.Minus, $1, $3) }
    | Expression STAR Expression { Binary(Operator.Times, $1, $3) }
    | Expression EQ Expression { Binary(Operator.Eq, $1, $3) }
    | Expression NEQ Expression { Binary(Operator.Neq, $1, $3) }
    | Expression LESS Expression { Binary(Operator.Less, $1, $3) }
    | Expression ATMOST Expression { Binary(Operator.AtMost, $1, $3) }
    | Expression AND Expression { Binary(Operator.And, $1, $3) }
    | Expression OR Expression { Binary(Operator.Or, $1, $3) }

AtomicExpr:
      INT32         { Constant($1) }
    | NULL          { Null }
    | ID            { Identifier(Var($1)) }
    | OLD LPAREN Expression RPAREN { Old($3) }
    | LPAREN Expression RPAREN { $2 }
    | FieldSelect { match $1 with e,f -> Select(e,f) }

FieldSelect:
    AtomicExpr DOT ID { $1, IdToField $3 }

ExprList:
    | Expression                { [$1] }
    | Expression COMMA ExprList { $1::$3 }

VarList:
    | ID ASSIGN        { [Var($1)] }
    | ID COMMA VarList { Var($1)::$3 }

StmtList:
    StmtListX  { Block($1) }

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

Stmt:
      ID ASSIGN Expression SEMI                           { Assign(Var($1), $3) }
    | ID ASSIGN NEW LPAREN Expression COMMA
                    Expression RPAREN SEMI                { Alloc(Var($1), $5, $7) }
    | FieldSelect ASSIGN Expression SEMI                  { match $1 with e,f -> Update(e, f, $3) }
    | IF Expression THEN StmtList ELSE StmtList END SEMI  { IfStmt($2,$4,$6) }
    | WHILE Expression Invariants DO StmtList END SEMI    { WhileStmt($2,$3,$5) }
    | CALL ID LPAREN RPAREN SEMI                          { CallStmt([],$2,[]) }
    | CALL ID LPAREN ExprList RPAREN SEMI                 { CallStmt([],$2,$4) }
    | CALL VarList ID LPAREN RPAREN SEMI                  { CallStmt($2,$3,[]) }
    | CALL VarList ID LPAREN ExprList RPAREN SEMI         { CallStmt($2,$3,$5) }
    | ASSERT Expression SEMI                              { Assert($2) }

Invariants:
                                       { [] }
    | INVARIANT Expression Invariants  { $2::$3 }