Copyright	(c) C. Maeder DFKI 2008
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	None

VSE.As

Contents

Pretty instances

Description

CASL extention to VSE programs and dynamic logic as described on page 4-7 (Sec 2.3.1, 2.5.2, 2.5.4, 2.6) of Bruno Langenstein's API description

Synopsis

Documentation

data Paramkind Source #

input or output procedure parameter kind

Constructors

In
Out

Instances

Eq Paramkind Source #
Methods (==) :: Paramkind -> Paramkind -> Bool (/=) :: Paramkind -> Paramkind -> Bool
Data Paramkind Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Paramkind -> c Paramkind gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Paramkind toConstr :: Paramkind -> Constr dataTypeOf :: Paramkind -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Paramkind) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Paramkind) gmapT :: (forall b. Data b => b -> b) -> Paramkind -> Paramkind gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Paramkind -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Paramkind -> r gmapQ :: (forall d. Data d => d -> u) -> Paramkind -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Paramkind -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Paramkind -> m Paramkind gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Paramkind -> m Paramkind gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Paramkind -> m Paramkind
Ord Paramkind Source #
Methods compare :: Paramkind -> Paramkind -> Ordering (<) :: Paramkind -> Paramkind -> Bool (<=) :: Paramkind -> Paramkind -> Bool (>) :: Paramkind -> Paramkind -> Bool (>=) :: Paramkind -> Paramkind -> Bool max :: Paramkind -> Paramkind -> Paramkind min :: Paramkind -> Paramkind -> Paramkind
Show Paramkind Source #
Methods showsPrec :: Int -> Paramkind -> ShowS show :: Paramkind -> String showList :: [Paramkind] -> ShowS

data Procparam Source #

a procedure parameter

Constructors

Procparam Paramkind SORT

Instances

Eq Procparam Source #
Methods (==) :: Procparam -> Procparam -> Bool (/=) :: Procparam -> Procparam -> Bool
Data Procparam Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Procparam -> c Procparam gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Procparam toConstr :: Procparam -> Constr dataTypeOf :: Procparam -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Procparam) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Procparam) gmapT :: (forall b. Data b => b -> b) -> Procparam -> Procparam gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Procparam -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Procparam -> r gmapQ :: (forall d. Data d => d -> u) -> Procparam -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Procparam -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Procparam -> m Procparam gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Procparam -> m Procparam gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Procparam -> m Procparam
Ord Procparam Source #
Methods compare :: Procparam -> Procparam -> Ordering (<) :: Procparam -> Procparam -> Bool (<=) :: Procparam -> Procparam -> Bool (>) :: Procparam -> Procparam -> Bool (>=) :: Procparam -> Procparam -> Bool max :: Procparam -> Procparam -> Procparam min :: Procparam -> Procparam -> Procparam
Show Procparam Source #
Methods showsPrec :: Int -> Procparam -> ShowS show :: Procparam -> String showList :: [Procparam] -> ShowS
Pretty Procparam Source #
Methods pretty :: Procparam -> Doc Source # pretties :: [Procparam] -> Doc Source #

data Profile Source #

procedure or function declaration

Constructors

Profile [Procparam] (Maybe SORT)

Instances

Eq Profile Source #
Methods (==) :: Profile -> Profile -> Bool (/=) :: Profile -> Profile -> Bool
Data Profile Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Profile -> c Profile gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Profile toConstr :: Profile -> Constr dataTypeOf :: Profile -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Profile) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Profile) gmapT :: (forall b. Data b => b -> b) -> Profile -> Profile gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Profile -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Profile -> r gmapQ :: (forall d. Data d => d -> u) -> Profile -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Profile -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Profile -> m Profile gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Profile -> m Profile gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Profile -> m Profile
Ord Profile Source #
Methods compare :: Profile -> Profile -> Ordering (<) :: Profile -> Profile -> Bool (<=) :: Profile -> Profile -> Bool (>) :: Profile -> Profile -> Bool (>=) :: Profile -> Profile -> Bool max :: Profile -> Profile -> Profile min :: Profile -> Profile -> Profile
Show Profile Source #
Methods showsPrec :: Int -> Profile -> ShowS show :: Profile -> String showList :: [Profile] -> ShowS
Pretty Profile Source #
Methods pretty :: Profile -> Doc Source # pretties :: [Profile] -> Doc Source #

data Sigentry Source #

further VSE signature entries

Constructors

Procedure Id Profile Range

Instances

