From e81b4fd1d8b384b7798b3d85048672d151dc86e2 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 9 Oct 2010 07:00:58 +0000
Subject: Chalice: * extended the cheap type inference to also consider "in"
 expressions and quantifiers * added some refinement keywords to the Emacs
 mode for Chalice

---
 Chalice/refinements/DuplicatesVideo.chalice | 4 ++--
 Chalice/src/Parser.scala                    | 2 ++
 Util/Emacs/chalice-mode.el                  | 1 +
 3 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/Chalice/refinements/DuplicatesVideo.chalice b/Chalice/refinements/DuplicatesVideo.chalice
index f4894faf..abb2a429 100644
--- a/Chalice/refinements/DuplicatesVideo.chalice
+++ b/Chalice/refinements/DuplicatesVideo.chalice
@@ -2,7 +2,7 @@ class Duplicates0 {
   method find(s:seq<int>) returns (b: bool)
     requires forall i in s :: i in [0..100];
   {
-    spec b [b <==> (exists i in [0..|s|] :: s[i] in s[..i])];
+    spec b [b <==> exists i in [0..|s|] :: s[i] in s[..i] ];
   }
 }
 
@@ -13,7 +13,7 @@ class Duplicates1 refines Duplicates0 {
     b := false;
     while (n < |s|)
       invariant 0 <= n && n <= |s|;
-      invariant b <==> (exists i in [0..n] :: s[i] in s[..i]);
+      invariant b <==> exists i in [0..n] :: s[i] in s[..i];
     {
       spec c:bool [c <==> s[n] in s[..n] ];
       b := b || c;
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index 2d3f99fc..27b4945d 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -274,6 +274,8 @@ class Parser extends StandardTokenParsers {
                          case Some(NewRhs(tid, _, _, _)) => Type(tid, Nil)
                          case Some(BoolLiteral(b)) => Type("bool", Nil)
                          case Some(x:BinaryExpr) if x.ResultType != null => new Type(x.ResultType);
+			 case Some(x:Contains) => Type("bool", Nil)
+			 case Some(x:Quantification) => Type("bool", Nil)
                          case _ => Type("int", Nil)
                        }
                    }, ghost, const)
diff --git a/Util/Emacs/chalice-mode.el b/Util/Emacs/chalice-mode.el
index 34a95a87..0798753e 100644
--- a/Util/Emacs/chalice-mode.el
+++ b/Util/Emacs/chalice-mode.el
@@ -33,6 +33,7 @@
         "class" "ghost" "var" "const" "external" "function" "method"
         "predicate" "returns" "requires" "ensures" "lockchange"
         "invariant" "channel" "condition" "where"
+        "refines" "replaces" "by" "transforms"
         )) . font-lock-builtin-face)
    `(,(chalice-regexp-opt '(
         "above" "acc" "acquire" "and" "assert" "assigned" "assume"
-- 
cgit v1.2.3