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
fromMarkedIdentifier :: Marked Identifier -> Symbol
fromMarkedIdentifier = \case
Original i -> SymName i
Marked i -> SymSharp $ SymName i
sortVariables :: Rule (Term Identifier s) -> Rule (Term Identifier s)
sortVariables r = r { lhs = vmap mapVar $ lhs r
, rhs = vmap mapVar $ rhs r
}
where
oldVars = nub $ voccs $ lhs r
newVars = zipWith mkNewVar [1..] oldVars
mkNewVar i v = v { name = "x" ++ show i }
mapping = M.fromList $ zip oldVars newVars
mapVar v = case M.lookup v mapping of
Just v' -> v'
Nothing -> error "TPDB.CPF.Proof.Util.sortVariables"