Eq Sigentry Source #
Methods (==) :: Sigentry -> Sigentry -> Bool (/=) :: Sigentry -> Sigentry -> Bool
Data Sigentry Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sigentry -> c Sigentry gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sigentry toConstr :: Sigentry -> Constr dataTypeOf :: Sigentry -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Sigentry) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sigentry) gmapT :: (forall b. Data b => b -> b) -> Sigentry -> Sigentry gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sigentry -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sigentry -> r gmapQ :: (forall d. Data d => d -> u) -> Sigentry -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Sigentry -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sigentry -> m Sigentry gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sigentry -> m Sigentry gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sigentry -> m Sigentry
Ord Sigentry Source #
Methods compare :: Sigentry -> Sigentry -> Ordering (<) :: Sigentry -> Sigentry -> Bool (<=) :: Sigentry -> Sigentry -> Bool (>) :: Sigentry -> Sigentry -> Bool (>=) :: Sigentry -> Sigentry -> Bool max :: Sigentry -> Sigentry -> Sigentry min :: Sigentry -> Sigentry -> Sigentry
Show Sigentry Source #
Methods showsPrec :: Int -> Sigentry -> ShowS show :: Sigentry -> String showList :: [Sigentry] -> ShowS
Pretty Sigentry Source #
Methods pretty :: Sigentry -> Doc Source # pretties :: [Sigentry] -> Doc Source #

data Procdecls Source #

Constructors

Procdecls [Annoted Sigentry] Range

Instances

Eq Procdecls Source #
Methods (==) :: Procdecls -> Procdecls -> Bool (/=) :: Procdecls -> Procdecls -> Bool
Data Procdecls Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Procdecls -> c Procdecls gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Procdecls toConstr :: Procdecls -> Constr dataTypeOf :: Procdecls -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Procdecls) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Procdecls) gmapT :: (forall b. Data b => b -> b) -> Procdecls -> Procdecls gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Procdecls -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Procdecls -> r gmapQ :: (forall d. Data d => d -> u) -> Procdecls -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Procdecls -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Procdecls -> m Procdecls gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Procdecls -> m Procdecls gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Procdecls -> m Procdecls
Ord Procdecls Source #
Methods compare :: Procdecls -> Procdecls -> Ordering (<) :: Procdecls -> Procdecls -> Bool (<=) :: Procdecls -> Procdecls -> Bool (>) :: Procdecls -> Procdecls -> Bool (>=) :: Procdecls -> Procdecls -> Bool max :: Procdecls -> Procdecls -> Procdecls min :: Procdecls -> Procdecls -> Procdecls
Show Procdecls Source #
Methods showsPrec :: Int -> Procdecls -> ShowS show :: Procdecls -> String showList :: [Procdecls] -> ShowS
GetRange Procdecls Source #
Methods getRange :: Procdecls -> Range Source # rangeSpan :: Procdecls -> [Pos] Source #
Pretty Procdecls Source #
Methods pretty :: Procdecls -> Doc Source # pretties :: [Procdecls] -> Doc Source #
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Methods parsersAndPrinters :: VSE -> Map String (PrefixMap -> AParser st VSEBasicSpec, VSEBasicSpec -> Doc) Source # parse_basic_spec :: VSE -> Maybe (PrefixMap -> AParser st VSEBasicSpec) Source # parseSingleSymbItem :: VSE -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_items :: VSE -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_map_items :: VSE -> Maybe (AParser st SYMB_MAP_ITEMS) Source # toItem :: VSE -> VSEBasicSpec -> Item Source # symb_items_name :: VSE -> SYMB_ITEMS -> [String] Source #
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source #
Methods basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source # sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source # stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source # ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source # signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source # qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source # symbol_to_raw :: VSE -> Symbol -> RawSymbol Source # id_to_raw :: VSE -> Id -> RawSymbol Source # matches :: VSE -> Symbol -> RawSymbol -> Bool Source # empty_signature :: VSE -> VSESign Source # add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source # signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source # signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source # intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source # final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source # morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source # is_subsig :: VSE -> VSESign -> VSESign -> Bool Source # subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source # generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source # cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source # induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source # induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source # is_transportable :: VSE -> VSEMor -> Bool Source # is_injective :: VSE -> VSEMor -> Bool Source # theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #
Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source # stability :: VSE -> Stability Source # data_logic :: VSE -> Maybe AnyLogic Source # top_sublogic :: VSE -> () Source # all_sublogics :: VSE -> [()] Source # bottomSublogic :: VSE -> Maybe () Source # sublogicDimensions :: VSE -> [[()]] Source # parseSublogic :: VSE -> String -> Maybe () Source # proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source # provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source # default_prover :: VSE -> String Source # cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source # conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source # empty_proof_tree :: VSE -> () Source # syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source # omdoc_metatheory :: VSE -> Maybe OMCD Source # export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source # addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source #
Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2VSE -> CASL Source # sourceSublogic :: CASL2VSE -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source # minSourceTheory :: CASL2VSE -> Maybe (LibName, String) Source # targetLogic :: CASL2VSE -> VSE Source # mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSE -> Bool Source # has_model_expansion :: CASL2VSE -> Bool Source # is_weakly_amalgamable :: CASL2VSE -> Bool Source # constituents :: CASL2VSE -> [String] Source # isInclusionComorphism :: CASL2VSE -> Bool Source # rps :: CASL2VSE -> Bool Source # eps :: CASL2VSE -> Bool Source #
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2VSEImport -> CASL Source # sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source # minSourceTheory :: CASL2VSEImport -> Maybe (LibName, String) Source # targetLogic :: CASL2VSEImport -> VSE Source # mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSEImport -> Bool Source # has_model_expansion :: CASL2VSEImport -> Bool Source # is_weakly_amalgamable :: CASL2VSEImport -> Bool Source # constituents :: CASL2VSEImport -> [String] Source # isInclusionComorphism :: CASL2VSEImport -> Bool Source # rps :: CASL2VSEImport -> Bool Source # eps :: CASL2VSEImport -> Bool Source #
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2VSERefine -> CASL Source # sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source # minSourceTheory :: CASL2VSERefine -> Maybe (LibName, String) Source # targetLogic :: CASL2VSERefine -> VSE Source # mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSERefine -> Bool Source # has_model_expansion :: CASL2VSERefine -> Bool Source # is_weakly_amalgamable :: CASL2VSERefine -> Bool Source # constituents :: CASL2VSERefine -> [String] Source # isInclusionComorphism :: CASL2VSERefine -> Bool Source # rps :: CASL2VSERefine -> Bool Source # eps :: CASL2VSERefine -> Bool Source #

