Copyright	(c) Stef Joosten Christian Maeder DFKI GmbH 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	Safe

Adl.Sign

Description

Documentation

type RelMap = Map Id (Set RelType) Source #

data Sign Source #

Constructors

Sign
Fields rels :: RelMap isas :: Rel Concept

Instances

Instances details

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

emptySign :: Sign Source #

closeSign :: Sign -> Sign Source #

isSubSignOf :: Sign -> Sign -> Bool Source #

signUnion :: Sign -> Sign -> Result Sign Source #

data Symbol Source #

Constructors

Con Concept
Rel Relation

Instances

Instances details

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

data SymbolKind Source #

Constructors

ConK
RelK

Instances

Instances details

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

sym_kind :: Symbol -> SymbolKind Source #

conceptToId :: Concept -> Id Source #

symName :: Symbol -> Id Source #

data RawSymbol Source #

Constructors

Symbol Symbol
AnId Id

Instances

Instances details

Eq RawSymbol Source #
Instance details Defined in Adl.Sign Methods (==) :: RawSymbol -> RawSymbol -> Bool (/=) :: RawSymbol -> RawSymbol -> Bool
Data RawSymbol Source #
Instance details Defined in Adl.Sign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RawSymbol -> c RawSymbol gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RawSymbol toConstr :: RawSymbol -> Constr dataTypeOf :: RawSymbol -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RawSymbol) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RawSymbol) gmapT :: (forall b. Data b => b -> b) -> RawSymbol -> RawSymbol gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RawSymbol -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RawSymbol -> r gmapQ :: (forall d. Data d => d -> u) -> RawSymbol -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RawSymbol -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
Ord RawSymbol Source #
Instance details Defined in Adl.Sign Methods compare :: RawSymbol -> RawSymbol -> Ordering (<) :: RawSymbol -> RawSymbol -> Bool (<=) :: RawSymbol -> RawSymbol -> Bool (>) :: RawSymbol -> RawSymbol -> Bool (>=) :: RawSymbol -> RawSymbol -> Bool max :: RawSymbol -> RawSymbol -> RawSymbol min :: RawSymbol -> RawSymbol -> RawSymbol
Show RawSymbol Source #
Instance details Defined in Adl.Sign Methods showsPrec :: Int -> RawSymbol -> ShowS show :: RawSymbol -> String showList :: [RawSymbol] -> ShowS
Generic RawSymbol
Instance details Defined in Adl.ATC_Adl Associated Types type Rep RawSymbol :: Type -> Type Methods from :: RawSymbol -> Rep RawSymbol x to :: Rep RawSymbol x -> RawSymbol
GetRange RawSymbol Source #
Instance details Defined in Adl.Sign Methods getRange :: RawSymbol -> Range Source # rangeSpan :: RawSymbol -> [Pos] Source #
FromJSON RawSymbol
Instance details Defined in Adl.ATC_Adl Methods parseJSON :: Value -> Parser RawSymbol parseJSONList :: Value -> Parser [RawSymbol]
ToJSON RawSymbol
Instance details Defined in Adl.ATC_Adl Methods toJSON :: RawSymbol -> Value toEncoding :: RawSymbol -> Encoding toJSONList :: [RawSymbol] -> Value toEncodingList :: [RawSymbol] -> Encoding
ShATermConvertible RawSymbol
Instance details Defined in Adl.ATC_Adl Methods toShATermAux :: ATermTable -> RawSymbol -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RawSymbol] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RawSymbol) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RawSymbol])
Pretty RawSymbol Source #
Instance details Defined in Adl.Sign Methods pretty :: RawSymbol -> Doc Source # pretties :: [RawSymbol] -> Doc Source #
StaticAnalysis Adl Context Sen () () Sign Morphism Symbol RawSymbol Source #
Instance details Defined in Adl.Logic_Adl Methods basic_analysis :: Adl -> Maybe ((Context, Sign, GlobalAnnos) -> Result (Context, ExtSign Sign Symbol, [Named Sen])) Source # sen_analysis :: Adl -> Maybe ((Context, Sign, Sen) -> Result Sen) Source # extBasicAnalysis :: Adl -> IRI -> LibName -> Context -> Sign -> GlobalAnnos -> Result (Context, ExtSign Sign Symbol, [Named Sen]) Source # stat_symb_map_items :: Adl -> Sign -> Maybe Sign -> [()] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Adl -> Sign -> [()] -> Result [RawSymbol] Source # convertTheory :: Adl -> Maybe ((Sign, [Named Sen]) -> Context) Source # ensures_amalgamability :: Adl -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Adl -> Morphism -> [Named Sen] -> Result (Sign, [Named Sen]) Source # signature_colimit :: Adl -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: Adl -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sen]) Source # symbol_to_raw :: Adl -> Symbol -> RawSymbol Source # id_to_raw :: Adl -> Id -> RawSymbol Source # matches :: Adl -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Adl -> Sign Source # add_symb_to_sign :: Adl -> Sign -> Symbol -> Result Sign Source # signature_union :: Adl -> Sign -> Sign -> Result Sign Source # signatureDiff :: Adl -> Sign -> Sign -> Result Sign Source # intersection :: Adl -> Sign -> Sign -> Result Sign Source # final_union :: Adl -> Sign -> Sign -> Result Sign Source # morphism_union :: Adl -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: Adl -> Sign -> Sign -> Bool Source # subsig_inclusion :: Adl -> Sign -> Sign -> Result Morphism Source # generated_sign :: Adl -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: Adl -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: Adl -> EndoMap RawSymbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: Adl -> EndoMap RawSymbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: Adl -> Morphism -> Bool Source # is_injective :: Adl -> Morphism -> Bool Source # theory_to_taxonomy :: Adl -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sen] -> Result MMiSSOntology Source # corresp2th :: Adl -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sen], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Adl -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Adl -> [IRI] -> (Sign, [Named Sen]) -> Result (Sign, [Named Sen]) Source #
Logic Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree Source #
Instance details Defined in Adl.Logic_Adl Methods parse_basic_sen :: Adl -> Maybe (Context -> AParser st Sen) Source # stability :: Adl -> Stability Source # data_logic :: Adl -> Maybe AnyLogic Source # top_sublogic :: Adl -> () Source # all_sublogics :: Adl -> [()] Source # bottomSublogic :: Adl -> Maybe () Source # sublogicDimensions :: Adl -> [[()]] Source # parseSublogic :: Adl -> String -> Maybe () Source # proj_sublogic_epsilon :: Adl -> () -> Sign -> Morphism Source # provers :: Adl -> [Prover Sign Sen Morphism () ProofTree] Source # default_prover :: Adl -> String Source # cons_checkers :: Adl -> [ConsChecker Sign Sen () Morphism ProofTree] Source # conservativityCheck :: Adl -> [ConservativityChecker Sign Sen Morphism] Source # empty_proof_tree :: Adl -> ProofTree Source # syntaxTable :: Adl -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: Adl -> Maybe OMCD Source # export_symToOmdoc :: Adl -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: Adl -> NameMap Symbol -> Sen -> Result TCorOMElement Source # export_theoryToOmdoc :: Adl -> SigMap Symbol -> Sign -> [Named Sen] -> Result [TCElement] Source # omdocToSym :: Adl -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: Adl -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sen)) Source # addOMadtToTheory :: Adl -> SigMapI Symbol -> (Sign, [Named Sen]) -> [[OmdADT]] -> Result (Sign, [Named Sen]) Source # addOmdocToTheory :: Adl -> SigMapI Symbol -> (Sign, [Named Sen]) -> [TCElement] -> Result (Sign, [Named Sen]) Source # sublogicOfTheo :: Adl -> (Sign, [Sen]) -> () Source #
Comorphism Adl2CASL Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Adl2CASL Methods sourceLogic :: Adl2CASL -> Adl Source # sourceSublogic :: Adl2CASL -> () Source # sourceSublogicLossy :: Adl2CASL -> () Source # minSourceTheory :: Adl2CASL -> Maybe (LibName, String) Source # targetLogic :: Adl2CASL -> CASL Source # mapSublogic :: Adl2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Adl2CASL -> Morphism -> Result CASLMor Source # map_sentence :: Adl2CASL -> Sign -> Sen -> Result CASLFORMULA Source # map_symbol :: Adl2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: Adl2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source # is_model_transportable :: Adl2CASL -> Bool Source # has_model_expansion :: Adl2CASL -> Bool Source # is_weakly_amalgamable :: Adl2CASL -> Bool Source # constituents :: Adl2CASL -> [String] Source # isInclusionComorphism :: Adl2CASL -> Bool Source # rps :: Adl2CASL -> Bool Source # eps :: Adl2CASL -> Bool Source # isGTC :: Adl2CASL -> Bool Source #
type Rep RawSymbol
Instance details Defined in Adl.ATC_Adl type Rep RawSymbol = D1 ('MetaData "RawSymbol" "Adl.Sign" "main" 'False) (C1 ('MetaCons "Symbol" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)) :+: C1 ('MetaCons "AnId" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id)))

symMatch :: Symbol -> RawSymbol -> Bool Source #

symOf :: Sign -> Set Symbol Source #

data Sen Source #

Constructors

DeclProp Relation RangedProp
Assertion (Maybe RuleKind) Rule

Instances

Instances details

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

printNSen :: Named Sen -> Doc Source #