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

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

Instances details
Eq Paramkind Source # 
Instance details

Defined in VSE.As

Methods

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

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

Data Paramkind Source # 
Instance details

Defined in VSE.As

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 :: forall r r'. (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 # 
Instance details

Defined in VSE.As

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

Defined in VSE.As

Methods

showsPrec :: Int -> Paramkind -> ShowS

show :: Paramkind -> String

showList :: [Paramkind] -> ShowS

Generic Paramkind 
Instance details

Defined in VSE.ATC_VSE

Associated Types

type Rep Paramkind :: Type -> Type

Methods

from :: Paramkind -> Rep Paramkind x

to :: Rep Paramkind x -> Paramkind

FromJSON Paramkind 
Instance details

Defined in VSE.ATC_VSE

Methods

parseJSON :: Value -> Parser Paramkind

parseJSONList :: Value -> Parser [Paramkind]

ToJSON Paramkind 
Instance details

Defined in VSE.ATC_VSE

Methods

toJSON :: Paramkind -> Value

toEncoding :: Paramkind -> Encoding

toJSONList :: [Paramkind] -> Value

toEncodingList :: [Paramkind] -> Encoding

ShATermConvertible Paramkind 
Instance details

Defined in VSE.ATC_VSE

Methods

toShATermAux :: ATermTable -> Paramkind -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Paramkind] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Paramkind)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Paramkind])

type Rep Paramkind 
Instance details

Defined in VSE.ATC_VSE

type Rep Paramkind = D1 ('MetaData "Paramkind" "VSE.As" "main" 'False) (C1 ('MetaCons "In" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Out" 'PrefixI 'False) (U1 :: Type -> Type))

data Procparam Source #

a procedure parameter

Constructors

Procparam Paramkind SORT 

Instances

Instances details
Eq Procparam Source # 
Instance details

Defined in VSE.As

Methods

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

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

Data Procparam Source # 
Instance details

Defined in VSE.As

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 :: forall r r'. (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 # 
Instance details

Defined in VSE.As

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

Defined in VSE.As

Methods

showsPrec :: Int -> Procparam -> ShowS

show :: Procparam -> String

showList :: [Procparam] -> ShowS

Generic Procparam 
Instance details

Defined in VSE.ATC_VSE

Associated Types

type Rep Procparam :: Type -> Type

Methods

from :: Procparam -> Rep Procparam x

to :: Rep Procparam x -> Procparam

FromJSON Procparam 
Instance details

Defined in VSE.ATC_VSE

Methods

parseJSON :: Value -> Parser Procparam

parseJSONList :: Value -> Parser [Procparam]

ToJSON Procparam 
Instance details

Defined in VSE.ATC_VSE

Methods

toJSON :: Procparam -> Value

toEncoding :: Procparam -> Encoding

toJSONList :: [Procparam] -> Value

toEncodingList :: [Procparam] -> Encoding

ShATermConvertible Procparam 
Instance details

Defined in VSE.ATC_VSE

Methods

toShATermAux :: ATermTable -> Procparam -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Procparam] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Procparam)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Procparam])

Pretty Procparam Source # 
Instance details

Defined in VSE.As

type Rep Procparam 
Instance details

Defined in VSE.ATC_VSE

type Rep Procparam = D1 ('MetaData "Procparam" "VSE.As" "main" 'False) (C1 ('MetaCons "Procparam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Paramkind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT)))

data Profile Source #

procedure or function declaration

Constructors

Profile [Procparam] (Maybe SORT) 

Instances

Instances details
Eq Profile Source # 
Instance details

Defined in VSE.As

Methods

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

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

Data Profile Source # 
Instance details

Defined in VSE.As

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 :: forall r r'. (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 # 
Instance details

Defined in VSE.As

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

Defined in VSE.As

Methods

showsPrec :: Int -> Profile -> ShowS

show :: Profile -> String

showList :: [Profile] -> ShowS

Generic Profile 
Instance details

Defined in VSE.ATC_VSE

Associated Types

type Rep Profile :: Type -> Type

Methods

from :: Profile -> Rep Profile x

to :: Rep Profile x -> Profile

FromJSON Profile 
Instance details

Defined in VSE.ATC_VSE

Methods

parseJSON :: Value -> Parser Profile

parseJSONList :: Value -> Parser [Profile]

ToJSON Profile 
Instance details

Defined in VSE.ATC_VSE

Methods

toJSON :: Profile -> Value

toEncoding :: Profile -> Encoding

toJSONList :: [Profile] -> Value

toEncodingList :: [Profile] -> Encoding

ShATermConvertible Profile 
Instance details

Defined in VSE.ATC_VSE

Methods

toShATermAux :: ATermTable -> Profile -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Profile] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Profile)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Profile])

