diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-04-07 19:25:15 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-04-07 19:25:15 -0700 |
| commit | b2700fe1b2122237f658a340f6c202d479dbd7e5 (patch) | |
| tree | 4149ad9f7218cb7b0dcdebaf4812db7185bbcc20 /Jennisys | |
| parent | 78549b3bd1a98ec35726daa8637b3cc804505e56 (diff) | |
Jennisys: Refined parsing of expressions, frames, and routine bodies
Diffstat (limited to 'Jennisys')
| -rw-r--r-- | Jennisys/Jennisys/Parser.fsy | 20 | ||||
| -rw-r--r-- | Jennisys/Jennisys/Printer.fs | 2 |
2 files changed, 17 insertions, 5 deletions
diff --git a/Jennisys/Jennisys/Parser.fsy b/Jennisys/Jennisys/Parser.fsy index b4b663e1..d8ffd454 100644 --- a/Jennisys/Jennisys/Parser.fsy +++ b/Jennisys/Jennisys/Parser.fsy @@ -86,8 +86,13 @@ ConcreteVars: | VAR VarDecl ConcreteVars { $2 :: $3 }
Frame:
- | { [] }
- | FRAME ExprList { $2 }
+ | { [] }
+ | FRAME { [] }
+ | FRAME FramePartitionList { $2 }
+
+FramePartitionList:
+ | FramePartition { $1 }
+ | FramePartition FramePartitionList { List.append $1 $2 }
Invariant:
| { IdLiteral "true" }
@@ -163,11 +168,18 @@ Expr90: Expr100:
| INTEGER { IntLiteral($1) }
| ID { IdLiteral($1) }
- | STAR { Star }
| Expr100 DOT ID { Dot($1, $3) }
- | Expr100 LBRACKET Expr RBRACKET { SelectExpr($1, $3) }
+ | Expr100 LBRACKET StarExpr RBRACKET { SelectExpr($1, $3) }
| Expr100 LBRACKET Expr GETS Expr RBRACKET { UpdateExpr($1, $3, $5) }
| LPAREN Expr RPAREN { $2 }
| LBRACKET ExprList RBRACKET { SequenceExpr($2) }
| VERTBAR Expr VERTBAR { SeqLength($2) }
| FORALL VarDeclList COLONCOLON Expr { ForallExpr($2, $4) }
+
+StarExpr:
+ | STAR { Star }
+ | Expr { $1 }
+
+FramePartition:
+ | Expr100 { [$1] }
+ | Expr100 STAR FramePartition { $1 :: $3 }
diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs index d92817e9..eea67588 100644 --- a/Jennisys/Jennisys/Printer.fs +++ b/Jennisys/Jennisys/Printer.fs @@ -75,7 +75,7 @@ let PrintRoutine signature pre body = PrintSig signature
printfn ""
pre |> ForeachConjunct (fun e -> printf " requires " ; PrintExpr 0 e ; printfn "")
- PrintStmtList body 2
+ PrintStmtList body 4
let PrintMember m =
match m with
|