Copyright	(c) Dominik Dietrich Ewaryst Schulz DFKI Bremen 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Ewaryst.Schulz@dfki.de
Stability	experimental
Portability	portable
Safe Haskell	Safe

CSL.AS_BASIC_CSL

Description

This module contains the abstract syntax types for EnCL as well as the predefined operator configuration.

Synopsis

Documentation

data EXPRESSION Source #

Datatype for expressions

Constructors

Var Token
Op OPID [EXTPARAM] [EXPRESSION] Range
List [EXPRESSION] Range
Interval Double Double Range
Int APInt Range
Rat APFloat Range

Instances

Eq EXPRESSION Source #
Methods (==) :: EXPRESSION -> EXPRESSION -> Bool (/=) :: EXPRESSION -> EXPRESSION -> Bool
Data EXPRESSION Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EXPRESSION -> c EXPRESSION gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EXPRESSION toConstr :: EXPRESSION -> Constr dataTypeOf :: EXPRESSION -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c EXPRESSION) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EXPRESSION) gmapT :: (forall b. Data b => b -> b) -> EXPRESSION -> EXPRESSION gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EXPRESSION -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EXPRESSION -> r gmapQ :: (forall d. Data d => d -> u) -> EXPRESSION -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> EXPRESSION -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> EXPRESSION -> m EXPRESSION gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EXPRESSION -> m EXPRESSION gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EXPRESSION -> m EXPRESSION
Ord EXPRESSION Source #
Methods compare :: EXPRESSION -> EXPRESSION -> Ordering (<) :: EXPRESSION -> EXPRESSION -> Bool (<=) :: EXPRESSION -> EXPRESSION -> Bool (>) :: EXPRESSION -> EXPRESSION -> Bool (>=) :: EXPRESSION -> EXPRESSION -> Bool max :: EXPRESSION -> EXPRESSION -> EXPRESSION min :: EXPRESSION -> EXPRESSION -> EXPRESSION
Show EXPRESSION Source #
Methods showsPrec :: Int -> EXPRESSION -> ShowS show :: EXPRESSION -> String showList :: [EXPRESSION] -> ShowS
Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION] Source #	Instance of Logic for reduce logc
Methods parse_basic_sen :: CSL -> Maybe (BASIC_SPEC -> AParser st CMD) Source # stability :: CSL -> Stability Source # data_logic :: CSL -> Maybe AnyLogic Source # top_sublogic :: CSL -> () Source # all_sublogics :: CSL -> [()] Source # bottomSublogic :: CSL -> Maybe () Source # sublogicDimensions :: CSL -> [[()]] Source # parseSublogic :: CSL -> String -> Maybe () Source # proj_sublogic_epsilon :: CSL -> () -> Sign -> Morphism Source # provers :: CSL -> [Prover Sign CMD Morphism () [EXPRESSION]] Source # default_prover :: CSL -> String Source # cons_checkers :: CSL -> [ConsChecker Sign CMD () Morphism [EXPRESSION]] Source # conservativityCheck :: CSL -> [ConservativityChecker Sign CMD Morphism] Source # empty_proof_tree :: CSL -> [EXPRESSION] Source # syntaxTable :: CSL -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: CSL -> Maybe OMCD Source # export_symToOmdoc :: CSL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CSL -> NameMap Symbol -> CMD -> Result TCorOMElement Source # export_theoryToOmdoc :: CSL -> SigMap Symbol -> Sign -> [Named CMD] -> Result [TCElement] Source # omdocToSym :: CSL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CSL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CMD)) Source # addOMadtToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [[OmdADT]] -> Result (Sign, [Named CMD]) Source # addOmdocToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [TCElement] -> Result (Sign, [Named CMD]) Source # sublogicOfTheo :: CSL -> (Sign, [CMD]) -> () Source #

data EXTPARAM Source #

Extended Parameter Datatype

Constructors

EP Token String APInt

Instances

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

data BASIC_ITEM Source #

basic items: an operator, extended parameter or variable declaration or an axiom

Constructors

Op_decl OP_ITEM
EP_decl [(Token, EPDomain)]
EP_domdecl [(Token, APInt)]
EP_defval [(Token, APInt)]
Var_decls [VAR_ITEM]
Axiom_item (Annoted CMD)

Instances

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

newtype BASIC_SPEC Source #

Constructors

Basic_spec [Annoted BASIC_ITEM]

Instances

