{-# 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"