diff options
| author |  rustanleino <unknown> | 2010-01-06 23:53:45 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-01-06 23:53:45 +0000 |
| commit | e143e726c93a44737dd12dcabe2858a9119cd541 (patch) | |
| tree | 18c7b59e6722f5f202801d3e8ae3e567517c9b52 /Chalice | |
| parent | d5f09caee2ca7395d0a3dae6c29d7d10a6bc1de9 (diff) | |
Chalice: updated Prelude to match new Boogie parsing of function parameters; fixed minor bug in Chalice grammar
Diffstat (limited to 'Chalice')
| -rw-r--r-- | Chalice/src/Parser.scala | 2 | ||||
| -rw-r--r-- | Chalice/src/Prelude.scala | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala index a92e5b40..4442526f 100644 --- a/Chalice/src/Parser.scala +++ b/Chalice/src/Parser.scala @@ -447,7 +447,7 @@ class Parser extends StandardTokenParsers { }
| "|" ~> expression <~ "|" ^^ Length
| ("eval" ~ "(") ~> (evalstate <~ ",") ~ (expression <~ ")") ^^ { case h ~ e => Eval(h, e) }
- | ("ite(" ~> expression <~ ",") ~ (expression <~ ",") ~ (expression <~ ")") ^^ {
+ | ("ite" ~> "(" ~> expression <~ ",") ~ (expression <~ ",") ~ (expression <~ ")") ^^ {
case con ~ then ~ els => IfThenElse (con, then, els) }
| "(" ~> expression <~ ")"
| forall
diff --git a/Chalice/src/Prelude.scala b/Chalice/src/Prelude.scala index 28442308..3dcc0ccb 100644 --- a/Chalice/src/Prelude.scala +++ b/Chalice/src/Prelude.scala @@ -176,7 +176,7 @@ axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) } (forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
-function Seq#Take<T>(Seq T, howMany: int) returns (Seq T);
+function Seq#Take<T>(s: Seq T, howMany: int) returns (Seq T);
axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }
0 <= n ==>
(n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&
@@ -185,7 +185,7 @@ axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } 0 <= j && j < n && j < Seq#Length(s) ==>
Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));
-function Seq#Drop<T>(Seq T, howMany: int) returns (Seq T);
+function Seq#Drop<T>(s: Seq T, howMany: int) returns (Seq T);
axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }
0 <= n ==>
(n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&
|