{-# 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 (a -> UniqueT m b -> UniqueT m a
(a -> b) -> UniqueT m a -> UniqueT m b
(forall a b. (a -> b) -> UniqueT m a -> UniqueT m b)
-> (forall a b. a -> UniqueT m b -> UniqueT m a)
-> Functor (UniqueT m)
forall a b. a -> UniqueT m b -> UniqueT m a
forall a b. (a -> b) -> UniqueT m a -> UniqueT m b
forall (m :: * -> *) a b.
Functor m =>
a -> UniqueT m b -> UniqueT m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> UniqueT m a -> UniqueT m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> UniqueT m b -> UniqueT m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> UniqueT m b -> UniqueT m a
fmap :: (a -> b) -> UniqueT m a -> UniqueT m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> UniqueT m a -> UniqueT m b
Functor, Functor (UniqueT m)
a -> UniqueT m a
Functor (UniqueT m) =>
(forall a. a -> UniqueT m a)
-> (forall a b. UniqueT m (a -> b) -> UniqueT m a -> UniqueT m b)
-> (forall a b c.
    (a -> b -> c) -> UniqueT m a -> UniqueT m b -> UniqueT m c)
-> (forall a b. UniqueT m a -> UniqueT m b -> UniqueT m b)
-> (forall a b. UniqueT m a -> UniqueT m b -> UniqueT m a)
-> Applicative (UniqueT m)
UniqueT m a -> UniqueT m b -> UniqueT m b
UniqueT m a -> UniqueT m b -> UniqueT m a
UniqueT m (a -> b) -> UniqueT m a -> UniqueT m b
(a -> b -> c) -> UniqueT m a -> UniqueT m b -> UniqueT m c
forall a. a -> UniqueT m a
forall a b. UniqueT m a -> UniqueT m b -> UniqueT m a
forall a b. UniqueT m a -> UniqueT m b -> UniqueT m b
forall a b. UniqueT m (a -> b) -> UniqueT m a -> UniqueT m b
forall a b c.
(a -> b -> c) -> UniqueT m a -> UniqueT m b -> UniqueT m c
forall (m :: * -> *). Monad m => Functor (UniqueT m)
forall (m :: * -> *) a. Monad m => a -> UniqueT m a
forall (m :: * -> *) a b.
Monad m =>
UniqueT m a -> UniqueT m b -> UniqueT m a
forall (m :: * -> *) a b.
Monad m =>
UniqueT m a -> UniqueT m b -> UniqueT m b
forall (m :: * -> *) a b.
Monad m =>
UniqueT m (a -> b) -> UniqueT m a -> UniqueT m b
forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> UniqueT m a -> UniqueT m b -> UniqueT m c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: UniqueT m a -> UniqueT m b -> UniqueT m a
$c<* :: forall (m :: * -> *) a b.
Monad m =>
UniqueT m a -> UniqueT m b -> UniqueT m a
*> :: UniqueT m a -> UniqueT m b -> UniqueT m b
$c*> :: forall (m :: * -> *) a b.
Monad m =>
UniqueT m a -> UniqueT m b -> UniqueT m b
liftA2 :: (a -> b -> c) -> UniqueT m a -> UniqueT m b -> UniqueT m c
$cliftA2 :: forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> UniqueT m a -> UniqueT m b -> UniqueT m c
<*> :: UniqueT m (a -> b) -> UniqueT m a -> UniqueT m b
$c<*> :: forall (m :: * -> *) a b.
Monad m =>
UniqueT m (a -> b) -> UniqueT m a -> UniqueT m b
pure :: a -> UniqueT m a
$cpure :: forall (m :: * -> *) a. Monad m => a -> UniqueT m a
$cp1Applicative :: forall (m :: * -> *). Monad m => Functor (UniqueT m)
Applicative, Applicative (UniqueT m)
a -> UniqueT m a
Applicative (UniqueT m) =>
(forall a b. UniqueT m a -> (a -> UniqueT m b) -> UniqueT m b)
-> (forall a b. UniqueT m a -> UniqueT m b -> UniqueT m b)
-> (forall a. a -> UniqueT m a)
-> Monad (UniqueT m)
UniqueT m a -> (a -> UniqueT m b) -> UniqueT m b
UniqueT m a -> UniqueT m b -> UniqueT m b
forall a. a -> UniqueT m a
forall a b. UniqueT m a -> UniqueT m b -> UniqueT m b
forall a b. UniqueT m a -> (a -> UniqueT m b) -> UniqueT m b
forall (m :: * -> *). Monad m => Applicative (UniqueT m)
forall (m :: * -> *) a. Monad m => a -> UniqueT m a
forall (m :: * -> *) a b.
Monad m =>
UniqueT m a -> UniqueT m b -> UniqueT m b
forall (m :: * -> *) a b.
Monad m =>
UniqueT m a -> (a -> UniqueT m b) -> UniqueT m b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> UniqueT m a
$creturn :: forall (m :: * -> *) a. Monad m => a -> UniqueT m a
>> :: UniqueT m a -> UniqueT m b -> UniqueT m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
UniqueT m a -> UniqueT m b -> UniqueT m b
>>= :: UniqueT m a -> (a -> UniqueT m b) -> UniqueT m b
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
UniqueT m a -> (a -> UniqueT m b) -> UniqueT m b
$cp1Monad :: forall (m :: * -> *). Monad m => Applicative (UniqueT m)
Monad, m a -> UniqueT m a
(forall (m :: * -> *) a. Monad m => m a -> UniqueT m a)
-> MonadTrans UniqueT
forall (m :: * -> *) a. Monad m => m a -> UniqueT m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
lift :: m a -> UniqueT m a
$clift :: forall (m :: * -> *) a. Monad m => m a -> UniqueT m a
MonadTrans, Monad (UniqueT m)
Monad (UniqueT m) =>
(forall a. IO a -> UniqueT m a) -> MonadIO (UniqueT m)
IO a -> UniqueT m a
forall a. IO a -> UniqueT m a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
forall (m :: * -> *). MonadIO m => Monad (UniqueT m)
forall (m :: * -> *) a. MonadIO m => IO a -> UniqueT m a
liftIO :: IO a -> UniqueT m a
$cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> UniqueT m a
$cp1MonadIO :: forall (m :: * -> *). MonadIO m => Monad (UniqueT m)
MonadIO)

newtype Unique a = Unique (UniqueT Identity a)
    deriving (a -> Unique b -> Unique a
(a -> b) -> Unique a -> Unique b
(forall a b. (a -> b) -> Unique a -> Unique b)
-> (forall a b. a -> Unique b -> Unique a) -> Functor Unique
forall a b. a -> Unique b -> Unique a
forall a b. (a -> b) -> Unique a -> Unique b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Unique b -> Unique a
$c<$ :: forall a b. a -> Unique b -> Unique a
fmap :: (a -> b) -> Unique a -> Unique b
$cfmap :: forall a b. (a -> b) -> Unique a -> Unique b
Functor, Functor Unique
a -> Unique a
Functor Unique =>
(forall a. a -> Unique a)
-> (forall a b. Unique (a -> b) -> Unique a -> Unique b)
-> (forall a b c.
    (a -> b -> c) -> Unique a -> Unique b -> Unique c)
-> (forall a b. Unique a -> Unique b -> Unique b)
-> (forall a b. Unique a -> Unique b -> Unique a)
-> Applicative Unique
Unique a -> Unique b -> Unique b
Unique a -> Unique b -> Unique a
Unique (a -> b) -> Unique a -> Unique b
(a -> b -> c) -> Unique a -> Unique b -> Unique c
forall a. a -> Unique a
forall a b. Unique a -> Unique b -> Unique a
forall a b. Unique a -> Unique b -> Unique b
forall a b. Unique (a -> b) -> Unique a -> Unique b
forall a b c. (a -> b -> c) -> Unique a -> Unique b -> Unique c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: Unique a -> Unique b -> Unique a
$c<* :: forall a b. Unique a -> Unique b -> Unique a
*> :: Unique a -> Unique b -> Unique b
$c*> :: forall a b. Unique a -> Unique b -> Unique b
liftA2 :: (a -> b -> c) -> Unique a -> Unique b -> Unique c
$cliftA2 :: forall a b c. (a -> b -> c) -> Unique a -> Unique b -> Unique c
<*> :: Unique (a -> b) -> Unique a -> Unique b
$c<*> :: forall a b. Unique (a -> b) -> Unique a -> Unique b
pure :: a -> Unique a
$cpure :: forall a. a -> Unique a
$cp1Applicative :: Functor Unique
Applicative, Applicative Unique
a -> Unique a
Applicative Unique =>
(forall a b. Unique a -> (a -> Unique b) -> Unique b)
-> (forall a b. Unique a -> Unique b -> Unique b)
-> (forall a. a -> Unique a)
-> Monad Unique
Unique a -> (a -> Unique b) -> Unique b
Unique a -> Unique b -> Unique b
forall a. a -> Unique a
forall a b. Unique a -> Unique b -> Unique b
forall a b. Unique a -> (a -> Unique b) -> Unique b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> Unique a
$creturn :: forall a. a -> Unique a
>> :: Unique a -> Unique b -> Unique b
$c>> :: forall a b. Unique a -> Unique b -> Unique b
>>= :: Unique a -> (a -> Unique b) -> Unique b
$c>>= :: forall a b. Unique a -> (a -> Unique b) -> Unique b
$cp1Monad :: Applicative Unique
Monad, Monad Unique
Unique Integer
Monad Unique => Unique Integer -> MonadUnique Unique
forall (m :: * -> *). Monad m => m Integer -> MonadUnique m
fresh :: Unique Integer
$cfresh :: Unique Integer
$cp1MonadUnique :: Monad Unique
MonadUnique)

