content: {-# 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)
  
  -- taken from http://www.haskell.org/haskellwiki/New_monads/MonadUnique
  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 []
  