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

VSE.As

Contents

Pretty instances

Description

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

Synopsis

data Paramkind
- = In
- | Out
data Procparam = Procparam Paramkind SORT
data Profile = Profile [Procparam] (Maybe SORT)
data Sigentry = Procedure Id Profile Range
data Procdecls = Procdecls [Annoted Sigentry] Range
data Ranged a = Ranged {
- unRanged :: a
- range :: Range
}
mkRanged :: a -> Ranged a
type Program = Ranged PlainProgram
data PlainProgram
- = Abort
- | Skip
- | Assign VAR (TERM ())
- | Call (FORMULA ())
- | Return (TERM ())
- | Block [VAR_DECL] Program
- | Seq Program Program
- | If (FORMULA ()) Program Program
- | While (FORMULA ()) Program
data VarDecl = VarDecl VAR SORT (Maybe (TERM ())) Range
toVarDecl :: [VAR_DECL] -> [VarDecl]
addInits :: [VarDecl] -> Program -> ([VarDecl], Program)
data VSEforms
- = Dlformula BoxOrDiamond Program Sentence
- | Defprocs [Defproc]
- | RestrictedConstraint [Constraint] (Map SORT Id) Bool
type Dlformula = Ranged VSEforms
type Sentence = FORMULA Dlformula
data BoxOrDiamond
- = Box
- | Diamond
data ProcKind
- = Proc
- | Func
data Defproc = Defproc ProcKind Id [VAR] Program Range
data Procs = Procs {
- procsMap :: Map Id Profile
}
emptyProcs :: Procs
unionProcs :: Procs -> Procs -> Result Procs
interProcs :: Procs -> Procs -> Result Procs
diffProcs :: Procs -> Procs -> Procs
isSubProcsMap :: Procs -> Procs -> Bool
block :: Doc -> Doc
prettyProcKind :: ProcKind -> Doc
assign :: Doc
genSortName :: String -> SORT -> Id
gnUniformName :: SORT -> Id
gnRestrName :: SORT -> Id
gnEqName :: SORT -> Id
genVars :: [SORT] -> [(Token, SORT)]
xVar :: Token
yVar :: Token
printRestrTypedecl :: Map SORT Id -> DATATYPE_DECL -> Doc
prettyProcdefs :: [Defproc] -> Doc

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 Methods pretty :: Procparam -> Doc Source # pretties :: [Procparam] -> Doc Source #
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 Methods pretty :: Profile -> Doc Source # pretties :: [Profile] -> Doc Source #
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 Methods pretty :: Sigentry -> Doc Source # pretties :: [Sigentry] -> Doc Source #
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 #

Constructors

