|
Opened structures |
---|
Type summary |
---|
|
|
|
|
|
Datatype summary |
---|
|
|
|
|
DataConstructor summary |
---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Type detail |
---|
type ident = ProofAst.ident
type term = ProofAst.term
type expType = ProofAst.formula
type typedIdent = ident * expType
type block = sequence * (ident list * typedIdent list)
type program = sequence
Datatype detail |
---|
datatype command =
Block of block
| For of ident * expression * block
| Affect of ident * expression
| Inc of ident
| Dec of ident
| ProcCall of expression * expression list * ident list
| Label of ident * block
| Jump of expression * expression list * typedIdent list
| CommRegion of command * region
datatype sequence =
Empty
| Comm of command * sequence
| Cst of ident * expression * sequence
| Var of ident * expression * sequence
| SeqRegion of sequence * region
datatype expression =
Id of ident
| Val of value
| Cast of expression * expType
| ExpRegion of expression * region
datatype value =
Star
| Int of int
| Proc of
ident list * typedIdent list * ident list * typedIdent list * block
| ValRegion of value * region
DataConstructor detail |
---|
constructor Block : block -> command
constructor For : ident * expression * block -> command
constructor Affect : ident * expression -> command
constructor Inc : ident -> command
constructor Dec : ident -> command
constructor ProcCall : expression * expression list * ident list -> command
constructor Label : ident * block -> command
constructor Jump : expression * expression list * typedIdent list -> command
constructor CommRegion : command * region -> command
constructor Empty : sequence
constructor Comm : command * sequence -> sequence
constructor Cst : ident * expression * sequence -> sequence
constructor Var : ident * expression * sequence -> sequence
constructor SeqRegion : sequence * region -> sequence
constructor Id : ident -> expression
constructor Val : value -> expression
constructor Cast : expression * expType -> expression
constructor ExpRegion : expression * region -> expression
constructor Star : value
constructor Int : int -> value
constructor Proc
: ident list *
typedIdent list *
ident list *
typedIdent list *
block ->
value
constructor ValRegion : value * region -> value
|