Pretty Profile Source # 
Instance details

Defined in VSE.As

type Rep Profile 
Instance details

Defined in VSE.ATC_VSE

type Rep Profile = D1 ('MetaData "Profile" "VSE.As" "main" 'False) (C1 ('MetaCons "Profile" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Procparam]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe SORT))))

data Sigentry Source #

further VSE signature entries

Constructors

Procedure Id Profile Range 

Instances

Instances details
Eq Sigentry Source # 
Instance details

Defined in VSE.As

Methods

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

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

Data Sigentry Source # 
Instance details

Defined in VSE.As

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 :: forall r r'. (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 # 
Instance details

Defined in VSE.As

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

Defined in VSE.As

Methods

showsPrec :: Int -> Sigentry -> ShowS

show :: Sigentry -> String

showList :: [Sigentry] -> ShowS

Generic Sigentry 
Instance details

Defined in VSE.ATC_VSE

Associated Types

type Rep Sigentry :: Type -> Type

Methods

from :: Sigentry -> Rep Sigentry x

to :: Rep Sigentry x -> Sigentry

FromJSON Sigentry 
Instance details

Defined in VSE.ATC_VSE

Methods

parseJSON :: Value -> Parser Sigentry

parseJSONList :: Value -> Parser [Sigentry]

ToJSON Sigentry 
Instance details

Defined in VSE.ATC_VSE

Methods

toJSON :: Sigentry -> Value

toEncoding :: Sigentry -> Encoding

toJSONList :: [Sigentry] -> Value

toEncodingList :: [Sigentry] -> Encoding

ShATermConvertible Sigentry 
Instance details

Defined in VSE.ATC_VSE

Methods

toShATermAux :: ATermTable -> Sigentry -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Sigentry] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Sigentry)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sigentry])

Pretty Sigentry Source # 
Instance details

Defined in VSE.As

type Rep Sigentry 
Instance details

Defined in VSE.ATC_VSE

type Rep Sigentry = D1 ('MetaData "Sigentry" "VSE.As" "main" 'False) (C1 ('MetaCons "Procedure" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Profile) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data Procdecls Source #

Instances

Instances details
Eq Procdecls Source # 
Instance details

Defined in VSE.As

Methods

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

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

Data Procdecls Source # 
Instance details

Defined in VSE.As

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 :: forall r r'. (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 # 
Instance details

Defined in VSE.As

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

Defined in VSE.As

Methods

showsPrec :: Int -> Procdecls -> ShowS

show :: Procdecls -> String

showList :: [Procdecls] -> ShowS

Generic Procdecls 
Instance details

Defined in VSE.ATC_VSE

Associated Types

type Rep Procdecls :: Type -> Type

Methods

from :: Procdecls -> Rep Procdecls x

to :: Rep Procdecls x -> Procdecls

GetRange Procdecls Source # 
Instance details

Defined in VSE.As

FromJSON Procdecls 
Instance details

Defined in VSE.ATC_VSE

Methods

parseJSON :: Value -> Parser Procdecls

parseJSONList :: Value -> Parser [Procdecls]

ToJSON Procdecls 
Instance details

Defined in VSE.ATC_VSE

Methods

toJSON :: Procdecls -> Value

toEncoding :: Procdecls -> Encoding

toJSONList :: [Procdecls] -> Value

toEncodingList :: [Procdecls] -> Encoding

ShATermConvertible Procdecls 
Instance details

Defined in VSE.ATC_VSE

Methods

toShATermAux :: ATermTable -> Procdecls -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Procdecls] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Procdecls)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Procdecls])

Pretty Procdecls Source # 
Instance details

Defined in VSE.As

AParsable Procdecls Source # 
Instance details

Defined in VSE.Parse

Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in VSE.Logic_VSE

StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 
Instance details

Defined in VSE.Logic_VSE

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

Defined in VSE.Logic_VSE

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 #

sublogicOfTheo :: VSE -> (VSESign, [Sentence]) -> () 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 # 
Instance details

Defined in Comorphisms.CASL2VSERefine

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

Defined in Comorphisms.CASL2VSEImport

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

Defined in Comorphisms.CASL2VSE

type Rep Procdecls 
Instance details

