Copyright	(c) A. Tsogias DFKI Bremen 2011
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Alexis.Tsogias@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	Safe

THF.As

Description

A Abstract Syntax for the TPTP-THF Input Syntax v5.1.0.2 taken from http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html In addition the Syntax for THF0 taken from http://www.ags.uni-sb.de/~chris/papers/C25.pdf P. 15-16 has been added where needed.

Documentation

data TPTP_THF Source #

Constructors

TPTP_THF_Annotated_Formula
Fields nameAF :: Name formulaRoleAF :: FormulaRole thfFormulaAF :: THFFormula annotationsAF :: Annotations
TPTP_Include Include
TPTP_Comment Comment
TPTP_Defined_Comment DefinedComment
TPTP_System_Comment SystemComment
TPTP_Header [Comment]

Instances

Instances details

Eq TPTP_THF Source #
Instance details Defined in THF.As Methods (==) :: TPTP_THF -> TPTP_THF -> Bool (/=) :: TPTP_THF -> TPTP_THF -> Bool
Data TPTP_THF Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TPTP_THF -> c TPTP_THF gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TPTP_THF toConstr :: TPTP_THF -> Constr dataTypeOf :: TPTP_THF -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TPTP_THF) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPTP_THF) gmapT :: (forall b. Data b => b -> b) -> TPTP_THF -> TPTP_THF gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPTP_THF -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPTP_THF -> r gmapQ :: (forall d. Data d => d -> u) -> TPTP_THF -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TPTP_THF -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TPTP_THF -> m TPTP_THF gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP_THF -> m TPTP_THF gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP_THF -> m TPTP_THF
Ord TPTP_THF Source #
Instance details Defined in THF.As Methods compare :: TPTP_THF -> TPTP_THF -> Ordering (<) :: TPTP_THF -> TPTP_THF -> Bool (<=) :: TPTP_THF -> TPTP_THF -> Bool (>) :: TPTP_THF -> TPTP_THF -> Bool (>=) :: TPTP_THF -> TPTP_THF -> Bool max :: TPTP_THF -> TPTP_THF -> TPTP_THF min :: TPTP_THF -> TPTP_THF -> TPTP_THF
Show TPTP_THF Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> TPTP_THF -> ShowS show :: TPTP_THF -> String showList :: [TPTP_THF] -> ShowS
Generic TPTP_THF
Instance details Defined in THF.ATC_THF Associated Types type Rep TPTP_THF :: Type -> Type Methods from :: TPTP_THF -> Rep TPTP_THF x to :: Rep TPTP_THF x -> TPTP_THF
GetRange TPTP_THF Source #
Instance details Defined in THF.As Methods getRange :: TPTP_THF -> Range Source # rangeSpan :: TPTP_THF -> [Pos] Source #
FromJSON TPTP_THF
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser TPTP_THF parseJSONList :: Value -> Parser [TPTP_THF]
ToJSON TPTP_THF
Instance details Defined in THF.ATC_THF Methods toJSON :: TPTP_THF -> Value toEncoding :: TPTP_THF -> Encoding toJSONList :: [TPTP_THF] -> Value toEncodingList :: [TPTP_THF] -> Encoding
ShATermConvertible TPTP_THF
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> TPTP_THF -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TPTP_THF] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TPTP_THF) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TPTP_THF])
Pretty TPTP_THF Source #
Instance details Defined in THF.PrintTHF Methods pretty :: TPTP_THF -> Doc Source # pretties :: [TPTP_THF] -> Doc Source #
type Rep TPTP_THF
Instance details Defined in THF.ATC_THF type Rep TPTP_THF = D1 ('MetaData "TPTP_THF" "THF.As" "main" 'False) ((C1 ('MetaCons "TPTP_THF_Annotated_Formula" 'PrefixI 'True) ((S1 ('MetaSel ('Just "nameAF") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Just "formulaRoleAF") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FormulaRole)) :: (S1 ('MetaSel ('Just "thfFormulaAF") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFFormula) :*: S1 ('MetaSel ('Just "annotationsAF") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Annotations))) :+: (C1 ('MetaCons "TPTP_Include" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Include)) :+: C1 ('MetaCons "TPTP_Comment" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Comment)))) :+: (C1 ('MetaCons "TPTP_Defined_Comment" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefinedComment)) :+: (C1 ('MetaCons "TPTP_System_Comment" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SystemComment)) :+: C1 ('MetaCons "TPTP_Header" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Comment])))))

data Comment Source #

Constructors

Comment_Line Token
Comment_Block Token

Instances

Instances details

Eq Comment Source #
Instance details Defined in THF.As Methods (==) :: Comment -> Comment -> Bool (/=) :: Comment -> Comment -> Bool
Data Comment Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Comment -> c Comment gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Comment toConstr :: Comment -> Constr dataTypeOf :: Comment -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Comment) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Comment) gmapT :: (forall b. Data b => b -> b) -> Comment -> Comment gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Comment -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Comment -> r gmapQ :: (forall d. Data d => d -> u) -> Comment -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Comment -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Comment -> m Comment gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Comment -> m Comment gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Comment -> m Comment
Ord Comment Source #
Instance details Defined in THF.As Methods compare :: Comment -> Comment -> Ordering (<) :: Comment -> Comment -> Bool (<=) :: Comment -> Comment -> Bool (>) :: Comment -> Comment -> Bool (>=) :: Comment -> Comment -> Bool max :: Comment -> Comment -> Comment min :: Comment -> Comment -> Comment
Show Comment Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> Comment -> ShowS show :: Comment -> String showList :: [Comment] -> ShowS
Generic Comment
Instance details Defined in THF.ATC_THF Associated Types type Rep Comment :: Type -> Type Methods from :: Comment -> Rep Comment x to :: Rep Comment x -> Comment
GetRange Comment Source #
Instance details Defined in THF.As Methods getRange :: Comment -> Range Source # rangeSpan :: Comment -> [Pos] Source #
FromJSON Comment
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser Comment parseJSONList :: Value -> Parser [Comment]
ToJSON Comment
Instance details Defined in THF.ATC_THF Methods toJSON :: Comment -> Value toEncoding :: Comment -> Encoding toJSONList :: [Comment] -> Value toEncodingList :: [Comment] -> Encoding
ShATermConvertible Comment
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> Comment -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Comment] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Comment) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Comment])
Pretty Comment Source #
Instance details Defined in THF.PrintTHF Methods pretty :: Comment -> Doc Source # pretties :: [Comment] -> Doc Source #
type Rep Comment
Instance details Defined in THF.ATC_THF type Rep Comment = D1 ('MetaData "Comment" "THF.As" "main" 'False) (C1 ('MetaCons "Comment_Line" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "Comment_Block" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data DefinedComment Source #

Constructors

Defined_Comment_Line Token
Defined_Comment_Block Token

Instances

Instances details

Eq DefinedComment Source #
Instance details Defined in THF.As Methods (==) :: DefinedComment -> DefinedComment -> Bool (/=) :: DefinedComment -> DefinedComment -> Bool
Data DefinedComment Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefinedComment -> c DefinedComment gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefinedComment toConstr :: DefinedComment -> Constr dataTypeOf :: DefinedComment -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefinedComment) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefinedComment) gmapT :: (forall b. Data b => b -> b) -> DefinedComment -> DefinedComment gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefinedComment -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefinedComment -> r gmapQ :: (forall d. Data d => d -> u) -> DefinedComment -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DefinedComment -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefinedComment -> m DefinedComment gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedComment -> m DefinedComment gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedComment -> m DefinedComment
Ord DefinedComment Source #
Instance details Defined in THF.As Methods compare :: DefinedComment -> DefinedComment -> Ordering (<) :: DefinedComment -> DefinedComment -> Bool (<=) :: DefinedComment -> DefinedComment -> Bool (>) :: DefinedComment -> DefinedComment -> Bool (>=) :: DefinedComment -> DefinedComment -> Bool max :: DefinedComment -> DefinedComment -> DefinedComment min :: DefinedComment -> DefinedComment -> DefinedComment
Show DefinedComment Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> DefinedComment -> ShowS show :: DefinedComment -> String showList :: [DefinedComment] -> ShowS
Generic DefinedComment
Instance details Defined in THF.ATC_THF Associated Types type Rep DefinedComment :: Type -> Type Methods from :: DefinedComment -> Rep DefinedComment x to :: Rep DefinedComment x -> DefinedComment
GetRange DefinedComment Source #
Instance details Defined in THF.As Methods getRange :: DefinedComment -> Range Source # rangeSpan :: DefinedComment -> [Pos] Source #
FromJSON DefinedComment
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser DefinedComment parseJSONList :: Value -> Parser [DefinedComment]
ToJSON DefinedComment
Instance details Defined in THF.ATC_THF Methods toJSON :: DefinedComment -> Value toEncoding :: DefinedComment -> Encoding toJSONList :: [DefinedComment] -> Value toEncodingList :: [DefinedComment] -> Encoding
ShATermConvertible DefinedComment
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> DefinedComment -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DefinedComment] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedComment) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DefinedComment])
Pretty DefinedComment Source #
Instance details Defined in THF.PrintTHF Methods pretty :: DefinedComment -> Doc Source # pretties :: [DefinedComment] -> Doc Source #
type Rep DefinedComment
Instance details Defined in THF.ATC_THF type Rep DefinedComment = D1 ('MetaData "DefinedComment" "THF.As" "main" 'False) (C1 ('MetaCons "Defined_Comment_Line" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "Defined_Comment_Block" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data SystemComment Source #

Constructors

System_Comment_Line Token
System_Comment_Block Token

Instances

Instances details

Eq SystemComment Source #
Instance details Defined in THF.As Methods (==) :: SystemComment -> SystemComment -> Bool (/=) :: SystemComment -> SystemComment -> Bool
Data SystemComment Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SystemComment -> c SystemComment gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SystemComment toConstr :: SystemComment -> Constr dataTypeOf :: SystemComment -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SystemComment) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SystemComment) gmapT :: (forall b. Data b => b -> b) -> SystemComment -> SystemComment gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SystemComment -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SystemComment -> r gmapQ :: (forall d. Data d => d -> u) -> SystemComment -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SystemComment -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SystemComment -> m SystemComment gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SystemComment -> m SystemComment gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SystemComment -> m SystemComment
Ord SystemComment Source #
Instance details Defined in THF.As Methods compare :: SystemComment -> SystemComment -> Ordering (<) :: SystemComment -> SystemComment -> Bool (<=) :: SystemComment -> SystemComment -> Bool (>) :: SystemComment -> SystemComment -> Bool (>=) :: SystemComment -> SystemComment -> Bool max :: SystemComment -> SystemComment -> SystemComment min :: SystemComment -> SystemComment -> SystemComment
Show SystemComment Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> SystemComment -> ShowS show :: SystemComment -> String showList :: [SystemComment] -> ShowS
Generic SystemComment
Instance details Defined in THF.ATC_THF Associated Types type Rep SystemComment :: Type -> Type Methods from :: SystemComment -> Rep SystemComment x to :: Rep SystemComment x -> SystemComment
GetRange SystemComment Source #
Instance details Defined in THF.As Methods getRange :: SystemComment -> Range Source # rangeSpan :: SystemComment -> [Pos] Source #
FromJSON SystemComment
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser SystemComment parseJSONList :: Value -> Parser [SystemComment]
ToJSON SystemComment
Instance details Defined in THF.ATC_THF Methods toJSON :: SystemComment -> Value toEncoding :: SystemComment -> Encoding toJSONList :: [SystemComment] -> Value toEncodingList :: [SystemComment] -> Encoding
ShATermConvertible SystemComment
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> SystemComment -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SystemComment] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SystemComment) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SystemComment])
Pretty SystemComment Source #
Instance details Defined in THF.PrintTHF Methods pretty :: SystemComment -> Doc Source # pretties :: [SystemComment] -> Doc Source #
type Rep SystemComment
Instance details Defined in THF.ATC_THF type Rep SystemComment = D1 ('MetaData "SystemComment" "THF.As" "main" 'False) (C1 ('MetaCons "System_Comment_Line" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "System_Comment_Block" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data Include Source #

Constructors

I_Include Token (Maybe NameList)

Instances

Instances details

Eq Include Source #
Instance details Defined in THF.As Methods (==) :: Include -> Include -> Bool (/=) :: Include -> Include -> Bool
Data Include Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Include -> c Include gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Include toConstr :: Include -> Constr dataTypeOf :: Include -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Include) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Include) gmapT :: (forall b. Data b => b -> b) -> Include -> Include gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Include -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Include -> r gmapQ :: (forall d. Data d => d -> u) -> Include -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Include -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Include -> m Include gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Include -> m Include gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Include -> m Include
Ord Include Source #
Instance details Defined in THF.As Methods compare :: Include -> Include -> Ordering (<) :: Include -> Include -> Bool (<=) :: Include -> Include -> Bool (>) :: Include -> Include -> Bool (>=) :: Include -> Include -> Bool max :: Include -> Include -> Include min :: Include -> Include -> Include
Show Include Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> Include -> ShowS show :: Include -> String showList :: [Include] -> ShowS
Generic Include
Instance details Defined in THF.ATC_THF Associated Types type Rep Include :: Type -> Type Methods from :: Include -> Rep Include x to :: Rep Include x -> Include
GetRange Include Source #
Instance details Defined in THF.As Methods getRange :: Include -> Range Source # rangeSpan :: Include -> [Pos] Source #
FromJSON Include
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser Include parseJSONList :: Value -> Parser [Include]
ToJSON Include
Instance details Defined in THF.ATC_THF Methods toJSON :: Include -> Value toEncoding :: Include -> Encoding toJSONList :: [Include] -> Value toEncodingList :: [Include] -> Encoding
ShATermConvertible Include
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> Include -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Include] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Include) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Include])
Pretty Include Source #
Instance details Defined in THF.PrintTHF Methods pretty :: Include -> Doc Source # pretties :: [Include] -> Doc Source #
type Rep Include
Instance details Defined in THF.ATC_THF type Rep Include = D1 ('MetaData "Include" "THF.As" "main" 'False) (C1 ('MetaCons "I_Include" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe NameList))))

data Annotations Source #

Constructors

Annotations Source OptionalInfo
Null

Instances

Instances details

Eq Annotations Source #
Instance details Defined in THF.As Methods (==) :: Annotations -> Annotations -> Bool (/=) :: Annotations -> Annotations -> Bool
Data Annotations Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annotations -> c Annotations gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Annotations toConstr :: Annotations -> Constr dataTypeOf :: Annotations -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Annotations) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annotations) gmapT :: (forall b. Data b => b -> b) -> Annotations -> Annotations gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annotations -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annotations -> r gmapQ :: (forall d. Data d => d -> u) -> Annotations -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Annotations -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annotations -> m Annotations
Ord Annotations Source #
Instance details Defined in THF.As Methods compare :: Annotations -> Annotations -> Ordering (<) :: Annotations -> Annotations -> Bool (<=) :: Annotations -> Annotations -> Bool (>) :: Annotations -> Annotations -> Bool (>=) :: Annotations -> Annotations -> Bool max :: Annotations -> Annotations -> Annotations min :: Annotations -> Annotations -> Annotations
Show Annotations Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> Annotations -> ShowS show :: Annotations -> String showList :: [Annotations] -> ShowS
Generic Annotations
Instance details Defined in THF.ATC_THF Associated Types type Rep Annotations :: Type -> Type Methods from :: Annotations -> Rep Annotations x to :: Rep Annotations x -> Annotations
GetRange Annotations Source #
Instance details Defined in THF.As Methods getRange :: Annotations -> Range Source # rangeSpan :: Annotations -> [Pos] Source #
FromJSON Annotations
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser Annotations parseJSONList :: Value -> Parser [Annotations]
ToJSON Annotations
Instance details Defined in THF.ATC_THF Methods toJSON :: Annotations -> Value toEncoding :: Annotations -> Encoding toJSONList :: [Annotations] -> Value toEncodingList :: [Annotations] -> Encoding
ShATermConvertible Annotations
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> Annotations -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Annotations] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Annotations) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Annotations])
Pretty Annotations Source #
Instance details Defined in THF.PrintTHF Methods pretty :: Annotations -> Doc Source # pretties :: [Annotations] -> Doc Source #
type Rep Annotations
Instance details Defined in THF.ATC_THF type Rep Annotations = D1 ('MetaData "Annotations" "THF.As" "main" 'False) (C1 ('MetaCons "Annotations" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Source) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OptionalInfo)) :+: C1 ('MetaCons "Null" 'PrefixI 'False) (U1 :: Type -> Type))

data FormulaRole Source #

Constructors

Axiom
Hypothesis
Definition
Assumption
Lemma
Theorem
Conjecture
Negated_Conjecture
Plain
Fi_Domain
Fi_Functors
Fi_Predicates
Type
Unknown

Instances

Instances details

