Module Mlw_expr

module Mlw_expr: sig .. end

Program Expressions




Program/logic symbols



Mlw_expr.plsymbols represent algebraic type constructors and projections. They must be fully applied and the result is equal to the application of the lsymbol. We need this kind of symbols to cover nullary constructors, such as Nil, which cannot be given a post-condition. They cannot be locally defined and therefore every type variable and region in their type signature can be instantiated.
type field = {
   fd_ity : Mlw_ty.T.ity;
   fd_ghost : bool;
   fd_mut : Mlw_ty.T.region option;
}
type plsymbol = private {
   pl_ls : Term.lsymbol;
   pl_args : field list;
   pl_value : field;
   pl_hidden : bool;
   pl_rdonly : bool;
}
val pl_equal : plsymbol -> plsymbol -> bool
val create_plsymbol : ?hidden:bool ->
?rdonly:bool ->
?constr:int ->
Ident.preid -> field list -> field -> plsymbol
val restore_pl : Term.lsymbol -> plsymbol
raises Not_found if the argument is not a pl_ls
exception HiddenPLS of plsymbol
exception RdOnlyPLS of plsymbol

Cloning


type symbol_map = private {
   sm_pure : Theory.symbol_map;
   sm_its : Mlw_ty.T.itysymbol Mlw_ty.Mits.t;
   sm_pls : plsymbol Term.Mls.t;
}
val pl_clone : Theory.symbol_map -> symbol_map

Patterns


type ppattern = private {
   ppat_pattern : Term.pattern;
   ppat_ity : Mlw_ty.T.ity;
   ppat_ghost : bool;
   ppat_fail : bool;
}
type pre_ppattern = 
| PPwild
| PPvar of Ident.preid
| PPlapp of Term.lsymbol * pre_ppattern list
| PPpapp of plsymbol * pre_ppattern list
| PPor of pre_ppattern * pre_ppattern
| PPas of pre_ppattern * Ident.preid
val make_ppattern : pre_ppattern ->
?ghost:bool ->
Mlw_ty.T.ity -> Mlw_ty.pvsymbol Stdlib.Mstr.t * ppattern

Program symbols



Mlw_expr.psymbols represent lambda-abstractions. They are polymorphic and can be type-instantiated in some type variables and regions of their type signature.
type psymbol = private {
   ps_name : Ident.ident;
   ps_aty : Mlw_ty.aty;
   ps_ghost : bool;
   ps_pvset : Mlw_ty.Spv.t;
   ps_vars : Mlw_ty.T.varset; (*
this varset covers the type variables and regions of the defining lambda that cannot be instantiated. Every other type variable and region in ps_aty is generalized and can be instantiated.
*)
   ps_subst : Mlw_ty.ity_subst; (*
this substitution instantiates every type variable and region in ps_vars to itself
*)
}
module Mps: Extmap.S  with type key = psymbol
module Sps: Extset.S  with module M = Mps
module Hps: Exthtbl.S  with type key = psymbol
module Wps: Weakhtbl.S  with type key = psymbol
val ps_equal : psymbol -> psymbol -> bool
val create_psymbol : Ident.preid -> ?ghost:bool -> Mlw_ty.aty -> psymbol

Program expressions