Defined in VSE.ATC_VSE

type Rep Procdecls = D1 ('MetaData "Procdecls" "VSE.As" "main" 'False) (C1 ('MetaCons "Procdecls" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Annoted Sigentry]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

data Ranged a Source #

wrapper for positions

Constructors

Ranged 

Fields

Instances

Instances details
TermExtension Dlformula Source # 
Instance details

Defined in VSE.Ana

TermParser Dlformula Source # 
Instance details

Defined in VSE.Parse

Methods

termParser :: Bool -> AParser st Dlformula Source #

Sentences VSE Sentence VSESign VSEMor Symbol Source # 
Instance details

Defined in VSE.Logic_VSE

Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in VSE.Logic_VSE

StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 
Instance details

Defined in VSE.Logic_VSE

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

Defined in VSE.Logic_VSE

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 #

sublogicOfTheo :: VSE -> (VSESign, [Sentence]) -> () 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 # 
Instance details

Defined in Comorphisms.CASL2VSERefine

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

Defined in Comorphisms.CASL2VSEImport

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

Defined in Comorphisms.CASL2VSE

Eq a => Eq (Ranged a) Source # 
Instance details

Defined in VSE.As

Methods

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

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

Data a => Data (Ranged a) Source # 
Instance details

Defined in VSE.As

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 :: forall r r'. (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 # 
Instance details

Defined in VSE.As

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

Defined in VSE.As

Methods

showsPrec :: Int -> Ranged a -> ShowS

show :: Ranged a -> String

showList :: [Ranged a] -> ShowS

Generic (Ranged a) 
Instance details

Defined in VSE.ATC_VSE

Associated Types

type Rep (Ranged a) :: Type -> Type

Methods

from :: Ranged a -> Rep (Ranged a) x

to :: Rep (Ranged a) x -> Ranged a

GetRange (Ranged a) Source # 
Instance details

Defined in VSE.As

FromJSON a => FromJSON (Ranged a) 
Instance details

Defined in VSE.ATC_VSE

Methods

parseJSON :: Value -> Parser (Ranged a)

parseJSONList :: Value -> Parser [Ranged a]

ToJSON a => ToJSON (Ranged a) 
Instance details

Defined in VSE.ATC_VSE

Methods

toJSON :: Ranged a -> Value

toEncoding :: Ranged a -> Encoding

toJSONList :: [Ranged a] -> Value

toEncodingList :: [Ranged a] -> Encoding

ShATermConvertible a => ShATermConvertible (Ranged a) 
Instance details

Defined in VSE.ATC_VSE

Methods

toShATermAux :: ATermTable -> Ranged a -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Ranged a] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Ranged a)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Ranged a])

Pretty a => Pretty (Ranged a) Source # 
Instance details

Defined in VSE.As

Methods

pretty :: Ranged a -> Doc Source #

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

FormExtension a => FormExtension (Ranged a) Source # 
Instance details

Defined in VSE.As

Methods

isQuantifierLike :: Ranged a -> Bool Source #

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

type Rep (Ranged a) 
Instance details

Defined in VSE.ATC_VSE