Data BASIC_SPEC Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BASIC_SPEC -> c BASIC_SPEC gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BASIC_SPEC toConstr :: BASIC_SPEC -> Constr dataTypeOf :: BASIC_SPEC -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c BASIC_SPEC) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BASIC_SPEC) gmapT :: (forall b. Data b => b -> b) -> BASIC_SPEC -> BASIC_SPEC gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_SPEC -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BASIC_SPEC -> r gmapQ :: (forall d. Data d => d -> u) -> BASIC_SPEC -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> BASIC_SPEC -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> BASIC_SPEC -> m BASIC_SPEC gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_SPEC -> m BASIC_SPEC gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BASIC_SPEC -> m BASIC_SPEC
Show BASIC_SPEC Source #
Methods showsPrec :: Int -> BASIC_SPEC -> ShowS show :: BASIC_SPEC -> String showList :: [BASIC_SPEC] -> ShowS
Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #	Syntax of CSL logic
Methods parsersAndPrinters :: CSL -> Map String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc) Source # parse_basic_spec :: CSL -> Maybe (PrefixMap -> AParser st BASIC_SPEC) Source # parseSingleSymbItem :: CSL -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_items :: CSL -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_map_items :: CSL -> Maybe (AParser st SYMB_MAP_ITEMS) Source # toItem :: CSL -> BASIC_SPEC -> Item Source # symb_items_name :: CSL -> SYMB_ITEMS -> [String] Source #
StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source #	Static Analysis for reduce logic
Methods basic_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])) Source # sen_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, CMD) -> Result CMD) Source # extBasicAnalysis :: CSL -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]) Source # stat_symb_map_items :: CSL -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: CSL -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source # convertTheory :: CSL -> Maybe ((Sign, [Named CMD]) -> BASIC_SPEC) Source # ensures_amalgamability :: CSL -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CSL -> Morphism -> [Named CMD] -> Result (Sign, [Named CMD]) Source # signature_colimit :: CSL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: CSL -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named CMD]) Source # symbol_to_raw :: CSL -> Symbol -> Symbol Source # id_to_raw :: CSL -> Id -> Symbol Source # matches :: CSL -> Symbol -> Symbol -> Bool Source # empty_signature :: CSL -> Sign Source # add_symb_to_sign :: CSL -> Sign -> Symbol -> Result Sign Source # signature_union :: CSL -> Sign -> Sign -> Result Sign Source # signatureDiff :: CSL -> Sign -> Sign -> Result Sign Source # intersection :: CSL -> Sign -> Sign -> Result Sign Source # final_union :: CSL -> Sign -> Sign -> Result Sign Source # morphism_union :: CSL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: CSL -> Sign -> Sign -> Bool Source # subsig_inclusion :: CSL -> Sign -> Sign -> Result Morphism Source # generated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: CSL -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: CSL -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: CSL -> Morphism -> Bool Source # is_injective :: CSL -> Morphism -> Bool Source # theory_to_taxonomy :: CSL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named CMD] -> Result MMiSSOntology Source # corresp2th :: CSL -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named CMD], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CSL -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CSL -> [IRI] -> (Sign, [Named CMD]) -> Result (Sign, [Named CMD]) Source #
Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION] Source #	Instance of Logic for reduce logc
Methods parse_basic_sen :: CSL -> Maybe (BASIC_SPEC -> AParser st CMD) Source # stability :: CSL -> Stability Source # data_logic :: CSL -> Maybe AnyLogic Source # top_sublogic :: CSL -> () Source # all_sublogics :: CSL -> [()] Source # bottomSublogic :: CSL -> Maybe () Source # sublogicDimensions :: CSL -> [[()]] Source # parseSublogic :: CSL -> String -> Maybe () Source # proj_sublogic_epsilon :: CSL -> () -> Sign -> Morphism Source # provers :: CSL -> [Prover Sign CMD Morphism () [EXPRESSION]] Source # default_prover :: CSL -> String Source # cons_checkers :: CSL -> [ConsChecker Sign CMD () Morphism [EXPRESSION]] Source # conservativityCheck :: CSL -> [ConservativityChecker Sign CMD Morphism] Source # empty_proof_tree :: CSL -> [EXPRESSION] Source # syntaxTable :: CSL -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: CSL -> Maybe OMCD Source # export_symToOmdoc :: CSL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CSL -> NameMap Symbol -> CMD -> Result TCorOMElement Source # export_theoryToOmdoc :: CSL -> SigMap Symbol -> Sign -> [Named CMD] -> Result [TCElement] Source # omdocToSym :: CSL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CSL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CMD)) Source # addOMadtToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [[OmdADT]] -> Result (Sign, [Named CMD]) Source # addOmdocToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [TCElement] -> Result (Sign, [Named CMD]) Source # sublogicOfTheo :: CSL -> (Sign, [CMD]) -> () Source #

data SYMB_ITEMS Source #

symbol lists for hiding

Constructors

Symb_items [SYMB] Range

Instances

