Hets - the Heterogeneous Tool Set

Copyright(c) Dominik Dietrich Ewaryst Schulz DFKI Bremen 2010
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerEwaryst.Schulz@dfki.de
Stabilityexperimental
Portabilityportable
Safe HaskellSafe

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

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 # 
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 #

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

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

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 #

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

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 #

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

Instances

Eq SYMB_MAP_ITEMS Source # 
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

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 #

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

data OPID Source #

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 # 
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 #

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

data GroundConstant Source #

Constructors

GCI APInt 
GCR APFloat 

Instances

Eq GroundConstant Source # 
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 # 
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 # 
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 # 
Show AssDefinition Source # 

Methods

showsPrec :: Int -> AssDefinition -> ShowS

show :: AssDefinition -> String

showList :: [AssDefinition] -> ShowS

data InstantiatedConstant Source #

Instances

Eq InstantiatedConstant Source # 
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 # 
Show InstantiatedConstant Source # 

Methods

showsPrec :: Int -> InstantiatedConstant -> ShowS

show :: InstantiatedConstant -> String

showList :: [InstantiatedConstant] -> ShowS

data CMD Source #

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

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 #

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

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

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

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 #