type Rep (Ranged a) = D1 ('MetaData "Ranged" "VSE.As" "main" 'False) (C1 ('MetaCons "Ranged" 'PrefixI 'True) (S1 ('MetaSel ('Just "unRanged") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Just "range") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))

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

Instances details
Eq PlainProgram Source # 
Instance details

Defined in VSE.As

Methods

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

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

Data PlainProgram Source # 
Instance details

Defined in VSE.As

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 :: forall r r'. (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 # 
Instance details

Defined in VSE.As

Show PlainProgram Source # 
Instance details

Defined in VSE.As

Methods

showsPrec :: Int -> PlainProgram -> ShowS

show :: PlainProgram -> String

showList :: [PlainProgram] -> ShowS

Generic PlainProgram 
Instance details

Defined in VSE.ATC_VSE

Associated Types

type Rep PlainProgram :: Type -> Type

FromJSON PlainProgram 
Instance details

Defined in VSE.ATC_VSE

Methods

parseJSON :: Value -> Parser PlainProgram

parseJSONList :: Value -> Parser [PlainProgram]

ToJSON PlainProgram 
Instance details

Defined in VSE.ATC_VSE

Methods

toJSON :: PlainProgram -> Value

toEncoding :: PlainProgram -> Encoding

toJSONList :: [PlainProgram] -> Value

toEncodingList :: [PlainProgram] -> Encoding

ShATermConvertible PlainProgram 
Instance details

Defined in VSE.ATC_VSE

Methods

toShATermAux :: ATermTable -> PlainProgram -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [PlainProgram] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, PlainProgram)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [PlainProgram])

Pretty PlainProgram Source # 
Instance details

Defined in VSE.As

type Rep PlainProgram 
Instance details

Defined in VSE.ATC_VSE

type Rep PlainProgram = D1 ('MetaData "PlainProgram" "VSE.As" "main" 'False) (((C1 ('MetaCons "Abort" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Skip" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Assign" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VAR) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TERM ()))) :+: C1 ('MetaCons "Call" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA ()))))) :+: ((C1 ('MetaCons "Return" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TERM ()))) :+: C1 ('MetaCons "Block" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VAR_DECL]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Program))) :+: (C1 ('MetaCons "Seq" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Program) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Program)) :+: (C1 ('MetaCons "If" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA ())) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Program) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Program))) :+: C1 ('MetaCons "While" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FORMULA ())) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Program))))))

data VarDecl Source #

alternative variable declaration

Constructors

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

Instances

Instances details
Data VarDecl Source # 
Instance details

Defined in VSE.As

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 :: forall r r'. (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 # 
Instance details

Defined in VSE.As

Methods

showsPrec :: Int -> VarDecl -> ShowS

show :: VarDecl -> String

showList :: [VarDecl] -> ShowS

Generic VarDecl 
Instance details

Defined in VSE.ATC_VSE

Associated Types

type Rep VarDecl :: Type -> Type

Methods

from :: VarDecl -> Rep VarDecl x

to :: Rep VarDecl x -> VarDecl

FromJSON VarDecl 
Instance details

Defined in VSE.ATC_VSE

Methods

parseJSON :: Value -> Parser VarDecl

parseJSONList :: Value -> Parser [VarDecl]

ToJSON VarDecl 
Instance details

Defined in VSE.ATC_VSE

Methods

toJSON :: VarDecl -> Value

toEncoding :: VarDecl -> Encoding

toJSONList :: [VarDecl] -> Value

toEncodingList :: [VarDecl] -> Encoding

ShATermConvertible VarDecl 
Instance details

Defined in VSE.ATC_VSE

Methods

toShATermAux :: ATermTable -> VarDecl -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [VarDecl] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, VarDecl)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [VarDecl])

Pretty VarDecl Source # 
Instance details

Defined in VSE.As

type Rep VarDecl 
Instance details

Defined in VSE.ATC_VSE

type Rep VarDecl = D1 ('MetaData "VarDecl" "VSE.As" "main" 'False) (C1 ('MetaCons "VarDecl" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VAR) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SORT)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (TERM ()))) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range))))

data VSEforms Source #

extend CASL formulas by box or diamond formulas and defprocs

Instances

Instances details
Eq VSEforms Source # 
Instance details

Defined in VSE.As

Methods

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

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

Data VSEforms Source # 
Instance details

Defined in VSE.As

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 :: forall r r'. (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 # 
Instance details

Defined in VSE.As

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

Defined in VSE.As

Methods

showsPrec :: Int -> VSEforms -> ShowS

show :: VSEforms -> String

showList :: [VSEforms] -> ShowS

Generic VSEforms 
Instance details

Defined in VSE.ATC_VSE

Associated Types

type Rep VSEforms :: Type -> Type

Methods

from :: VSEforms -> Rep VSEforms x

to :: Rep VSEforms x -> VSEforms

GetRange VSEforms Source # 
Instance details

Defined in VSE.As

FromJSON VSEforms 
Instance details

Defined in VSE.ATC_VSE

Methods

parseJSON :: Value -> Parser VSEforms

parseJSONList :: Value -> Parser [VSEforms]

ToJSON VSEforms 
Instance details

Defined in VSE.ATC_VSE

Methods

toJSON :: VSEforms -> Value

toEncoding :: VSEforms -> Encoding

toJSONList :: [VSEforms] -> Value

toEncodingList :: [VSEforms] -> Encoding

ShATermConvertible VSEforms 
Instance details

Defined in VSE.ATC_VSE

Methods

toShATermAux :: ATermTable -> VSEforms -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [VSEforms] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, VSEforms)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [VSEforms])

Pretty VSEforms Source # 
Instance details

Defined in VSE.As

FormExtension VSEforms Source # 
Instance details

Defined in VSE.As

TermExtension Dlformula Source # 
Instance details

Defined in VSE.Ana

