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

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