{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE FlexibleContexts #-}

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)
import Data.Hashable

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 :: (Ord s, Hashable s) => Rule (Term Identifier s) -> Rule (Term Identifier s)
sortVariables :: forall s.
(Ord s, Hashable s) =>
Rule (Term Identifier s) -> Rule (Term Identifier s)
sortVariables Rule (Term Identifier s)
r = Rule (Term Identifier s)
r { lhs = vmap mapVar $ lhs r
                    , rhs = vmap mapVar $ rhs 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. (() :: Constraint) => 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 = fromString $ "x" ++ show 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"