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.Cons

Description

Data structures and functions used in Logic_THF and HasCASL2THF. Note: Some of the implenentations depend on the THF0 Syntax.

Documentation

data BasicSpecTHF Source #

Constructors

BasicSpecTHF [TPTP_THF]

Instances

Instances details

Eq BasicSpecTHF Source #
Instance details Defined in THF.Cons Methods (==) :: BasicSpecTHF -> BasicSpecTHF -> Bool (/=) :: BasicSpecTHF -> BasicSpecTHF -> Bool
Data BasicSpecTHF Source #
Instance details Defined in THF.Cons Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BasicSpecTHF -> c BasicSpecTHF gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BasicSpecTHF toConstr :: BasicSpecTHF -> Constr dataTypeOf :: BasicSpecTHF -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BasicSpecTHF) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BasicSpecTHF) gmapT :: (forall b. Data b => b -> b) -> BasicSpecTHF -> BasicSpecTHF gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BasicSpecTHF -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BasicSpecTHF -> r gmapQ :: (forall d. Data d => d -> u) -> BasicSpecTHF -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BasicSpecTHF -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BasicSpecTHF -> m BasicSpecTHF gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BasicSpecTHF -> m BasicSpecTHF gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BasicSpecTHF -> m BasicSpecTHF
Ord BasicSpecTHF Source #
Instance details Defined in THF.Cons Methods compare :: BasicSpecTHF -> BasicSpecTHF -> Ordering (<) :: BasicSpecTHF -> BasicSpecTHF -> Bool (<=) :: BasicSpecTHF -> BasicSpecTHF -> Bool (>) :: BasicSpecTHF -> BasicSpecTHF -> Bool (>=) :: BasicSpecTHF -> BasicSpecTHF -> Bool max :: BasicSpecTHF -> BasicSpecTHF -> BasicSpecTHF min :: BasicSpecTHF -> BasicSpecTHF -> BasicSpecTHF
Show BasicSpecTHF Source #
Instance details Defined in THF.Cons Methods showsPrec :: Int -> BasicSpecTHF -> ShowS show :: BasicSpecTHF -> String showList :: [BasicSpecTHF] -> ShowS
Generic BasicSpecTHF
Instance details Defined in THF.ATC_THF Associated Types type Rep BasicSpecTHF :: Type -> Type Methods from :: BasicSpecTHF -> Rep BasicSpecTHF x to :: Rep BasicSpecTHF x -> BasicSpecTHF
Semigroup BasicSpecTHF
Instance details Defined in THF.Logic_THF Methods (<>) :: BasicSpecTHF -> BasicSpecTHF -> BasicSpecTHF # sconcat :: NonEmpty BasicSpecTHF -> BasicSpecTHF stimes :: Integral b => b -> BasicSpecTHF -> BasicSpecTHF
Monoid BasicSpecTHF
Instance details Defined in THF.Logic_THF Methods mempty :: BasicSpecTHF mappend :: BasicSpecTHF -> BasicSpecTHF -> BasicSpecTHF mconcat :: [BasicSpecTHF] -> BasicSpecTHF
GetRange BasicSpecTHF Source #
Instance details Defined in THF.Cons Methods getRange :: BasicSpecTHF -> Range Source # rangeSpan :: BasicSpecTHF -> [Pos] Source #
FromJSON BasicSpecTHF
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser BasicSpecTHF parseJSONList :: Value -> Parser [BasicSpecTHF]
ToJSON BasicSpecTHF
Instance details Defined in THF.ATC_THF Methods toJSON :: BasicSpecTHF -> Value toEncoding :: BasicSpecTHF -> Encoding toJSONList :: [BasicSpecTHF] -> Value toEncodingList :: [BasicSpecTHF] -> Encoding
ShATermConvertible BasicSpecTHF
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> BasicSpecTHF -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [BasicSpecTHF] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, BasicSpecTHF) fromShATermList' :: Int -> ATermTable -> (ATermTable, [BasicSpecTHF])
Pretty BasicSpecTHF Source #
Instance details Defined in THF.Print Methods pretty :: BasicSpecTHF -> Doc Source # pretties :: [BasicSpecTHF] -> Doc Source #
ProjectSublogic THFSl BasicSpecTHF Source #
Instance details Defined in THF.Logic_THF Methods projectSublogic :: THFSl -> BasicSpecTHF -> BasicSpecTHF Source #
MinSublogic THFSl BasicSpecTHF Source #
Instance details Defined in THF.Logic_THF Methods minSublogic :: BasicSpecTHF -> THFSl Source #
Syntax THF BasicSpecTHF SymbolTHF () () Source #
Instance details Defined in THF.Logic_THF Methods parsersAndPrinters :: THF -> Map String (PrefixMap -> AParser st BasicSpecTHF, BasicSpecTHF -> Doc) Source # parse_basic_spec :: THF -> Maybe (PrefixMap -> AParser st BasicSpecTHF) Source # parseSingleSymbItem :: THF -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: THF -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: THF -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: THF -> BasicSpecTHF -> Item Source # symb_items_name :: THF -> () -> [String] 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 BasicSpecTHF
Instance details Defined in THF.ATC_THF type Rep BasicSpecTHF = D1 ('MetaData "BasicSpecTHF" "THF.Cons" "main" 'False) (C1 ('MetaCons "BasicSpecTHF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TPTP_THF])))

data SymbolTHF Source #

Constructors

Symbol
Fields symId :: Constant symName :: Name symType :: SymbolType

Instances

Instances details

Eq SymbolTHF Source #
Instance details Defined in THF.Cons Methods (==) :: SymbolTHF -> SymbolTHF -> Bool (/=) :: SymbolTHF -> SymbolTHF -> Bool
Data SymbolTHF Source #
Instance details Defined in THF.Cons Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbolTHF -> c SymbolTHF gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbolTHF toConstr :: SymbolTHF -> Constr dataTypeOf :: SymbolTHF -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SymbolTHF) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbolTHF) gmapT :: (forall b. Data b => b -> b) -> SymbolTHF -> SymbolTHF gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbolTHF -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbolTHF -> r gmapQ :: (forall d. Data d => d -> u) -> SymbolTHF -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbolTHF -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbolTHF -> m SymbolTHF gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbolTHF -> m SymbolTHF gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbolTHF -> m SymbolTHF
Ord SymbolTHF Source #
Instance details Defined in THF.Cons Methods compare :: SymbolTHF -> SymbolTHF -> Ordering (<) :: SymbolTHF -> SymbolTHF -> Bool (<=) :: SymbolTHF -> SymbolTHF -> Bool (>) :: SymbolTHF -> SymbolTHF -> Bool (>=) :: SymbolTHF -> SymbolTHF -> Bool max :: SymbolTHF -> SymbolTHF -> SymbolTHF min :: SymbolTHF -> SymbolTHF -> SymbolTHF
Show SymbolTHF Source #
Instance details Defined in THF.Cons Methods showsPrec :: Int -> SymbolTHF -> ShowS show :: SymbolTHF -> String showList :: [SymbolTHF] -> ShowS
Generic SymbolTHF
Instance details Defined in THF.ATC_THF Associated Types type Rep SymbolTHF :: Type -> Type Methods from :: SymbolTHF -> Rep SymbolTHF x to :: Rep SymbolTHF x -> SymbolTHF
GetRange SymbolTHF Source #
Instance details Defined in THF.Cons Methods getRange :: SymbolTHF -> Range Source # rangeSpan :: SymbolTHF -> [Pos] Source #
FromJSON SymbolTHF
Instance details Defined in THF.ATC_THF Methods parseJSON :: Value -> Parser SymbolTHF parseJSONList :: Value -> Parser [SymbolTHF]
ToJSON SymbolTHF
Instance details Defined in THF.ATC_THF Methods toJSON :: SymbolTHF -> Value toEncoding :: SymbolTHF -> Encoding toJSONList :: [SymbolTHF] -> Value toEncodingList :: [SymbolTHF] -> Encoding
ShATermConvertible SymbolTHF
Instance details Defined in THF.ATC_THF Methods toShATermAux :: ATermTable -> SymbolTHF -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SymbolTHF] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbolTHF) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SymbolTHF])
Pretty SymbolTHF Source #
Instance details Defined in THF.Print Methods pretty :: SymbolTHF -> Doc Source # pretties :: [SymbolTHF] -> Doc Source #
ProjectSublogicM THFSl SymbolTHF Source #
Instance details Defined in THF.Logic_THF Methods projectSublogicM :: THFSl -> SymbolTHF -> Maybe SymbolTHF Source #
MinSublogic THFSl SymbolTHF Source #
Instance details Defined in THF.Logic_THF Methods minSublogic :: SymbolTHF -> 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 #
Syntax THF BasicSpecTHF SymbolTHF () () Source #
Instance details Defined in THF.Logic_THF Methods parsersAndPrinters :: THF -> Map String (PrefixMap -> AParser st BasicSpecTHF, BasicSpecTHF -> Doc) Source # parse_basic_spec :: THF -> Maybe (PrefixMap -> AParser st BasicSpecTHF) Source # parseSingleSymbItem :: THF -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: THF -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: THF -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: THF -> BasicSpecTHF -> Item Source # symb_items_name :: THF -> () -> [String] 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 SymbolTHF
Instance details Defined in THF.ATC_THF type Rep SymbolTHF = D1 ('MetaData "SymbolTHF" "THF.Cons" "main" 'False) (C1 ('MetaCons "Symbol" 'PrefixI 'True) (S1 ('MetaSel ('Just "symId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Constant) :: (S1 ('MetaSel ('Just "symName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Just "symType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SymbolType))))

data SymbolType Source #

Constructors

ST_Const Type
ST_Type Kind

Instances

Instances details

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

data Type Source #

Constructors

TType
OType
IType
MapType Type Type
ProdType [Type]
CType Constant
SType Token
VType Token
ParType Type

Instances

Instances details

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

data Kind Source #

Constructors

Kind

Instances

Instances details

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