Procdecls [Annoted Sigentry] Range

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 Methods getRange :: Procdecls -> Range Source # rangeSpan :: Procdecls -> [Pos] Source #
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 Methods pretty :: Procdecls -> Doc Source # pretties :: [Procdecls] -> Doc Source #
AParsable Procdecls Source #
Instance details Defined in VSE.Parse Methods aparser :: AParser st Procdecls Source #
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in VSE.Logic_VSE Methods parsersAndPrinters :: VSE -> Map String (PrefixMap -> AParser st VSEBasicSpec, VSEBasicSpec -> Doc) Source # parse_basic_spec :: VSE -> Maybe (PrefixMap -> AParser st VSEBasicSpec) Source # parseSingleSymbItem :: VSE -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: VSE -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: VSE -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: VSE -> VSEBasicSpec -> Item Source # symb_items_name :: VSE -> SYMB_ITEMS -> [String] Source #
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source #
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 Methods sourceLogic :: CASL2VSERefine -> CASL Source # sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source # minSourceTheory :: CASL2VSERefine -> Maybe (LibName, String) Source # targetLogic :: CASL2VSERefine -> VSE Source # mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSERefine -> Bool Source # has_model_expansion :: CASL2VSERefine -> Bool Source # is_weakly_amalgamable :: CASL2VSERefine -> Bool Source # constituents :: CASL2VSERefine -> [String] Source # isInclusionComorphism :: CASL2VSERefine -> Bool Source # rps :: CASL2VSERefine -> Bool Source # eps :: CASL2VSERefine -> Bool Source # isGTC :: CASL2VSERefine -> Bool Source #
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSEImport Methods sourceLogic :: CASL2VSEImport -> CASL Source # sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source # minSourceTheory :: CASL2VSEImport -> Maybe (LibName, String) Source # targetLogic :: CASL2VSEImport -> VSE Source # mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSEImport -> Bool Source # has_model_expansion :: CASL2VSEImport -> Bool Source # is_weakly_amalgamable :: CASL2VSEImport -> Bool Source # constituents :: CASL2VSEImport -> [String] Source # isInclusionComorphism :: CASL2VSEImport -> Bool Source # rps :: CASL2VSEImport -> Bool Source # eps :: CASL2VSEImport -> Bool Source # isGTC :: CASL2VSEImport -> Bool 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 #
Instance details Defined in Comorphisms.CASL2VSE Methods sourceLogic :: CASL2VSE -> CASL Source # sourceSublogic :: CASL2VSE -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source # minSourceTheory :: CASL2VSE -> Maybe (LibName, String) Source # targetLogic :: CASL2VSE -> VSE Source # mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSE -> Bool Source # has_model_expansion :: CASL2VSE -> Bool Source # is_weakly_amalgamable :: CASL2VSE -> Bool Source # constituents :: CASL2VSE -> [String] Source # isInclusionComorphism :: CASL2VSE -> Bool Source # rps :: CASL2VSE -> Bool Source # eps :: CASL2VSE -> Bool Source # isGTC :: CASL2VSE -> Bool Source #
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 unRanged :: a range :: Range

Instances

Instances details

TermExtension Dlformula Source #
Instance details Defined in VSE.Ana Methods freeVarsOfExt :: Sign Dlformula e -> Dlformula -> VarSet Source # optTermSort :: Dlformula -> Maybe SORT Source # sortOfTerm :: Dlformula -> SORT Source # termToFormula :: TERM Dlformula -> Result (FORMULA Dlformula) Source #
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 Methods map_sen :: VSE -> VSEMor -> Sentence -> Result Sentence Source # simplify_sen :: VSE -> VSESign -> Sentence -> Sentence Source # negation :: VSE -> Sentence -> Maybe Sentence Source # print_sign :: VSE -> VSESign -> Doc Source # print_named :: VSE -> Named Sentence -> Doc Source # sym_of :: VSE -> VSESign -> [Set Symbol] Source # mostSymsOf :: VSE -> VSESign -> [Symbol] Source # symmap_of :: VSE -> VSEMor -> EndoMap Symbol Source # sym_name :: VSE -> Symbol -> Id Source # sym_label :: VSE -> Symbol -> Maybe String Source # fullSymName :: VSE -> Symbol -> String Source # symKind :: VSE -> Symbol -> String Source # symsOfSen :: VSE -> VSESign -> Sentence -> [Symbol] Source # pair_symbols :: VSE -> Symbol -> Symbol -> Result Symbol Source #
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in VSE.Logic_VSE Methods parsersAndPrinters :: VSE -> Map String (PrefixMap -> AParser st VSEBasicSpec, VSEBasicSpec -> Doc) Source # parse_basic_spec :: VSE -> Maybe (PrefixMap -> AParser st VSEBasicSpec) Source # parseSingleSymbItem :: VSE -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: VSE -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: VSE -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: VSE -> VSEBasicSpec -> Item Source # symb_items_name :: VSE -> SYMB_ITEMS -> [String] Source #
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source #
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 Methods sourceLogic :: CASL2VSERefine -> CASL Source # sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source # minSourceTheory :: CASL2VSERefine -> Maybe (LibName, String) Source # targetLogic :: CASL2VSERefine -> VSE Source # mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSERefine -> Bool Source # has_model_expansion :: CASL2VSERefine -> Bool Source # is_weakly_amalgamable :: CASL2VSERefine -> Bool Source # constituents :: CASL2VSERefine -> [String] Source # isInclusionComorphism :: CASL2VSERefine -> Bool Source # rps :: CASL2VSERefine -> Bool Source # eps :: CASL2VSERefine -> Bool Source # isGTC :: CASL2VSERefine -> Bool Source #
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSEImport Methods sourceLogic :: CASL2VSEImport -> CASL Source # sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source # minSourceTheory :: CASL2VSEImport -> Maybe (LibName, String) Source # targetLogic :: CASL2VSEImport -> VSE Source # mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSEImport -> Bool Source # has_model_expansion :: CASL2VSEImport -> Bool Source # is_weakly_amalgamable :: CASL2VSEImport -> Bool Source # constituents :: CASL2VSEImport -> [String] Source # isInclusionComorphism :: CASL2VSEImport -> Bool Source # rps :: CASL2VSEImport -> Bool Source # eps :: CASL2VSEImport -> Bool Source # isGTC :: CASL2VSEImport -> Bool 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 #
Instance details Defined in Comorphisms.CASL2VSE Methods sourceLogic :: CASL2VSE -> CASL Source # sourceSublogic :: CASL2VSE -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source # minSourceTheory :: CASL2VSE -> Maybe (LibName, String) Source # targetLogic :: CASL2VSE -> VSE Source # mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSE -> Bool Source # has_model_expansion :: CASL2VSE -> Bool Source # is_weakly_amalgamable :: CASL2VSE -> Bool Source # constituents :: CASL2VSE -> [String] Source # isInclusionComorphism :: CASL2VSE -> Bool Source # rps :: CASL2VSE -> Bool Source # eps :: CASL2VSE -> Bool Source # isGTC :: CASL2VSE -> Bool Source #
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 Methods getRange :: Ranged a -> Range Source # rangeSpan :: Ranged a -> [Pos] Source #
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 Methods compare :: PlainProgram -> PlainProgram -> Ordering (<) :: PlainProgram -> PlainProgram -> Bool (<=) :: PlainProgram -> PlainProgram -> Bool (>) :: PlainProgram -> PlainProgram -> Bool (>=) :: PlainProgram -> PlainProgram -> Bool max :: PlainProgram -> PlainProgram -> PlainProgram min :: PlainProgram -> PlainProgram -> PlainProgram
Show PlainProgram Source #
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 Methods from :: PlainProgram -> Rep PlainProgram x to :: Rep PlainProgram x -> PlainProgram
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 Methods pretty :: PlainProgram -> Doc Source # pretties :: [PlainProgram] -> Doc Source #
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 Methods pretty :: VarDecl -> Doc Source # pretties :: [VarDecl] -> Doc Source #
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))))

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

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

