Previous  Up  Next

Module Expr

module Expr: sig .. end

WhyML program expressions

Routine symbols

type rsymbol = private {
   rs_name : Ident.ident;
   rs_cty : Ity.cty;
   rs_logic : rs_logic;
   rs_field : Ity.pvsymbol option;
} 
type rs_logic =
| RLnone
| RLpv of Ity.pvsymbol
| RLls of Term.lsymbol
| RLlemma 
module Mrs: Extmap.S  with type key = rsymbol
module Srs: Extset.S  with module M = Mrs
module Hrs: Exthtbl.S  with type key = rsymbol
module Wrs: Weakhtbl.S  with type key = rsymbol
val rs_compare : rsymbol -> rsymbol -> int
val rs_equal : rsymbol -> rsymbol -> bool
val rs_hash : rsymbol -> int
type rs_kind =
| RKnone
| RKlocal
| RKfunc
| RKpred
| RKlemma 
val rs_kind : rsymbol -> rs_kind
val create_rsymbol : Ident.preid -> ?ghost:bool -> ?kind:rs_kind -> Ity.cty -> rsymbol

If ?kind is supplied and is not RKnone, then cty must have no effects except for resets which are ignored. If ?kind is RKnone or RKlemma, external mutable reads are allowed, otherwise cty.cty_freeze.isb_reg must be empty. If ?kind is RKlocal, the type variables in cty are frozen but regions are instantiable. If ?kind is RKpred the result type must be ity_bool. If ?kind is RKlemma and the result type is not ity_unit, an existential premise is generated.

val create_constructor : constr:int ->
       Ident.preid -> Ity.itysymbol -> Ity.pvsymbol list -> rsymbol
val create_projection : bool -> Ity.itysymbol -> Ity.pvsymbol -> rsymbol
val restore_rs : Term.lsymbol -> rsymbol

raises Not_found if the argument is not a rs_logic

val rs_ghost : rsymbol -> bool
val ls_of_rs : rsymbol -> Term.lsymbol

raises Invalid_argument is rs_logic is not an RLls

val fd_of_rs : rsymbol -> Ity.pvsymbol

raises Invalid_argument is rs_field is None

Program patterns

type pat_ghost =
| PGfail
| PGlast
| PGnone 
type prog_pattern = private {
   pp_pat : Term.pattern;
   pp_ity : Ity.ity;
   pp_mask : Ity.mask;
   pp_fail : pat_ghost;
} 
type pre_pattern =
| PPwild
| PPvar of Ident.preid * bool (*

preid * if ghost

*)
| PPapp of rsymbol * pre_pattern list
| PPas of pre_pattern * Ident.preid * bool
| PPor of pre_pattern * pre_pattern 
exception ConstructorExpected of rsymbol
val create_prog_pattern : pre_pattern ->
       Ity.ity -> Ity.mask -> Ity.pvsymbol Wstdlib.Mstr.t * prog_pattern

Program expressions

type assertion_kind =
| Assert
| Assume
| Check 
type for_direction =
| To
| DownTo 
type for_bounds = Ity.pvsymbol * for_direction * Ity.pvsymbol 
type invariant = Term.term 
type variant = Term.term * Term.lsymbol option

tau * (tau -> tau -> prop)

type assign = Ity.pvsymbol * rsymbol * Ity.pvsymbol 
type expr_id = int 
val create_eid_attr : expr_id -> Ident.attribute

create_eid_attr id generates an attribute corresponding to the given expression identifier id

type expr = private {
   e_node : expr_node;
   e_ity : Ity.ity;
   e_mask : Ity.mask;
   e_effect : Ity.effect;
   e_attrs : Ident.Sattr.t;
   e_loc : Loc.position option;
   e_id : expr_id;
} 
type expr_node =
| Evar of Ity.pvsymbol
| Econst of Constant.constant
| Eexec of cexp * Ity.cty
| Eassign of assign list
| Elet of let_defn * expr
| Eif of expr * expr * expr
| Ematch of expr * reg_branch list * exn_branch Ity.Mxs.t
| Ewhile of expr * invariant list * variant list * expr
| Efor of Ity.pvsymbol * for_bounds * Ity.pvsymbol * invariant list
* expr
| Eraise of Ity.xsymbol * expr
| Eexn of Ity.xsymbol * expr
| Eassert of assertion_kind * Term.term
| Eghost of expr
| Epure of Term.term
| Eabsurd 
type reg_branch = prog_pattern * expr 
type exn_branch = Ity.pvsymbol list * expr 
type cexp = private {
   c_node : cexp_node;
   c_cty : Ity.cty;
} 
type cexp_node =
| Capp of rsymbol * Ity.pvsymbol list
| Cpur of Term.lsymbol * Ity.pvsymbol list
| Cfun of expr
| Cany 
type let_defn = private
| LDvar of Ity.pvsymbol * expr
| LDsym of rsymbol * cexp
| LDrec of rec_defn list 
type rec_defn = private {
   rec_sym : rsymbol;
   rec_rsym : rsymbol;
   rec_fun : cexp;
   rec_varl : variant list;
}