Eq SYMB_ITEMS Source #
Methods (==) :: SYMB_ITEMS -> SYMB_ITEMS -> Bool (/=) :: SYMB_ITEMS -> SYMB_ITEMS -> Bool
Data SYMB_ITEMS Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB_ITEMS toConstr :: SYMB_ITEMS -> Constr dataTypeOf :: SYMB_ITEMS -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c SYMB_ITEMS) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_ITEMS) gmapT :: (forall b. Data b => b -> b) -> SYMB_ITEMS -> SYMB_ITEMS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r gmapQ :: (forall d. Data d => d -> u) -> SYMB_ITEMS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_ITEMS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS
Show SYMB_ITEMS Source #
Methods showsPrec :: Int -> SYMB_ITEMS -> ShowS show :: SYMB_ITEMS -> String showList :: [SYMB_ITEMS] -> ShowS
Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #	Syntax of CSL logic
Methods parsersAndPrinters :: CSL -> Map String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc) Source # parse_basic_spec :: CSL -> Maybe (PrefixMap -> AParser st BASIC_SPEC) Source # parseSingleSymbItem :: CSL -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_items :: CSL -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_map_items :: CSL -> Maybe (AParser st SYMB_MAP_ITEMS) Source # toItem :: CSL -> BASIC_SPEC -> Item Source # symb_items_name :: CSL -> SYMB_ITEMS -> [String] Source #
StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source #	Static Analysis for reduce logic
Methods basic_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])) Source # sen_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, CMD) -> Result CMD) Source # extBasicAnalysis :: CSL -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]) Source # stat_symb_map_items :: CSL -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: CSL -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source # convertTheory :: CSL -> Maybe ((Sign, [Named CMD]) -> BASIC_SPEC) Source # ensures_amalgamability :: CSL -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CSL -> Morphism -> [Named CMD] -> Result (Sign, [Named CMD]) Source # signature_colimit :: CSL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: CSL -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named CMD]) Source # symbol_to_raw :: CSL -> Symbol -> Symbol Source # id_to_raw :: CSL -> Id -> Symbol Source # matches :: CSL -> Symbol -> Symbol -> Bool Source # empty_signature :: CSL -> Sign Source # add_symb_to_sign :: CSL -> Sign -> Symbol -> Result Sign Source # signature_union :: CSL -> Sign -> Sign -> Result Sign Source # signatureDiff :: CSL -> Sign -> Sign -> Result Sign Source # intersection :: CSL -> Sign -> Sign -> Result Sign Source # final_union :: CSL -> Sign -> Sign -> Result Sign Source # morphism_union :: CSL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: CSL -> Sign -> Sign -> Bool Source # subsig_inclusion :: CSL -> Sign -> Sign -> Result Morphism Source # generated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: CSL -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: CSL -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: CSL -> Morphism -> Bool Source # is_injective :: CSL -> Morphism -> Bool Source # theory_to_taxonomy :: CSL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named CMD] -> Result MMiSSOntology Source # corresp2th :: CSL -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named CMD], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CSL -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CSL -> [IRI] -> (Sign, [Named CMD]) -> Result (Sign, [Named CMD]) Source #
Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION] Source #	Instance of Logic for reduce logc
Methods parse_basic_sen :: CSL -> Maybe (BASIC_SPEC -> AParser st CMD) Source # stability :: CSL -> Stability Source # data_logic :: CSL -> Maybe AnyLogic Source # top_sublogic :: CSL -> () Source # all_sublogics :: CSL -> [()] Source # bottomSublogic :: CSL -> Maybe () Source # sublogicDimensions :: CSL -> [[()]] Source # parseSublogic :: CSL -> String -> Maybe () Source # proj_sublogic_epsilon :: CSL -> () -> Sign -> Morphism Source # provers :: CSL -> [Prover Sign CMD Morphism () [EXPRESSION]] Source # default_prover :: CSL -> String Source # cons_checkers :: CSL -> [ConsChecker Sign CMD () Morphism [EXPRESSION]] Source # conservativityCheck :: CSL -> [ConservativityChecker Sign CMD Morphism] Source # empty_proof_tree :: CSL -> [EXPRESSION] Source # syntaxTable :: CSL -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: CSL -> Maybe OMCD Source # export_symToOmdoc :: CSL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CSL -> NameMap Symbol -> CMD -> Result TCorOMElement Source # export_theoryToOmdoc :: CSL -> SigMap Symbol -> Sign -> [Named CMD] -> Result [TCElement] Source # omdocToSym :: CSL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CSL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CMD)) Source # addOMadtToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [[OmdADT]] -> Result (Sign, [Named CMD]) Source # addOmdocToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [TCElement] -> Result (Sign, [Named CMD]) Source # sublogicOfTheo :: CSL -> (Sign, [CMD]) -> () Source #

