{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{- |
Module : ./THF/Utils.hs
Description : A couple helper functions
Copyright : (c) J. von Schroeder, DFKI Bremen 2012
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Stability : provisional
Portability : non-portable
-}
module THF.Utils (
Unique (..),
UniqueT,
fresh,
evalUniqueT,
evalUnique,
numbered,
numberedTok,
mkNames,
addSuffix,
recreateSymbols,
thfTopLevelTypeToType,
typeToTopLevelType,
typeToUnitaryType,
typeToBinaryType,
toToken,
toId,
RewriteFuns (..),
rewriteSenFun,
rewriteTHF0,
AnaFuns (..),
anaSenFun,
anaTHF0
) where
import THF.As
import THF.Sign
import THF.Cons
import THF.Print ()
import Common.Id (Token (..), Id, mkId, nullRange)
import Common.AS_Annotation (Named, SenAttr (..))
import Common.Result
import Control.Applicative
import Control.Monad.State
import Control.Monad.Identity
import qualified Data.Map as Map
import Data.Maybe (fromJust, isJust)
newtype UniqueT m a = UniqueT (StateT Integer m a)
deriving (Functor, Applicative, Monad, MonadTrans, MonadIO)
newtype Unique a = Unique (UniqueT Identity a)
deriving (Functor, Applicative, Monad, MonadUnique)
class Monad m => MonadUnique m where
fresh :: m Integer
instance (Monad m) => MonadUnique (UniqueT m) where
fresh = UniqueT $ do
n <- get
put (succ n)
return n
evalUniqueT :: Monad m => UniqueT m a -> m a
evalUniqueT (UniqueT s) = evalStateT s 1
evalUnique :: Unique a -> a
evalUnique (Unique s) = runIdentity (evalUniqueT s)
addSuffix :: String -> AtomicWord -> AtomicWord
addSuffix s a = case a of
A_Lower_Word t -> A_Lower_Word $ rename t
A_Single_Quoted t -> A_Single_Quoted $ rename t
where rename t = t { tokStr = tokStr t ++ s }
addSuffixN :: String -> Name -> Name
addSuffixN s n = case n of
N_Atomic_Word a -> N_Atomic_Word $ addSuffix s a
N_Integer t -> rename s t
T0N_Unsigned_Integer t -> rename s t
where rename sf t = N_Atomic_Word $ addSuffix sf
(A_Lower_Word $ t { tokStr = 'i' : show t })
numbered :: Monad m => AtomicWord -> UniqueT m AtomicWord
numbered a = do
f <- fresh
return (addSuffix ('_' : show f) a)
numberedTok :: Monad m => Token -> UniqueT m Token
numberedTok = liftM toToken . numbered . A_Single_Quoted
mkNames :: Constant -> Name -> Int -> [(Constant, Name)]
mkNames c n i = evalUnique $ replicateM i $ do
f <- fresh
let s = '_' : show f
return (addSuffix s c, addSuffixN s n)
recreateSymbols :: SignTHF -> SignTHF
recreateSymbols (Sign tps cs _) =
let name = N_Atomic_Word
symbs1 = foldl (\ m (c, t) -> Map.insert c
(Symbol c (name c) (ST_Type $ typeKind t)) m)
Map.empty $ Map.toList tps
symbs = foldl (\ m (c, k) -> Map.insert c
(Symbol c (name c) (ST_Const $ constType k)) m)
symbs1 $ Map.toList cs
in Sign tps cs symbs
toToken :: Constant -> Token
toToken (A_Lower_Word t) = t
toToken (A_Single_Quoted t) = t
toId :: Constant -> Id
toId c = mkId [toToken c]
thfTopLevelTypeToType :: THFTopLevelType -> Maybe Type
thfTopLevelTypeToType tlt = case tlt of
T0TLT_Defined_Type dt -> thfDefinedTypeToType dt
T0TLT_THF_Binary_Type bt -> thfBinaryTypeToType bt
T0TLT_Constant c -> Just $ CType c
T0TLT_System_Type st -> Just $ SType st
T0TLT_Variable v -> Just $ VType v
_ -> Nothing
thfDefinedTypeToType :: DefinedType -> Maybe Type
thfDefinedTypeToType dt = case dt of
DT_oType -> Just OType
DT_o -> Just OType
DT_iType -> Just IType
DT_i -> Just IType
DT_tType -> Just TType
_ -> Nothing
thfBinaryTypeToType :: THFBinaryType -> Maybe Type
thfBinaryTypeToType bt = case bt of
TBT_THF_Mapping_Type [] -> Nothing
TBT_THF_Mapping_Type (_ : []) -> Nothing
TBT_THF_Mapping_Type mt -> thfMappingTypeToType mt
T0BT_THF_Binary_Type_Par btp -> fmap ParType (thfBinaryTypeToType btp)
TBT_THF_Xprod_Type [] -> Nothing
TBT_THF_Xprod_Type (u : []) -> thfUnitaryTypeToType u
TBT_THF_Xprod_Type us -> let us' = map thfUnitaryTypeToType us
in if all isJust us' then
(Just . ProdType) $ map fromJust us'
else Nothing
_ -> Nothing
thfMappingTypeToType :: [THFUnitaryType] -> Maybe Type
thfMappingTypeToType [] = Nothing
thfMappingTypeToType (u : []) = thfUnitaryTypeToType u
thfMappingTypeToType (u : ru) =
let k1 = thfUnitaryTypeToType u
k2 = thfMappingTypeToType ru
in if isJust k1 && isJust k2
then Just $ MapType (fromJust k1) (fromJust k2)
else Nothing
thfUnitaryTypeToType :: THFUnitaryType -> Maybe Type
thfUnitaryTypeToType ut = case ut of
T0UT_THF_Binary_Type_Par bt -> fmap ParType (thfBinaryTypeToType bt)
T0UT_Defined_Type dt -> thfDefinedTypeToType dt
T0UT_Constant c -> Just $ CType c
T0UT_System_Type st -> Just $ SType st
T0UT_Variable v -> Just $ VType v
_ -> Nothing
typeToTopLevelType :: Type -> Result THFTopLevelType
typeToTopLevelType t = case t of
TType -> return $ T0TLT_Defined_Type DT_tType
OType -> return $ T0TLT_Defined_Type DT_oType
IType -> return $ T0TLT_Defined_Type DT_iType
MapType t1 t2 -> liftM (T0TLT_THF_Binary_Type . TBT_THF_Mapping_Type)
(mapM typeToUnitaryType [t1, t2])
ProdType ts -> liftM (T0TLT_THF_Binary_Type . TBT_THF_Xprod_Type)
(mapM typeToUnitaryType ts)
CType c -> return $ T0TLT_Constant c
SType t' -> return $ T0TLT_System_Type t'
VType t' -> return $ T0TLT_Variable t'
ParType t' -> liftM (T0TLT_THF_Binary_Type . T0BT_THF_Binary_Type_Par)
(typeToBinaryType t')
typeToUnitaryType :: Type -> Result THFUnitaryType
typeToUnitaryType t = do
tl <- typeToTopLevelType t
case tl of
T0TLT_Constant c -> return $ T0UT_Constant c
T0TLT_Variable t' -> return $ T0UT_Variable t'
T0TLT_Defined_Type d -> return $ T0UT_Defined_Type d
T0TLT_System_Type t' -> return $ T0UT_System_Type t'
T0TLT_THF_Binary_Type b -> return $ T0UT_THF_Binary_Type_Par b
TTLT_THF_Logic_Formula _ -> mkError "Not yet implemented!" nullRange
typeToBinaryType :: Type -> Result THFBinaryType
typeToBinaryType t = do
tl <- typeToTopLevelType t
case tl of
T0TLT_THF_Binary_Type b -> return b
_ -> mkError ("Cannot represent type " ++ show t ++
"as THFBinaryType!") nullRange
data RewriteFuns a = RewriteFuns {
rewriteLogicFormula :: (RewriteFuns a, a) -> THFLogicFormula
-> Result THFLogicFormula,
rewriteBinaryFormula :: (RewriteFuns a, a) -> THFBinaryFormula
-> Result THFBinaryFormula,
rewriteUnitaryFormula :: (RewriteFuns a, a) -> THFUnitaryFormula
-> Result THFUnitaryFormula,
rewriteBinaryPair :: (RewriteFuns a, a) -> (THFUnitaryFormula,
THFPairConnective, THFUnitaryFormula)
-> Result THFBinaryFormula,
rewriteBinaryTuple :: (RewriteFuns a, a) -> THFBinaryTuple
-> Result THFBinaryTuple,
rewriteQuantifiedFormula :: (RewriteFuns a, a) -> THFQuantifiedFormula
-> Result THFQuantifiedFormula,
rewriteAtom :: (RewriteFuns a, a) -> THFAtom -> Result THFUnitaryFormula,
rewriteVariableList :: (RewriteFuns a, a) -> [THFVariable]
-> Result [THFVariable],
rewriteConst :: (RewriteFuns a, a) -> Constant -> Result THFUnitaryFormula,
rewriteConnTerm :: (RewriteFuns a, a) -> THFConnTerm -> Result THFConnTerm }
rewriteTHF0 :: RewriteFuns a
rewriteTHF0 = RewriteFuns {
rewriteLogicFormula = rewriteLogicFormula',
rewriteBinaryFormula = rewriteBinaryFormula',
rewriteUnitaryFormula = rewriteUnitaryFormula',
rewriteBinaryPair = rewriteBinaryPair',
rewriteBinaryTuple = rewriteBinaryTuple',
rewriteQuantifiedFormula = rewriteQuantifiedFormula',
rewriteAtom = rewriteAtom',
rewriteVariableList = rewriteVariableList',
rewriteConst = rewriteConst',
rewriteConnTerm = rewriteConnTerm' }
rewriteSenFun :: (RewriteFuns a, a) -> Named THFFormula
-> Result (Named THFFormula)
rewriteSenFun (fns, d) sen = do
sen' <- case sentence sen of
TF_THF_Logic_Formula lf ->
liftM TF_THF_Logic_Formula (rewriteLogicFormula fns (fns, d) lf)
T0F_THF_Typed_Const tc ->
mkError "THF.Utils.rewriteSen: Typed constants are not in THF0! "
tc
TF_THF_Sequent s ->
mkError "THF.Utils.rewriteSen: Sequents are not in THF0!" s
return $ sen { sentence = sen' }
rewriteLogicFormula' :: (RewriteFuns a, a) -> THFLogicFormula
-> Result THFLogicFormula
rewriteLogicFormula' (fns, d) lf = case lf of
TLF_THF_Binary_Formula bf -> liftM TLF_THF_Binary_Formula $
rewriteBinaryFormula fns (fns, d) bf
TLF_THF_Unitary_Formula uf -> liftM TLF_THF_Unitary_Formula $
rewriteUnitaryFormula fns (fns, d) uf
TLF_THF_Type_Formula _ ->
mkError "THF.Utils.rewriteLogicFormula: Type Formula not in THF0!" lf
TLF_THF_Sub_Type _ ->
mkError "THF.Utils.rewriteLogicFormula: Sub Type Formula not in THF0!" lf
rewriteBinaryFormula' :: (RewriteFuns a, a) -> THFBinaryFormula
-> Result THFBinaryFormula
rewriteBinaryFormula' (fns, d) bf = case bf of
TBF_THF_Binary_Type _ -> mkError
"THF.Utils.rewriteBinaryFormula: Binary Type not in THF0!" bf
TBF_THF_Binary_Pair uf1 cn uf2 ->
rewriteBinaryPair fns (fns, d) (uf1, cn, uf2)
TBF_THF_Binary_Tuple bt -> liftM TBF_THF_Binary_Tuple $
rewriteBinaryTuple fns (fns, d) bt
rewriteBinaryPair' :: (RewriteFuns a, a) -> (THFUnitaryFormula,
THFPairConnective, THFUnitaryFormula)
-> Result THFBinaryFormula
rewriteBinaryPair' (fns, d) (uf1, cn, uf2) = do
uf1' <- rewriteUnitaryFormula fns (fns, d) uf1
uf2' <- rewriteUnitaryFormula fns (fns, d) uf2
return $ TBF_THF_Binary_Pair uf1' cn uf2'
rewriteBinaryTuple' :: (RewriteFuns a, a) -> THFBinaryTuple
-> Result THFBinaryTuple
rewriteBinaryTuple' (fns, d) bt = case bt of
TBT_THF_Or_Formula ufs -> liftM TBT_THF_Or_Formula $
mapR (rewriteUnitaryFormula fns (fns, d)) ufs
TBT_THF_And_Formula ufs -> liftM TBT_THF_And_Formula $
mapR (rewriteUnitaryFormula fns (fns, d)) ufs
TBT_THF_Apply_Formula ufs -> liftM TBT_THF_Apply_Formula $
mapR (rewriteUnitaryFormula fns (fns, d)) ufs
rewriteUnitaryFormula' :: (RewriteFuns a, a) -> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula' (fns, d) uf = case uf of
TUF_THF_Conditional {} ->
mkError ("THF.Utils.rewriteUnitaryFOrmula: " ++
"Conditional not in THF0!") uf
TUF_THF_Quantified_Formula qf -> liftM TUF_THF_Quantified_Formula $
rewriteQuantifiedFormula fns (fns, d) qf
TUF_THF_Unary_Formula c lf -> liftM (TUF_THF_Unary_Formula c) $
rewriteLogicFormula fns (fns, d) lf
TUF_THF_Atom a -> rewriteAtom fns (fns, d) a
TUF_THF_Tuple t -> liftM TUF_THF_Tuple $
mapR (rewriteLogicFormula fns (fns, d)) t
TUF_THF_Logic_Formula_Par lf -> liftM TUF_THF_Logic_Formula_Par $
rewriteLogicFormula fns (fns, d) lf
T0UF_THF_Abstraction vs uf' -> do
vs' <- rewriteVariableList fns (fns, d) vs
uf'' <- rewriteUnitaryFormula fns (fns, d) uf'
return $ T0UF_THF_Abstraction vs' uf''
rewriteQuantifiedFormula' :: (RewriteFuns a, a) -> THFQuantifiedFormula
-> Result THFQuantifiedFormula
rewriteQuantifiedFormula' (fns, d) qf = case qf of
TQF_THF_Quantified_Formula q vs uf -> do
vs' <- rewriteVariableList fns (fns, d) vs
uf' <- rewriteUnitaryFormula fns (fns, d) uf
return $ TQF_THF_Quantified_Formula q vs' uf'
T0QF_THF_Quantified_Var q vs uf -> do
vs' <- rewriteVariableList fns (fns, d) vs
uf' <- rewriteUnitaryFormula fns (fns, d) uf
return $ T0QF_THF_Quantified_Var q vs' uf'
T0QF_THF_Quantified_Novar _ _ ->
mkError "THF.Utils.rewriteQuantifiedFormula: Quantified Novar not in THF0!" qf
rewriteVariableList' :: (RewriteFuns a, a) -> [THFVariable]
-> Result [THFVariable]
rewriteVariableList' _ = return
rewriteAtom' :: (RewriteFuns a, a) -> THFAtom -> Result THFUnitaryFormula
rewriteAtom' (fns, d) a = case a of
TA_Term _ -> mkError "THF.Utils.rewriteAtom: Term not in THF0!" a
TA_THF_Conn_Term c -> liftM (TUF_THF_Atom . TA_THF_Conn_Term) $
rewriteConnTerm fns (fns, d) c
TA_Defined_Type _ ->
mkError "THF.Utils.rewriteAtom: Defined Type not in THF0!" a
TA_Defined_Plain_Formula _ ->
mkError "THF.Utils.rewriteAtom: Defined Plain Formula not in THF0!" a
TA_System_Type _ ->
mkError "THF.Utils.rewriteAtom: System Type not in THF0!" a
TA_System_Atomic_Formula _ ->
mkError "THF.Utils.rewriteAtom: System Atomic Formula not in THF0!" a
T0A_Constant c -> rewriteConst fns (fns, d) c
T0A_Defined_Constant _ -> return $ TUF_THF_Atom a
T0A_System_Constant _ -> return $ TUF_THF_Atom a
T0A_Variable v -> do
v' <- rewriteVariableList fns (fns, d) [TV_Variable v]
case v' of
TV_Variable t : _ -> return $ TUF_THF_Atom $ T0A_Variable t
_ -> mkError "THF.Utils.rewriteAtom: Invalid rewrite!" v
rewriteConst' :: (RewriteFuns a, a) -> Constant -> Result THFUnitaryFormula
rewriteConst' _ = return . TUF_THF_Atom . T0A_Constant
rewriteConnTerm' :: (RewriteFuns a, a) -> THFConnTerm -> Result THFConnTerm
rewriteConnTerm' _ c = return c
data AnaFuns a b = AnaFuns {
anaLogicFormula :: (AnaFuns a b, a) -> THFLogicFormula -> Result [b],
anaBinaryFormula :: (AnaFuns a b, a) -> THFBinaryFormula -> Result [b],
anaUnitaryFormula :: (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b],
anaBinaryPair :: (AnaFuns a b, a) -> (THFUnitaryFormula,
THFPairConnective, THFUnitaryFormula) -> Result [b],
anaBinaryTuple :: (AnaFuns a b, a) -> THFBinaryTuple -> Result [b],
anaQuantifiedFormula :: (AnaFuns a b, a) -> THFQuantifiedFormula -> Result [b],
anaAtom :: (AnaFuns a b, a) -> THFAtom -> Result [b],
anaVariableList :: (AnaFuns a b, a) -> [THFVariable] -> Result [b],
anaConst :: (AnaFuns a b, a) -> Constant -> Result [b],
anaConnTerm :: (AnaFuns a b, a) -> THFConnTerm -> Result [b] }
anaTHF0 :: AnaFuns a b
anaTHF0 = AnaFuns {
anaLogicFormula = anaLogicFormula',
anaBinaryFormula = anaBinaryFormula',
anaUnitaryFormula = anaUnitaryFormula',
anaBinaryPair = anaBinaryPair',
anaBinaryTuple = anaBinaryTuple',
anaQuantifiedFormula = anaQuantifiedFormula',
anaAtom = anaAtom',
anaVariableList = anaVariableList',
anaConst = anaConst',
anaConnTerm = anaConnTerm' }
anaSenFun :: (AnaFuns a b, a) -> Named THFFormula -> Result [b]
anaSenFun (fns, d) sen = case sentence sen of
TF_THF_Logic_Formula lf -> anaLogicFormula fns (fns, d) lf
T0F_THF_Typed_Const tc ->
mkError "THF.Utils.anaSen: Typed constants are not in THF0! " tc
TF_THF_Sequent s ->
mkError "THF.Utils.anaSen: Sequents are not in THF0!" s
anaLogicFormula' :: (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
anaLogicFormula' (fns, d) lf = case lf of
TLF_THF_Binary_Formula bf -> anaBinaryFormula fns (fns, d) bf
TLF_THF_Unitary_Formula uf -> anaUnitaryFormula fns (fns, d) uf
TLF_THF_Type_Formula _ ->
mkError "THF.Utils.anaLogicFormula: Type Formula not in THF0!" lf
TLF_THF_Sub_Type _ ->
mkError "THF.Utils.anaLogicFormula: Sub Type Formula not in THF0!" lf
anaBinaryFormula' :: (AnaFuns a b, a) -> THFBinaryFormula -> Result [b]
anaBinaryFormula' (fns, d) bf = case bf of
TBF_THF_Binary_Type _ -> mkError
"THF.Utils.anaBinaryFormula: Binary Type not in THF0!" bf
TBF_THF_Binary_Pair uf1 cn uf2 ->
anaBinaryPair fns (fns, d) (uf1, cn, uf2)
TBF_THF_Binary_Tuple bt -> anaBinaryTuple fns (fns, d) bt
anaBinaryPair' :: (AnaFuns a b, a) -> (THFUnitaryFormula,
THFPairConnective, THFUnitaryFormula)
-> Result [b]
anaBinaryPair' (fns, d) (uf1, _, uf2) = do
l1 <- anaUnitaryFormula fns (fns, d) uf1
l2 <- anaUnitaryFormula fns (fns, d) uf2
return $ l1 ++ l2
anaBinaryTuple' :: (AnaFuns a b, a) -> THFBinaryTuple -> Result [b]
anaBinaryTuple' (fns, d) bt = case bt of
TBT_THF_Or_Formula ufs -> do
r <- mapR (anaUnitaryFormula fns (fns, d)) ufs
return $ concat r
TBT_THF_And_Formula ufs -> do
r <- mapR (anaUnitaryFormula fns (fns, d)) ufs
return $ concat r
TBT_THF_Apply_Formula ufs -> do
r <- mapR (anaUnitaryFormula fns (fns, d)) ufs
return $ concat r
anaUnitaryFormula' :: (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula' (fns, d) uf = case uf of
TUF_THF_Conditional {} ->
mkError ("THF.Utils.anaUnitaryFOrmula: " ++
"Conditional not in THF0!") uf
TUF_THF_Quantified_Formula qf -> anaQuantifiedFormula fns (fns, d) qf
TUF_THF_Unary_Formula _ lf -> anaLogicFormula fns (fns, d) lf
TUF_THF_Atom a -> anaAtom fns (fns, d) a
TUF_THF_Tuple t -> do
r <- mapR (anaLogicFormula fns (fns, d)) t
return $ concat r
TUF_THF_Logic_Formula_Par lf -> anaLogicFormula fns (fns, d) lf
T0UF_THF_Abstraction vs uf' -> do
l1 <- anaVariableList fns (fns, d) vs
l2 <- anaUnitaryFormula fns (fns, d) uf'
return $ l1 ++ l2
anaQuantifiedFormula' :: (AnaFuns a b, a) -> THFQuantifiedFormula
-> Result [b]
anaQuantifiedFormula' (fns, d) qf = case qf of
TQF_THF_Quantified_Formula _ vs uf -> do
l1 <- anaVariableList fns (fns, d) vs
l2 <- anaUnitaryFormula fns (fns, d) uf
return $ l1 ++ l2
T0QF_THF_Quantified_Var _ vs uf -> do
l1 <- anaVariableList fns (fns, d) vs
l2 <- anaUnitaryFormula fns (fns, d) uf
return $ l1 ++ l2
T0QF_THF_Quantified_Novar _ _ ->
mkError "THF.Utils.anaQuantifiedFormula: Quantified Novar not in THF0!" qf
anaVariableList' :: (AnaFuns a b, a) -> [THFVariable] -> Result [b]
anaVariableList' _ _ = return []
anaAtom' :: (AnaFuns a b, a) -> THFAtom -> Result [b]
anaAtom' (fns, d) a = case a of
TA_Term _ -> mkError "THF.Utils.anaAtom: Term not in THF0!" a
TA_THF_Conn_Term c -> anaConnTerm fns (fns, d) c
TA_Defined_Type _ ->
mkError "THF.Utils.anaAtom: Defined Type not in THF0!" a
TA_Defined_Plain_Formula _ ->
mkError "THF.Utils.anaAtom: Defined Plain Formula not in THF0!" a
TA_System_Type _ ->
mkError "THF.Utils.anaAtom: System Type not in THF0!" a
TA_System_Atomic_Formula _ ->
mkError "THF.Utils.anaAtom: System Atomic Formula not in THF0!" a
T0A_Constant c -> anaConst fns (fns, d) c
T0A_Defined_Constant _ -> return []
T0A_System_Constant _ -> return []
T0A_Variable v -> anaVariableList fns (fns, d) [TV_Variable v]
anaConst' :: (AnaFuns a b, a) -> Constant -> Result [b]
anaConst' _ _ = return []
anaConnTerm' :: (AnaFuns a b, a) -> THFConnTerm -> Result [b]
anaConnTerm' _ _ = return []