{-# LANGUAGE LambdaCase #-} module TPDB.CPF.Proof.Util where import qualified Data.Map as M import Data.List (nub) import TPDB.Data import TPDB.CPF.Proof.Type hiding (name) import TPDB.DP import Data.String (fromString) fromMarkedIdentifier :: Marked Identifier -> Symbol fromMarkedIdentifier :: Marked Identifier -> Symbol fromMarkedIdentifier = \case Original Identifier i -> Identifier -> Symbol SymName Identifier i Marked Identifier i -> Symbol -> Symbol SymSharp (Symbol -> Symbol) -> Symbol -> Symbol forall a b. (a -> b) -> a -> b $ Identifier -> Symbol SymName Identifier i sortVariables :: Rule (Term Identifier s) -> Rule (Term Identifier s) sortVariables :: Rule (Term Identifier s) -> Rule (Term Identifier s) sortVariables Rule (Term Identifier s) r = Rule (Term Identifier s) r { lhs :: Term Identifier s lhs = (Identifier -> Identifier) -> Term Identifier s -> Term Identifier s forall v u s. (v -> u) -> Term v s -> Term u s vmap Identifier -> Identifier mapVar (Term Identifier s -> Term Identifier s) -> Term Identifier s -> Term Identifier s forall a b. (a -> b) -> a -> b $ Rule (Term Identifier s) -> Term Identifier s forall a. Rule a -> a lhs Rule (Term Identifier s) r , rhs :: Term Identifier s rhs = (Identifier -> Identifier) -> Term Identifier s -> Term Identifier s forall v u s. (v -> u) -> Term v s -> Term u s vmap Identifier -> Identifier mapVar (Term Identifier s -> Term Identifier s) -> Term Identifier s -> Term Identifier s forall a b. (a -> b) -> a -> b $ Rule (Term Identifier s) -> Term Identifier s forall a. Rule a -> a rhs Rule (Term Identifier s) r } where oldVars :: [Identifier] oldVars = [Identifier] -> [Identifier] forall a. Eq a => [a] -> [a] nub ([Identifier] -> [Identifier]) -> [Identifier] -> [Identifier] forall a b. (a -> b) -> a -> b $ Term Identifier s -> [Identifier] forall v c. Term v c -> [v] voccs (Term Identifier s -> [Identifier]) -> Term Identifier s -> [Identifier] forall a b. (a -> b) -> a -> b $ Rule (Term Identifier s) -> Term Identifier s forall a. Rule a -> a lhs Rule (Term Identifier s) r newVars :: [Identifier] newVars = (Integer -> Identifier -> Identifier) -> [Integer] -> [Identifier] -> [Identifier] forall a b c. (a -> b -> c) -> [a] -> [b] -> [c] zipWith Integer -> Identifier -> Identifier forall a. Show a => a -> Identifier -> Identifier mkNewVar [Integer 1..] [Identifier] oldVars mkNewVar :: a -> Identifier -> Identifier mkNewVar a i Identifier v = Identifier v { name :: Text name = String -> Text forall a. IsString a => String -> a fromString (String -> Text) -> String -> Text forall a b. (a -> b) -> a -> b $ String "x" String -> String -> String forall a. [a] -> [a] -> [a] ++ a -> String forall a. Show a => a -> String show a i } mapping :: Map Identifier Identifier mapping = [(Identifier, Identifier)] -> Map Identifier Identifier forall k a. Ord k => [(k, a)] -> Map k a M.fromList ([(Identifier, Identifier)] -> Map Identifier Identifier) -> [(Identifier, Identifier)] -> Map Identifier Identifier forall a b. (a -> b) -> a -> b $ [Identifier] -> [Identifier] -> [(Identifier, Identifier)] forall a b. [a] -> [b] -> [(a, b)] zip [Identifier] oldVars [Identifier] newVars mapVar :: Identifier -> Identifier mapVar Identifier v = case Identifier -> Map Identifier Identifier -> Maybe Identifier forall k a. Ord k => k -> Map k a -> Maybe a M.lookup Identifier v Map Identifier Identifier mapping of Just Identifier v' -> Identifier v' Maybe Identifier Nothing -> String -> Identifier forall a. HasCallStack => String -> a error String "TPDB.CPF.Proof.Util.sortVariables"