TermParser Dlformula Source # 
Instance details

Defined in VSE.Parse

Methods

termParser :: Bool -> AParser st Dlformula Source #

Sentences VSE Sentence VSESign VSEMor Symbol Source # 
Instance details

Defined in VSE.Logic_VSE

Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
Instance details

Defined in VSE.Logic_VSE

StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 
Instance details

Defined in VSE.Logic_VSE

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

Defined in VSE.Logic_VSE

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 #

sublogicOfTheo :: VSE -> (VSESign, [Sentence]) -> () 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 # 
Instance details

Defined in Comorphisms.CASL2VSERefine

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

Defined in Comorphisms.CASL2VSEImport

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

Defined in Comorphisms.CASL2VSE

type Rep VSEforms 
Instance details

Defined in VSE.ATC_VSE

type Rep VSEforms = D1 ('MetaData "VSEforms" "VSE.As" "main" 'False) (C1 ('MetaCons "Dlformula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BoxOrDiamond) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Program) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sentence))) :+: (C1 ('MetaCons "Defprocs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Defproc])) :+: C1 ('MetaCons "RestrictedConstraint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Constraint]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map SORT Id)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

data BoxOrDiamond Source #

box or diamond indicator

Constructors

Box 
Diamond 

Instances

Instances details
Eq BoxOrDiamond Source # 
Instance details

Defined in VSE.As

Methods

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

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

Data BoxOrDiamond Source # 
Instance details

Defined in VSE.As

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 :: forall r r'. (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 # 
Instance details

Defined in VSE.As

Show BoxOrDiamond Source # 
Instance details

Defined in VSE.As

Methods

showsPrec :: Int -> BoxOrDiamond -> ShowS

show :: BoxOrDiamond -> String

showList :: [BoxOrDiamond] -> ShowS

Generic BoxOrDiamond 
Instance details

Defined in VSE.ATC_VSE

Associated Types

type Rep BoxOrDiamond :: Type -> Type

FromJSON BoxOrDiamond 
Instance details

Defined in VSE.ATC_VSE

Methods

parseJSON :: Value -> Parser BoxOrDiamond

parseJSONList :: Value -> Parser [BoxOrDiamond]

ToJSON BoxOrDiamond 
Instance details

Defined in VSE.ATC_VSE

Methods

toJSON :: BoxOrDiamond -> Value

toEncoding :: BoxOrDiamond -> Encoding

toJSONList :: [BoxOrDiamond] -> Value

toEncodingList :: [BoxOrDiamond] -> Encoding

ShATermConvertible BoxOrDiamond 
Instance details

Defined in VSE.ATC_VSE

Methods

toShATermAux :: ATermTable -> BoxOrDiamond -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [BoxOrDiamond] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, BoxOrDiamond)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [BoxOrDiamond])

type Rep BoxOrDiamond 
Instance details

Defined in VSE.ATC_VSE

type Rep BoxOrDiamond = D1 ('MetaData "BoxOrDiamond" "VSE.As" "main" 'False) (C1 ('MetaCons "Box" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Diamond" 'PrefixI 'False) (U1 :: Type -> Type))

data ProcKind Source #

Constructors

Proc 
Func 

Instances

Instances details
Eq ProcKind Source # 
Instance details

Defined in VSE.As

Methods

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

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

Data ProcKind Source # 
Instance details

Defined in VSE.As

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 :: forall r r'. (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 # 
Instance details

Defined in VSE.As

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

Defined in VSE.As

Methods

showsPrec :: Int -> ProcKind -> ShowS

show :: ProcKind -> String

showList :: [ProcKind] -> ShowS

Generic ProcKind 
Instance details

Defined in VSE.ATC_VSE

Associated Types

type Rep ProcKind :: Type -> Type

Methods

from :: ProcKind -> Rep ProcKind x

to :: Rep ProcKind x -> ProcKind

FromJSON ProcKind 
Instance details

Defined in VSE.ATC_VSE

Methods

parseJSON :: Value -> Parser ProcKind

parseJSONList :: Value -> Parser [ProcKind]

ToJSON ProcKind 
Instance details

Defined in VSE.ATC_VSE

Methods

toJSON :: ProcKind -> Value

toEncoding :: ProcKind -> Encoding

toJSONList :: [ProcKind] -> Value

toEncodingList :: [ProcKind] -> Encoding

ShATermConvertible ProcKind 
Instance details

Defined in VSE.ATC_VSE

Methods

toShATermAux :: ATermTable -> ProcKind -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [ProcKind] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, ProcKind)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProcKind])

