Rewriting system.

jvm/src/test/scala/org/sireum/logika/example/list.sc

@@ -0,0 +1,105 @@
+// #Sireum #Logika
+//@Logika: --par --par-branch --background disabled
+
+import org.sireum._
+
+import org.sireum.justification._
+
+@datatype trait List[T]
+
+object List {
+
+  @datatype class Nil[T] extends List[T]
+
+  @datatype class Cons[T](val value: T, val next: List[T]) extends List[T]
+
+  type Map[K, V] = List[(K, V)]
+
+  object Map {
+
+    @tailrec @abs def lookup[K, V](map: Map[K, V], key: K): V = map match {
+      case Cons((k, v), next) => if (k ≡ key) v else lookup(next, key)
+      case _ => halt(s"Could not lookup $key")
+    }
+
+    @abs def update[K, V](map: Map[K, V], key: K, value: V): Map[K, V] = map match {
+      case Cons(p, next) =>
+        if (p._1 ≡ key) Cons(key ~> value, next)
+        else Cons(p, update(next, key, value))
+      case _ => Cons(key ~> value, Nil())
+    }
+
+    @pure def lookupUpdateEq[K, V](map: Map[K, V], key: K, value: V): Unit = {
+      Contract(
+        Ensures(lookup(update(map, key, value), key) ≡ value)
+      )
+
+      map match {
+        case Cons(p, next) => {
+
+          Deduce((  map ≡ Cons(p, next)  ) by Auto)
+
+          if (p._1 ≡ key) {
+
+            Deduce(
+              //@formatter:off
+              1  (  map ≡ Cons(p, next)                                 ) by Auto,
+              2  (  p._1 ≡ key                                          ) by Premise,
+              3  (  update(map, key, value) ≡ Cons(key ~> value, next)  ) by RSimpl(RS(update[K, V] _)), //Auto,
+              4  (  lookup(update(map, key, value), key) ≡ value        ) by RSimpl(RS(lookup[K, V] _)) //Auto
+              //@formatter:on
+            )
+
+          } else {
+
+            Deduce(
+              //@formatter:off
+              1  (  map ≡ Cons(p, next)                                          ) by Auto,
+              2  (  p._1 ≢ key                                                   ) by Auto,
+              3  (  update(map, key, value) ≡ Cons(p, update(next, key, value))  ) by Auto,
+              4  (  lookup(Cons(p, update(next, key, value)), key) ≡
+                    lookup(update(next, key, value), key)                        ) by RSimpl(RS(lookup[K, V] _)),
+              5  (  lookup(Cons(p, update(next, key, value)), key) ≡ value       ) by Rewrite(RS(lookupUpdateEq[K, V] _), 4)
+              //@formatter:on
+            )
+
+          }
+        }
+        case _ => {
+
+          Deduce(
+            //@formatter:off
+            1  (  map ≡ Nil[(K, V)]()                                          ) by Auto,
+            2  (  update(map, key, value) ≡ Cons(key ~> value, Nil[(K, V)]())  ) by Auto,
+            3  (  lookup(update(map, key, value), key) ≡ value                 ) by Auto
+            //@formatter:on
+          )
+
+        }
+      }
+    }
+
+    @pure def lookupUpdateNe[K, V](map: Map[K, V], key1: K, key2: K, value: V): Unit = {
+      Contract(
+        Requires(key1 ≢ key2),
+        Ensures(lookup(update(map, key1, value), key2) ≡ lookup(map, key1))
+      )
+      map match {
+        case Cons(p, next) =>
+          Deduce(
+            //@formatter:off
+            1  (  map ≡ Cons(p, next)  ) by Auto
+            //@formatter:on
+          )
+        case _ =>
+          Deduce(
+            //@formatter:off
+            1  (  map ≡ Nil[(K, V)]()  ) by Auto
+            //@formatter:on
+          )
+      }
+      halt("TODO")
+    }
+
+  }
+}

shared/src/main/scala/org/sireum/logika/RewritingSystem.scala

@@ -609,7 +609,6 @@ object RewritingSystem {
                 i = i + 1
               }
               r = r :+ AST.CoreExp.condAnd(AST.CoreExp.InstanceOfExp(T, exp, t), AST.CoreExp.bigAnd(conds))
-              lMap = localMap
             case t: AST.Typed.Name =>
               var conds = ISZ[AST.CoreExp.Base]()
               if (t.ids == AST.Typed.isName || t.ids == AST.Typed.msName) {
@@ -651,7 +650,6 @@ object RewritingSystem {
                 }
               }
               r = r :+ AST.CoreExp.condAnd(AST.CoreExp.InstanceOfExp(T, exp, t), AST.CoreExp.bigAnd(conds))
-              lMap = localMap
             case _ => halt("Infeasible")
           }
         case pattern: AST.Pattern.Ref =>
@@ -696,7 +694,8 @@ object RewritingSystem {
     }
     @pure def translateStmt(stmt: AST.Stmt, funStack: FunStack, localMap: LocalMap): (Option[AST.CoreExp.Base], LocalMap) = {
       stmt match {
-        case stmt: AST.Stmt.Expr => return (Some(translateExp(stmt.exp, funStack, localMap)), localMap)
+        case stmt: AST.Stmt.Expr =>
+          return (Some(translateExp(stmt.exp, funStack, localMap)), localMap)
         case stmt: AST.Stmt.Var =>
           val res = stmt.attr.resOpt.get.asInstanceOf[AST.ResolvedInfo.LocalVar]
           return (None(), localMap + (res.context, res.id) ~>
@@ -830,7 +829,7 @@ object RewritingSystem {
             case _ => return translateExp(AST.Exp.Ident(e.id, e.attr), funStack, localMap)
           }
         case e: AST.Exp.If =>
-          return AST.CoreExp.ite(translateExp(e.cond, funStack, localMap), translateExp(e.elseExp, funStack, localMap),
+          return AST.CoreExp.ite(translateExp(e.cond, funStack, localMap), translateExp(e.thenExp, funStack, localMap),
             translateExp(e.elseExp, funStack, localMap), e.typedOpt.get)
         case e: AST.Exp.Fun =>
           val params: ISZ[(String, AST.Typed)] = for (p <- e.params) yield
@@ -867,7 +866,9 @@ object RewritingSystem {
         case e: AST.Exp.StrictPureBlock =>
           return translateStmt(e.block, funStack, localMap)._1.get
         case e: AST.Exp.Invoke =>
-          val args: ISZ[AST.CoreExp.Base] = for (arg <- e.args) yield translateExp(arg, funStack, localMap)
+          def args: ISZ[AST.CoreExp.Base] = {
+            return for (arg <- e.args) yield translateExp(arg, funStack, localMap)
+          }
           e.attr.resOpt.get match {
             case res: AST.ResolvedInfo.Method =>
               res.mode match {
@@ -902,6 +903,8 @@ object RewritingSystem {
                 case AST.MethodMode.Just => halt("Infeasible")
                 case AST.MethodMode.Copy => halt("Infeasible")
               }
+            case AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.Halt) =>
+              return AST.CoreExp.Abort
             case _ =>
           }
           e.receiverOpt match {