data Ranged a Source #

wrapper for positions

Constructors

Ranged
Fields unRanged :: a range :: Range

Instances

Sentences VSE Sentence VSESign VSEMor Symbol Source #
Methods map_sen :: VSE -> VSEMor -> Sentence -> Result Sentence Source # simplify_sen :: VSE -> VSESign -> Sentence -> Sentence Source # negation :: VSE -> Sentence -> Maybe Sentence Source # print_sign :: VSE -> VSESign -> Doc Source # print_named :: VSE -> Named Sentence -> Doc Source # sym_of :: VSE -> VSESign -> [Set Symbol] Source # mostSymsOf :: VSE -> VSESign -> [Symbol] Source # symmap_of :: VSE -> VSEMor -> EndoMap Symbol Source # sym_name :: VSE -> Symbol -> Id Source # sym_label :: VSE -> Symbol -> Maybe String Source # fullSymName :: VSE -> Symbol -> String Source # symKind :: VSE -> Symbol -> String Source # symsOfSen :: VSE -> VSESign -> Sentence -> [Symbol] Source # pair_symbols :: VSE -> Symbol -> Symbol -> Result Symbol Source #
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Methods parsersAndPrinters :: VSE -> Map String (PrefixMap -> AParser st VSEBasicSpec, VSEBasicSpec -> Doc) Source # parse_basic_spec :: VSE -> Maybe (PrefixMap -> AParser st VSEBasicSpec) Source # parseSingleSymbItem :: VSE -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_items :: VSE -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_map_items :: VSE -> Maybe (AParser st SYMB_MAP_ITEMS) Source # toItem :: VSE -> VSEBasicSpec -> Item Source # symb_items_name :: VSE -> SYMB_ITEMS -> [String] Source #
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source #
Methods basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source # sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source # stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source # ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source # signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source # qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source # symbol_to_raw :: VSE -> Symbol -> RawSymbol Source # id_to_raw :: VSE -> Id -> RawSymbol Source # matches :: VSE -> Symbol -> RawSymbol -> Bool Source # empty_signature :: VSE -> VSESign Source # add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source # signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source # signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source # intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source # final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source # morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source # is_subsig :: VSE -> VSESign -> VSESign -> Bool Source # subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source # generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source # cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source # induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source # induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source # is_transportable :: VSE -> VSEMor -> Bool Source # is_injective :: VSE -> VSEMor -> Bool Source # theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #
Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source # stability :: VSE -> Stability Source # data_logic :: VSE -> Maybe AnyLogic Source # top_sublogic :: VSE -> () Source # all_sublogics :: VSE -> [()] Source # bottomSublogic :: VSE -> Maybe () Source # sublogicDimensions :: VSE -> [[()]] Source # parseSublogic :: VSE -> String -> Maybe () Source # proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source # provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source # default_prover :: VSE -> String Source # cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source # conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source # empty_proof_tree :: VSE -> () Source # syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source # omdoc_metatheory :: VSE -> Maybe OMCD Source # export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source # addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source #
Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2VSE -> CASL Source # sourceSublogic :: CASL2VSE -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source # minSourceTheory :: CASL2VSE -> Maybe (LibName, String) Source # targetLogic :: CASL2VSE -> VSE Source # mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSE -> Bool Source # has_model_expansion :: CASL2VSE -> Bool Source # is_weakly_amalgamable :: CASL2VSE -> Bool Source # constituents :: CASL2VSE -> [String] Source # isInclusionComorphism :: CASL2VSE -> Bool Source # rps :: CASL2VSE -> Bool Source # eps :: CASL2VSE -> Bool Source #
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2VSEImport -> CASL Source # sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source # minSourceTheory :: CASL2VSEImport -> Maybe (LibName, String) Source # targetLogic :: CASL2VSEImport -> VSE Source # mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSEImport -> Bool Source # has_model_expansion :: CASL2VSEImport -> Bool Source # is_weakly_amalgamable :: CASL2VSEImport -> Bool Source # constituents :: CASL2VSEImport -> [String] Source # isInclusionComorphism :: CASL2VSEImport -> Bool Source # rps :: CASL2VSEImport -> Bool Source # eps :: CASL2VSEImport -> Bool Source #
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2VSERefine -> CASL Source # sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source # minSourceTheory :: CASL2VSERefine -> Maybe (LibName, String) Source # targetLogic :: CASL2VSERefine -> VSE Source # mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSERefine -> Bool Source # has_model_expansion :: CASL2VSERefine -> Bool Source # is_weakly_amalgamable :: CASL2VSERefine -> Bool Source # constituents :: CASL2VSERefine -> [String] Source # isInclusionComorphism :: CASL2VSERefine -> Bool Source # rps :: CASL2VSERefine -> Bool Source # eps :: CASL2VSERefine -> Bool Source #
Eq a => Eq (Ranged a) Source #
Methods (==) :: Ranged a -> Ranged a -> Bool (/=) :: Ranged a -> Ranged a -> Bool
Data a => Data (Ranged a) Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ranged a -> c (Ranged a) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Ranged a) toConstr :: Ranged a -> Constr dataTypeOf :: Ranged a -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c (Ranged a)) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ranged a)) gmapT :: (forall b. Data b => b -> b) -> Ranged a -> Ranged a gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r gmapQ :: (forall d. Data d => d -> u) -> Ranged a -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Ranged a -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a)
Ord a => Ord (Ranged a) Source #
Methods compare :: Ranged a -> Ranged a -> Ordering (<) :: Ranged a -> Ranged a -> Bool (<=) :: Ranged a -> Ranged a -> Bool (>) :: Ranged a -> Ranged a -> Bool (>=) :: Ranged a -> Ranged a -> Bool max :: Ranged a -> Ranged a -> Ranged a min :: Ranged a -> Ranged a -> Ranged a
Show a => Show (Ranged a) Source #
Methods showsPrec :: Int -> Ranged a -> ShowS show :: Ranged a -> String showList :: [Ranged a] -> ShowS
GetRange (Ranged a) Source #
Methods getRange :: Ranged a -> Range Source # rangeSpan :: Ranged a -> [Pos] Source #
Pretty a => Pretty (Ranged a) Source #
Methods pretty :: Ranged a -> Doc Source # pretties :: [Ranged a] -> Doc Source #
FormExtension a => FormExtension (Ranged a) Source #
Methods isQuantifierLike :: Ranged a -> Bool Source # prefixExt :: Ranged a -> Doc -> Doc Source #

