Hets - the Heterogeneous Tool Set

Copyright(c) C. Maeder DFKI 2008
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

VSE.As

Contents

Description

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

Synopsis

Documentation

data Paramkind Source #

input or output procedure parameter kind

Constructors

In 
Out 

Instances

Eq Paramkind Source # 

Methods

(==) :: Paramkind -> Paramkind -> Bool

(/=) :: Paramkind -> Paramkind -> Bool

Data Paramkind Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Paramkind -> c Paramkind

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Paramkind

toConstr :: Paramkind -> Constr

dataTypeOf :: Paramkind -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Paramkind)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Paramkind)

gmapT :: (forall b. Data b => b -> b) -> Paramkind -> Paramkind

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Paramkind -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Paramkind -> r

gmapQ :: (forall d. Data d => d -> u) -> Paramkind -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Paramkind -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Paramkind -> m Paramkind

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Paramkind -> m Paramkind

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Paramkind -> m Paramkind

Ord Paramkind Source # 

Methods

compare :: Paramkind -> Paramkind -> Ordering

(<) :: Paramkind -> Paramkind -> Bool

(<=) :: Paramkind -> Paramkind -> Bool

(>) :: Paramkind -> Paramkind -> Bool

(>=) :: Paramkind -> Paramkind -> Bool

max :: Paramkind -> Paramkind -> Paramkind

min :: Paramkind -> Paramkind -> Paramkind

Show Paramkind Source # 

Methods

showsPrec :: Int -> Paramkind -> ShowS

show :: Paramkind -> String

showList :: [Paramkind] -> ShowS

data Procparam Source #

a procedure parameter

Constructors

Procparam Paramkind SORT 

Instances

Eq Procparam Source # 

Methods

(==) :: Procparam -> Procparam -> Bool

(/=) :: Procparam -> Procparam -> Bool

Data Procparam Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Procparam -> c Procparam

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Procparam

toConstr :: Procparam -> Constr

dataTypeOf :: Procparam -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Procparam)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Procparam)

gmapT :: (forall b. Data b => b -> b) -> Procparam -> Procparam

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Procparam -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Procparam -> r

gmapQ :: (forall d. Data d => d -> u) -> Procparam -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Procparam -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Procparam -> m Procparam

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Procparam -> m Procparam

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Procparam -> m Procparam

Ord Procparam Source # 

Methods

compare :: Procparam -> Procparam -> Ordering

(<) :: Procparam -> Procparam -> Bool

(<=) :: Procparam -> Procparam -> Bool

(>) :: Procparam -> Procparam -> Bool

(>=) :: Procparam -> Procparam -> Bool

max :: Procparam -> Procparam -> Procparam

min :: Procparam -> Procparam -> Procparam

Show Procparam Source # 

Methods

showsPrec :: Int -> Procparam -> ShowS

show :: Procparam -> String

showList :: [Procparam] -> ShowS

Pretty Procparam Source # 

data Profile Source #

procedure or function declaration

Constructors

Profile [Procparam] (Maybe SORT) 

Instances

Eq Profile Source # 

Methods

(==) :: Profile -> Profile -> Bool

(/=) :: Profile -> Profile -> Bool

Data Profile Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Profile -> c Profile

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Profile

toConstr :: Profile -> Constr

dataTypeOf :: Profile -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Profile)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Profile)

gmapT :: (forall b. Data b => b -> b) -> Profile -> Profile

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Profile -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Profile -> r

gmapQ :: (forall d. Data d => d -> u) -> Profile -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Profile -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Profile -> m Profile

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Profile -> m Profile

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Profile -> m Profile

Ord Profile Source # 

Methods

compare :: Profile -> Profile -> Ordering

(<) :: Profile -> Profile -> Bool

(<=) :: Profile -> Profile -> Bool

(>) :: Profile -> Profile -> Bool

(>=) :: Profile -> Profile -> Bool

max :: Profile -> Profile -> Profile

min :: Profile -> Profile -> Profile

Show Profile Source # 

Methods

showsPrec :: Int -> Profile -> ShowS

show :: Profile -> String

showList :: [Profile] -> ShowS

Pretty Profile Source # 

data Sigentry Source #

further VSE signature entries

Constructors

Procedure Id Profile Range 

Instances

