|
Opened structures |
---|
Type summary |
---|
|
|
|
|
DataConstructor summary |
---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Type detail |
---|
type ident = string * int
type sequence = i_sequence * (ident list * (ident * formula) list)
type expression = i_expression * formula
type value = i_value * formula
type block =
(i_sequence * (ident list * (ident * formula) list)) *
(ident list * (ident * formula) list)
type program = sequence
Datatype detail |
---|
datatype term = FId of ident | FZero | FFun of ident * term list
datatype formula =
TNat of term
| TProc of ident list * formula list * ident list * formula list
| TEqual of term * term
| TBot
| TVar of ident
datatype command =
Block of block
| For of ident * ident * expression * formula * block
| Affect of ident * formula * expression
| Inc of ident * formula
| Dec of ident * formula
| ProcCall of
(* p : proc(tau[i], sig) *)
expression *
formula *
(* (e1 : tau1[u], ..., en : taun[u]; *) (expression * formula) list *
(* [u/i] *) (ident * term) list *
(* r1 : sig1, ..., rp : sigp) *) (ident * formula) list
| Label of ident * formula * block
| Jump of
(* k : ~tau *)
expression *
formula *
(expression * formula) list *
(ident * term) list *
(ident * formula) list
| CommRegion of command * region
datatype i_sequence =
Empty of (ident * term) list
| Comm of command * sequence
| Cst of ident * formula * expression * sequence
| Var of ident * formula * expression * sequence
| SSubst of
(* s *)
sequence *
(* ({j}Omega)[i] *) (ident * formula) list *
(* i *) ident *
(* e : (n = m) *) expression *
formula
| SeqRegion of i_sequence * region
datatype i_expression =
Id of ident
| Val of value
| ESubst of
(* e *)
expression *
(* tau[i] *) formula *
(* i *) ident *
(* e' : (n = m) *) expression *
formula
| Lemma of formula list * formula
| ExpRegion of i_expression * region
datatype i_value =
Star
| Int of int
| Proc of
(* {il} in x:fl *)
ident list *
(ident * formula) list *
(* {jl} out y:fl' *) ident list *
(ident * formula) list *
(* { s }{jl}yfl *) block
| ValRegion of i_value * region
DataConstructor detail |
---|
constructor FId : ident -> term
constructor FZero : term
constructor FFun : ident * term list -> term
constructor TNat : term -> formula
constructor TProc
: ident list * formula list * ident list * formula list -> formula
constructor TEqual : term * term -> formula
constructor TBot : formula
constructor TVar : ident -> formula
constructor Block : block -> command
constructor For : ident * ident * expression * formula * block -> command
constructor Affect : ident * formula * expression -> command
constructor Inc : ident * formula -> command
constructor Dec : ident * formula -> command
constructor ProcCall
: (* p : proc(tau[i], sig) *)
expression *
formula *
(* (e1 : tau1[u], ..., en : taun[u]; *) (expression * formula) list *
(* [u/i] *) (ident * term) list *
(* r1 : sig1, ..., rp : sigp) *) (ident * formula) list ->
command
constructor Label : ident * formula * block -> command
constructor Jump
: (* k : ~tau *)
expression *
formula *
(expression * formula) list *
(ident * term) list *
(ident * formula) list ->
command
constructor CommRegion : command * region -> command
constructor Empty : (ident * term) list -> i_sequence
constructor Comm : command * sequence -> i_sequence
constructor Cst : ident * formula * expression * sequence -> i_sequence
constructor Var : ident * formula * expression * sequence -> i_sequence
constructor SSubst
: (* s *)
sequence *
(* ({j}Omega)[i] *) (ident * formula) list *
(* i *) ident *
(* e : (n = m) *) expression *
formula ->
i_sequence
constructor SeqRegion : i_sequence * region -> i_sequence
constructor Id : ident -> i_expression
constructor Val : value -> i_expression
constructor ESubst
: (* e *)
expression *
(* tau[i] *) formula *
(* i *) ident *
(* e' : (n = m) *) expression *
formula ->
i_expression
constructor Lemma : formula list * formula -> i_expression
constructor ExpRegion : i_expression * region -> i_expression
constructor Star : i_value
constructor Int : int -> i_value
constructor Proc
: (* {il} in x:fl *)
ident list *
(ident * formula) list *
(* {jl} out y:fl' *) ident list *
(ident * formula) list *
(* { s }{jl}yfl *) block ->
i_value
constructor ValRegion : i_value * region -> i_value
|