%{

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 PLUS MINUS
%token STAR
%token EQ NEQ LESS ATMOST
%token AND OR
%token OLD LPAREN RPAREN SEMI 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
    REQUIRES Expression ENSURES Expression
    DO StmtList END SEMI
    { match $2 with outs,id,ins -> Proc(id, StringsToVariables ins, StringsToVariables outs, $4, $6, $8) }

Signature:
      IdList                  { [], List.head $1, List.tail $1 }
    | IdList ASSIGN IdList    { $1, List.head $3, List.tail $3 }

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

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:  // possibly empty
                          { [] }
    | Expression ExprList { $1::$2 }

VarList:   // nonempty
    | ID ASSIGN        { [Var($1)] }
    | ID VarList { Var($1)::$2 }

StmtList:
    StmtListX  { Block($1) }

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

Stmt:
      ID ASSIGN Expression SEMI                           { Assign(Var($1), $3) }
    | ID ASSIGN NEW Expression Expression SEMI            { Alloc(Var($1), $4, $5) }
    | 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 ExprList RPAREN SEMI                 { CallStmt([],$2,$4) }
    | CALL VarList ID LPAREN ExprList RPAREN SEMI         { CallStmt($2,$3,$5) }
    | ASSERT Expression SEMI                              { Assert($2) }

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