mkRanged :: a -> Ranged a Source #

attach a nullRange

type Program = Ranged PlainProgram Source #

programs with ranges

data PlainProgram Source #

programs based on restricted terms and formulas

Constructors

Abort
Skip
Assign VAR (TERM ())
Call (FORMULA ())	a procedure call as predication
Return (TERM ())
Block [VAR_DECL] Program
Seq Program Program
If (FORMULA ()) Program Program
While (FORMULA ()) Program

Instances

Eq PlainProgram Source #
Methods (==) :: PlainProgram -> PlainProgram -> Bool (/=) :: PlainProgram -> PlainProgram -> Bool
Data PlainProgram Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PlainProgram -> c PlainProgram gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PlainProgram toConstr :: PlainProgram -> Constr dataTypeOf :: PlainProgram -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c PlainProgram) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PlainProgram) gmapT :: (forall b. Data b => b -> b) -> PlainProgram -> PlainProgram gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PlainProgram -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PlainProgram -> r gmapQ :: (forall d. Data d => d -> u) -> PlainProgram -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> PlainProgram -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram
Ord PlainProgram Source #
Methods compare :: PlainProgram -> PlainProgram -> Ordering (<) :: PlainProgram -> PlainProgram -> Bool (<=) :: PlainProgram -> PlainProgram -> Bool (>) :: PlainProgram -> PlainProgram -> Bool (>=) :: PlainProgram -> PlainProgram -> Bool max :: PlainProgram -> PlainProgram -> PlainProgram min :: PlainProgram -> PlainProgram -> PlainProgram
Show PlainProgram Source #
Methods showsPrec :: Int -> PlainProgram -> ShowS show :: PlainProgram -> String showList :: [PlainProgram] -> ShowS
Pretty PlainProgram Source #
Methods pretty :: PlainProgram -> Doc Source # pretties :: [PlainProgram] -> Doc Source #

