From 53809d5c20d63d869aed67e28d16d2206178cd0d Mon Sep 17 00:00:00 2001
From: kyessenov <unknown>
Date: Thu, 2 Sep 2010 20:01:33 +0000
Subject: Chalice: fix in refinement loop target resolution; added "spec" as a
 keyword synonym to "var"

---
 Chalice/src/Ast.scala           | 1 +
 Chalice/src/Parser.scala        | 3 ++-
 Chalice/src/PrettyPrinter.scala | 2 +-
 Chalice/src/Resolver.scala      | 1 +
 4 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'Chalice')

diff --git a/Chalice/src/Ast.scala b/Chalice/src/Ast.scala
index 7beba704..edeb52ba 100644
--- a/Chalice/src/Ast.scala
+++ b/Chalice/src/Ast.scala
@@ -268,6 +268,7 @@ case class RefinementBlock(con: List[Statement], abs: List[Statement]) extends S
     (a,c)
   }         
   override def Declares = con flatMap {_.Declares}
+  override def Targets = (con ++ abs :\ Set[Variable]()) { (s, vars) => vars ++ s.Targets}
 }
 
 /**
diff --git a/Chalice/src/Parser.scala b/Chalice/src/Parser.scala
index f086487d..2d3f99fc 100644
--- a/Chalice/src/Parser.scala
+++ b/Chalice/src/Parser.scala
@@ -31,7 +31,7 @@ class Parser extends StandardTokenParsers {
                        "ite", "fold", "unfold", "unfolding", "in", "forall", "exists",
                        "seq", "nil", "result", "eval", "token",
                        "wait", "signal", "unlimited", 
-                       "refines", "transforms", "replaces", "by"
+                       "refines", "transforms", "replaces", "by", "spec"
                       )
   // todo: can we remove "nil"?
   lexical.delimiters += ("(", ")", "{", "}", "[[", "]]",
@@ -158,6 +158,7 @@ class Parser extends StandardTokenParsers {
     | "assume" ~> expression <~ Semi ^^ Assume
     | blockStatement ^^ BlockStmt
     | "var" ~> localVarStmt(false, false)
+    | "spec" ~> localVarStmt(false, false)
     | "const" ~> localVarStmt(true, false)
     | "ghost" ~> "const" ~> localVarStmt(true, true)
     | "ghost" ~> "var" ~> localVarStmt(false, true)
diff --git a/Chalice/src/PrettyPrinter.scala b/Chalice/src/PrettyPrinter.scala
index 236e74cc..17e81923 100644
--- a/Chalice/src/PrettyPrinter.scala
+++ b/Chalice/src/PrettyPrinter.scala
@@ -321,7 +321,7 @@ object PrintProgram {
     case ExplicitSeq(es) =>
       print("["); ExprList(es); print("]");
     case Range(min, max) =>
-      print("("); Expr(min); print(":"); Expr(max); print(")");
+      print("["); Expr(min); print(":"); Expr(max); print("]");
     case Length(e)=>
       print("|"); Expr(e); print("|");
     case At(s, n) =>
diff --git a/Chalice/src/Resolver.scala b/Chalice/src/Resolver.scala
index 2729a0d5..7ccfe7e3 100644
--- a/Chalice/src/Resolver.scala
+++ b/Chalice/src/Resolver.scala
@@ -1109,6 +1109,7 @@ object Resolver {
              if (!inv.typ.IsBool) ctx.Error(inv.pos, "loop invariant must be boolean (found " + inv.typ.FullName + ")")
            }
            resolveBody(body.ss, ctx, locals)
+           w.LoopTargets = body.Targets.filter(ctx.IsVariablePresent).toList
          case IfStmt(_, thn, None) =>
            resolveBody(thn.ss, ctx, locals)
          case IfStmt(_, thn, Some(els)) =>
-- 
cgit v1.2.3