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

Description

Data structures and functions for thf THF Signatures. Note: Most of the implenentations support only THF0.

Documentation

type MorphismTHF = DefaultMorphism SignTHF Source #

data SignTHF Source #

Constructors

Sign
Fields types :: TypeMap consts :: ConstMap symbols :: SymbolMap

Instances

Instances details

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

type TypeMap = Map Constant TypeInfo Source #

type ConstMap = Map Constant ConstInfo Source #

type SymbolMap = Map Constant SymbolTHF Source #

data TypeInfo Source #

Constructors

TypeInfo
Fields typeId :: Constant typeName :: Name typeKind :: Kind typeAnno :: Annotations

Instances

Instances details

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

data ConstInfo Source #

Constructors

ConstInfo
Fields constId :: Constant constName :: Name constType :: Type constAnno :: Annotations

Instances

Instances details

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

emptySign :: SignTHF Source #

type EitherMap c x = Map c (Either x Diagnosis) Source #

toEitherLeftMap :: Map c x -> EitherMap c x Source #

eitherMapHasDiagnosis :: EitherMap c x -> Bool Source #

eitherMapGetDiagnosis :: EitherMap c x -> [Diagnosis] Source #

eitherMapGetMap :: EitherMap c x -> Map c x Source #

genRes :: EitherMap c x -> Either (Map c x) [Diagnosis] Source #

sigUnion :: SignTHF -> SignTHF -> Result SignTHF Source #

typeMapUnion :: TypeMap -> TypeMap -> Either TypeMap [Diagnosis] Source #

constMapUnion :: ConstMap -> ConstMap -> Either ConstMap [Diagnosis] Source #

symbolMapUnion :: SymbolMap -> SymbolMap -> Either SymbolMap [Diagnosis] Source #

unite :: (Ord c, Eq x, Show x) => String -> EitherMap c x -> EitherMap c x -> EitherMap c x Source #

sigDiff :: SignTHF -> SignTHF -> Result SignTHF Source #

diff :: (Ord c, Eq x) => Map c x -> Map c x -> Map c x Source #

sigIntersect :: SignTHF -> SignTHF -> Result SignTHF Source #

typeMapIntersect :: TypeMap -> TypeMap -> Either TypeMap [Diagnosis] Source #

constMapIntersect :: ConstMap -> ConstMap -> Either ConstMap [Diagnosis] Source #

symbolMapIntersect :: SymbolMap -> SymbolMap -> Either SymbolMap [Diagnosis] Source #

intersect :: (Ord c, Eq x, Show x) => String -> EitherMap c x -> EitherMap c x -> EitherMap c x Source #