data VarDecl Source #

alternative variable declaration

Constructors

VarDecl VAR SORT (Maybe (TERM ())) Range

Instances

Data VarDecl Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VarDecl -> c VarDecl gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VarDecl toConstr :: VarDecl -> Constr dataTypeOf :: VarDecl -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c VarDecl) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarDecl) gmapT :: (forall b. Data b => b -> b) -> VarDecl -> VarDecl gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VarDecl -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VarDecl -> r gmapQ :: (forall d. Data d => d -> u) -> VarDecl -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> VarDecl -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl
Show VarDecl Source #
Methods showsPrec :: Int -> VarDecl -> ShowS show :: VarDecl -> String showList :: [VarDecl] -> ShowS
Pretty VarDecl Source #
Methods pretty :: VarDecl -> Doc Source # pretties :: [VarDecl] -> Doc Source #

toVarDecl :: [VAR_DECL] -> [VarDecl] Source #

addInits :: [VarDecl] -> Program -> ([VarDecl], Program) Source #

data VSEforms Source #

extend CASL formulas by box or diamond formulas and defprocs

Constructors

Dlformula BoxOrDiamond Program Sentence
Defprocs [Defproc]
RestrictedConstraint [Constraint] (Map SORT Id) Bool

Instances

Eq VSEforms Source #
Methods (==) :: VSEforms -> VSEforms -> Bool (/=) :: VSEforms -> VSEforms -> Bool
Data VSEforms Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VSEforms -> c VSEforms gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VSEforms toConstr :: VSEforms -> Constr dataTypeOf :: VSEforms -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c VSEforms) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VSEforms) gmapT :: (forall b. Data b => b -> b) -> VSEforms -> VSEforms gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VSEforms -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VSEforms -> r gmapQ :: (forall d. Data d => d -> u) -> VSEforms -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> VSEforms -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> VSEforms -> m VSEforms gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VSEforms -> m VSEforms gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VSEforms -> m VSEforms
Ord VSEforms Source #
Methods compare :: VSEforms -> VSEforms -> Ordering (<) :: VSEforms -> VSEforms -> Bool (<=) :: VSEforms -> VSEforms -> Bool (>) :: VSEforms -> VSEforms -> Bool (>=) :: VSEforms -> VSEforms -> Bool max :: VSEforms -> VSEforms -> VSEforms min :: VSEforms -> VSEforms -> VSEforms
Show VSEforms Source #
Methods showsPrec :: Int -> VSEforms -> ShowS show :: VSEforms -> String showList :: [VSEforms] -> ShowS
GetRange VSEforms Source #
Methods getRange :: VSEforms -> Range Source # rangeSpan :: VSEforms -> [Pos] Source #
Pretty VSEforms Source #
Methods pretty :: VSEforms -> Doc Source # pretties :: [VSEforms] -> Doc Source #
FormExtension VSEforms Source #
Methods isQuantifierLike :: VSEforms -> Bool Source # prefixExt :: VSEforms -> Doc -> Doc Source #
Sentences VSE Sentence VSESign VSEMor Symbol Source #
Methods map_sen :: VSE -> VSEMor -> Sentence -> Result Sentence Source # simplify_sen :: VSE -> VSESign -> Sentence -> Sentence Source # negation :: VSE -> Sentence -> Maybe Sentence Source # print_sign :: VSE -> VSESign -> Doc Source # print_named :: VSE -> Named Sentence -> Doc Source # sym_of :: VSE -> VSESign -> [Set Symbol] Source # mostSymsOf :: VSE -> VSESign -> [Symbol] Source # symmap_of :: VSE -> VSEMor -> EndoMap Symbol Source # sym_name :: VSE -> Symbol -> Id Source # sym_label :: VSE -> Symbol -> Maybe String Source # fullSymName :: VSE -> Symbol -> String Source # symKind :: VSE -> Symbol -> String Source # symsOfSen :: VSE -> VSESign -> Sentence -> [Symbol] Source # pair_symbols :: VSE -> Symbol -> Symbol -> Result Symbol Source #
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Methods parsersAndPrinters :: VSE -> Map String (PrefixMap -> AParser st VSEBasicSpec, VSEBasicSpec -> Doc) Source # parse_basic_spec :: VSE -> Maybe (PrefixMap -> AParser st VSEBasicSpec) Source # parseSingleSymbItem :: VSE -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_items :: VSE -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_map_items :: VSE -> Maybe (AParser st SYMB_MAP_ITEMS) Source # toItem :: VSE -> VSEBasicSpec -> Item Source # symb_items_name :: VSE -> SYMB_ITEMS -> [String] Source #
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source #
Methods basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source # sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source # stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source # ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source # signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source # qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source # symbol_to_raw :: VSE -> Symbol -> RawSymbol Source # id_to_raw :: VSE -> Id -> RawSymbol Source # matches :: VSE -> Symbol -> RawSymbol -> Bool Source # empty_signature :: VSE -> VSESign Source # add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source # signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source # signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source # intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source # final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source # morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source # is_subsig :: VSE -> VSESign -> VSESign -> Bool Source # subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source # generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source # cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source # induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source # induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source # is_transportable :: VSE -> VSEMor -> Bool Source # is_injective :: VSE -> VSEMor -> Bool Source # theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #
Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source # stability :: VSE -> Stability Source # data_logic :: VSE -> Maybe AnyLogic Source # top_sublogic :: VSE -> () Source # all_sublogics :: VSE -> [()] Source # bottomSublogic :: VSE -> Maybe () Source # sublogicDimensions :: VSE -> [[()]] Source # parseSublogic :: VSE -> String -> Maybe () Source # proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source # provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source # default_prover :: VSE -> String Source # cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source # conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source # empty_proof_tree :: VSE -> () Source # syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source # omdoc_metatheory :: VSE -> Maybe OMCD Source # export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source # addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source #
Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2VSE -> CASL Source # sourceSublogic :: CASL2VSE -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source # minSourceTheory :: CASL2VSE -> Maybe (LibName, String) Source # targetLogic :: CASL2VSE -> VSE Source # mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSE -> Bool Source # has_model_expansion :: CASL2VSE -> Bool Source # is_weakly_amalgamable :: CASL2VSE -> Bool Source # constituents :: CASL2VSE -> [String] Source # isInclusionComorphism :: CASL2VSE -> Bool Source # rps :: CASL2VSE -> Bool Source # eps :: CASL2VSE -> Bool Source #
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2VSEImport -> CASL Source # sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source # minSourceTheory :: CASL2VSEImport -> Maybe (LibName, String) Source # targetLogic :: CASL2VSEImport -> VSE Source # mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSEImport -> Bool Source # has_model_expansion :: CASL2VSEImport -> Bool Source # is_weakly_amalgamable :: CASL2VSEImport -> Bool Source # constituents :: CASL2VSEImport -> [String] Source # isInclusionComorphism :: CASL2VSEImport -> Bool Source # rps :: CASL2VSEImport -> Bool Source # eps :: CASL2VSEImport -> Bool Source #
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2VSERefine -> CASL Source # sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source # minSourceTheory :: CASL2VSERefine -> Maybe (LibName, String) Source # targetLogic :: CASL2VSERefine -> VSE Source # mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSERefine -> Bool Source # has_model_expansion :: CASL2VSERefine -> Bool Source # is_weakly_amalgamable :: CASL2VSERefine -> Bool Source # constituents :: CASL2VSERefine -> [String] Source # isInclusionComorphism :: CASL2VSERefine -> Bool Source # rps :: CASL2VSERefine -> Bool Source # eps :: CASL2VSERefine -> Bool Source #

