sig
type rsymbol = private {
rs_name : Ident.ident;
rs_cty : Ity.cty;
rs_logic : Expr.rs_logic;
rs_field : Ity.pvsymbol option;
}
and rs_logic =
RLnone
| RLpv of Ity.pvsymbol
| RLls of Term.lsymbol
| RLlemma
module Mrs :
sig
type key = rsymbol
type +'a t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val max_binding : 'a t -> key * 'a
val choose : 'a t -> key * 'a
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
val set_union : 'a t -> 'a t -> 'a t
val set_inter : 'a t -> 'b t -> 'a t
val set_diff : 'a t -> 'b t -> 'a t
val set_submap : 'a t -> 'b t -> bool
val set_disjoint : 'a t -> 'b t -> bool
val set_compare : 'a t -> 'b t -> int
val set_equal : 'a t -> 'b t -> bool
val find_def : 'a -> key -> 'a t -> 'a
val find_opt : key -> 'a t -> 'a option
val find_exn : exn -> key -> 'a t -> 'a
val map_filter : ('a -> 'b option) -> 'a t -> 'b t
val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
val mapi_fold :
(key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
val mapi_filter_fold :
(key -> 'a -> 'acc -> 'acc * 'b option) ->
'a t -> 'acc -> 'acc * 'b t
val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
val fold2_inter :
(key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
val fold2_union :
(key -> 'a option -> 'b option -> 'c -> 'c) ->
'a t -> 'b t -> 'c -> 'c
val translate : (key -> key) -> 'a t -> 'a t
val add_new : exn -> key -> 'a -> 'a t -> 'a t
val replace : exn -> key -> 'a -> 'a t -> 'a t
val keys : 'a t -> key list
val values : 'a t -> 'a list
val of_list : (key * 'a) list -> 'a t
val contains : 'a t -> key -> bool
val domain : 'a t -> unit t
val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
val is_num_elt : int -> 'a t -> bool
type 'a enumeration
val val_enum : 'a enumeration -> (key * 'a) option
val start_enum : 'a t -> 'a enumeration
val next_enum : 'a enumeration -> 'a enumeration
val start_ge_enum : key -> 'a t -> 'a enumeration
val next_ge_enum : key -> 'a enumeration -> 'a enumeration
end
module Srs :
sig
module M :
sig
type key = rsymbol
type 'a t = 'a Mrs.t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t -> 'b t -> 'c t
val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val max_binding : 'a t -> key * 'a
val choose : 'a t -> key * 'a
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
val set_union : 'a t -> 'a t -> 'a t
val set_inter : 'a t -> 'b t -> 'a t
val set_diff : 'a t -> 'b t -> 'a t
val set_submap : 'a t -> 'b t -> bool
val set_disjoint : 'a t -> 'b t -> bool
val set_compare : 'a t -> 'b t -> int
val set_equal : 'a t -> 'b t -> bool
val find_def : 'a -> key -> 'a t -> 'a
val find_opt : key -> 'a t -> 'a option
val find_exn : exn -> key -> 'a t -> 'a
val map_filter : ('a -> 'b option) -> 'a t -> 'b t
val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
val mapi_fold :
(key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
val mapi_filter_fold :
(key -> 'a -> 'acc -> 'acc * 'b option) ->
'a t -> 'acc -> 'acc * 'b t
val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
val fold2_inter :
(key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
val fold2_union :
(key -> 'a option -> 'b option -> 'c -> 'c) ->
'a t -> 'b t -> 'c -> 'c
val translate : (key -> key) -> 'a t -> 'a t
val add_new : exn -> key -> 'a -> 'a t -> 'a t
val replace : exn -> key -> 'a -> 'a t -> 'a t
val keys : 'a t -> key list
val values : 'a t -> 'a list
val of_list : (key * 'a) list -> 'a t
val contains : 'a t -> key -> bool
val domain : 'a t -> unit t
val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
val is_num_elt : int -> 'a t -> bool
type 'a enumeration = 'a Mrs.enumeration
val val_enum : 'a enumeration -> (key * 'a) option
val start_enum : 'a t -> 'a enumeration
val next_enum : 'a enumeration -> 'a enumeration
val start_ge_enum : key -> 'a t -> 'a enumeration
val next_ge_enum : key -> 'a enumeration -> 'a enumeration
end
type elt = M.key
type t = unit M.t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val merge : (elt -> bool -> bool -> bool) -> t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val disjoint : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val split : elt -> t -> t * bool * t
val change : (bool -> bool) -> elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val fold_left : ('b -> elt -> 'b) -> 'b -> t -> 'b
val fold2_inter : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
val fold2_union : (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
val translate : (elt -> elt) -> t -> t
val add_new : exn -> elt -> t -> t
val is_num_elt : int -> t -> bool
val of_list : elt list -> t
val contains : t -> elt -> bool
val add_left : t -> elt -> t
val remove_left : t -> elt -> t
val print :
(Format.formatter -> elt -> unit) -> Format.formatter -> t -> unit
end
module Hrs :
sig
type key = rsymbol
type !'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
val to_seq : 'a t -> (key * 'a) Seq.t
val to_seq_keys : 'a t -> key Seq.t
val to_seq_values : 'a t -> 'a Seq.t
val add_seq : 'a t -> (key * 'a) Seq.t -> unit
val replace_seq : 'a t -> (key * 'a) Seq.t -> unit
val of_seq : (key * 'a) Seq.t -> 'a t
val find_def : 'a t -> 'a -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_exn : 'a t -> exn -> key -> 'a
val map : (key -> 'a -> 'b) -> 'a t -> 'b t
val memo : int -> (key -> 'a) -> key -> 'a
val is_empty : 'a t -> bool
end
module Wrs :
sig
type key = rsymbol
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val copy : 'a t -> 'a t
val find : 'a t -> key -> 'a
val mem : 'a t -> key -> bool
val set : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val length : 'a t -> int
val memoize : int -> (key -> 'a) -> key -> 'a
val memoize_rec : int -> ((key -> 'a) -> key -> 'a) -> key -> 'a
val memoize_option : int -> (key option -> 'a) -> key option -> 'a
end
val rs_compare : Expr.rsymbol -> Expr.rsymbol -> int
val rs_equal : Expr.rsymbol -> Expr.rsymbol -> bool
val rs_hash : Expr.rsymbol -> int
type rs_kind = RKnone | RKlocal | RKfunc | RKpred | RKlemma
val rs_kind : Expr.rsymbol -> Expr.rs_kind
val create_rsymbol :
Ident.preid ->
?ghost:bool -> ?kind:Expr.rs_kind -> Ity.cty -> Expr.rsymbol
val create_constructor :
constr:int ->
Ident.preid -> Ity.itysymbol -> Ity.pvsymbol list -> Expr.rsymbol
val create_projection :
bool -> Ity.itysymbol -> Ity.pvsymbol -> Expr.rsymbol
val restore_rs : Term.lsymbol -> Expr.rsymbol
val rs_ghost : Expr.rsymbol -> bool
val ls_of_rs : Expr.rsymbol -> Term.lsymbol
val fd_of_rs : Expr.rsymbol -> Ity.pvsymbol
type pat_ghost = PGfail | PGlast | PGnone
type prog_pattern = private {
pp_pat : Term.pattern;
pp_ity : Ity.ity;
pp_mask : Ity.mask;
pp_fail : Expr.pat_ghost;
}
type pre_pattern =
PPwild
| PPvar of Ident.preid * bool
| PPapp of Expr.rsymbol * Expr.pre_pattern list
| PPas of Expr.pre_pattern * Ident.preid * bool
| PPor of Expr.pre_pattern * Expr.pre_pattern
exception ConstructorExpected of Expr.rsymbol
val create_prog_pattern :
Expr.pre_pattern ->
Ity.ity -> Ity.mask -> Ity.pvsymbol Wstdlib.Mstr.t * Expr.prog_pattern
type assertion_kind = Assert | Assume | Check
type for_direction = To | DownTo
type for_bounds = Ity.pvsymbol * Expr.for_direction * Ity.pvsymbol
type invariant = Term.term
type variant = Term.term * Term.lsymbol option
type assign = Ity.pvsymbol * Expr.rsymbol * Ity.pvsymbol
type expr_id = int
val create_eid_attr : Expr.expr_id -> Ident.attribute
type expr = private {
e_node : Expr.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.expr_id;
}
and expr_node =
Evar of Ity.pvsymbol
| Econst of Constant.constant
| Eexec of Expr.cexp * Ity.cty
| Eassign of Expr.assign list
| Elet of Expr.let_defn * Expr.expr
| Eif of Expr.expr * Expr.expr * Expr.expr
| Ematch of Expr.expr * Expr.reg_branch list * Expr.exn_branch Ity.Mxs.t
| Ewhile of Expr.expr * Expr.invariant list * Expr.variant list *
Expr.expr
| Efor of Ity.pvsymbol * Expr.for_bounds * Ity.pvsymbol *
Expr.invariant list * Expr.expr
| Eraise of Ity.xsymbol * Expr.expr
| Eexn of Ity.xsymbol * Expr.expr
| Eassert of Expr.assertion_kind * Term.term
| Eghost of Expr.expr
| Epure of Term.term
| Eabsurd
and reg_branch = Expr.prog_pattern * Expr.expr
and exn_branch = Ity.pvsymbol list * Expr.expr
and cexp = private { c_node : Expr.cexp_node; c_cty : Ity.cty; }
and cexp_node =
Capp of Expr.rsymbol * Ity.pvsymbol list
| Cpur of Term.lsymbol * Ity.pvsymbol list
| Cfun of Expr.expr
| Cany
and let_defn = private
LDvar of Ity.pvsymbol * Expr.expr
| LDsym of Expr.rsymbol * Expr.cexp
| LDrec of Expr.rec_defn list
and rec_defn = private {
rec_sym : Expr.rsymbol;
rec_rsym : Expr.rsymbol;
rec_fun : Expr.cexp;
rec_varl : Expr.variant list;
}
val e_attr_set :
?loc:Loc.position -> Ident.Sattr.t -> Expr.expr -> Expr.expr
val e_attr_push :
?loc:Loc.position -> Ident.Sattr.t -> Expr.expr -> Expr.expr
val e_attr_add : Ident.attribute -> Expr.expr -> Expr.expr
val e_attr_copy : Expr.expr -> Expr.expr -> Expr.expr
val let_var :
Ident.preid -> ?ghost:bool -> Expr.expr -> Expr.let_defn * Ity.pvsymbol
val let_sym :
Ident.preid ->
?ghost:bool ->
?kind:Expr.rs_kind -> Expr.cexp -> Expr.let_defn * Expr.rsymbol
val let_rec :
(Expr.rsymbol * Expr.cexp * Expr.variant list * Expr.rs_kind) list ->
Expr.let_defn * Expr.rec_defn list
val ls_decr_of_rec_defn : Expr.rec_defn -> Term.lsymbol option
val c_app :
Expr.rsymbol -> Ity.pvsymbol list -> Ity.ity list -> Ity.ity -> Expr.cexp
val c_pur :
Term.lsymbol -> Ity.pvsymbol list -> Ity.ity list -> Ity.ity -> Expr.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.expr -> Expr.cexp
val cty_from_formula : Term.term -> Ity.cty
val c_any : Ity.cty -> Expr.cexp
val e_var : Ity.pvsymbol -> Expr.expr
val e_const : Constant.constant -> Ity.ity -> Expr.expr
val e_nat_const : int -> Expr.expr
val proxy_attrs : Ident.Sattr.t
val mk_proxy_decl : ghost:bool -> Expr.expr -> Expr.let_defn * Ity.pvsymbol
val e_exec : Expr.cexp -> Expr.expr
val e_app :
Expr.rsymbol -> Expr.expr list -> Ity.ity list -> Ity.ity -> Expr.expr
val e_pur :
Term.lsymbol -> Expr.expr list -> Ity.ity list -> Ity.ity -> Expr.expr
val e_let : Expr.let_defn -> Expr.expr -> Expr.expr
exception FieldExpected of Expr.rsymbol
val e_assign : (Expr.expr * Expr.rsymbol * Expr.expr) list -> Expr.expr
val e_if : Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
val e_and : Expr.expr -> Expr.expr -> Expr.expr
val e_or : Expr.expr -> Expr.expr -> Expr.expr
val e_not : Expr.expr -> Expr.expr
val e_true : Expr.expr
val e_false : Expr.expr
val is_e_true : Expr.expr -> bool
val is_e_false : Expr.expr -> bool
exception ExceptionLeak of Ity.xsymbol
val e_exn : Ity.xsymbol -> Expr.expr -> Expr.expr
val e_raise : Ity.xsymbol -> Expr.expr -> Ity.ity -> Expr.expr
val e_match :
Expr.expr ->
Expr.reg_branch list -> Expr.exn_branch Ity.Mxs.t -> Expr.expr
val e_while :
Expr.expr ->
Expr.invariant list -> Expr.variant list -> Expr.expr -> Expr.expr
val e_for :
Ity.pvsymbol ->
Expr.expr ->
Expr.for_direction ->
Expr.expr ->
Ity.pvsymbol -> Expr.invariant list -> Expr.expr -> Expr.expr
val e_assert : Expr.assertion_kind -> Term.term -> Expr.expr
val e_ghostify : bool -> Expr.expr -> Expr.expr
val e_pure : Term.term -> Expr.expr
val e_absurd : Ity.ity -> Expr.expr
val e_fold : ('a -> Expr.expr -> 'a) -> 'a -> Expr.expr -> 'a
val e_locate_effect :
(Ity.effect -> bool) -> Expr.expr -> Loc.position option
val e_rs_subst : Expr.rsymbol Expr.Mrs.t -> Expr.expr -> Expr.expr
val c_rs_subst : Expr.rsymbol Expr.Mrs.t -> Expr.cexp -> Expr.cexp
val term_of_post :
prop:bool -> Term.vsymbol -> Term.term -> (Term.term * Term.term) option
val term_of_expr : prop:bool -> Expr.expr -> Term.term option
val post_of_expr : Term.term -> Expr.expr -> Term.term option
val e_ghost : Expr.expr -> bool
val c_ghost : Expr.cexp -> bool
val rs_true : Expr.rsymbol
val rs_false : Expr.rsymbol
val rs_tuple : int -> Expr.rsymbol
val e_tuple : Expr.expr list -> Expr.expr
val rs_void : Expr.rsymbol
val fs_void : Term.lsymbol
val e_void : Expr.expr
val t_void : Term.term
val is_e_void : Expr.expr -> bool
val is_rs_tuple : Expr.rsymbol -> bool
val rs_func_app : Expr.rsymbol
val ld_func_app : Expr.let_defn
val e_func_app : Expr.expr -> Expr.expr -> Expr.expr
val e_func_app_l : Expr.expr -> Expr.expr list -> Expr.expr
val forget_rs : Expr.rsymbol -> unit
val print_rs : Stdlib.Format.formatter -> Expr.rsymbol -> unit
val print_expr : Stdlib.Format.formatter -> Expr.expr -> unit
val print_cexp :
bool -> int -> Stdlib.Format.formatter -> Expr.cexp -> unit
val print_let_defn : Stdlib.Format.formatter -> Expr.let_defn -> unit
end