From 776eb757b0e4b7b98ea9c7ca9bcee002eaf6bee2 Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 11 Jul 2011 13:52:58 -0700 Subject: - added Set.jen example - fixed implementation for sets - generalized unification rules - added command line options - removed the "Exact" active pattern for strings (the same thing is already supported by F#) - added a ternary if-then-else expression to Jennisys langauge and IteExpr and SetExpr to AST --- Jennisys/Parser.fsy | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'Jennisys/Parser.fsy') diff --git a/Jennisys/Parser.fsy b/Jennisys/Parser.fsy index 5053bd18..395ee223 100644 --- a/Jennisys/Parser.fsy +++ b/Jennisys/Parser.fsy @@ -26,7 +26,7 @@ let rec MyFold ee acc = %token IMPLIES %token IFF %token LPAREN RPAREN LBRACKET RBRACKET LCURLY RCURLY VERTBAR -%token GETS COLON COLONCOLON COMMA +%token GETS COLON COLONCOLON COMMA QMARK %token CLASS MODEL CODE %token VAR CONSTRUCTOR METHOD FRAME INVARIANT RETURNS REQUIRES ENSURES FORALL %token INTTYPE BOOLTYPE SEQTYPE SETTYPE @@ -134,9 +134,12 @@ Expr10: | Expr10 IFF Expr20 { BinaryExpr(10,"<==>",$1,$3) } Expr20: - | Expr30 { $1 } - | Expr30 IMPLIES Expr20 { BinaryExpr(20,"==>",$1,$3) } + | 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 } @@ -183,6 +186,7 @@ Expr100: | 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, $4) } -- cgit v1.2.3