type Dlformula = Ranged VSEforms Source #

type Sentence = FORMULA Dlformula Source #

data BoxOrDiamond Source #

box or diamond indicator

Constructors

Box
Diamond

Instances

Eq BoxOrDiamond Source #
Methods (==) :: BoxOrDiamond -> BoxOrDiamond -> Bool (/=) :: BoxOrDiamond -> BoxOrDiamond -> Bool
Data BoxOrDiamond Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BoxOrDiamond -> c BoxOrDiamond gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BoxOrDiamond toConstr :: BoxOrDiamond -> Constr dataTypeOf :: BoxOrDiamond -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c BoxOrDiamond) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BoxOrDiamond) gmapT :: (forall b. Data b => b -> b) -> BoxOrDiamond -> BoxOrDiamond gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BoxOrDiamond -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BoxOrDiamond -> r gmapQ :: (forall d. Data d => d -> u) -> BoxOrDiamond -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BoxOrDiamond -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BoxOrDiamond -> m BoxOrDiamond gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BoxOrDiamond -> m BoxOrDiamond gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BoxOrDiamond -> m BoxOrDiamond
Ord BoxOrDiamond Source #
Methods compare :: BoxOrDiamond -> BoxOrDiamond -> Ordering (<) :: BoxOrDiamond -> BoxOrDiamond -> Bool (<=) :: BoxOrDiamond -> BoxOrDiamond -> Bool (>) :: BoxOrDiamond -> BoxOrDiamond -> Bool (>=) :: BoxOrDiamond -> BoxOrDiamond -> Bool max :: BoxOrDiamond -> BoxOrDiamond -> BoxOrDiamond min :: BoxOrDiamond -> BoxOrDiamond -> BoxOrDiamond
Show BoxOrDiamond Source #
Methods showsPrec :: Int -> BoxOrDiamond -> ShowS show :: BoxOrDiamond -> String showList :: [BoxOrDiamond] -> ShowS