Eq FormulaRole Source #
Instance details Defined in THF.As Methods (==) :: FormulaRole -> FormulaRole -> Bool (/=) :: FormulaRole -> FormulaRole -> Bool
Data FormulaRole Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FormulaRole -> c FormulaRole gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FormulaRole toConstr :: FormulaRole -> Constr dataTypeOf :: FormulaRole -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FormulaRole) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FormulaRole) gmapT :: (forall b. Data b => b -> b) -> FormulaRole -> FormulaRole gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FormulaRole -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FormulaRole -> r gmapQ :: (forall d. Data d => d -> u) -> FormulaRole -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FormulaRole -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FormulaRole -> m FormulaRole gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FormulaRole -> m FormulaRole gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FormulaRole -> m FormulaRole
Ord FormulaRole Source #
Instance details Defined in THF.As Methods compare :: FormulaRole -> FormulaRole -> Ordering (<) :: FormulaRole -> FormulaRole -> Bool (<=) :: FormulaRole -> FormulaRole -> Bool (>) :: FormulaRole -> FormulaRole -> Bool (>=) :: FormulaRole -> FormulaRole -> Bool max :: FormulaRole -> FormulaRole -> FormulaRole min :: FormulaRole -> FormulaRole -> FormulaRole
Show FormulaRole Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> FormulaRole -> ShowS show :: FormulaRole -> String showList :: [FormulaRole] -> ShowS
Generic FormulaRole
Instance details Defined in THF.ATC_THF Associated Types type Rep FormulaRole :: Type -> Type Methods from :: FormulaRole -> Rep FormulaRole x to :: Rep FormulaRole x -> FormulaRole
GetRange FormulaRole Source #
Instance details Defined in THF.As Methods getRange :: FormulaRole -> Range Source # rangeSpan :: FormulaRole -> [Pos] Source #
FromJSON FormulaRole
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser FormulaRole parseJSONList :: Value -> Parser [FormulaRole]
ToJSON FormulaRole
Instance details Defined in THF.ATC_THF Methods toJSON :: FormulaRole -> Value toEncoding :: FormulaRole -> Encoding toJSONList :: [FormulaRole] -> Value toEncodingList :: [FormulaRole] -> Encoding
ShATermConvertible FormulaRole
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> FormulaRole -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FormulaRole] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FormulaRole) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FormulaRole])
Pretty FormulaRole Source #
Instance details Defined in THF.PrintTHF Methods pretty :: FormulaRole -> Doc Source # pretties :: [FormulaRole] -> Doc Source #
type Rep FormulaRole
Instance details Defined in THF.ATC_THF type Rep FormulaRole = D1 ('MetaData "FormulaRole" "THF.As" "main" 'False) (((C1 ('MetaCons "Axiom" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Hypothesis" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Definition" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Assumption" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Lemma" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Theorem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Conjecture" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Negated_Conjecture" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Plain" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Fi_Domain" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Fi_Functors" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Fi_Predicates" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Type" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Unknown" 'PrefixI 'False) (U1 :: Type -> Type)))))

data THFFormula Source #

Constructors

TF_THF_Logic_Formula THFLogicFormula
TF_THF_Sequent THFSequent
T0F_THF_Typed_Const THFTypedConst

Instances

Instances details

Eq THFFormula Source #
Instance details Defined in THF.As Methods (==) :: THFFormula -> THFFormula -> Bool (/=) :: THFFormula -> THFFormula -> Bool
Data THFFormula Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFFormula -> c THFFormula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFFormula toConstr :: THFFormula -> Constr dataTypeOf :: THFFormula -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFFormula) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFFormula) gmapT :: (forall b. Data b => b -> b) -> THFFormula -> THFFormula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFFormula -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFFormula -> r gmapQ :: (forall d. Data d => d -> u) -> THFFormula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFFormula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFFormula -> m THFFormula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFFormula -> m THFFormula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFFormula -> m THFFormula
Ord THFFormula Source #
Instance details Defined in THF.As Methods compare :: THFFormula -> THFFormula -> Ordering (<) :: THFFormula -> THFFormula -> Bool (<=) :: THFFormula -> THFFormula -> Bool (>) :: THFFormula -> THFFormula -> Bool (>=) :: THFFormula -> THFFormula -> Bool max :: THFFormula -> THFFormula -> THFFormula min :: THFFormula -> THFFormula -> THFFormula
Show THFFormula Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFFormula -> ShowS show :: THFFormula -> String showList :: [THFFormula] -> ShowS
Generic THFFormula
Instance details Defined in THF.ATC_THF Associated Types type Rep THFFormula :: Type -> Type Methods from :: THFFormula -> Rep THFFormula x to :: Rep THFFormula x -> THFFormula
GetRange THFFormula Source #
Instance details Defined in THF.As Methods getRange :: THFFormula -> Range Source # rangeSpan :: THFFormula -> [Pos] Source #
FromJSON THFFormula
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFFormula parseJSONList :: Value -> Parser [THFFormula]
ToJSON THFFormula
Instance details Defined in THF.ATC_THF Methods toJSON :: THFFormula -> Value toEncoding :: THFFormula -> Encoding toJSONList :: [THFFormula] -> Value toEncodingList :: [THFFormula] -> Encoding
ShATermConvertible THFFormula
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFFormula -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFFormula] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFFormula) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFFormula])
Pretty THFFormula Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFFormula -> Doc Source # pretties :: [THFFormula] -> Doc Source #
MinSublogic THFSl THFFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFFormula -> THFSl Source #
Sentences THF THFFormula SignTHF MorphismTHF SymbolTHF Source #
Instance details Defined in THF.Logic_THF Methods map_sen :: THF -> MorphismTHF -> THFFormula -> Result THFFormula Source # simplify_sen :: THF -> SignTHF -> THFFormula -> THFFormula Source # negation :: THF -> THFFormula -> Maybe THFFormula Source # print_sign :: THF -> SignTHF -> Doc Source # print_named :: THF -> Named THFFormula -> Doc Source # sym_of :: THF -> SignTHF -> [Set SymbolTHF] Source # mostSymsOf :: THF -> SignTHF -> [SymbolTHF] Source # symmap_of :: THF -> MorphismTHF -> EndoMap SymbolTHF Source # sym_name :: THF -> SymbolTHF -> Id Source # sym_label :: THF -> SymbolTHF -> Maybe String Source # fullSymName :: THF -> SymbolTHF -> String Source # symKind :: THF -> SymbolTHF -> String Source # symsOfSen :: THF -> SignTHF -> THFFormula -> [SymbolTHF] Source # pair_symbols :: THF -> SymbolTHF -> SymbolTHF -> Result SymbolTHF Source #
StaticAnalysis THF BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () Source #
Instance details Defined in THF.Logic_THF Methods basic_analysis :: THF -> Maybe ((BasicSpecTHF, SignTHF, GlobalAnnos) -> Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])) Source # sen_analysis :: THF -> Maybe ((BasicSpecTHF, SignTHF, THFFormula) -> Result THFFormula) Source # extBasicAnalysis :: THF -> IRI -> LibName -> BasicSpecTHF -> SignTHF -> GlobalAnnos -> Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula]) Source # stat_symb_map_items :: THF -> SignTHF -> Maybe SignTHF -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: THF -> SignTHF -> [()] -> Result [()] Source # convertTheory :: THF -> Maybe ((SignTHF, [Named THFFormula]) -> BasicSpecTHF) Source # ensures_amalgamability :: THF -> ([CASLAmalgOpt], Gr SignTHF (Int, MorphismTHF), [(Int, MorphismTHF)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: THF -> MorphismTHF -> [Named THFFormula] -> Result (SignTHF, [Named THFFormula]) Source # signature_colimit :: THF -> Gr SignTHF (Int, MorphismTHF) -> Result (SignTHF, Map Int MorphismTHF) Source # qualify :: THF -> SIMPLE_ID -> LibName -> MorphismTHF -> SignTHF -> Result (MorphismTHF, [Named THFFormula]) Source # symbol_to_raw :: THF -> SymbolTHF -> () Source # id_to_raw :: THF -> Id -> () Source # matches :: THF -> SymbolTHF -> () -> Bool Source # empty_signature :: THF -> SignTHF Source # add_symb_to_sign :: THF -> SignTHF -> SymbolTHF -> Result SignTHF Source # signature_union :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # signatureDiff :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # intersection :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # final_union :: THF -> SignTHF -> SignTHF -> Result SignTHF Source # morphism_union :: THF -> MorphismTHF -> MorphismTHF -> Result MorphismTHF Source # is_subsig :: THF -> SignTHF -> SignTHF -> Bool Source # subsig_inclusion :: THF -> SignTHF -> SignTHF -> Result MorphismTHF Source # generated_sign :: THF -> Set SymbolTHF -> SignTHF -> Result MorphismTHF Source # cogenerated_sign :: THF -> Set SymbolTHF -> SignTHF -> Result MorphismTHF Source # induced_from_morphism :: THF -> EndoMap () -> SignTHF -> Result MorphismTHF Source # induced_from_to_morphism :: THF -> EndoMap () -> ExtSign SignTHF SymbolTHF -> ExtSign SignTHF SymbolTHF -> Result MorphismTHF Source # is_transportable :: THF -> MorphismTHF -> Bool Source # is_injective :: THF -> MorphismTHF -> Bool Source # theory_to_taxonomy :: THF -> TaxoGraphKind -> MMiSSOntology -> SignTHF -> [Named THFFormula] -> Result MMiSSOntology Source # corresp2th :: THF -> String -> Bool -> SignTHF -> SignTHF -> [()] -> [()] -> EndoMap SymbolTHF -> EndoMap SymbolTHF -> REL_REF -> Result (SignTHF, [Named THFFormula], SignTHF, SignTHF, EndoMap SymbolTHF, EndoMap SymbolTHF) Source # equiv2cospan :: THF -> SignTHF -> SignTHF -> [()] -> [()] -> Result (SignTHF, SignTHF, SignTHF, EndoMap SymbolTHF, EndoMap SymbolTHF) Source # extract_module :: THF -> [IRI] -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #
Logic THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in THF.Logic_THF Methods parse_basic_sen :: THF -> Maybe (BasicSpecTHF -> AParser st THFFormula) Source # stability :: THF -> Stability Source # data_logic :: THF -> Maybe AnyLogic Source # top_sublogic :: THF -> THFSl Source # all_sublogics :: THF -> [THFSl] Source # bottomSublogic :: THF -> Maybe THFSl Source # sublogicDimensions :: THF -> [[THFSl]] Source # parseSublogic :: THF -> String -> Maybe THFSl Source # proj_sublogic_epsilon :: THF -> THFSl -> SignTHF -> MorphismTHF Source # provers :: THF -> [Prover SignTHF THFFormula MorphismTHF THFSl ProofTree] Source # default_prover :: THF -> String Source # cons_checkers :: THF -> [ConsChecker SignTHF THFFormula THFSl MorphismTHF ProofTree] Source # conservativityCheck :: THF -> [ConservativityChecker SignTHF THFFormula MorphismTHF] Source # empty_proof_tree :: THF -> ProofTree Source # syntaxTable :: THF -> SignTHF -> Maybe SyntaxTable Source # omdoc_metatheory :: THF -> Maybe OMCD Source # export_symToOmdoc :: THF -> NameMap SymbolTHF -> SymbolTHF -> String -> Result TCElement Source # export_senToOmdoc :: THF -> NameMap SymbolTHF -> THFFormula -> Result TCorOMElement Source # export_theoryToOmdoc :: THF -> SigMap SymbolTHF -> SignTHF -> [Named THFFormula] -> Result [TCElement] Source # omdocToSym :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result SymbolTHF Source # omdocToSen :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result (Maybe (Named THFFormula)) Source # addOMadtToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [[OmdADT]] -> Result (SignTHF, [Named THFFormula]) Source # addOmdocToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [TCElement] -> Result (SignTHF, [Named THFFormula]) Source # sublogicOfTheo :: THF -> (SignTHF, [THFFormula]) -> THFSl Source #
Comorphism THFP_P2THFP THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.THFP_P2THFP Methods sourceLogic :: THFP_P2THFP -> THF Source # sourceSublogic :: THFP_P2THFP -> THFSl Source # sourceSublogicLossy :: THFP_P2THFP -> THFSl Source # minSourceTheory :: THFP_P2THFP -> Maybe (LibName, String) Source # targetLogic :: THFP_P2THFP -> THF Source # mapSublogic :: THFP_P2THFP -> THFSl -> Maybe THFSl Source # map_theory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: THFP_P2THFP -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: THFP_P2THFP -> MorphismTHF -> Result MorphismTHF Source # map_sentence :: THFP_P2THFP -> SignTHF -> THFFormula -> Result THFFormula Source # map_symbol :: THFP_P2THFP -> SignTHF -> SymbolTHF -> Set SymbolTHF Source # extractModel :: THFP_P2THFP -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2THFP -> Bool Source # has_model_expansion :: THFP_P2THFP -> Bool Source # is_weakly_amalgamable :: THFP_P2THFP -> Bool Source # constituents :: THFP_P2THFP -> [String] Source # isInclusionComorphism :: THFP_P2THFP -> Bool Source # rps :: THFP_P2THFP -> Bool Source # eps :: THFP_P2THFP -> Bool Source # isGTC :: THFP_P2THFP -> Bool Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source # isGTC :: THFP_P2HasCASL -> Bool Source #
Comorphism THFP2THF0 THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.THFP2THF0 Methods sourceLogic :: THFP2THF0 -> THF Source # sourceSublogic :: THFP2THF0 -> THFSl Source # sourceSublogicLossy :: THFP2THF0 -> THFSl Source # minSourceTheory :: THFP2THF0 -> Maybe (LibName, String) Source # targetLogic :: THFP2THF0 -> THF Source # mapSublogic :: THFP2THF0 -> THFSl -> Maybe THFSl Source # map_theory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: THFP2THF0 -> MorphismTHF -> Result MorphismTHF Source # map_sentence :: THFP2THF0 -> SignTHF -> THFFormula -> Result THFFormula Source # map_symbol :: THFP2THF0 -> SignTHF -> SymbolTHF -> Set SymbolTHF Source # extractModel :: THFP2THF0 -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP2THF0 -> Bool Source # has_model_expansion :: THFP2THF0 -> Bool Source # is_weakly_amalgamable :: THFP2THF0 -> Bool Source # constituents :: THFP2THF0 -> [String] Source # isInclusionComorphism :: THFP2THF0 -> Bool Source # rps :: THFP2THF0 -> Bool Source # eps :: THFP2THF0 -> Bool Source # isGTC :: THFP2THF0 -> Bool Source #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.HasCASL2THFP_P Methods sourceLogic :: HasCASL2THFP_P -> HasCASL Source # sourceSublogic :: HasCASL2THFP_P -> Sublogic Source # sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source # minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source # targetLogic :: HasCASL2THFP_P -> THF Source # mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source # map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source # map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source # map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source # extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2THFP_P -> Bool Source # has_model_expansion :: HasCASL2THFP_P -> Bool Source # is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source # constituents :: HasCASL2THFP_P -> [String] Source # isInclusionComorphism :: HasCASL2THFP_P -> Bool Source # rps :: HasCASL2THFP_P -> Bool Source # eps :: HasCASL2THFP_P -> Bool Source # isGTC :: HasCASL2THFP_P -> Bool Source #
type Rep THFFormula
Instance details Defined in THF.ATC_THF type Rep THFFormula = D1 ('MetaData "THFFormula" "THF.As" "main" 'False) (C1 ('MetaCons "TF_THF_Logic_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFLogicFormula)) :+: (C1 ('MetaCons "TF_THF_Sequent" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFSequent)) :+: C1 ('MetaCons "T0F_THF_Typed_Const" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFTypedConst))))

data THFLogicFormula Source #

Constructors

TLF_THF_Binary_Formula THFBinaryFormula
TLF_THF_Unitary_Formula THFUnitaryFormula
TLF_THF_Type_Formula THFTypeFormula
TLF_THF_Sub_Type THFSubType

Instances

Instances details

Eq THFLogicFormula Source #
Instance details Defined in THF.As Methods (==) :: THFLogicFormula -> THFLogicFormula -> Bool (/=) :: THFLogicFormula -> THFLogicFormula -> Bool
Data THFLogicFormula Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFLogicFormula -> c THFLogicFormula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFLogicFormula toConstr :: THFLogicFormula -> Constr dataTypeOf :: THFLogicFormula -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFLogicFormula) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFLogicFormula) gmapT :: (forall b. Data b => b -> b) -> THFLogicFormula -> THFLogicFormula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFLogicFormula -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFLogicFormula -> r gmapQ :: (forall d. Data d => d -> u) -> THFLogicFormula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFLogicFormula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFLogicFormula -> m THFLogicFormula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFLogicFormula -> m THFLogicFormula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFLogicFormula -> m THFLogicFormula
Ord THFLogicFormula Source #
Instance details Defined in THF.As Methods compare :: THFLogicFormula -> THFLogicFormula -> Ordering (<) :: THFLogicFormula -> THFLogicFormula -> Bool (<=) :: THFLogicFormula -> THFLogicFormula -> Bool (>) :: THFLogicFormula -> THFLogicFormula -> Bool (>=) :: THFLogicFormula -> THFLogicFormula -> Bool max :: THFLogicFormula -> THFLogicFormula -> THFLogicFormula min :: THFLogicFormula -> THFLogicFormula -> THFLogicFormula
Show THFLogicFormula Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFLogicFormula -> ShowS show :: THFLogicFormula -> String showList :: [THFLogicFormula] -> ShowS
Generic THFLogicFormula
Instance details Defined in THF.ATC_THF Associated Types type Rep THFLogicFormula :: Type -> Type Methods from :: THFLogicFormula -> Rep THFLogicFormula x to :: Rep THFLogicFormula x -> THFLogicFormula
GetRange THFLogicFormula Source #
Instance details Defined in THF.As Methods getRange :: THFLogicFormula -> Range Source # rangeSpan :: THFLogicFormula -> [Pos] Source #
FromJSON THFLogicFormula
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFLogicFormula parseJSONList :: Value -> Parser [THFLogicFormula]
ToJSON THFLogicFormula
Instance details Defined in THF.ATC_THF Methods toJSON :: THFLogicFormula -> Value toEncoding :: THFLogicFormula -> Encoding toJSONList :: [THFLogicFormula] -> Value toEncodingList :: [THFLogicFormula] -> Encoding
ShATermConvertible THFLogicFormula
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFLogicFormula -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFLogicFormula] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFLogicFormula) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFLogicFormula])
Pretty THFLogicFormula Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFLogicFormula -> Doc Source # pretties :: [THFLogicFormula] -> Doc Source #
MinSublogic THFSl THFLogicFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFLogicFormula -> THFSl Source #
type Rep THFLogicFormula
Instance details Defined in THF.ATC_THF type Rep THFLogicFormula = D1 ('MetaData "THFLogicFormula" "THF.As" "main" 'False) ((C1 ('MetaCons "TLF_THF_Binary_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFBinaryFormula)) :+: C1 ('MetaCons "TLF_THF_Unitary_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFUnitaryFormula))) :+: (C1 ('MetaCons "TLF_THF_Type_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFTypeFormula)) :+: C1 ('MetaCons "TLF_THF_Sub_Type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFSubType))))

data THFBinaryFormula Source #

Constructors

TBF_THF_Binary_Pair THFUnitaryFormula THFPairConnective THFUnitaryFormula
TBF_THF_Binary_Tuple THFBinaryTuple
TBF_THF_Binary_Type THFBinaryType

Instances

Instances details

Eq THFBinaryFormula Source #
Instance details Defined in THF.As Methods (==) :: THFBinaryFormula -> THFBinaryFormula -> Bool (/=) :: THFBinaryFormula -> THFBinaryFormula -> Bool
Data THFBinaryFormula Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFBinaryFormula -> c THFBinaryFormula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFBinaryFormula toConstr :: THFBinaryFormula -> Constr dataTypeOf :: THFBinaryFormula -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFBinaryFormula) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFBinaryFormula) gmapT :: (forall b. Data b => b -> b) -> THFBinaryFormula -> THFBinaryFormula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFBinaryFormula -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFBinaryFormula -> r gmapQ :: (forall d. Data d => d -> u) -> THFBinaryFormula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFBinaryFormula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFBinaryFormula -> m THFBinaryFormula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFBinaryFormula -> m THFBinaryFormula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFBinaryFormula -> m THFBinaryFormula
Ord THFBinaryFormula Source #
Instance details Defined in THF.As Methods compare :: THFBinaryFormula -> THFBinaryFormula -> Ordering (<) :: THFBinaryFormula -> THFBinaryFormula -> Bool (<=) :: THFBinaryFormula -> THFBinaryFormula -> Bool (>) :: THFBinaryFormula -> THFBinaryFormula -> Bool (>=) :: THFBinaryFormula -> THFBinaryFormula -> Bool max :: THFBinaryFormula -> THFBinaryFormula -> THFBinaryFormula min :: THFBinaryFormula -> THFBinaryFormula -> THFBinaryFormula
Show THFBinaryFormula Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFBinaryFormula -> ShowS show :: THFBinaryFormula -> String showList :: [THFBinaryFormula] -> ShowS
Generic THFBinaryFormula
Instance details Defined in THF.ATC_THF Associated Types type Rep THFBinaryFormula :: Type -> Type Methods from :: THFBinaryFormula -> Rep THFBinaryFormula x to :: Rep THFBinaryFormula x -> THFBinaryFormula
GetRange THFBinaryFormula Source #
Instance details Defined in THF.As Methods getRange :: THFBinaryFormula -> Range Source # rangeSpan :: THFBinaryFormula -> [Pos] Source #
FromJSON THFBinaryFormula
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFBinaryFormula parseJSONList :: Value -> Parser [THFBinaryFormula]
ToJSON THFBinaryFormula
Instance details Defined in THF.ATC_THF Methods toJSON :: THFBinaryFormula -> Value toEncoding :: THFBinaryFormula -> Encoding toJSONList :: [THFBinaryFormula] -> Value toEncodingList :: [THFBinaryFormula] -> Encoding
ShATermConvertible THFBinaryFormula
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFBinaryFormula -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFBinaryFormula] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFBinaryFormula) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFBinaryFormula])
Pretty THFBinaryFormula Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFBinaryFormula -> Doc Source # pretties :: [THFBinaryFormula] -> Doc Source #
MinSublogic THFSl THFBinaryFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFBinaryFormula -> THFSl Source #
type Rep THFBinaryFormula
Instance details Defined in THF.ATC_THF type Rep THFBinaryFormula = D1 ('MetaData "THFBinaryFormula" "THF.As" "main" 'False) (C1 ('MetaCons "TBF_THF_Binary_Pair" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFUnitaryFormula) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFPairConnective) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFUnitaryFormula))) :+: (C1 ('MetaCons "TBF_THF_Binary_Tuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFBinaryTuple)) :+: C1 ('MetaCons "TBF_THF_Binary_Type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFBinaryType))))

data THFBinaryTuple Source #

Constructors

TBT_THF_Or_Formula [THFUnitaryFormula]
TBT_THF_And_Formula [THFUnitaryFormula]
TBT_THF_Apply_Formula [THFUnitaryFormula]

Instances

Instances details

Eq THFBinaryTuple Source #
Instance details Defined in THF.As Methods (==) :: THFBinaryTuple -> THFBinaryTuple -> Bool (/=) :: THFBinaryTuple -> THFBinaryTuple -> Bool
Data THFBinaryTuple Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFBinaryTuple -> c THFBinaryTuple gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFBinaryTuple toConstr :: THFBinaryTuple -> Constr dataTypeOf :: THFBinaryTuple -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFBinaryTuple) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFBinaryTuple) gmapT :: (forall b. Data b => b -> b) -> THFBinaryTuple -> THFBinaryTuple gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFBinaryTuple -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFBinaryTuple -> r gmapQ :: (forall d. Data d => d -> u) -> THFBinaryTuple -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFBinaryTuple -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFBinaryTuple -> m THFBinaryTuple gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFBinaryTuple -> m THFBinaryTuple gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFBinaryTuple -> m THFBinaryTuple
Ord THFBinaryTuple Source #
Instance details Defined in THF.As Methods compare :: THFBinaryTuple -> THFBinaryTuple -> Ordering (<) :: THFBinaryTuple -> THFBinaryTuple -> Bool (<=) :: THFBinaryTuple -> THFBinaryTuple -> Bool (>) :: THFBinaryTuple -> THFBinaryTuple -> Bool (>=) :: THFBinaryTuple -> THFBinaryTuple -> Bool max :: THFBinaryTuple -> THFBinaryTuple -> THFBinaryTuple min :: THFBinaryTuple -> THFBinaryTuple -> THFBinaryTuple
Show THFBinaryTuple Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFBinaryTuple -> ShowS show :: THFBinaryTuple -> String showList :: [THFBinaryTuple] -> ShowS
Generic THFBinaryTuple
Instance details Defined in THF.ATC_THF Associated Types type Rep THFBinaryTuple :: Type -> Type Methods from :: THFBinaryTuple -> Rep THFBinaryTuple x to :: Rep THFBinaryTuple x -> THFBinaryTuple
GetRange THFBinaryTuple Source #
Instance details Defined in THF.As Methods getRange :: THFBinaryTuple -> Range Source # rangeSpan :: THFBinaryTuple -> [Pos] Source #
FromJSON THFBinaryTuple
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFBinaryTuple parseJSONList :: Value -> Parser [THFBinaryTuple]
ToJSON THFBinaryTuple
Instance details Defined in THF.ATC_THF Methods toJSON :: THFBinaryTuple -> Value toEncoding :: THFBinaryTuple -> Encoding toJSONList :: [THFBinaryTuple] -> Value toEncodingList :: [THFBinaryTuple] -> Encoding
ShATermConvertible THFBinaryTuple
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFBinaryTuple -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFBinaryTuple] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFBinaryTuple) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFBinaryTuple])
Pretty THFBinaryTuple Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFBinaryTuple -> Doc Source # pretties :: [THFBinaryTuple] -> Doc Source #
MinSublogic THFSl THFBinaryTuple Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFBinaryTuple -> THFSl Source #
type Rep THFBinaryTuple
Instance details Defined in THF.ATC_THF type Rep THFBinaryTuple = D1 ('MetaData "THFBinaryTuple" "THF.As" "main" 'False) (C1 ('MetaCons "TBT_THF_Or_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [THFUnitaryFormula])) :+: (C1 ('MetaCons "TBT_THF_And_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [THFUnitaryFormula])) :+: C1 ('MetaCons "TBT_THF_Apply_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [THFUnitaryFormula]))))

data THFUnitaryFormula Source #

Constructors

TUF_THF_Quantified_Formula THFQuantifiedFormula
TUF_THF_Unary_Formula THFUnaryConnective THFLogicFormula
TUF_THF_Atom THFAtom
TUF_THF_Tuple THFTuple
TUF_THF_Conditional THFLogicFormula THFLogicFormula THFLogicFormula
TUF_THF_Logic_Formula_Par THFLogicFormula
T0UF_THF_Abstraction THFVariableList THFUnitaryFormula

Instances

Instances details

Eq THFUnitaryFormula Source #
Instance details Defined in THF.As Methods (==) :: THFUnitaryFormula -> THFUnitaryFormula -> Bool (/=) :: THFUnitaryFormula -> THFUnitaryFormula -> Bool
Data THFUnitaryFormula Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFUnitaryFormula -> c THFUnitaryFormula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFUnitaryFormula toConstr :: THFUnitaryFormula -> Constr dataTypeOf :: THFUnitaryFormula -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFUnitaryFormula) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFUnitaryFormula) gmapT :: (forall b. Data b => b -> b) -> THFUnitaryFormula -> THFUnitaryFormula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFUnitaryFormula -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFUnitaryFormula -> r gmapQ :: (forall d. Data d => d -> u) -> THFUnitaryFormula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFUnitaryFormula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFUnitaryFormula -> m THFUnitaryFormula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFUnitaryFormula -> m THFUnitaryFormula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFUnitaryFormula -> m THFUnitaryFormula
Ord THFUnitaryFormula Source #
Instance details Defined in THF.As Methods compare :: THFUnitaryFormula -> THFUnitaryFormula -> Ordering (<) :: THFUnitaryFormula -> THFUnitaryFormula -> Bool (<=) :: THFUnitaryFormula -> THFUnitaryFormula -> Bool (>) :: THFUnitaryFormula -> THFUnitaryFormula -> Bool (>=) :: THFUnitaryFormula -> THFUnitaryFormula -> Bool max :: THFUnitaryFormula -> THFUnitaryFormula -> THFUnitaryFormula min :: THFUnitaryFormula -> THFUnitaryFormula -> THFUnitaryFormula
Show THFUnitaryFormula Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFUnitaryFormula -> ShowS show :: THFUnitaryFormula -> String showList :: [THFUnitaryFormula] -> ShowS
Generic THFUnitaryFormula
Instance details Defined in THF.ATC_THF Associated Types type Rep THFUnitaryFormula :: Type -> Type Methods from :: THFUnitaryFormula -> Rep THFUnitaryFormula x to :: Rep THFUnitaryFormula x -> THFUnitaryFormula
GetRange THFUnitaryFormula Source #
Instance details Defined in THF.As Methods getRange :: THFUnitaryFormula -> Range Source # rangeSpan :: THFUnitaryFormula -> [Pos] Source #
FromJSON THFUnitaryFormula
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFUnitaryFormula parseJSONList :: Value -> Parser [THFUnitaryFormula]
ToJSON THFUnitaryFormula
Instance details Defined in THF.ATC_THF Methods toJSON :: THFUnitaryFormula -> Value toEncoding :: THFUnitaryFormula -> Encoding toJSONList :: [THFUnitaryFormula] -> Value toEncodingList :: [THFUnitaryFormula] -> Encoding
ShATermConvertible THFUnitaryFormula
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFUnitaryFormula -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFUnitaryFormula] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFUnitaryFormula) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFUnitaryFormula])
Pretty THFUnitaryFormula Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFUnitaryFormula -> Doc Source # pretties :: [THFUnitaryFormula] -> Doc Source #
MinSublogic THFSl THFUnitaryFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFUnitaryFormula -> THFSl Source #
type Rep THFUnitaryFormula
Instance details Defined in THF.ATC_THF type Rep THFUnitaryFormula = D1 ('MetaData "THFUnitaryFormula" "THF.As" "main" 'False) ((C1 ('MetaCons "TUF_THF_Quantified_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFQuantifiedFormula)) :+: (C1 ('MetaCons "TUF_THF_Unary_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFUnaryConnective) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFLogicFormula)) :+: C1 ('MetaCons "TUF_THF_Atom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFAtom)))) :+: ((C1 ('MetaCons "TUF_THF_Tuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFTuple)) :+: C1 ('MetaCons "TUF_THF_Conditional" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFLogicFormula) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFLogicFormula) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFLogicFormula)))) :+: (C1 ('MetaCons "TUF_THF_Logic_Formula_Par" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFLogicFormula)) :+: C1 ('MetaCons "T0UF_THF_Abstraction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFVariableList) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFUnitaryFormula)))))

data THFQuantifiedFormula Source #

Constructors

TQF_THF_Quantified_Formula THFQuantifier THFVariableList THFUnitaryFormula
T0QF_THF_Quantified_Var Quantifier THFVariableList THFUnitaryFormula
T0QF_THF_Quantified_Novar THFQuantifier THFUnitaryFormula

Instances

Instances details

Eq THFQuantifiedFormula Source #
Instance details Defined in THF.As Methods (==) :: THFQuantifiedFormula -> THFQuantifiedFormula -> Bool (/=) :: THFQuantifiedFormula -> THFQuantifiedFormula -> Bool
Data THFQuantifiedFormula Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFQuantifiedFormula -> c THFQuantifiedFormula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFQuantifiedFormula toConstr :: THFQuantifiedFormula -> Constr dataTypeOf :: THFQuantifiedFormula -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFQuantifiedFormula) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFQuantifiedFormula) gmapT :: (forall b. Data b => b -> b) -> THFQuantifiedFormula -> THFQuantifiedFormula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFQuantifiedFormula -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFQuantifiedFormula -> r gmapQ :: (forall d. Data d => d -> u) -> THFQuantifiedFormula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFQuantifiedFormula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFQuantifiedFormula -> m THFQuantifiedFormula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFQuantifiedFormula -> m THFQuantifiedFormula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFQuantifiedFormula -> m THFQuantifiedFormula
Ord THFQuantifiedFormula Source #
Instance details Defined in THF.As Methods compare :: THFQuantifiedFormula -> THFQuantifiedFormula -> Ordering (<) :: THFQuantifiedFormula -> THFQuantifiedFormula -> Bool (<=) :: THFQuantifiedFormula -> THFQuantifiedFormula -> Bool (>) :: THFQuantifiedFormula -> THFQuantifiedFormula -> Bool (>=) :: THFQuantifiedFormula -> THFQuantifiedFormula -> Bool max :: THFQuantifiedFormula -> THFQuantifiedFormula -> THFQuantifiedFormula min :: THFQuantifiedFormula -> THFQuantifiedFormula -> THFQuantifiedFormula
Show THFQuantifiedFormula Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFQuantifiedFormula -> ShowS show :: THFQuantifiedFormula -> String showList :: [THFQuantifiedFormula] -> ShowS
Generic THFQuantifiedFormula
Instance details Defined in THF.ATC_THF Associated Types type Rep THFQuantifiedFormula :: Type -> Type Methods from :: THFQuantifiedFormula -> Rep THFQuantifiedFormula x to :: Rep THFQuantifiedFormula x -> THFQuantifiedFormula
GetRange THFQuantifiedFormula Source #
Instance details Defined in THF.As Methods getRange :: THFQuantifiedFormula -> Range Source # rangeSpan :: THFQuantifiedFormula -> [Pos] Source #
FromJSON THFQuantifiedFormula
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFQuantifiedFormula parseJSONList :: Value -> Parser [THFQuantifiedFormula]
ToJSON THFQuantifiedFormula
Instance details Defined in THF.ATC_THF Methods toJSON :: THFQuantifiedFormula -> Value toEncoding :: THFQuantifiedFormula -> Encoding toJSONList :: [THFQuantifiedFormula] -> Value toEncodingList :: [THFQuantifiedFormula] -> Encoding
ShATermConvertible THFQuantifiedFormula
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFQuantifiedFormula -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFQuantifiedFormula] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFQuantifiedFormula) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFQuantifiedFormula])
Pretty THFQuantifiedFormula Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFQuantifiedFormula -> Doc Source # pretties :: [THFQuantifiedFormula] -> Doc Source #
MinSublogic THFSl THFQuantifiedFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFQuantifiedFormula -> THFSl Source #
type Rep THFQuantifiedFormula
Instance details Defined in THF.ATC_THF type Rep THFQuantifiedFormula = D1 ('MetaData "THFQuantifiedFormula" "THF.As" "main" 'False) (C1 ('MetaCons "TQF_THF_Quantified_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFQuantifier) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFVariableList) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFUnitaryFormula))) :+: (C1 ('MetaCons "T0QF_THF_Quantified_Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Quantifier) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFVariableList) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFUnitaryFormula))) :+: C1 ('MetaCons "T0QF_THF_Quantified_Novar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFQuantifier) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFUnitaryFormula))))

