Consolidate variable marking API (#461)

Closes #456 --------- Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Jan 16, 2024 · 2d2dd7f · 2d2dd7f
1 parent 98e9b26
commit 2d2dd7f
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 21 deletions.
diff --git a/library/Booster/Pattern/Rewrite.hs b/library/Booster/Pattern/Rewrite.hs
@@ -328,7 +328,7 @@ applyRule pat@Pattern{ceilConditions} rule = runRewriteRuleAppT $ do
         forbiddenVars = varsFromInput <> varsFromSubst
         existentialSubst =
             Map.fromSet
-                (\v -> Var $ freshenVar v{variableName = stripVarOriginPrefix v.variableName} forbiddenVars)
+                (\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars)
                 rule.existentials
 
     -- modify the substitution to include the existentials

diff --git a/library/Booster/Pattern/Util.hs b/library/Booster/Pattern/Util.hs
@@ -29,7 +29,9 @@ module Booster.Pattern.Util (
     abstractSymbolicConstructorArguments,
     cellSymbolStats,
     cellVariableStats,
-    stripVarOriginPrefix,
+    stripMarker,
+    markAsExVar,
+    markAsRuleVar,
     incrementNameCounter,
 ) where
 
@@ -117,11 +119,17 @@ modifyVariablesInT f = cata $ \case
 modifyVarName :: (VarName -> VarName) -> Variable -> Variable
 modifyVarName f v = v{variableName = f v.variableName}
 
-{- | Strip variable provenance prefixes introduced
-in "Syntax.ParsedKore.Internalize.internationalization"
+markAsRuleVar :: VarName -> VarName
+markAsRuleVar = ("Rule#" <>)
+
+markAsExVar :: VarName -> VarName
+markAsExVar = ("Ex#" <>)
+
+{- | Strip variable provenance prefixes introduced using "markAsRuleVar" and "markAsExVar"
+in "Syntax.ParsedKore.Internalize"
 -}
-stripVarOriginPrefix :: VarName -> VarName
-stripVarOriginPrefix name =
+stripMarker :: VarName -> VarName
+stripMarker name =
     let noRule = BS.stripPrefix "Rule#" name
         noEx = BS.stripPrefix "Ex#" name
      in fromMaybe name $ noRule <|> noEx

diff --git a/library/Booster/Syntax/ParsedKore/Internalise.hs b/library/Booster/Syntax/ParsedKore/Internalise.hs
@@ -786,14 +786,15 @@ internaliseRewriteRuleNoAlias ::
     Except DefinitionError (RewriteRule k)
 internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do
     let ref = sourceRef axAttributes
-    -- prefix all variables in lhs and rhs with "Rule#" and "Ex#" to avoid
-    -- name clashes with patterns from the user
+    -- mark all variables in lhs as rule-variables
+    -- and in rhs as either rule- or existential-variables
+    -- to avoid name clashes with patterns from the user;
     -- filter out literal `Top` constraints
-    lhs <- internalisePattern' ref (Util.modifyVarName ("Rule#" <>)) left
+    lhs <- internalisePattern' ref (Util.modifyVarName Util.markAsRuleVar) left
     existentials' <- fmap Set.fromList $ withExcept (DefinitionPatternError ref) $ mapM mkVar exs
     let renameVariable v
-            | v `Set.member` existentials' = Util.modifyVarName ("Ex#" <>) v
-            | otherwise = Util.modifyVarName ("Rule#" <>) v
+            | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v
+            | otherwise = Util.modifyVarName Util.markAsRuleVar v
     rhs <- internalisePattern' ref renameVariable right
     let notPreservesDefinednessReasons =
             -- users can override the definedness computation by an explicit attribute
@@ -803,15 +804,11 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do
                     [ UndefinedSymbol s.name
                     | s <- Util.filterTermSymbols (not . Util.isDefinedSymbol) rhs.term
                     ]
-        -- <> [ UndefinedSymbol s.name
-        --    | c <- Set.toList lhs.constraints
-        --    , s <- Util.filterTermSymbols (not . Util.isDefinedSymbol) $ coerce c
-        --    ]
         containsAcSymbols =
             Util.checkTermSymbols Util.checkSymbolIsAc lhs.term
         computedAttributes =
             ComputedAxiomAttributes{notPreservesDefinednessReasons, containsAcSymbols}
-        existentials = Set.map (Util.modifyVarName ("Ex#" <>)) existentials'
+        existentials = Set.map (Util.modifyVarName Util.markAsExVar) existentials'
     return
         RewriteRule
             { lhs = lhs.term
@@ -866,13 +863,13 @@ internaliseRewriteRule partialDefinition exs aliasName aliasArgs right axAttribu
     -- name clashes with patterns from the user
     -- filter out literal `Top` constraints
     lhs <-
-        fmap (removeTrueBools . Util.modifyVariables (Util.modifyVarName ("Rule#" <>))) $
+        fmap (removeTrueBools . Util.modifyVariables (Util.modifyVarName Util.markAsRuleVar)) $
             retractPattern result
                 `orFailWith` DefinitionTermOrPredicateError ref (PatternExpected result)
     existentials' <- fmap Set.fromList $ withExcept (DefinitionPatternError ref) $ mapM mkVar exs
     let renameVariable v
-            | v `Set.member` existentials' = Util.modifyVarName ("Ex#" <>) v
-            | otherwise = Util.modifyVarName ("Rule#" <>) v
+            | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v
+            | otherwise = Util.modifyVarName Util.markAsRuleVar v
     rhs <- internalisePattern' ref renameVariable right
 
     let notPreservesDefinednessReasons =
@@ -887,9 +884,11 @@ internaliseRewriteRule partialDefinition exs aliasName aliasArgs right axAttribu
             Util.checkTermSymbols Util.checkSymbolIsAc lhs.term
         computedAttributes =
             ComputedAxiomAttributes{notPreservesDefinednessReasons, containsAcSymbols}
-        existentials = Set.map (Util.modifyVarName ("Ex#" <>)) existentials'
+        existentials = Set.map (Util.modifyVarName Util.markAsExVar) existentials'
         attributes =
-            axAttributes{concreteness = Util.modifyVarNameConcreteness ("Rule#" <>) axAttributes.concreteness}
+            axAttributes
+                { concreteness = Util.modifyVarNameConcreteness Util.markAsRuleVar axAttributes.concreteness
+                }
     return
         RewriteRule
             { lhs = lhs.term