data VSEforms Source #

extend CASL formulas by box or diamond formulas and defprocs

Constructors

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

Instances

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 Methods getRange :: VSEforms -> Range Source # rangeSpan :: VSEforms -> [Pos] Source #
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 Methods pretty :: VSEforms -> Doc Source # pretties :: [VSEforms] -> Doc Source #
FormExtension VSEforms Source #
Instance details Defined in VSE.As Methods isQuantifierLike :: VSEforms -> Bool Source # prefixExt :: VSEforms -> Doc -> Doc Source #
TermExtension Dlformula Source #
Instance details Defined in VSE.Ana Methods freeVarsOfExt :: Sign Dlformula e -> Dlformula -> VarSet Source # optTermSort :: Dlformula -> Maybe SORT Source # sortOfTerm :: Dlformula -> SORT Source # termToFormula :: TERM Dlformula -> Result (FORMULA Dlformula) Source #
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 Methods map_sen :: VSE -> VSEMor -> Sentence -> Result Sentence Source # simplify_sen :: VSE -> VSESign -> Sentence -> Sentence Source # negation :: VSE -> Sentence -> Maybe Sentence Source # print_sign :: VSE -> VSESign -> Doc Source # print_named :: VSE -> Named Sentence -> Doc Source # sym_of :: VSE -> VSESign -> [Set Symbol] Source # mostSymsOf :: VSE -> VSESign -> [Symbol] Source # symmap_of :: VSE -> VSEMor -> EndoMap Symbol Source # sym_name :: VSE -> Symbol -> Id Source # sym_label :: VSE -> Symbol -> Maybe String Source # fullSymName :: VSE -> Symbol -> String Source # symKind :: VSE -> Symbol -> String Source # symsOfSen :: VSE -> VSESign -> Sentence -> [Symbol] Source # pair_symbols :: VSE -> Symbol -> Symbol -> Result Symbol Source #
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in VSE.Logic_VSE Methods parsersAndPrinters :: VSE -> Map String (PrefixMap -> AParser st VSEBasicSpec, VSEBasicSpec -> Doc) Source # parse_basic_spec :: VSE -> Maybe (PrefixMap -> AParser st VSEBasicSpec) Source # parseSingleSymbItem :: VSE -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: VSE -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: VSE -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: VSE -> VSEBasicSpec -> Item Source # symb_items_name :: VSE -> SYMB_ITEMS -> [String] Source #
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source #
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 Methods sourceLogic :: CASL2VSERefine -> CASL Source # sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source # minSourceTheory :: CASL2VSERefine -> Maybe (LibName, String) Source # targetLogic :: CASL2VSERefine -> VSE Source # mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSERefine -> Bool Source # has_model_expansion :: CASL2VSERefine -> Bool Source # is_weakly_amalgamable :: CASL2VSERefine -> Bool Source # constituents :: CASL2VSERefine -> [String] Source # isInclusionComorphism :: CASL2VSERefine -> Bool Source # rps :: CASL2VSERefine -> Bool Source # eps :: CASL2VSERefine -> Bool Source # isGTC :: CASL2VSERefine -> Bool Source #
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSEImport Methods sourceLogic :: CASL2VSEImport -> CASL Source # sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source # minSourceTheory :: CASL2VSEImport -> Maybe (LibName, String) Source # targetLogic :: CASL2VSEImport -> VSE Source # mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSEImport -> Bool Source # has_model_expansion :: CASL2VSEImport -> Bool Source # is_weakly_amalgamable :: CASL2VSEImport -> Bool Source # constituents :: CASL2VSEImport -> [String] Source # isInclusionComorphism :: CASL2VSEImport -> Bool Source # rps :: CASL2VSEImport -> Bool Source # eps :: CASL2VSEImport -> Bool Source # isGTC :: CASL2VSEImport -> Bool 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 #
Instance details Defined in Comorphisms.CASL2VSE Methods sourceLogic :: CASL2VSE -> CASL Source # sourceSublogic :: CASL2VSE -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source # minSourceTheory :: CASL2VSE -> Maybe (LibName, String) Source # targetLogic :: CASL2VSE -> VSE Source # mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSE -> Bool Source # has_model_expansion :: CASL2VSE -> Bool Source # is_weakly_amalgamable :: CASL2VSE -> Bool Source # constituents :: CASL2VSE -> [String] Source # isInclusionComorphism :: CASL2VSE -> Bool Source # rps :: CASL2VSE -> Bool Source # eps :: CASL2VSE -> Bool Source # isGTC :: CASL2VSE -> Bool Source #
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)))))