data ProcKind Source #

Constructors

Proc
Func

Instances

Eq ProcKind Source #
Methods (==) :: ProcKind -> ProcKind -> Bool (/=) :: ProcKind -> ProcKind -> Bool
Data ProcKind Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProcKind -> c ProcKind gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProcKind toConstr :: ProcKind -> Constr dataTypeOf :: ProcKind -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c ProcKind) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProcKind) gmapT :: (forall b. Data b => b -> b) -> ProcKind -> ProcKind gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProcKind -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProcKind -> r gmapQ :: (forall d. Data d => d -> u) -> ProcKind -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ProcKind -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProcKind -> m ProcKind gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProcKind -> m ProcKind gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProcKind -> m ProcKind
Ord ProcKind Source #
Methods compare :: ProcKind -> ProcKind -> Ordering (<) :: ProcKind -> ProcKind -> Bool (<=) :: ProcKind -> ProcKind -> Bool (>) :: ProcKind -> ProcKind -> Bool (>=) :: ProcKind -> ProcKind -> Bool max :: ProcKind -> ProcKind -> ProcKind min :: ProcKind -> ProcKind -> ProcKind
Show ProcKind Source #
Methods showsPrec :: Int -> ProcKind -> ShowS show :: ProcKind -> String showList :: [ProcKind] -> ShowS

data Defproc Source #

procedure definitions as basic items becoming sentences

Constructors

Defproc ProcKind Id [VAR] Program Range

Instances

Eq Defproc Source #
Methods (==) :: Defproc -> Defproc -> Bool (/=) :: Defproc -> Defproc -> Bool
Data Defproc Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Defproc -> c Defproc gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Defproc toConstr :: Defproc -> Constr dataTypeOf :: Defproc -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Defproc) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defproc) gmapT :: (forall b. Data b => b -> b) -> Defproc -> Defproc gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defproc -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defproc -> r gmapQ :: (forall d. Data d => d -> u) -> Defproc -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Defproc -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Defproc -> m Defproc gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Defproc -> m Defproc gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Defproc -> m Defproc
Ord Defproc Source #
Methods compare :: Defproc -> Defproc -> Ordering (<) :: Defproc -> Defproc -> Bool (<=) :: Defproc -> Defproc -> Bool (>) :: Defproc -> Defproc -> Bool (>=) :: Defproc -> Defproc -> Bool max :: Defproc -> Defproc -> Defproc min :: Defproc -> Defproc -> Defproc
Show Defproc Source #
Methods showsPrec :: Int -> Defproc -> ShowS show :: Defproc -> String showList :: [Defproc] -> ShowS
Pretty Defproc Source #
Methods pretty :: Defproc -> Doc Source # pretties :: [Defproc] -> Doc Source #

data Procs Source #

Constructors

Procs
Fields procsMap :: Map Id Profile

Instances