Eq Sigentry Source # 

Methods

(==) :: Sigentry -> Sigentry -> Bool

(/=) :: Sigentry -> Sigentry -> Bool

Data Sigentry Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sigentry -> c Sigentry

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sigentry

toConstr :: Sigentry -> Constr

dataTypeOf :: Sigentry -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Sigentry)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sigentry)

gmapT :: (forall b. Data b => b -> b) -> Sigentry -> Sigentry

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sigentry -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sigentry -> r

gmapQ :: (forall d. Data d => d -> u) -> Sigentry -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Sigentry -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sigentry -> m Sigentry

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sigentry -> m Sigentry

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sigentry -> m Sigentry

Ord Sigentry Source # 

Methods

compare :: Sigentry -> Sigentry -> Ordering

(<) :: Sigentry -> Sigentry -> Bool

(<=) :: Sigentry -> Sigentry -> Bool

(>) :: Sigentry -> Sigentry -> Bool

(>=) :: Sigentry -> Sigentry -> Bool

max :: Sigentry -> Sigentry -> Sigentry

min :: Sigentry -> Sigentry -> Sigentry

Show Sigentry Source # 

Methods

showsPrec :: Int -> Sigentry -> ShowS

show :: Sigentry -> String

showList :: [Sigentry] -> ShowS

Pretty Sigentry Source # 

data Procdecls Source #

Instances

Eq Procdecls Source # 

Methods

(==) :: Procdecls -> Procdecls -> Bool

(/=) :: Procdecls -> Procdecls -> Bool

Data Procdecls Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Procdecls -> c Procdecls

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Procdecls

toConstr :: Procdecls -> Constr

dataTypeOf :: Procdecls -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Procdecls)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Procdecls)

gmapT :: (forall b. Data b => b -> b) -> Procdecls -> Procdecls

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Procdecls -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Procdecls -> r

gmapQ :: (forall d. Data d => d -> u) -> Procdecls -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Procdecls -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Procdecls -> m Procdecls

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Procdecls -> m Procdecls

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Procdecls -> m Procdecls

Ord Procdecls Source # 

Methods

compare :: Procdecls -> Procdecls -> Ordering

(<) :: Procdecls -> Procdecls -> Bool

(<=) :: Procdecls -> Procdecls -> Bool

(>) :: Procdecls -> Procdecls -> Bool

(>=) :: Procdecls -> Procdecls -> Bool

max :: Procdecls -> Procdecls -> Procdecls

min :: Procdecls -> Procdecls -> Procdecls

Show Procdecls Source # 

Methods

showsPrec :: Int -> Procdecls -> ShowS

show :: Procdecls -> String

showList :: [Procdecls] -> ShowS

GetRange Procdecls Source # 
Pretty Procdecls Source # 
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 

Methods

basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source #

sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source #

ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source #

signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source #

qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source #

symbol_to_raw :: VSE -> Symbol -> RawSymbol Source #

id_to_raw :: VSE -> Id -> RawSymbol Source #

matches :: VSE -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: VSE -> VSESign Source #

add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source #

signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source #

intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source #

final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source #

is_subsig :: VSE -> VSESign -> VSESign -> Bool Source #

subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source #

generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source #

induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source #

is_transportable :: VSE -> VSEMor -> Bool Source #

is_injective :: VSE -> VSEMor -> Bool Source #

theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #

Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source #

stability :: VSE -> Stability Source #

data_logic :: VSE -> Maybe AnyLogic Source #

top_sublogic :: VSE -> () Source #

all_sublogics :: VSE -> [()] Source #

bottomSublogic :: VSE -> Maybe () Source #

sublogicDimensions :: VSE -> [[()]] Source #

parseSublogic :: VSE -> String -> Maybe () Source #

proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source #

provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source #

default_prover :: VSE -> String Source #

cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source #

conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source #

empty_proof_tree :: VSE -> () Source #

syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source #

omdoc_metatheory :: VSE -> Maybe OMCD Source #

export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source #

addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source #

Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 

data Ranged a Source #

wrapper for positions

Constructors

Ranged 

Fields

Instances

Sentences VSE Sentence VSESign VSEMor Symbol Source # 
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 

Methods

basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source #

sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source #

ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source #

signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source #

qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source #

symbol_to_raw :: VSE -> Symbol -> RawSymbol Source #

id_to_raw :: VSE -> Id -> RawSymbol Source #

matches :: VSE -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: VSE -> VSESign Source #

add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source #

signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source #

intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source #

final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source #

is_subsig :: VSE -> VSESign -> VSESign -> Bool Source #

subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source #

generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source #

induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source #

is_transportable :: VSE -> VSEMor -> Bool Source #

is_injective :: VSE -> VSEMor -> Bool Source #

theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #

Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source #

stability :: VSE -> Stability Source #

data_logic :: VSE -> Maybe AnyLogic Source #

top_sublogic :: VSE -> () Source #

all_sublogics :: VSE -> [()] Source #

bottomSublogic :: VSE -> Maybe () Source #

sublogicDimensions :: VSE -> [[()]] Source #

parseSublogic :: VSE -> String -> Maybe () Source #

proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source #

provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source #

default_prover :: VSE -> String Source #

cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source #

conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source #

empty_proof_tree :: VSE -> () Source #

syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source #

omdoc_metatheory :: VSE -> Maybe OMCD Source #

export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source #

addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source #

Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Eq a => Eq (Ranged a) Source # 

Methods

(==) :: Ranged a -> Ranged a -> Bool

(/=) :: Ranged a -> Ranged a -> Bool

Data a => Data (Ranged a) Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ranged a -> c (Ranged a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Ranged a)

toConstr :: Ranged a -> Constr

dataTypeOf :: Ranged a -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Ranged a))

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ranged a))

gmapT :: (forall b. Data b => b -> b) -> Ranged a -> Ranged a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ranged a -> r

gmapQ :: (forall d. Data d => d -> u) -> Ranged a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Ranged a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ranged a -> m (Ranged a)

Ord a => Ord (Ranged a) Source # 

Methods

compare :: Ranged a -> Ranged a -> Ordering

(<) :: Ranged a -> Ranged a -> Bool

(<=) :: Ranged a -> Ranged a -> Bool

(>) :: Ranged a -> Ranged a -> Bool

(>=) :: Ranged a -> Ranged a -> Bool

max :: Ranged a -> Ranged a -> Ranged a

min :: Ranged a -> Ranged a -> Ranged a

Show a => Show (Ranged a) Source # 

Methods

showsPrec :: Int -> Ranged a -> ShowS

show :: Ranged a -> String

showList :: [Ranged a] -> ShowS

GetRange (Ranged a) Source # 
Pretty a => Pretty (Ranged a) Source # 

Methods

pretty :: Ranged a -> Doc Source #

pretties :: [Ranged a] -> Doc Source #

FormExtension a => FormExtension (Ranged a) Source # 

Methods

isQuantifierLike :: Ranged a -> Bool Source #

prefixExt :: Ranged a -> Doc -> Doc Source #

mkRanged :: a -> Ranged a Source #

attach a nullRange

type Program = Ranged PlainProgram Source #

programs with ranges

data PlainProgram Source #

programs based on restricted terms and formulas

Constructors

Abort 
Skip 
Assign VAR (TERM ()) 
Call (FORMULA ())

a procedure call as predication

Return (TERM ()) 
Block [VAR_DECL] Program 
Seq Program Program 
If (FORMULA ()) Program Program 
While (FORMULA ()) Program 

Instances

Eq PlainProgram Source # 

Methods

(==) :: PlainProgram -> PlainProgram -> Bool

(/=) :: PlainProgram -> PlainProgram -> Bool

Data PlainProgram Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PlainProgram -> c PlainProgram

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PlainProgram

toConstr :: PlainProgram -> Constr

dataTypeOf :: PlainProgram -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c PlainProgram)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PlainProgram)

gmapT :: (forall b. Data b => b -> b) -> PlainProgram -> PlainProgram

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PlainProgram -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PlainProgram -> r

gmapQ :: (forall d. Data d => d -> u) -> PlainProgram -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> PlainProgram -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PlainProgram -> m PlainProgram

Ord PlainProgram Source # 
Show PlainProgram Source # 

Methods

showsPrec :: Int -> PlainProgram -> ShowS

show :: PlainProgram -> String

showList :: [PlainProgram] -> ShowS