type THFVariableList = [THFVariable] Source #

data THFVariable Source #

Constructors

TV_THF_Typed_Variable Token THFTopLevelType
TV_Variable Token

Instances

Instances details

Eq THFVariable Source #
Instance details Defined in THF.As Methods (==) :: THFVariable -> THFVariable -> Bool (/=) :: THFVariable -> THFVariable -> Bool
Data THFVariable Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFVariable -> c THFVariable gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFVariable toConstr :: THFVariable -> Constr dataTypeOf :: THFVariable -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFVariable) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFVariable) gmapT :: (forall b. Data b => b -> b) -> THFVariable -> THFVariable gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFVariable -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFVariable -> r gmapQ :: (forall d. Data d => d -> u) -> THFVariable -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFVariable -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFVariable -> m THFVariable gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFVariable -> m THFVariable gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFVariable -> m THFVariable
Ord THFVariable Source #
Instance details Defined in THF.As Methods compare :: THFVariable -> THFVariable -> Ordering (<) :: THFVariable -> THFVariable -> Bool (<=) :: THFVariable -> THFVariable -> Bool (>) :: THFVariable -> THFVariable -> Bool (>=) :: THFVariable -> THFVariable -> Bool max :: THFVariable -> THFVariable -> THFVariable min :: THFVariable -> THFVariable -> THFVariable
Show THFVariable Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFVariable -> ShowS show :: THFVariable -> String showList :: [THFVariable] -> ShowS
Generic THFVariable
Instance details Defined in THF.ATC_THF Associated Types type Rep THFVariable :: Type -> Type Methods from :: THFVariable -> Rep THFVariable x to :: Rep THFVariable x -> THFVariable
GetRange THFVariable Source #
Instance details Defined in THF.As Methods getRange :: THFVariable -> Range Source # rangeSpan :: THFVariable -> [Pos] Source #
FromJSON THFVariable
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFVariable parseJSONList :: Value -> Parser [THFVariable]
ToJSON THFVariable
Instance details Defined in THF.ATC_THF Methods toJSON :: THFVariable -> Value toEncoding :: THFVariable -> Encoding toJSONList :: [THFVariable] -> Value toEncodingList :: [THFVariable] -> Encoding
ShATermConvertible THFVariable
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFVariable -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFVariable] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFVariable) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFVariable])
Pretty THFVariable Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFVariable -> Doc Source # pretties :: [THFVariable] -> Doc Source #
MinSublogic THFSl THFVariable Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFVariable -> THFSl Source #
type Rep THFVariable
Instance details Defined in THF.ATC_THF type Rep THFVariable = D1 ('MetaData "THFVariable" "THF.As" "main" 'False) (C1 ('MetaCons "TV_THF_Typed_Variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFTopLevelType)) :+: C1 ('MetaCons "TV_Variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data THFTypedConst Source #

Constructors

T0TC_Typed_Const Constant THFTopLevelType
T0TC_THF_TypedConst_Par THFTypedConst

Instances

Instances details

Eq THFTypedConst Source #
Instance details Defined in THF.As Methods (==) :: THFTypedConst -> THFTypedConst -> Bool (/=) :: THFTypedConst -> THFTypedConst -> Bool
Data THFTypedConst Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFTypedConst -> c THFTypedConst gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFTypedConst toConstr :: THFTypedConst -> Constr dataTypeOf :: THFTypedConst -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFTypedConst) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFTypedConst) gmapT :: (forall b. Data b => b -> b) -> THFTypedConst -> THFTypedConst gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFTypedConst -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFTypedConst -> r gmapQ :: (forall d. Data d => d -> u) -> THFTypedConst -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFTypedConst -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFTypedConst -> m THFTypedConst gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFTypedConst -> m THFTypedConst gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFTypedConst -> m THFTypedConst
Ord THFTypedConst Source #
Instance details Defined in THF.As Methods compare :: THFTypedConst -> THFTypedConst -> Ordering (<) :: THFTypedConst -> THFTypedConst -> Bool (<=) :: THFTypedConst -> THFTypedConst -> Bool (>) :: THFTypedConst -> THFTypedConst -> Bool (>=) :: THFTypedConst -> THFTypedConst -> Bool max :: THFTypedConst -> THFTypedConst -> THFTypedConst min :: THFTypedConst -> THFTypedConst -> THFTypedConst
Show THFTypedConst Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFTypedConst -> ShowS show :: THFTypedConst -> String showList :: [THFTypedConst] -> ShowS
Generic THFTypedConst
Instance details Defined in THF.ATC_THF Associated Types type Rep THFTypedConst :: Type -> Type Methods from :: THFTypedConst -> Rep THFTypedConst x to :: Rep THFTypedConst x -> THFTypedConst
GetRange THFTypedConst Source #
Instance details Defined in THF.As Methods getRange :: THFTypedConst -> Range Source # rangeSpan :: THFTypedConst -> [Pos] Source #
FromJSON THFTypedConst
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFTypedConst parseJSONList :: Value -> Parser [THFTypedConst]
ToJSON THFTypedConst
Instance details Defined in THF.ATC_THF Methods toJSON :: THFTypedConst -> Value toEncoding :: THFTypedConst -> Encoding toJSONList :: [THFTypedConst] -> Value toEncodingList :: [THFTypedConst] -> Encoding
ShATermConvertible THFTypedConst
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFTypedConst -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFTypedConst] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFTypedConst) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFTypedConst])
Pretty THFTypedConst Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFTypedConst -> Doc Source # pretties :: [THFTypedConst] -> Doc Source #
MinSublogic THFSl THFTypedConst Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFTypedConst -> THFSl Source #
type Rep THFTypedConst
Instance details Defined in THF.ATC_THF type Rep THFTypedConst = D1 ('MetaData "THFTypedConst" "THF.As" "main" 'False) (C1 ('MetaCons "T0TC_Typed_Const" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Constant) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFTopLevelType)) :+: C1 ('MetaCons "T0TC_THF_TypedConst_Par" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFTypedConst)))

data THFTypeFormula Source #

Constructors

TTF_THF_Type_Formula THFTypeableFormula THFTopLevelType
TTF_THF_Typed_Const Constant THFTopLevelType

Instances

Instances details

Eq THFTypeFormula Source #
Instance details Defined in THF.As Methods (==) :: THFTypeFormula -> THFTypeFormula -> Bool (/=) :: THFTypeFormula -> THFTypeFormula -> Bool
Data THFTypeFormula Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFTypeFormula -> c THFTypeFormula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFTypeFormula toConstr :: THFTypeFormula -> Constr dataTypeOf :: THFTypeFormula -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFTypeFormula) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFTypeFormula) gmapT :: (forall b. Data b => b -> b) -> THFTypeFormula -> THFTypeFormula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeFormula -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeFormula -> r gmapQ :: (forall d. Data d => d -> u) -> THFTypeFormula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFTypeFormula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFTypeFormula -> m THFTypeFormula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFTypeFormula -> m THFTypeFormula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFTypeFormula -> m THFTypeFormula
Ord THFTypeFormula Source #
Instance details Defined in THF.As Methods compare :: THFTypeFormula -> THFTypeFormula -> Ordering (<) :: THFTypeFormula -> THFTypeFormula -> Bool (<=) :: THFTypeFormula -> THFTypeFormula -> Bool (>) :: THFTypeFormula -> THFTypeFormula -> Bool (>=) :: THFTypeFormula -> THFTypeFormula -> Bool max :: THFTypeFormula -> THFTypeFormula -> THFTypeFormula min :: THFTypeFormula -> THFTypeFormula -> THFTypeFormula
Show THFTypeFormula Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFTypeFormula -> ShowS show :: THFTypeFormula -> String showList :: [THFTypeFormula] -> ShowS
Generic THFTypeFormula
Instance details Defined in THF.ATC_THF Associated Types type Rep THFTypeFormula :: Type -> Type Methods from :: THFTypeFormula -> Rep THFTypeFormula x to :: Rep THFTypeFormula x -> THFTypeFormula
GetRange THFTypeFormula Source #
Instance details Defined in THF.As Methods getRange :: THFTypeFormula -> Range Source # rangeSpan :: THFTypeFormula -> [Pos] Source #
FromJSON THFTypeFormula
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFTypeFormula parseJSONList :: Value -> Parser [THFTypeFormula]
ToJSON THFTypeFormula
Instance details Defined in THF.ATC_THF Methods toJSON :: THFTypeFormula -> Value toEncoding :: THFTypeFormula -> Encoding toJSONList :: [THFTypeFormula] -> Value toEncodingList :: [THFTypeFormula] -> Encoding
ShATermConvertible THFTypeFormula
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFTypeFormula -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFTypeFormula] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFTypeFormula) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFTypeFormula])
Pretty THFTypeFormula Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFTypeFormula -> Doc Source # pretties :: [THFTypeFormula] -> Doc Source #
MinSublogic THFSl THFTypeFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFTypeFormula -> THFSl Source #
type Rep THFTypeFormula
Instance details Defined in THF.ATC_THF type Rep THFTypeFormula = D1 ('MetaData "THFTypeFormula" "THF.As" "main" 'False) (C1 ('MetaCons "TTF_THF_Type_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFTypeableFormula) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFTopLevelType)) :+: C1 ('MetaCons "TTF_THF_Typed_Const" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Constant) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFTopLevelType)))

data THFTypeableFormula Source #

Constructors

TTyF_THF_Atom THFAtom
TTyF_THF_Tuple THFTuple
TTyF_THF_Logic_Formula THFLogicFormula

Instances

Instances details

Eq THFTypeableFormula Source #
Instance details Defined in THF.As Methods (==) :: THFTypeableFormula -> THFTypeableFormula -> Bool (/=) :: THFTypeableFormula -> THFTypeableFormula -> Bool
Data THFTypeableFormula Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFTypeableFormula -> c THFTypeableFormula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFTypeableFormula toConstr :: THFTypeableFormula -> Constr dataTypeOf :: THFTypeableFormula -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFTypeableFormula) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFTypeableFormula) gmapT :: (forall b. Data b => b -> b) -> THFTypeableFormula -> THFTypeableFormula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeableFormula -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFTypeableFormula -> r gmapQ :: (forall d. Data d => d -> u) -> THFTypeableFormula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFTypeableFormula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFTypeableFormula -> m THFTypeableFormula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFTypeableFormula -> m THFTypeableFormula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFTypeableFormula -> m THFTypeableFormula
Ord THFTypeableFormula Source #
Instance details Defined in THF.As Methods compare :: THFTypeableFormula -> THFTypeableFormula -> Ordering (<) :: THFTypeableFormula -> THFTypeableFormula -> Bool (<=) :: THFTypeableFormula -> THFTypeableFormula -> Bool (>) :: THFTypeableFormula -> THFTypeableFormula -> Bool (>=) :: THFTypeableFormula -> THFTypeableFormula -> Bool max :: THFTypeableFormula -> THFTypeableFormula -> THFTypeableFormula min :: THFTypeableFormula -> THFTypeableFormula -> THFTypeableFormula
Show THFTypeableFormula Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFTypeableFormula -> ShowS show :: THFTypeableFormula -> String showList :: [THFTypeableFormula] -> ShowS
Generic THFTypeableFormula
Instance details Defined in THF.ATC_THF Associated Types type Rep THFTypeableFormula :: Type -> Type Methods from :: THFTypeableFormula -> Rep THFTypeableFormula x to :: Rep THFTypeableFormula x -> THFTypeableFormula
GetRange THFTypeableFormula Source #
Instance details Defined in THF.As Methods getRange :: THFTypeableFormula -> Range Source # rangeSpan :: THFTypeableFormula -> [Pos] Source #
FromJSON THFTypeableFormula
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFTypeableFormula parseJSONList :: Value -> Parser [THFTypeableFormula]
ToJSON THFTypeableFormula
Instance details Defined in THF.ATC_THF Methods toJSON :: THFTypeableFormula -> Value toEncoding :: THFTypeableFormula -> Encoding toJSONList :: [THFTypeableFormula] -> Value toEncodingList :: [THFTypeableFormula] -> Encoding
ShATermConvertible THFTypeableFormula
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFTypeableFormula -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFTypeableFormula] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFTypeableFormula) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFTypeableFormula])
Pretty THFTypeableFormula Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFTypeableFormula -> Doc Source # pretties :: [THFTypeableFormula] -> Doc Source #
MinSublogic THFSl THFTypeableFormula Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFTypeableFormula -> THFSl Source #
type Rep THFTypeableFormula
Instance details Defined in THF.ATC_THF type Rep THFTypeableFormula = D1 ('MetaData "THFTypeableFormula" "THF.As" "main" 'False) (C1 ('MetaCons "TTyF_THF_Atom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFAtom)) :+: (C1 ('MetaCons "TTyF_THF_Tuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFTuple)) :+: C1 ('MetaCons "TTyF_THF_Logic_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFLogicFormula))))

data THFSubType Source #

Constructors

TST_THF_Sub_Type Constant Constant

Instances

Instances details

Eq THFSubType Source #
Instance details Defined in THF.As Methods (==) :: THFSubType -> THFSubType -> Bool (/=) :: THFSubType -> THFSubType -> Bool
Data THFSubType Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFSubType -> c THFSubType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFSubType toConstr :: THFSubType -> Constr dataTypeOf :: THFSubType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFSubType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFSubType) gmapT :: (forall b. Data b => b -> b) -> THFSubType -> THFSubType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFSubType -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFSubType -> r gmapQ :: (forall d. Data d => d -> u) -> THFSubType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFSubType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFSubType -> m THFSubType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFSubType -> m THFSubType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFSubType -> m THFSubType
Ord THFSubType Source #
Instance details Defined in THF.As Methods compare :: THFSubType -> THFSubType -> Ordering (<) :: THFSubType -> THFSubType -> Bool (<=) :: THFSubType -> THFSubType -> Bool (>) :: THFSubType -> THFSubType -> Bool (>=) :: THFSubType -> THFSubType -> Bool max :: THFSubType -> THFSubType -> THFSubType min :: THFSubType -> THFSubType -> THFSubType
Show THFSubType Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFSubType -> ShowS show :: THFSubType -> String showList :: [THFSubType] -> ShowS
Generic THFSubType
Instance details Defined in THF.ATC_THF Associated Types type Rep THFSubType :: Type -> Type Methods from :: THFSubType -> Rep THFSubType x to :: Rep THFSubType x -> THFSubType
GetRange THFSubType Source #
Instance details Defined in THF.As Methods getRange :: THFSubType -> Range Source # rangeSpan :: THFSubType -> [Pos] Source #
FromJSON THFSubType
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFSubType parseJSONList :: Value -> Parser [THFSubType]
ToJSON THFSubType
Instance details Defined in THF.ATC_THF Methods toJSON :: THFSubType -> Value toEncoding :: THFSubType -> Encoding toJSONList :: [THFSubType] -> Value toEncodingList :: [THFSubType] -> Encoding
ShATermConvertible THFSubType
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFSubType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFSubType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFSubType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFSubType])
Pretty THFSubType Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFSubType -> Doc Source # pretties :: [THFSubType] -> Doc Source #
MinSublogic THFSl THFSubType Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFSubType -> THFSl Source #
type Rep THFSubType
Instance details Defined in THF.ATC_THF type Rep THFSubType = D1 ('MetaData "THFSubType" "THF.As" "main" 'False) (C1 ('MetaCons "TST_THF_Sub_Type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Constant) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Constant)))

data THFTopLevelType Source #

Constructors

TTLT_THF_Logic_Formula THFLogicFormula
T0TLT_Constant Constant
T0TLT_Variable Token
T0TLT_Defined_Type DefinedType
T0TLT_System_Type Token
T0TLT_THF_Binary_Type THFBinaryType

Instances

Instances details

Eq THFTopLevelType Source #
Instance details Defined in THF.As Methods (==) :: THFTopLevelType -> THFTopLevelType -> Bool (/=) :: THFTopLevelType -> THFTopLevelType -> Bool
Data THFTopLevelType Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFTopLevelType -> c THFTopLevelType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFTopLevelType toConstr :: THFTopLevelType -> Constr dataTypeOf :: THFTopLevelType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFTopLevelType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFTopLevelType) gmapT :: (forall b. Data b => b -> b) -> THFTopLevelType -> THFTopLevelType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFTopLevelType -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFTopLevelType -> r gmapQ :: (forall d. Data d => d -> u) -> THFTopLevelType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFTopLevelType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFTopLevelType -> m THFTopLevelType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFTopLevelType -> m THFTopLevelType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFTopLevelType -> m THFTopLevelType
Ord THFTopLevelType Source #
Instance details Defined in THF.As Methods compare :: THFTopLevelType -> THFTopLevelType -> Ordering (<) :: THFTopLevelType -> THFTopLevelType -> Bool (<=) :: THFTopLevelType -> THFTopLevelType -> Bool (>) :: THFTopLevelType -> THFTopLevelType -> Bool (>=) :: THFTopLevelType -> THFTopLevelType -> Bool max :: THFTopLevelType -> THFTopLevelType -> THFTopLevelType min :: THFTopLevelType -> THFTopLevelType -> THFTopLevelType
Show THFTopLevelType Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFTopLevelType -> ShowS show :: THFTopLevelType -> String showList :: [THFTopLevelType] -> ShowS
Generic THFTopLevelType
Instance details Defined in THF.ATC_THF Associated Types type Rep THFTopLevelType :: Type -> Type Methods from :: THFTopLevelType -> Rep THFTopLevelType x to :: Rep THFTopLevelType x -> THFTopLevelType
GetRange THFTopLevelType Source #
Instance details Defined in THF.As Methods getRange :: THFTopLevelType -> Range Source # rangeSpan :: THFTopLevelType -> [Pos] Source #
FromJSON THFTopLevelType
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFTopLevelType parseJSONList :: Value -> Parser [THFTopLevelType]
ToJSON THFTopLevelType
Instance details Defined in THF.ATC_THF Methods toJSON :: THFTopLevelType -> Value toEncoding :: THFTopLevelType -> Encoding toJSONList :: [THFTopLevelType] -> Value toEncodingList :: [THFTopLevelType] -> Encoding
ShATermConvertible THFTopLevelType
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFTopLevelType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFTopLevelType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFTopLevelType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFTopLevelType])
Pretty THFTopLevelType Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFTopLevelType -> Doc Source # pretties :: [THFTopLevelType] -> Doc Source #
MinSublogic THFSl THFTopLevelType Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFTopLevelType -> THFSl Source #
type Rep THFTopLevelType
Instance details Defined in THF.ATC_THF type Rep THFTopLevelType = D1 ('MetaData "THFTopLevelType" "THF.As" "main" 'False) ((C1 ('MetaCons "TTLT_THF_Logic_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFLogicFormula)) :+: (C1 ('MetaCons "T0TLT_Constant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Constant)) :+: C1 ('MetaCons "T0TLT_Variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))) :+: (C1 ('MetaCons "T0TLT_Defined_Type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefinedType)) :+: (C1 ('MetaCons "T0TLT_System_Type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "T0TLT_THF_Binary_Type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFBinaryType)))))

data THFUnitaryType Source #

Constructors

TUT_THF_Unitary_Formula THFUnitaryFormula
T0UT_Constant Constant
T0UT_Variable Token
T0UT_Defined_Type DefinedType
T0UT_System_Type Token
T0UT_THF_Binary_Type_Par THFBinaryType

Instances

Instances details

