Rewriting system.

sireum · Mar 5, 2024 · e964d7f · e964d7f
1 parent 5c73080
commit e964d7f
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/jvm/src/test/scala/org/sireum/logika/example/list.sc b/jvm/src/test/scala/org/sireum/logika/example/list.sc
@@ -90,6 +90,8 @@ object List {
 
           } else {
 
+            lookupUpdateEq(next, key, value) // either this or proof step #5 below
+
             Deduce(
               //@formatter:off
               1 (  map ≡ Cons(p, next)                                          ) by Auto,

diff --git a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
@@ -126,6 +126,11 @@ object RewritingSystem {
         st"""Begin $title ${exp.prettyST} ..."""
     }
 
+    @datatype class BeginST(val title: ST) extends Trace {
+      @strictpure def toST: ST =
+        st"""Begin $title"""
+    }
+
     @datatype class Eval(val desc: ST,
                          val from: AST.CoreExp.Base,
                          val to: AST.CoreExp.Base) extends Trace {
@@ -2388,6 +2393,9 @@ object RewritingSystem {
           for (i <- 0 until params.size) {
             map = map + (params.size - i) ~> args(i)
           }
+          if (shouldTrace) {
+            trace = trace :+ Trace.BeginST(st"function application ${f.prettyST}(${(for (arg <- ops.ISZOps(args).slice(0, if (args.size > params.size) params.size else args.size)) yield arg.prettyST, ", ")})")
+          }
           evalBaseH(map, body) match {
             case Some(body2) =>
               if (args.size > params.size) {