newtype SYMB Source #

symbol for identifiers

Constructors

Symb_id Token

Instances

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

data SYMB_MAP_ITEMS Source #

symbol maps for renamings

Constructors

Symb_map_items [SYMB_OR_MAP] Range

Instances

Eq SYMB_MAP_ITEMS Source #
Methods (==) :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool (/=) :: SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS -> Bool
Data SYMB_MAP_ITEMS Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB_MAP_ITEMS -> c SYMB_MAP_ITEMS gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB_MAP_ITEMS toConstr :: SYMB_MAP_ITEMS -> Constr dataTypeOf :: SYMB_MAP_ITEMS -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c SYMB_MAP_ITEMS) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_MAP_ITEMS) gmapT :: (forall b. Data b => b -> b) -> SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r gmapQ :: (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS
Show SYMB_MAP_ITEMS Source #
Methods showsPrec :: Int -> SYMB_MAP_ITEMS -> ShowS show :: SYMB_MAP_ITEMS -> String showList :: [SYMB_MAP_ITEMS] -> ShowS
Syntax CSL BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #	Syntax of CSL logic
Methods parsersAndPrinters :: CSL -> Map String (PrefixMap -> AParser st BASIC_SPEC, BASIC_SPEC -> Doc) Source # parse_basic_spec :: CSL -> Maybe (PrefixMap -> AParser st BASIC_SPEC) Source # parseSingleSymbItem :: CSL -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_items :: CSL -> Maybe (AParser st SYMB_ITEMS) Source # parse_symb_map_items :: CSL -> Maybe (AParser st SYMB_MAP_ITEMS) Source # toItem :: CSL -> BASIC_SPEC -> Item Source # symb_items_name :: CSL -> SYMB_ITEMS -> [String] Source #
StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source #	Static Analysis for reduce logic
Methods basic_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])) Source # sen_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, CMD) -> Result CMD) Source # extBasicAnalysis :: CSL -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]) Source # stat_symb_map_items :: CSL -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: CSL -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source # convertTheory :: CSL -> Maybe ((Sign, [Named CMD]) -> BASIC_SPEC) Source # ensures_amalgamability :: CSL -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CSL -> Morphism -> [Named CMD] -> Result (Sign, [Named CMD]) Source # signature_colimit :: CSL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: CSL -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named CMD]) Source # symbol_to_raw :: CSL -> Symbol -> Symbol Source # id_to_raw :: CSL -> Id -> Symbol Source # matches :: CSL -> Symbol -> Symbol -> Bool Source # empty_signature :: CSL -> Sign Source # add_symb_to_sign :: CSL -> Sign -> Symbol -> Result Sign Source # signature_union :: CSL -> Sign -> Sign -> Result Sign Source # signatureDiff :: CSL -> Sign -> Sign -> Result Sign Source # intersection :: CSL -> Sign -> Sign -> Result Sign Source # final_union :: CSL -> Sign -> Sign -> Result Sign Source # morphism_union :: CSL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: CSL -> Sign -> Sign -> Bool Source # subsig_inclusion :: CSL -> Sign -> Sign -> Result Morphism Source # generated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: CSL -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: CSL -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: CSL -> Morphism -> Bool Source # is_injective :: CSL -> Morphism -> Bool Source # theory_to_taxonomy :: CSL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named CMD] -> Result MMiSSOntology Source # corresp2th :: CSL -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named CMD], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CSL -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CSL -> [IRI] -> (Sign, [Named CMD]) -> Result (Sign, [Named CMD]) Source #
Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION] Source #	Instance of Logic for reduce logc
Methods parse_basic_sen :: CSL -> Maybe (BASIC_SPEC -> AParser st CMD) Source # stability :: CSL -> Stability Source # data_logic :: CSL -> Maybe AnyLogic Source # top_sublogic :: CSL -> () Source # all_sublogics :: CSL -> [()] Source # bottomSublogic :: CSL -> Maybe () Source # sublogicDimensions :: CSL -> [[()]] Source # parseSublogic :: CSL -> String -> Maybe () Source # proj_sublogic_epsilon :: CSL -> () -> Sign -> Morphism Source # provers :: CSL -> [Prover Sign CMD Morphism () [EXPRESSION]] Source # default_prover :: CSL -> String Source # cons_checkers :: CSL -> [ConsChecker Sign CMD () Morphism [EXPRESSION]] Source # conservativityCheck :: CSL -> [ConservativityChecker Sign CMD Morphism] Source # empty_proof_tree :: CSL -> [EXPRESSION] Source # syntaxTable :: CSL -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: CSL -> Maybe OMCD Source # export_symToOmdoc :: CSL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CSL -> NameMap Symbol -> CMD -> Result TCorOMElement Source # export_theoryToOmdoc :: CSL -> SigMap Symbol -> Sign -> [Named CMD] -> Result [TCElement] Source # omdocToSym :: CSL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CSL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CMD)) Source # addOMadtToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [[OmdADT]] -> Result (Sign, [Named CMD]) Source # addOmdocToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [TCElement] -> Result (Sign, [Named CMD]) Source # sublogicOfTheo :: CSL -> (Sign, [CMD]) -> () Source #