type assertion_kind = 
| Aassert
| Aassume
| Acheck
type for_direction = 
| To
| DownTo
type for_bounds = Mlw_ty.pvsymbol * for_direction * Mlw_ty.pvsymbol 
type invariant = Term.term 
type let_sym = 
| LetV of Mlw_ty.pvsymbol
| LetA of psymbol
type symset = private {
   syms_pv : Mlw_ty.Spv.t;
   syms_ps : Sps.t;
}
type expr = private {
   e_node : expr_node;
   e_vty : Mlw_ty.vty;
   e_ghost : bool;
   e_effect : Mlw_ty.effect;
   e_syms : symset;
   e_label : Ident.Slab.t;
   e_loc : Loc.position option;
}
type expr_node = private 
| Elogic of Term.term
| Evalue of Mlw_ty.pvsymbol
| Earrow of psymbol
| Eapp of expr * Mlw_ty.pvsymbol * Mlw_ty.spec
| Elet of let_defn * expr
| Erec of fun_defn list * expr
| Eif of expr * expr * expr
| Ecase of expr * (ppattern * expr) list
| Eassign of plsymbol * expr * Mlw_ty.T.region * Mlw_ty.pvsymbol
| Eghost of expr
| Eany of Mlw_ty.spec
| Eloop of invariant * Mlw_ty.variant list * expr
| Efor of Mlw_ty.pvsymbol * for_bounds * invariant * expr
| Eraise of Mlw_ty.xsymbol * expr
| Etry of expr * (Mlw_ty.xsymbol * Mlw_ty.pvsymbol * expr) list
| Eabstr of expr * Mlw_ty.spec
| Eassert of assertion_kind * Term.term
| Eabsurd
type let_defn = private {
   let_sym : let_sym;
   let_expr : expr;
}
type fun_defn = private {
   fun_ps : psymbol;
   fun_lambda : lambda;
   fun_syms : symset;
}
type lambda = {
   l_args : Mlw_ty.pvsymbol list;
   l_expr : expr;
   l_spec : Mlw_ty.spec;
}
val e_label : ?loc:Loc.position -> Ident.Slab.t -> expr -> expr
val e_label_add : Ident.label -> expr -> expr
val e_label_copy : expr -> expr -> expr
val e_value : Mlw_ty.pvsymbol -> expr
val e_arrow : psymbol -> Mlw_ty.T.ity list -> Mlw_ty.T.ity -> expr
e_arrow p argl res instantiates the program function symbol p into a program expression having the given types of the arguments and the result. The resulting expression can be applied to arguments using Mlw_expr.e_app given below.

See also examples/use_api/mlw.ml

exception ValueExpected of expr
exception ArrowExpected of expr
val ity_of_expr : expr -> Mlw_ty.T.ity
val aty_of_expr : expr -> Mlw_ty.aty
val e_app : expr -> expr list -> expr
e_app e el builds the application of e to arguments el. e is typically constructed using Mlw_expr.e_arrow defined above.

See also examples/use_api/mlw.ml

val e_lapp : Term.lsymbol -> expr list -> Mlw_ty.T.ity -> expr
val e_plapp : plsymbol -> expr list -> Mlw_ty.T.ity -> expr
val create_let_defn : Ident.preid -> expr -> let_defn
val create_let_pv_defn : Ident.preid -> expr -> let_defn * Mlw_ty.pvsymbol
val create_let_ps_defn : Ident.preid -> expr -> let_defn * psymbol
val create_fun_defn : Ident.preid -> lambda -> fun_defn
val create_rec_defn : (psymbol * lambda) list -> fun_defn list
exception StaleRegion of expr * Ident.ident
freshness violation: a previously reset region is associated to an ident
val e_let : let_defn -> expr -> expr
val e_rec : fun_defn list -> expr -> expr
val e_if : expr -> expr -> expr -> expr
val e_case : expr -> (ppattern * expr) list -> expr
exception Immutable of expr
val e_assign : plsymbol -> expr -> expr -> expr
val e_ghost : expr -> expr
val fs_void : Term.lsymbol
val t_void : Term.term
val e_void : expr
val e_const : Number.constant -> expr
val e_lazy_and : expr -> expr -> expr
val e_lazy_or : expr -> expr -> expr
val e_not : expr -> expr
val e_true : expr
val e_false : expr
val e_raise : Mlw_ty.xsymbol -> expr -> Mlw_ty.T.ity -> expr
val e_try : expr ->
(Mlw_ty.xsymbol * Mlw_ty.pvsymbol * expr) list -> expr
val e_loop : invariant -> Mlw_ty.variant list -> expr -> expr
val e_for : Mlw_ty.pvsymbol ->
expr ->
for_direction ->
expr -> invariant -> expr -> expr
val e_abstract : expr -> Mlw_ty.spec -> expr
val e_any : Mlw_ty.spec option -> Mlw_ty.vty -> expr
val e_assert : assertion_kind -> Term.term -> expr
val e_absurd : Mlw_ty.T.ity -> expr

Expression traversal


val e_fold : ('a -> expr -> 'a) -> 'a -> expr -> 'a
val e_find : (expr -> bool) -> expr -> expr
e_find pr e returns a sub-expression of e satisfying pr. raises Not_found if no sub-expression satisfies pr.
val e_purify : expr -> Term.term option