Eq THFUnitaryType Source #
Instance details Defined in THF.As Methods (==) :: THFUnitaryType -> THFUnitaryType -> Bool (/=) :: THFUnitaryType -> THFUnitaryType -> Bool
Data THFUnitaryType Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFUnitaryType -> c THFUnitaryType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFUnitaryType toConstr :: THFUnitaryType -> Constr dataTypeOf :: THFUnitaryType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFUnitaryType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFUnitaryType) gmapT :: (forall b. Data b => b -> b) -> THFUnitaryType -> THFUnitaryType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFUnitaryType -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFUnitaryType -> r gmapQ :: (forall d. Data d => d -> u) -> THFUnitaryType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFUnitaryType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFUnitaryType -> m THFUnitaryType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFUnitaryType -> m THFUnitaryType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFUnitaryType -> m THFUnitaryType
Ord THFUnitaryType Source #
Instance details Defined in THF.As Methods compare :: THFUnitaryType -> THFUnitaryType -> Ordering (<) :: THFUnitaryType -> THFUnitaryType -> Bool (<=) :: THFUnitaryType -> THFUnitaryType -> Bool (>) :: THFUnitaryType -> THFUnitaryType -> Bool (>=) :: THFUnitaryType -> THFUnitaryType -> Bool max :: THFUnitaryType -> THFUnitaryType -> THFUnitaryType min :: THFUnitaryType -> THFUnitaryType -> THFUnitaryType
Show THFUnitaryType Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFUnitaryType -> ShowS show :: THFUnitaryType -> String showList :: [THFUnitaryType] -> ShowS
Generic THFUnitaryType
Instance details Defined in THF.ATC_THF Associated Types type Rep THFUnitaryType :: Type -> Type Methods from :: THFUnitaryType -> Rep THFUnitaryType x to :: Rep THFUnitaryType x -> THFUnitaryType
GetRange THFUnitaryType Source #
Instance details Defined in THF.As Methods getRange :: THFUnitaryType -> Range Source # rangeSpan :: THFUnitaryType -> [Pos] Source #
FromJSON THFUnitaryType
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFUnitaryType parseJSONList :: Value -> Parser [THFUnitaryType]
ToJSON THFUnitaryType
Instance details Defined in THF.ATC_THF Methods toJSON :: THFUnitaryType -> Value toEncoding :: THFUnitaryType -> Encoding toJSONList :: [THFUnitaryType] -> Value toEncodingList :: [THFUnitaryType] -> Encoding
ShATermConvertible THFUnitaryType
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFUnitaryType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFUnitaryType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFUnitaryType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFUnitaryType])
Pretty THFUnitaryType Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFUnitaryType -> Doc Source # pretties :: [THFUnitaryType] -> Doc Source #
MinSublogic THFSl THFUnitaryType Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFUnitaryType -> THFSl Source #
type Rep THFUnitaryType
Instance details Defined in THF.ATC_THF type Rep THFUnitaryType = D1 ('MetaData "THFUnitaryType" "THF.As" "main" 'False) ((C1 ('MetaCons "TUT_THF_Unitary_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFUnitaryFormula)) :+: (C1 ('MetaCons "T0UT_Constant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Constant)) :+: C1 ('MetaCons "T0UT_Variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))) :+: (C1 ('MetaCons "T0UT_Defined_Type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefinedType)) :+: (C1 ('MetaCons "T0UT_System_Type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "T0UT_THF_Binary_Type_Par" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFBinaryType)))))

data THFBinaryType Source #

Constructors

TBT_THF_Mapping_Type [THFUnitaryType]
TBT_THF_Xprod_Type [THFUnitaryType]
TBT_THF_Union_Type [THFUnitaryType]
T0BT_THF_Binary_Type_Par THFBinaryType

Instances

Instances details

Eq THFBinaryType Source #
Instance details Defined in THF.As Methods (==) :: THFBinaryType -> THFBinaryType -> Bool (/=) :: THFBinaryType -> THFBinaryType -> Bool
Data THFBinaryType Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFBinaryType -> c THFBinaryType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFBinaryType toConstr :: THFBinaryType -> Constr dataTypeOf :: THFBinaryType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFBinaryType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFBinaryType) gmapT :: (forall b. Data b => b -> b) -> THFBinaryType -> THFBinaryType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFBinaryType -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFBinaryType -> r gmapQ :: (forall d. Data d => d -> u) -> THFBinaryType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFBinaryType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFBinaryType -> m THFBinaryType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFBinaryType -> m THFBinaryType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFBinaryType -> m THFBinaryType
Ord THFBinaryType Source #
Instance details Defined in THF.As Methods compare :: THFBinaryType -> THFBinaryType -> Ordering (<) :: THFBinaryType -> THFBinaryType -> Bool (<=) :: THFBinaryType -> THFBinaryType -> Bool (>) :: THFBinaryType -> THFBinaryType -> Bool (>=) :: THFBinaryType -> THFBinaryType -> Bool max :: THFBinaryType -> THFBinaryType -> THFBinaryType min :: THFBinaryType -> THFBinaryType -> THFBinaryType
Show THFBinaryType Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFBinaryType -> ShowS show :: THFBinaryType -> String showList :: [THFBinaryType] -> ShowS
Generic THFBinaryType
Instance details Defined in THF.ATC_THF Associated Types type Rep THFBinaryType :: Type -> Type Methods from :: THFBinaryType -> Rep THFBinaryType x to :: Rep THFBinaryType x -> THFBinaryType
GetRange THFBinaryType Source #
Instance details Defined in THF.As Methods getRange :: THFBinaryType -> Range Source # rangeSpan :: THFBinaryType -> [Pos] Source #
FromJSON THFBinaryType
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFBinaryType parseJSONList :: Value -> Parser [THFBinaryType]
ToJSON THFBinaryType
Instance details Defined in THF.ATC_THF Methods toJSON :: THFBinaryType -> Value toEncoding :: THFBinaryType -> Encoding toJSONList :: [THFBinaryType] -> Value toEncodingList :: [THFBinaryType] -> Encoding
ShATermConvertible THFBinaryType
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFBinaryType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFBinaryType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFBinaryType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFBinaryType])
Pretty THFBinaryType Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFBinaryType -> Doc Source # pretties :: [THFBinaryType] -> Doc Source #
MinSublogic THFSl THFBinaryType Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFBinaryType -> THFSl Source #
type Rep THFBinaryType
Instance details Defined in THF.ATC_THF type Rep THFBinaryType = D1 ('MetaData "THFBinaryType" "THF.As" "main" 'False) ((C1 ('MetaCons "TBT_THF_Mapping_Type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [THFUnitaryType])) :+: C1 ('MetaCons "TBT_THF_Xprod_Type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [THFUnitaryType]))) :+: (C1 ('MetaCons "TBT_THF_Union_Type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [THFUnitaryType])) :+: C1 ('MetaCons "T0BT_THF_Binary_Type_Par" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFBinaryType))))

data THFAtom Source #

Instances

Instances details

Eq THFAtom Source #
Instance details Defined in THF.As Methods (==) :: THFAtom -> THFAtom -> Bool (/=) :: THFAtom -> THFAtom -> Bool
Data THFAtom Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFAtom -> c THFAtom gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFAtom toConstr :: THFAtom -> Constr dataTypeOf :: THFAtom -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFAtom) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFAtom) gmapT :: (forall b. Data b => b -> b) -> THFAtom -> THFAtom gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFAtom -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFAtom -> r gmapQ :: (forall d. Data d => d -> u) -> THFAtom -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFAtom -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFAtom -> m THFAtom gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFAtom -> m THFAtom gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFAtom -> m THFAtom
Ord THFAtom Source #
Instance details Defined in THF.As Methods compare :: THFAtom -> THFAtom -> Ordering (<) :: THFAtom -> THFAtom -> Bool (<=) :: THFAtom -> THFAtom -> Bool (>) :: THFAtom -> THFAtom -> Bool (>=) :: THFAtom -> THFAtom -> Bool max :: THFAtom -> THFAtom -> THFAtom min :: THFAtom -> THFAtom -> THFAtom
Show THFAtom Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFAtom -> ShowS show :: THFAtom -> String showList :: [THFAtom] -> ShowS
Generic THFAtom
Instance details Defined in THF.ATC_THF Associated Types type Rep THFAtom :: Type -> Type Methods from :: THFAtom -> Rep THFAtom x to :: Rep THFAtom x -> THFAtom
GetRange THFAtom Source #
Instance details Defined in THF.As Methods getRange :: THFAtom -> Range Source # rangeSpan :: THFAtom -> [Pos] Source #
FromJSON THFAtom
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFAtom parseJSONList :: Value -> Parser [THFAtom]
ToJSON THFAtom
Instance details Defined in THF.ATC_THF Methods toJSON :: THFAtom -> Value toEncoding :: THFAtom -> Encoding toJSONList :: [THFAtom] -> Value toEncodingList :: [THFAtom] -> Encoding
ShATermConvertible THFAtom
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFAtom -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFAtom] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFAtom) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFAtom])
Pretty THFAtom Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFAtom -> Doc Source # pretties :: [THFAtom] -> Doc Source #
MinSublogic THFSl THFAtom Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFAtom -> THFSl Source #
type Rep THFAtom
Instance details Defined in THF.ATC_THF type Rep THFAtom = D1 ('MetaData "THFAtom" "THF.As" "main" 'False) (((C1 ('MetaCons "TA_Term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "TA_THF_Conn_Term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFConnTerm))) :+: (C1 ('MetaCons "TA_Defined_Type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefinedType)) :+: (C1 ('MetaCons "TA_Defined_Plain_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefinedPlainFormula)) :+: C1 ('MetaCons "TA_System_Type" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token))))) :+: ((C1 ('MetaCons "TA_System_Atomic_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SystemTerm)) :+: C1 ('MetaCons "T0A_Constant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Constant))) :+: (C1 ('MetaCons "T0A_Defined_Constant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: (C1 ('MetaCons "T0A_System_Constant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "T0A_Variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token))))))

type THFTuple = [THFLogicFormula] Source #

data THFSequent Source #

Constructors

TS_THF_Sequent THFTuple THFTuple
TS_THF_Sequent_Par THFSequent

Instances

Instances details

Eq THFSequent Source #
Instance details Defined in THF.As Methods (==) :: THFSequent -> THFSequent -> Bool (/=) :: THFSequent -> THFSequent -> Bool
Data THFSequent Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFSequent -> c THFSequent gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFSequent toConstr :: THFSequent -> Constr dataTypeOf :: THFSequent -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFSequent) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFSequent) gmapT :: (forall b. Data b => b -> b) -> THFSequent -> THFSequent gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFSequent -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFSequent -> r gmapQ :: (forall d. Data d => d -> u) -> THFSequent -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFSequent -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFSequent -> m THFSequent gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFSequent -> m THFSequent gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFSequent -> m THFSequent
Ord THFSequent Source #
Instance details Defined in THF.As Methods compare :: THFSequent -> THFSequent -> Ordering (<) :: THFSequent -> THFSequent -> Bool (<=) :: THFSequent -> THFSequent -> Bool (>) :: THFSequent -> THFSequent -> Bool (>=) :: THFSequent -> THFSequent -> Bool max :: THFSequent -> THFSequent -> THFSequent min :: THFSequent -> THFSequent -> THFSequent
Show THFSequent Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFSequent -> ShowS show :: THFSequent -> String showList :: [THFSequent] -> ShowS
Generic THFSequent
Instance details Defined in THF.ATC_THF Associated Types type Rep THFSequent :: Type -> Type Methods from :: THFSequent -> Rep THFSequent x to :: Rep THFSequent x -> THFSequent
GetRange THFSequent Source #
Instance details Defined in THF.As Methods getRange :: THFSequent -> Range Source # rangeSpan :: THFSequent -> [Pos] Source #
FromJSON THFSequent
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFSequent parseJSONList :: Value -> Parser [THFSequent]
ToJSON THFSequent
Instance details Defined in THF.ATC_THF Methods toJSON :: THFSequent -> Value toEncoding :: THFSequent -> Encoding toJSONList :: [THFSequent] -> Value toEncodingList :: [THFSequent] -> Encoding
ShATermConvertible THFSequent
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFSequent -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFSequent] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFSequent) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFSequent])
Pretty THFSequent Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFSequent -> Doc Source # pretties :: [THFSequent] -> Doc Source #
MinSublogic THFSl THFSequent Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFSequent -> THFSl Source #
type Rep THFSequent
Instance details Defined in THF.ATC_THF type Rep THFSequent = D1 ('MetaData "THFSequent" "THF.As" "main" 'False) (C1 ('MetaCons "TS_THF_Sequent" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFTuple) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFTuple)) :+: C1 ('MetaCons "TS_THF_Sequent_Par" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFSequent)))

data THFConnTerm Source #

Constructors

TCT_THF_Pair_Connective THFPairConnective
TCT_Assoc_Connective AssocConnective
TCT_THF_Unary_Connective THFUnaryConnective
T0CT_THF_Quantifier THFQuantifier

Instances

Instances details

Eq THFConnTerm Source #
Instance details Defined in THF.As Methods (==) :: THFConnTerm -> THFConnTerm -> Bool (/=) :: THFConnTerm -> THFConnTerm -> Bool
Data THFConnTerm Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFConnTerm -> c THFConnTerm gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFConnTerm toConstr :: THFConnTerm -> Constr dataTypeOf :: THFConnTerm -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFConnTerm) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFConnTerm) gmapT :: (forall b. Data b => b -> b) -> THFConnTerm -> THFConnTerm gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFConnTerm -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFConnTerm -> r gmapQ :: (forall d. Data d => d -> u) -> THFConnTerm -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFConnTerm -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFConnTerm -> m THFConnTerm gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFConnTerm -> m THFConnTerm gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFConnTerm -> m THFConnTerm
Ord THFConnTerm Source #
Instance details Defined in THF.As Methods compare :: THFConnTerm -> THFConnTerm -> Ordering (<) :: THFConnTerm -> THFConnTerm -> Bool (<=) :: THFConnTerm -> THFConnTerm -> Bool (>) :: THFConnTerm -> THFConnTerm -> Bool (>=) :: THFConnTerm -> THFConnTerm -> Bool max :: THFConnTerm -> THFConnTerm -> THFConnTerm min :: THFConnTerm -> THFConnTerm -> THFConnTerm
Show THFConnTerm Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFConnTerm -> ShowS show :: THFConnTerm -> String showList :: [THFConnTerm] -> ShowS
Generic THFConnTerm
Instance details Defined in THF.ATC_THF Associated Types type Rep THFConnTerm :: Type -> Type Methods from :: THFConnTerm -> Rep THFConnTerm x to :: Rep THFConnTerm x -> THFConnTerm
GetRange THFConnTerm Source #
Instance details Defined in THF.As Methods getRange :: THFConnTerm -> Range Source # rangeSpan :: THFConnTerm -> [Pos] Source #
FromJSON THFConnTerm
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFConnTerm parseJSONList :: Value -> Parser [THFConnTerm]
ToJSON THFConnTerm
Instance details Defined in THF.ATC_THF Methods toJSON :: THFConnTerm -> Value toEncoding :: THFConnTerm -> Encoding toJSONList :: [THFConnTerm] -> Value toEncodingList :: [THFConnTerm] -> Encoding
ShATermConvertible THFConnTerm
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFConnTerm -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFConnTerm] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFConnTerm) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFConnTerm])
Pretty THFConnTerm Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFConnTerm -> Doc Source # pretties :: [THFConnTerm] -> Doc Source #
type Rep THFConnTerm
Instance details Defined in THF.ATC_THF type Rep THFConnTerm = D1 ('MetaData "THFConnTerm" "THF.As" "main" 'False) ((C1 ('MetaCons "TCT_THF_Pair_Connective" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFPairConnective)) :+: C1 ('MetaCons "TCT_Assoc_Connective" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AssocConnective))) :+: (C1 ('MetaCons "TCT_THF_Unary_Connective" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFUnaryConnective)) :+: C1 ('MetaCons "T0CT_THF_Quantifier" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFQuantifier))))

data THFQuantifier Source #

Constructors

TQ_ForAll
TQ_Exists
TQ_Lambda_Binder
TQ_Dependent_Product
TQ_Dependent_Sum
TQ_Indefinite_Description
TQ_Definite_Description
T0Q_PiForAll
T0Q_SigmaExists

Instances

Instances details