class Monad m => MonadUnique m where
    fresh :: m Integer

instance (Monad m) => MonadUnique (UniqueT m) where
    fresh :: UniqueT m Integer
fresh = StateT Integer m Integer -> UniqueT m Integer
forall (m :: * -> *) a. StateT Integer m a -> UniqueT m a
UniqueT (StateT Integer m Integer -> UniqueT m Integer)
-> StateT Integer m Integer -> UniqueT m Integer
forall a b. (a -> b) -> a -> b
$ do
                Integer
n <- StateT Integer m Integer
forall s (m :: * -> *). MonadState s m => m s
get
                Integer -> StateT Integer m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Integer -> Integer
forall a. Enum a => a -> a
succ Integer
n)
                Integer -> StateT Integer m Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
n

evalUniqueT :: Monad m => UniqueT m a -> m a
evalUniqueT :: UniqueT m a -> m a
evalUniqueT (UniqueT s :: StateT Integer m a
s) = StateT Integer m a -> Integer -> m a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT Integer m a
s 1

evalUnique :: Unique a -> a
evalUnique :: Unique a -> a
evalUnique (Unique s :: UniqueT Identity a
s) = Identity a -> a
forall a. Identity a -> a
runIdentity (UniqueT Identity a -> Identity a
forall (m :: * -> *) a. Monad m => UniqueT m a -> m a
evalUniqueT UniqueT Identity a
s)

addSuffix :: String -> AtomicWord -> AtomicWord
addSuffix :: String -> AtomicWord -> AtomicWord
addSuffix s :: String
s a :: AtomicWord
a = case AtomicWord
a of
  A_Lower_Word t :: Token
t -> Token -> AtomicWord
A_Lower_Word (Token -> AtomicWord) -> Token -> AtomicWord
forall a b. (a -> b) -> a -> b
$ Token -> Token
rename Token
t
  A_Single_Quoted t :: Token
t -> Token -> AtomicWord
A_Single_Quoted (Token -> AtomicWord) -> Token -> AtomicWord
forall a b. (a -> b) -> a -> b
$ Token -> Token
rename Token
t
 where rename :: Token -> Token
rename t :: Token
t = Token
t { tokStr :: String
tokStr = Token -> String
tokStr Token
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s }

addSuffixN :: String -> Name -> Name
addSuffixN :: String -> Name -> Name
addSuffixN s :: String
s n :: Name
n = case Name
n of
  N_Atomic_Word a :: AtomicWord
a -> AtomicWord -> Name
N_Atomic_Word (AtomicWord -> Name) -> AtomicWord -> Name
forall a b. (a -> b) -> a -> b
$ String -> AtomicWord -> AtomicWord
addSuffix String
s AtomicWord
a
  N_Integer t :: Token
t -> String -> Token -> Name
rename String
s Token
t
  T0N_Unsigned_Integer t :: Token
t -> String -> Token -> Name
rename String
s Token
t
 where rename :: String -> Token -> Name
rename sf :: String
sf t :: Token
t = AtomicWord -> Name
N_Atomic_Word (AtomicWord -> Name) -> AtomicWord -> Name
forall a b. (a -> b) -> a -> b
$ String -> AtomicWord -> AtomicWord
addSuffix String
sf
                      (Token -> AtomicWord
A_Lower_Word (Token -> AtomicWord) -> Token -> AtomicWord
forall a b. (a -> b) -> a -> b
$ Token
t { tokStr :: String
tokStr = 'i' Char -> String -> String
forall a. a -> [a] -> [a]
: Token -> String
forall a. Show a => a -> String
show Token
t })

numbered :: Monad m => AtomicWord -> UniqueT m AtomicWord
numbered :: AtomicWord -> UniqueT m AtomicWord
numbered a :: AtomicWord
a = do
 Integer
f <- UniqueT m Integer
forall (m :: * -> *). MonadUnique m => m Integer
fresh
 AtomicWord -> UniqueT m AtomicWord
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> AtomicWord -> AtomicWord
addSuffix ('_' Char -> String -> String
forall a. a -> [a] -> [a]
: Integer -> String
forall a. Show a => a -> String
show Integer
f) AtomicWord
a)

numberedTok :: Monad m => Token -> UniqueT m Token
numberedTok :: Token -> UniqueT m Token
numberedTok = (AtomicWord -> Token) -> UniqueT m AtomicWord -> UniqueT m Token
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM AtomicWord -> Token
toToken (UniqueT m AtomicWord -> UniqueT m Token)
-> (Token -> UniqueT m AtomicWord) -> Token -> UniqueT m Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtomicWord -> UniqueT m AtomicWord
forall (m :: * -> *). Monad m => AtomicWord -> UniqueT m AtomicWord
numbered (AtomicWord -> UniqueT m AtomicWord)
-> (Token -> AtomicWord) -> Token -> UniqueT m AtomicWord
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> AtomicWord
A_Single_Quoted

mkNames :: Constant -> Name -> Int -> [(Constant, Name)]
mkNames :: AtomicWord -> Name -> Int -> [(AtomicWord, Name)]
mkNames c :: AtomicWord
c n :: Name
n i :: Int
i = Unique [(AtomicWord, Name)] -> [(AtomicWord, Name)]
forall a. Unique a -> a
evalUnique (Unique [(AtomicWord, Name)] -> [(AtomicWord, Name)])
-> Unique [(AtomicWord, Name)] -> [(AtomicWord, Name)]
forall a b. (a -> b) -> a -> b
$ Int -> Unique (AtomicWord, Name) -> Unique [(AtomicWord, Name)]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
i (Unique (AtomicWord, Name) -> Unique [(AtomicWord, Name)])
-> Unique (AtomicWord, Name) -> Unique [(AtomicWord, Name)]
forall a b. (a -> b) -> a -> b
$ do
 Integer
f <- Unique Integer
forall (m :: * -> *). MonadUnique m => m Integer
fresh
 let s :: String
s = '_' Char -> String -> String
forall a. a -> [a] -> [a]
: Integer -> String
forall a. Show a => a -> String
show Integer
f
 (AtomicWord, Name) -> Unique (AtomicWord, Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> AtomicWord -> AtomicWord
addSuffix String
s AtomicWord
c, String -> Name -> Name
addSuffixN String
s Name
n)

recreateSymbols :: SignTHF -> SignTHF
recreateSymbols :: SignTHF -> SignTHF
recreateSymbols (Sign tps :: TypeMap
tps cs :: ConstMap
cs _) =
 let name :: AtomicWord -> Name
name = AtomicWord -> Name
N_Atomic_Word
     symbs1 :: Map AtomicWord SymbolTHF
symbs1 = (Map AtomicWord SymbolTHF
 -> (AtomicWord, TypeInfo) -> Map AtomicWord SymbolTHF)
-> Map AtomicWord SymbolTHF
-> [(AtomicWord, TypeInfo)]
-> Map AtomicWord SymbolTHF
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: Map AtomicWord SymbolTHF
m (c :: AtomicWord
c, t :: TypeInfo
t) -> AtomicWord
-> SymbolTHF
-> Map AtomicWord SymbolTHF
-> Map AtomicWord SymbolTHF
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AtomicWord
c
                      (AtomicWord -> Name -> SymbolType -> SymbolTHF
Symbol AtomicWord
c (AtomicWord -> Name
name AtomicWord
c) (Kind -> SymbolType
ST_Type (Kind -> SymbolType) -> Kind -> SymbolType
forall a b. (a -> b) -> a -> b
$ TypeInfo -> Kind
typeKind TypeInfo
t)) Map AtomicWord SymbolTHF
m)
              Map AtomicWord SymbolTHF