type Rep ProcKind 
Instance details

Defined in VSE.ATC_VSE

type Rep ProcKind = D1 ('MetaData "ProcKind" "VSE.As" "main" 'False) (C1 ('MetaCons "Proc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Func" 'PrefixI 'False) (U1 :: Type -> Type))

data Defproc Source #

procedure definitions as basic items becoming sentences

Instances

Instances details
Eq Defproc Source # 
Instance details

Defined in VSE.As

Methods

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

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

Data Defproc Source # 
Instance details

Defined in VSE.As

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 :: forall r r'. (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 # 
Instance details

Defined in VSE.As

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

Defined in VSE.As

Methods

showsPrec :: Int -> Defproc -> ShowS

show :: Defproc -> String

showList :: [Defproc] -> ShowS

Generic Defproc 
Instance details

Defined in VSE.ATC_VSE

Associated Types

type Rep Defproc :: Type -> Type

Methods

from :: Defproc -> Rep Defproc x

to :: Rep Defproc x -> Defproc

FromJSON Defproc 
Instance details

Defined in VSE.ATC_VSE

Methods

parseJSON :: Value -> Parser Defproc

parseJSONList :: Value -> Parser [Defproc]

ToJSON Defproc 
Instance details

Defined in VSE.ATC_VSE

Methods

toJSON :: Defproc -> Value

toEncoding :: Defproc -> Encoding

toJSONList :: [Defproc] -> Value

toEncodingList :: [Defproc] -> Encoding

ShATermConvertible Defproc 
Instance details

Defined in VSE.ATC_VSE

Methods

toShATermAux :: ATermTable -> Defproc -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Defproc] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Defproc)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Defproc])

Pretty Defproc Source # 
Instance details

Defined in VSE.As

type Rep Defproc 
Instance details

Defined in VSE.ATC_VSE

type Rep Defproc = D1 ('MetaData "Defproc" "VSE.As" "main" 'False) (C1 ('MetaCons "Defproc" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProcKind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VAR]) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Program) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)))))

data Procs Source #

Constructors

Procs 

Fields

Instances

Instances details
Eq Procs Source # 
Instance details

Defined in VSE.As

Methods

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

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

Data Procs Source # 
Instance details

Defined in VSE.As

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 :: forall r r'. (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 # 
Instance details

Defined in VSE.As

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

Defined in VSE.As

Methods

showsPrec :: Int -> Procs -> ShowS

show :: Procs -> String

showList :: [Procs] -> ShowS

Generic Procs 
Instance details

Defined in VSE.ATC_VSE

Associated Types

type Rep Procs :: Type -> Type

Methods

from :: Procs -> Rep Procs x

to :: Rep Procs x -> Procs

FromJSON Procs 
Instance details

Defined in VSE.ATC_VSE

Methods

parseJSON :: Value -> Parser Procs

parseJSONList :: Value -> Parser [Procs]

ToJSON Procs 
Instance details

Defined in VSE.ATC_VSE

Methods

toJSON :: Procs -> Value

toEncoding :: Procs -> Encoding

toJSONList :: [Procs] -> Value

toEncodingList :: [Procs] -> Encoding

ShATermConvertible Procs 
Instance details

Defined in VSE.ATC_VSE

Methods

toShATermAux :: ATermTable -> Procs -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Procs] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Procs)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Procs])

Pretty Procs Source # 
Instance details

Defined in VSE.As

SignExtension Procs Source # 
Instance details

Defined in VSE.Logic_VSE

Methods

isSubSignExtension :: Procs -> Procs -> Bool Source #

Sentences VSE Sentence VSESign VSEMor Symbol Source # 
Instance details

Defined in VSE.Logic_VSE

StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source # 
Instance details

Defined in VSE.Logic_VSE

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

Defined in VSE.Logic_VSE

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 #

sublogicOfTheo :: VSE -> (VSESign, [Sentence]) -> () 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 # 
Instance details

Defined in Comorphisms.CASL2VSERefine

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

Defined in Comorphisms.CASL2VSEImport

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

Defined in Comorphisms.CASL2VSE

type Rep Procs 
Instance details

Defined in VSE.ATC_VSE

type Rep Procs = D1 ('MetaData "Procs" "VSE.As" "main" 'False) (C1 ('MetaCons "Procs" 'PrefixI 'True) (S1 ('MetaSel ('Just "procsMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Id Profile))))

Pretty instances

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

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