data SYMB_OR_MAP Source #

symbol map or renaming (renaming then denotes the identity renaming)

Constructors

Symb SYMB
Symb_map SYMB SYMB Range

Instances

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

data OPNAME Source #

Instances

Eq OPNAME Source #
Methods (==) :: OPNAME -> OPNAME -> Bool (/=) :: OPNAME -> OPNAME -> Bool
Data OPNAME Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OPNAME -> c OPNAME gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OPNAME toConstr :: OPNAME -> Constr dataTypeOf :: OPNAME -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c OPNAME) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OPNAME) gmapT :: (forall b. Data b => b -> b) -> OPNAME -> OPNAME gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OPNAME -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OPNAME -> r gmapQ :: (forall d. Data d => d -> u) -> OPNAME -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OPNAME -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OPNAME -> m OPNAME gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OPNAME -> m OPNAME gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OPNAME -> m OPNAME
Ord OPNAME Source #
Methods compare :: OPNAME -> OPNAME -> Ordering (<) :: OPNAME -> OPNAME -> Bool (<=) :: OPNAME -> OPNAME -> Bool (>) :: OPNAME -> OPNAME -> Bool (>=) :: OPNAME -> OPNAME -> Bool max :: OPNAME -> OPNAME -> OPNAME min :: OPNAME -> OPNAME -> OPNAME
Show OPNAME Source #
Methods showsPrec :: Int -> OPNAME -> ShowS show :: OPNAME -> String showList :: [OPNAME] -> ShowS
ExpressionPrinter (Reader OpInfoNameMap) Source #	An `OpInfoNameMap` can be interpreted as an `ExpressionPrinter`
Methods getOINM :: Reader OpInfoNameMap OpInfoNameMap Source # printConstant :: ConstantName -> Reader OpInfoNameMap Doc Source # printOpname :: OPNAME -> Reader OpInfoNameMap Doc Source # prefixMode :: Reader OpInfoNameMap Bool Source # printArgs :: [Doc] -> Reader OpInfoNameMap Doc Source # printArgPattern :: String -> Reader OpInfoNameMap Doc Source # printInterval :: Double -> Double -> Reader OpInfoNameMap Doc Source # printRational :: APFloat -> Reader OpInfoNameMap Doc Source #

data OPID Source #

Constructors

OpId OPNAME
OpUser ConstantName

Instances

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

data ConstantName Source #

We differentiate between simple constant names and indexed constant names resulting from the extended parameter elimination.

Constructors

SimpleConstant String
ElimConstant String Int

Instances

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

data OP_ITEM Source #

operator symbol declaration

Constructors

Op_item [Token] Range

Instances

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

data VAR_ITEM Source #

variable symbol declaration

Constructors

Var_item [Token] Domain Range

Instances

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

data VarDecl Source #

Constructors

VarDecl Token (Maybe Domain)

Instances

Eq VarDecl Source #
Methods (==) :: VarDecl -> VarDecl -> Bool (/=) :: VarDecl -> VarDecl -> Bool
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
Ord VarDecl Source #
Methods compare :: VarDecl -> VarDecl -> Ordering (<) :: VarDecl -> VarDecl -> Bool (<=) :: VarDecl -> VarDecl -> Bool (>) :: VarDecl -> VarDecl -> Bool (>=) :: VarDecl -> VarDecl -> Bool max :: VarDecl -> VarDecl -> VarDecl min :: VarDecl -> VarDecl -> VarDecl
Show VarDecl Source #
Methods showsPrec :: Int -> VarDecl -> ShowS show :: VarDecl -> String showList :: [VarDecl] -> ShowS

data OpDecl Source #

Constructors

OpDecl ConstantName [EXTPARAM] [VarDecl] Range

Instances

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

data EPDecl Source #

Constructors

EPDecl Token EPDomain (Maybe APInt)

Instances

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

data EPVal Source #

Extended Parameter value may be an integer or a reference to an EPDomVal. This type is used for the domain specification of EPs (see EPDomain).

Constructors

EPVal APInt
EPConstRef Token

Instances

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

getEPVarRef :: EPVal -> Maybe Token Source #

