Rewriting system.

sireum · Feb 20, 2024 · 329c426 · 329c426
1 parent b34551f
commit 329c426
Show file tree

Hide file tree

Showing 7 changed files with 165 additions and 81 deletions.
diff --git a/jvm/src/main/scala/org/sireum/logika/NoTransitionSmt2Cache_Ext.scala b/jvm/src/main/scala/org/sireum/logika/NoTransitionSmt2Cache_Ext.scala
@@ -112,9 +112,9 @@ final class NoTransitionSmt2CacheImpl(val persistentCache: java.util.concurrent.
 
   def setSmt2(isSat: B, th: TypeHierarchy, config: Config, timeoutInMs: Z, claims: ISZ[State.Claim], result: Smt2Query.Result): Unit = {}
 
-  def getPatterns(th: TypeHierarchy, name: ISZ[String]): Option[ISZ[RewritingSystem.Rewriter.Pattern]] = None()
+  def getPatterns(th: TypeHierarchy, isInObject: B, name: ISZ[String]): Option[ISZ[RewritingSystem.Rewriter.Pattern]] = None()
 
-  def setPatterns(th: TypeHierarchy, name: ISZ[String], patterns: ISZ[RewritingSystem.Rewriter.Pattern]): Unit = {}
+  def setPatterns(th: TypeHierarchy, isInObject: B, name: ISZ[String], patterns: ISZ[RewritingSystem.Rewriter.Pattern]): Unit = {}
 
   def clearTaskCache(): Unit = {}
 

diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala
@@ -78,9 +78,9 @@ object Logika {
 
     def setSmt2(isSat: B, th: TypeHierarchy, config: Config, timeoutInMs: Z, claims: ISZ[State.Claim], result: Smt2Query.Result): Unit
 
-    def getPatterns(th: TypeHierarchy, name: ISZ[String]): Option[ISZ[RewritingSystem.Rewriter.Pattern]]
+    def getPatterns(th: TypeHierarchy, isInObject: B, name: ISZ[String]): Option[ISZ[RewritingSystem.Rewriter.Pattern]]
 
-    def setPatterns(th: TypeHierarchy, name: ISZ[String], patterns: ISZ[RewritingSystem.Rewriter.Pattern]): Unit
+    def setPatterns(th: TypeHierarchy, isInObject: B, name: ISZ[String], patterns: ISZ[RewritingSystem.Rewriter.Pattern]): Unit
 
     def keys: ISZ[Cache.Key]
 

diff --git a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
diff --git a/shared/src/main/scala/org/sireum/logika/StepProofContext.scala b/shared/src/main/scala/org/sireum/logika/StepProofContext.scala
@@ -45,7 +45,7 @@ object StepProofContext {
                           val claims: ISZ[State.Claim]) extends StepProofContext {
     @strictpure override def prettyST: ST = st"(${stepNo.prettyST}, ${exp.prettyST}, ${(for (claim <- claims) yield claim.toRawST, ", ")})"
     @memoize def coreExpClaim: AST.CoreExp.Base = {
-      return RewritingSystem.translate(th, F, exp)
+      return RewritingSystem.translateExp(th, F, exp)
     }
   }
 

diff --git a/shared/src/main/scala/org/sireum/logika/Util.scala b/shared/src/main/scala/org/sireum/logika/Util.scala
@@ -3005,7 +3005,7 @@ object Util {
   }
 
   def extractAssignExpOpt(mi: lang.symbol.Info.Method): Option[AST.AssignExp] = {
-    if (mi.ast.purity == AST.Purity.StrictPure && mi.ast.bodyOpt.nonEmpty) {
+    if (mi.ast.isStrictPure && mi.ast.bodyOpt.nonEmpty) {
       mi.ast.bodyOpt.get.stmts match {
         case ISZ(stmt: AST.Stmt.Var, _: AST.Stmt.Return) => return stmt.initOpt
         case stmts => halt(s"Infeasible: $stmts")

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/FoldUnfoldPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/FoldUnfoldPlugin.scala
@@ -151,7 +151,7 @@ import FoldUnfoldPlugin._
           val typeRel = TypeChecker.TypeRelation.Supertype
           if (res.isInObject) {
             val mi = logika.th.nameMap.get(res.owner :+ res.id).get.asInstanceOf[Info.Method]
-            if (mi.ast.purity != AST.Purity.StrictPure) {
+            if (!mi.ast.isStrictPure) {
               return errSp()
             }
             val msm = TypeChecker.unifyFun(Logika.kind, logika.th, unfoldFrom.posOpt, typeRel, res.tpeOpt.get,
@@ -165,7 +165,7 @@ import FoldUnfoldPlugin._
             logika.th.typeMap.get(res.owner).get match {
               case info: TypeInfo.Sig =>
                 val mi = info.methods.get(res.id).get
-                if (mi.ast.purity != AST.Purity.StrictPure) {
+                if (!mi.ast.isStrictPure) {
                   return errSp()
                 }
                 val tsm = TypeChecker.buildTypeSubstMap(res.owner, posOpt, info.ast.typeParams,

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala
@@ -95,7 +95,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
       else None()
     val rwPc = Rewriter(if (logika.config.rwPar) logika.config.parCores else 1,
       logika.th, provenClaims, patterns, logika.config.rwTrace, logika.config.rwEvalTrace, F, ISZ())
-    val stepClaim = RewritingSystem.translate(logika.th, F, step.claim)
+    val stepClaim = RewritingSystem.translateExp(logika.th, F, step.claim)
 
     if (logika.config.rwEvalTrace) {
       rwPc.trace = rwPc.trace :+ RewritingSystem.Trace.Begin("simplifying", stepClaim)
@@ -149,7 +149,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
         reporter.error(from.posOpt, Logika.kind, s"Expecting a regular proof step")
         return emptyResult
     }
-    val fromCoreClaim = RewritingSystem.translate(logika.th, F, fromClaim)
+    val fromCoreClaim = RewritingSystem.translateExp(logika.th, F, fromClaim)
     @strictpure def simplTraceOpt: Option[ST] = if (stepClaim == stepClaimEv) None() else Some(
       st"""and/or after simplifying the step claim to:
           |  ${stepClaimEv.prettyST}"""