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
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
- data Paramkind
- 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 {}
- mkRanged :: a -> Ranged a
- type Program = Ranged PlainProgram
- data PlainProgram
- 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
- data ProcKind
- data Defproc = Defproc ProcKind Id [VAR] Program Range
- data Procs = Procs {}
- 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
input or output procedure parameter kind
a procedure parameter
procedure or function declaration
further VSE signature entries
Instances
wrapper for positions
Instances
type Program = Ranged PlainProgram Source #
programs with ranges
data PlainProgram Source #
programs based on restricted terms and formulas
Constructors
Abort | |
Skip | |
Assign VAR (TERM ()) | |
Call (FORMULA ()) | a procedure call as predication |
Return (TERM ()) | |
Block [VAR_DECL] Program | |
Seq Program Program | |
If (FORMULA ()) Program Program | |
While (FORMULA ()) Program |
Instances
Eq PlainProgram Source # | |
Data PlainProgram Source # | |
Ord PlainProgram Source # | |
Show PlainProgram Source # | |
Pretty PlainProgram Source # | |
alternative variable declaration
extend CASL formulas by box or diamond formulas and defprocs
Constructors
Dlformula BoxOrDiamond Program Sentence | |
Defprocs [Defproc] | |
RestrictedConstraint [Constraint] (Map SORT Id) Bool |
Instances
data BoxOrDiamond Source #
box or diamond indicator
Instances
Eq BoxOrDiamond Source # | |
Data BoxOrDiamond Source # | |
Ord BoxOrDiamond Source # | |
Show BoxOrDiamond Source # | |
procedure definitions as basic items becoming sentences
Instances
emptyProcs :: Procs Source #
isSubProcsMap :: Procs -> Procs -> Bool Source #
Pretty instances
prettyProcKind :: ProcKind -> Doc Source #
genSortName :: String -> SORT -> Id Source #
gnUniformName :: SORT -> Id Source #
gnRestrName :: SORT -> Id Source #
printRestrTypedecl :: Map SORT Id -> DATATYPE_DECL -> Doc Source #
prettyProcdefs :: [Defproc] -> Doc Source #