Pretty PlainProgram Source # 

data VarDecl Source #

alternative variable declaration

Constructors

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

Instances

Data VarDecl Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VarDecl -> c VarDecl

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VarDecl

toConstr :: VarDecl -> Constr

dataTypeOf :: VarDecl -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c VarDecl)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarDecl)

gmapT :: (forall b. Data b => b -> b) -> VarDecl -> VarDecl

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VarDecl -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VarDecl -> r

gmapQ :: (forall d. Data d => d -> u) -> VarDecl -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> VarDecl -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VarDecl -> m VarDecl

Show VarDecl Source # 

Methods

showsPrec :: Int -> VarDecl -> ShowS

show :: VarDecl -> String

showList :: [VarDecl] -> ShowS

Pretty VarDecl Source # 

data VSEforms Source #

extend CASL formulas by box or diamond formulas and defprocs

Instances

Eq VSEforms Source # 

Methods

(==) :: VSEforms -> VSEforms -> Bool

(/=) :: VSEforms -> VSEforms -> Bool

Data VSEforms Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VSEforms -> c VSEforms

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VSEforms

toConstr :: VSEforms -> Constr

dataTypeOf :: VSEforms -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c VSEforms)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VSEforms)

gmapT :: (forall b. Data b => b -> b) -> VSEforms -> VSEforms

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VSEforms -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VSEforms -> r

gmapQ :: (forall d. Data d => d -> u) -> VSEforms -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> VSEforms -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> VSEforms -> m VSEforms

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VSEforms -> m VSEforms

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VSEforms -> m VSEforms

Ord VSEforms Source # 

Methods

compare :: VSEforms -> VSEforms -> Ordering

(<) :: VSEforms -> VSEforms -> Bool

(<=) :: VSEforms -> VSEforms -> Bool

(>) :: VSEforms -> VSEforms -> Bool

(>=) :: VSEforms -> VSEforms -> Bool

max :: VSEforms -> VSEforms -> VSEforms

min :: VSEforms -> VSEforms -> VSEforms

Show VSEforms Source # 

Methods

showsPrec :: Int -> VSEforms -> ShowS

show :: VSEforms -> String

showList :: [VSEforms] -> ShowS

GetRange VSEforms Source # 
Pretty VSEforms Source # 
FormExtension VSEforms Source # 
Sentences VSE Sentence VSESign VSEMor Symbol Source # 
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 

Methods

basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source #

sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source #

ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source #

signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source #

qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source #

symbol_to_raw :: VSE -> Symbol -> RawSymbol Source #

id_to_raw :: VSE -> Id -> RawSymbol Source #

matches :: VSE -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: VSE -> VSESign Source #

add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source #

signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source #

intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source #

final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source #

is_subsig :: VSE -> VSESign -> VSESign -> Bool Source #

subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source #

generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source #

induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source #

is_transportable :: VSE -> VSEMor -> Bool Source #

is_injective :: VSE -> VSEMor -> Bool Source #

theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #

Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source #

stability :: VSE -> Stability Source #

data_logic :: VSE -> Maybe AnyLogic Source #

top_sublogic :: VSE -> () Source #

all_sublogics :: VSE -> [()] Source #

bottomSublogic :: VSE -> Maybe () Source #

sublogicDimensions :: VSE -> [[()]] Source #

parseSublogic :: VSE -> String -> Maybe () Source #

proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source #

provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source #

default_prover :: VSE -> String Source #

cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source #

conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source #

empty_proof_tree :: VSE -> () Source #

syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source #

omdoc_metatheory :: VSE -> Maybe OMCD Source #

export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source #

addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source #

Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 

data BoxOrDiamond Source #

box or diamond indicator

Constructors

Box 
Diamond 

Instances

Eq BoxOrDiamond Source # 

Methods

(==) :: BoxOrDiamond -> BoxOrDiamond -> Bool

(/=) :: BoxOrDiamond -> BoxOrDiamond -> Bool

Data BoxOrDiamond Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BoxOrDiamond -> c BoxOrDiamond

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BoxOrDiamond

toConstr :: BoxOrDiamond -> Constr

dataTypeOf :: BoxOrDiamond -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c BoxOrDiamond)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BoxOrDiamond)

