Jennisys: change of keywords, now: interface/datamodel/code

Jennisys: allow assignment statements in interfaces (for now, these are syntactic sugar for ensures clauses)

1 files changed, 4 insertions, 3 deletions

diff --git a/Jennisys/Parser.fsy b/Jennisys/Parser.fsy
index 0cf9dba9..5072cc0f 100644
--- a/Jennisys/Parser.fsy
+++ b/Jennisys/Parser.fsy
@@ -28,7 +28,7 @@ let rec MyFold ee acc =
 %token IFF

 %token LPAREN RPAREN LBRACKET RBRACKET LCURLY RCURLY VERTBAR

 %token GETS COLON COLONCOLON COMMA QMARK

-%token CLASS MODEL CODE

+%token INTERFACE DATAMODEL CODE

 %token VAR CONSTRUCTOR METHOD FRAME INVARIANT RETURNS REQUIRES ENSURES FORALL

 %token INTTYPE BOOLTYPE SEQTYPE SETTYPE

 %token EOF

@@ -49,8 +49,8 @@ TopLevelDecls:
     | TopLevelDecl TopLevelDecls  { $1 :: $2 }

 

 TopLevelDecl:

-    | CLASS ID TypeParams LCURLY Members RCURLY       { Class($2, $3, $5) }

-    | MODEL ID TypeParams LCURLY FrameMembers RCURLY  { match $5 with (vv,fr,inv) -> Model($2, $3, vv, fr, inv) }

+    | 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:

@@ -76,6 +76,7 @@ Pre:
 Post: 

   |                           { TrueLiteral }

 	| ENSURES Expr Post         { BinaryAnd $2 $3 }

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

 

 StmtList:

     |                    { [] }