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 t -> 'a t
      val singleton : key -> '-> '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 option) -> 'a t -> 'a t -> 'a t
      val compare : ('-> '-> int) -> 'a t -> 'a t -> int
      val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val for_all : (key -> '-> bool) -> 'a t -> bool
      val exists : (key -> '-> bool) -> 'a t -> bool
      val filter : (key -> '-> bool) -> 'a t -> 'a t
      val partition : (key -> '-> 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 : ('-> 'b) -> 'a t -> 'b t
      val mapi : (key -> '-> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> '-> '-> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> '-> '-> 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 : '-> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('-> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> '-> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> '-> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> '-> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('-> key -> '-> 'b) -> '-> 'a t -> 'b
      val fold2_inter :
        (key -> '-> '-> '-> 'c) -> 'a t -> 'b t -> '-> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> '-> 'c) ->
        'a t -> 'b t -> '-> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> '-> 'a t -> 'a t
      val replace : exn -> key -> '-> '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 -> '-> 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 = 'Mrs.t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val mem : key -> 'a t -> bool
          val add : key -> '-> 'a t -> 'a t
          val singleton : key -> '-> '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 option) -> 'a t -> 'a t -> 'a t
          val compare : ('-> '-> int) -> 'a t -> 'a t -> int
          val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
          val iter : (key -> '-> unit) -> 'a t -> unit
          val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
          val for_all : (key -> '-> bool) -> 'a t -> bool
          val exists : (key -> '-> bool) -> 'a t -> bool
          val filter : (key -> '-> bool) -> 'a t -> 'a t
          val partition : (key -> '-> 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 : ('-> 'b) -> 'a t -> 'b t
          val mapi : (key -> '-> 'b) -> 'a t -> 'b t
          val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
          val inter : (key -> '-> '-> 'c option) -> 'a t -> 'b t -> 'c t
          val diff : (key -> '-> '-> 'a option) -> 'a t -> 'b t -> 'a t
          val submap : (key -> '-> '-> bool) -> 'a t -> 'b t -> bool
          val disjoint : (key -> '-> '-> 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 : '-> key -> 'a t -> 'a
          val find_opt : key -> 'a t -> 'a option
          val find_exn : exn -> key -> 'a t -> 'a
          val map_filter : ('-> 'b option) -> 'a t -> 'b t
          val mapi_filter : (key -> '-> 'b option) -> 'a t -> 'b t
          val mapi_fold :
            (key -> '-> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
          val mapi_filter_fold :
            (key -> '-> 'acc -> 'acc * 'b option) ->
            'a t -> 'acc -> 'acc * 'b t
          val fold_left : ('-> key -> '-> 'b) -> '-> 'a t -> 'b
          val fold2_inter :
            (key -> '-> '-> '-> 'c) -> 'a t -> 'b t -> '-> 'c
          val fold2_union :
            (key -> 'a option -> 'b option -> '-> 'c) ->
            'a t -> 'b t -> '-> 'c
          val translate : (key -> key) -> 'a t -> 'a t
          val add_new : exn -> key -> '-> 'a t -> 'a t
          val replace : exn -> key -> '-> '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 -> '-> bool) -> 'a t -> unit t
          val is_num_elt : int -> 'a t -> bool
          type 'a enumeration = '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) -> t -> '-> '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 : ('-> elt -> 'b) -> '-> t -> 'b
      val fold2_inter : (elt -> '-> 'a) -> t -> t -> '-> 'a
      val fold2_union : (elt -> '-> 'a) -> t -> t -> '-> '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 -> '-> 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 -> '-> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> '-> 'a option) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
      val find_def : 'a t -> '-> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_exn : 'a t -> exn -> key -> 'a
      val map : (key -> '-> '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 -> '-> unit
      val remove : 'a t -> key -> unit
      val iter : (key -> '-> unit) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val iterk : (key -> unit) -> 'a t -> unit
      val foldk : (key -> '-> 'b) -> 'a t -> '-> 'b
      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 : 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 = 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;
  }
  and expr_node =
      Evar of Ity.pvsymbol
    | Econst of Number.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 c_any : Ity.cty -> Expr.cexp
  val e_var : Ity.pvsymbol -> Expr.expr
  val e_const : Number.constant -> Ity.ity -> Expr.expr
  val e_nat_const : int -> Expr.expr
  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 : ('-> Expr.expr -> '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 : Format.formatter -> Expr.rsymbol -> unit
  val print_expr : Format.formatter -> Expr.expr -> unit
  val print_let_defn : Format.formatter -> Expr.let_defn -> unit
end