type Dlformula = Ranged VSEforms Source #

type Sentence = FORMULA Dlformula Source #

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 Methods compare :: BoxOrDiamond -> BoxOrDiamond -> Ordering (<) :: BoxOrDiamond -> BoxOrDiamond -> Bool (<=) :: BoxOrDiamond -> BoxOrDiamond -> Bool (>) :: BoxOrDiamond -> BoxOrDiamond -> Bool (>=) :: BoxOrDiamond -> BoxOrDiamond -> Bool max :: BoxOrDiamond -> BoxOrDiamond -> BoxOrDiamond min :: BoxOrDiamond -> BoxOrDiamond -> BoxOrDiamond
Show BoxOrDiamond Source #
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 Methods from :: BoxOrDiamond -> Rep BoxOrDiamond x to :: Rep BoxOrDiamond x -> BoxOrDiamond
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

Constructors

Defproc ProcKind Id [VAR] Program Range

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 Methods pretty :: Defproc -> Doc Source # pretties :: [Defproc] -> Doc Source #
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 procsMap :: Map Id Profile

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 Methods pretty :: Procs -> Doc Source # pretties :: [Procs] -> Doc Source #
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 Methods map_sen :: VSE -> VSEMor -> Sentence -> Result Sentence Source # simplify_sen :: VSE -> VSESign -> Sentence -> Sentence Source # negation :: VSE -> Sentence -> Maybe Sentence Source # print_sign :: VSE -> VSESign -> Doc Source # print_named :: VSE -> Named Sentence -> Doc Source # sym_of :: VSE -> VSESign -> [Set Symbol] Source # mostSymsOf :: VSE -> VSESign -> [Symbol] Source # symmap_of :: VSE -> VSEMor -> EndoMap Symbol Source # sym_name :: VSE -> Symbol -> Id Source # sym_label :: VSE -> Symbol -> Maybe String Source # fullSymName :: VSE -> Symbol -> String Source # symKind :: VSE -> Symbol -> String Source # symsOfSen :: VSE -> VSESign -> Sentence -> [Symbol] Source # pair_symbols :: VSE -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol Source #
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 Methods sourceLogic :: CASL2VSERefine -> CASL Source # sourceSublogic :: CASL2VSERefine -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSERefine -> CASL_Sublogics Source # minSourceTheory :: CASL2VSERefine -> Maybe (LibName, String) Source # targetLogic :: CASL2VSERefine -> VSE Source # mapSublogic :: CASL2VSERefine -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSERefine -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSERefine -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSERefine -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSERefine -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSERefine -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSERefine -> Bool Source # has_model_expansion :: CASL2VSERefine -> Bool Source # is_weakly_amalgamable :: CASL2VSERefine -> Bool Source # constituents :: CASL2VSERefine -> [String] Source # isInclusionComorphism :: CASL2VSERefine -> Bool Source # rps :: CASL2VSERefine -> Bool Source # eps :: CASL2VSERefine -> Bool Source # isGTC :: CASL2VSERefine -> Bool Source #
Comorphism CASL2VSEImport CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2VSEImport Methods sourceLogic :: CASL2VSEImport -> CASL Source # sourceSublogic :: CASL2VSEImport -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSEImport -> CASL_Sublogics Source # minSourceTheory :: CASL2VSEImport -> Maybe (LibName, String) Source # targetLogic :: CASL2VSEImport -> VSE Source # mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSEImport -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSEImport -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSEImport -> Bool Source # has_model_expansion :: CASL2VSEImport -> Bool Source # is_weakly_amalgamable :: CASL2VSEImport -> Bool Source # constituents :: CASL2VSEImport -> [String] Source # isInclusionComorphism :: CASL2VSEImport -> Bool Source # rps :: CASL2VSEImport -> Bool Source # eps :: CASL2VSEImport -> Bool Source # isGTC :: CASL2VSEImport -> Bool 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 #
Instance details Defined in Comorphisms.CASL2VSE Methods sourceLogic :: CASL2VSE -> CASL Source # sourceSublogic :: CASL2VSE -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2VSE -> CASL_Sublogics Source # minSourceTheory :: CASL2VSE -> Maybe (LibName, String) Source # targetLogic :: CASL2VSE -> VSE Source # mapSublogic :: CASL2VSE -> CASL_Sublogics -> Maybe () Source # map_theory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # mapMarkedTheory :: CASL2VSE -> (CASLSign, [Named CASLFORMULA]) -> Result (VSESign, [Named Sentence]) Source # map_morphism :: CASL2VSE -> CASLMor -> Result VSEMor Source # map_sentence :: CASL2VSE -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2VSE -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2VSE -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2VSE -> Bool Source # has_model_expansion :: CASL2VSE -> Bool Source # is_weakly_amalgamable :: CASL2VSE -> Bool Source # constituents :: CASL2VSE -> [String] Source # isInclusionComorphism :: CASL2VSE -> Bool Source # rps :: CASL2VSE -> Bool Source # eps :: CASL2VSE -> Bool Source # isGTC :: CASL2VSE -> Bool Source #
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))))

emptyProcs :: Procs Source #

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

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

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

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

Pretty instances

block :: Doc -> Doc Source #

prettyProcKind :: ProcKind -> Doc Source #

assign :: Doc Source #

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

gnUniformName :: SORT -> Id Source #

gnRestrName :: SORT -> Id Source #

gnEqName :: SORT -> Id Source #

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

xVar :: Token Source #

yVar :: Token Source #

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

prettyProcdefs :: [Defproc] -> Doc Source #