Eq THFQuantifier Source #
Instance details Defined in THF.As Methods (==) :: THFQuantifier -> THFQuantifier -> Bool (/=) :: THFQuantifier -> THFQuantifier -> Bool
Data THFQuantifier Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFQuantifier -> c THFQuantifier gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFQuantifier toConstr :: THFQuantifier -> Constr dataTypeOf :: THFQuantifier -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFQuantifier) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFQuantifier) gmapT :: (forall b. Data b => b -> b) -> THFQuantifier -> THFQuantifier gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFQuantifier -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFQuantifier -> r gmapQ :: (forall d. Data d => d -> u) -> THFQuantifier -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFQuantifier -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFQuantifier -> m THFQuantifier gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFQuantifier -> m THFQuantifier gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFQuantifier -> m THFQuantifier
Ord THFQuantifier Source #
Instance details Defined in THF.As Methods compare :: THFQuantifier -> THFQuantifier -> Ordering (<) :: THFQuantifier -> THFQuantifier -> Bool (<=) :: THFQuantifier -> THFQuantifier -> Bool (>) :: THFQuantifier -> THFQuantifier -> Bool (>=) :: THFQuantifier -> THFQuantifier -> Bool max :: THFQuantifier -> THFQuantifier -> THFQuantifier min :: THFQuantifier -> THFQuantifier -> THFQuantifier
Show THFQuantifier Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFQuantifier -> ShowS show :: THFQuantifier -> String showList :: [THFQuantifier] -> ShowS
Generic THFQuantifier
Instance details Defined in THF.ATC_THF Associated Types type Rep THFQuantifier :: Type -> Type Methods from :: THFQuantifier -> Rep THFQuantifier x to :: Rep THFQuantifier x -> THFQuantifier
GetRange THFQuantifier Source #
Instance details Defined in THF.As Methods getRange :: THFQuantifier -> Range Source # rangeSpan :: THFQuantifier -> [Pos] Source #
FromJSON THFQuantifier
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFQuantifier parseJSONList :: Value -> Parser [THFQuantifier]
ToJSON THFQuantifier
Instance details Defined in THF.ATC_THF Methods toJSON :: THFQuantifier -> Value toEncoding :: THFQuantifier -> Encoding toJSONList :: [THFQuantifier] -> Value toEncodingList :: [THFQuantifier] -> Encoding
ShATermConvertible THFQuantifier
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFQuantifier -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFQuantifier] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFQuantifier) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFQuantifier])
Pretty THFQuantifier Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFQuantifier -> Doc Source # pretties :: [THFQuantifier] -> Doc Source #
MinSublogic THFSl THFQuantifier Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFQuantifier -> THFSl Source #
type Rep THFQuantifier
Instance details Defined in THF.ATC_THF type Rep THFQuantifier = D1 ('MetaData "THFQuantifier" "THF.As" "main" 'False) (((C1 ('MetaCons "TQ_ForAll" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TQ_Exists" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TQ_Lambda_Binder" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TQ_Dependent_Product" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TQ_Dependent_Sum" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TQ_Indefinite_Description" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TQ_Definite_Description" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "T0Q_PiForAll" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "T0Q_SigmaExists" 'PrefixI 'False) (U1 :: Type -> Type)))))

data Quantifier Source #

Constructors

T0Q_ForAll
T0Q_Exists

Instances

Instances details

Eq Quantifier Source #
Instance details Defined in THF.As Methods (==) :: Quantifier -> Quantifier -> Bool (/=) :: Quantifier -> Quantifier -> Bool
Data Quantifier Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Quantifier -> c Quantifier gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quantifier toConstr :: Quantifier -> Constr dataTypeOf :: Quantifier -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Quantifier) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quantifier) gmapT :: (forall b. Data b => b -> b) -> Quantifier -> Quantifier gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quantifier -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quantifier -> r gmapQ :: (forall d. Data d => d -> u) -> Quantifier -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Quantifier -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quantifier -> m Quantifier gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantifier -> m Quantifier gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quantifier -> m Quantifier
Ord Quantifier Source #
Instance details Defined in THF.As Methods compare :: Quantifier -> Quantifier -> Ordering (<) :: Quantifier -> Quantifier -> Bool (<=) :: Quantifier -> Quantifier -> Bool (>) :: Quantifier -> Quantifier -> Bool (>=) :: Quantifier -> Quantifier -> Bool max :: Quantifier -> Quantifier -> Quantifier min :: Quantifier -> Quantifier -> Quantifier
Show Quantifier Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> Quantifier -> ShowS show :: Quantifier -> String showList :: [Quantifier] -> ShowS
Generic Quantifier
Instance details Defined in THF.ATC_THF Associated Types type Rep Quantifier :: Type -> Type Methods from :: Quantifier -> Rep Quantifier x to :: Rep Quantifier x -> Quantifier
GetRange Quantifier Source #
Instance details Defined in THF.As Methods getRange :: Quantifier -> Range Source # rangeSpan :: Quantifier -> [Pos] Source #
FromJSON Quantifier
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser Quantifier parseJSONList :: Value -> Parser [Quantifier]
ToJSON Quantifier
Instance details Defined in THF.ATC_THF Methods toJSON :: Quantifier -> Value toEncoding :: Quantifier -> Encoding toJSONList :: [Quantifier] -> Value toEncodingList :: [Quantifier] -> Encoding
ShATermConvertible Quantifier
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> Quantifier -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Quantifier] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Quantifier) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Quantifier])
Pretty Quantifier Source #
Instance details Defined in THF.PrintTHF Methods pretty :: Quantifier -> Doc Source # pretties :: [Quantifier] -> Doc Source #
MinSublogic THFSl Quantifier Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: Quantifier -> THFSl Source #
type Rep Quantifier
Instance details Defined in THF.ATC_THF type Rep Quantifier = D1 ('MetaData "Quantifier" "THF.As" "main" 'False) (C1 ('MetaCons "T0Q_ForAll" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "T0Q_Exists" 'PrefixI 'False) (U1 :: Type -> Type))

data THFPairConnective Source #

Constructors

Infix_Equality
Infix_Inequality
Equivalent
Implication
IF
XOR
NOR
NAND

Instances

Instances details

Eq THFPairConnective Source #
Instance details Defined in THF.As Methods (==) :: THFPairConnective -> THFPairConnective -> Bool (/=) :: THFPairConnective -> THFPairConnective -> Bool
Data THFPairConnective Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFPairConnective -> c THFPairConnective gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFPairConnective toConstr :: THFPairConnective -> Constr dataTypeOf :: THFPairConnective -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFPairConnective) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFPairConnective) gmapT :: (forall b. Data b => b -> b) -> THFPairConnective -> THFPairConnective gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFPairConnective -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFPairConnective -> r gmapQ :: (forall d. Data d => d -> u) -> THFPairConnective -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFPairConnective -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFPairConnective -> m THFPairConnective gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFPairConnective -> m THFPairConnective gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFPairConnective -> m THFPairConnective
Ord THFPairConnective Source #
Instance details Defined in THF.As Methods compare :: THFPairConnective -> THFPairConnective -> Ordering (<) :: THFPairConnective -> THFPairConnective -> Bool (<=) :: THFPairConnective -> THFPairConnective -> Bool (>) :: THFPairConnective -> THFPairConnective -> Bool (>=) :: THFPairConnective -> THFPairConnective -> Bool max :: THFPairConnective -> THFPairConnective -> THFPairConnective min :: THFPairConnective -> THFPairConnective -> THFPairConnective
Show THFPairConnective Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFPairConnective -> ShowS show :: THFPairConnective -> String showList :: [THFPairConnective] -> ShowS
Generic THFPairConnective
Instance details Defined in THF.ATC_THF Associated Types type Rep THFPairConnective :: Type -> Type Methods from :: THFPairConnective -> Rep THFPairConnective x to :: Rep THFPairConnective x -> THFPairConnective
GetRange THFPairConnective Source #
Instance details Defined in THF.As Methods getRange :: THFPairConnective -> Range Source # rangeSpan :: THFPairConnective -> [Pos] Source #
FromJSON THFPairConnective
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFPairConnective parseJSONList :: Value -> Parser [THFPairConnective]
ToJSON THFPairConnective
Instance details Defined in THF.ATC_THF Methods toJSON :: THFPairConnective -> Value toEncoding :: THFPairConnective -> Encoding toJSONList :: [THFPairConnective] -> Value toEncodingList :: [THFPairConnective] -> Encoding
ShATermConvertible THFPairConnective
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFPairConnective -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFPairConnective] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFPairConnective) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFPairConnective])
Pretty THFPairConnective Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFPairConnective -> Doc Source # pretties :: [THFPairConnective] -> Doc Source #
MinSublogic THFSl THFPairConnective Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFPairConnective -> THFSl Source #
type Rep THFPairConnective
Instance details Defined in THF.ATC_THF type Rep THFPairConnective = D1 ('MetaData "THFPairConnective" "THF.As" "main" 'False) (((C1 ('MetaCons "Infix_Equality" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Infix_Inequality" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Equivalent" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Implication" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "IF" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "XOR" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NOR" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NAND" 'PrefixI 'False) (U1 :: Type -> Type))))

data THFUnaryConnective Source #

Constructors

Negation
PiForAll
SigmaExists

Instances

Instances details

Eq THFUnaryConnective Source #
Instance details Defined in THF.As Methods (==) :: THFUnaryConnective -> THFUnaryConnective -> Bool (/=) :: THFUnaryConnective -> THFUnaryConnective -> Bool
Data THFUnaryConnective Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> THFUnaryConnective -> c THFUnaryConnective gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c THFUnaryConnective toConstr :: THFUnaryConnective -> Constr dataTypeOf :: THFUnaryConnective -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c THFUnaryConnective) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c THFUnaryConnective) gmapT :: (forall b. Data b => b -> b) -> THFUnaryConnective -> THFUnaryConnective gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> THFUnaryConnective -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> THFUnaryConnective -> r gmapQ :: (forall d. Data d => d -> u) -> THFUnaryConnective -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> THFUnaryConnective -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> THFUnaryConnective -> m THFUnaryConnective gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> THFUnaryConnective -> m THFUnaryConnective gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> THFUnaryConnective -> m THFUnaryConnective
Ord THFUnaryConnective Source #
Instance details Defined in THF.As Methods compare :: THFUnaryConnective -> THFUnaryConnective -> Ordering (<) :: THFUnaryConnective -> THFUnaryConnective -> Bool (<=) :: THFUnaryConnective -> THFUnaryConnective -> Bool (>) :: THFUnaryConnective -> THFUnaryConnective -> Bool (>=) :: THFUnaryConnective -> THFUnaryConnective -> Bool max :: THFUnaryConnective -> THFUnaryConnective -> THFUnaryConnective min :: THFUnaryConnective -> THFUnaryConnective -> THFUnaryConnective
Show THFUnaryConnective Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> THFUnaryConnective -> ShowS show :: THFUnaryConnective -> String showList :: [THFUnaryConnective] -> ShowS
Generic THFUnaryConnective
Instance details Defined in THF.ATC_THF Associated Types type Rep THFUnaryConnective :: Type -> Type Methods from :: THFUnaryConnective -> Rep THFUnaryConnective x to :: Rep THFUnaryConnective x -> THFUnaryConnective
GetRange THFUnaryConnective Source #
Instance details Defined in THF.As Methods getRange :: THFUnaryConnective -> Range Source # rangeSpan :: THFUnaryConnective -> [Pos] Source #
FromJSON THFUnaryConnective
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser THFUnaryConnective parseJSONList :: Value -> Parser [THFUnaryConnective]
ToJSON THFUnaryConnective
Instance details Defined in THF.ATC_THF Methods toJSON :: THFUnaryConnective -> Value toEncoding :: THFUnaryConnective -> Encoding toJSONList :: [THFUnaryConnective] -> Value toEncodingList :: [THFUnaryConnective] -> Encoding
ShATermConvertible THFUnaryConnective
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> THFUnaryConnective -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [THFUnaryConnective] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, THFUnaryConnective) fromShATermList' :: Int -> ATermTable -> (ATermTable, [THFUnaryConnective])
Pretty THFUnaryConnective Source #
Instance details Defined in THF.PrintTHF Methods pretty :: THFUnaryConnective -> Doc Source # pretties :: [THFUnaryConnective] -> Doc Source #
MinSublogic THFSl THFUnaryConnective Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: THFUnaryConnective -> THFSl Source #
type Rep THFUnaryConnective
Instance details Defined in THF.ATC_THF type Rep THFUnaryConnective = D1 ('MetaData "THFUnaryConnective" "THF.As" "main" 'False) (C1 ('MetaCons "Negation" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PiForAll" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SigmaExists" 'PrefixI 'False) (U1 :: Type -> Type)))

data AssocConnective Source #

Constructors

OR
AND

Instances

Instances details

Eq AssocConnective Source #
Instance details Defined in THF.As Methods (==) :: AssocConnective -> AssocConnective -> Bool (/=) :: AssocConnective -> AssocConnective -> Bool
Data AssocConnective Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AssocConnective -> c AssocConnective gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AssocConnective toConstr :: AssocConnective -> Constr dataTypeOf :: AssocConnective -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AssocConnective) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AssocConnective) gmapT :: (forall b. Data b => b -> b) -> AssocConnective -> AssocConnective gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AssocConnective -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AssocConnective -> r gmapQ :: (forall d. Data d => d -> u) -> AssocConnective -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> AssocConnective -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> AssocConnective -> m AssocConnective gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AssocConnective -> m AssocConnective gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AssocConnective -> m AssocConnective
Ord AssocConnective Source #
Instance details Defined in THF.As Methods compare :: AssocConnective -> AssocConnective -> Ordering (<) :: AssocConnective -> AssocConnective -> Bool (<=) :: AssocConnective -> AssocConnective -> Bool (>) :: AssocConnective -> AssocConnective -> Bool (>=) :: AssocConnective -> AssocConnective -> Bool max :: AssocConnective -> AssocConnective -> AssocConnective min :: AssocConnective -> AssocConnective -> AssocConnective
Show AssocConnective Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> AssocConnective -> ShowS show :: AssocConnective -> String showList :: [AssocConnective] -> ShowS
Generic AssocConnective
Instance details Defined in THF.ATC_THF Associated Types type Rep AssocConnective :: Type -> Type Methods from :: AssocConnective -> Rep AssocConnective x to :: Rep AssocConnective x -> AssocConnective
GetRange AssocConnective Source #
Instance details Defined in THF.As Methods getRange :: AssocConnective -> Range Source # rangeSpan :: AssocConnective -> [Pos] Source #
FromJSON AssocConnective
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser AssocConnective parseJSONList :: Value -> Parser [AssocConnective]
ToJSON AssocConnective
Instance details Defined in THF.ATC_THF Methods toJSON :: AssocConnective -> Value toEncoding :: AssocConnective -> Encoding toJSONList :: [AssocConnective] -> Value toEncodingList :: [AssocConnective] -> Encoding
ShATermConvertible AssocConnective
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> AssocConnective -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [AssocConnective] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, AssocConnective) fromShATermList' :: Int -> ATermTable -> (ATermTable, [AssocConnective])
Pretty AssocConnective Source #
Instance details Defined in THF.PrintTHF Methods pretty :: AssocConnective -> Doc Source # pretties :: [AssocConnective] -> Doc Source #
type Rep AssocConnective
Instance details Defined in THF.ATC_THF type Rep AssocConnective = D1 ('MetaData "AssocConnective" "THF.As" "main" 'False) (C1 ('MetaCons "OR" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AND" 'PrefixI 'False) (U1 :: Type -> Type))

data DefinedType Source #

Constructors

DT_oType
DT_o
DT_iType
DT_i
DT_tType
DT_real
DT_rat
DT_int

Instances

Instances details

Eq DefinedType Source #
Instance details Defined in THF.As Methods (==) :: DefinedType -> DefinedType -> Bool (/=) :: DefinedType -> DefinedType -> Bool
Data DefinedType Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefinedType -> c DefinedType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefinedType toConstr :: DefinedType -> Constr dataTypeOf :: DefinedType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefinedType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefinedType) gmapT :: (forall b. Data b => b -> b) -> DefinedType -> DefinedType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefinedType -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefinedType -> r gmapQ :: (forall d. Data d => d -> u) -> DefinedType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DefinedType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefinedType -> m DefinedType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedType -> m DefinedType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedType -> m DefinedType
Ord DefinedType Source #
Instance details Defined in THF.As Methods compare :: DefinedType -> DefinedType -> Ordering (<) :: DefinedType -> DefinedType -> Bool (<=) :: DefinedType -> DefinedType -> Bool (>) :: DefinedType -> DefinedType -> Bool (>=) :: DefinedType -> DefinedType -> Bool max :: DefinedType -> DefinedType -> DefinedType min :: DefinedType -> DefinedType -> DefinedType
Show DefinedType Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> DefinedType -> ShowS show :: DefinedType -> String showList :: [DefinedType] -> ShowS
Generic DefinedType
Instance details Defined in THF.ATC_THF Associated Types type Rep DefinedType :: Type -> Type Methods from :: DefinedType -> Rep DefinedType x to :: Rep DefinedType x -> DefinedType
GetRange DefinedType Source #
Instance details Defined in THF.As Methods getRange :: DefinedType -> Range Source # rangeSpan :: DefinedType -> [Pos] Source #
FromJSON DefinedType
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser DefinedType parseJSONList :: Value -> Parser [DefinedType]
ToJSON DefinedType
Instance details Defined in THF.ATC_THF Methods toJSON :: DefinedType -> Value toEncoding :: DefinedType -> Encoding toJSONList :: [DefinedType] -> Value toEncodingList :: [DefinedType] -> Encoding
ShATermConvertible DefinedType
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> DefinedType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DefinedType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DefinedType])
Pretty DefinedType Source #
Instance details Defined in THF.PrintTHF Methods pretty :: DefinedType -> Doc Source # pretties :: [DefinedType] -> Doc Source #
MinSublogic THFSl DefinedType Source #
Instance details Defined in THF.Sublogic Methods minSublogic :: DefinedType -> THFSl Source #
type Rep DefinedType
Instance details Defined in THF.ATC_THF type Rep DefinedType = D1 ('MetaData "DefinedType" "THF.As" "main" 'False) (((C1 ('MetaCons "DT_oType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DT_o" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DT_iType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DT_i" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "DT_tType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DT_real" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DT_rat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DT_int" 'PrefixI 'False) (U1 :: Type -> Type))))

data DefinedPlainFormula Source #

Constructors

DPF_Defined_Prop DefinedProp
DPF_Defined_Formula DefinedPred Arguments

Instances

Instances details

Eq DefinedPlainFormula Source #
Instance details Defined in THF.As Methods (==) :: DefinedPlainFormula -> DefinedPlainFormula -> Bool (/=) :: DefinedPlainFormula -> DefinedPlainFormula -> Bool
Data DefinedPlainFormula Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefinedPlainFormula -> c DefinedPlainFormula gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefinedPlainFormula toConstr :: DefinedPlainFormula -> Constr dataTypeOf :: DefinedPlainFormula -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefinedPlainFormula) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefinedPlainFormula) gmapT :: (forall b. Data b => b -> b) -> DefinedPlainFormula -> DefinedPlainFormula gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefinedPlainFormula -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefinedPlainFormula -> r gmapQ :: (forall d. Data d => d -> u) -> DefinedPlainFormula -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DefinedPlainFormula -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefinedPlainFormula -> m DefinedPlainFormula gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedPlainFormula -> m DefinedPlainFormula gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedPlainFormula -> m DefinedPlainFormula
Ord DefinedPlainFormula Source #
Instance details Defined in THF.As Methods compare :: DefinedPlainFormula -> DefinedPlainFormula -> Ordering (<) :: DefinedPlainFormula -> DefinedPlainFormula -> Bool (<=) :: DefinedPlainFormula -> DefinedPlainFormula -> Bool (>) :: DefinedPlainFormula -> DefinedPlainFormula -> Bool (>=) :: DefinedPlainFormula -> DefinedPlainFormula -> Bool max :: DefinedPlainFormula -> DefinedPlainFormula -> DefinedPlainFormula min :: DefinedPlainFormula -> DefinedPlainFormula -> DefinedPlainFormula
Show DefinedPlainFormula Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> DefinedPlainFormula -> ShowS show :: DefinedPlainFormula -> String showList :: [DefinedPlainFormula] -> ShowS
Generic DefinedPlainFormula
Instance details Defined in THF.ATC_THF Associated Types type Rep DefinedPlainFormula :: Type -> Type Methods from :: DefinedPlainFormula -> Rep DefinedPlainFormula x to :: Rep DefinedPlainFormula x -> DefinedPlainFormula
GetRange DefinedPlainFormula Source #
Instance details Defined in THF.As Methods getRange :: DefinedPlainFormula -> Range Source # rangeSpan :: DefinedPlainFormula -> [Pos] Source #
FromJSON DefinedPlainFormula
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser DefinedPlainFormula parseJSONList :: Value -> Parser [DefinedPlainFormula]
ToJSON DefinedPlainFormula
Instance details Defined in THF.ATC_THF Methods toJSON :: DefinedPlainFormula -> Value toEncoding :: DefinedPlainFormula -> Encoding toJSONList :: [DefinedPlainFormula] -> Value toEncodingList :: [DefinedPlainFormula] -> Encoding
ShATermConvertible DefinedPlainFormula
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> DefinedPlainFormula -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DefinedPlainFormula] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedPlainFormula) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DefinedPlainFormula])
Pretty DefinedPlainFormula Source #
Instance details Defined in THF.PrintTHF Methods pretty :: DefinedPlainFormula -> Doc Source # pretties :: [DefinedPlainFormula] -> Doc Source #
type Rep DefinedPlainFormula
Instance details Defined in THF.ATC_THF type Rep DefinedPlainFormula = D1 ('MetaData "DefinedPlainFormula" "THF.As" "main" 'False) (C1 ('MetaCons "DPF_Defined_Prop" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefinedProp)) :+: C1 ('MetaCons "DPF_Defined_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefinedPred) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Arguments)))

data DefinedProp Source #

Constructors

DP_True
DP_False

Instances

Instances details

Eq DefinedProp Source #
Instance details Defined in THF.As Methods (==) :: DefinedProp -> DefinedProp -> Bool (/=) :: DefinedProp -> DefinedProp -> Bool
Data DefinedProp Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefinedProp -> c DefinedProp gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefinedProp toConstr :: DefinedProp -> Constr dataTypeOf :: DefinedProp -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefinedProp) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefinedProp) gmapT :: (forall b. Data b => b -> b) -> DefinedProp -> DefinedProp gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefinedProp -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefinedProp -> r gmapQ :: (forall d. Data d => d -> u) -> DefinedProp -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DefinedProp -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefinedProp -> m DefinedProp gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedProp -> m DefinedProp gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedProp -> m DefinedProp
Ord DefinedProp Source #
Instance details Defined in THF.As Methods compare :: DefinedProp -> DefinedProp -> Ordering (<) :: DefinedProp -> DefinedProp -> Bool (<=) :: DefinedProp -> DefinedProp -> Bool (>) :: DefinedProp -> DefinedProp -> Bool (>=) :: DefinedProp -> DefinedProp -> Bool max :: DefinedProp -> DefinedProp -> DefinedProp min :: DefinedProp -> DefinedProp -> DefinedProp
Show DefinedProp Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> DefinedProp -> ShowS show :: DefinedProp -> String showList :: [DefinedProp] -> ShowS
Generic DefinedProp
Instance details Defined in THF.ATC_THF Associated Types type Rep DefinedProp :: Type -> Type Methods from :: DefinedProp -> Rep DefinedProp x to :: Rep DefinedProp x -> DefinedProp
GetRange DefinedProp Source #
Instance details Defined in THF.As Methods getRange :: DefinedProp -> Range Source # rangeSpan :: DefinedProp -> [Pos] Source #
FromJSON DefinedProp
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser DefinedProp parseJSONList :: Value -> Parser [DefinedProp]
ToJSON DefinedProp
Instance details Defined in THF.ATC_THF Methods toJSON :: DefinedProp -> Value toEncoding :: DefinedProp -> Encoding toJSONList :: [DefinedProp] -> Value toEncodingList :: [DefinedProp] -> Encoding
ShATermConvertible DefinedProp
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> DefinedProp -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DefinedProp] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedProp) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DefinedProp])
Pretty DefinedProp Source #
Instance details Defined in THF.PrintTHF Methods pretty :: DefinedProp -> Doc Source # pretties :: [DefinedProp] -> Doc Source #
type Rep DefinedProp
Instance details Defined in THF.ATC_THF type Rep DefinedProp = D1 ('MetaData "DefinedProp" "THF.As" "main" 'False) (C1 ('MetaCons "DP_True" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "DP_False" 'PrefixI 'False) (U1 :: Type -> Type))

data DefinedPred Source #

Constructors

Disrinct
Less
Lesseq
Greater
Greatereq
Is_int
Is_rat

Instances

Instances details

Eq DefinedPred Source #
Instance details Defined in THF.As Methods (==) :: DefinedPred -> DefinedPred -> Bool (/=) :: DefinedPred -> DefinedPred -> Bool
Data DefinedPred Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefinedPred -> c DefinedPred gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefinedPred toConstr :: DefinedPred -> Constr dataTypeOf :: DefinedPred -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefinedPred) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefinedPred) gmapT :: (forall b. Data b => b -> b) -> DefinedPred -> DefinedPred gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefinedPred -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefinedPred -> r gmapQ :: (forall d. Data d => d -> u) -> DefinedPred -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DefinedPred -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefinedPred -> m DefinedPred gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedPred -> m DefinedPred gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedPred -> m DefinedPred
Ord DefinedPred Source #
Instance details Defined in THF.As Methods compare :: DefinedPred -> DefinedPred -> Ordering (<) :: DefinedPred -> DefinedPred -> Bool (<=) :: DefinedPred -> DefinedPred -> Bool (>) :: DefinedPred -> DefinedPred -> Bool (>=) :: DefinedPred -> DefinedPred -> Bool max :: DefinedPred -> DefinedPred -> DefinedPred min :: DefinedPred -> DefinedPred -> DefinedPred
Show DefinedPred Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> DefinedPred -> ShowS show :: DefinedPred -> String showList :: [DefinedPred] -> ShowS
Generic DefinedPred
Instance details Defined in THF.ATC_THF Associated Types type Rep DefinedPred :: Type -> Type Methods from :: DefinedPred -> Rep DefinedPred x to :: Rep DefinedPred x -> DefinedPred
GetRange DefinedPred Source #
Instance details Defined in THF.As Methods getRange :: DefinedPred -> Range Source # rangeSpan :: DefinedPred -> [Pos] Source #
FromJSON DefinedPred
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser DefinedPred parseJSONList :: Value -> Parser [DefinedPred]
ToJSON DefinedPred
Instance details Defined in THF.ATC_THF Methods toJSON :: DefinedPred -> Value toEncoding :: DefinedPred -> Encoding toJSONList :: [DefinedPred] -> Value toEncodingList :: [DefinedPred] -> Encoding
ShATermConvertible DefinedPred
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> DefinedPred -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DefinedPred] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedPred) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DefinedPred])
Pretty DefinedPred Source #
Instance details Defined in THF.PrintTHF Methods pretty :: DefinedPred -> Doc Source # pretties :: [DefinedPred] -> Doc Source #
type Rep DefinedPred
Instance details Defined in THF.ATC_THF type Rep DefinedPred = D1 ('MetaData "DefinedPred" "THF.As" "main" 'False) ((C1 ('MetaCons "Disrinct" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Less" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Lesseq" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Greater" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Greatereq" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Is_int" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Is_rat" 'PrefixI 'False) (U1 :: Type -> Type))))

data Term Source #

Constructors

T_Function_Term FunctionTerm
T_Variable Token

Instances

Instances details

Eq Term Source #
Instance details Defined in THF.As Methods (==) :: Term -> Term -> Bool (/=) :: Term -> Term -> Bool
Data Term Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term toConstr :: Term -> Constr dataTypeOf :: Term -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Term) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term) gmapT :: (forall b. Data b => b -> b) -> Term -> Term gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r gmapQ :: (forall d. Data d => d -> u) -> Term -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term
Ord Term Source #
Instance details Defined in THF.As Methods compare :: Term -> Term -> Ordering (<) :: Term -> Term -> Bool (<=) :: Term -> Term -> Bool (>) :: Term -> Term -> Bool (>=) :: Term -> Term -> Bool max :: Term -> Term -> Term min :: Term -> Term -> Term
Show Term Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> Term -> ShowS show :: Term -> String showList :: [Term] -> ShowS
Generic Term
Instance details Defined in THF.ATC_THF Associated Types type Rep Term :: Type -> Type Methods from :: Term -> Rep Term x to :: Rep Term x -> Term
GetRange Term Source #
Instance details Defined in THF.As Methods getRange :: Term -> Range Source # rangeSpan :: Term -> [Pos] Source #
FromJSON Term
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser Term parseJSONList :: Value -> Parser [Term]
ToJSON Term
Instance details Defined in THF.ATC_THF Methods toJSON :: Term -> Value toEncoding :: Term -> Encoding toJSONList :: [Term] -> Value toEncodingList :: [Term] -> Encoding
ShATermConvertible Term
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> Term -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Term] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Term) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Term])
Pretty Term Source #
Instance details Defined in THF.PrintTHF Methods pretty :: Term -> Doc Source # pretties :: [Term] -> Doc Source #
type Rep Term
Instance details Defined in THF.ATC_THF type Rep Term = D1 ('MetaData "Term" "THF.As" "main" 'False) (C1 ('MetaCons "T_Function_Term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FunctionTerm)) :+: C1 ('MetaCons "T_Variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data FunctionTerm Source #

Constructors

FT_Plain_Term PlainTerm
FT_Defined_Term DefinedTerm
FT_System_Term SystemTerm

Instances

Instances details

Eq FunctionTerm Source #
Instance details Defined in THF.As Methods (==) :: FunctionTerm -> FunctionTerm -> Bool (/=) :: FunctionTerm -> FunctionTerm -> Bool
Data FunctionTerm Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunctionTerm -> c FunctionTerm gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunctionTerm toConstr :: FunctionTerm -> Constr dataTypeOf :: FunctionTerm -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FunctionTerm) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunctionTerm) gmapT :: (forall b. Data b => b -> b) -> FunctionTerm -> FunctionTerm gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunctionTerm -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunctionTerm -> r gmapQ :: (forall d. Data d => d -> u) -> FunctionTerm -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FunctionTerm -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunctionTerm -> m FunctionTerm gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionTerm -> m FunctionTerm gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionTerm -> m FunctionTerm
Ord FunctionTerm Source #
Instance details Defined in THF.As Methods compare :: FunctionTerm -> FunctionTerm -> Ordering (<) :: FunctionTerm -> FunctionTerm -> Bool (<=) :: FunctionTerm -> FunctionTerm -> Bool (>) :: FunctionTerm -> FunctionTerm -> Bool (>=) :: FunctionTerm -> FunctionTerm -> Bool max :: FunctionTerm -> FunctionTerm -> FunctionTerm min :: FunctionTerm -> FunctionTerm -> FunctionTerm
Show FunctionTerm Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> FunctionTerm -> ShowS show :: FunctionTerm -> String showList :: [FunctionTerm] -> ShowS
Generic FunctionTerm
Instance details Defined in THF.ATC_THF Associated Types type Rep FunctionTerm :: Type -> Type Methods from :: FunctionTerm -> Rep FunctionTerm x to :: Rep FunctionTerm x -> FunctionTerm
GetRange FunctionTerm Source #
Instance details Defined in THF.As Methods getRange :: FunctionTerm -> Range Source # rangeSpan :: FunctionTerm -> [Pos] Source #
FromJSON FunctionTerm
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser FunctionTerm parseJSONList :: Value -> Parser [FunctionTerm]
ToJSON FunctionTerm
Instance details Defined in THF.ATC_THF Methods toJSON :: FunctionTerm -> Value toEncoding :: FunctionTerm -> Encoding toJSONList :: [FunctionTerm] -> Value toEncodingList :: [FunctionTerm] -> Encoding
ShATermConvertible FunctionTerm
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> FunctionTerm -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FunctionTerm] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FunctionTerm) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FunctionTerm])
Pretty FunctionTerm Source #
Instance details Defined in THF.PrintTHF Methods pretty :: FunctionTerm -> Doc Source # pretties :: [FunctionTerm] -> Doc Source #
type Rep FunctionTerm
Instance details Defined in THF.ATC_THF type Rep FunctionTerm = D1 ('MetaData "FunctionTerm" "THF.As" "main" 'False) (C1 ('MetaCons "FT_Plain_Term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PlainTerm)) :+: (C1 ('MetaCons "FT_Defined_Term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefinedTerm)) :+: C1 ('MetaCons "FT_System_Term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SystemTerm))))

data PlainTerm Source #

Constructors

PT_Plain_Term AtomicWord Arguments
PT_Constant Constant

Instances

Instances details