forall k a. Map k a
Map.empty ([(AtomicWord, TypeInfo)] -> Map AtomicWord SymbolTHF)
-> [(AtomicWord, TypeInfo)] -> Map AtomicWord SymbolTHF
forall a b. (a -> b) -> a -> b
$ TypeMap -> [(AtomicWord, TypeInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList TypeMap
tps
     symbs :: Map AtomicWord SymbolTHF
symbs = (Map AtomicWord SymbolTHF
 -> (AtomicWord, ConstInfo) -> Map AtomicWord SymbolTHF)
-> Map AtomicWord SymbolTHF
-> [(AtomicWord, ConstInfo)]
-> Map AtomicWord SymbolTHF
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m :: Map AtomicWord SymbolTHF
m (c :: AtomicWord
c, k :: ConstInfo
k) -> AtomicWord
-> SymbolTHF
-> Map AtomicWord SymbolTHF
-> Map AtomicWord SymbolTHF
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert AtomicWord
c
                      (AtomicWord -> Name -> SymbolType -> SymbolTHF
Symbol AtomicWord
c (AtomicWord -> Name
name AtomicWord
c) (Type -> SymbolType
ST_Const (Type -> SymbolType) -> Type -> SymbolType
forall a b. (a -> b) -> a -> b
$ ConstInfo -> Type
constType ConstInfo
k)) Map AtomicWord SymbolTHF
m)
              Map AtomicWord SymbolTHF
symbs1 ([(AtomicWord, ConstInfo)] -> Map AtomicWord SymbolTHF)
-> [(AtomicWord, ConstInfo)] -> Map AtomicWord SymbolTHF
forall a b. (a -> b) -> a -> b
$ ConstMap -> [(AtomicWord, ConstInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList ConstMap
cs
 in TypeMap -> ConstMap -> Map AtomicWord SymbolTHF -> SignTHF
Sign TypeMap
tps ConstMap
cs Map AtomicWord SymbolTHF
symbs

toToken :: Constant -> Token
toToken :: AtomicWord -> Token
toToken (A_Lower_Word t :: Token
t) = Token
t
toToken (A_Single_Quoted t :: Token
t) = Token
t

toId :: Constant -> Id
toId :: AtomicWord -> Id
toId c :: AtomicWord
c = [Token] -> Id
mkId [AtomicWord -> Token
toToken AtomicWord
c]

thfTopLevelTypeToType :: THFTopLevelType -> Maybe Type
thfTopLevelTypeToType :: THFTopLevelType -> Maybe Type
thfTopLevelTypeToType tlt :: THFTopLevelType
tlt = case THFTopLevelType
tlt of
    T0TLT_Defined_Type dt :: DefinedType
dt -> DefinedType -> Maybe Type
thfDefinedTypeToType DefinedType
dt
    T0TLT_THF_Binary_Type bt :: THFBinaryType
bt -> THFBinaryType -> Maybe Type
thfBinaryTypeToType THFBinaryType
bt
    T0TLT_Constant c :: AtomicWord
c -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ AtomicWord -> Type
CType AtomicWord
c
    T0TLT_System_Type st :: Token
st -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Token -> Type
SType Token
st
    T0TLT_Variable v :: Token
v -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Token -> Type
VType Token
v
    _ -> Maybe Type
forall a. Maybe a
Nothing

thfDefinedTypeToType :: DefinedType -> Maybe Type
thfDefinedTypeToType :: DefinedType -> Maybe Type
thfDefinedTypeToType dt :: DefinedType
dt = case DefinedType
dt of
    DT_oType -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
OType
    DT_o -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
OType
    DT_iType -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
IType
    DT_i -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
IType
    DT_tType -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
TType
    _ -> Maybe Type
forall a. Maybe a
Nothing

thfBinaryTypeToType :: THFBinaryType -> Maybe Type
thfBinaryTypeToType :: THFBinaryType -> Maybe Type
thfBinaryTypeToType bt :: THFBinaryType
bt = case THFBinaryType
bt of
    TBT_THF_Mapping_Type [] -> Maybe Type
forall a. Maybe a
Nothing
    TBT_THF_Mapping_Type (_ : []) -> Maybe Type
forall a. Maybe a
Nothing
    TBT_THF_Mapping_Type mt :: [THFUnitaryType]
mt -> [THFUnitaryType] -> Maybe Type
thfMappingTypeToType [THFUnitaryType]
mt
    T0BT_THF_Binary_Type_Par btp :: THFBinaryType
btp -> (Type -> Type) -> Maybe Type -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> Type
ParType (THFBinaryType -> Maybe Type
thfBinaryTypeToType THFBinaryType
btp)
    TBT_THF_Xprod_Type [] -> Maybe Type
forall a. Maybe a
Nothing
    TBT_THF_Xprod_Type (u :: THFUnitaryType
u : []) -> THFUnitaryType -> Maybe Type
thfUnitaryTypeToType THFUnitaryType
u
    TBT_THF_Xprod_Type us :: [THFUnitaryType]
us -> let us' :: [Maybe Type]
us' = (THFUnitaryType -> Maybe Type) -> [THFUnitaryType] -> [Maybe Type]
forall a b. (a -> b) -> [a] -> [b]
map THFUnitaryType -> Maybe Type
thfUnitaryTypeToType [THFUnitaryType]
us
                                       in if (Maybe Type -> Bool) -> [Maybe Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust [Maybe Type]
us' then
                                           (Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> ([Type] -> Type) -> [Type] -> Maybe Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> Type
ProdType) ([Type] -> Maybe Type) -> [Type] -> Maybe Type
forall a b. (a -> b) -> a -> b
$ (Maybe Type -> Type) -> [Maybe Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Maybe Type -> Type
forall a. HasCallStack => Maybe a -> a
fromJust [Maybe Type]
us'
                                          else Maybe Type
forall a. Maybe a
Nothing
    _ -> Maybe Type
forall a. Maybe a
Nothing

thfMappingTypeToType :: [THFUnitaryType] -> Maybe Type
thfMappingTypeToType :: [THFUnitaryType] -> Maybe Type
thfMappingTypeToType [] = Maybe Type
forall a. Maybe a
Nothing
thfMappingTypeToType (u :: THFUnitaryType
u : []) = THFUnitaryType -> Maybe Type
thfUnitaryTypeToType THFUnitaryType
u
thfMappingTypeToType (u :: THFUnitaryType
u : ru :: [THFUnitaryType]
ru) =
    let k1 :: Maybe Type
k1 = THFUnitaryType -> Maybe Type
thfUnitaryTypeToType THFUnitaryType
u
        k2 :: Maybe Type
k2 = [THFUnitaryType] -> Maybe Type
thfMappingTypeToType [THFUnitaryType]
ru
    in if Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust Maybe Type
k1 Bool -> Bool -> Bool
&& Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust Maybe Type
k2
       then Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
MapType (Maybe Type -> Type
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Type
k1) (Maybe Type -> Type
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Type
k2)
       else Maybe Type
forall a. Maybe a
Nothing

thfUnitaryTypeToType :: THFUnitaryType -> Maybe Type
thfUnitaryTypeToType :: THFUnitaryType -> Maybe Type
thfUnitaryTypeToType ut :: THFUnitaryType
ut = case THFUnitaryType
ut of
    T0UT_THF_Binary_Type_Par bt :: THFBinaryType
bt -> (Type -> Type) -> Maybe Type -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> Type
ParType (THFBinaryType -> Maybe Type
thfBinaryTypeToType THFBinaryType
bt)
    T0UT_Defined_Type dt :: DefinedType
dt -> DefinedType -> Maybe Type
thfDefinedTypeToType DefinedType
dt
    T0UT_Constant c :: AtomicWord
c -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ AtomicWord -> Type
CType AtomicWord
c
    T0UT_System_Type st :: Token
st -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Token -> Type
SType Token
st
    T0UT_Variable v :: Token
v -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Token -> Type
VType Token
v
    _ -> Maybe Type
forall a. Maybe a
Nothing

typeToTopLevelType :: Type -> Result THFTopLevelType
typeToTopLevelType :: Type -> Result THFTopLevelType
typeToTopLevelType t :: Type
t = case Type
t of
 TType -> THFTopLevelType -> Result THFTopLevelType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFTopLevelType -> Result THFTopLevelType)
-> THFTopLevelType -> Result THFTopLevelType
forall a b. (a -> b) -> a -> b
$ DefinedType -> THFTopLevelType
T0TLT_Defined_Type DefinedType
DT_tType
 OType -> THFTopLevelType -> Result THFTopLevelType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFTopLevelType -> Result THFTopLevelType)
-> THFTopLevelType -> Result THFTopLevelType
forall a b. (a -> b) -> a -> b
$ DefinedType -> THFTopLevelType
T0TLT_Defined_Type DefinedType
DT_oType
 IType -> THFTopLevelType -> Result THFTopLevelType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFTopLevelType -> Result THFTopLevelType)
-> THFTopLevelType -> Result THFTopLevelType
forall a b. (a -> b) -> a -> b
$ DefinedType -> THFTopLevelType
T0TLT_Defined_Type DefinedType
DT_iType
 MapType t1 :: Type
t1 t2 :: Type
t2 -> ([THFUnitaryType] -> THFTopLevelType)
-> Result [THFUnitaryType] -> Result THFTopLevelType
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (THFBinaryType -> THFTopLevelType
T0TLT_THF_Binary_Type (THFBinaryType -> THFTopLevelType)
-> ([THFUnitaryType] -> THFBinaryType)
-> [THFUnitaryType]
-> THFTopLevelType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [THFUnitaryType] -> THFBinaryType
TBT_THF_Mapping_Type)
                        ((Type -> Result THFUnitaryType)
-> [Type] -> Result [THFUnitaryType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> Result THFUnitaryType
typeToUnitaryType [Type
t1, Type
t2])
 ProdType ts :: [Type]
ts -> ([THFUnitaryType] -> THFTopLevelType)
-> Result [THFUnitaryType] -> Result THFTopLevelType
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (THFBinaryType -> THFTopLevelType
T0TLT_THF_Binary_Type (THFBinaryType -> THFTopLevelType)
-> ([THFUnitaryType] -> THFBinaryType)
-> [THFUnitaryType]
-> THFTopLevelType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [THFUnitaryType] -> THFBinaryType
TBT_THF_Xprod_Type)
                      ((Type -> Result THFUnitaryType)
-> [Type] -> Result [THFUnitaryType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> Result THFUnitaryType
typeToUnitaryType [Type]
ts)
 CType c :: AtomicWord
c -> THFTopLevelType -> Result THFTopLevelType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFTopLevelType -> Result THFTopLevelType)
-> THFTopLevelType -> Result THFTopLevelType
forall a b. (a -> b) -> a -> b
$ AtomicWord -> THFTopLevelType
T0TLT_Constant AtomicWord
c
 SType t' :: Token
t' -> THFTopLevelType -> Result THFTopLevelType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFTopLevelType -> Result THFTopLevelType)
-> THFTopLevelType -> Result THFTopLevelType
forall a b. (a -> b) -> a -> b
$ Token -> THFTopLevelType
T0TLT_System_Type Token
t'
 VType t' :: Token
t' -> THFTopLevelType -> Result THFTopLevelType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFTopLevelType -> Result THFTopLevelType)
-> THFTopLevelType -> Result THFTopLevelType
forall a b. (a -> b) -> a -> b
$ Token -> THFTopLevelType
T0TLT_Variable Token
t'
 ParType t' :: Type
t' -> (THFBinaryType -> THFTopLevelType)
-> Result THFBinaryType -> Result THFTopLevelType
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (THFBinaryType -> THFTopLevelType
T0TLT_THF_Binary_Type (THFBinaryType -> THFTopLevelType)
-> (THFBinaryType -> THFBinaryType)
-> THFBinaryType
-> THFTopLevelType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFBinaryType -> THFBinaryType
T0BT_THF_Binary_Type_Par)
                     (Type -> Result THFBinaryType
typeToBinaryType Type
t')

typeToUnitaryType :: Type -> Result THFUnitaryType
typeToUnitaryType :: Type -> Result THFUnitaryType
typeToUnitaryType t :: Type
t = do
 THFTopLevelType
tl <- Type -> Result THFTopLevelType
typeToTopLevelType Type
t
 case THFTopLevelType
tl of
  T0TLT_Constant c :: AtomicWord
c -> THFUnitaryType -> Result THFUnitaryType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryType -> Result THFUnitaryType)
-> THFUnitaryType -> Result THFUnitaryType
forall a b. (a -> b) -> a -> b
$ AtomicWord -> THFUnitaryType
T0UT_Constant AtomicWord
c
  T0TLT_Variable t' :: Token
t' -> THFUnitaryType -> Result THFUnitaryType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryType -> Result THFUnitaryType)
-> THFUnitaryType -> Result THFUnitaryType
forall a b. (a -> b) -> a -> b
$ Token -> THFUnitaryType
T0UT_Variable Token
t'
  T0TLT_Defined_Type d :: DefinedType
d -> THFUnitaryType -> Result THFUnitaryType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryType -> Result THFUnitaryType)
-> THFUnitaryType -> Result THFUnitaryType
forall a b. (a -> b) -> a -> b
$ DefinedType -> THFUnitaryType
T0UT_Defined_Type DefinedType
d
  T0TLT_System_Type t' :: Token
t' -> THFUnitaryType -> Result THFUnitaryType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryType -> Result THFUnitaryType)
-> THFUnitaryType -> Result THFUnitaryType
forall a b. (a -> b) -> a -> b
$ Token -> THFUnitaryType
T0UT_System_Type Token
t'
  T0TLT_THF_Binary_Type b :: THFBinaryType
b -> THFUnitaryType -> Result THFUnitaryType
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryType -> Result THFUnitaryType)
-> THFUnitaryType -> Result THFUnitaryType
forall a b. (a -> b) -> a -> b
$ THFBinaryType -> THFUnitaryType
T0UT_THF_Binary_Type_Par THFBinaryType
b
  TTLT_THF_Logic_Formula _ -> String -> Range -> Result THFUnitaryType
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Not yet implemented!" Range
nullRange

typeToBinaryType :: Type -> Result THFBinaryType
typeToBinaryType :: Type -> Result THFBinaryType
typeToBinaryType t :: Type
t = do
 THFTopLevelType
tl <- Type -> Result THFTopLevelType
typeToTopLevelType Type
t
 case THFTopLevelType
tl of
  T0TLT_THF_Binary_Type b :: THFBinaryType
b -> THFBinaryType -> Result THFBinaryType
forall (m :: * -> *) a. Monad m => a -> m a
return THFBinaryType
b
  _ -> String -> Range -> Result THFBinaryType
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError ("Cannot represent type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
t String -> String -> String
forall a. [a] -> [a] -> [a]
++
                "as THFBinaryType!") Range
nullRange

data RewriteFuns a = RewriteFuns {
 RewriteFuns a
-> (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
rewriteLogicFormula :: (RewriteFuns a, a) -> THFLogicFormula
  -> Result THFLogicFormula,
 RewriteFuns a
-> (RewriteFuns a, a)
-> THFBinaryFormula
-> Result THFBinaryFormula
rewriteBinaryFormula :: (RewriteFuns a, a) -> THFBinaryFormula
  -> Result THFBinaryFormula,
 RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula :: (RewriteFuns a, a) -> THFUnitaryFormula
  -> Result THFUnitaryFormula,
 RewriteFuns a
-> (RewriteFuns a, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result THFBinaryFormula
rewriteBinaryPair :: (RewriteFuns a, a) -> (THFUnitaryFormula,
                       THFPairConnective, THFUnitaryFormula)
                       -> Result THFBinaryFormula,
 RewriteFuns a
-> (RewriteFuns a, a) -> THFBinaryTuple -> Result THFBinaryTuple
rewriteBinaryTuple :: (RewriteFuns a, a) -> THFBinaryTuple
                        -> Result THFBinaryTuple,
 RewriteFuns a
-> (RewriteFuns a, a)
-> THFQuantifiedFormula
-> Result THFQuantifiedFormula
rewriteQuantifiedFormula :: (RewriteFuns a, a) -> THFQuantifiedFormula
                              -> Result THFQuantifiedFormula,
 RewriteFuns a
-> (RewriteFuns a, a) -> THFAtom -> Result THFUnitaryFormula
rewriteAtom :: (RewriteFuns a, a) -> THFAtom -> Result THFUnitaryFormula,
 RewriteFuns a
-> (RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
rewriteVariableList :: (RewriteFuns a, a) -> [THFVariable]
                         -> Result [THFVariable],
 RewriteFuns a
-> (RewriteFuns a, a) -> AtomicWord -> Result THFUnitaryFormula
rewriteConst :: (RewriteFuns a, a) -> Constant -> Result THFUnitaryFormula,
 RewriteFuns a
-> (RewriteFuns a, a) -> THFConnTerm -> Result THFConnTerm
rewriteConnTerm :: (RewriteFuns a, a) -> THFConnTerm -> Result THFConnTerm }

rewriteTHF0 :: RewriteFuns a
rewriteTHF0 :: RewriteFuns a
rewriteTHF0 = RewriteFuns :: forall a.
((RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula)
-> ((RewriteFuns a, a)
    -> THFBinaryFormula -> Result THFBinaryFormula)
-> ((RewriteFuns a, a)
    -> THFUnitaryFormula -> Result THFUnitaryFormula)
-> ((RewriteFuns a, a)
    -> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
    -> Result THFBinaryFormula)
-> ((RewriteFuns a, a) -> THFBinaryTuple -> Result THFBinaryTuple)
-> ((RewriteFuns a, a)
    -> THFQuantifiedFormula -> Result THFQuantifiedFormula)
-> ((RewriteFuns a, a) -> THFAtom -> Result THFUnitaryFormula)
-> ((RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable])
-> ((RewriteFuns a, a) -> AtomicWord -> Result THFUnitaryFormula)
-> ((RewriteFuns a, a) -> THFConnTerm -> Result THFConnTerm)
-> RewriteFuns a
RewriteFuns {
 rewriteLogicFormula :: (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
rewriteLogicFormula = (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
forall a.
(RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
rewriteLogicFormula',
 rewriteBinaryFormula :: (RewriteFuns a, a) -> THFBinaryFormula -> Result THFBinaryFormula
rewriteBinaryFormula = (RewriteFuns a, a) -> THFBinaryFormula -> Result THFBinaryFormula
forall a.
(RewriteFuns a, a) -> THFBinaryFormula -> Result THFBinaryFormula
rewriteBinaryFormula',
 rewriteUnitaryFormula :: (RewriteFuns a, a) -> THFUnitaryFormula -> Result THFUnitaryFormula
rewriteUnitaryFormula = (RewriteFuns a, a) -> THFUnitaryFormula -> Result THFUnitaryFormula
forall a.
(RewriteFuns a, a) -> THFUnitaryFormula -> Result THFUnitaryFormula
rewriteUnitaryFormula',
 rewriteBinaryPair :: (RewriteFuns a, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result THFBinaryFormula
rewriteBinaryPair = (RewriteFuns a, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result THFBinaryFormula
forall a.
(RewriteFuns a, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result THFBinaryFormula
rewriteBinaryPair',
 rewriteBinaryTuple :: (RewriteFuns a, a) -> THFBinaryTuple -> Result THFBinaryTuple
rewriteBinaryTuple = (RewriteFuns a, a) -> THFBinaryTuple -> Result THFBinaryTuple
forall a.
(RewriteFuns a, a) -> THFBinaryTuple -> Result THFBinaryTuple
rewriteBinaryTuple',
 rewriteQuantifiedFormula :: (RewriteFuns a, a)
-> THFQuantifiedFormula -> Result THFQuantifiedFormula
rewriteQuantifiedFormula = (RewriteFuns a, a)
-> THFQuantifiedFormula -> Result THFQuantifiedFormula
forall a.
(RewriteFuns a, a)
-> THFQuantifiedFormula -> Result THFQuantifiedFormula
rewriteQuantifiedFormula',
 rewriteAtom :: (RewriteFuns a, a) -> THFAtom -> Result THFUnitaryFormula
rewriteAtom = (RewriteFuns a, a) -> THFAtom -> Result THFUnitaryFormula
forall a. (RewriteFuns a, a) -> THFAtom -> Result THFUnitaryFormula
rewriteAtom',
 rewriteVariableList :: (RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
rewriteVariableList = (RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
forall a.
(RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
rewriteVariableList',
 rewriteConst :: (RewriteFuns a, a) -> AtomicWord -> Result THFUnitaryFormula
rewriteConst = (RewriteFuns a, a) -> AtomicWord -> Result THFUnitaryFormula
forall a.
(RewriteFuns a, a) -> AtomicWord -> Result THFUnitaryFormula
rewriteConst',
 rewriteConnTerm :: (RewriteFuns a, a) -> THFConnTerm -> Result THFConnTerm
rewriteConnTerm = (RewriteFuns a, a) -> THFConnTerm -> Result THFConnTerm
forall a. (RewriteFuns a, a) -> THFConnTerm -> Result THFConnTerm
rewriteConnTerm' }

rewriteSenFun :: (RewriteFuns a, a) -> Named THFFormula
               -> Result (Named THFFormula)
rewriteSenFun :: (RewriteFuns a, a) -> Named THFFormula -> Result (Named THFFormula)
rewriteSenFun (fns :: RewriteFuns a
fns, d :: a
d) sen :: Named THFFormula
sen = do
 THFFormula
sen' <- case Named THFFormula -> THFFormula
forall s a. SenAttr s a -> s
sentence Named THFFormula
sen of
             TF_THF_Logic_Formula lf :: THFLogicFormula
lf ->
              (THFLogicFormula -> THFFormula)
-> Result THFLogicFormula -> Result THFFormula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM THFLogicFormula -> THFFormula
TF_THF_Logic_Formula (RewriteFuns a
-> (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
rewriteLogicFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFLogicFormula
lf)
             T0F_THF_Typed_Const tc :: THFTypedConst
tc ->
              String -> THFTypedConst -> Result THFFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.rewriteSen: Typed constants are not in THF0! "
               THFTypedConst
tc
             TF_THF_Sequent s :: THFSequent
s ->
              String -> THFSequent -> Result THFFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.rewriteSen: Sequents are not in THF0!" THFSequent
s
 Named THFFormula -> Result (Named THFFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named THFFormula -> Result (Named THFFormula))
-> Named THFFormula -> Result (Named THFFormula)
forall a b. (a -> b) -> a -> b
$ Named THFFormula
sen { sentence :: THFFormula
sentence = THFFormula
sen' }

rewriteLogicFormula' :: (RewriteFuns a, a) -> THFLogicFormula
                        -> Result THFLogicFormula
rewriteLogicFormula' :: (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
rewriteLogicFormula' (fns :: RewriteFuns a
fns, d :: a
d) lf :: THFLogicFormula
lf = case THFLogicFormula
lf of
 TLF_THF_Binary_Formula bf :: THFBinaryFormula
bf -> (THFBinaryFormula -> THFLogicFormula)
-> Result THFBinaryFormula -> Result THFLogicFormula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM THFBinaryFormula -> THFLogicFormula
TLF_THF_Binary_Formula (Result THFBinaryFormula -> Result THFLogicFormula)
-> Result THFBinaryFormula -> Result THFLogicFormula
forall a b. (a -> b) -> a -> b
$
  RewriteFuns a
-> (RewriteFuns a, a)
-> THFBinaryFormula
-> Result THFBinaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFBinaryFormula
-> Result THFBinaryFormula
rewriteBinaryFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFBinaryFormula
bf
 TLF_THF_Unitary_Formula uf :: THFUnitaryFormula
uf -> (THFUnitaryFormula -> THFLogicFormula)
-> Result THFUnitaryFormula -> Result THFLogicFormula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM THFUnitaryFormula -> THFLogicFormula
TLF_THF_Unitary_Formula (Result THFUnitaryFormula -> Result THFLogicFormula)
-> Result THFUnitaryFormula -> Result THFLogicFormula
forall a b. (a -> b) -> a -> b
$
  RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFUnitaryFormula
uf
 TLF_THF_Type_Formula _ ->
  String -> THFLogicFormula -> Result THFLogicFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.rewriteLogicFormula: Type Formula not in THF0!" THFLogicFormula
lf
 TLF_THF_Sub_Type _ ->
  String -> THFLogicFormula -> Result THFLogicFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.rewriteLogicFormula: Sub Type Formula not in THF0!" THFLogicFormula
lf

rewriteBinaryFormula' :: (RewriteFuns a, a) -> THFBinaryFormula
                          -> Result THFBinaryFormula
rewriteBinaryFormula' :: (RewriteFuns a, a) -> THFBinaryFormula -> Result THFBinaryFormula
rewriteBinaryFormula' (fns :: RewriteFuns a
fns, d :: a
d) bf :: THFBinaryFormula
bf = case THFBinaryFormula
bf of
 TBF_THF_Binary_Type _ -> String -> THFBinaryFormula -> Result THFBinaryFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError
  "THF.Utils.rewriteBinaryFormula: Binary Type not in THF0!" THFBinaryFormula
bf
 TBF_THF_Binary_Pair uf1 :: THFUnitaryFormula
uf1 cn :: THFPairConnective
cn uf2 :: THFUnitaryFormula
uf2 ->
  RewriteFuns a
-> (RewriteFuns a, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result THFBinaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result THFBinaryFormula
rewriteBinaryPair RewriteFuns a
fns (RewriteFuns a
fns, a
d) (THFUnitaryFormula
uf1, THFPairConnective
cn, THFUnitaryFormula
uf2)
 TBF_THF_Binary_Tuple bt :: THFBinaryTuple
bt -> (THFBinaryTuple -> THFBinaryFormula)
-> Result THFBinaryTuple -> Result THFBinaryFormula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM THFBinaryTuple -> THFBinaryFormula
TBF_THF_Binary_Tuple (Result THFBinaryTuple -> Result THFBinaryFormula)
-> Result THFBinaryTuple -> Result THFBinaryFormula
forall a b. (a -> b) -> a -> b
$
  RewriteFuns a
-> (RewriteFuns a, a) -> THFBinaryTuple -> Result THFBinaryTuple
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> THFBinaryTuple -> Result THFBinaryTuple
rewriteBinaryTuple RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFBinaryTuple
bt

rewriteBinaryPair' :: (RewriteFuns a, a) -> (THFUnitaryFormula,
                       THFPairConnective, THFUnitaryFormula)
                       -> Result THFBinaryFormula
rewriteBinaryPair' :: (RewriteFuns a, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result THFBinaryFormula
rewriteBinaryPair' (fns :: RewriteFuns a
fns, d :: a
d) (uf1 :: THFUnitaryFormula
uf1, cn :: THFPairConnective
cn, uf2 :: THFUnitaryFormula
uf2) = do
 THFUnitaryFormula
uf1' <- RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFUnitaryFormula
uf1
 THFUnitaryFormula
uf2' <- RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFUnitaryFormula
uf2
 THFBinaryFormula -> Result THFBinaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFBinaryFormula -> Result THFBinaryFormula)
-> THFBinaryFormula -> Result THFBinaryFormula
forall a b. (a -> b) -> a -> b
$ THFUnitaryFormula
-> THFPairConnective -> THFUnitaryFormula -> THFBinaryFormula
TBF_THF_Binary_Pair THFUnitaryFormula
uf1' THFPairConnective
cn THFUnitaryFormula
uf2'

rewriteBinaryTuple' :: (RewriteFuns a, a) -> THFBinaryTuple
                        -> Result THFBinaryTuple
rewriteBinaryTuple' :: (RewriteFuns a, a) -> THFBinaryTuple -> Result THFBinaryTuple
rewriteBinaryTuple' (fns :: RewriteFuns a
fns, d :: a
d) bt :: THFBinaryTuple
bt = case THFBinaryTuple
bt of
 TBT_THF_Or_Formula ufs :: [THFUnitaryFormula]
ufs -> ([THFUnitaryFormula] -> THFBinaryTuple)
-> Result [THFUnitaryFormula] -> Result THFBinaryTuple
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [THFUnitaryFormula] -> THFBinaryTuple
TBT_THF_Or_Formula (Result [THFUnitaryFormula] -> Result THFBinaryTuple)
-> Result [THFUnitaryFormula] -> Result THFBinaryTuple
forall a b. (a -> b) -> a -> b
$
  (THFUnitaryFormula -> Result THFUnitaryFormula)
-> [THFUnitaryFormula] -> Result [THFUnitaryFormula]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d)) [THFUnitaryFormula]
ufs
 TBT_THF_And_Formula ufs :: [THFUnitaryFormula]
ufs -> ([THFUnitaryFormula] -> THFBinaryTuple)
-> Result [THFUnitaryFormula] -> Result THFBinaryTuple
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [THFUnitaryFormula] -> THFBinaryTuple
TBT_THF_And_Formula (Result [THFUnitaryFormula] -> Result THFBinaryTuple)
-> Result [THFUnitaryFormula] -> Result THFBinaryTuple
forall a b. (a -> b) -> a -> b
$
  (THFUnitaryFormula -> Result THFUnitaryFormula)
-> [THFUnitaryFormula] -> Result [THFUnitaryFormula]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d)) [THFUnitaryFormula]
ufs
 TBT_THF_Apply_Formula ufs :: [THFUnitaryFormula]
ufs -> ([THFUnitaryFormula] -> THFBinaryTuple)
-> Result [THFUnitaryFormula] -> Result THFBinaryTuple
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [THFUnitaryFormula] -> THFBinaryTuple
TBT_THF_Apply_Formula (Result [THFUnitaryFormula] -> Result THFBinaryTuple)
-> Result [THFUnitaryFormula] -> Result THFBinaryTuple
forall a b. (a -> b) -> a -> b
$
  (THFUnitaryFormula -> Result THFUnitaryFormula)
-> [THFUnitaryFormula] -> Result [THFUnitaryFormula]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d)) [THFUnitaryFormula]
ufs

rewriteUnitaryFormula' :: (RewriteFuns a, a) -> THFUnitaryFormula
                           -> Result THFUnitaryFormula
rewriteUnitaryFormula' :: (RewriteFuns a, a) -> THFUnitaryFormula -> Result THFUnitaryFormula
rewriteUnitaryFormula' (fns :: RewriteFuns a
fns, d :: a
d) uf :: THFUnitaryFormula
uf = case THFUnitaryFormula
uf of
 TUF_THF_Conditional {} ->
  String -> THFUnitaryFormula -> Result THFUnitaryFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError ("THF.Utils.rewriteUnitaryFOrmula: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
           "Conditional not in THF0!") THFUnitaryFormula
uf
 TUF_THF_Quantified_Formula qf :: THFQuantifiedFormula
qf -> (THFQuantifiedFormula -> THFUnitaryFormula)
-> Result THFQuantifiedFormula -> Result THFUnitaryFormula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM THFQuantifiedFormula -> THFUnitaryFormula
TUF_THF_Quantified_Formula (Result THFQuantifiedFormula -> Result THFUnitaryFormula)
-> Result THFQuantifiedFormula -> Result THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$
  RewriteFuns a
-> (RewriteFuns a, a)
-> THFQuantifiedFormula
-> Result THFQuantifiedFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFQuantifiedFormula
-> Result THFQuantifiedFormula
rewriteQuantifiedFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFQuantifiedFormula
qf
 TUF_THF_Unary_Formula c :: THFUnaryConnective
c lf :: THFLogicFormula
lf -> (THFLogicFormula -> THFUnitaryFormula)
-> Result THFLogicFormula -> Result THFUnitaryFormula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (THFUnaryConnective -> THFLogicFormula -> THFUnitaryFormula
TUF_THF_Unary_Formula THFUnaryConnective
c) (Result THFLogicFormula -> Result THFUnitaryFormula)
-> Result THFLogicFormula -> Result THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$
  RewriteFuns a
-> (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
rewriteLogicFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFLogicFormula
lf
 TUF_THF_Atom a :: THFAtom
a -> RewriteFuns a
-> (RewriteFuns a, a) -> THFAtom -> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> THFAtom -> Result THFUnitaryFormula
rewriteAtom RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFAtom
a
 TUF_THF_Tuple t :: THFTuple
t -> (THFTuple -> THFUnitaryFormula)
-> Result THFTuple -> Result THFUnitaryFormula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM THFTuple -> THFUnitaryFormula
TUF_THF_Tuple (Result THFTuple -> Result THFUnitaryFormula)
-> Result THFTuple -> Result THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$
  (THFLogicFormula -> Result THFLogicFormula)
-> THFTuple -> Result THFTuple
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (RewriteFuns a
-> (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
rewriteLogicFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d)) THFTuple
t
 TUF_THF_Logic_Formula_Par lf :: THFLogicFormula
lf -> (THFLogicFormula -> THFUnitaryFormula)
-> Result THFLogicFormula -> Result THFUnitaryFormula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM THFLogicFormula -> THFUnitaryFormula
TUF_THF_Logic_Formula_Par (Result THFLogicFormula -> Result THFUnitaryFormula)
-> Result THFLogicFormula -> Result THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$
  RewriteFuns a
-> (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
rewriteLogicFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFLogicFormula
lf
 T0UF_THF_Abstraction vs :: [THFVariable]
vs uf' :: THFUnitaryFormula
uf' -> do
  [THFVariable]
vs' <- RewriteFuns a
-> (RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
rewriteVariableList RewriteFuns a
fns (RewriteFuns a
fns, a
d) [THFVariable]
vs
  THFUnitaryFormula
uf'' <- RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFUnitaryFormula
uf'
  THFUnitaryFormula -> Result THFUnitaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> Result THFUnitaryFormula)
-> THFUnitaryFormula -> Result THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ [THFVariable] -> THFUnitaryFormula -> THFUnitaryFormula
T0UF_THF_Abstraction [THFVariable]
vs' THFUnitaryFormula
uf''

rewriteQuantifiedFormula' :: (RewriteFuns a, a) -> THFQuantifiedFormula
                             -> Result THFQuantifiedFormula
rewriteQuantifiedFormula' :: (RewriteFuns a, a)
-> THFQuantifiedFormula -> Result THFQuantifiedFormula
rewriteQuantifiedFormula' (fns :: RewriteFuns a
fns, d :: a
d) qf :: THFQuantifiedFormula
qf = case THFQuantifiedFormula
qf of
 TQF_THF_Quantified_Formula q :: THFQuantifier
q vs :: [THFVariable]
vs uf :: THFUnitaryFormula
uf -> do
  [THFVariable]
vs' <- RewriteFuns a
-> (RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
rewriteVariableList RewriteFuns a
fns (RewriteFuns a
fns, a
d) [THFVariable]
vs
  THFUnitaryFormula
uf' <- RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFUnitaryFormula
uf
  THFQuantifiedFormula -> Result THFQuantifiedFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFQuantifiedFormula -> Result THFQuantifiedFormula)
-> THFQuantifiedFormula -> Result THFQuantifiedFormula
forall a b. (a -> b) -> a -> b
$ THFQuantifier
-> [THFVariable] -> THFUnitaryFormula -> THFQuantifiedFormula
TQF_THF_Quantified_Formula THFQuantifier
q [THFVariable]
vs' THFUnitaryFormula
uf'
 T0QF_THF_Quantified_Var q :: Quantifier
q vs :: [THFVariable]
vs uf :: THFUnitaryFormula
uf -> do
  [THFVariable]
vs' <- RewriteFuns a
-> (RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
rewriteVariableList RewriteFuns a
fns (RewriteFuns a
fns, a
d) [THFVariable]
vs
  THFUnitaryFormula
uf' <- RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFUnitaryFormula
uf
  THFQuantifiedFormula -> Result THFQuantifiedFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFQuantifiedFormula -> Result THFQuantifiedFormula)
-> THFQuantifiedFormula -> Result THFQuantifiedFormula
forall a b. (a -> b) -> a -> b
$ Quantifier
-> [THFVariable] -> THFUnitaryFormula -> THFQuantifiedFormula
T0QF_THF_Quantified_Var Quantifier
q [THFVariable]
vs' THFUnitaryFormula
uf'
 T0QF_THF_Quantified_Novar _ _ ->
  String -> THFQuantifiedFormula -> Result THFQuantifiedFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.rewriteQuantifiedFormula: Quantified Novar not in THF0!" THFQuantifiedFormula
qf

rewriteVariableList' :: (RewriteFuns a, a) -> [THFVariable]
                         -> Result [THFVariable]
rewriteVariableList' :: (RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
rewriteVariableList' _ = [THFVariable] -> Result [THFVariable]
forall (m :: * -> *) a. Monad m => a -> m a
return

rewriteAtom' :: (RewriteFuns a, a) -> THFAtom -> Result THFUnitaryFormula
rewriteAtom' :: (RewriteFuns a, a) -> THFAtom -> Result THFUnitaryFormula
rewriteAtom' (fns :: RewriteFuns a
fns, d :: a
d) a :: THFAtom
a = case THFAtom
a of
 TA_Term _ -> String -> THFAtom -> Result THFUnitaryFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.rewriteAtom: Term not in THF0!" THFAtom
a
 TA_THF_Conn_Term c :: THFConnTerm
c -> (THFConnTerm -> THFUnitaryFormula)
-> Result THFConnTerm -> Result THFUnitaryFormula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (THFAtom -> THFUnitaryFormula
TUF_THF_Atom (THFAtom -> THFUnitaryFormula)
-> (THFConnTerm -> THFAtom) -> THFConnTerm -> THFUnitaryFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFConnTerm -> THFAtom
TA_THF_Conn_Term) (Result THFConnTerm -> Result THFUnitaryFormula)
-> Result THFConnTerm -> Result THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$
  RewriteFuns a
-> (RewriteFuns a, a) -> THFConnTerm -> Result THFConnTerm
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> THFConnTerm -> Result THFConnTerm
rewriteConnTerm RewriteFuns a
fns (RewriteFuns a
fns, a
d) THFConnTerm
c
 TA_Defined_Type _ ->
  String -> THFAtom -> Result THFUnitaryFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.rewriteAtom: Defined Type not in THF0!" THFAtom
a
 TA_Defined_Plain_Formula _ ->
  String -> THFAtom -> Result THFUnitaryFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.rewriteAtom: Defined Plain Formula not in THF0!" THFAtom
a
 TA_System_Type _ ->
  String -> THFAtom -> Result THFUnitaryFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.rewriteAtom: System Type not in THF0!" THFAtom
a
 TA_System_Atomic_Formula _ ->
  String -> THFAtom -> Result THFUnitaryFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.rewriteAtom: System Atomic Formula not in THF0!" THFAtom
a
 T0A_Constant c :: AtomicWord
c -> RewriteFuns a
-> (RewriteFuns a, a) -> AtomicWord -> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> AtomicWord -> Result THFUnitaryFormula
rewriteConst RewriteFuns a
fns (RewriteFuns a
fns, a
d) AtomicWord
c
 T0A_Defined_Constant _ -> THFUnitaryFormula -> Result THFUnitaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> Result THFUnitaryFormula)
-> THFUnitaryFormula -> Result THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ THFAtom -> THFUnitaryFormula
TUF_THF_Atom THFAtom
a
 T0A_System_Constant _ -> THFUnitaryFormula -> Result THFUnitaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> Result THFUnitaryFormula)
-> THFUnitaryFormula -> Result THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ THFAtom -> THFUnitaryFormula
TUF_THF_Atom THFAtom
a
 T0A_Variable v :: Token
v -> do
  [THFVariable]
v' <- RewriteFuns a
-> (RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> [THFVariable] -> Result [THFVariable]
rewriteVariableList RewriteFuns a
fns (RewriteFuns a
fns, a
d) [Token -> THFVariable
TV_Variable Token
v]
  case [THFVariable]
v' of
   TV_Variable t :: Token
t : _ -> THFUnitaryFormula -> Result THFUnitaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> Result THFUnitaryFormula)
-> THFUnitaryFormula -> Result THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ THFAtom -> THFUnitaryFormula
TUF_THF_Atom (THFAtom -> THFUnitaryFormula) -> THFAtom -> THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ Token -> THFAtom
T0A_Variable Token
t
   _ -> String -> Token -> Result THFUnitaryFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.rewriteAtom: Invalid rewrite!" Token
v

rewriteConst' :: (RewriteFuns a, a) -> Constant -> Result THFUnitaryFormula
rewriteConst' :: (RewriteFuns a, a) -> AtomicWord -> Result THFUnitaryFormula
rewriteConst' _ = THFUnitaryFormula -> Result THFUnitaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> Result THFUnitaryFormula)
-> (AtomicWord -> THFUnitaryFormula)
-> AtomicWord
-> Result THFUnitaryFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFAtom -> THFUnitaryFormula
TUF_THF_Atom (THFAtom -> THFUnitaryFormula)
-> (AtomicWord -> THFAtom) -> AtomicWord -> THFUnitaryFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtomicWord -> THFAtom
T0A_Constant

rewriteConnTerm' :: (RewriteFuns a, a) -> THFConnTerm -> Result THFConnTerm
rewriteConnTerm' :: (RewriteFuns a, a) -> THFConnTerm -> Result THFConnTerm
rewriteConnTerm' _ c :: THFConnTerm
c = THFConnTerm -> Result THFConnTerm
forall (m :: * -> *) a. Monad m => a -> m a
return THFConnTerm
c

data AnaFuns a b = AnaFuns {
 AnaFuns a b -> (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
anaLogicFormula :: (AnaFuns a b, a) -> THFLogicFormula -> Result [b],
 AnaFuns a b -> (AnaFuns a b, a) -> THFBinaryFormula -> Result [b]
anaBinaryFormula :: (AnaFuns a b, a) -> THFBinaryFormula -> Result [b],
 AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula :: (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b],
 AnaFuns a b
-> (AnaFuns a b, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result [b]
anaBinaryPair :: (AnaFuns a b, a) -> (THFUnitaryFormula,
                       THFPairConnective, THFUnitaryFormula) -> Result [b],
 AnaFuns a b -> (AnaFuns a b, a) -> THFBinaryTuple -> Result [b]
anaBinaryTuple :: (AnaFuns a b, a) -> THFBinaryTuple -> Result [b],
 AnaFuns a b
-> (AnaFuns a b, a) -> THFQuantifiedFormula -> Result [b]
anaQuantifiedFormula :: (AnaFuns a b, a) -> THFQuantifiedFormula -> Result [b],
 AnaFuns a b -> (AnaFuns a b, a) -> THFAtom -> Result [b]
anaAtom :: (AnaFuns a b, a) -> THFAtom -> Result [b],
 AnaFuns a b -> (AnaFuns a b, a) -> [THFVariable] -> Result [b]
anaVariableList :: (AnaFuns a b, a) -> [THFVariable] -> Result [b],
 AnaFuns a b -> (AnaFuns a b, a) -> AtomicWord -> Result [b]
anaConst :: (AnaFuns a b, a) -> Constant -> Result [b],
 AnaFuns a b -> (AnaFuns a b, a) -> THFConnTerm -> Result [b]
anaConnTerm :: (AnaFuns a b, a) -> THFConnTerm -> Result [b] }

anaTHF0 :: AnaFuns a b
anaTHF0 :: AnaFuns a b
anaTHF0 = AnaFuns :: forall a b.
((AnaFuns a b, a) -> THFLogicFormula -> Result [b])
-> ((AnaFuns a b, a) -> THFBinaryFormula -> Result [b])
-> ((AnaFuns a b, a) -> THFUnitaryFormula -> Result [b])
-> ((AnaFuns a b, a)
    -> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
    -> Result [b])
-> ((AnaFuns a b, a) -> THFBinaryTuple -> Result [b])
-> ((AnaFuns a b, a) -> THFQuantifiedFormula -> Result [b])
-> ((AnaFuns a b, a) -> THFAtom -> Result [b])
-> ((AnaFuns a b, a) -> [THFVariable] -> Result [b])
-> ((AnaFuns a b, a) -> AtomicWord -> Result [b])
-> ((AnaFuns a b, a) -> THFConnTerm -> Result [b])
-> AnaFuns a b
AnaFuns {
 anaLogicFormula :: (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
anaLogicFormula = (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
forall a b. (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
anaLogicFormula',
 anaBinaryFormula :: (AnaFuns a b, a) -> THFBinaryFormula -> Result [b]
anaBinaryFormula = (AnaFuns a b, a) -> THFBinaryFormula -> Result [b]
forall a b. (AnaFuns a b, a) -> THFBinaryFormula -> Result [b]
anaBinaryFormula',
 anaUnitaryFormula :: (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula = (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
forall a b. (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula',
 anaBinaryPair :: (AnaFuns a b, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result [b]
anaBinaryPair = (AnaFuns a b, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result [b]
forall a b.
(AnaFuns a b, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result [b]
anaBinaryPair',
 anaBinaryTuple :: (AnaFuns a b, a) -> THFBinaryTuple -> Result [b]
anaBinaryTuple = (AnaFuns a b, a) -> THFBinaryTuple -> Result [b]
forall a b. (AnaFuns a b, a) -> THFBinaryTuple -> Result [b]
anaBinaryTuple',
 anaQuantifiedFormula :: (AnaFuns a b, a) -> THFQuantifiedFormula -> Result [b]
anaQuantifiedFormula = (AnaFuns a b, a) -> THFQuantifiedFormula -> Result [b]
forall a b. (AnaFuns a b, a) -> THFQuantifiedFormula -> Result [b]
anaQuantifiedFormula',
 anaAtom :: (AnaFuns a b, a) -> THFAtom -> Result [b]
anaAtom = (AnaFuns a b, a) -> THFAtom -> Result [b]
forall a b. (AnaFuns a b, a) -> THFAtom -> Result [b]
anaAtom',
 anaVariableList :: (AnaFuns a b, a) -> [THFVariable] -> Result [b]
anaVariableList = (AnaFuns a b, a) -> [THFVariable] -> Result [b]
forall a b. (AnaFuns a b, a) -> [THFVariable] -> Result [b]
anaVariableList',
 anaConst :: (AnaFuns a b, a) -> AtomicWord -> Result [b]
anaConst = (AnaFuns a b, a) -> AtomicWord -> Result [b]
forall a b. (AnaFuns a b, a) -> AtomicWord -> Result [b]
anaConst',
 anaConnTerm :: (AnaFuns a b, a) -> THFConnTerm -> Result [b]
anaConnTerm = (AnaFuns a b, a) -> THFConnTerm -> Result [b]
forall a b. (AnaFuns a b, a) -> THFConnTerm -> Result [b]
anaConnTerm' }

anaSenFun :: (AnaFuns a b, a) -> Named THFFormula -> Result [b]
anaSenFun :: (AnaFuns a b, a) -> Named THFFormula -> Result [b]
anaSenFun (fns :: AnaFuns a b
fns, d :: a
d) sen :: Named THFFormula
sen = case Named THFFormula -> THFFormula
forall s a. SenAttr s a -> s
sentence Named THFFormula
sen of
 TF_THF_Logic_Formula lf :: THFLogicFormula
lf -> AnaFuns a b -> (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
anaLogicFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFLogicFormula
lf
 T0F_THF_Typed_Const tc :: THFTypedConst
tc ->
  String -> THFTypedConst -> Result [b]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.anaSen: Typed constants are not in THF0! " THFTypedConst
tc
 TF_THF_Sequent s :: THFSequent
s ->
  String -> THFSequent -> Result [b]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.anaSen: Sequents are not in THF0!" THFSequent
s

anaLogicFormula' :: (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
anaLogicFormula' :: (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
anaLogicFormula' (fns :: AnaFuns a b
fns, d :: a
d) lf :: THFLogicFormula
lf = case THFLogicFormula
lf of
 TLF_THF_Binary_Formula bf :: THFBinaryFormula
bf -> AnaFuns a b -> (AnaFuns a b, a) -> THFBinaryFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFBinaryFormula -> Result [b]
anaBinaryFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFBinaryFormula
bf
 TLF_THF_Unitary_Formula uf :: THFUnitaryFormula
uf -> AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFUnitaryFormula
uf
 TLF_THF_Type_Formula _ ->
  String -> THFLogicFormula -> Result [b]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.anaLogicFormula: Type Formula not in THF0!" THFLogicFormula
lf
 TLF_THF_Sub_Type _ ->
  String -> THFLogicFormula -> Result [b]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.anaLogicFormula: Sub Type Formula not in THF0!" THFLogicFormula
lf

anaBinaryFormula' :: (AnaFuns a b, a) -> THFBinaryFormula -> Result [b]
anaBinaryFormula' :: (AnaFuns a b, a) -> THFBinaryFormula -> Result [b]
anaBinaryFormula' (fns :: AnaFuns a b
fns, d :: a
d) bf :: THFBinaryFormula
bf = case THFBinaryFormula
bf of
 TBF_THF_Binary_Type _ -> String -> THFBinaryFormula -> Result [b]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError
  "THF.Utils.anaBinaryFormula: Binary Type not in THF0!" THFBinaryFormula
bf
 TBF_THF_Binary_Pair uf1 :: THFUnitaryFormula
uf1 cn :: THFPairConnective
cn uf2 :: THFUnitaryFormula
uf2 ->
  AnaFuns a b
-> (AnaFuns a b, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result [b]
forall a b.
AnaFuns a b
-> (AnaFuns a b, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result [b]
anaBinaryPair AnaFuns a b
fns (AnaFuns a b
fns, a
d) (THFUnitaryFormula
uf1, THFPairConnective
cn, THFUnitaryFormula
uf2)
 TBF_THF_Binary_Tuple bt :: THFBinaryTuple
bt -> AnaFuns a b -> (AnaFuns a b, a) -> THFBinaryTuple -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFBinaryTuple -> Result [b]
anaBinaryTuple AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFBinaryTuple
bt

anaBinaryPair' :: (AnaFuns a b, a) -> (THFUnitaryFormula,
                       THFPairConnective, THFUnitaryFormula)
                       -> Result [b]
anaBinaryPair' :: (AnaFuns a b, a)
-> (THFUnitaryFormula, THFPairConnective, THFUnitaryFormula)
-> Result [b]
anaBinaryPair' (fns :: AnaFuns a b
fns, d :: a
d) (uf1 :: THFUnitaryFormula
uf1, _, uf2 :: THFUnitaryFormula
uf2) = do
 [b]
l1 <- AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFUnitaryFormula
uf1
 [b]
l2 <- AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFUnitaryFormula
uf2
 [b] -> Result [b]
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> Result [b]) -> [b] -> Result [b]
forall a b. (a -> b) -> a -> b
$ [b]
l1 [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [b]
l2

anaBinaryTuple' :: (AnaFuns a b, a) -> THFBinaryTuple -> Result [b]
anaBinaryTuple' :: (AnaFuns a b, a) -> THFBinaryTuple -> Result [b]
anaBinaryTuple' (fns :: AnaFuns a b
fns, d :: a
d) bt :: THFBinaryTuple
bt = case THFBinaryTuple
bt of
 TBT_THF_Or_Formula ufs :: [THFUnitaryFormula]
ufs -> do
  [[b]]
r <- (THFUnitaryFormula -> Result [b])
-> [THFUnitaryFormula] -> Result [[b]]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d)) [THFUnitaryFormula]
ufs
  [b] -> Result [b]
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> Result [b]) -> [b] -> Result [b]
forall a b. (a -> b) -> a -> b
$ [[b]] -> [b]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[b]]
r
 TBT_THF_And_Formula ufs :: [THFUnitaryFormula]
ufs -> do
  [[b]]
r <- (THFUnitaryFormula -> Result [b])
-> [THFUnitaryFormula] -> Result [[b]]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d)) [THFUnitaryFormula]
ufs
  [b] -> Result [b]
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> Result [b]) -> [b] -> Result [b]
forall a b. (a -> b) -> a -> b
$ [[b]] -> [b]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[b]]
r
 TBT_THF_Apply_Formula ufs :: [THFUnitaryFormula]
ufs -> do
  [[b]]
r <- (THFUnitaryFormula -> Result [b])
-> [THFUnitaryFormula] -> Result [[b]]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d)) [THFUnitaryFormula]
ufs
  [b] -> Result [b]
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> Result [b]) -> [b] -> Result [b]
forall a b. (a -> b) -> a -> b
$ [[b]] -> [b]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[b]]
r

anaUnitaryFormula' :: (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula' :: (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula' (fns :: AnaFuns a b
fns, d :: a
d) uf :: THFUnitaryFormula
uf = case THFUnitaryFormula
uf of
 TUF_THF_Conditional {} ->
  String -> THFUnitaryFormula -> Result [b]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError ("THF.Utils.anaUnitaryFOrmula: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
           "Conditional not in THF0!") THFUnitaryFormula
uf
 TUF_THF_Quantified_Formula qf :: THFQuantifiedFormula
qf -> AnaFuns a b
-> (AnaFuns a b, a) -> THFQuantifiedFormula -> Result [b]
forall a b.
AnaFuns a b
-> (AnaFuns a b, a) -> THFQuantifiedFormula -> Result [b]
anaQuantifiedFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFQuantifiedFormula
qf
 TUF_THF_Unary_Formula _ lf :: THFLogicFormula
lf -> AnaFuns a b -> (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
anaLogicFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFLogicFormula
lf
 TUF_THF_Atom a :: THFAtom
a -> AnaFuns a b -> (AnaFuns a b, a) -> THFAtom -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFAtom -> Result [b]
anaAtom AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFAtom
a
 TUF_THF_Tuple t :: THFTuple
t -> do
  [[b]]
r <- (THFLogicFormula -> Result [b]) -> THFTuple -> Result [[b]]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (AnaFuns a b -> (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
anaLogicFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d)) THFTuple
t
  [b] -> Result [b]
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> Result [b]) -> [b] -> Result [b]
forall a b. (a -> b) -> a -> b
$ [[b]] -> [b]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[b]]
r
 TUF_THF_Logic_Formula_Par lf :: THFLogicFormula