type Domain = SetOrInterval GroundConstant Source #

type EPDomain = ClosedInterval EPVal Source #

data GroundConstant Source #

Constructors

GCI APInt
GCR APFloat

Instances

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

cmpFloatToInt :: APFloat -> APInt -> Ordering Source #

data AssDefinition Source #

A constant or function definition

Constructors

ConstDef EXPRESSION
FunDef [String] EXPRESSION

Instances

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

data InstantiatedConstant Source #

Constructors

InstantiatedConstant
Fields constName :: ConstantName instantiation :: [EXPRESSION]

Instances

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

data CMD Source #

Constructors

Ass OpDecl EXPRESSION
Cmd String [EXPRESSION]
Sequence [CMD]
Cond [(EXPRESSION, [CMD])]
Repeat EXPRESSION [CMD]

Instances

Eq CMD Source #
Methods (==) :: CMD -> CMD -> Bool (/=) :: CMD -> CMD -> Bool
Data CMD Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CMD -> c CMD gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CMD toConstr :: CMD -> Constr dataTypeOf :: CMD -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c CMD) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CMD) gmapT :: (forall b. Data b => b -> b) -> CMD -> CMD gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CMD -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CMD -> r gmapQ :: (forall d. Data d => d -> u) -> CMD -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> CMD -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> CMD -> m CMD gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CMD -> m CMD gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CMD -> m CMD
Ord CMD Source #
Methods compare :: CMD -> CMD -> Ordering (<) :: CMD -> CMD -> Bool (<=) :: CMD -> CMD -> Bool (>) :: CMD -> CMD -> Bool (>=) :: CMD -> CMD -> Bool max :: CMD -> CMD -> CMD min :: CMD -> CMD -> CMD
Show CMD Source #
Methods showsPrec :: Int -> CMD -> ShowS show :: CMD -> String showList :: [CMD] -> ShowS
Sentences CSL CMD Sign Morphism Symbol Source #	Instance of Sentences for reduce logic
Methods map_sen :: CSL -> Morphism -> CMD -> Result CMD Source # simplify_sen :: CSL -> Sign -> CMD -> CMD Source # negation :: CSL -> CMD -> Maybe CMD Source # print_sign :: CSL -> Sign -> Doc Source # print_named :: CSL -> Named CMD -> Doc Source # sym_of :: CSL -> Sign -> [Set Symbol] Source # mostSymsOf :: CSL -> Sign -> [Symbol] Source # symmap_of :: CSL -> Morphism -> EndoMap Symbol Source # sym_name :: CSL -> Symbol -> Id Source # sym_label :: CSL -> Symbol -> Maybe String Source # fullSymName :: CSL -> Symbol -> String Source # symKind :: CSL -> Symbol -> String Source # symsOfSen :: CSL -> Sign -> CMD -> [Symbol] Source # pair_symbols :: CSL -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source #	Static Analysis for reduce logic
Methods basic_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])) Source # sen_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, CMD) -> Result CMD) Source # extBasicAnalysis :: CSL -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]) Source # stat_symb_map_items :: CSL -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: CSL -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source # convertTheory :: CSL -> Maybe ((Sign, [Named CMD]) -> BASIC_SPEC) Source # ensures_amalgamability :: CSL -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CSL -> Morphism -> [Named CMD] -> Result (Sign, [Named CMD]) Source # signature_colimit :: CSL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: CSL -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named CMD]) Source # symbol_to_raw :: CSL -> Symbol -> Symbol Source # id_to_raw :: CSL -> Id -> Symbol Source # matches :: CSL -> Symbol -> Symbol -> Bool Source # empty_signature :: CSL -> Sign Source # add_symb_to_sign :: CSL -> Sign -> Symbol -> Result Sign Source # signature_union :: CSL -> Sign -> Sign -> Result Sign Source # signatureDiff :: CSL -> Sign -> Sign -> Result Sign Source # intersection :: CSL -> Sign -> Sign -> Result Sign Source # final_union :: CSL -> Sign -> Sign -> Result Sign Source # morphism_union :: CSL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: CSL -> Sign -> Sign -> Bool Source # subsig_inclusion :: CSL -> Sign -> Sign -> Result Morphism Source # generated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: CSL -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: CSL -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: CSL -> Morphism -> Bool Source # is_injective :: CSL -> Morphism -> Bool Source # theory_to_taxonomy :: CSL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named CMD] -> Result MMiSSOntology Source # corresp2th :: CSL -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named CMD], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CSL -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CSL -> [IRI] -> (Sign, [Named CMD]) -> Result (Sign, [Named CMD]) Source #
Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION] Source #	Instance of Logic for reduce logc
Methods parse_basic_sen :: CSL -> Maybe (BASIC_SPEC -> AParser st CMD) Source # stability :: CSL -> Stability Source # data_logic :: CSL -> Maybe AnyLogic Source # top_sublogic :: CSL -> () Source # all_sublogics :: CSL -> [()] Source # bottomSublogic :: CSL -> Maybe () Source # sublogicDimensions :: CSL -> [[()]] Source # parseSublogic :: CSL -> String -> Maybe () Source # proj_sublogic_epsilon :: CSL -> () -> Sign -> Morphism Source # provers :: CSL -> [Prover Sign CMD Morphism () [EXPRESSION]] Source # default_prover :: CSL -> String Source # cons_checkers :: CSL -> [ConsChecker Sign CMD () Morphism [EXPRESSION]] Source # conservativityCheck :: CSL -> [ConservativityChecker Sign CMD Morphism] Source # empty_proof_tree :: CSL -> [EXPRESSION] Source # syntaxTable :: CSL -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: CSL -> Maybe OMCD Source # export_symToOmdoc :: CSL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CSL -> NameMap Symbol -> CMD -> Result TCorOMElement Source # export_theoryToOmdoc :: CSL -> SigMap Symbol -> Sign -> [Named CMD] -> Result [TCElement] Source # omdocToSym :: CSL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CSL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CMD)) Source # addOMadtToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [[OmdADT]] -> Result (Sign, [Named CMD]) Source # addOmdocToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [TCElement] -> Result (Sign, [Named CMD]) Source # sublogicOfTheo :: CSL -> (Sign, [CMD]) -> () Source #