Expressions

val e_attr_set : ?loc:Loc.position -> Ident.Sattr.t -> expr -> expr
val e_attr_push : ?loc:Loc.position -> Ident.Sattr.t -> expr -> expr
val e_attr_add : Ident.attribute -> expr -> expr
val e_attr_copy : expr -> expr -> expr

Definitions

val let_var : Ident.preid -> ?ghost:bool -> expr -> let_defn * Ity.pvsymbol
val let_sym : Ident.preid ->
       ?ghost:bool ->
       ?kind:rs_kind -> cexp -> let_defn * rsymbol
val let_rec : (rsymbol * cexp * variant list * rs_kind) list ->
       let_defn * rec_defn list
val ls_decr_of_rec_defn : rec_defn -> Term.lsymbol option

Callable expressions

val c_app : rsymbol -> Ity.pvsymbol list -> Ity.ity list -> Ity.ity -> cexp
val c_pur : Term.lsymbol -> Ity.pvsymbol list -> Ity.ity list -> Ity.ity -> cexp
val c_fun : ?mask:Ity.mask ->
       Ity.pvsymbol list ->
       Ity.pre list ->
       Ity.post list ->
       Ity.post list Ity.Mxs.t -> Ity.pvsymbol Ity.Mpv.t -> expr -> cexp
val cty_from_formula : Term.term -> Ity.cty
val c_any : Ity.cty -> cexp

Expression constructors

val e_var : Ity.pvsymbol -> expr
val e_const : Constant.constant -> Ity.ity -> expr
val e_nat_const : int -> expr
val proxy_attrs : Ident.Sattr.t
val mk_proxy_decl : ghost:bool -> expr -> let_defn * Ity.pvsymbol

mk_proxy_decl ~ghost e returns a pair (ld,v) providing a fresh variable v that can be used as a substitute for expression e. ld is the corresponding let-definition. The fresh variable is marked as proxy except when e is a function call. In the latter case its name is chosen appropriately to match the post-condition.

val e_exec : cexp -> expr
val e_app : rsymbol -> expr list -> Ity.ity list -> Ity.ity -> expr
val e_pur : Term.lsymbol -> expr list -> Ity.ity list -> Ity.ity -> expr
val e_let : let_defn -> expr -> expr
exception FieldExpected of rsymbol
val e_assign : (expr * rsymbol * expr) list -> expr
val e_if : expr -> expr -> expr -> expr
val e_and : expr -> expr -> expr
val e_or : expr -> expr -> expr
val e_not : expr -> expr
val e_true : expr
val e_false : expr
val is_e_true : expr -> bool
val is_e_false : expr -> bool
exception ExceptionLeak of Ity.xsymbol
val e_exn : Ity.xsymbol -> expr -> expr
val e_raise : Ity.xsymbol -> expr -> Ity.ity -> expr
val e_match : expr -> reg_branch list -> exn_branch Ity.Mxs.t -> expr
val e_while : expr ->
       invariant list -> variant list -> expr -> expr
val e_for : Ity.pvsymbol ->
       expr ->
       for_direction ->
       expr -> Ity.pvsymbol -> invariant list -> expr -> expr
val e_assert : assertion_kind -> Term.term -> expr
val e_ghostify : bool -> expr -> expr
val e_pure : Term.term -> expr
val e_absurd : Ity.ity -> expr

Expression manipulation tools

val e_fold : ('a -> expr -> 'a) -> 'a -> expr -> 'a

e_fold does not descend into Cfun

val e_locate_effect : (Ity.effect -> bool) -> expr -> Loc.position option

e_locate_effect pr e looks for a minimal sub-expression of e whose effect satisfies pr and returns its location

val e_rs_subst : rsymbol Mrs.t -> expr -> expr
val c_rs_subst : rsymbol Mrs.t -> cexp -> cexp
val term_of_post : prop:bool -> Term.vsymbol -> Term.term -> (Term.term * Term.term) option
val term_of_expr : prop:bool -> expr -> Term.term option
val post_of_expr : Term.term -> expr -> Term.term option
val e_ghost : expr -> bool
val c_ghost : cexp -> bool

Built-in symbols

val rs_true : rsymbol
val rs_false : rsymbol
val rs_tuple : int -> rsymbol
val e_tuple : expr list -> expr
val rs_void : rsymbol
val fs_void : Term.lsymbol
val e_void : expr
val t_void : Term.term
val is_e_void : expr -> bool
val is_rs_tuple : rsymbol -> bool
val rs_func_app : rsymbol
val ld_func_app : let_defn
val e_func_app : expr -> expr -> expr
val e_func_app_l : expr -> expr list -> expr

Pretty-printing

val forget_rs : rsymbol -> unit
val print_rs : Stdlib.Format.formatter -> rsymbol -> unit
val print_expr : Stdlib.Format.formatter -> expr -> unit
val print_cexp : bool -> int -> Stdlib.Format.formatter -> cexp -> unit
val print_let_defn : Stdlib.Format.formatter -> let_defn -> unit