summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Assumed.ml11
-rw-r--r--compiler/Contexts.ml8
-rw-r--r--compiler/Print.ml35
-rw-r--r--compiler/PrintPure.ml18
-rw-r--r--compiler/Pure.ml24
-rw-r--r--compiler/PureTypeCheck.ml14
-rw-r--r--compiler/PureUtils.ml8
-rw-r--r--compiler/Substitute.ml320
-rw-r--r--compiler/SynthesizeSymbolic.ml8
-rw-r--r--compiler/TypesAnalysis.ml11
-rw-r--r--compiler/Values.ml15
11 files changed, 246 insertions, 226 deletions
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index e751d0ba..2fbb9044 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -53,6 +53,8 @@ module Sig = struct
(** Type parameter [T] of id 0 *)
let type_param_0 : T.type_var = { T.index = tvar_id_0; name = "T" }
+ let empty_const_generic_params : T.const_generic_var list = []
+
let mk_ref_ty (r : T.RegionVarId.id T.region) (ty : T.sty) (is_mut : bool) :
T.sty =
let ref_kind = if is_mut then T.Mut else T.Shared in
@@ -73,6 +75,7 @@ module Sig = struct
num_early_bound_regions = 0;
regions_hierarchy;
type_params;
+ const_generic_params = empty_const_generic_params;
inputs;
output;
}
@@ -84,6 +87,7 @@ module Sig = struct
num_early_bound_regions = 0;
regions_hierarchy = [];
type_params = [ type_param_0 ] (* <T> *);
+ const_generic_params = empty_const_generic_params;
inputs = [ tvar_0 (* T *) ];
output = mk_box_ty tvar_0 (* Box<T> *);
}
@@ -95,6 +99,7 @@ module Sig = struct
num_early_bound_regions = 0;
regions_hierarchy = [];
type_params = [ type_param_0 ] (* <T> *);
+ const_generic_params = empty_const_generic_params;
inputs = [ mk_box_ty tvar_0 (* Box<T> *) ];
output = mk_unit_ty (* () *);
}
@@ -112,6 +117,7 @@ module Sig = struct
num_early_bound_regions = 0;
regions_hierarchy;
type_params = [ type_param_0 ] (* <T> *);
+ const_generic_params = empty_const_generic_params;
inputs =
[ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box<T> *) ];
output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *);
@@ -135,6 +141,7 @@ module Sig = struct
num_early_bound_regions = 0;
regions_hierarchy;
type_params;
+ const_generic_params = empty_const_generic_params;
inputs;
output;
}
@@ -157,6 +164,7 @@ module Sig = struct
num_early_bound_regions = 0;
regions_hierarchy;
type_params;
+ const_generic_params = empty_const_generic_params;
inputs;
output;
}
@@ -180,6 +188,7 @@ module Sig = struct
num_early_bound_regions = 0;
regions_hierarchy;
type_params;
+ const_generic_params = empty_const_generic_params;
inputs;
output;
}
@@ -199,6 +208,7 @@ module Sig = struct
num_early_bound_regions = 0;
regions_hierarchy;
type_params;
+ const_generic_params = empty_const_generic_params;
inputs;
output;
}
@@ -223,6 +233,7 @@ module Sig = struct
num_early_bound_regions = 0;
regions_hierarchy;
type_params;
+ const_generic_params = empty_const_generic_params;
inputs;
output;
}
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index a425d42b..2ca5653d 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -12,7 +12,8 @@ open Identifiers
in the environment, because they contain borrows for instance, typically
because they might be overwritten during an assignment.
*)
-module DummyVarId = IdGen ()
+module DummyVarId =
+IdGen ()
type dummy_var_id = DummyVarId.id [@@deriving show, ord]
@@ -261,6 +262,7 @@ type eval_ctx = {
global_context : global_context;
region_groups : RegionGroupId.id list;
type_vars : type_var list;
+ const_generic_vars : const_generic_var list;
env : env;
ended_regions : RegionId.Set.t;
}
@@ -269,6 +271,10 @@ type eval_ctx = {
let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
TypeVarId.nth ctx.type_vars vid
+let lookup_const_generic_var (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
+ const_generic_var =
+ ConstGenericVarId.nth ctx.const_generic_vars vid
+
(** Lookup a variable in the current frame *)
let env_lookup_var (env : env) (vid : VarId.id) : var_binder * typed_value =
(* We take care to stop at the end of current frame: different variables
diff --git a/compiler/Print.ml b/compiler/Print.ml
index f544c0db..23cebd4c 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -19,6 +19,8 @@ module Values = struct
r_to_string : T.RegionId.id -> string;
type_var_id_to_string : T.TypeVarId.id -> string;
type_decl_id_to_string : T.TypeDeclId.id -> string;
+ const_generic_var_id_to_string : T.ConstGenericVarId.id -> string;
+ global_decl_id_to_string : T.GlobalDeclId.id -> string;
adt_variant_to_string : T.TypeDeclId.id -> T.VariantId.id -> string;
var_id_to_string : E.VarId.id -> string;
adt_field_names :
@@ -30,6 +32,8 @@ module Values = struct
PT.r_to_string = PT.erased_region_to_string;
PT.type_var_id_to_string = fmt.type_var_id_to_string;
PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
+ PT.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
+ PT.global_decl_id_to_string = fmt.global_decl_id_to_string;
}
let value_to_rtype_formatter (fmt : value_formatter) : PT.rtype_formatter =
@@ -37,6 +41,8 @@ module Values = struct
PT.r_to_string = PT.region_to_string fmt.r_to_string;
PT.type_var_id_to_string = fmt.type_var_id_to_string;
PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
+ PT.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
+ PT.global_decl_id_to_string = fmt.global_decl_id_to_string;
}
let value_to_stype_formatter (fmt : value_formatter) : PT.stype_formatter =
@@ -44,6 +50,8 @@ module Values = struct
PT.r_to_string = PT.region_to_string fmt.rvar_to_string;
PT.type_var_id_to_string = fmt.type_var_id_to_string;
PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
+ PT.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
+ PT.global_decl_id_to_string = fmt.global_decl_id_to_string;
}
let var_id_to_string (id : E.VarId.id) : string =
@@ -72,16 +80,16 @@ module Values = struct
string =
let ty_fmt : PT.etype_formatter = value_to_etype_formatter fmt in
match v.value with
- | Primitive cv -> PPV.primitive_value_to_string cv
+ | Primitive cv -> PPV.literal_to_string cv
| Adt av -> (
let field_values =
List.map (typed_value_to_string fmt) av.field_values
in
match v.ty with
- | T.Adt (T.Tuple, _, _) ->
+ | T.Adt (T.Tuple, _, _, _) ->
(* Tuple *)
"(" ^ String.concat ", " field_values ^ ")"
- | T.Adt (T.AdtId def_id, _, _) ->
+ | T.Adt (T.AdtId def_id, _, _, _) ->
(* "Regular" ADT *)
let adt_ident =
match av.variant_id with
@@ -103,7 +111,7 @@ module Values = struct
let field_values = String.concat " " field_values in
adt_ident ^ " { " ^ field_values ^ " }"
else adt_ident
- | T.Adt (T.Assumed aty, _, _) -> (
+ | T.Adt (T.Assumed aty, _, _, _) -> (
(* Assumed type *)
match (aty, field_values) with
| Box, [ bv ] -> "@Box(" ^ bv ^ ")"
@@ -188,10 +196,10 @@ module Values = struct
List.map (typed_avalue_to_string fmt) av.field_values
in
match v.ty with
- | T.Adt (T.Tuple, _, _) ->
+ | T.Adt (T.Tuple, _, _, _) ->
(* Tuple *)
"(" ^ String.concat ", " field_values ^ ")"
- | T.Adt (T.AdtId def_id, _, _) ->
+ | T.Adt (T.AdtId def_id, _, _, _) ->
(* "Regular" ADT *)
let adt_ident =
match av.variant_id with
@@ -213,7 +221,7 @@ module Values = struct
let field_values = String.concat " " field_values in
adt_ident ^ " { " ^ field_values ^ " }"
else adt_ident
- | T.Adt (T.Assumed aty, _, _) -> (
+ | T.Adt (T.Assumed aty, _, _, _) -> (
(* Assumed type *)
match (aty, field_values) with
| Box, [ bv ] -> "@Box(" ^ bv ^ ")"
@@ -425,6 +433,8 @@ module Contexts = struct
PV.r_to_string = fmt.r_to_string;
PV.type_var_id_to_string = fmt.type_var_id_to_string;
PV.type_decl_id_to_string = fmt.type_decl_id_to_string;
+ PV.const_generic_var_id_to_string = fmt.const_generic_var_id_to_string;
+ PV.global_decl_id_to_string = fmt.global_decl_id_to_string;
PV.adt_variant_to_string = fmt.adt_variant_to_string;
PV.var_id_to_string = fmt.var_id_to_string;
PV.adt_field_names = fmt.adt_field_names;
@@ -450,10 +460,18 @@ module Contexts = struct
let v = C.lookup_type_var ctx vid in
v.name
in
+ let const_generic_var_id_to_string vid =
+ let v = C.lookup_const_generic_var ctx vid in
+ v.name
+ in
let type_decl_id_to_string def_id =
let def = C.ctx_lookup_type_decl ctx def_id in
name_to_string def.name
in
+ let global_decl_id_to_string def_id =
+ let def = C.ctx_lookup_global_decl ctx def_id in
+ name_to_string def.name
+ in
let adt_variant_to_string =
PT.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls
in
@@ -469,6 +487,8 @@ module Contexts = struct
r_to_string;
type_var_id_to_string;
type_decl_id_to_string;
+ const_generic_var_id_to_string;
+ global_decl_id_to_string;
adt_variant_to_string;
var_id_to_string;
adt_field_names;
@@ -492,6 +512,7 @@ module Contexts = struct
r_to_string = ctx_fmt.PV.r_to_string;
type_var_id_to_string = ctx_fmt.PV.type_var_id_to_string;
type_decl_id_to_string = ctx_fmt.PV.type_decl_id_to_string;
+ const_generic_var_id_to_string = ctx_fmt.PV.const_generic_var_id_to_string;
adt_variant_to_string = ctx_fmt.PV.adt_variant_to_string;
var_id_to_string = ctx_fmt.PV.var_id_to_string;
adt_field_names = ctx_fmt.PV.adt_field_names;
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 3f35a023..03252200 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -55,8 +55,10 @@ let fun_name_to_string = Print.fun_name_to_string
let global_name_to_string = Print.global_name_to_string
let option_to_string = Print.option_to_string
let type_var_to_string = Print.Types.type_var_to_string
-let integer_type_to_string = Print.Types.integer_type_to_string
+let integer_type_to_string = Print.PrimitiveValues.integer_type_to_string
+let literal_type_to_string = Print.PrimitiveValues.literal_type_to_string
let scalar_value_to_string = Print.PrimitiveValues.scalar_value_to_string
+let literal_to_string = Print.PrimitiveValues.literal_to_string
let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
(type_params : type_var list) : type_formatter =
@@ -392,7 +394,7 @@ let adt_g_value_to_string (fmt : value_formatter)
let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) :
string =
match v.value with
- | PatConstant cv -> Print.PrimitiveValues.primitive_value_to_string cv
+ | PatConstant cv -> literal_to_string cv
| PatVar (v, None) -> var_to_string (ast_to_type_formatter fmt) v
| PatVar (v, Some mp) ->
let mp = "[@mplace=" ^ mplace_to_string fmt mp ^ "]" in
@@ -450,6 +452,16 @@ let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string =
| A.VecLen -> "alloc::vec::Vec::len"
| A.VecIndex -> "core::ops::index::Index<alloc::vec::Vec>::index"
| A.VecIndexMut -> "core::ops::index::IndexMut<alloc::vec::Vec>::index_mut"
+ | ArraySharedIndex -> "@ArraySharedIndex"
+ | ArrayMutIndex -> "@ArrayMutIndex"
+ | ArrayToSharedSlice -> "@ArrayToSharedSlice"
+ | ArrayToMutSlice -> "@ArrayToMutSlice"
+ | ArraySharedSubslice -> "@ArraySharedSubslice"
+ | ArrayMutSubslice -> "@ArrayMutSubslice"
+ | SliceSharedIndex -> "@SliceSharedIndex"
+ | SliceMutIndex -> "@SliceMutIndex"
+ | SliceSharedSubslice -> "@SliceSharedSubslice"
+ | SliceMutSubslice -> "@SliceMutSubslice"
let pure_assumed_fun_id_to_string (fid : pure_assumed_fun_id) : string =
match fid with
@@ -495,7 +507,7 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
| Var var_id ->
let s = fmt.var_id_to_string var_id in
if inside then "(" ^ s ^ ")" else s
- | Const cv -> Print.PrimitiveValues.primitive_value_to_string cv
+ | Const cv -> literal_to_string cv
| App _ ->
(* Recursively destruct the app, to have a pair (app, arguments list) *)
let app, args = destruct_apps e in
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index b251a005..5af28efd 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -187,7 +187,7 @@ type type_decl = {
[@@deriving show]
type scalar_value = V.scalar_value [@@deriving show]
-type primitive_value = V.primitive_value [@@deriving show]
+type literal = V.literal [@@deriving show]
(** Because we introduce a lot of temporary variables, the list of variables
is not fixed: we thus must carry all its information with the variable
@@ -232,10 +232,7 @@ type variant_id = VariantId.id [@@deriving show]
class ['self] iter_typed_pattern_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.iter
-
- method visit_primitive_value : 'env -> primitive_value -> unit =
- fun _ _ -> ()
-
+ method visit_literal : 'env -> literal -> unit = fun _ _ -> ()
method visit_var : 'env -> var -> unit = fun _ _ -> ()
method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
method visit_ty : 'env -> ty -> unit = fun _ _ -> ()
@@ -246,10 +243,7 @@ class ['self] iter_typed_pattern_base =
class ['self] map_typed_pattern_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.map
-
- method visit_primitive_value : 'env -> primitive_value -> primitive_value =
- fun _ x -> x
-
+ method visit_literal : 'env -> literal -> literal = fun _ x -> x
method visit_var : 'env -> var -> var = fun _ x -> x
method visit_mplace : 'env -> mplace -> mplace = fun _ x -> x
method visit_ty : 'env -> ty -> ty = fun _ x -> x
@@ -260,10 +254,7 @@ class ['self] map_typed_pattern_base =
class virtual ['self] reduce_typed_pattern_base =
object (self : 'self)
inherit [_] VisitorsRuntime.reduce
-
- method visit_primitive_value : 'env -> primitive_value -> 'a =
- fun _ _ -> self#zero
-
+ method visit_literal : 'env -> literal -> 'a = fun _ _ -> self#zero
method visit_var : 'env -> var -> 'a = fun _ _ -> self#zero
method visit_mplace : 'env -> mplace -> 'a = fun _ _ -> self#zero
method visit_ty : 'env -> ty -> 'a = fun _ _ -> self#zero
@@ -275,8 +266,7 @@ class virtual ['self] mapreduce_typed_pattern_base =
object (self : 'self)
inherit [_] VisitorsRuntime.mapreduce
- method visit_primitive_value
- : 'env -> primitive_value -> primitive_value * 'a =
+ method visit_literal : 'env -> literal -> literal * 'a =
fun _ x -> (x, self#zero)
method visit_var : 'env -> var -> var * 'a = fun _ x -> (x, self#zero)
@@ -292,7 +282,7 @@ class virtual ['self] mapreduce_typed_pattern_base =
(** A pattern (which appears on the left of assignments, in matches, etc.). *)
type pattern =
- | PatConstant of primitive_value
+ | PatConstant of literal
(** {!PatConstant} is necessary because we merge the switches over integer
values and the matches over enumerations *)
| PatVar of var * mplace option
@@ -486,7 +476,7 @@ class virtual ['self] mapreduce_expression_base =
*)
type expression =
| Var of var_id (** a variable *)
- | Const of primitive_value
+ | Const of literal
| App of texpression * texpression
(** Application of a function to an argument.
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 018ea6b5..72084dfc 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -56,17 +56,17 @@ type tc_ctx = {
env : ty VarId.Map.t; (** Environment from variables to types *)
}
-let check_primitive_value (v : primitive_value) (ty : ty) : unit =
+let check_literal (v : literal) (ty : ty) : unit =
match (ty, v) with
| Integer int_ty, PV.Scalar sv -> assert (int_ty = sv.PV.int_ty)
- | Bool, Bool _ | Char, Char _ | Str, String _ -> ()
+ | Bool, Bool _ | Char, Char _ -> ()
| _ -> raise (Failure "Inconsistent type")
let rec check_typed_pattern (ctx : tc_ctx) (v : typed_pattern) : tc_ctx =
log#ldebug (lazy ("check_typed_pattern: " ^ show_typed_pattern v));
match v.value with
| PatConstant cv ->
- check_primitive_value cv v.ty;
+ check_literal cv v.ty;
ctx
| PatDummy -> ctx
| PatVar (var, _) ->
@@ -108,7 +108,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
match VarId.Map.find_opt var_id ctx.env with
| None -> ()
| Some ty -> assert (ty = e.ty))
- | Const cv -> check_primitive_value cv e.ty
+ | Const cv -> check_literal cv e.ty
| App (app, arg) ->
let input_ty, output_ty = destruct_arrow app.ty in
assert (input_ty = arg.ty);
@@ -197,9 +197,9 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
| StructUpdate supd ->
(* Check the init value *)
(if Option.is_some supd.init then
- match VarId.Map.find_opt (Option.get supd.init) ctx.env with
- | None -> ()
- | Some ty -> assert (ty = e.ty));
+ match VarId.Map.find_opt (Option.get supd.init) ctx.env with
+ | None -> ()
+ | Some ty -> assert (ty = e.ty));
(* Check the fields *)
(* Retrieve and check the expected field type *)
let adt_id, adt_type_args =
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 647678c1..88b18e89 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -62,18 +62,16 @@ let dest_arrow_ty (ty : ty) : ty * ty =
| Arrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
| _ -> raise (Failure "Unreachable")
-let compute_primitive_value_ty (cv : primitive_value) : ty =
+let compute_literal_ty (cv : literal) : ty =
match cv with
| PV.Scalar sv -> Integer sv.PV.int_ty
| Bool _ -> Bool
| Char _ -> Char
- | String _ -> Str
let var_get_id (v : var) : VarId.id = v.id
-let mk_typed_pattern_from_primitive_value (cv : primitive_value) : typed_pattern
- =
- let ty = compute_primitive_value_ty cv in
+let mk_typed_pattern_from_literal (cv : literal) : typed_pattern =
+ let ty = compute_literal_ty cv in
{ value = PatConstant cv; ty }
let mk_let (monadic : bool) (lv : typed_pattern) (re : texpression)
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 5040fd9f..a1b1572e 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -11,7 +11,8 @@ module C = Contexts
(** Substitute types variables and regions in a type. *)
let ty_substitute (rsubst : 'r1 -> 'r2) (tsubst : T.TypeVarId.id -> 'r2 T.ty)
- (ty : 'r1 T.ty) : 'r2 T.ty =
+ (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (ty : 'r1 T.ty) :
+ 'r2 T.ty =
let open T in
let visitor =
object
@@ -22,25 +23,37 @@ let ty_substitute (rsubst : 'r1 -> 'r2) (tsubst : T.TypeVarId.id -> 'r2 T.ty)
method! visit_type_var_id _ _ =
(* We should never get here because we reimplemented [visit_TypeVar] *)
raise (Failure "Unexpected")
+
+ method! visit_ConstGenericVar _ id = cgsubst id
+
+ method! visit_const_generic_var_id _ _ =
+ (* We should never get here because we reimplemented [visit_Var] *)
+ raise (Failure "Unexpected")
end
in
visitor#visit_ty () ty
let rty_substitute (rsubst : T.RegionId.id -> T.RegionId.id)
- (tsubst : T.TypeVarId.id -> T.rty) (ty : T.rty) : T.rty =
+ (tsubst : T.TypeVarId.id -> T.rty)
+ (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (ty : T.rty) : T.rty =
let rsubst r =
match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid)
in
- ty_substitute rsubst tsubst ty
+ ty_substitute rsubst tsubst cgsubst ty
-let ety_substitute (tsubst : T.TypeVarId.id -> T.ety) (ty : T.ety) : T.ety =
+let ety_substitute (tsubst : T.TypeVarId.id -> T.ety)
+ (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (ty : T.ety) : T.ety =
let rsubst r = r in
- ty_substitute rsubst tsubst ty
+ ty_substitute rsubst tsubst cgsubst ty
(** Convert an {!T.rty} to an {!T.ety} by erasing the region variables *)
let erase_regions (ty : T.rty) : T.ety =
- ty_substitute (fun _ -> T.Erased) (fun vid -> T.TypeVar vid) ty
+ ty_substitute
+ (fun _ -> T.Erased)
+ (fun vid -> T.TypeVar vid)
+ (fun id -> T.ConstGenericVar id)
+ ty
(** Generate fresh regions for region variables.
@@ -59,7 +72,7 @@ let fresh_regions_with_substs (region_vars : T.region_var list) :
let ls = List.combine region_vars fresh_region_ids in
let rid_map =
List.fold_left
- (fun mp (k, v) -> T.RegionVarId.Map.add k.T.index v mp)
+ (fun mp ((k : T.region_var), v) -> T.RegionVarId.Map.add k.T.index v mp)
T.RegionVarId.Map.empty ls
in
(* Generate the substitution from region var id to region *)
@@ -73,9 +86,10 @@ let fresh_regions_with_substs (region_vars : T.region_var list) :
(** Erase the regions in a type and substitute the type variables *)
let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety)
+ (cgsubst : T.ConstGenericVarId.id -> T.const_generic)
(ty : 'r T.region T.ty) : T.ety =
let rsubst (_ : 'r T.region) : T.erased_region = T.Erased in
- ty_substitute rsubst tsubst ty
+ ty_substitute rsubst tsubst cgsubst ty
(** Create a region substitution from a list of region variable ids and a list of
regions (with which to substitute the region variable ids *)
@@ -92,6 +106,12 @@ let make_region_subst (var_ids : T.RegionVarId.id list)
| T.Static -> T.Static
| T.Var id -> T.RegionVarId.Map.find id mp
+let make_region_subst_from_vars (vars : T.region_var list)
+ (regions : 'r T.region list) : T.RegionVarId.id T.region -> 'r T.region =
+ make_region_subst
+ (List.map (fun (x : T.region_var) -> x.T.index) vars)
+ regions
+
(** Create a type substitution from a list of type variable ids and a list of
types (with which to substitute the type variable ids) *)
let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) :
@@ -104,18 +124,37 @@ let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) :
in
fun id -> T.TypeVarId.Map.find id mp
+let make_type_subst_from_vars (vars : T.type_var list) (tys : 'r T.ty list) :
+ T.TypeVarId.id -> 'r T.ty =
+ make_type_subst (List.map (fun (x : T.type_var) -> x.T.index) vars) tys
+
+(** Create a const generic substitution from a list of const generic variable ids and a list of
+ const generics (with which to substitute the const generic variable ids) *)
+let make_const_generic_subst (var_ids : T.ConstGenericVarId.id list)
+ (cgs : T.const_generic list) : T.ConstGenericVarId.id -> T.const_generic =
+ let ls = List.combine var_ids cgs in
+ let mp =
+ List.fold_left
+ (fun mp (k, v) -> T.ConstGenericVarId.Map.add k v mp)
+ T.ConstGenericVarId.Map.empty ls
+ in
+ fun id -> T.ConstGenericVarId.Map.find id mp
+
+let make_const_generic_subst_from_vars (vars : T.const_generic_var list)
+ (cgs : T.const_generic list) : T.ConstGenericVarId.id -> T.const_generic =
+ make_const_generic_subst
+ (List.map (fun (x : T.const_generic_var) -> x.T.index) vars)
+ cgs
+
(** Instantiate the type variables in an ADT definition, and return, for
every variant, the list of the types of its fields *)
let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
- (regions : T.RegionId.id T.region list) (types : T.rty list) :
- (T.VariantId.id option * T.rty list) list =
- let r_subst =
- make_region_subst
- (List.map (fun x -> x.T.index) def.T.region_params)
- regions
- in
- let ty_subst =
- make_type_subst (List.map (fun x -> x.T.index) def.T.type_params) types
+ (regions : T.RegionId.id T.region list) (types : T.rty list)
+ (cgs : T.const_generic list) : (T.VariantId.id option * T.rty list) list =
+ let r_subst = make_region_subst_from_vars def.T.region_params regions in
+ let ty_subst = make_type_subst_from_vars def.T.type_params types in
+ let cg_subst =
+ make_const_generic_subst_from_vars def.T.const_generic_params cgs
in
let (variants_fields : (T.VariantId.id option * T.field list) list) =
match def.T.kind with
@@ -133,45 +172,47 @@ let type_decl_get_instantiated_variants_fields_rtypes (def : T.type_decl)
List.map
(fun (id, fields) ->
( id,
- List.map (fun f -> ty_substitute r_subst ty_subst f.T.field_ty) fields
- ))
+ List.map
+ (fun f -> ty_substitute r_subst ty_subst cg_subst f.T.field_ty)
+ fields ))
variants_fields
(** Instantiate the type variables in an ADT definition, and return the list
of types of the fields for the chosen variant *)
let type_decl_get_instantiated_field_rtypes (def : T.type_decl)
(opt_variant_id : T.VariantId.id option)
- (regions : T.RegionId.id T.region list) (types : T.rty list) : T.rty list =
- let r_subst =
- make_region_subst
- (List.map (fun x -> x.T.index) def.T.region_params)
- regions
- in
- let ty_subst =
- make_type_subst (List.map (fun x -> x.T.index) def.T.type_params) types
+ (regions : T.RegionId.id T.region list) (types : T.rty list)
+ (cgs : T.const_generic list) : T.rty list =
+ let r_subst = make_region_subst_from_vars def.T.region_params regions in
+ let ty_subst = make_type_subst_from_vars def.T.type_params types in
+ let cg_subst =
+ make_const_generic_subst_from_vars def.T.const_generic_params cgs
in
let fields = TU.type_decl_get_fields def opt_variant_id in
- List.map (fun f -> ty_substitute r_subst ty_subst f.T.field_ty) fields
+ List.map
+ (fun f -> ty_substitute r_subst ty_subst cg_subst f.T.field_ty)
+ fields
(** Return the types of the properly instantiated ADT's variant, provided a
context *)
let ctx_adt_get_instantiated_field_rtypes (ctx : C.eval_ctx)
(def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
- (regions : T.RegionId.id T.region list) (types : T.rty list) : T.rty list =
+ (regions : T.RegionId.id T.region list) (types : T.rty list)
+ (cgs : T.const_generic list) : T.rty list =
let def = C.ctx_lookup_type_decl ctx def_id in
- type_decl_get_instantiated_field_rtypes def opt_variant_id regions types
+ type_decl_get_instantiated_field_rtypes def opt_variant_id regions types cgs
(** Return the types of the properly instantiated ADT value (note that
here, ADT is understood in its broad meaning: ADT, assumed value or tuple) *)
let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
(adt : V.adt_value) (id : T.type_id)
- (region_params : T.RegionId.id T.region list) (type_params : T.rty list) :
- T.rty list =
+ (region_params : T.RegionId.id T.region list) (type_params : T.rty list)
+ (cg_params : T.const_generic list) : T.rty list =
match id with
| T.AdtId id ->
(* Retrieve the types of the fields *)
ctx_adt_get_instantiated_field_rtypes ctx id adt.V.variant_id
- region_params type_params
+ region_params type_params cg_params
| T.Tuple ->
assert (List.length region_params = 0);
type_params
@@ -180,182 +221,116 @@ let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
| T.Box | T.Vec ->
assert (List.length region_params = 0);
assert (List.length type_params = 1);
+ assert (List.length cg_params = 0);
type_params
| T.Option ->
assert (List.length region_params = 0);
assert (List.length type_params = 1);
+ assert (List.length cg_params = 0);
if adt.V.variant_id = Some T.option_some_id then type_params
else if adt.V.variant_id = Some T.option_none_id then []
- else raise (Failure "Unreachable"))
+ else raise (Failure "Unreachable")
+ | T.Array | T.Slice | T.Str ->
+ (* Those types don't have fields *)
+ raise (Failure "Unreachable"))
(** Instantiate the type variables in an ADT definition, and return the list
of types of the fields for the chosen variant *)
let type_decl_get_instantiated_field_etypes (def : T.type_decl)
- (opt_variant_id : T.VariantId.id option) (types : T.ety list) : T.ety list =
- let ty_subst =
- make_type_subst (List.map (fun x -> x.T.index) def.T.type_params) types
+ (opt_variant_id : T.VariantId.id option) (types : T.ety list)
+ (cgs : T.const_generic list) : T.ety list =
+ let ty_subst = make_type_subst_from_vars def.T.type_params types in
+ let cg_subst =
+ make_const_generic_subst_from_vars def.T.const_generic_params cgs
in
let fields = TU.type_decl_get_fields def opt_variant_id in
List.map
- (fun f -> erase_regions_substitute_types ty_subst f.T.field_ty)
+ (fun f -> erase_regions_substitute_types ty_subst cg_subst f.T.field_ty)
fields
(** Return the types of the properly instantiated ADT's variant, provided a
context *)
let ctx_adt_get_instantiated_field_etypes (ctx : C.eval_ctx)
(def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
- (types : T.ety list) : T.ety list =
+ (types : T.ety list) (cgs : T.const_generic list) : T.ety list =
let def = C.ctx_lookup_type_decl ctx def_id in
- type_decl_get_instantiated_field_etypes def opt_variant_id types
+ type_decl_get_instantiated_field_etypes def opt_variant_id types cgs
+
+let statement_substitute_visitor (tsubst : T.TypeVarId.id -> T.ety)
+ (cgsubst : T.ConstGenericVarId.id -> T.const_generic) =
+ object
+ inherit [_] A.map_statement
+ method! visit_ety _ ty = ety_substitute tsubst cgsubst ty
+ method! visit_ConstGenericVar _ id = cgsubst id
+
+ method! visit_const_generic_var_id _ _ =
+ (* We should never get here because we reimplemented [visit_Var] *)
+ raise (Failure "Unexpected")
+ end
(** Apply a type substitution to a place *)
-let place_substitute (_tsubst : T.TypeVarId.id -> T.ety) (p : E.place) : E.place
- =
- (* There is nothing to do *)
- p
+let place_substitute (tsubst : T.TypeVarId.id -> T.ety)
+ (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (p : E.place) :
+ E.place =
+ (* There is in fact nothing to do *)
+ (statement_substitute_visitor tsubst cgsubst)#visit_place () p
(** Apply a type substitution to an operand *)
-let operand_substitute (tsubst : T.TypeVarId.id -> T.ety) (op : E.operand) :
+let operand_substitute (tsubst : T.TypeVarId.id -> T.ety)
+ (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (op : E.operand) :
E.operand =
- let p_subst = place_substitute tsubst in
- match op with
- | E.Copy p -> E.Copy (p_subst p)
- | E.Move p -> E.Move (p_subst p)
- | E.Constant (ety, cv) ->
- let rsubst x = x in
- E.Constant (ty_substitute rsubst tsubst ety, cv)
+ (statement_substitute_visitor tsubst cgsubst)#visit_operand () op
(** Apply a type substitution to an rvalue *)
-let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety) (rv : E.rvalue) :
+let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety)
+ (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (rv : E.rvalue) :
E.rvalue =
- let op_subst = operand_substitute tsubst in
- let p_subst = place_substitute tsubst in
- match rv with
- | E.Use op -> E.Use (op_subst op)
- | E.Ref (p, bkind) -> E.Ref (p_subst p, bkind)
- | E.UnaryOp (unop, op) -> E.UnaryOp (unop, op_subst op)
- | E.BinaryOp (binop, op1, op2) ->
- E.BinaryOp (binop, op_subst op1, op_subst op2)
- | E.Discriminant p -> E.Discriminant (p_subst p)
- | E.Global _ -> (* Globals don't have type parameters *) rv
- | E.Aggregate (kind, ops) ->
- let ops = List.map op_subst ops in
- let kind =
- match kind with
- | E.AggregatedTuple -> E.AggregatedTuple
- | E.AggregatedOption (variant_id, ty) ->
- let rsubst r = r in
- E.AggregatedOption (variant_id, ty_substitute rsubst tsubst ty)
- | E.AggregatedAdt (def_id, variant_id, regions, tys) ->
- let rsubst r = r in
- E.AggregatedAdt
- ( def_id,
- variant_id,
- regions,
- List.map (ty_substitute rsubst tsubst) tys )
- in
- E.Aggregate (kind, ops)
+ (statement_substitute_visitor tsubst cgsubst)#visit_rvalue () rv
(** Apply a type substitution to an assertion *)
-let assertion_substitute (tsubst : T.TypeVarId.id -> T.ety) (a : A.assertion) :
+let assertion_substitute (tsubst : T.TypeVarId.id -> T.ety)
+ (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (a : A.assertion) :
A.assertion =
- { A.cond = operand_substitute tsubst a.A.cond; A.expected = a.A.expected }
+ (statement_substitute_visitor tsubst cgsubst)#visit_assertion () a
(** Apply a type substitution to a call *)
-let call_substitute (tsubst : T.TypeVarId.id -> T.ety) (call : A.call) : A.call
- =
- let rsubst x = x in
- let type_args = List.map (ty_substitute rsubst tsubst) call.A.type_args in
- let args = List.map (operand_substitute tsubst) call.A.args in
- let dest = place_substitute tsubst call.A.dest in
- (* Putting all the paramters on purpose: we want to get a compiler error if
- something moves - we may add a field on which we need to apply a substitution *)
- {
- func = call.A.func;
- region_args = call.A.region_args;
- A.type_args;
- args;
- dest;
- }
-
-(** Apply a type substitution to a statement - TODO: use a map iterator *)
-let rec statement_substitute (tsubst : T.TypeVarId.id -> T.ety)
- (st : A.statement) : A.statement =
- { st with A.content = raw_statement_substitute tsubst st.content }
-
-and raw_statement_substitute (tsubst : T.TypeVarId.id -> T.ety)
- (st : A.raw_statement) : A.raw_statement =
- match st with
- | A.Assign (p, rvalue) ->
- let p = place_substitute tsubst p in
- let rvalue = rvalue_substitute tsubst rvalue in
- A.Assign (p, rvalue)
- | A.FakeRead p ->
- let p = place_substitute tsubst p in
- A.FakeRead p
- | A.SetDiscriminant (p, vid) ->
- let p = place_substitute tsubst p in
- A.SetDiscriminant (p, vid)
- | A.Drop p ->
- let p = place_substitute tsubst p in
- A.Drop p
- | A.Assert assertion ->
- let assertion = assertion_substitute tsubst assertion in
- A.Assert assertion
- | A.Call call ->
- let call = call_substitute tsubst call in
- A.Call call
- | A.Panic | A.Return | A.Break _ | A.Continue _ | A.Nop -> st
- | A.Sequence (st1, st2) ->
- A.Sequence
- (statement_substitute tsubst st1, statement_substitute tsubst st2)
- | A.Switch switch -> A.Switch (switch_substitute tsubst switch)
- | A.Loop le -> A.Loop (statement_substitute tsubst le)
-
-(** Apply a type substitution to a switch *)
-and switch_substitute (tsubst : T.TypeVarId.id -> T.ety) (switch : A.switch) :
- A.switch =
- match switch with
- | A.If (op, st1, st2) ->
- A.If
- ( operand_substitute tsubst op,
- statement_substitute tsubst st1,
- statement_substitute tsubst st2 )
- | A.SwitchInt (op, int_ty, tgts, otherwise) ->
- let tgts =
- List.map (fun (sv, st) -> (sv, statement_substitute tsubst st)) tgts
- in
- let otherwise = statement_substitute tsubst otherwise in
- A.SwitchInt (operand_substitute tsubst op, int_ty, tgts, otherwise)
- | A.Match (p, tgts, otherwise) ->
- let tgts =
- List.map (fun (sv, st) -> (sv, statement_substitute tsubst st)) tgts
- in
- let otherwise = statement_substitute tsubst otherwise in
- A.Match (place_substitute tsubst p, tgts, otherwise)
+let call_substitute (tsubst : T.TypeVarId.id -> T.ety)
+ (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (call : A.call) :
+ A.call =
+ (statement_substitute_visitor tsubst cgsubst)#visit_call () call
+
+(** Apply a type substitution to a statement *)
+let statement_substitute (tsubst : T.TypeVarId.id -> T.ety)
+ (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (st : A.statement) :
+ A.statement =
+ (statement_substitute_visitor tsubst cgsubst)#visit_statement () st
(** Apply a type substitution to a function body. Return the local variables
and the body. *)
let fun_body_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety)
- (body : A.fun_body) : A.var list * A.statement =
+ (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (body : A.fun_body) :
+ A.var list * A.statement =
let rsubst r = r in
let locals =
List.map
- (fun v -> { v with A.var_ty = ty_substitute rsubst tsubst v.A.var_ty })
+ (fun (v : A.var) ->
+ { v with A.var_ty = ty_substitute rsubst tsubst cgsubst v.A.var_ty })
body.A.locals
in
- let body = statement_substitute tsubst body.body in
+ let body = statement_substitute tsubst cgsubst body.body in
(locals, body)
(** Substitute a function signature *)
let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
(rsubst : T.RegionVarId.id -> T.RegionId.id)
- (tsubst : T.TypeVarId.id -> T.rty) (sg : A.fun_sig) : A.inst_fun_sig =
+ (tsubst : T.TypeVarId.id -> T.rty)
+ (cgsubst : T.ConstGenericVarId.id -> T.const_generic) (sg : A.fun_sig) :
+ A.inst_fun_sig =
let rsubst' (r : T.RegionVarId.id T.region) : T.RegionId.id T.region =
match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid)
in
- let inputs = List.map (ty_substitute rsubst' tsubst) sg.A.inputs in
- let output = ty_substitute rsubst' tsubst sg.A.output in
+ let inputs = List.map (ty_substitute rsubst' tsubst cgsubst) sg.A.inputs in
+ let output = ty_substitute rsubst' tsubst cgsubst sg.A.output in
let subst_region_group (rg : T.region_var_group) : A.abs_region_group =
let id = asubst rg.id in
let regions = List.map rsubst rg.regions in
@@ -366,7 +341,8 @@ let substitute_signature (asubst : T.RegionGroupId.id -> V.AbstractionId.id)
{ A.regions_hierarchy; inputs; output }
(** Substitute type variable identifiers in a type *)
-let ty_substitute_ids (tsubst : T.TypeVarId.id -> T.TypeVarId.id) (ty : 'r T.ty)
+let ty_substitute_ids (tsubst : T.TypeVarId.id -> T.TypeVarId.id)
+ (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id) (ty : 'r T.ty)
: 'r T.ty =
let open T in
let visitor =
@@ -374,6 +350,7 @@ let ty_substitute_ids (tsubst : T.TypeVarId.id -> T.TypeVarId.id) (ty : 'r T.ty)
inherit [_] map_ty
method visit_'r _ r = r
method! visit_type_var_id _ id = tsubst id
+ method! visit_const_generic_var_id _ id = cgsubst id
end
in
@@ -384,7 +361,7 @@ let ty_substitute_ids (tsubst : T.TypeVarId.id -> T.TypeVarId.id) (ty : 'r T.ty)
We want to write a class which visits abstractions, values, etc. *and their
types* to substitute identifiers.
- The issue comes is that we derive two specialized types (ety and rty) from a
+ The issue is that we derive two specialized types (ety and rty) from a
polymorphic type (ty). Because of this, there are typing issues with
[visit_'r] if we define a class which visits objects of types [ety] and [rty]
while inheriting a class which visit [ty]...
@@ -392,6 +369,7 @@ let ty_substitute_ids (tsubst : T.TypeVarId.id -> T.TypeVarId.id) (ty : 'r T.ty)
let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
(rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
(tsubst : T.TypeVarId.id -> T.TypeVarId.id)
+ (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
(ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
(bsubst : V.BorrowId.id -> V.BorrowId.id)
(asubst : V.AbstractionId.id -> V.AbstractionId.id) =
@@ -403,6 +381,7 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
match r with T.Static -> T.Static | T.Var rid -> T.Var (rsubst rid)
method! visit_type_var_id _ id = tsubst id
+ method! visit_const_generic_var_id _ id = cgsubst id
end
in
@@ -411,7 +390,7 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
inherit [_] C.map_env
method! visit_borrow_id _ bid = bsubst bid
method! visit_loan_id _ bid = bsubst bid
- method! visit_ety _ ty = ty_substitute_ids tsubst ty
+ method! visit_ety _ ty = ty_substitute_ids tsubst cgsubst ty
method! visit_rty env ty = subst_rty#visit_ty env ty
method! visit_symbolic_value_id _ id = ssubst id
@@ -444,11 +423,12 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
let typed_value_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
(rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
(tsubst : T.TypeVarId.id -> T.TypeVarId.id)
+ (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
(ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
(bsubst : V.BorrowId.id -> V.BorrowId.id) (v : V.typed_value) :
V.typed_value =
let asubst _ = raise (Failure "Unreachable") in
- (subst_ids_visitor rsubst rvsubst tsubst ssubst bsubst asubst)
+ (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst)
#visit_typed_value v
let typed_value_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
@@ -458,33 +438,39 @@ let typed_value_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
(fun x -> x)
(fun x -> x)
(fun x -> x)
+ (fun x -> x)
v
let typed_avalue_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
(rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
(tsubst : T.TypeVarId.id -> T.TypeVarId.id)
+ (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
(ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
(bsubst : V.BorrowId.id -> V.BorrowId.id) (v : V.typed_avalue) :
V.typed_avalue =
let asubst _ = raise (Failure "Unreachable") in
- (subst_ids_visitor rsubst rvsubst tsubst ssubst bsubst asubst)
+ (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst)
#visit_typed_avalue v
let abs_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
(rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
(tsubst : T.TypeVarId.id -> T.TypeVarId.id)
+ (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
(ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
(bsubst : V.BorrowId.id -> V.BorrowId.id)
(asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : V.abs) : V.abs =
- (subst_ids_visitor rsubst rvsubst tsubst ssubst bsubst asubst)#visit_abs x
+ (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst)
+ #visit_abs x
let env_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
(rvsubst : T.RegionVarId.id -> T.RegionVarId.id)
(tsubst : T.TypeVarId.id -> T.TypeVarId.id)
+ (cgsubst : T.ConstGenericVarId.id -> T.ConstGenericVarId.id)
(ssubst : V.SymbolicValueId.id -> V.SymbolicValueId.id)
(bsubst : V.BorrowId.id -> V.BorrowId.id)
(asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : C.env) : C.env =
- (subst_ids_visitor rsubst rvsubst tsubst ssubst bsubst asubst)#visit_env x
+ (subst_ids_visitor rsubst rvsubst tsubst cgsubst ssubst bsubst asubst)
+ #visit_env x
let typed_avalue_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
(x : V.typed_avalue) : V.typed_avalue =
@@ -494,6 +480,7 @@ let typed_avalue_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
(fun x -> x)
(fun x -> x)
(fun x -> x)
+ (fun x -> x)
asubst)
#visit_typed_avalue
x
@@ -505,6 +492,7 @@ let env_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id) (x : C.env) : C.env
(fun x -> x)
(fun x -> x)
(fun x -> x)
+ (fun x -> x)
(fun x -> x))
#visit_env
x
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 6668c043..a6e11363 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -32,7 +32,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
(* Match on the symbolic value type to know which can of expansion happened *)
let expansion =
match sv.V.sv_ty with
- | T.Bool -> (
+ | T.Literal PV.Bool -> (
(* Boolean expansion: there should be two branches *)
match ls with
| [
@@ -41,7 +41,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
] ->
ExpandBool (true_exp, false_exp)
| _ -> raise (Failure "Ill-formed boolean expansion"))
- | T.Integer int_ty ->
+ | T.Literal (PV.Integer int_ty) ->
(* Switch over an integer: split between the "regular" branches
and the "otherwise" branch (which should be the last branch) *)
let branches, otherwise = C.List.pop_last ls in
@@ -64,7 +64,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
assert (otherwise_see = None);
(* Return *)
ExpandInt (int_ty, branches, otherwise)
- | T.Adt (_, _, _) ->
+ | T.Adt (_, _, _, _) ->
(* Branching: it is necessarily an enumeration expansion *)
let get_variant (see : V.symbolic_expansion option) :
T.VariantId.id option * V.symbolic_value list =
@@ -85,7 +85,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
match ls with
| [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
| _ -> raise (Failure "Ill-formed borrow expansion"))
- | T.TypeVar _ | Char | Never | Str | Array _ | Slice _ ->
+ | T.TypeVar _ | T.Literal Char | Never ->
raise (Failure "Ill-formed symbolic expansion")
in
Some (Expansion (place, sv, expansion))
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index db6d3b98..b4bb0386 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -122,7 +122,7 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
let rec analyze (expl_info : expl_info) (ty_info : partial_type_info)
(ty : 'r ty) : partial_type_info =
match ty with
- | Bool | Char | Never | Integer _ | Str -> ty_info
+ | Literal _ | Never -> ty_info
| TypeVar var_id -> (
(* Update the information for the proper parameter, if necessary *)
match ty_info.param_infos with
@@ -145,9 +145,6 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
in
let param_infos = Some param_infos in
{ ty_info with param_infos })
- | Array ty | Slice ty ->
- (* Just dive in *)
- analyze expl_info ty_info ty
| Ref (r, rty, rkind) ->
(* Update the type info *)
let contains_static = r_is_static r in
@@ -172,12 +169,14 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
in
(* Continue exploring *)
analyze expl_info ty_info rty
- | Adt ((Tuple | Assumed (Box | Vec | Option)), _, tys) ->
+ | Adt
+ ((Tuple | Assumed (Box | Vec | Option | Slice | Array | Str)), _, tys, _)
+ ->
(* Nothing to update: just explore the type parameters *)
List.fold_left
(fun ty_info ty -> analyze expl_info ty_info ty)
ty_info tys
- | Adt (AdtId adt_id, regions, tys) ->
+ | Adt (AdtId adt_id, regions, tys, _cgs) ->
(* Lookup the information for this type definition *)
let adt_info = TypeDeclId.Map.find adt_id infos in
(* Update the type info with the information from the adt *)
diff --git a/compiler/Values.ml b/compiler/Values.ml
index d4eff58a..3d6bc9c1 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -14,7 +14,7 @@ module LoopId = IdGen ()
type big_int = PrimitiveValues.big_int [@@deriving show, ord]
type scalar_value = PrimitiveValues.scalar_value [@@deriving show, ord]
-type primitive_value = PrimitiveValues.primitive_value [@@deriving show, ord]
+type literal = PrimitiveValues.literal [@@deriving show, ord]
type symbolic_value_id = SymbolicValueId.id [@@deriving show, ord]
type symbolic_value_id_set = SymbolicValueId.Set.t [@@deriving show, ord]
type loop_id = LoopId.id [@@deriving show, ord]
@@ -110,10 +110,7 @@ type loan_id_set = BorrowId.Set.t [@@deriving show, ord]
class ['self] iter_typed_value_base =
object (self : 'self)
inherit [_] iter_symbolic_value
-
- method visit_primitive_value : 'env -> primitive_value -> unit =
- fun _ _ -> ()
-
+ method visit_literal : 'env -> literal -> unit = fun _ _ -> ()
method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
method visit_variant_id : 'env -> variant_id -> unit = fun _ _ -> ()
method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
@@ -131,9 +128,7 @@ class ['self] iter_typed_value_base =
class ['self] map_typed_value_base =
object (self : 'self)
inherit [_] map_symbolic_value
-
- method visit_primitive_value : 'env -> primitive_value -> primitive_value =
- fun _ cv -> cv
+ method visit_literal : 'env -> literal -> literal = fun _ cv -> cv
method visit_erased_region : 'env -> erased_region -> erased_region =
fun _ r -> r
@@ -152,7 +147,7 @@ class ['self] map_typed_value_base =
(** An untyped value, used in the environments *)
type value =
- | Primitive of primitive_value (** Non-symbolic primitive value *)
+ | Primitive of literal (** Non-symbolic primitive value *)
| Adt of adt_value (** Enumerations and structures *)
| Bottom (** No value (uninitialized or moved value) *)
| Borrow of borrow_content (** A borrowed value *)
@@ -1019,7 +1014,7 @@ type abs = {
TODO: this should rather be name "expanded_symbolic"
*)
type symbolic_expansion =
- | SePrimitive of primitive_value
+ | SePrimitive of literal
| SeAdt of (VariantId.id option * symbolic_value list)
| SeMutRef of BorrowId.id * symbolic_value
| SeSharedRef of BorrowId.Set.t * symbolic_value
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 15:09:16 +0000