Eq PlainTerm Source #
Instance details Defined in THF.As Methods (==) :: PlainTerm -> PlainTerm -> Bool (/=) :: PlainTerm -> PlainTerm -> Bool
Data PlainTerm Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PlainTerm -> c PlainTerm gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PlainTerm toConstr :: PlainTerm -> Constr dataTypeOf :: PlainTerm -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PlainTerm) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PlainTerm) gmapT :: (forall b. Data b => b -> b) -> PlainTerm -> PlainTerm gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PlainTerm -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PlainTerm -> r gmapQ :: (forall d. Data d => d -> u) -> PlainTerm -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PlainTerm -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PlainTerm -> m PlainTerm gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PlainTerm -> m PlainTerm gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PlainTerm -> m PlainTerm
Ord PlainTerm Source #
Instance details Defined in THF.As Methods compare :: PlainTerm -> PlainTerm -> Ordering (<) :: PlainTerm -> PlainTerm -> Bool (<=) :: PlainTerm -> PlainTerm -> Bool (>) :: PlainTerm -> PlainTerm -> Bool (>=) :: PlainTerm -> PlainTerm -> Bool max :: PlainTerm -> PlainTerm -> PlainTerm min :: PlainTerm -> PlainTerm -> PlainTerm
Show PlainTerm Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> PlainTerm -> ShowS show :: PlainTerm -> String showList :: [PlainTerm] -> ShowS
Generic PlainTerm
Instance details Defined in THF.ATC_THF Associated Types type Rep PlainTerm :: Type -> Type Methods from :: PlainTerm -> Rep PlainTerm x to :: Rep PlainTerm x -> PlainTerm
GetRange PlainTerm Source #
Instance details Defined in THF.As Methods getRange :: PlainTerm -> Range Source # rangeSpan :: PlainTerm -> [Pos] Source #
FromJSON PlainTerm
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser PlainTerm parseJSONList :: Value -> Parser [PlainTerm]
ToJSON PlainTerm
Instance details Defined in THF.ATC_THF Methods toJSON :: PlainTerm -> Value toEncoding :: PlainTerm -> Encoding toJSONList :: [PlainTerm] -> Value toEncodingList :: [PlainTerm] -> Encoding
ShATermConvertible PlainTerm
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> PlainTerm -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [PlainTerm] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, PlainTerm) fromShATermList' :: Int -> ATermTable -> (ATermTable, [PlainTerm])
Pretty PlainTerm Source #
Instance details Defined in THF.PrintTHF Methods pretty :: PlainTerm -> Doc Source # pretties :: [PlainTerm] -> Doc Source #
type Rep PlainTerm
Instance details Defined in THF.ATC_THF type Rep PlainTerm = D1 ('MetaData "PlainTerm" "THF.As" "main" 'False) (C1 ('MetaCons "PT_Plain_Term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AtomicWord) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Arguments)) :+: C1 ('MetaCons "PT_Constant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Constant)))

type Constant = AtomicWord Source #

data DefinedTerm Source #

Constructors

DT_Defined_Atom DefinedAtom
DT_Defined_Atomic_Term DefinedPlainTerm

Instances

Instances details

Eq DefinedTerm Source #
Instance details Defined in THF.As Methods (==) :: DefinedTerm -> DefinedTerm -> Bool (/=) :: DefinedTerm -> DefinedTerm -> Bool
Data DefinedTerm Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefinedTerm -> c DefinedTerm gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefinedTerm toConstr :: DefinedTerm -> Constr dataTypeOf :: DefinedTerm -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefinedTerm) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefinedTerm) gmapT :: (forall b. Data b => b -> b) -> DefinedTerm -> DefinedTerm gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefinedTerm -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefinedTerm -> r gmapQ :: (forall d. Data d => d -> u) -> DefinedTerm -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DefinedTerm -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefinedTerm -> m DefinedTerm gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedTerm -> m DefinedTerm gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedTerm -> m DefinedTerm
Ord DefinedTerm Source #
Instance details Defined in THF.As Methods compare :: DefinedTerm -> DefinedTerm -> Ordering (<) :: DefinedTerm -> DefinedTerm -> Bool (<=) :: DefinedTerm -> DefinedTerm -> Bool (>) :: DefinedTerm -> DefinedTerm -> Bool (>=) :: DefinedTerm -> DefinedTerm -> Bool max :: DefinedTerm -> DefinedTerm -> DefinedTerm min :: DefinedTerm -> DefinedTerm -> DefinedTerm
Show DefinedTerm Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> DefinedTerm -> ShowS show :: DefinedTerm -> String showList :: [DefinedTerm] -> ShowS
Generic DefinedTerm
Instance details Defined in THF.ATC_THF Associated Types type Rep DefinedTerm :: Type -> Type Methods from :: DefinedTerm -> Rep DefinedTerm x to :: Rep DefinedTerm x -> DefinedTerm
GetRange DefinedTerm Source #
Instance details Defined in THF.As Methods getRange :: DefinedTerm -> Range Source # rangeSpan :: DefinedTerm -> [Pos] Source #
FromJSON DefinedTerm
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser DefinedTerm parseJSONList :: Value -> Parser [DefinedTerm]
ToJSON DefinedTerm
Instance details Defined in THF.ATC_THF Methods toJSON :: DefinedTerm -> Value toEncoding :: DefinedTerm -> Encoding toJSONList :: [DefinedTerm] -> Value toEncodingList :: [DefinedTerm] -> Encoding
ShATermConvertible DefinedTerm
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> DefinedTerm -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DefinedTerm] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedTerm) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DefinedTerm])
Pretty DefinedTerm Source #
Instance details Defined in THF.PrintTHF Methods pretty :: DefinedTerm -> Doc Source # pretties :: [DefinedTerm] -> Doc Source #
type Rep DefinedTerm
Instance details Defined in THF.ATC_THF type Rep DefinedTerm = D1 ('MetaData "DefinedTerm" "THF.As" "main" 'False) (C1 ('MetaCons "DT_Defined_Atom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefinedAtom)) :+: C1 ('MetaCons "DT_Defined_Atomic_Term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefinedPlainTerm)))

data DefinedAtom Source #

Constructors

DA_Number Number
DA_Distinct_Object Token

Instances

Instances details

Eq DefinedAtom Source #
Instance details Defined in THF.As Methods (==) :: DefinedAtom -> DefinedAtom -> Bool (/=) :: DefinedAtom -> DefinedAtom -> Bool
Data DefinedAtom Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefinedAtom -> c DefinedAtom gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefinedAtom toConstr :: DefinedAtom -> Constr dataTypeOf :: DefinedAtom -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefinedAtom) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefinedAtom) gmapT :: (forall b. Data b => b -> b) -> DefinedAtom -> DefinedAtom gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefinedAtom -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefinedAtom -> r gmapQ :: (forall d. Data d => d -> u) -> DefinedAtom -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DefinedAtom -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefinedAtom -> m DefinedAtom gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedAtom -> m DefinedAtom gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedAtom -> m DefinedAtom
Ord DefinedAtom Source #
Instance details Defined in THF.As Methods compare :: DefinedAtom -> DefinedAtom -> Ordering (<) :: DefinedAtom -> DefinedAtom -> Bool (<=) :: DefinedAtom -> DefinedAtom -> Bool (>) :: DefinedAtom -> DefinedAtom -> Bool (>=) :: DefinedAtom -> DefinedAtom -> Bool max :: DefinedAtom -> DefinedAtom -> DefinedAtom min :: DefinedAtom -> DefinedAtom -> DefinedAtom
Show DefinedAtom Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> DefinedAtom -> ShowS show :: DefinedAtom -> String showList :: [DefinedAtom] -> ShowS
Generic DefinedAtom
Instance details Defined in THF.ATC_THF Associated Types type Rep DefinedAtom :: Type -> Type Methods from :: DefinedAtom -> Rep DefinedAtom x to :: Rep DefinedAtom x -> DefinedAtom
GetRange DefinedAtom Source #
Instance details Defined in THF.As Methods getRange :: DefinedAtom -> Range Source # rangeSpan :: DefinedAtom -> [Pos] Source #
FromJSON DefinedAtom
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser DefinedAtom parseJSONList :: Value -> Parser [DefinedAtom]
ToJSON DefinedAtom
Instance details Defined in THF.ATC_THF Methods toJSON :: DefinedAtom -> Value toEncoding :: DefinedAtom -> Encoding toJSONList :: [DefinedAtom] -> Value toEncodingList :: [DefinedAtom] -> Encoding
ShATermConvertible DefinedAtom
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> DefinedAtom -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DefinedAtom] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedAtom) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DefinedAtom])
Pretty DefinedAtom Source #
Instance details Defined in THF.PrintTHF Methods pretty :: DefinedAtom -> Doc Source # pretties :: [DefinedAtom] -> Doc Source #
type Rep DefinedAtom
Instance details Defined in THF.ATC_THF type Rep DefinedAtom = D1 ('MetaData "DefinedAtom" "THF.As" "main" 'False) (C1 ('MetaCons "DA_Number" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Number)) :+: C1 ('MetaCons "DA_Distinct_Object" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data DefinedPlainTerm Source #

Constructors

DPT_Defined_Function DefinedFunctor Arguments
DPT_Defined_Constant DefinedFunctor

Instances

Instances details

Eq DefinedPlainTerm Source #
Instance details Defined in THF.As Methods (==) :: DefinedPlainTerm -> DefinedPlainTerm -> Bool (/=) :: DefinedPlainTerm -> DefinedPlainTerm -> Bool
Data DefinedPlainTerm Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefinedPlainTerm -> c DefinedPlainTerm gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefinedPlainTerm toConstr :: DefinedPlainTerm -> Constr dataTypeOf :: DefinedPlainTerm -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefinedPlainTerm) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefinedPlainTerm) gmapT :: (forall b. Data b => b -> b) -> DefinedPlainTerm -> DefinedPlainTerm gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefinedPlainTerm -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefinedPlainTerm -> r gmapQ :: (forall d. Data d => d -> u) -> DefinedPlainTerm -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DefinedPlainTerm -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefinedPlainTerm -> m DefinedPlainTerm gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedPlainTerm -> m DefinedPlainTerm gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedPlainTerm -> m DefinedPlainTerm
Ord DefinedPlainTerm Source #
Instance details Defined in THF.As Methods compare :: DefinedPlainTerm -> DefinedPlainTerm -> Ordering (<) :: DefinedPlainTerm -> DefinedPlainTerm -> Bool (<=) :: DefinedPlainTerm -> DefinedPlainTerm -> Bool (>) :: DefinedPlainTerm -> DefinedPlainTerm -> Bool (>=) :: DefinedPlainTerm -> DefinedPlainTerm -> Bool max :: DefinedPlainTerm -> DefinedPlainTerm -> DefinedPlainTerm min :: DefinedPlainTerm -> DefinedPlainTerm -> DefinedPlainTerm
Show DefinedPlainTerm Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> DefinedPlainTerm -> ShowS show :: DefinedPlainTerm -> String showList :: [DefinedPlainTerm] -> ShowS
Generic DefinedPlainTerm
Instance details Defined in THF.ATC_THF Associated Types type Rep DefinedPlainTerm :: Type -> Type Methods from :: DefinedPlainTerm -> Rep DefinedPlainTerm x to :: Rep DefinedPlainTerm x -> DefinedPlainTerm
GetRange DefinedPlainTerm Source #
Instance details Defined in THF.As Methods getRange :: DefinedPlainTerm -> Range Source # rangeSpan :: DefinedPlainTerm -> [Pos] Source #
FromJSON DefinedPlainTerm
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser DefinedPlainTerm parseJSONList :: Value -> Parser [DefinedPlainTerm]
ToJSON DefinedPlainTerm
Instance details Defined in THF.ATC_THF Methods toJSON :: DefinedPlainTerm -> Value toEncoding :: DefinedPlainTerm -> Encoding toJSONList :: [DefinedPlainTerm] -> Value toEncodingList :: [DefinedPlainTerm] -> Encoding
ShATermConvertible DefinedPlainTerm
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> DefinedPlainTerm -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DefinedPlainTerm] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedPlainTerm) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DefinedPlainTerm])
Pretty DefinedPlainTerm Source #
Instance details Defined in THF.PrintTHF Methods pretty :: DefinedPlainTerm -> Doc Source # pretties :: [DefinedPlainTerm] -> Doc Source #
type Rep DefinedPlainTerm
Instance details Defined in THF.ATC_THF type Rep DefinedPlainTerm = D1 ('MetaData "DefinedPlainTerm" "THF.As" "main" 'False) (C1 ('MetaCons "DPT_Defined_Function" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefinedFunctor) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Arguments)) :+: C1 ('MetaCons "DPT_Defined_Constant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DefinedFunctor)))

data DefinedFunctor Source #

Constructors

UMinus
Sum
Difference
Product
Quotient
Quotient_e
Quotient_t
Quotient_f
Remainder_e
Remainder_t
Remainder_f
Floor
Ceiling
Truncate
Round
To_int
To_rat
To_real

Instances

Instances details

Eq DefinedFunctor Source #
Instance details Defined in THF.As Methods (==) :: DefinedFunctor -> DefinedFunctor -> Bool (/=) :: DefinedFunctor -> DefinedFunctor -> Bool
Data DefinedFunctor Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefinedFunctor -> c DefinedFunctor gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefinedFunctor toConstr :: DefinedFunctor -> Constr dataTypeOf :: DefinedFunctor -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefinedFunctor) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefinedFunctor) gmapT :: (forall b. Data b => b -> b) -> DefinedFunctor -> DefinedFunctor gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefinedFunctor -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefinedFunctor -> r gmapQ :: (forall d. Data d => d -> u) -> DefinedFunctor -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DefinedFunctor -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefinedFunctor -> m DefinedFunctor gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedFunctor -> m DefinedFunctor gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefinedFunctor -> m DefinedFunctor
Ord DefinedFunctor Source #
Instance details Defined in THF.As Methods compare :: DefinedFunctor -> DefinedFunctor -> Ordering (<) :: DefinedFunctor -> DefinedFunctor -> Bool (<=) :: DefinedFunctor -> DefinedFunctor -> Bool (>) :: DefinedFunctor -> DefinedFunctor -> Bool (>=) :: DefinedFunctor -> DefinedFunctor -> Bool max :: DefinedFunctor -> DefinedFunctor -> DefinedFunctor min :: DefinedFunctor -> DefinedFunctor -> DefinedFunctor
Show DefinedFunctor Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> DefinedFunctor -> ShowS show :: DefinedFunctor -> String showList :: [DefinedFunctor] -> ShowS
Generic DefinedFunctor
Instance details Defined in THF.ATC_THF Associated Types type Rep DefinedFunctor :: Type -> Type Methods from :: DefinedFunctor -> Rep DefinedFunctor x to :: Rep DefinedFunctor x -> DefinedFunctor
GetRange DefinedFunctor Source #
Instance details Defined in THF.As Methods getRange :: DefinedFunctor -> Range Source # rangeSpan :: DefinedFunctor -> [Pos] Source #
FromJSON DefinedFunctor
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser DefinedFunctor parseJSONList :: Value -> Parser [DefinedFunctor]
ToJSON DefinedFunctor
Instance details Defined in THF.ATC_THF Methods toJSON :: DefinedFunctor -> Value toEncoding :: DefinedFunctor -> Encoding toJSONList :: [DefinedFunctor] -> Value toEncodingList :: [DefinedFunctor] -> Encoding
ShATermConvertible DefinedFunctor
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> DefinedFunctor -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DefinedFunctor] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DefinedFunctor) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DefinedFunctor])
Pretty DefinedFunctor Source #
Instance details Defined in THF.PrintTHF Methods pretty :: DefinedFunctor -> Doc Source # pretties :: [DefinedFunctor] -> Doc Source #
type Rep DefinedFunctor
Instance details Defined in THF.ATC_THF type Rep DefinedFunctor = D1 ('MetaData "DefinedFunctor" "THF.As" "main" 'False) ((((C1 ('MetaCons "UMinus" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Sum" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Difference" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Product" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Quotient" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Quotient_e" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Quotient_t" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Quotient_f" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Remainder_e" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "Remainder_t" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Remainder_f" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Floor" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ceiling" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Truncate" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Round" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "To_int" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "To_rat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "To_real" 'PrefixI 'False) (U1 :: Type -> Type))))))

data SystemTerm Source #

Constructors

ST_System_Term Token Arguments
ST_System_Constant Token

Instances

Instances details

Eq SystemTerm Source #
Instance details Defined in THF.As Methods (==) :: SystemTerm -> SystemTerm -> Bool (/=) :: SystemTerm -> SystemTerm -> Bool
Data SystemTerm Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SystemTerm -> c SystemTerm gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SystemTerm toConstr :: SystemTerm -> Constr dataTypeOf :: SystemTerm -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SystemTerm) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SystemTerm) gmapT :: (forall b. Data b => b -> b) -> SystemTerm -> SystemTerm gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SystemTerm -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SystemTerm -> r gmapQ :: (forall d. Data d => d -> u) -> SystemTerm -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SystemTerm -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SystemTerm -> m SystemTerm gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SystemTerm -> m SystemTerm gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SystemTerm -> m SystemTerm
Ord SystemTerm Source #
Instance details Defined in THF.As Methods compare :: SystemTerm -> SystemTerm -> Ordering (<) :: SystemTerm -> SystemTerm -> Bool (<=) :: SystemTerm -> SystemTerm -> Bool (>) :: SystemTerm -> SystemTerm -> Bool (>=) :: SystemTerm -> SystemTerm -> Bool max :: SystemTerm -> SystemTerm -> SystemTerm min :: SystemTerm -> SystemTerm -> SystemTerm
Show SystemTerm Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> SystemTerm -> ShowS show :: SystemTerm -> String showList :: [SystemTerm] -> ShowS
Generic SystemTerm
Instance details Defined in THF.ATC_THF Associated Types type Rep SystemTerm :: Type -> Type Methods from :: SystemTerm -> Rep SystemTerm x to :: Rep SystemTerm x -> SystemTerm
GetRange SystemTerm Source #
Instance details Defined in THF.As Methods getRange :: SystemTerm -> Range Source # rangeSpan :: SystemTerm -> [Pos] Source #
FromJSON SystemTerm
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser SystemTerm parseJSONList :: Value -> Parser [SystemTerm]
ToJSON SystemTerm
Instance details Defined in THF.ATC_THF Methods toJSON :: SystemTerm -> Value toEncoding :: SystemTerm -> Encoding toJSONList :: [SystemTerm] -> Value toEncodingList :: [SystemTerm] -> Encoding
ShATermConvertible SystemTerm
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> SystemTerm -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SystemTerm] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SystemTerm) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SystemTerm])
Pretty SystemTerm Source #
Instance details Defined in THF.PrintTHF Methods pretty :: SystemTerm -> Doc Source # pretties :: [SystemTerm] -> Doc Source #
type Rep SystemTerm
Instance details Defined in THF.ATC_THF type Rep SystemTerm = D1 ('MetaData "SystemTerm" "THF.As" "main" 'False) (C1 ('MetaCons "ST_System_Term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Arguments)) :+: C1 ('MetaCons "ST_System_Constant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

type Arguments = [Term] Source #

data PrincipalSymbol Source #

Constructors

PS_Functor AtomicWord
PS_Variable Token

Instances

Instances details

Eq PrincipalSymbol Source #
Instance details Defined in THF.As Methods (==) :: PrincipalSymbol -> PrincipalSymbol -> Bool (/=) :: PrincipalSymbol -> PrincipalSymbol -> Bool
Data PrincipalSymbol Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PrincipalSymbol -> c PrincipalSymbol gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PrincipalSymbol toConstr :: PrincipalSymbol -> Constr dataTypeOf :: PrincipalSymbol -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c PrincipalSymbol) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PrincipalSymbol) gmapT :: (forall b. Data b => b -> b) -> PrincipalSymbol -> PrincipalSymbol gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PrincipalSymbol -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PrincipalSymbol -> r gmapQ :: (forall d. Data d => d -> u) -> PrincipalSymbol -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PrincipalSymbol -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PrincipalSymbol -> m PrincipalSymbol gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PrincipalSymbol -> m PrincipalSymbol gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PrincipalSymbol -> m PrincipalSymbol
Ord PrincipalSymbol Source #
Instance details Defined in THF.As Methods compare :: PrincipalSymbol -> PrincipalSymbol -> Ordering (<) :: PrincipalSymbol -> PrincipalSymbol -> Bool (<=) :: PrincipalSymbol -> PrincipalSymbol -> Bool (>) :: PrincipalSymbol -> PrincipalSymbol -> Bool (>=) :: PrincipalSymbol -> PrincipalSymbol -> Bool max :: PrincipalSymbol -> PrincipalSymbol -> PrincipalSymbol min :: PrincipalSymbol -> PrincipalSymbol -> PrincipalSymbol
Show PrincipalSymbol Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> PrincipalSymbol -> ShowS show :: PrincipalSymbol -> String showList :: [PrincipalSymbol] -> ShowS
Generic PrincipalSymbol
Instance details Defined in THF.ATC_THF Associated Types type Rep PrincipalSymbol :: Type -> Type Methods from :: PrincipalSymbol -> Rep PrincipalSymbol x to :: Rep PrincipalSymbol x -> PrincipalSymbol
GetRange PrincipalSymbol Source #
Instance details Defined in THF.As Methods getRange :: PrincipalSymbol -> Range Source # rangeSpan :: PrincipalSymbol -> [Pos] Source #
FromJSON PrincipalSymbol
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser PrincipalSymbol parseJSONList :: Value -> Parser [PrincipalSymbol]
ToJSON PrincipalSymbol
Instance details Defined in THF.ATC_THF Methods toJSON :: PrincipalSymbol -> Value toEncoding :: PrincipalSymbol -> Encoding toJSONList :: [PrincipalSymbol] -> Value toEncodingList :: [PrincipalSymbol] -> Encoding
ShATermConvertible PrincipalSymbol
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> PrincipalSymbol -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [PrincipalSymbol] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, PrincipalSymbol) fromShATermList' :: Int -> ATermTable -> (ATermTable, [PrincipalSymbol])
Pretty PrincipalSymbol Source #
Instance details Defined in THF.PrintTHF Methods pretty :: PrincipalSymbol -> Doc Source # pretties :: [PrincipalSymbol] -> Doc Source #
type Rep PrincipalSymbol
Instance details Defined in THF.ATC_THF type Rep PrincipalSymbol = D1 ('MetaData "PrincipalSymbol" "THF.As" "main" 'False) (C1 ('MetaCons "PS_Functor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AtomicWord)) :+: C1 ('MetaCons "PS_Variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data Source Source #

Constructors

S_Dag_Source DagSource
S_Internal_Source IntroType OptionalInfo
S_External_Source ExternalSource
S_Sources [Source]
S_Unknown

Instances

Instances details

Eq Source Source #
Instance details Defined in THF.As Methods (==) :: Source -> Source -> Bool (/=) :: Source -> Source -> Bool
Data Source Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Source -> c Source gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Source toConstr :: Source -> Constr dataTypeOf :: Source -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Source) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Source) gmapT :: (forall b. Data b => b -> b) -> Source -> Source gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Source -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Source -> r gmapQ :: (forall d. Data d => d -> u) -> Source -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Source -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Source -> m Source gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Source -> m Source gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Source -> m Source
Ord Source Source #
Instance details Defined in THF.As Methods compare :: Source -> Source -> Ordering (<) :: Source -> Source -> Bool (<=) :: Source -> Source -> Bool (>) :: Source -> Source -> Bool (>=) :: Source -> Source -> Bool max :: Source -> Source -> Source min :: Source -> Source -> Source
Show Source Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> Source -> ShowS show :: Source -> String showList :: [Source] -> ShowS
Generic Source
Instance details Defined in THF.ATC_THF Associated Types type Rep Source :: Type -> Type Methods from :: Source -> Rep Source x to :: Rep Source x -> Source
GetRange Source Source #
Instance details Defined in THF.As Methods getRange :: Source -> Range Source # rangeSpan :: Source -> [Pos] Source #
FromJSON Source
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser Source parseJSONList :: Value -> Parser [Source]
ToJSON Source
Instance details Defined in THF.ATC_THF Methods toJSON :: Source -> Value toEncoding :: Source -> Encoding toJSONList :: [Source] -> Value toEncodingList :: [Source] -> Encoding
ShATermConvertible Source
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> Source -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Source] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Source) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Source])
Pretty Source Source #
Instance details Defined in THF.PrintTHF Methods pretty :: Source -> Doc Source # pretties :: [Source] -> Doc Source #
type Rep Source
Instance details Defined in THF.ATC_THF type Rep Source = D1 ('MetaData "Source" "THF.As" "main" 'False) ((C1 ('MetaCons "S_Dag_Source" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DagSource)) :+: C1 ('MetaCons "S_Internal_Source" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IntroType) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OptionalInfo))) :+: (C1 ('MetaCons "S_External_Source" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExternalSource)) :+: (C1 ('MetaCons "S_Sources" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Source])) :+: C1 ('MetaCons "S_Unknown" 'PrefixI 'False) (U1 :: Type -> Type))))

data DagSource Source #

Constructors

DS_Name Name
DS_Inference_Record AtomicWord UsefulInfo [ParentInfo]

Instances

Instances details

Eq DagSource Source #
Instance details Defined in THF.As Methods (==) :: DagSource -> DagSource -> Bool (/=) :: DagSource -> DagSource -> Bool
Data DagSource Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DagSource -> c DagSource gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DagSource toConstr :: DagSource -> Constr dataTypeOf :: DagSource -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DagSource) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DagSource) gmapT :: (forall b. Data b => b -> b) -> DagSource -> DagSource gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DagSource -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DagSource -> r gmapQ :: (forall d. Data d => d -> u) -> DagSource -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DagSource -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DagSource -> m DagSource gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DagSource -> m DagSource gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DagSource -> m DagSource
Ord DagSource Source #
Instance details Defined in THF.As Methods compare :: DagSource -> DagSource -> Ordering (<) :: DagSource -> DagSource -> Bool (<=) :: DagSource -> DagSource -> Bool (>) :: DagSource -> DagSource -> Bool (>=) :: DagSource -> DagSource -> Bool max :: DagSource -> DagSource -> DagSource min :: DagSource -> DagSource -> DagSource
Show DagSource Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> DagSource -> ShowS show :: DagSource -> String showList :: [DagSource] -> ShowS
Generic DagSource
Instance details Defined in THF.ATC_THF Associated Types type Rep DagSource :: Type -> Type Methods from :: DagSource -> Rep DagSource x to :: Rep DagSource x -> DagSource
GetRange DagSource Source #
Instance details Defined in THF.As Methods getRange :: DagSource -> Range Source # rangeSpan :: DagSource -> [Pos] Source #
FromJSON DagSource
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser DagSource parseJSONList :: Value -> Parser [DagSource]
ToJSON DagSource
Instance details Defined in THF.ATC_THF Methods toJSON :: DagSource -> Value toEncoding :: DagSource -> Encoding toJSONList :: [DagSource] -> Value toEncodingList :: [DagSource] -> Encoding
ShATermConvertible DagSource
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> DagSource -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DagSource] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DagSource) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DagSource])
Pretty DagSource Source #
Instance details Defined in THF.PrintTHF Methods pretty :: DagSource -> Doc Source # pretties :: [DagSource] -> Doc Source #
type Rep DagSource
Instance details Defined in THF.ATC_THF type Rep DagSource = D1 ('MetaData "DagSource" "THF.As" "main" 'False) (C1 ('MetaCons "DS_Name" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "DS_Inference_Record" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AtomicWord) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UsefulInfo) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [ParentInfo]))))

data ParentInfo Source #

Constructors

PI_Parent_Info Source (Maybe GeneralList)

Instances

Instances details

Eq ParentInfo Source #
Instance details Defined in THF.As Methods (==) :: ParentInfo -> ParentInfo -> Bool (/=) :: ParentInfo -> ParentInfo -> Bool
Data ParentInfo Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ParentInfo -> c ParentInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ParentInfo toConstr :: ParentInfo -> Constr dataTypeOf :: ParentInfo -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ParentInfo) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ParentInfo) gmapT :: (forall b. Data b => b -> b) -> ParentInfo -> ParentInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ParentInfo -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ParentInfo -> r gmapQ :: (forall d. Data d => d -> u) -> ParentInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ParentInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ParentInfo -> m ParentInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ParentInfo -> m ParentInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ParentInfo -> m ParentInfo
Ord ParentInfo Source #
Instance details Defined in THF.As Methods compare :: ParentInfo -> ParentInfo -> Ordering (<) :: ParentInfo -> ParentInfo -> Bool (<=) :: ParentInfo -> ParentInfo -> Bool (>) :: ParentInfo -> ParentInfo -> Bool (>=) :: ParentInfo -> ParentInfo -> Bool max :: ParentInfo -> ParentInfo -> ParentInfo min :: ParentInfo -> ParentInfo -> ParentInfo
Show ParentInfo Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> ParentInfo -> ShowS show :: ParentInfo -> String showList :: [ParentInfo] -> ShowS
Generic ParentInfo
Instance details Defined in THF.ATC_THF Associated Types type Rep ParentInfo :: Type -> Type Methods from :: ParentInfo -> Rep ParentInfo x to :: Rep ParentInfo x -> ParentInfo
GetRange ParentInfo Source #
Instance details Defined in THF.As Methods getRange :: ParentInfo -> Range Source # rangeSpan :: ParentInfo -> [Pos] Source #
FromJSON ParentInfo
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser ParentInfo parseJSONList :: Value -> Parser [ParentInfo]
ToJSON ParentInfo
Instance details Defined in THF.ATC_THF Methods toJSON :: ParentInfo -> Value toEncoding :: ParentInfo -> Encoding toJSONList :: [ParentInfo] -> Value toEncodingList :: [ParentInfo] -> Encoding
ShATermConvertible ParentInfo
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> ParentInfo -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ParentInfo] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ParentInfo) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ParentInfo])
Pretty ParentInfo Source #
Instance details Defined in THF.PrintTHF Methods pretty :: ParentInfo -> Doc Source # pretties :: [ParentInfo] -> Doc Source #
type Rep ParentInfo
Instance details Defined in THF.ATC_THF type Rep ParentInfo = D1 ('MetaData "ParentInfo" "THF.As" "main" 'False) (C1 ('MetaCons "PI_Parent_Info" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Source) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe GeneralList))))

data IntroType Source #

Constructors

IT_definition
IT_axiom_of_choice
IT_tautology
IT_assumption

Instances

Instances details

Eq IntroType Source #
Instance details Defined in THF.As Methods (==) :: IntroType -> IntroType -> Bool (/=) :: IntroType -> IntroType -> Bool
Data IntroType Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IntroType -> c IntroType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IntroType toConstr :: IntroType -> Constr dataTypeOf :: IntroType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IntroType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IntroType) gmapT :: (forall b. Data b => b -> b) -> IntroType -> IntroType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IntroType -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IntroType -> r gmapQ :: (forall d. Data d => d -> u) -> IntroType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> IntroType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> IntroType -> m IntroType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IntroType -> m IntroType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IntroType -> m IntroType
Ord IntroType Source #
Instance details Defined in THF.As Methods compare :: IntroType -> IntroType -> Ordering (<) :: IntroType -> IntroType -> Bool (<=) :: IntroType -> IntroType -> Bool (>) :: IntroType -> IntroType -> Bool (>=) :: IntroType -> IntroType -> Bool max :: IntroType -> IntroType -> IntroType min :: IntroType -> IntroType -> IntroType
Show IntroType Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> IntroType -> ShowS show :: IntroType -> String showList :: [IntroType] -> ShowS
Generic IntroType
Instance details Defined in THF.ATC_THF Associated Types type Rep IntroType :: Type -> Type Methods from :: IntroType -> Rep IntroType x to :: Rep IntroType x -> IntroType
GetRange IntroType Source #
Instance details Defined in THF.As Methods getRange :: IntroType -> Range Source # rangeSpan :: IntroType -> [Pos] Source #
FromJSON IntroType
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser IntroType parseJSONList :: Value -> Parser [IntroType]
ToJSON IntroType
Instance details Defined in THF.ATC_THF Methods toJSON :: IntroType -> Value toEncoding :: IntroType -> Encoding toJSONList :: [IntroType] -> Value toEncodingList :: [IntroType] -> Encoding
ShATermConvertible IntroType
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> IntroType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [IntroType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, IntroType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [IntroType])
Pretty IntroType Source #
Instance details Defined in THF.PrintTHF Methods pretty :: IntroType -> Doc Source # pretties :: [IntroType] -> Doc Source #
type Rep IntroType
Instance details Defined in THF.ATC_THF type Rep IntroType = D1 ('MetaData "IntroType" "THF.As" "main" 'False) ((C1 ('MetaCons "IT_definition" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IT_axiom_of_choice" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "IT_tautology" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IT_assumption" 'PrefixI 'False) (U1 :: Type -> Type)))

data ExternalSource Source #

Constructors

ES_File_Source FileSource
ES_Theory TheoryName OptionalInfo
ES_Creator_Source AtomicWord OptionalInfo

Instances

Instances details

Eq ExternalSource Source #
Instance details Defined in THF.As Methods (==) :: ExternalSource -> ExternalSource -> Bool (/=) :: ExternalSource -> ExternalSource -> Bool
Data ExternalSource Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExternalSource -> c ExternalSource gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExternalSource toConstr :: ExternalSource -> Constr dataTypeOf :: ExternalSource -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExternalSource) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExternalSource) gmapT :: (forall b. Data b => b -> b) -> ExternalSource -> ExternalSource gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExternalSource -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExternalSource -> r gmapQ :: (forall d. Data d => d -> u) -> ExternalSource -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ExternalSource -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExternalSource -> m ExternalSource gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExternalSource -> m ExternalSource gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExternalSource -> m ExternalSource
Ord ExternalSource Source #
Instance details Defined in THF.As Methods compare :: ExternalSource -> ExternalSource -> Ordering (<) :: ExternalSource -> ExternalSource -> Bool (<=) :: ExternalSource -> ExternalSource -> Bool (>) :: ExternalSource -> ExternalSource -> Bool (>=) :: ExternalSource -> ExternalSource -> Bool max :: ExternalSource -> ExternalSource -> ExternalSource min :: ExternalSource -> ExternalSource -> ExternalSource
Show ExternalSource Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> ExternalSource -> ShowS show :: ExternalSource -> String showList :: [ExternalSource] -> ShowS
Generic ExternalSource
Instance details Defined in THF.ATC_THF Associated Types type Rep ExternalSource :: Type -> Type Methods from :: ExternalSource -> Rep ExternalSource x to :: Rep ExternalSource x -> ExternalSource
GetRange ExternalSource Source #
Instance details Defined in THF.As Methods getRange :: ExternalSource -> Range Source # rangeSpan :: ExternalSource -> [Pos] Source #
FromJSON ExternalSource
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser ExternalSource parseJSONList :: Value -> Parser [ExternalSource]
ToJSON ExternalSource
Instance details Defined in THF.ATC_THF Methods toJSON :: ExternalSource -> Value toEncoding :: ExternalSource -> Encoding toJSONList :: [ExternalSource] -> Value toEncodingList :: [ExternalSource] -> Encoding
ShATermConvertible ExternalSource
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> ExternalSource -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ExternalSource] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ExternalSource) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ExternalSource])
Pretty ExternalSource Source #
Instance details Defined in THF.PrintTHF Methods pretty :: ExternalSource -> Doc Source # pretties :: [ExternalSource] -> Doc Source #
type Rep ExternalSource
Instance details Defined in THF.ATC_THF type Rep ExternalSource = D1 ('MetaData "ExternalSource" "THF.As" "main" 'False) (C1 ('MetaCons "ES_File_Source" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileSource)) :+: (C1 ('MetaCons "ES_Theory" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TheoryName) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OptionalInfo)) :+: C1 ('MetaCons "ES_Creator_Source" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AtomicWord) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OptionalInfo))))

data FileSource Source #

Constructors

FS_File Token (Maybe Name)

Instances

Instances details

Eq FileSource Source #
Instance details Defined in THF.As Methods (==) :: FileSource -> FileSource -> Bool (/=) :: FileSource -> FileSource -> Bool
Data FileSource Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FileSource -> c FileSource gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FileSource toConstr :: FileSource -> Constr dataTypeOf :: FileSource -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FileSource) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FileSource) gmapT :: (forall b. Data b => b -> b) -> FileSource -> FileSource gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FileSource -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FileSource -> r gmapQ :: (forall d. Data d => d -> u) -> FileSource -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FileSource -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FileSource -> m FileSource gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FileSource -> m FileSource gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FileSource -> m FileSource
Ord FileSource Source #
Instance details Defined in THF.As Methods compare :: FileSource -> FileSource -> Ordering (<) :: FileSource -> FileSource -> Bool (<=) :: FileSource -> FileSource -> Bool (>) :: FileSource -> FileSource -> Bool (>=) :: FileSource -> FileSource -> Bool max :: FileSource -> FileSource -> FileSource min :: FileSource -> FileSource -> FileSource
Show FileSource Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> FileSource -> ShowS show :: FileSource -> String showList :: [FileSource] -> ShowS
Generic FileSource
Instance details Defined in THF.ATC_THF Associated Types type Rep FileSource :: Type -> Type Methods from :: FileSource -> Rep FileSource x to :: Rep FileSource x -> FileSource
GetRange FileSource Source #
Instance details Defined in THF.As Methods getRange :: FileSource -> Range Source # rangeSpan :: FileSource -> [Pos] Source #
FromJSON FileSource
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser FileSource parseJSONList :: Value -> Parser [FileSource]
ToJSON FileSource
Instance details Defined in THF.ATC_THF Methods toJSON :: FileSource -> Value toEncoding :: FileSource -> Encoding toJSONList :: [FileSource] -> Value toEncodingList :: [FileSource] -> Encoding
ShATermConvertible FileSource
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> FileSource -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FileSource] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FileSource) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FileSource])
Pretty FileSource Source #
Instance details Defined in THF.PrintTHF Methods pretty :: FileSource -> Doc Source # pretties :: [FileSource] -> Doc Source #
type Rep FileSource
Instance details Defined in THF.ATC_THF type Rep FileSource = D1 ('MetaData "FileSource" "THF.As" "main" 'False) (C1 ('MetaCons "FS_File" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Name))))

data TheoryName Source #

Constructors

Equality
Ac

Instances

Instances details

Eq TheoryName Source #
Instance details Defined in THF.As Methods (==) :: TheoryName -> TheoryName -> Bool (/=) :: TheoryName -> TheoryName -> Bool
Data TheoryName Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TheoryName -> c TheoryName gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TheoryName toConstr :: TheoryName -> Constr dataTypeOf :: TheoryName -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TheoryName) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TheoryName) gmapT :: (forall b. Data b => b -> b) -> TheoryName -> TheoryName gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TheoryName -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TheoryName -> r gmapQ :: (forall d. Data d => d -> u) -> TheoryName -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TheoryName -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TheoryName -> m TheoryName gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TheoryName -> m TheoryName gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TheoryName -> m TheoryName
Ord TheoryName Source #
Instance details Defined in THF.As Methods compare :: TheoryName -> TheoryName -> Ordering (<) :: TheoryName -> TheoryName -> Bool (<=) :: TheoryName -> TheoryName -> Bool (>) :: TheoryName -> TheoryName -> Bool (>=) :: TheoryName -> TheoryName -> Bool max :: TheoryName -> TheoryName -> TheoryName min :: TheoryName -> TheoryName -> TheoryName
Show TheoryName Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> TheoryName -> ShowS show :: TheoryName -> String showList :: [TheoryName] -> ShowS
Generic TheoryName
Instance details Defined in THF.ATC_THF Associated Types type Rep TheoryName :: Type -> Type Methods from :: TheoryName -> Rep TheoryName x to :: Rep TheoryName x -> TheoryName
GetRange TheoryName Source #
Instance details Defined in THF.As Methods getRange :: TheoryName -> Range Source # rangeSpan :: TheoryName -> [Pos] Source #
FromJSON TheoryName
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser TheoryName parseJSONList :: Value -> Parser [TheoryName]
ToJSON TheoryName
Instance details Defined in THF.ATC_THF Methods toJSON :: TheoryName -> Value toEncoding :: TheoryName -> Encoding toJSONList :: [TheoryName] -> Value toEncodingList :: [TheoryName] -> Encoding
ShATermConvertible TheoryName
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> TheoryName -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TheoryName] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TheoryName) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TheoryName])
Pretty TheoryName Source #
Instance details Defined in THF.PrintTHF Methods pretty :: TheoryName -> Doc Source # pretties :: [TheoryName] -> Doc Source #
type Rep TheoryName
Instance details Defined in THF.ATC_THF type Rep TheoryName = D1 ('MetaData "TheoryName" "THF.As" "main" 'False) (C1 ('MetaCons "Equality" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ac" 'PrefixI 'False) (U1 :: Type -> Type))

type OptionalInfo = Maybe UsefulInfo Source #

type UsefulInfo = [InfoItem] Source #

data InfoItem Source #

Constructors

II_Formula_Item FormulaItem
II_Inference_Item InferenceItem
II_General_Function GeneralFunction

Instances

Instances details

Eq InfoItem Source #
Instance details Defined in THF.As Methods (==) :: InfoItem -> InfoItem -> Bool (/=) :: InfoItem -> InfoItem -> Bool
Data InfoItem Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InfoItem -> c InfoItem gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InfoItem toConstr :: InfoItem -> Constr dataTypeOf :: InfoItem -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c InfoItem) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InfoItem) gmapT :: (forall b. Data b => b -> b) -> InfoItem -> InfoItem gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InfoItem -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InfoItem -> r gmapQ :: (forall d. Data d => d -> u) -> InfoItem -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> InfoItem -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> InfoItem -> m InfoItem gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InfoItem -> m InfoItem gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InfoItem -> m InfoItem
Ord InfoItem Source #
Instance details Defined in THF.As Methods compare :: InfoItem -> InfoItem -> Ordering (<) :: InfoItem -> InfoItem -> Bool (<=) :: InfoItem -> InfoItem -> Bool (>) :: InfoItem -> InfoItem -> Bool (>=) :: InfoItem -> InfoItem -> Bool max :: InfoItem -> InfoItem -> InfoItem min :: InfoItem -> InfoItem -> InfoItem
Show InfoItem Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> InfoItem -> ShowS show :: InfoItem -> String showList :: [InfoItem] -> ShowS
Generic InfoItem
Instance details Defined in THF.ATC_THF Associated Types type Rep InfoItem :: Type -> Type Methods from :: InfoItem -> Rep InfoItem x to :: Rep InfoItem x -> InfoItem
GetRange InfoItem Source #
Instance details Defined in THF.As Methods getRange :: InfoItem -> Range Source # rangeSpan :: InfoItem -> [Pos] Source #
FromJSON InfoItem
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser InfoItem parseJSONList :: Value -> Parser [InfoItem]
ToJSON InfoItem
Instance details Defined in THF.ATC_THF Methods toJSON :: InfoItem -> Value toEncoding :: InfoItem -> Encoding toJSONList :: [InfoItem] -> Value toEncodingList :: [InfoItem] -> Encoding
ShATermConvertible InfoItem
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> InfoItem -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [InfoItem] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, InfoItem) fromShATermList' :: Int -> ATermTable -> (ATermTable, [InfoItem])
Pretty InfoItem Source #
Instance details Defined in THF.PrintTHF Methods pretty :: InfoItem -> Doc Source # pretties :: [InfoItem] -> Doc Source #
type Rep InfoItem
Instance details Defined in THF.ATC_THF type Rep InfoItem = D1 ('MetaData "InfoItem" "THF.As" "main" 'False) (C1 ('MetaCons "II_Formula_Item" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FormulaItem)) :+: (C1 ('MetaCons "II_Inference_Item" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InferenceItem)) :+: C1 ('MetaCons "II_General_Function" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralFunction))))

data FormulaItem Source #

Constructors

FI_Description_Item AtomicWord
FI_Iquote_Item AtomicWord

Instances

Instances details

Eq FormulaItem Source #
Instance details Defined in THF.As Methods (==) :: FormulaItem -> FormulaItem -> Bool (/=) :: FormulaItem -> FormulaItem -> Bool
Data FormulaItem Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FormulaItem -> c FormulaItem gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FormulaItem toConstr :: FormulaItem -> Constr dataTypeOf :: FormulaItem -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FormulaItem) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FormulaItem) gmapT :: (forall b. Data b => b -> b) -> FormulaItem -> FormulaItem gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FormulaItem -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FormulaItem -> r gmapQ :: (forall d. Data d => d -> u) -> FormulaItem -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FormulaItem -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FormulaItem -> m FormulaItem gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FormulaItem -> m FormulaItem gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FormulaItem -> m FormulaItem
Ord FormulaItem Source #
Instance details Defined in THF.As Methods compare :: FormulaItem -> FormulaItem -> Ordering (<) :: FormulaItem -> FormulaItem -> Bool (<=) :: FormulaItem -> FormulaItem -> Bool (>) :: FormulaItem -> FormulaItem -> Bool (>=) :: FormulaItem -> FormulaItem -> Bool max :: FormulaItem -> FormulaItem -> FormulaItem min :: FormulaItem -> FormulaItem -> FormulaItem
Show FormulaItem Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> FormulaItem -> ShowS show :: FormulaItem -> String showList :: [FormulaItem] -> ShowS
Generic FormulaItem
Instance details Defined in THF.ATC_THF Associated Types type Rep FormulaItem :: Type -> Type Methods from :: FormulaItem -> Rep FormulaItem x to :: Rep FormulaItem x -> FormulaItem
GetRange FormulaItem Source #
Instance details Defined in THF.As Methods getRange :: FormulaItem -> Range Source # rangeSpan :: FormulaItem -> [Pos] Source #
FromJSON FormulaItem
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser FormulaItem parseJSONList :: Value -> Parser [FormulaItem]
ToJSON FormulaItem
Instance details Defined in THF.ATC_THF Methods toJSON :: FormulaItem -> Value toEncoding :: FormulaItem -> Encoding toJSONList :: [FormulaItem] -> Value toEncodingList :: [FormulaItem] -> Encoding
ShATermConvertible FormulaItem
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> FormulaItem -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FormulaItem] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FormulaItem) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FormulaItem])
Pretty FormulaItem Source #
Instance details Defined in THF.PrintTHF Methods pretty :: FormulaItem -> Doc Source # pretties :: [FormulaItem] -> Doc Source #
type Rep FormulaItem
Instance details Defined in THF.ATC_THF type Rep FormulaItem = D1 ('MetaData "FormulaItem" "THF.As" "main" 'False) (C1 ('MetaCons "FI_Description_Item" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AtomicWord)) :+: C1 ('MetaCons "FI_Iquote_Item" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AtomicWord)))