lf -> AnaFuns a b -> (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFLogicFormula -> Result [b]
anaLogicFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFLogicFormula
lf
 T0UF_THF_Abstraction vs :: [THFVariable]
vs uf' :: THFUnitaryFormula
uf' -> do
  [b]
l1 <- AnaFuns a b -> (AnaFuns a b, a) -> [THFVariable] -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> [THFVariable] -> Result [b]
anaVariableList AnaFuns a b
fns (AnaFuns a b
fns, a
d) [THFVariable]
vs
  [b]
l2 <- AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFUnitaryFormula
uf'
  [b] -> Result [b]
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> Result [b]) -> [b] -> Result [b]
forall a b. (a -> b) -> a -> b
$ [b]
l1 [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [b]
l2

anaQuantifiedFormula' :: (AnaFuns a b, a) -> THFQuantifiedFormula
                             -> Result [b]
anaQuantifiedFormula' :: (AnaFuns a b, a) -> THFQuantifiedFormula -> Result [b]
anaQuantifiedFormula' (fns :: AnaFuns a b
fns, d :: a
d) qf :: THFQuantifiedFormula
qf = case THFQuantifiedFormula
qf of
 TQF_THF_Quantified_Formula _ vs :: [THFVariable]
vs uf :: THFUnitaryFormula
uf -> do
  [b]
