Add substitution conversion helpers

runtimeverification · Oct 16, 2024 · 77c8c57 · 77c8c57
1 parent c232909
commit 77c8c57
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 15 deletions.
diff --git a/booster/library/Booster/Pattern/Bool.hs b/booster/library/Booster/Pattern/Bool.hs
@@ -10,7 +10,9 @@ module Booster.Pattern.Bool (
     negateBool,
     splitBoolPredicates,
     splitAndBools,
+    mkEq,
     destructEq,
+    asEquations,
     -- patterns
     pattern TrueBool,
     pattern FalseBool,
@@ -25,6 +27,8 @@ module Booster.Pattern.Bool (
 ) where
 
 import Data.ByteString.Char8 (ByteString)
+import Data.Map.Strict (Map)
+import Data.Map.Strict qualified as Map
 
 import Booster.Definition.Attributes.Base (
     FunctionType (..),
@@ -52,7 +56,7 @@ import Booster.Pattern.Base (
     pattern SymbolApplication,
     pattern Var,
  )
-import Booster.Pattern.Util (isConcrete)
+import Booster.Pattern.Util (isConcrete, sortOfTerm)
 import Booster.SMT.Base (SExpr (Atom), SMTId (..))
 
 pattern HookedTotalFunction :: ByteString -> SymbolAttributes
@@ -210,6 +214,12 @@ splitAndBools p@(Predicate t)
     | AndBool l r <- t = concatMap (splitAndBools . Predicate) [l, r]
     | otherwise = [p]
 
+mkEq :: Variable -> Term -> Predicate
+mkEq x t = Predicate $ case sortOfTerm t of
+    SortInt -> EqualsInt (Var x) t
+    SortBool -> EqualsBool (Var x) t
+    otherSort -> EqualsK (KSeq otherSort (Var x)) (KSeq otherSort t)
+
 -- | Pattern match on an equality predicate and try extracting a variable assignment
 destructEq :: Predicate -> Maybe (Variable, Term)
 destructEq = \case
@@ -218,3 +228,7 @@ destructEq = \case
     Predicate
         (EqualsK (KSeq _lhsSort (Var x)) (KSeq _rhsSort t)) -> Just (x, t)
     _ -> Nothing
+
+-- | turns a substitution into a list of equations
+asEquations :: Map Variable Term -> [Predicate]
+asEquations = map (uncurry mkEq) . Map.assocs
diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs
@@ -463,7 +463,7 @@ mkSubstitution initialSubst =
             Map.partition ((== 1) . length) $
                 Map.fromListWith (<>) [(v, [t]) | SubstitutionPred v t <- initialSubst]
         equations =
-            [mkEq v t | (v, ts) <- Map.assocs duplicates, t <- ts]
+            [Internal.mkEq v t | (v, ts) <- Map.assocs duplicates, t <- ts]
      in execState breakCycles (Map.map head substMap, equations)
   where
     breakCycles :: State (Map Internal.Variable Internal.Term, [Internal.Predicate]) ()
@@ -477,20 +477,10 @@ mkSubstitution initialSubst =
             else do
                 modify $ \(m, eqs) ->
                     ( m `Map.withoutKeys` cycleNodes
-                    , eqs <> (map (uncurry mkEq) $ Map.assocs $ m `Map.restrictKeys` cycleNodes)
+                    , eqs <> (map (uncurry Internal.mkEq) $ Map.assocs $ m `Map.restrictKeys` cycleNodes)
                     )
                 breakCycles
 
-mkEq :: Internal.Variable -> Internal.Term -> Internal.Predicate
-mkEq x t = Internal.Predicate $ case sortOfTerm t of
-    Internal.SortInt -> Internal.EqualsInt (Internal.Var x) t
-    Internal.SortBool -> Internal.EqualsBool (Internal.Var x) t
-    otherSort -> Internal.EqualsK (Internal.KSeq otherSort (Internal.Var x)) (Internal.KSeq otherSort t)
-
--- | turns a substitution into a list of equations
-asEquations :: Map Internal.Variable Internal.Term -> [Internal.Predicate]
-asEquations = map (uncurry mkEq) . Map.assocs
-
 internalisePred ::
     Flag "alias" ->
     Flag "subsorts" ->
@@ -562,12 +552,12 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort
                         pure [BoolPred $ Internal.Predicate $ Internal.NotBool x]
                     (_, Internal.Var x, t)
                         | x `Set.member` freeVariables t ->
-                            pure [BoolPred $ mkEq x t]
+                            pure [BoolPred $ Internal.mkEq x t]
                         | otherwise ->
                             pure [SubstitutionPred x t]
                     (_, t, Internal.Var x)
                         | x `Set.member` freeVariables t ->
-                            pure [BoolPred $ mkEq x t]
+                            pure [BoolPred $ Internal.mkEq x t]
                         | otherwise ->
                             pure [SubstitutionPred x t]
                     (Internal.SortInt, _, _) ->