class OperatorState a where Source #

Minimal complete definition

lookupOperator, lookupBinder

Methods

addVar :: a -> String -> a Source #

isVar :: a -> String -> Bool Source #

lookupOperator :: a -> String -> Int -> Either Bool OpInfo Source #

lookupBinder :: a -> String -> Maybe OpInfo Source #

Instances

OperatorState () Source #
Methods addVar :: () -> String -> () Source # isVar :: () -> String -> Bool Source # lookupOperator :: () -> String -> Int -> Either Bool OpInfo Source # lookupBinder :: () -> String -> Maybe OpInfo Source #
OperatorState a => OperatorState (OpVarState a) Source #
Methods addVar :: OpVarState a -> String -> OpVarState a Source # isVar :: OpVarState a -> String -> Bool Source # lookupOperator :: OpVarState a -> String -> Int -> Either Bool OpInfo Source # lookupBinder :: OpVarState a -> String -> Maybe OpInfo Source #
OperatorState (OpInfoMap, BindInfoMap) Source #
Methods addVar :: (OpInfoMap, BindInfoMap) -> String -> (OpInfoMap, BindInfoMap) Source # isVar :: (OpInfoMap, BindInfoMap) -> String -> Bool Source # lookupOperator :: (OpInfoMap, BindInfoMap) -> String -> Int -> Either Bool OpInfo Source # lookupBinder :: (OpInfoMap, BindInfoMap) -> String -> Maybe OpInfo Source #

data OpInfo Source #

Constructors

OpInfo
Fields prec :: Int precedence between 0 and maxPrecedence infx :: Bool True = infix arity :: Int the operator arity foldNAry :: Bool True = fold nary-applications during construction into binary ones opname :: OPNAME The actual operator name bind :: Maybe BindInfo More info for binders

Instances

Eq OpInfo Source #
Methods (==) :: OpInfo -> OpInfo -> Bool (/=) :: OpInfo -> OpInfo -> Bool
Data OpInfo Source #
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpInfo -> c OpInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpInfo toConstr :: OpInfo -> Constr dataTypeOf :: OpInfo -> DataType dataCast1 :: Typeable (* -> ) t => (forall d. Data d => c (t d)) -> Maybe (c OpInfo) dataCast2 :: Typeable ( -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpInfo) gmapT :: (forall b. Data b => b -> b) -> OpInfo -> OpInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r gmapQ :: (forall d. Data d => d -> u) -> OpInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OpInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo
Ord OpInfo Source #
Methods compare :: OpInfo -> OpInfo -> Ordering (<) :: OpInfo -> OpInfo -> Bool (<=) :: OpInfo -> OpInfo -> Bool (>) :: OpInfo -> OpInfo -> Bool (>=) :: OpInfo -> OpInfo -> Bool max :: OpInfo -> OpInfo -> OpInfo min :: OpInfo -> OpInfo -> OpInfo
Show OpInfo Source #
Methods showsPrec :: Int -> OpInfo -> ShowS show :: OpInfo -> String showList :: [OpInfo] -> ShowS
ExpressionPrinter (Reader OpInfoNameMap) Source #	An `OpInfoNameMap` can be interpreted as an `ExpressionPrinter`
Methods getOINM :: Reader OpInfoNameMap OpInfoNameMap Source # printConstant :: ConstantName -> Reader OpInfoNameMap Doc Source # printOpname :: OPNAME -> Reader OpInfoNameMap Doc Source # prefixMode :: Reader OpInfoNameMap Bool Source # printArgs :: [Doc] -> Reader OpInfoNameMap Doc Source # printArgPattern :: String -> Reader OpInfoNameMap Doc Source # printInterval :: Double -> Double -> Reader OpInfoNameMap Doc Source # printRational :: APFloat -> Reader OpInfoNameMap Doc Source #
OperatorState (OpInfoMap, BindInfoMap) Source #
Methods addVar :: (OpInfoMap, BindInfoMap) -> String -> (OpInfoMap, BindInfoMap) Source # isVar :: (OpInfoMap, BindInfoMap) -> String -> Bool Source # lookupOperator :: (OpInfoMap, BindInfoMap) -> String -> Int -> Either Bool OpInfo Source # lookupBinder :: (OpInfoMap, BindInfoMap) -> String -> Maybe OpInfo Source #