gmapT :: (forall b. Data b => b -> b) -> BoxOrDiamond -> BoxOrDiamond

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BoxOrDiamond -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BoxOrDiamond -> r

gmapQ :: (forall d. Data d => d -> u) -> BoxOrDiamond -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BoxOrDiamond -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BoxOrDiamond -> m BoxOrDiamond

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BoxOrDiamond -> m BoxOrDiamond

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BoxOrDiamond -> m BoxOrDiamond

Ord BoxOrDiamond Source # 
Show BoxOrDiamond Source # 

Methods

showsPrec :: Int -> BoxOrDiamond -> ShowS

show :: BoxOrDiamond -> String

showList :: [BoxOrDiamond] -> ShowS

data ProcKind Source #

Constructors

Proc 
Func 

Instances

Eq ProcKind Source # 

Methods

(==) :: ProcKind -> ProcKind -> Bool

(/=) :: ProcKind -> ProcKind -> Bool

Data ProcKind Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProcKind -> c ProcKind

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProcKind

toConstr :: ProcKind -> Constr

dataTypeOf :: ProcKind -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ProcKind)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProcKind)

gmapT :: (forall b. Data b => b -> b) -> ProcKind -> ProcKind

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProcKind -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProcKind -> r

gmapQ :: (forall d. Data d => d -> u) -> ProcKind -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProcKind -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProcKind -> m ProcKind

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProcKind -> m ProcKind

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProcKind -> m ProcKind

Ord ProcKind Source # 

Methods

compare :: ProcKind -> ProcKind -> Ordering

(<) :: ProcKind -> ProcKind -> Bool

(<=) :: ProcKind -> ProcKind -> Bool

(>) :: ProcKind -> ProcKind -> Bool

(>=) :: ProcKind -> ProcKind -> Bool

max :: ProcKind -> ProcKind -> ProcKind

min :: ProcKind -> ProcKind -> ProcKind

Show ProcKind Source # 

Methods

showsPrec :: Int -> ProcKind -> ShowS

show :: ProcKind -> String

showList :: [ProcKind] -> ShowS

data Defproc Source #

procedure definitions as basic items becoming sentences

Instances

Eq Defproc Source # 

Methods

(==) :: Defproc -> Defproc -> Bool

(/=) :: Defproc -> Defproc -> Bool

Data Defproc Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Defproc -> c Defproc

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Defproc

toConstr :: Defproc -> Constr

dataTypeOf :: Defproc -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Defproc)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defproc)

gmapT :: (forall b. Data b => b -> b) -> Defproc -> Defproc

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defproc -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defproc -> r

gmapQ :: (forall d. Data d => d -> u) -> Defproc -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Defproc -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Defproc -> m Defproc

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Defproc -> m Defproc

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Defproc -> m Defproc

Ord Defproc Source # 

Methods

compare :: Defproc -> Defproc -> Ordering

(<) :: Defproc -> Defproc -> Bool

(<=) :: Defproc -> Defproc -> Bool

(>) :: Defproc -> Defproc -> Bool

(>=) :: Defproc -> Defproc -> Bool

max :: Defproc -> Defproc -> Defproc

min :: Defproc -> Defproc -> Defproc

Show Defproc Source # 

Methods

showsPrec :: Int -> Defproc -> ShowS

show :: Defproc -> String

showList :: [Defproc] -> ShowS

Pretty Defproc Source # 

data Procs Source #

Constructors

Procs 

Fields

Instances

Eq Procs Source # 

Methods

(==) :: Procs -> Procs -> Bool

(/=) :: Procs -> Procs -> Bool

Data Procs Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Procs -> c Procs

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Procs

toConstr :: Procs -> Constr

dataTypeOf :: Procs -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Procs)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Procs)

gmapT :: (forall b. Data b => b -> b) -> Procs -> Procs

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Procs -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Procs -> r

gmapQ :: (forall d. Data d => d -> u) -> Procs -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Procs -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Procs -> m Procs

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Procs -> m Procs

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Procs -> m Procs

Ord Procs Source # 

Methods

compare :: Procs -> Procs -> Ordering

(<) :: Procs -> Procs -> Bool

(<=) :: Procs -> Procs -> Bool

(>) :: Procs -> Procs -> Bool