data InferenceItem Source #

Constructors

II_Inference_Status InferenceStatus
II_Assumptions_Record NameList
II_New_Symbol_Record AtomicWord [PrincipalSymbol]
II_Refutation FileSource

Instances

Instances details

Eq InferenceItem Source #
Instance details Defined in THF.As Methods (==) :: InferenceItem -> InferenceItem -> Bool (/=) :: InferenceItem -> InferenceItem -> Bool
Data InferenceItem Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InferenceItem -> c InferenceItem gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InferenceItem toConstr :: InferenceItem -> Constr dataTypeOf :: InferenceItem -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c InferenceItem) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InferenceItem) gmapT :: (forall b. Data b => b -> b) -> InferenceItem -> InferenceItem gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InferenceItem -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InferenceItem -> r gmapQ :: (forall d. Data d => d -> u) -> InferenceItem -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> InferenceItem -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> InferenceItem -> m InferenceItem gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InferenceItem -> m InferenceItem gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InferenceItem -> m InferenceItem
Ord InferenceItem Source #
Instance details Defined in THF.As Methods compare :: InferenceItem -> InferenceItem -> Ordering (<) :: InferenceItem -> InferenceItem -> Bool (<=) :: InferenceItem -> InferenceItem -> Bool (>) :: InferenceItem -> InferenceItem -> Bool (>=) :: InferenceItem -> InferenceItem -> Bool max :: InferenceItem -> InferenceItem -> InferenceItem min :: InferenceItem -> InferenceItem -> InferenceItem
Show InferenceItem Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> InferenceItem -> ShowS show :: InferenceItem -> String showList :: [InferenceItem] -> ShowS
Generic InferenceItem
Instance details Defined in THF.ATC_THF Associated Types type Rep InferenceItem :: Type -> Type Methods from :: InferenceItem -> Rep InferenceItem x to :: Rep InferenceItem x -> InferenceItem
GetRange InferenceItem Source #
Instance details Defined in THF.As Methods getRange :: InferenceItem -> Range Source # rangeSpan :: InferenceItem -> [Pos] Source #
FromJSON InferenceItem
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser InferenceItem parseJSONList :: Value -> Parser [InferenceItem]
ToJSON InferenceItem
Instance details Defined in THF.ATC_THF Methods toJSON :: InferenceItem -> Value toEncoding :: InferenceItem -> Encoding toJSONList :: [InferenceItem] -> Value toEncodingList :: [InferenceItem] -> Encoding
ShATermConvertible InferenceItem
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> InferenceItem -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [InferenceItem] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, InferenceItem) fromShATermList' :: Int -> ATermTable -> (ATermTable, [InferenceItem])
Pretty InferenceItem Source #
Instance details Defined in THF.PrintTHF Methods pretty :: InferenceItem -> Doc Source # pretties :: [InferenceItem] -> Doc Source #
type Rep InferenceItem
Instance details Defined in THF.ATC_THF type Rep InferenceItem = D1 ('MetaData "InferenceItem" "THF.As" "main" 'False) ((C1 ('MetaCons "II_Inference_Status" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 InferenceStatus)) :+: C1 ('MetaCons "II_Assumptions_Record" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameList))) :+: (C1 ('MetaCons "II_New_Symbol_Record" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AtomicWord) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [PrincipalSymbol])) :+: C1 ('MetaCons "II_Refutation" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileSource))))

data InferenceStatus Source #

Constructors

IS_Status StatusValue
IS_Inference_Info AtomicWord AtomicWord GeneralList

Instances

Instances details

Eq InferenceStatus Source #
Instance details Defined in THF.As Methods (==) :: InferenceStatus -> InferenceStatus -> Bool (/=) :: InferenceStatus -> InferenceStatus -> Bool
Data InferenceStatus Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> InferenceStatus -> c InferenceStatus gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c InferenceStatus toConstr :: InferenceStatus -> Constr dataTypeOf :: InferenceStatus -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c InferenceStatus) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c InferenceStatus) gmapT :: (forall b. Data b => b -> b) -> InferenceStatus -> InferenceStatus gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> InferenceStatus -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> InferenceStatus -> r gmapQ :: (forall d. Data d => d -> u) -> InferenceStatus -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> InferenceStatus -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> InferenceStatus -> m InferenceStatus gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> InferenceStatus -> m InferenceStatus gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> InferenceStatus -> m InferenceStatus
Ord InferenceStatus Source #
Instance details Defined in THF.As Methods compare :: InferenceStatus -> InferenceStatus -> Ordering (<) :: InferenceStatus -> InferenceStatus -> Bool (<=) :: InferenceStatus -> InferenceStatus -> Bool (>) :: InferenceStatus -> InferenceStatus -> Bool (>=) :: InferenceStatus -> InferenceStatus -> Bool max :: InferenceStatus -> InferenceStatus -> InferenceStatus min :: InferenceStatus -> InferenceStatus -> InferenceStatus
Show InferenceStatus Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> InferenceStatus -> ShowS show :: InferenceStatus -> String showList :: [InferenceStatus] -> ShowS
Generic InferenceStatus
Instance details Defined in THF.ATC_THF Associated Types type Rep InferenceStatus :: Type -> Type Methods from :: InferenceStatus -> Rep InferenceStatus x to :: Rep InferenceStatus x -> InferenceStatus
GetRange InferenceStatus Source #
Instance details Defined in THF.As Methods getRange :: InferenceStatus -> Range Source # rangeSpan :: InferenceStatus -> [Pos] Source #
FromJSON InferenceStatus
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser InferenceStatus parseJSONList :: Value -> Parser [InferenceStatus]
ToJSON InferenceStatus
Instance details Defined in THF.ATC_THF Methods toJSON :: InferenceStatus -> Value toEncoding :: InferenceStatus -> Encoding toJSONList :: [InferenceStatus] -> Value toEncodingList :: [InferenceStatus] -> Encoding
ShATermConvertible InferenceStatus
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> InferenceStatus -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [InferenceStatus] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, InferenceStatus) fromShATermList' :: Int -> ATermTable -> (ATermTable, [InferenceStatus])
Pretty InferenceStatus Source #
Instance details Defined in THF.PrintTHF Methods pretty :: InferenceStatus -> Doc Source # pretties :: [InferenceStatus] -> Doc Source #
type Rep InferenceStatus
Instance details Defined in THF.ATC_THF type Rep InferenceStatus = D1 ('MetaData "InferenceStatus" "THF.As" "main" 'False) (C1 ('MetaCons "IS_Status" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 StatusValue)) :+: C1 ('MetaCons "IS_Inference_Info" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AtomicWord) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AtomicWord) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralList))))