l1 <- AnaFuns a b -> (AnaFuns a b, a) -> [THFVariable] -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> [THFVariable] -> Result [b]
anaVariableList AnaFuns a b
fns (AnaFuns a b
fns, a
d) [THFVariable]
vs
  [b]
l2 <- AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFUnitaryFormula
uf
  [b] -> Result [b]
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> Result [b]) -> [b] -> Result [b]
forall a b. (a -> b) -> a -> b
$ [b]
l1 [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [b]
l2
 T0QF_THF_Quantified_Var _ vs :: [THFVariable]
vs uf :: THFUnitaryFormula
uf -> do
  [b]
l1 <- AnaFuns a b -> (AnaFuns a b, a) -> [THFVariable] -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> [THFVariable] -> Result [b]
anaVariableList AnaFuns a b
fns (AnaFuns a b
fns, a
d) [THFVariable]
vs
  [b]
l2 <- AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFUnitaryFormula -> Result [b]
anaUnitaryFormula AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFUnitaryFormula
uf
  [b] -> Result [b]
forall (m :: * -> *) a. Monad m => a -> m a
return ([b] -> Result [b]) -> [b] -> Result [b]
forall a b. (a -> b) -> a -> b
$ [b]
l1 [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [b]
l2
 T0QF_THF_Quantified_Novar _ _ ->
  String -> THFQuantifiedFormula -> Result [b]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.anaQuantifiedFormula: Quantified Novar not in THF0!" THFQuantifiedFormula
qf

anaVariableList' :: (AnaFuns a b, a) -> [THFVariable] -> Result [b]
anaVariableList' :: (AnaFuns a b, a) -> [THFVariable] -> Result [b]
anaVariableList' _ _ = [b] -> Result [b]
forall (m :: * -> *) a. Monad m => a -> m a
return []

anaAtom' :: (AnaFuns a b, a) -> THFAtom -> Result [b]
anaAtom' :: (AnaFuns a b, a) -> THFAtom -> Result [b]
anaAtom' (fns :: AnaFuns a b
fns, d :: a
d) a :: THFAtom
a = case THFAtom
a of
 TA_Term _ -> String -> THFAtom -> Result [b]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.anaAtom: Term not in THF0!" THFAtom
a
 TA_THF_Conn_Term c :: THFConnTerm
c -> AnaFuns a b -> (AnaFuns a b, a) -> THFConnTerm -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> THFConnTerm -> Result [b]
anaConnTerm AnaFuns a b
fns (AnaFuns a b
fns, a
d) THFConnTerm
c
 TA_Defined_Type _ ->
  String -> THFAtom -> Result [b]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.anaAtom: Defined Type not in THF0!" THFAtom
a
 TA_Defined_Plain_Formula _ ->
  String -> THFAtom -> Result [b]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.anaAtom: Defined Plain Formula not in THF0!" THFAtom
a
 TA_System_Type _ ->
  String -> THFAtom -> Result [b]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.anaAtom: System Type not in THF0!" THFAtom
a
 TA_System_Atomic_Formula _ ->
  String -> THFAtom -> Result [b]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THF.Utils.anaAtom: System Atomic Formula not in THF0!" THFAtom
a
 T0A_Constant c :: AtomicWord
c -> AnaFuns a b -> (AnaFuns a b, a) -> AtomicWord -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> AtomicWord -> Result [b]
anaConst AnaFuns a b
fns (AnaFuns a b
fns, a
d) AtomicWord
c
 T0A_Defined_Constant _ -> [b] -> Result [b]
forall (m :: * -> *) a. Monad m => a -> m a
return []
 T0A_System_Constant _ -> [b] -> Result [b]
forall (m :: * -> *) a. Monad m => a -> m a
return []
 T0A_Variable v :: Token
v -> AnaFuns a b -> (AnaFuns a b, a) -> [THFVariable] -> Result [b]
forall a b.
AnaFuns a b -> (AnaFuns a b, a) -> [THFVariable] -> Result [b]
anaVariableList AnaFuns a b
fns (AnaFuns a b
fns, a
d) [Token -> THFVariable
TV_Variable Token
v]

anaConst' :: (AnaFuns a b, a) -> Constant -> Result [b]
anaConst' :: (AnaFuns a b, a) -> AtomicWord -> Result [b]
anaConst' _ _ = [b] -> Result [b]
forall (m :: * -> *) a. Monad m => a -> m a
return []

anaConnTerm' :: (AnaFuns a b, a) -> THFConnTerm -> Result [b]
anaConnTerm' :: (AnaFuns a b, a) -> THFConnTerm -> Result [b]
anaConnTerm' _ _ = [b] -> Result [b]
forall (m :: * -> *) a. Monad m => a -> m a
return []