(>=) :: Procs -> Procs -> Bool

max :: Procs -> Procs -> Procs

min :: Procs -> Procs -> Procs

Show Procs Source # 

Methods

showsPrec :: Int -> Procs -> ShowS

show :: Procs -> String

showList :: [Procs] -> ShowS

Pretty Procs Source # 
Sentences VSE Sentence VSESign VSEMor Symbol Source # 
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 

Methods

basic_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, GlobalAnnos) -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])) Source #

sen_analysis :: VSE -> Maybe ((VSEBasicSpec, VSESign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: VSE -> IRI -> LibName -> VSEBasicSpec -> VSESign -> GlobalAnnos -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: VSE -> VSESign -> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol] Source #

convertTheory :: VSE -> Maybe ((VSESign, [Named Sentence]) -> VSEBasicSpec) Source #

ensures_amalgamability :: VSE -> ([CASLAmalgOpt], Gr VSESign (Int, VSEMor), [(Int, VSEMor)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: VSE -> VSEMor -> [Named Sentence] -> Result (VSESign, [Named Sentence]) Source #

signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor) Source #

qualify :: VSE -> SIMPLE_ID -> LibName -> VSEMor -> VSESign -> Result (VSEMor, [Named Sentence]) Source #

symbol_to_raw :: VSE -> Symbol -> RawSymbol Source #

id_to_raw :: VSE -> Id -> RawSymbol Source #

matches :: VSE -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: VSE -> VSESign Source #

add_symb_to_sign :: VSE -> VSESign -> Symbol -> Result VSESign Source #

signature_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

signatureDiff :: VSE -> VSESign -> VSESign -> Result VSESign Source #

intersection :: VSE -> VSESign -> VSESign -> Result VSESign Source #

final_union :: VSE -> VSESign -> VSESign -> Result VSESign Source #

morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor Source #

is_subsig :: VSE -> VSESign -> VSESign -> Bool Source #

subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor Source #

generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor Source #

induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor Source #

induced_from_to_morphism :: VSE -> EndoMap RawSymbol -> ExtSign VSESign Symbol -> ExtSign VSESign Symbol -> Result VSEMor Source #

is_transportable :: VSE -> VSEMor -> Bool Source #

is_injective :: VSE -> VSEMor -> Bool Source #

theory_to_taxonomy :: VSE -> TaxoGraphKind -> MMiSSOntology -> VSESign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: VSE -> String -> Bool -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (VSESign, [Named Sentence], VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: VSE -> VSESign -> VSESign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (VSESign, VSESign, VSESign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: VSE -> [IRI] -> (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence]) Source #

Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: VSE -> Maybe (VSEBasicSpec -> AParser st Sentence) Source #

stability :: VSE -> Stability Source #

data_logic :: VSE -> Maybe AnyLogic Source #

top_sublogic :: VSE -> () Source #

all_sublogics :: VSE -> [()] Source #

bottomSublogic :: VSE -> Maybe () Source #

sublogicDimensions :: VSE -> [[()]] Source #

parseSublogic :: VSE -> String -> Maybe () Source #

proj_sublogic_epsilon :: VSE -> () -> VSESign -> VSEMor Source #

provers :: VSE -> [Prover VSESign Sentence VSEMor () ()] Source #

default_prover :: VSE -> String Source #

cons_checkers :: VSE -> [ConsChecker VSESign Sentence () VSEMor ()] Source #

conservativityCheck :: VSE -> [ConservativityChecker VSESign Sentence VSEMor] Source #

empty_proof_tree :: VSE -> () Source #

syntaxTable :: VSE -> VSESign -> Maybe SyntaxTable Source #

omdoc_metatheory :: VSE -> Maybe OMCD Source #

export_symToOmdoc :: VSE -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: VSE -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: VSE -> SigMap Symbol -> VSESign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: VSE -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: VSE -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [[OmdADT]] -> Result (VSESign, [Named Sentence]) Source #

addOmdocToTheory :: VSE -> SigMapI Symbol -> (VSESign, [Named Sentence]) -> [TCElement] -> Result (VSESign, [Named Sentence]) Source #

Comorphism CASL2VSE CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 
Comorphism CASL2VSERefine CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source # 

Pretty instances

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

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