Copyright	(c) Kristina Sojakova DFKI Bremen 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	k.sojakova@jacobs-university.de
Stability	experimental
Portability	portable
Safe Haskell	Safe

Framework.AS

Description

Documentation

type NAME = IRI Source #

type SIG_NAME = IRI Source #

type MORPH_NAME = IRI Source #

type PATTERN_NAME = Token Source #

data FRAM Source #

Constructors

LF
Isabelle
Maude

Instances

Instances details

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

data LogicDef Source #

Constructors

LogicDef
Fields newlogicName :: NAME meta :: FRAM syntax :: MORPH_NAME models :: MORPH_NAME foundation :: SIG_NAME proofs :: MORPH_NAME patterns :: PATTERN_NAME

Instances

Instances details

Eq LogicDef Source #
Instance details Defined in Framework.AS Methods (==) :: LogicDef -> LogicDef -> Bool (/=) :: LogicDef -> LogicDef -> Bool
Data LogicDef Source #
Instance details Defined in Framework.AS Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LogicDef -> c LogicDef gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LogicDef toConstr :: LogicDef -> Constr dataTypeOf :: LogicDef -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LogicDef) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LogicDef) gmapT :: (forall b. Data b => b -> b) -> LogicDef -> LogicDef gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LogicDef -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LogicDef -> r gmapQ :: (forall d. Data d => d -> u) -> LogicDef -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> LogicDef -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> LogicDef -> m LogicDef gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LogicDef -> m LogicDef gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LogicDef -> m LogicDef
Ord LogicDef Source #
Instance details Defined in Framework.AS Methods compare :: LogicDef -> LogicDef -> Ordering (<) :: LogicDef -> LogicDef -> Bool (<=) :: LogicDef -> LogicDef -> Bool (>) :: LogicDef -> LogicDef -> Bool (>=) :: LogicDef -> LogicDef -> Bool max :: LogicDef -> LogicDef -> LogicDef min :: LogicDef -> LogicDef -> LogicDef
Show LogicDef Source #
Instance details Defined in Framework.AS Methods showsPrec :: Int -> LogicDef -> ShowS show :: LogicDef -> String showList :: [LogicDef] -> ShowS
Generic LogicDef
Instance details Defined in Framework.ATC_Framework Associated Types type Rep LogicDef :: Type -> Type Methods from :: LogicDef -> Rep LogicDef x to :: Rep LogicDef x -> LogicDef
Semigroup LogicDef
Instance details Defined in Framework.Logic_Framework Methods (<>) :: LogicDef -> LogicDef -> LogicDef # sconcat :: NonEmpty LogicDef -> LogicDef stimes :: Integral b => b -> LogicDef -> LogicDef
Monoid LogicDef
Instance details Defined in Framework.Logic_Framework Methods mempty :: LogicDef mappend :: LogicDef -> LogicDef -> LogicDef mconcat :: [LogicDef] -> LogicDef
GetRange LogicDef Source #
Instance details Defined in Framework.AS Methods getRange :: LogicDef -> Range Source # rangeSpan :: LogicDef -> [Pos] Source #
FromJSON LogicDef
Instance details Defined in Framework.ATC_Framework Methods parseJSON :: Value -> Parser LogicDef parseJSONList :: Value -> Parser [LogicDef]
ToJSON LogicDef
Instance details Defined in Framework.ATC_Framework Methods toJSON :: LogicDef -> Value toEncoding :: LogicDef -> Encoding toJSONList :: [LogicDef] -> Value toEncodingList :: [LogicDef] -> Encoding
ShATermConvertible LogicDef
Instance details Defined in Framework.ATC_Framework Methods toShATermAux :: ATermTable -> LogicDef -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [LogicDef] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, LogicDef) fromShATermList' :: Int -> ATermTable -> (ATermTable, [LogicDef])
Pretty LogicDef Source #
Instance details Defined in Framework.AS Methods pretty :: LogicDef -> Doc Source # pretties :: [LogicDef] -> Doc Source #
Sentences Framework () LogicDef Morphism () Source #
Instance details Defined in Framework.Logic_Framework Methods map_sen :: Framework -> Morphism -> () -> Result () Source # simplify_sen :: Framework -> LogicDef -> () -> () Source # negation :: Framework -> () -> Maybe () Source # print_sign :: Framework -> LogicDef -> Doc Source # print_named :: Framework -> Named () -> Doc Source # sym_of :: Framework -> LogicDef -> [Set ()] Source # mostSymsOf :: Framework -> LogicDef -> [()] Source # symmap_of :: Framework -> Morphism -> EndoMap () Source # sym_name :: Framework -> () -> Id Source # sym_label :: Framework -> () -> Maybe String Source # fullSymName :: Framework -> () -> String Source # symKind :: Framework -> () -> String Source # symsOfSen :: Framework -> LogicDef -> () -> [()] Source # pair_symbols :: Framework -> () -> () -> Result () Source #
Syntax Framework LogicDef () () () Source #
Instance details Defined in Framework.Logic_Framework Methods parsersAndPrinters :: Framework -> Map String (PrefixMap -> AParser st LogicDef, LogicDef -> Doc) Source # parse_basic_spec :: Framework -> Maybe (PrefixMap -> AParser st LogicDef) Source # parseSingleSymbItem :: Framework -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: Framework -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: Framework -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: Framework -> LogicDef -> Item Source # symb_items_name :: Framework -> () -> [String] Source #
StaticAnalysis Framework LogicDef () () () LogicDef Morphism () () Source #
Instance details Defined in Framework.Logic_Framework Methods basic_analysis :: Framework -> Maybe ((LogicDef, LogicDef, GlobalAnnos) -> Result (LogicDef, ExtSign LogicDef (), [Named ()])) Source # sen_analysis :: Framework -> Maybe ((LogicDef, LogicDef, ()) -> Result ()) Source # extBasicAnalysis :: Framework -> IRI -> LibName -> LogicDef -> LogicDef -> GlobalAnnos -> Result (LogicDef, ExtSign LogicDef (), [Named ()]) Source # stat_symb_map_items :: Framework -> LogicDef -> Maybe LogicDef -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: Framework -> LogicDef -> [()] -> Result [()] Source # convertTheory :: Framework -> Maybe ((LogicDef, [Named ()]) -> LogicDef) Source # ensures_amalgamability :: Framework -> ([CASLAmalgOpt], Gr LogicDef (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Framework -> Morphism -> [Named ()] -> Result (LogicDef, [Named ()]) Source # signature_colimit :: Framework -> Gr LogicDef (Int, Morphism) -> Result (LogicDef, Map Int Morphism) Source # qualify :: Framework -> SIMPLE_ID -> LibName -> Morphism -> LogicDef -> Result (Morphism, [Named ()]) Source # symbol_to_raw :: Framework -> () -> () Source # id_to_raw :: Framework -> Id -> () Source # matches :: Framework -> () -> () -> Bool Source # empty_signature :: Framework -> LogicDef Source # add_symb_to_sign :: Framework -> LogicDef -> () -> Result LogicDef Source # signature_union :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source # signatureDiff :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source # intersection :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source # final_union :: Framework -> LogicDef -> LogicDef -> Result LogicDef Source # morphism_union :: Framework -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: Framework -> LogicDef -> LogicDef -> Bool Source # subsig_inclusion :: Framework -> LogicDef -> LogicDef -> Result Morphism Source # generated_sign :: Framework -> Set () -> LogicDef -> Result Morphism Source # cogenerated_sign :: Framework -> Set () -> LogicDef -> Result Morphism Source # induced_from_morphism :: Framework -> EndoMap () -> LogicDef -> Result Morphism Source # induced_from_to_morphism :: Framework -> EndoMap () -> ExtSign LogicDef () -> ExtSign LogicDef () -> Result Morphism Source # is_transportable :: Framework -> Morphism -> Bool Source # is_injective :: Framework -> Morphism -> Bool Source # theory_to_taxonomy :: Framework -> TaxoGraphKind -> MMiSSOntology -> LogicDef -> [Named ()] -> Result MMiSSOntology Source # corresp2th :: Framework -> String -> Bool -> LogicDef -> LogicDef -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (LogicDef, [Named ()], LogicDef, LogicDef, EndoMap (), EndoMap ()) Source # equiv2cospan :: Framework -> LogicDef -> LogicDef -> [()] -> [()] -> Result (LogicDef, LogicDef, LogicDef, EndoMap (), EndoMap ()) Source # extract_module :: Framework -> [IRI] -> (LogicDef, [Named ()]) -> Result (LogicDef, [Named ()]) Source #
Logic Framework () LogicDef () () () LogicDef Morphism () () () Source #
Instance details Defined in Framework.Logic_Framework Methods parse_basic_sen :: Framework -> Maybe (LogicDef -> AParser st ()) Source # stability :: Framework -> Stability Source # data_logic :: Framework -> Maybe AnyLogic Source # top_sublogic :: Framework -> () Source # all_sublogics :: Framework -> [()] Source # bottomSublogic :: Framework -> Maybe () Source # sublogicDimensions :: Framework -> [[()]] Source # parseSublogic :: Framework -> String -> Maybe () Source # proj_sublogic_epsilon :: Framework -> () -> LogicDef -> Morphism Source # provers :: Framework -> [Prover LogicDef () Morphism () ()] Source # default_prover :: Framework -> String Source # cons_checkers :: Framework -> [ConsChecker LogicDef () () Morphism ()] Source # conservativityCheck :: Framework -> [ConservativityChecker LogicDef () Morphism] Source # empty_proof_tree :: Framework -> () Source # syntaxTable :: Framework -> LogicDef -> Maybe SyntaxTable Source # omdoc_metatheory :: Framework -> Maybe OMCD Source # export_symToOmdoc :: Framework -> NameMap () -> () -> String -> Result TCElement Source # export_senToOmdoc :: Framework -> NameMap () -> () -> Result TCorOMElement Source # export_theoryToOmdoc :: Framework -> SigMap () -> LogicDef -> [Named ()] -> Result [TCElement] Source # omdocToSym :: Framework -> SigMapI () -> TCElement -> String -> Result () Source # omdocToSen :: Framework -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source # addOMadtToTheory :: Framework -> SigMapI () -> (LogicDef, [Named ()]) -> [[OmdADT]] -> Result (LogicDef, [Named ()]) Source # addOmdocToTheory :: Framework -> SigMapI () -> (LogicDef, [Named ()]) -> [TCElement] -> Result (LogicDef, [Named ()]) Source # sublogicOfTheo :: Framework -> (LogicDef, [()]) -> () Source #
type Rep LogicDef
Instance details Defined in Framework.ATC_Framework type Rep LogicDef = D1 ('MetaData "LogicDef" "Framework.AS" "main" 'False) (C1 ('MetaCons "LogicDef" 'PrefixI 'True) ((S1 ('MetaSel ('Just "newlogicName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NAME) :: (S1 ('MetaSel ('Just "meta") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FRAM) :: S1 ('MetaSel ('Just "syntax") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MORPH_NAME))) :: ((S1 ('MetaSel ('Just "models") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MORPH_NAME) :: S1 ('MetaSel ('Just "foundation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SIG_NAME)) :: (S1 ('MetaSel ('Just "proofs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MORPH_NAME) :: S1 ('MetaSel ('Just "patterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PATTERN_NAME)))))

data ComorphismDef Source #

Constructors

ComorphismDef
Fields newcomorphismName :: NAME metaC :: FRAM source :: SIG_NAME target :: SIG_NAME syntaxC :: MORPH_NAME modelC :: MORPH_NAME proofC :: MORPH_NAME

Instances

Instances details

Eq ComorphismDef Source #
Instance details Defined in Framework.AS Methods (==) :: ComorphismDef -> ComorphismDef -> Bool (/=) :: ComorphismDef -> ComorphismDef -> Bool
Data ComorphismDef Source #
Instance details Defined in Framework.AS Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ComorphismDef -> c ComorphismDef gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ComorphismDef toConstr :: ComorphismDef -> Constr dataTypeOf :: ComorphismDef -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ComorphismDef) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ComorphismDef) gmapT :: (forall b. Data b => b -> b) -> ComorphismDef -> ComorphismDef gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ComorphismDef -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ComorphismDef -> r gmapQ :: (forall d. Data d => d -> u) -> ComorphismDef -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ComorphismDef -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ComorphismDef -> m ComorphismDef
Ord ComorphismDef Source #
Instance details Defined in Framework.AS Methods compare :: ComorphismDef -> ComorphismDef -> Ordering (<) :: ComorphismDef -> ComorphismDef -> Bool (<=) :: ComorphismDef -> ComorphismDef -> Bool (>) :: ComorphismDef -> ComorphismDef -> Bool (>=) :: ComorphismDef -> ComorphismDef -> Bool max :: ComorphismDef -> ComorphismDef -> ComorphismDef min :: ComorphismDef -> ComorphismDef -> ComorphismDef
Show ComorphismDef Source #
Instance details Defined in Framework.AS Methods showsPrec :: Int -> ComorphismDef -> ShowS show :: ComorphismDef -> String showList :: [ComorphismDef] -> ShowS
Generic ComorphismDef
Instance details Defined in Framework.ATC_Framework Associated Types type Rep ComorphismDef :: Type -> Type Methods from :: ComorphismDef -> Rep ComorphismDef x to :: Rep ComorphismDef x -> ComorphismDef
Semigroup ComorphismDef
Instance details Defined in Framework.Logic_Framework Methods (<>) :: ComorphismDef -> ComorphismDef -> ComorphismDef # sconcat :: NonEmpty ComorphismDef -> ComorphismDef stimes :: Integral b => b -> ComorphismDef -> ComorphismDef
Monoid ComorphismDef
Instance details Defined in Framework.Logic_Framework Methods mempty :: ComorphismDef mappend :: ComorphismDef -> ComorphismDef -> ComorphismDef mconcat :: [ComorphismDef] -> ComorphismDef
GetRange ComorphismDef Source #
Instance details Defined in Framework.AS Methods getRange :: ComorphismDef -> Range Source # rangeSpan :: ComorphismDef -> [Pos] Source #
FromJSON ComorphismDef
Instance details Defined in Framework.ATC_Framework Methods parseJSON :: Value -> Parser ComorphismDef parseJSONList :: Value -> Parser [ComorphismDef]
ToJSON ComorphismDef
Instance details Defined in Framework.ATC_Framework Methods toJSON :: ComorphismDef -> Value toEncoding :: ComorphismDef -> Encoding toJSONList :: [ComorphismDef] -> Value toEncodingList :: [ComorphismDef] -> Encoding
ShATermConvertible ComorphismDef
Instance details Defined in Framework.ATC_Framework Methods toShATermAux :: ATermTable -> ComorphismDef -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ComorphismDef] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ComorphismDef) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ComorphismDef])
Pretty ComorphismDef Source #
Instance details Defined in Framework.AS Methods pretty :: ComorphismDef -> Doc Source # pretties :: [ComorphismDef] -> Doc Source #
Sentences FrameworkCom () ComorphismDef MorphismCom () Source #
Instance details Defined in Framework.Logic_Framework Methods map_sen :: FrameworkCom -> MorphismCom -> () -> Result () Source # simplify_sen :: FrameworkCom -> ComorphismDef -> () -> () Source # negation :: FrameworkCom -> () -> Maybe () Source # print_sign :: FrameworkCom -> ComorphismDef -> Doc Source # print_named :: FrameworkCom -> Named () -> Doc Source # sym_of :: FrameworkCom -> ComorphismDef -> [Set ()] Source # mostSymsOf :: FrameworkCom -> ComorphismDef -> [()] Source # symmap_of :: FrameworkCom -> MorphismCom -> EndoMap () Source # sym_name :: FrameworkCom -> () -> Id Source # sym_label :: FrameworkCom -> () -> Maybe String Source # fullSymName :: FrameworkCom -> () -> String Source # symKind :: FrameworkCom -> () -> String Source # symsOfSen :: FrameworkCom -> ComorphismDef -> () -> [()] Source # pair_symbols :: FrameworkCom -> () -> () -> Result () Source #
Syntax FrameworkCom ComorphismDef () () () Source #
Instance details Defined in Framework.Logic_Framework Methods parsersAndPrinters :: FrameworkCom -> Map String (PrefixMap -> AParser st ComorphismDef, ComorphismDef -> Doc) Source # parse_basic_spec :: FrameworkCom -> Maybe (PrefixMap -> AParser st ComorphismDef) Source # parseSingleSymbItem :: FrameworkCom -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: FrameworkCom -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: FrameworkCom -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: FrameworkCom -> ComorphismDef -> Item Source # symb_items_name :: FrameworkCom -> () -> [String] Source #
StaticAnalysis FrameworkCom ComorphismDef () () () ComorphismDef MorphismCom () () Source #
Instance details Defined in Framework.Logic_Framework Methods basic_analysis :: FrameworkCom -> Maybe ((ComorphismDef, ComorphismDef, GlobalAnnos) -> Result (ComorphismDef, ExtSign ComorphismDef (), [Named ()])) Source # sen_analysis :: FrameworkCom -> Maybe ((ComorphismDef, ComorphismDef, ()) -> Result ()) Source # extBasicAnalysis :: FrameworkCom -> IRI -> LibName -> ComorphismDef -> ComorphismDef -> GlobalAnnos -> Result (ComorphismDef, ExtSign ComorphismDef (), [Named ()]) Source # stat_symb_map_items :: FrameworkCom -> ComorphismDef -> Maybe ComorphismDef -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: FrameworkCom -> ComorphismDef -> [()] -> Result [()] Source # convertTheory :: FrameworkCom -> Maybe ((ComorphismDef, [Named ()]) -> ComorphismDef) Source # ensures_amalgamability :: FrameworkCom -> ([CASLAmalgOpt], Gr ComorphismDef (Int, MorphismCom), [(Int, MorphismCom)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: FrameworkCom -> MorphismCom -> [Named ()] -> Result (ComorphismDef, [Named ()]) Source # signature_colimit :: FrameworkCom -> Gr ComorphismDef (Int, MorphismCom) -> Result (ComorphismDef, Map Int MorphismCom) Source # qualify :: FrameworkCom -> SIMPLE_ID -> LibName -> MorphismCom -> ComorphismDef -> Result (MorphismCom, [Named ()]) Source # symbol_to_raw :: FrameworkCom -> () -> () Source # id_to_raw :: FrameworkCom -> Id -> () Source # matches :: FrameworkCom -> () -> () -> Bool Source # empty_signature :: FrameworkCom -> ComorphismDef Source # add_symb_to_sign :: FrameworkCom -> ComorphismDef -> () -> Result ComorphismDef Source # signature_union :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source # signatureDiff :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source # intersection :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source # final_union :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result ComorphismDef Source # morphism_union :: FrameworkCom -> MorphismCom -> MorphismCom -> Result MorphismCom Source # is_subsig :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Bool Source # subsig_inclusion :: FrameworkCom -> ComorphismDef -> ComorphismDef -> Result MorphismCom Source # generated_sign :: FrameworkCom -> Set () -> ComorphismDef -> Result MorphismCom Source # cogenerated_sign :: FrameworkCom -> Set () -> ComorphismDef -> Result MorphismCom Source # induced_from_morphism :: FrameworkCom -> EndoMap () -> ComorphismDef -> Result MorphismCom Source # induced_from_to_morphism :: FrameworkCom -> EndoMap () -> ExtSign ComorphismDef () -> ExtSign ComorphismDef () -> Result MorphismCom Source # is_transportable :: FrameworkCom -> MorphismCom -> Bool Source # is_injective :: FrameworkCom -> MorphismCom -> Bool Source # theory_to_taxonomy :: FrameworkCom -> TaxoGraphKind -> MMiSSOntology -> ComorphismDef -> [Named ()] -> Result MMiSSOntology Source # corresp2th :: FrameworkCom -> String -> Bool -> ComorphismDef -> ComorphismDef -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (ComorphismDef, [Named ()], ComorphismDef, ComorphismDef, EndoMap (), EndoMap ()) Source # equiv2cospan :: FrameworkCom -> ComorphismDef -> ComorphismDef -> [()] -> [()] -> Result (ComorphismDef, ComorphismDef, ComorphismDef, EndoMap (), EndoMap ()) Source # extract_module :: FrameworkCom -> [IRI] -> (ComorphismDef, [Named ()]) -> Result (ComorphismDef, [Named ()]) Source #
Logic FrameworkCom () ComorphismDef () () () ComorphismDef MorphismCom () () () Source #
Instance details Defined in Framework.Logic_Framework Methods parse_basic_sen :: FrameworkCom -> Maybe (ComorphismDef -> AParser st ()) Source # stability :: FrameworkCom -> Stability Source # data_logic :: FrameworkCom -> Maybe AnyLogic Source # top_sublogic :: FrameworkCom -> () Source # all_sublogics :: FrameworkCom -> [()] Source # bottomSublogic :: FrameworkCom -> Maybe () Source # sublogicDimensions :: FrameworkCom -> [[()]] Source # parseSublogic :: FrameworkCom -> String -> Maybe () Source # proj_sublogic_epsilon :: FrameworkCom -> () -> ComorphismDef -> MorphismCom Source # provers :: FrameworkCom -> [Prover ComorphismDef () MorphismCom () ()] Source # default_prover :: FrameworkCom -> String Source # cons_checkers :: FrameworkCom -> [ConsChecker ComorphismDef () () MorphismCom ()] Source # conservativityCheck :: FrameworkCom -> [ConservativityChecker ComorphismDef () MorphismCom] Source # empty_proof_tree :: FrameworkCom -> () Source # syntaxTable :: FrameworkCom -> ComorphismDef -> Maybe SyntaxTable Source # omdoc_metatheory :: FrameworkCom -> Maybe OMCD Source # export_symToOmdoc :: FrameworkCom -> NameMap () -> () -> String -> Result TCElement Source # export_senToOmdoc :: FrameworkCom -> NameMap () -> () -> Result TCorOMElement Source # export_theoryToOmdoc :: FrameworkCom -> SigMap () -> ComorphismDef -> [Named ()] -> Result [TCElement] Source # omdocToSym :: FrameworkCom -> SigMapI () -> TCElement -> String -> Result () Source # omdocToSen :: FrameworkCom -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source # addOMadtToTheory :: FrameworkCom -> SigMapI () -> (ComorphismDef, [Named ()]) -> [[OmdADT]] -> Result (ComorphismDef, [Named ()]) Source # addOmdocToTheory :: FrameworkCom -> SigMapI () -> (ComorphismDef, [Named ()]) -> [TCElement] -> Result (ComorphismDef, [Named ()]) Source # sublogicOfTheo :: FrameworkCom -> (ComorphismDef, [()]) -> () Source #
type Rep ComorphismDef
Instance details Defined in Framework.ATC_Framework type Rep ComorphismDef = D1 ('MetaData "ComorphismDef" "Framework.AS" "main" 'False) (C1 ('MetaCons "ComorphismDef" 'PrefixI 'True) ((S1 ('MetaSel ('Just "newcomorphismName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NAME) :: (S1 ('MetaSel ('Just "metaC") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FRAM) :: S1 ('MetaSel ('Just "source") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SIG_NAME))) :: ((S1 ('MetaSel ('Just "target") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SIG_NAME) :: S1 ('MetaSel ('Just "syntaxC") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MORPH_NAME)) :: (S1 ('MetaSel ('Just "modelC") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MORPH_NAME) :: S1 ('MetaSel ('Just "proofC") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MORPH_NAME)))))

printLogicDef :: LogicDef -> Doc Source #

printComorphismDef :: ComorphismDef -> Doc Source #

printFram :: FRAM -> Doc Source #