data BindInfo Source #

Constructors

BindInfo
Fields bindingVarPos :: [Int] argument positions of binding variables boundBodyPos :: [Int] argument positions of bound terms

Instances

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

operatorInfo :: [OpInfo] Source #

Mapping of operator names to arity-OpInfo-maps (an operator may behave differently for different arities).

operatorInfoMap :: OpInfoMap Source #

opInfoMap for the predefined operatorInfo

operatorInfoNameMap :: OpInfoNameMap Source #

opInfoNameMap for the predefined operatorInfo

operatorBindInfoMap :: BindInfoMap Source #

mergeOpArityMap :: Ord a => OpInfoArityMap a -> OpInfoArityMap a -> OpInfoArityMap a Source #

Merges two OpInfoArityMaps together with the first map as default map and the second overwriting the default values

getOpInfoMap :: (OpInfo -> String) -> [OpInfo] -> OpInfoMap Source #

Mapping of operator names to arity-OpInfo-maps (an operator may behave differently for different arities).

getOpInfoNameMap :: [OpInfo] -> OpInfoNameMap Source #

Same as operatorInfoMap but with keys of type OPNAME instead of String

getBindInfoMap :: [OpInfo] -> BindInfoMap Source #

a special map for binders which have to be unique for each name (no different arities).

lookupOpInfo Source #

Arguments

:: OpInfoNameMap
-> OPID	operator id
-> Int	operator arity
-> Either Bool OpInfo

For the given name and arity we lookup an OpInfo, where arity=-1 means flexible arity. If an operator is registered for the given string but not for the arity we return: Left True.

lookupOpInfoForParsing Source #

Arguments

:: OpInfoMap	map to be used for lookup
-> String	operator name
-> Int	operator arity
-> Either Bool OpInfo

For the given name and arity we lookup an OpInfo, where arity=-1 means flexible arity. If an operator is registered for the given string but not for the arity we return: Left True. This function is designed for the lookup of operators in not statically analyzed terms. For statically analyzed terms use lookupOpInfo.

lookupBindInfo Source #

Arguments

:: OpInfoNameMap
-> OPID	operator name
-> Int	operator arity
-> Maybe BindInfo

For the given name and arity we lookup an BindInfo, where arity=-1 means flexible arity.

type APInt = Integer Source #

type APFloat = Rational Source #

toFraction :: APFloat -> (Integer, Integer) Source #

fromFraction :: Integer -> Integer -> APFloat Source #

type OpInfoMap = OpInfoArityMap String Source #

type OpInfoNameMap = OpInfoArityMap OPNAME Source #

type BindInfoMap = Map String OpInfo Source #

showOPNAME :: OPNAME -> String Source #

maxPrecedence :: Int Source #

OP_mult
OP_div
OP_plus
OP_minus
OP_neg
OP_pow
OP_fthrt
OP_sqrt
OP_abs
OP_max
OP_min
OP_sign
OP_cos
OP_sin
OP_tan
OP_cot
OP_Pi
OP_reldist
OP_minimize
OP_minloc
OP_maximize
OP_maxloc
OP_factor
OP_approx
OP_divide
OP_factorize
OP_int
OP_rlqe
OP_simplify
OP_solve
OP_neq
OP_lt
OP_leq
OP_eq
OP_gt
OP_geq
OP_convergence
OP_reldistLe
OP_in
OP_undef
OP_failure
OP_false
OP_true
OP_not
OP_and
OP_or
OP_impl
OP_ex
OP_all
OP_hastype
OP_real