data StatusValue Source #

Constructors

Suc
Unp
Sap
Esa
Sat
Fsa
Thm
Eqv
Tac
Wec
Eth
Tau
Wtc
Wth
Cax
Sca
Tca
Wca
Cup
Csp
Ecs
Csa
Cth
Ceq
Unc
Wcc
Ect
Fun
Uns
Wuc
Wct
Scc
Uca
Noc

Instances

Instances details

Eq StatusValue Source #
Instance details Defined in THF.As Methods (==) :: StatusValue -> StatusValue -> Bool (/=) :: StatusValue -> StatusValue -> Bool
Data StatusValue Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> StatusValue -> c StatusValue gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c StatusValue toConstr :: StatusValue -> Constr dataTypeOf :: StatusValue -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c StatusValue) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c StatusValue) gmapT :: (forall b. Data b => b -> b) -> StatusValue -> StatusValue gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> StatusValue -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> StatusValue -> r gmapQ :: (forall d. Data d => d -> u) -> StatusValue -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> StatusValue -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> StatusValue -> m StatusValue gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> StatusValue -> m StatusValue gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> StatusValue -> m StatusValue
Ord StatusValue Source #
Instance details Defined in THF.As Methods compare :: StatusValue -> StatusValue -> Ordering (<) :: StatusValue -> StatusValue -> Bool (<=) :: StatusValue -> StatusValue -> Bool (>) :: StatusValue -> StatusValue -> Bool (>=) :: StatusValue -> StatusValue -> Bool max :: StatusValue -> StatusValue -> StatusValue min :: StatusValue -> StatusValue -> StatusValue
Show StatusValue Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> StatusValue -> ShowS show :: StatusValue -> String showList :: [StatusValue] -> ShowS
Generic StatusValue
Instance details Defined in THF.ATC_THF Associated Types type Rep StatusValue :: Type -> Type Methods from :: StatusValue -> Rep StatusValue x to :: Rep StatusValue x -> StatusValue
GetRange StatusValue Source #
Instance details Defined in THF.As Methods getRange :: StatusValue -> Range Source # rangeSpan :: StatusValue -> [Pos] Source #
FromJSON StatusValue
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser StatusValue parseJSONList :: Value -> Parser [StatusValue]
ToJSON StatusValue
Instance details Defined in THF.ATC_THF Methods toJSON :: StatusValue -> Value toEncoding :: StatusValue -> Encoding toJSONList :: [StatusValue] -> Value toEncodingList :: [StatusValue] -> Encoding
ShATermConvertible StatusValue
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> StatusValue -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [StatusValue] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, StatusValue) fromShATermList' :: Int -> ATermTable -> (ATermTable, [StatusValue])
Pretty StatusValue Source #
Instance details Defined in THF.PrintTHF Methods pretty :: StatusValue -> Doc Source # pretties :: [StatusValue] -> Doc Source #
type Rep StatusValue
Instance details Defined in THF.ATC_THF type Rep StatusValue = D1 ('MetaData "StatusValue" "THF.As" "main" 'False) (((((C1 ('MetaCons "Suc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Unp" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Sap" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Esa" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Sat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Fsa" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Thm" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Eqv" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "Tac" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Wec" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Eth" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Tau" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Wtc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Wth" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Cax" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Sca" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Tca" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "Wca" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cup" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Csp" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ecs" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Csa" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cth" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Ceq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Unc" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "Wcc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ect" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Fun" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Uns" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Wuc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Wct" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Scc" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Uca" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Noc" 'PrefixI 'False) (U1 :: Type -> Type)))))))

type NameList = [Name] Source #

data GeneralTerm Source #

Constructors

GT_General_Data GeneralData
GT_General_Data_Term GeneralData GeneralTerm
GT_General_List GeneralList

Instances

Instances details

Eq GeneralTerm Source #
Instance details Defined in THF.As Methods (==) :: GeneralTerm -> GeneralTerm -> Bool (/=) :: GeneralTerm -> GeneralTerm -> Bool
Data GeneralTerm Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GeneralTerm -> c GeneralTerm gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GeneralTerm toConstr :: GeneralTerm -> Constr dataTypeOf :: GeneralTerm -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GeneralTerm) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GeneralTerm) gmapT :: (forall b. Data b => b -> b) -> GeneralTerm -> GeneralTerm gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GeneralTerm -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GeneralTerm -> r gmapQ :: (forall d. Data d => d -> u) -> GeneralTerm -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> GeneralTerm -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> GeneralTerm -> m GeneralTerm gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralTerm -> m GeneralTerm gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralTerm -> m GeneralTerm
Ord GeneralTerm Source #
Instance details Defined in THF.As Methods compare :: GeneralTerm -> GeneralTerm -> Ordering (<) :: GeneralTerm -> GeneralTerm -> Bool (<=) :: GeneralTerm -> GeneralTerm -> Bool (>) :: GeneralTerm -> GeneralTerm -> Bool (>=) :: GeneralTerm -> GeneralTerm -> Bool max :: GeneralTerm -> GeneralTerm -> GeneralTerm min :: GeneralTerm -> GeneralTerm -> GeneralTerm
Show GeneralTerm Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> GeneralTerm -> ShowS show :: GeneralTerm -> String showList :: [GeneralTerm] -> ShowS
Generic GeneralTerm
Instance details Defined in THF.ATC_THF Associated Types type Rep GeneralTerm :: Type -> Type Methods from :: GeneralTerm -> Rep GeneralTerm x to :: Rep GeneralTerm x -> GeneralTerm
GetRange GeneralTerm Source #
Instance details Defined in THF.As Methods getRange :: GeneralTerm -> Range Source # rangeSpan :: GeneralTerm -> [Pos] Source #
FromJSON GeneralTerm
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser GeneralTerm parseJSONList :: Value -> Parser [GeneralTerm]
ToJSON GeneralTerm
Instance details Defined in THF.ATC_THF Methods toJSON :: GeneralTerm -> Value toEncoding :: GeneralTerm -> Encoding toJSONList :: [GeneralTerm] -> Value toEncodingList :: [GeneralTerm] -> Encoding
ShATermConvertible GeneralTerm
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> GeneralTerm -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [GeneralTerm] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, GeneralTerm) fromShATermList' :: Int -> ATermTable -> (ATermTable, [GeneralTerm])
Pretty GeneralTerm Source #
Instance details Defined in THF.PrintTHF Methods pretty :: GeneralTerm -> Doc Source # pretties :: [GeneralTerm] -> Doc Source #
type Rep GeneralTerm
Instance details Defined in THF.ATC_THF type Rep GeneralTerm = D1 ('MetaData "GeneralTerm" "THF.As" "main" 'False) (C1 ('MetaCons "GT_General_Data" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralData)) :+: (C1 ('MetaCons "GT_General_Data_Term" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralData) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralTerm)) :+: C1 ('MetaCons "GT_General_List" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralList))))

data GeneralData Source #

Constructors

GD_Atomic_Word AtomicWord
GD_Variable Token
GD_Number Number
GD_Distinct_Object Token
GD_Formula_Data FormulaData
GD_Bind Token FormulaData
GD_General_Function GeneralFunction

Instances

Instances details

Eq GeneralData Source #
Instance details Defined in THF.As Methods (==) :: GeneralData -> GeneralData -> Bool (/=) :: GeneralData -> GeneralData -> Bool
Data GeneralData Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GeneralData -> c GeneralData gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GeneralData toConstr :: GeneralData -> Constr dataTypeOf :: GeneralData -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GeneralData) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GeneralData) gmapT :: (forall b. Data b => b -> b) -> GeneralData -> GeneralData gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GeneralData -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GeneralData -> r gmapQ :: (forall d. Data d => d -> u) -> GeneralData -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> GeneralData -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> GeneralData -> m GeneralData gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralData -> m GeneralData gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralData -> m GeneralData
Ord GeneralData Source #
Instance details Defined in THF.As Methods compare :: GeneralData -> GeneralData -> Ordering (<) :: GeneralData -> GeneralData -> Bool (<=) :: GeneralData -> GeneralData -> Bool (>) :: GeneralData -> GeneralData -> Bool (>=) :: GeneralData -> GeneralData -> Bool max :: GeneralData -> GeneralData -> GeneralData min :: GeneralData -> GeneralData -> GeneralData
Show GeneralData Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> GeneralData -> ShowS show :: GeneralData -> String showList :: [GeneralData] -> ShowS
Generic GeneralData
Instance details Defined in THF.ATC_THF Associated Types type Rep GeneralData :: Type -> Type Methods from :: GeneralData -> Rep GeneralData x to :: Rep GeneralData x -> GeneralData
GetRange GeneralData Source #
Instance details Defined in THF.As Methods getRange :: GeneralData -> Range Source # rangeSpan :: GeneralData -> [Pos] Source #
FromJSON GeneralData
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser GeneralData parseJSONList :: Value -> Parser [GeneralData]
ToJSON GeneralData
Instance details Defined in THF.ATC_THF Methods toJSON :: GeneralData -> Value toEncoding :: GeneralData -> Encoding toJSONList :: [GeneralData] -> Value toEncodingList :: [GeneralData] -> Encoding
ShATermConvertible GeneralData
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> GeneralData -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [GeneralData] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, GeneralData) fromShATermList' :: Int -> ATermTable -> (ATermTable, [GeneralData])
Pretty GeneralData Source #
Instance details Defined in THF.PrintTHF Methods pretty :: GeneralData -> Doc Source # pretties :: [GeneralData] -> Doc Source #
type Rep GeneralData
Instance details Defined in THF.ATC_THF type Rep GeneralData = D1 ('MetaData "GeneralData" "THF.As" "main" 'False) ((C1 ('MetaCons "GD_Atomic_Word" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AtomicWord)) :+: (C1 ('MetaCons "GD_Variable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "GD_Number" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Number)))) :+: ((C1 ('MetaCons "GD_Distinct_Object" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "GD_Formula_Data" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FormulaData))) :+: (C1 ('MetaCons "GD_Bind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FormulaData)) :+: C1 ('MetaCons "GD_General_Function" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralFunction)))))

data GeneralFunction Source #

Constructors

GF_General_Function AtomicWord GeneralTerms

Instances

Instances details

Eq GeneralFunction Source #
Instance details Defined in THF.As Methods (==) :: GeneralFunction -> GeneralFunction -> Bool (/=) :: GeneralFunction -> GeneralFunction -> Bool
Data GeneralFunction Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GeneralFunction -> c GeneralFunction gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GeneralFunction toConstr :: GeneralFunction -> Constr dataTypeOf :: GeneralFunction -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GeneralFunction) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GeneralFunction) gmapT :: (forall b. Data b => b -> b) -> GeneralFunction -> GeneralFunction gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GeneralFunction -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GeneralFunction -> r gmapQ :: (forall d. Data d => d -> u) -> GeneralFunction -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> GeneralFunction -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> GeneralFunction -> m GeneralFunction gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralFunction -> m GeneralFunction gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralFunction -> m GeneralFunction
Ord GeneralFunction Source #
Instance details Defined in THF.As Methods compare :: GeneralFunction -> GeneralFunction -> Ordering (<) :: GeneralFunction -> GeneralFunction -> Bool (<=) :: GeneralFunction -> GeneralFunction -> Bool (>) :: GeneralFunction -> GeneralFunction -> Bool (>=) :: GeneralFunction -> GeneralFunction -> Bool max :: GeneralFunction -> GeneralFunction -> GeneralFunction min :: GeneralFunction -> GeneralFunction -> GeneralFunction
Show GeneralFunction Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> GeneralFunction -> ShowS show :: GeneralFunction -> String showList :: [GeneralFunction] -> ShowS
Generic GeneralFunction
Instance details Defined in THF.ATC_THF Associated Types type Rep GeneralFunction :: Type -> Type Methods from :: GeneralFunction -> Rep GeneralFunction x to :: Rep GeneralFunction x -> GeneralFunction
GetRange GeneralFunction Source #
Instance details Defined in THF.As Methods getRange :: GeneralFunction -> Range Source # rangeSpan :: GeneralFunction -> [Pos] Source #
FromJSON GeneralFunction
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser GeneralFunction parseJSONList :: Value -> Parser [GeneralFunction]
ToJSON GeneralFunction
Instance details Defined in THF.ATC_THF Methods toJSON :: GeneralFunction -> Value toEncoding :: GeneralFunction -> Encoding toJSONList :: [GeneralFunction] -> Value toEncodingList :: [GeneralFunction] -> Encoding
ShATermConvertible GeneralFunction
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> GeneralFunction -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [GeneralFunction] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, GeneralFunction) fromShATermList' :: Int -> ATermTable -> (ATermTable, [GeneralFunction])
Pretty GeneralFunction Source #
Instance details Defined in THF.PrintTHF Methods pretty :: GeneralFunction -> Doc Source # pretties :: [GeneralFunction] -> Doc Source #
type Rep GeneralFunction
Instance details Defined in THF.ATC_THF type Rep GeneralFunction = D1 ('MetaData "GeneralFunction" "THF.As" "main" 'False) (C1 ('MetaCons "GF_General_Function" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AtomicWord) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GeneralTerms)))

data FormulaData Source #

Constructors

THF_Formula THFFormula

Instances

Instances details

Eq FormulaData Source #
Instance details Defined in THF.As Methods (==) :: FormulaData -> FormulaData -> Bool (/=) :: FormulaData -> FormulaData -> Bool
Data FormulaData Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FormulaData -> c FormulaData gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FormulaData toConstr :: FormulaData -> Constr dataTypeOf :: FormulaData -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FormulaData) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FormulaData) gmapT :: (forall b. Data b => b -> b) -> FormulaData -> FormulaData gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FormulaData -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FormulaData -> r gmapQ :: (forall d. Data d => d -> u) -> FormulaData -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FormulaData -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FormulaData -> m FormulaData gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FormulaData -> m FormulaData gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FormulaData -> m FormulaData
Ord FormulaData Source #
Instance details Defined in THF.As Methods compare :: FormulaData -> FormulaData -> Ordering (<) :: FormulaData -> FormulaData -> Bool (<=) :: FormulaData -> FormulaData -> Bool (>) :: FormulaData -> FormulaData -> Bool (>=) :: FormulaData -> FormulaData -> Bool max :: FormulaData -> FormulaData -> FormulaData min :: FormulaData -> FormulaData -> FormulaData
Show FormulaData Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> FormulaData -> ShowS show :: FormulaData -> String showList :: [FormulaData] -> ShowS
Generic FormulaData
Instance details Defined in THF.ATC_THF Associated Types type Rep FormulaData :: Type -> Type Methods from :: FormulaData -> Rep FormulaData x to :: Rep FormulaData x -> FormulaData
GetRange FormulaData Source #
Instance details Defined in THF.As Methods getRange :: FormulaData -> Range Source # rangeSpan :: FormulaData -> [Pos] Source #
FromJSON FormulaData
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser FormulaData parseJSONList :: Value -> Parser [FormulaData]
ToJSON FormulaData
Instance details Defined in THF.ATC_THF Methods toJSON :: FormulaData -> Value toEncoding :: FormulaData -> Encoding toJSONList :: [FormulaData] -> Value toEncodingList :: [FormulaData] -> Encoding
ShATermConvertible FormulaData
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> FormulaData -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FormulaData] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FormulaData) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FormulaData])
Pretty FormulaData Source #
Instance details Defined in THF.PrintTHF Methods pretty :: FormulaData -> Doc Source # pretties :: [FormulaData] -> Doc Source #
type Rep FormulaData
Instance details Defined in THF.ATC_THF type Rep FormulaData = D1 ('MetaData "FormulaData" "THF.As" "main" 'False) (C1 ('MetaCons "THF_Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 THFFormula)))

type GeneralList = GeneralTerms Source #

type GeneralTerms = [GeneralTerm] Source #

data Name Source #

Constructors

N_Atomic_Word AtomicWord
N_Integer Token
T0N_Unsigned_Integer Token

Instances

Instances details

Eq Name Source #
Instance details Defined in THF.As Methods (==) :: Name -> Name -> Bool (/=) :: Name -> Name -> Bool
Data Name Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Name -> c Name gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name toConstr :: Name -> Constr dataTypeOf :: Name -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Name) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name) gmapT :: (forall b. Data b => b -> b) -> Name -> Name gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r gmapQ :: (forall d. Data d => d -> u) -> Name -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name
Ord Name Source #
Instance details Defined in THF.As Methods compare :: Name -> Name -> Ordering (<) :: Name -> Name -> Bool (<=) :: Name -> Name -> Bool (>) :: Name -> Name -> Bool (>=) :: Name -> Name -> Bool max :: Name -> Name -> Name min :: Name -> Name -> Name
Show Name Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> Name -> ShowS show :: Name -> String showList :: [Name] -> ShowS
Generic Name
Instance details Defined in THF.ATC_THF Associated Types type Rep Name :: Type -> Type Methods from :: Name -> Rep Name x to :: Rep Name x -> Name
GetRange Name Source #
Instance details Defined in THF.As Methods getRange :: Name -> Range Source # rangeSpan :: Name -> [Pos] Source #
FromJSON Name
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser Name parseJSONList :: Value -> Parser [Name]
ToJSON Name
Instance details Defined in THF.ATC_THF Methods toJSON :: Name -> Value toEncoding :: Name -> Encoding toJSONList :: [Name] -> Value toEncodingList :: [Name] -> Encoding
ShATermConvertible Name
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> Name -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Name] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Name) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Name])
Pretty Name Source #
Instance details Defined in THF.PrintTHF Methods pretty :: Name -> Doc Source # pretties :: [Name] -> Doc Source #
type Rep Name
Instance details Defined in THF.ATC_THF type Rep Name = D1 ('MetaData "Name" "THF.As" "main" 'False) (C1 ('MetaCons "N_Atomic_Word" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AtomicWord)) :+: (C1 ('MetaCons "N_Integer" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "T0N_Unsigned_Integer" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token))))

data AtomicWord Source #

Constructors

A_Lower_Word Token
A_Single_Quoted Token

Instances

Instances details

Eq AtomicWord Source #
Instance details Defined in THF.As Methods (==) :: AtomicWord -> AtomicWord -> Bool (/=) :: AtomicWord -> AtomicWord -> Bool
Data AtomicWord Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AtomicWord -> c AtomicWord gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AtomicWord toConstr :: AtomicWord -> Constr dataTypeOf :: AtomicWord -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AtomicWord) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AtomicWord) gmapT :: (forall b. Data b => b -> b) -> AtomicWord -> AtomicWord gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AtomicWord -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AtomicWord -> r gmapQ :: (forall d. Data d => d -> u) -> AtomicWord -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> AtomicWord -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AtomicWord -> m AtomicWord
Ord AtomicWord Source #
Instance details Defined in THF.As Methods compare :: AtomicWord -> AtomicWord -> Ordering (<) :: AtomicWord -> AtomicWord -> Bool (<=) :: AtomicWord -> AtomicWord -> Bool (>) :: AtomicWord -> AtomicWord -> Bool (>=) :: AtomicWord -> AtomicWord -> Bool max :: AtomicWord -> AtomicWord -> AtomicWord min :: AtomicWord -> AtomicWord -> AtomicWord
Show AtomicWord Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> AtomicWord -> ShowS show :: AtomicWord -> String showList :: [AtomicWord] -> ShowS
Generic AtomicWord
Instance details Defined in THF.ATC_THF Associated Types type Rep AtomicWord :: Type -> Type Methods from :: AtomicWord -> Rep AtomicWord x to :: Rep AtomicWord x -> AtomicWord
GetRange AtomicWord Source #
Instance details Defined in THF.As Methods getRange :: AtomicWord -> Range Source # rangeSpan :: AtomicWord -> [Pos] Source #
FromJSON AtomicWord
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser AtomicWord parseJSONList :: Value -> Parser [AtomicWord]
ToJSON AtomicWord
Instance details Defined in THF.ATC_THF Methods toJSON :: AtomicWord -> Value toEncoding :: AtomicWord -> Encoding toJSONList :: [AtomicWord] -> Value toEncodingList :: [AtomicWord] -> Encoding
ShATermConvertible AtomicWord
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> AtomicWord -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [AtomicWord] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, AtomicWord) fromShATermList' :: Int -> ATermTable -> (ATermTable, [AtomicWord])
Pretty AtomicWord Source #
Instance details Defined in THF.PrintTHF Methods pretty :: AtomicWord -> Doc Source # pretties :: [AtomicWord] -> Doc Source #
type Rep AtomicWord
Instance details Defined in THF.ATC_THF type Rep AtomicWord = D1 ('MetaData "AtomicWord" "THF.As" "main" 'False) (C1 ('MetaCons "A_Lower_Word" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "A_Single_Quoted" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)))

data Number Source #

Constructors

Num_Integer Token
Num_Rational Token
Num_Real Token

Instances

Instances details

Eq Number Source #
Instance details Defined in THF.As Methods (==) :: Number -> Number -> Bool (/=) :: Number -> Number -> Bool
Data Number Source #
Instance details Defined in THF.As Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Number -> c Number gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Number toConstr :: Number -> Constr dataTypeOf :: Number -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Number) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Number) gmapT :: (forall b. Data b => b -> b) -> Number -> Number gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Number -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Number -> r gmapQ :: (forall d. Data d => d -> u) -> Number -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Number -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Number -> m Number gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Number -> m Number gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Number -> m Number
Ord Number Source #
Instance details Defined in THF.As Methods compare :: Number -> Number -> Ordering (<) :: Number -> Number -> Bool (<=) :: Number -> Number -> Bool (>) :: Number -> Number -> Bool (>=) :: Number -> Number -> Bool max :: Number -> Number -> Number min :: Number -> Number -> Number
Show Number Source #
Instance details Defined in THF.As Methods showsPrec :: Int -> Number -> ShowS show :: Number -> String showList :: [Number] -> ShowS
Generic Number
Instance details Defined in THF.ATC_THF Associated Types type Rep Number :: Type -> Type Methods from :: Number -> Rep Number x to :: Rep Number x -> Number
GetRange Number Source #
Instance details Defined in THF.As Methods getRange :: Number -> Range Source # rangeSpan :: Number -> [Pos] Source #
FromJSON Number
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser Number parseJSONList :: Value -> Parser [Number]
ToJSON Number
Instance details Defined in THF.ATC_THF Methods toJSON :: Number -> Value toEncoding :: Number -> Encoding toJSONList :: [Number] -> Value toEncodingList :: [Number] -> Encoding
ShATermConvertible Number
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> Number -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Number] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Number) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Number])
Pretty Number Source #
Instance details Defined in THF.PrintTHF Methods pretty :: Number -> Doc Source # pretties :: [Number] -> Doc Source #
type Rep Number
Instance details Defined in THF.ATC_THF type Rep Number = D1 ('MetaData "Number" "THF.As" "main" 'False) (C1 ('MetaCons "Num_Integer" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: (C1 ('MetaCons "Num_Rational" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token)) :+: C1 ('MetaCons "Num_Real" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Token))))

TA_Term Term
TA_THF_Conn_Term THFConnTerm
TA_Defined_Type DefinedType
TA_Defined_Plain_Formula DefinedPlainFormula
TA_System_Type Token
TA_System_Atomic_Formula SystemTerm
T0A_Constant Constant
T0A_Defined_Constant Token
T0A_System_Constant Token
T0A_Variable Token

Suc
Unp
Sap
Esa
Sat
Fsa
Thm
Eqv
Tac
Wec
Eth
Tau
Wtc
Wth
Cax
Sca
Tca
Wca
Cup
Csp
Ecs
Csa
Cth
Ceq
Unc
Wcc
Ect
Fun
Uns
Wuc
Wct
Scc
Uca
Noc

Suc
Unp
Sap
Esa
Sat
Fsa
Thm
Eqv
Tac
Wec
Eth
Tau
Wtc
Wth
Cax
Sca
Tca
Wca
Cup
Csp
Ecs
Csa
Cth
Ceq
Unc
Wcc
Ect
Fun
Uns
Wuc
Wct
Scc
Uca
Noc

Suc
Unp
Sap
Esa
Sat
Fsa
Thm
Eqv
Tac
Wec
Eth
Tau
Wtc
Wth
Cax
Sca
Tca
Wca
Cup
Csp
Ecs
Csa
Cth
Ceq
Unc
Wcc
Ect
Fun
Uns
Wuc
Wct
Scc
Uca
Noc