Eq Procs Source #
Methods (==) :: Procs -> Procs -> Bool (/=) :: Procs -> Procs -> Bool
Data Procs Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Procs -> c Procs gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Procs toConstr :: Procs -> Constr dataTypeOf :: Procs -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c Procs) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Procs) gmapT :: (forall b. Data b => b -> b) -> Procs -> Procs gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Procs -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Procs -> r gmapQ :: (forall d. Data d => d -> u) -> Procs -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Procs -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Procs -> m Procs gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Procs -> m Procs gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Procs -> m Procs
Ord Procs Source #
Methods compare :: Procs -> Procs -> Ordering (<) :: Procs -> Procs -> Bool (<=) :: Procs -> Procs -> Bool (>) :: Procs -> Procs -> Bool (>=) :: Procs -> Procs -> Bool max :: Procs -> Procs -> Procs min :: Procs -> Procs -> Procs
Show Procs Source #
Methods showsPrec :: Int -> Procs -> ShowS show :: Procs -> String showList :: [Procs] -> ShowS
Pretty Procs Source #
Methods pretty :: Procs -> Doc Source # pretties :: [Procs] -> Doc Source #
Sentences VSE Sentence VSESign VSEMor Symbol Source #
Methods map_sen :: VSE -> VSEMor -> Sentence -> Result Sentence Source # simplify_sen :: VSE -> VSESign -> Sentence -> Sentence Source # negation :: VSE -> Sentence -> Maybe Sentence Source # print_sign :: VSE -> VSESign -> Doc Source # print_named :: VSE -> Named Sentence -> Doc Source # sym_of :: VSE -> VSESign -> [Set Symbol] Source # mostSymsOf :: VSE -> VSESign -> [Symbol] Source # symmap_of :: VSE -> VSEMor -> EndoMap Symbol Source # sym_name :: VSE -> Symbol -> Id Source # sym_label :: VSE -> Symbol -> Maybe String Source # fullSymName :: VSE -> Symbol -> String Source # symKind :: VSE -> Symbol -> String Source # symsOfSen :: VSE -> VSESign -> Sentence -> [Symbol] Source # pair_symbols :: VSE -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source #
Methods basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source # sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source # stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source # ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source # signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source # qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source # symbol_to_raw :: VSE -> Symbol -> RawSymbol Source # id_to_raw :: VSE -> Id -> RawSymbol Source # matches :: VSE -> Symbol -> RawSymbol -> Bool Source # empty_signature :: VSE -> VSESign Source # add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source # signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source # signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source # intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source # final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source # morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source # is_subsig :: VSE -> VSESign -> VSESign -> Bool Source # subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source # generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source # cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source # induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source # induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source # is_transportable :: VSE -> VSEMor -> Bool Source # is_injective :: VSE -> VSEMor -> Bool Source # theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #
Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source # stability :: VSE -> Stability Source # data_logic :: VSE -> Maybe AnyLogic Source # top_sublogic :: VSE -> () Source # all_sublogics :: VSE -> [()] Source # bottomSublogic :: VSE -> Maybe () Source # sublogicDimensions :: VSE -> [[()]] Source # parseSublogic :: VSE -> String -> Maybe () Source # proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source # provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source # default_prover :: VSE -> String Source # cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source # conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source # empty_proof_tree :: VSE -> () Source # syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source # omdoc_metatheory :: VSE -> Maybe OMCD Source # export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source # addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source #
Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2VSE -> CASL Source # sourceSublogic :: CASL2VSE -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source # minSourceTheory :: CASL2VSE -> Maybe (LibName, String) Source # targetLogic :: CASL2VSE -> VSE Source # mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSE -> Bool Source # has_model_expansion :: CASL2VSE -> Bool Source # is_weakly_amalgamable :: CASL2VSE -> Bool Source # constituents :: CASL2VSE -> [String] Source # isInclusionComorphism :: CASL2VSE -> Bool Source # rps :: CASL2VSE -> Bool Source # eps :: CASL2VSE -> Bool Source #
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2VSEImport -> CASL Source # sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source # minSourceTheory :: CASL2VSEImport -> Maybe (LibName, String) Source # targetLogic :: CASL2VSEImport -> VSE Source # mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSEImport -> Bool Source # has_model_expansion :: CASL2VSEImport -> Bool Source # is_weakly_amalgamable :: CASL2VSEImport -> Bool Source # constituents :: CASL2VSEImport -> [String] Source # isInclusionComorphism :: CASL2VSEImport -> Bool Source # rps :: CASL2VSEImport -> Bool Source # eps :: CASL2VSEImport -> Bool Source #
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Methods sourceLogic :: CASL2VSERefine -> CASL Source # sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source # minSourceTheory :: CASL2VSERefine -> Maybe (LibName, String) Source # targetLogic :: CASL2VSERefine -> VSE Source # mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSERefine -> Bool Source # has_model_expansion :: CASL2VSERefine -> Bool Source # is_weakly_amalgamable :: CASL2VSERefine -> Bool Source # constituents :: CASL2VSERefine -> [String] Source # isInclusionComorphism :: CASL2VSERefine -> Bool Source # rps :: CASL2VSERefine -> Bool Source # eps :: CASL2VSERefine -> Bool Source #

emptyProcs :: Procs Source #

unionProcs :: Procs -> Procs -> Result Procs Source #

interProcs :: Procs -> Procs -> Result Procs Source #

diffProcs :: Procs -> Procs -> Procs Source #

isSubProcsMap :: Procs -> Procs -> Bool Source #

Pretty instances

block :: Doc -> Doc Source #

prettyProcKind :: ProcKind -> Doc Source #

assign :: Doc Source #

genSortName :: String -> SORT -> Id Source #

gnUniformName :: SORT -> Id Source #

gnRestrName :: SORT -> Id Source #

gnEqName :: SORT -> Id Source #

genVars :: [SORT] -> [(Token, SORT)] Source #

xVar :: Token Source #

yVar :: Token Source #

printRestrTypedecl :: Map SORT Id -> DATATYPE_DECL -> Doc Source #

prettyProcdefs :: [Defproc] -> Doc Source #