From ea1898f88e2edcecf3a58923fcd1a5d2b87219a8 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 6 Nov 2010 19:47:03 +0000
Subject: Introducing Forr?!  Forr? is a tiny language that translates to
 Boogie.  The purpose of the language and verifier is to serve as a tutorial
 example for how to build a verifier on top of Boogie.

---
 Source/Forro/Parser.fsy | 115 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 115 insertions(+)
 create mode 100644 Source/Forro/Parser.fsy

(limited to 'Source/Forro/Parser.fsy')

diff --git a/Source/Forro/Parser.fsy b/Source/Forro/Parser.fsy
new file mode 100644
index 00000000..6fa41431
--- /dev/null
+++ b/Source/Forro/Parser.fsy
@@ -0,0 +1,115 @@
+%{
+
+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 }
-- 
cgit v1.2.3