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

Documentation

data Paramkind

input or output procedure parameter kind

Constructors

In
Out

Instances

Eq Paramkind
Data Paramkind
Ord Paramkind
Show Paramkind
ShATermConvertible Paramkind
Typeable * Paramkind

data Procparam

a procedure parameter

Constructors

Procparam Paramkind SORT

Instances

Eq Procparam
Data Procparam
Ord Procparam
Show Procparam
ShATermConvertible Procparam
Pretty Procparam
Typeable * Procparam

data Profile

procedure or function declaration

Constructors

Profile [Procparam] (Maybe SORT)

Instances

Eq Profile
Data Profile
Ord Profile
Show Profile
ShATermConvertible Profile
Pretty Profile
Typeable * Profile

data Sigentry

further VSE signature entries

Constructors

Procedure Id Profile Range

Instances

Eq Sigentry
Data Sigentry
Ord Sigentry
Show Sigentry
ShATermConvertible Sigentry
Pretty Sigentry
Typeable * Sigentry

data Procdecls

Constructors

Procdecls [Annoted Sigentry] Range

Instances

Eq Procdecls
Data Procdecls
Ord Procdecls
Show Procdecls
ShATermConvertible Procdecls
GetRange Procdecls
Pretty Procdecls
AParsable Procdecls
Typeable * Procdecls
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol
Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol ()
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 ()
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 ()
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 ()

data Ranged a

wrapper for positions

Constructors

Ranged
Fields unRanged :: a range :: Range

Instances

TermParser Dlformula
TermExtension Dlformula
Sentences VSE Sentence VSESign VSEMor Symbol
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol
Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol ()
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 ()
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 ()
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 ()
Eq a => Eq (Ranged a)
Data a => Data (Ranged a)
Ord a => Ord (Ranged a)
Show a => Show (Ranged a)
ShATermConvertible a => ShATermConvertible (Ranged a)
GetRange (Ranged a)
Pretty a => Pretty (Ranged a)
FormExtension a => FormExtension (Ranged a)
Typeable (* -> *) Ranged

mkRanged :: a -> Ranged a

attach a nullRange

type Program = Ranged PlainProgram

programs with ranges

data PlainProgram

programs based on restricted terms and formulas

Constructors

Abort
Skip
Assign VAR (TERM ())
Call (FORMULA ())	a procedure call as predication
Return (TERM ())
Block [VAR_DECL] Program
Seq Program Program
If (FORMULA ()) Program Program
While (FORMULA ()) Program

Instances

Eq PlainProgram
Data PlainProgram
Ord PlainProgram
Show PlainProgram
ShATermConvertible PlainProgram
Pretty PlainProgram
Typeable * PlainProgram

data VarDecl

alternative variable declaration

Constructors

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

Instances

Data VarDecl
Show VarDecl
ShATermConvertible VarDecl
Pretty VarDecl
Typeable * VarDecl

toVarDecl :: [VAR_DECL] -> [VarDecl]

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

data VSEforms

extend CASL formulas by box or diamond formulas and defprocs

Constructors

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

Instances

Eq VSEforms
Data VSEforms
Ord VSEforms
Show VSEforms
ShATermConvertible VSEforms
GetRange VSEforms
Pretty VSEforms
TermParser Dlformula
FormExtension VSEforms
TermExtension Dlformula
Typeable * VSEforms
Sentences VSE Sentence VSESign VSEMor Symbol
Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol
Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol ()
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 ()
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 ()
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 ()

type Dlformula = Ranged VSEforms

type Sentence = FORMULA Dlformula

data BoxOrDiamond

box or diamond indicator

Constructors

Box
Diamond

Instances

Eq BoxOrDiamond
Data BoxOrDiamond
Ord BoxOrDiamond
Show BoxOrDiamond
ShATermConvertible BoxOrDiamond
Typeable * BoxOrDiamond

data ProcKind

Constructors

Proc
Func

Instances

Eq ProcKind
Data ProcKind
Ord ProcKind
Show ProcKind
ShATermConvertible ProcKind
Typeable * ProcKind

data Defproc

procedure definitions as basic items becoming sentences

Constructors

Defproc ProcKind Id [VAR] Program Range

Instances

Eq Defproc
Data Defproc
Ord Defproc
Show Defproc
ShATermConvertible Defproc
Pretty Defproc
Typeable * Defproc

data Procs

Constructors

Procs
Fields procsMap :: Map Id Profile

Instances

Eq Procs
Data Procs
Ord Procs
Show Procs
ShATermConvertible Procs
Pretty Procs
SignExtension Procs
Typeable * Procs
Sentences VSE Sentence VSESign VSEMor Symbol
StaticAnalysis VSE VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol
Logic VSE () VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS VSESign VSEMor Symbol RawSymbol ()
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 ()
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 ()
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 ()

emptyProcs :: Procs

unionProcs :: Procs -> Procs -> Result Procs

interProcs :: Procs -> Procs -> Result Procs

diffProcs :: Procs -> Procs -> Procs

isSubProcsMap :: Procs -> Procs -> Bool

Pretty instances

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