summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Assumed.ml254
-rw-r--r--compiler/Config.ml7
-rw-r--r--compiler/Extract.ml753
-rw-r--r--compiler/ExtractAssumed.ml61
-rw-r--r--compiler/ExtractBase.ml405
-rw-r--r--compiler/ExtractBuiltin.ml560
-rw-r--r--compiler/FunsAnalysis.ml2
-rw-r--r--compiler/InterpreterExpansion.ml15
-rw-r--r--compiler/InterpreterExpressions.ml100
-rw-r--r--compiler/InterpreterPaths.ml31
-rw-r--r--compiler/InterpreterPaths.mli4
-rw-r--r--compiler/InterpreterStatements.ml107
-rw-r--r--compiler/Invariants.ml15
-rw-r--r--compiler/LlbcAstUtils.ml8
-rw-r--r--compiler/PrePasses.ml2
-rw-r--r--compiler/Print.ml11
-rw-r--r--compiler/PrintPure.ml57
-rw-r--r--compiler/Pure.ml12
-rw-r--r--compiler/PureMicroPasses.ml44
-rw-r--r--compiler/PureTypeCheck.ml13
-rw-r--r--compiler/Substitute.ml14
-rw-r--r--compiler/SymbolicToPure.ml31
-rw-r--r--compiler/Translate.ml327
-rw-r--r--compiler/TypesAnalysis.ml4
-rw-r--r--compiler/dune2
25 files changed, 1477 insertions, 1362 deletions
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index b1ec0660..94fb7a72 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -80,8 +80,6 @@ module Sig = struct
let mk_slice_ty (ty : T.sty) : T.sty =
Adt (Assumed Slice, mk_generic_args [] [ ty ] [])
- let range_ty : T.sty = Adt (Assumed Range, mk_generic_args [] [ usize_ty ] [])
-
let mk_sig generics regions_hierarchy inputs output : A.fun_sig =
let preds : T.predicates =
{ regions_outlive = []; types_outlive = []; trait_type_constraints = [] }
@@ -95,19 +93,6 @@ module Sig = struct
output;
}
- (** [fn<T>(&'a mut T, T) -> T] *)
- let mem_replace_sig : A.fun_sig =
- (* The signature fields *)
- let regions = [ region_param_0 ] (* <'a> *) in
- let regions_hierarchy = [ region_group_0 ] (* [{<'a>}] *) in
- let types = [ type_param_0 ] (* <T> *) in
- let generics = mk_generic_params regions types [] in
- let inputs =
- [ mk_ref_ty rvar_0 tvar_0 true (* &'a mut T *); tvar_0 (* T *) ]
- in
- let output = tvar_0 (* T *) in
- mk_sig generics regions_hierarchy inputs output
-
(** [fn<T>(T) -> Box<T>] *)
let box_new_sig : A.fun_sig =
let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in
@@ -124,101 +109,6 @@ module Sig = struct
let output = mk_unit_ty (* () *) in
mk_sig generics regions_hierarchy inputs output
- (** Helper for [Box::deref_shared] and [Box::deref_mut].
- Returns:
- [fn<'a, T>(&'a (mut) Box<T>) -> &'a (mut) T]
- *)
- let box_deref_gen_sig (is_mut : bool) : A.fun_sig =
- let generics =
- mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
- in
- let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
- let inputs =
- [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box<T> *) ]
- in
- let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in
- mk_sig generics regions_hierarchy inputs output
-
- (** [fn<'a, T>(&'a Box<T>) -> &'a T] *)
- let box_deref_shared_sig = box_deref_gen_sig false
-
- (** [fn<'a, T>(&'a mut Box<T>) -> &'a mut T] *)
- let box_deref_mut_sig = box_deref_gen_sig true
-
- (** [fn<T>() -> Vec<T>] *)
- let vec_new_sig : A.fun_sig =
- let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in
- let regions_hierarchy = [] in
- let inputs = [] in
- let output = mk_vec_ty tvar_0 (* Vec<T> *) in
- mk_sig generics regions_hierarchy inputs output
-
- (** [fn<T>(&'a mut Vec<T>, T)] *)
- let vec_push_sig : A.fun_sig =
- let generics =
- mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
- in
- let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
- let inputs =
- [
- mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec<T> *);
- tvar_0 (* T *);
- ]
- in
- let output = mk_unit_ty (* () *) in
- mk_sig generics regions_hierarchy inputs output
-
- (** [fn<T>(&'a mut Vec<T>, usize, T)] *)
- let vec_insert_sig : A.fun_sig =
- let generics =
- mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
- in
- let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
- let inputs =
- [
- mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec<T> *);
- mk_usize_ty (* usize *);
- tvar_0 (* T *);
- ]
- in
- let output = mk_unit_ty (* () *) in
- mk_sig generics regions_hierarchy inputs output
-
- (** [fn<T>(&'a Vec<T>) -> usize] *)
- let vec_len_sig : A.fun_sig =
- let generics =
- mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
- in
- let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
- let inputs =
- [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) false (* &'a Vec<T> *) ]
- in
- let output = mk_usize_ty (* usize *) in
- mk_sig generics regions_hierarchy inputs output
-
- (** Helper:
- [fn<T>(&'a (mut) Vec<T>, usize) -> &'a (mut) T]
- *)
- let vec_index_gen_sig (is_mut : bool) : A.fun_sig =
- let generics =
- mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
- in
- let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
- let inputs =
- [
- mk_ref_ty rvar_0 (mk_vec_ty tvar_0) is_mut (* &'a (mut) Vec<T> *);
- mk_usize_ty (* usize *);
- ]
- in
- let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in
- mk_sig generics regions_hierarchy inputs output
-
- (** [fn<T>(&'a Vec<T>, usize) -> &'a T] *)
- let vec_index_shared_sig : A.fun_sig = vec_index_gen_sig false
-
- (** [fn<T>(&'a mut Vec<T>, usize) -> &'a mut T] *)
- let vec_index_mut_sig : A.fun_sig = vec_index_gen_sig true
-
(** Array/slice functions *)
(** Small helper.
@@ -281,23 +171,6 @@ module Sig = struct
let cgs = [ cg_param_0 ] in
mk_array_slice_borrow_sig cgs input_ty None output_ty is_mut
- let mk_array_slice_subslice_sig (is_array : bool) (is_mut : bool) : A.fun_sig
- =
- (* Array<T, N> *)
- let input_ty id =
- if is_array then mk_array_ty (T.TypeVar id) cgvar_0
- else mk_slice_ty (T.TypeVar id)
- in
- (* Range *)
- let index_ty = range_ty in
- (* Slice<T> *)
- let output_ty id = mk_slice_ty (T.TypeVar id) in
- let cgs = if is_array then [ cg_param_0 ] else [] in
- mk_array_slice_borrow_sig cgs input_ty (Some index_ty) output_ty is_mut
-
- let array_subslice_sig (is_mut : bool) =
- mk_array_slice_subslice_sig true is_mut
-
let array_repeat_sig =
let generics =
(* <T, N> *)
@@ -311,9 +184,6 @@ module Sig = struct
in
mk_sig generics regions_hierarchy inputs output
- let slice_subslice_sig (is_mut : bool) =
- mk_array_slice_subslice_sig false is_mut
-
(** Helper:
[fn<T>(&'a [T]) -> usize]
*)
@@ -329,7 +199,25 @@ module Sig = struct
mk_sig generics regions_hierarchy inputs output
end
-type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name
+type raw_assumed_fun_info =
+ A.assumed_fun_id * A.fun_sig * bool * name * bool list option
+
+type assumed_fun_info = {
+ fun_id : A.assumed_fun_id;
+ fun_sig : A.fun_sig;
+ can_fail : bool;
+ name : name;
+ keep_types : bool list option;
+ (** We may want to filter some type arguments.
+
+ For instance, all the `Vec` functions (and the `Vec` type itself) take
+ an `Allocator` type as argument, that we ignore.
+ *)
+}
+
+let mk_assumed_fun_info (raw : raw_assumed_fun_info) : assumed_fun_info =
+ let fun_id, fun_sig, can_fail, name, keep_types = raw in
+ { fun_id; fun_sig; can_fail; name; keep_types }
(** The list of assumed functions and all their information:
- their signature
@@ -342,96 +230,72 @@ type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name
a [usize], we have to make sure that vectors are bounded by the max usize.
As a consequence, [Vec::push] is monadic.
*)
-let assumed_infos : assumed_info list =
- let deref_pre = [ "core"; "ops"; "deref" ] in
- let vec_pre = [ "alloc"; "vec"; "Vec" ] in
- let index_pre = [ "core"; "ops"; "index" ] in
+let raw_assumed_fun_infos : raw_assumed_fun_info list =
[
- (Replace, Sig.mem_replace_sig, false, to_name [ "core"; "mem"; "replace" ]);
- (BoxNew, Sig.box_new_sig, false, to_name [ "alloc"; "boxed"; "Box"; "new" ]);
+ ( BoxNew,
+ Sig.box_new_sig,
+ false,
+ to_name [ "alloc"; "boxed"; "Box"; "new" ],
+ Some [ true; false ] );
+ (* BoxFree shouldn't be used *)
( BoxFree,
Sig.box_free_sig,
false,
- to_name [ "alloc"; "boxed"; "Box"; "free" ] );
- ( BoxDeref,
- Sig.box_deref_shared_sig,
- false,
- to_name (deref_pre @ [ "Deref"; "deref" ]) );
- ( BoxDerefMut,
- Sig.box_deref_mut_sig,
- false,
- to_name (deref_pre @ [ "DerefMut"; "deref_mut" ]) );
- (VecNew, Sig.vec_new_sig, false, to_name (vec_pre @ [ "new" ]));
- (VecPush, Sig.vec_push_sig, true, to_name (vec_pre @ [ "push" ]));
- (VecInsert, Sig.vec_insert_sig, true, to_name (vec_pre @ [ "insert" ]));
- (VecLen, Sig.vec_len_sig, false, to_name (vec_pre @ [ "len" ]));
- ( VecIndex,
- Sig.vec_index_shared_sig,
- true,
- to_name (index_pre @ [ "Index"; "index" ]) );
- ( VecIndexMut,
- Sig.vec_index_mut_sig,
- true,
- to_name (index_pre @ [ "IndexMut"; "index_mut" ]) );
+ to_name [ "alloc"; "boxed"; "Box"; "free" ],
+ Some [ true; false ] );
(* Array Index *)
( ArrayIndexShared,
Sig.array_index_sig false,
true,
- to_name [ "@ArrayIndexShared" ] );
- (ArrayIndexMut, Sig.array_index_sig true, true, to_name [ "@ArrayIndexMut" ]);
+ to_name [ "@ArrayIndexShared" ],
+ None );
+ ( ArrayIndexMut,
+ Sig.array_index_sig true,
+ true,
+ to_name [ "@ArrayIndexMut" ],
+ None );
(* Array to slice*)
( ArrayToSliceShared,
Sig.array_to_slice_sig false,
true,
- to_name [ "@ArrayToSliceShared" ] );
+ to_name [ "@ArrayToSliceShared" ],
+ None );
( ArrayToSliceMut,
Sig.array_to_slice_sig true,
true,
- to_name [ "@ArrayToSliceMut" ] );
- (* Array Subslice *)
- ( ArraySubsliceShared,
- Sig.array_subslice_sig false,
- true,
- to_name [ "@ArraySubsliceShared" ] );
- ( ArraySubsliceMut,
- Sig.array_subslice_sig true,
- true,
- to_name [ "@ArraySubsliceMut" ] );
+ to_name [ "@ArrayToSliceMut" ],
+ None );
(* Array Repeat *)
- (ArrayRepeat, Sig.array_repeat_sig, false, to_name [ "@ArrayRepeat" ]);
+ (ArrayRepeat, Sig.array_repeat_sig, false, to_name [ "@ArrayRepeat" ], None);
(* Slice Index *)
( SliceIndexShared,
Sig.slice_index_sig false,
true,
- to_name [ "@SliceIndexShared" ] );
- (SliceIndexMut, Sig.slice_index_sig true, true, to_name [ "@SliceIndexMut" ]);
- (* Slice Subslice *)
- ( SliceSubsliceShared,
- Sig.slice_subslice_sig false,
+ to_name [ "@SliceIndexShared" ],
+ None );
+ ( SliceIndexMut,
+ Sig.slice_index_sig true,
true,
- to_name [ "@SliceSubsliceShared" ] );
- ( SliceSubsliceMut,
- Sig.slice_subslice_sig true,
- true,
- to_name [ "@SliceSubsliceMut" ] );
- (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ]);
+ to_name [ "@SliceIndexMut" ],
+ None );
+ (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ], None);
]
-let get_assumed_info (id : A.assumed_fun_id) : assumed_info =
- match List.find_opt (fun (id', _, _, _) -> id = id') assumed_infos with
+let assumed_fun_infos : assumed_fun_info list =
+ List.map mk_assumed_fun_info raw_assumed_fun_infos
+
+let get_assumed_fun_info (id : A.assumed_fun_id) : assumed_fun_info =
+ match List.find_opt (fun x -> id = x.fun_id) assumed_fun_infos with
| Some info -> info
| None ->
raise
- (Failure ("get_assumed_info: not found: " ^ A.show_assumed_fun_id id))
+ (Failure ("get_assumed_fun_info: not found: " ^ A.show_assumed_fun_id id))
-let get_assumed_sig (id : A.assumed_fun_id) : A.fun_sig =
- let _, sg, _, _ = get_assumed_info id in
- sg
+let get_assumed_fun_sig (id : A.assumed_fun_id) : A.fun_sig =
+ (get_assumed_fun_info id).fun_sig
-let get_assumed_name (id : A.assumed_fun_id) : fun_name =
- let _, _, _, name = get_assumed_info id in
- name
+let get_assumed_fun_name (id : A.assumed_fun_id) : fun_name =
+ (get_assumed_fun_info id).name
-let assumed_can_fail (id : A.assumed_fun_id) : bool =
- let _, _, b, _ = get_assumed_info id in
- b
+let assumed_fun_can_fail (id : A.assumed_fun_id) : bool =
+ (get_assumed_fun_info id).can_fail
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 62f6c300..cd0903b6 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -306,13 +306,6 @@ let filter_useless_monadic_calls = ref true
*)
let filter_useless_functions = ref true
-(** Obsolete. TODO: remove.
-
- For Lean we used to parameterize the entire development by a section variable
- called opaque_defs, of type OpaqueDefs.
- *)
-let wrap_opaque_in_sig = ref false
-
(** Use short names for the record fields.
Some backends can't disambiguate records when their field names have collisions.
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index e24cae16..91827a31 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -229,12 +229,9 @@ let assumed_adts () : (assumed_ty * string) list =
(Result, "Result");
(Error, "Error");
(Fuel, "Nat");
- (Option, "Option");
- (Vec, "Vec");
(Array, "Array");
(Slice, "Slice");
(Str, "Str");
- (Range, "Range");
]
| Coq | FStar ->
[
@@ -242,12 +239,9 @@ let assumed_adts () : (assumed_ty * string) list =
(Result, "result");
(Error, "error");
(Fuel, "nat");
- (Option, "option");
- (Vec, "vec");
(Array, "array");
(Slice, "slice");
(Str, "str");
- (Range, "range");
]
| HOL4 ->
[
@@ -255,20 +249,17 @@ let assumed_adts () : (assumed_ty * string) list =
(Result, "result");
(Error, "error");
(Fuel, "num");
- (Option, "option");
- (Vec, "vec");
(Array, "array");
(Slice, "slice");
(Str, "str");
- (Range, "range");
]
let assumed_struct_constructors () : (assumed_ty * string) list =
match !backend with
- | Lean -> [ (Range, "Range.mk"); (Array, "Array.make") ]
- | Coq -> [ (Range, "mk_range"); (Array, "mk_array") ]
- | FStar -> [ (Range, "Mkrange"); (Array, "mk_array") ]
- | HOL4 -> [ (Range, "mk_range"); (Array, "mk_array") ]
+ | Lean -> [ (Array, "Array.make") ]
+ | Coq -> [ (Array, "mk_array") ]
+ | FStar -> [ (Array, "mk_array") ]
+ | HOL4 -> [ (Array, "mk_array") ]
let assumed_variants () : (assumed_ty * VariantId.id * string) list =
match !backend with
@@ -280,8 +271,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
(Error, error_out_of_fuel_id, "OutOfFuel");
(* No Fuel::Zero on purpose *)
(* No Fuel::Succ on purpose *)
- (Option, option_some_id, "Some");
- (Option, option_none_id, "None");
]
| Coq ->
[
@@ -291,8 +280,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
(Error, error_out_of_fuel_id, "OutOfFuel");
(Fuel, fuel_zero_id, "O");
(Fuel, fuel_succ_id, "S");
- (Option, option_some_id, "Some");
- (Option, option_none_id, "None");
]
| Lean ->
[
@@ -301,8 +288,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
(Error, error_failure_id, "panic");
(* No Fuel::Zero on purpose *)
(* No Fuel::Succ on purpose *)
- (Option, option_some_id, "some");
- (Option, option_none_id, "none");
]
| HOL4 ->
[
@@ -311,8 +296,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
(Error, error_failure_id, "Failure");
(* No Fuel::Zero on purpose *)
(* No Fuel::Succ on purpose *)
- (Option, option_some_id, "SOME");
- (Option, option_none_id, "NONE");
]
let assumed_llbc_functions () :
@@ -321,66 +304,30 @@ let assumed_llbc_functions () :
match !backend with
| FStar | Coq | HOL4 ->
[
- (Replace, None, "mem_replace_fwd");
- (Replace, rg0, "mem_replace_back");
- (VecNew, None, "vec_new");
- (VecPush, None, "vec_push_fwd") (* Shouldn't be used *);
- (VecPush, rg0, "vec_push_back");
- (VecInsert, None, "vec_insert_fwd") (* Shouldn't be used *);
- (VecInsert, rg0, "vec_insert_back");
- (VecLen, None, "vec_len");
- (VecIndex, None, "vec_index_fwd");
- (VecIndex, rg0, "vec_index_back") (* shouldn't be used *);
- (VecIndexMut, None, "vec_index_mut_fwd");
- (VecIndexMut, rg0, "vec_index_mut_back");
(ArrayIndexShared, None, "array_index_shared");
(ArrayIndexMut, None, "array_index_mut_fwd");
(ArrayIndexMut, rg0, "array_index_mut_back");
(ArrayToSliceShared, None, "array_to_slice_shared");
(ArrayToSliceMut, None, "array_to_slice_mut_fwd");
(ArrayToSliceMut, rg0, "array_to_slice_mut_back");
- (ArraySubsliceShared, None, "array_subslice_shared");
- (ArraySubsliceMut, None, "array_subslice_mut_fwd");
- (ArraySubsliceMut, rg0, "array_subslice_mut_back");
(ArrayRepeat, None, "array_repeat");
(SliceIndexShared, None, "slice_index_shared");
(SliceIndexMut, None, "slice_index_mut_fwd");
(SliceIndexMut, rg0, "slice_index_mut_back");
- (SliceSubsliceShared, None, "slice_subslice_shared");
- (SliceSubsliceMut, None, "slice_subslice_mut_fwd");
- (SliceSubsliceMut, rg0, "slice_subslice_mut_back");
(SliceLen, None, "slice_len");
]
| Lean ->
[
- (Replace, None, "mem.replace");
- (Replace, rg0, "mem.replace_back");
- (VecNew, None, "Vec.new");
- (VecPush, None, "Vec.push_fwd") (* Shouldn't be used *);
- (VecPush, rg0, "Vec.push");
- (VecInsert, None, "Vec.insert_fwd") (* Shouldn't be used *);
- (VecInsert, rg0, "Vec.insert");
- (VecLen, None, "Vec.len");
- (VecIndex, None, "Vec.index_shared");
- (VecIndex, rg0, "Vec.index_shared_back") (* shouldn't be used *);
- (VecIndexMut, None, "Vec.index_mut");
- (VecIndexMut, rg0, "Vec.index_mut_back");
(ArrayIndexShared, None, "Array.index_shared");
(ArrayIndexMut, None, "Array.index_mut");
(ArrayIndexMut, rg0, "Array.index_mut_back");
(ArrayToSliceShared, None, "Array.to_slice_shared");
(ArrayToSliceMut, None, "Array.to_slice_mut");
(ArrayToSliceMut, rg0, "Array.to_slice_mut_back");
- (ArraySubsliceShared, None, "Array.subslice_shared");
- (ArraySubsliceMut, None, "Array.subslice_mut");
- (ArraySubsliceMut, rg0, "Array.subslice_mut_back");
(ArrayRepeat, None, "Array.repeat");
(SliceIndexShared, None, "Slice.index_shared");
(SliceIndexMut, None, "Slice.index_mut");
(SliceIndexMut, rg0, "Slice.index_mut_back");
- (SliceSubsliceShared, None, "Slice.subslice_shared");
- (SliceSubsliceMut, None, "Slice.subslice_mut");
- (SliceSubsliceMut, rg0, "Slice.subslice_mut_back");
(SliceLen, None, "Slice.len");
]
@@ -814,12 +761,6 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
fname ^ lp_suffix ^ suffix
in
- let opaque_pre () =
- match !Config.backend with
- | FStar | Coq | HOL4 -> ""
- | Lean -> if !Config.wrap_opaque_in_sig then "opaque_defs." else ""
- in
-
let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
: string =
(* Small helper to derive var names from ADT type names.
@@ -853,12 +794,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
| Assumed Result -> "r"
| Assumed Error -> ConstStrings.error_basename
| Assumed Fuel -> ConstStrings.fuel_basename
- | Assumed Option -> "opt"
- | Assumed Vec -> "v"
| Assumed Array -> "a"
| Assumed Slice -> "s"
| Assumed Str -> "s"
- | Assumed Range -> "r"
| Assumed State -> ConstStrings.state_basename
| AdtId adt_id ->
let def = TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls in
@@ -927,10 +865,12 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
(* We need to add parentheses if the value is negative *)
if sv.PV.value >= Z.of_int 0 then
F.pp_print_string fmt (Z.to_string sv.PV.value)
- else
+ else if !backend = Lean then
+ (* TODO: parsing issues with Lean because there are ambiguous
+ interpretations between int values and nat values *)
F.pp_print_string fmt
- ("(" ^ Z.to_string sv.PV.value
- ^ if !backend = Lean then ":Int" else "" ^ ")");
+ ("(-(" ^ Z.to_string (Z.neg sv.PV.value) ^ ":Int))")
+ else F.pp_print_string fmt ("(" ^ Z.to_string sv.PV.value ^ ")");
(match !backend with
| Coq ->
let iname = int_name sv.PV.int_ty in
@@ -993,7 +933,6 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
trait_type_name;
trait_method_name;
trait_type_clause_name;
- opaque_pre;
var_basename;
type_var_basename;
const_generic_var_basename;
@@ -1042,11 +981,8 @@ let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
(* In HOL4, opaque functions have a special treatment *)
if is_single_opaque_fun_decl_group dg then ()
else
- let with_opaque_pre = false in
let compute_fun_def_name (def : Pure.fun_decl) : string =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id
- def.back_id ctx
- ^ "_def"
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx ^ "_def"
in
let names = List.map compute_fun_def_name dg in
(* Add a break before *)
@@ -1169,7 +1105,7 @@ let extract_const_generic (ctx : extraction_ctx) (fmt : F.formatter)
(inside : bool) (cg : const_generic) : unit =
match cg with
| ConstGenericGlobal id ->
- let s = ctx_get_global ctx.use_opaque_pre id ctx in
+ let s = ctx_get_global id ctx in
F.pp_print_string fmt s
| ConstGenericValue v -> ctx.fmt.extract_literal fmt inside v
| ConstGenericVar id ->
@@ -1237,14 +1173,33 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
In HOL4 we would write:
`('a, 'b) tree`
*)
- let with_opaque_pre = false in
match !backend with
| FStar | Coq | Lean ->
let print_paren = inside && has_params in
if print_paren then F.pp_print_string fmt "(";
(* TODO: for now, only the opaque *functions* are extracted in the
opaque module. The opaque *types* are assumed. *)
- F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx);
+ F.pp_print_string fmt (ctx_get_type type_id ctx);
+ (* We might need to filter the type arguments, if the type
+ is builtin (for instance, we filter the global allocator type
+ argument for `Vec`). *)
+ let generics =
+ match type_id with
+ | AdtId id -> (
+ match
+ TypeDeclId.Map.find_opt id ctx.types_filter_type_args_map
+ with
+ | None -> generics
+ | Some filter ->
+ let types = List.combine filter generics.types in
+ let types =
+ List.filter_map
+ (fun (b, ty) -> if b then Some ty else None)
+ types
+ in
+ { generics with types })
+ | _ -> generics
+ in
extract_generic_args ctx fmt no_params_tys generics;
if print_paren then F.pp_print_string fmt ")"
| HOL4 ->
@@ -1267,7 +1222,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
(extract_rec true) types;
if print_paren then F.pp_print_string fmt ")";
F.pp_print_space fmt ());
- F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx);
+ F.pp_print_string fmt (ctx_get_type type_id ctx);
if trait_refs <> [] then (
F.pp_print_space fmt ();
Collections.List.iter_link (F.pp_print_space fmt)
@@ -1332,11 +1287,13 @@ and extract_trait_decl_ref (ctx : extraction_ctx) (fmt : F.formatter)
(no_params_tys : TypeDeclId.Set.t) (inside : bool) (tr : trait_decl_ref) :
unit =
let use_brackets = tr.decl_generics <> empty_generic_args && inside in
- let is_opaque = false in
- let name = ctx_get_trait_decl is_opaque tr.trait_decl_id ctx in
+ let name = ctx_get_trait_decl tr.trait_decl_id ctx in
if use_brackets then F.pp_print_string fmt "(";
F.pp_print_string fmt name;
- extract_generic_args ctx fmt no_params_tys tr.decl_generics;
+ (* There is something subtle here: the trait obligations for the implemented
+ trait are put inside the parent clauses, so we must ignore them here *)
+ let generics = { tr.decl_generics with trait_refs = [] } in
+ extract_generic_args ctx fmt no_params_tys generics;
if use_brackets then F.pp_print_string fmt ")"
and extract_generic_args (ctx : extraction_ctx) (fmt : F.formatter)
@@ -1363,14 +1320,13 @@ and extract_generic_args (ctx : extraction_ctx) (fmt : F.formatter)
and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter)
(no_params_tys : TypeDeclId.Set.t) (inside : bool) (id : trait_instance_id)
: unit =
- let with_opaque_pre = false in
match id with
| Self ->
(* This has specific treatment depending on the item we're extracting
(associated type, etc.). We should have caught this elsewhere. *)
raise (Failure "Unexpected")
| TraitImpl id ->
- let name = ctx_get_trait_impl with_opaque_pre id ctx in
+ let name = ctx_get_trait_impl id ctx in
F.pp_print_string fmt name
| Clause id ->
let name = ctx_get_local_trait_clause id ctx in
@@ -1400,8 +1356,28 @@ and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter)
*)
let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
extraction_ctx =
+ (* Lookup the builtin information, if there is *)
+ let open ExtractBuiltin in
+ let sname = name_to_simple_name def.name in
+ let info = SimpleNameMap.find_opt sname (builtin_types_map ()) in
+ (* Register the filtering information, if there is *)
+ let ctx =
+ match info with
+ | Some { keep_params = Some keep; _ } ->
+ {
+ ctx with
+ types_filter_type_args_map =
+ TypeDeclId.Map.add def.def_id keep ctx.types_filter_type_args_map;
+ }
+ | _ -> ctx
+ in
(* Compute and register the type def name *)
- let ctx = ctx_add_type_decl def ctx in
+ let def_name =
+ match info with
+ | None -> ctx.fmt.type_name def.name
+ | Some info -> String.concat "." info.rust_name
+ in
+ let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in
(* Compute and register:
* - the variant names, if this is an enumeration
* - the field names, if this is a structure
@@ -1409,18 +1385,77 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
let ctx =
match def.kind with
| Struct fields ->
+ (* Compute the names *)
+ let field_names, cons_name =
+ match info with
+ | None | Some { body_info = None; _ } ->
+ let field_names =
+ FieldId.mapi
+ (fun fid (field : field) ->
+ (fid, ctx.fmt.field_name def.name fid field.field_name))
+ fields
+ in
+ let cons_name = ctx.fmt.struct_constructor def.name in
+ (field_names, cons_name)
+ | Some { body_info = Some (Struct (cons_name, field_names)); _ } ->
+ let field_names =
+ FieldId.mapi
+ (fun fid (_, name) -> (fid, name))
+ (List.combine fields field_names)
+ in
+ (field_names, cons_name)
+ | Some info ->
+ raise
+ (Failure
+ ("Invalid builtin information: "
+ ^ show_builtin_type_info info))
+ in
(* Add the fields *)
let ctx =
- fst
- (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx)
+ List.fold_left
+ (fun ctx (fid, name) ->
+ ctx_add (FieldId (AdtId def.def_id, fid)) name ctx)
+ ctx field_names
in
(* Add the constructor name *)
- fst (ctx_add_struct def ctx)
+ ctx_add (StructId (AdtId def.def_id)) cons_name ctx
| Enum variants ->
- fst
- (ctx_add_variants def
- (VariantId.mapi (fun id v -> (id, v)) variants)
- ctx)
+ let variant_names =
+ match info with
+ | None ->
+ VariantId.mapi
+ (fun variant_id (variant : variant) ->
+ let name =
+ ctx.fmt.variant_name def.name variant.variant_name
+ in
+ (* Add the type name prefix for Lean *)
+ let name =
+ if !Config.backend = Lean then
+ let type_name = ctx.fmt.type_name def.name in
+ type_name ^ "." ^ name
+ else name
+ in
+ (variant_id, name))
+ variants
+ | Some { body_info = Some (Enum variant_infos); _ } ->
+ (* We need to compute the map from variant to variant *)
+ let variant_map =
+ StringMap.of_list
+ (List.map
+ (fun (info : builtin_enum_variant_info) ->
+ (info.rust_variant_name, info.extract_variant_name))
+ variant_infos)
+ in
+ VariantId.mapi
+ (fun variant_id (variant : variant) ->
+ (variant_id, StringMap.find variant.variant_name variant_map))
+ variants
+ | _ -> raise (Failure "Invalid builtin information")
+ in
+ List.fold_left
+ (fun ctx (vid, vname) ->
+ ctx_add (VariantId (AdtId def.def_id, vid)) vname ctx)
+ ctx variant_names
| Opaque ->
(* Nothing to do *)
ctx
@@ -1622,9 +1657,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(* If Coq: print the constructor name *)
(* TODO: remove superfluous test not is_rec below *)
if !backend = Coq && not is_rec then (
- let with_opaque_pre = false in
- F.pp_print_string fmt
- (ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx);
+ F.pp_print_string fmt (ctx_get_struct (AdtId def.def_id) ctx);
F.pp_print_string fmt " ");
(match !backend with
| Lean -> ()
@@ -1668,16 +1701,14 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(* We extract for Coq or Lean, and we have a recursive record, or a record in
a group of mutually recursive types: we extract it as an inductive type *)
assert (is_rec && (!backend = Coq || !backend = Lean));
- let with_opaque_pre = false in
(* Small trick: in Lean we use namespaces, meaning we don't need to prefix
the constructor name with the name of the type at definition site,
i.e., instead of generating `inductive Foo := | MkFoo ...` like in Coq
we generate `inductive Foo := | mk ... *)
let cons_name =
- if !backend = Lean then "mk"
- else ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx
+ if !backend = Lean then "mk" else ctx_get_struct (AdtId def.def_id) ctx
in
- let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+ let def_name = ctx_get_local_type def.def_id ctx in
extract_type_decl_variant ctx fmt type_decl_group def_name type_params
cg_params cons_name fields)
in
@@ -1707,8 +1738,7 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit =
let extract_trait_clause_type (ctx : extraction_ctx) (fmt : F.formatter)
(no_params_tys : TypeDeclId.Set.t) (clause : trait_clause) : unit =
- let with_opaque_pre = false in
- let trait_name = ctx_get_trait_decl with_opaque_pre clause.trait_id ctx in
+ let trait_name = ctx_get_trait_decl clause.trait_id ctx in
F.pp_print_string fmt trait_name;
extract_generic_args ctx fmt no_params_tys clause.generics
@@ -1730,8 +1760,7 @@ let extract_trait_self_clause (insert_req_space : unit -> unit)
F.pp_print_space fmt ();
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
- let with_opaque_pre = false in
- let trait_id = ctx_get_trait_decl with_opaque_pre trait_decl.def_id ctx in
+ let trait_id = ctx_get_trait_decl trait_decl.def_id ctx in
F.pp_print_string fmt trait_id;
List.iter
(fun p ->
@@ -1900,8 +1929,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
let is_opaque_coq = !backend = Coq && is_opaque in
let use_forall = is_opaque_coq && def.generics <> empty_generic_params in
(* Retrieve the definition name *)
- let with_opaque_pre = false in
- let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+ let def_name = ctx_get_local_type def.def_id ctx in
(* Add the type and const generic params - note that we need those bindings only for the
* body translation (they are not top-level) *)
let ctx_body, type_params, cg_params, trait_clauses =
@@ -1988,8 +2016,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
(def : type_decl) : unit =
(* Retrieve the definition name *)
- let with_opaque_pre = false in
- let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+ let def_name = ctx_get_local_type def.def_id ctx in
(* Generic parameters are unsupported *)
assert (def.generics.const_generics = []);
(* Trait clauses on type definitions are unsupported *)
@@ -2014,8 +2041,7 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
let extract_type_decl_hol4_empty_record (ctx : extraction_ctx)
(fmt : F.formatter) (def : type_decl) : unit =
(* Retrieve the definition name *)
- let with_opaque_pre = false in
- let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+ let def_name = ctx_get_local_type def.def_id ctx in
(* Sanity check *)
assert (def.generics = empty_generic_params);
(* Generate the declaration *)
@@ -2098,8 +2124,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
| Struct fields ->
let adt_id = AdtId decl.def_id in
(* Generate the instruction for the record constructor *)
- let with_opaque_pre = false in
- let cons_name = ctx_get_struct with_opaque_pre adt_id ctx in
+ let cons_name = ctx_get_struct adt_id ctx in
extract_arguments_info cons_name fields;
(* Generate the instruction for the record projectors, if there are *)
let is_rec = decl_is_from_rec_group kind in
@@ -2143,11 +2168,8 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
in
let ctx, record_var = ctx_add_var "x" (VarId.of_int 0) ctx in
let ctx, field_var = ctx_add_var "x" (VarId.of_int 1) ctx in
- let with_opaque_pre = false in
- let def_name = ctx_get_local_type with_opaque_pre decl.def_id ctx in
- let cons_name =
- ctx_get_struct with_opaque_pre (AdtId decl.def_id) ctx
- in
+ let def_name = ctx_get_local_type decl.def_id ctx in
+ let cons_name = ctx_get_struct (AdtId decl.def_id) ctx in
let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
F.pp_print_space fmt ();
(* Outer box for the projector definition *)
@@ -2359,33 +2381,81 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
let extract_fun_decl_register_names (ctx : extraction_ctx)
(has_decreases_clause : fun_decl -> bool) (def : pure_fun_translation) :
extraction_ctx =
- let fwd = def.fwd in
- let backs = def.backs in
- (* Register the decrease clauses, if necessary *)
- let register_decreases ctx def =
- if has_decreases_clause def then
- (* Add the termination measure *)
- let ctx = ctx_add_termination_measure def ctx in
- (* Add the decreases proof for Lean only *)
- match !Config.backend with
- | Coq | FStar -> ctx
- | HOL4 -> raise (Failure "Unexpected")
- | Lean -> ctx_add_decreases_proof def ctx
- else ctx
- in
- let ctx = List.fold_left register_decreases ctx (fwd.f :: fwd.loops) in
- let register_fun ctx f = ctx_add_fun_decl def f ctx in
- let register_funs ctx fl = List.fold_left register_fun ctx fl in
- (* Register the names of the forward functions *)
- let ctx =
- if def.keep_fwd then register_funs ctx (fwd.f :: fwd.loops) else ctx
- in
- (* Register the names of the backward functions *)
- List.fold_left
- (fun ctx { f = back; loops = loop_backs } ->
- let ctx = register_fun ctx back in
- register_funs ctx loop_backs)
- ctx backs
+ (* Ignore the trait methods **declarations** (rem.: we do not ignore the trait
+ method implementations): we do not need to refer to them directly. We will
+ only use their type for the fields of the records we generate for the trait
+ declarations *)
+ match def.fwd.f.kind with
+ | TraitMethodDecl _ -> ctx
+ | _ -> (
+ (* Check if the function is builtin *)
+ let builtin =
+ let open ExtractBuiltin in
+ let funs_map = builtin_funs_map () in
+ let sname = name_to_simple_name def.fwd.f.basename in
+ SimpleNameMap.find_opt sname funs_map
+ in
+ (* Use the builtin names if necessary *)
+ match builtin with
+ | Some (filter_info, info) ->
+ (* Register the filtering information, if there is *)
+ let ctx =
+ match filter_info with
+ | Some keep ->
+ {
+ ctx with
+ funs_filter_type_args_map =
+ FunDeclId.Map.add def.fwd.f.def_id keep
+ ctx.funs_filter_type_args_map;
+ }
+ | _ -> ctx
+ in
+ let backs = List.map (fun f -> f.f) def.backs in
+ let funs = if def.keep_fwd then def.fwd.f :: backs else backs in
+ List.fold_left
+ (fun ctx (f : fun_decl) ->
+ let open ExtractBuiltin in
+ let fun_id =
+ (Pure.FunId (Regular f.def_id), f.loop_id, f.back_id)
+ in
+ let fun_name =
+ (List.find
+ (fun (x : builtin_fun_info) -> x.rg = f.back_id)
+ info)
+ .extract_name
+ in
+ ctx_add (FunId (FromLlbc fun_id)) fun_name ctx)
+ ctx funs
+ | None ->
+ let fwd = def.fwd in
+ let backs = def.backs in
+ (* Register the decrease clauses, if necessary *)
+ let register_decreases ctx def =
+ if has_decreases_clause def then
+ (* Add the termination measure *)
+ let ctx = ctx_add_termination_measure def ctx in
+ (* Add the decreases proof for Lean only *)
+ match !Config.backend with
+ | Coq | FStar -> ctx
+ | HOL4 -> raise (Failure "Unexpected")
+ | Lean -> ctx_add_decreases_proof def ctx
+ else ctx
+ in
+ let ctx =
+ List.fold_left register_decreases ctx (fwd.f :: fwd.loops)
+ in
+ let register_fun ctx f = ctx_add_fun_decl def f ctx in
+ let register_funs ctx fl = List.fold_left register_fun ctx fl in
+ (* Register the names of the forward functions *)
+ let ctx =
+ if def.keep_fwd then register_funs ctx (fwd.f :: fwd.loops) else ctx
+ in
+ (* Register the names of the backward functions *)
+ List.fold_left
+ (fun ctx { f = back; loops = loop_backs } ->
+ let ctx = register_fun ctx back in
+ register_funs ctx loop_backs)
+ ctx backs)
(** Simply add the global name to the context. *)
let extract_global_decl_register_names (ctx : extraction_ctx)
@@ -2459,18 +2529,14 @@ let extract_adt_g_value
* [{ field0=...; ...; fieldn=...; }] in case of structures.
*)
let cons =
- (* The ADT shouldn't be opaque *)
- let with_opaque_pre = false in
match variant_id with
| Some vid -> (
(* In the case of Lean, we might have to add the type name as a prefix *)
match (!backend, adt_id) with
| Lean, Assumed _ ->
- ctx_get_type with_opaque_pre adt_id ctx
- ^ "."
- ^ ctx_get_variant adt_id vid ctx
+ ctx_get_type adt_id ctx ^ "." ^ ctx_get_variant adt_id vid ctx
| _ -> ctx_get_variant adt_id vid ctx)
- | None -> ctx_get_struct with_opaque_pre adt_id ctx
+ | None -> ctx_get_struct adt_id ctx
in
let use_parentheses = inside && field_values <> [] in
if use_parentheses then F.pp_print_string fmt "(";
@@ -2489,8 +2555,7 @@ let extract_adt_g_value
(* Extract globals in the same way as variables *)
let extract_global (ctx : extraction_ctx) (fmt : F.formatter)
(id : A.GlobalDeclId.id) : unit =
- let with_opaque_pre = ctx.use_opaque_pre in
- F.pp_print_string fmt (ctx_get_global with_opaque_pre id ctx)
+ F.pp_print_string fmt (ctx_get_global id ctx)
(** [inside]: see {!extract_ty}.
@@ -2626,9 +2691,9 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
if inside then F.pp_print_string fmt "(";
(* Open a box for the function call *)
F.pp_open_hovbox fmt ctx.indent_incr;
- (* Print the function name *)
- let with_opaque_pre = ctx.use_opaque_pre in
- (* For the function name: the id is not the same depending on whether
+ (* Print the function name.
+
+ For the function name: the id is not the same depending on whether
we call a trait method and a "regular" function (remark: trait
method *implementations* are considered as regular functions here;
only calls to method of traits which are parameterized in a where
@@ -2701,7 +2766,7 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
let fun_id =
FromLlbc (FunId (Regular method_id.id), lp_id, rg_id)
in
- let fun_name = ctx_get_function with_opaque_pre fun_id ctx in
+ let fun_name = ctx_get_function fun_id ctx in
F.pp_print_string fmt fun_name;
(* Note that we do not need to print the generics for the trait
@@ -2712,12 +2777,32 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
extract_trait_ref ctx fmt TypeDeclId.Set.empty true trait_ref
| _ ->
- let fun_name = ctx_get_function with_opaque_pre fun_id ctx in
+ let fun_name = ctx_get_function fun_id ctx in
F.pp_print_string fmt fun_name);
(* Sanity check: HOL4 doesn't support const generics *)
assert (generics.const_generics = [] || !backend <> HOL4);
- (* Print the generics *)
+ (* Print the generics.
+
+ We might need to filter some of the type arguments, if the type
+ is builtin (for instance, we filter the global allocator type
+ argument for `Vec::new`).
+ *)
+ let generics =
+ match fun_id with
+ | FromLlbc (FunId (Regular id), _, _) -> (
+ match FunDeclId.Map.find_opt id ctx.funs_filter_type_args_map with
+ | None -> generics
+ | Some filter ->
+ let types = List.combine filter generics.types in
+ let types =
+ List.filter_map
+ (fun (b, ty) -> if b then Some ty else None)
+ types
+ in
+ { generics with types })
+ | _ -> generics
+ in
extract_generic_args ctx fmt TypeDeclId.Set.empty generics;
(* Print the arguments *)
List.iter
@@ -3210,7 +3295,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
(* Open the box for `Array.replicate T N [` *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the array constructor *)
- let cs = ctx_get_struct false (Assumed Array) ctx in
+ let cs = ctx_get_struct (Assumed Array) ctx in
F.pp_print_string fmt cs;
(* Print the parameters *)
let _, generics = ty_as_adt e_ty in
@@ -3563,10 +3648,8 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
assert (not def.is_global_decl_body);
(* Retrieve the function name *)
- let with_opaque_pre = false in
let def_name =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id def.back_id
- ctx
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx
in
(* Add a break before *)
if !backend <> HOL4 || not (decl_is_first_from_group kind) then
@@ -3594,19 +3677,13 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
let use_forall =
is_opaque_coq && def.signature.generics <> empty_generic_params
in
- (* Print the qualifier ("assume", etc.).
-
- if `wrap_opaque_in_sig`: we generate a record of assumed funcions.
- TODO: this is obsolete.
- *)
- (if not (!Config.wrap_opaque_in_sig && (kind = Assumed || kind = Declared))
- then
- let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
- match qualif with
- | Some qualif ->
- F.pp_print_string fmt qualif;
- F.pp_print_space fmt ()
- | None -> ());
+ (* Print the qualifier ("assume", etc.). *)
+ let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
+ (match qualif with
+ | Some qualif ->
+ F.pp_print_string fmt qualif;
+ F.pp_print_space fmt ()
+ | None -> ());
F.pp_print_string fmt def_name;
F.pp_print_space fmt ();
if use_forall then (
@@ -3817,10 +3894,8 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
(def : fun_decl) : unit =
(* Retrieve the definition name *)
- let with_opaque_pre = false in
let def_name =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id def.back_id
- ctx
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx
in
assert (def.signature.generics.const_generics = []);
(* Add the type/const gen parameters - note that we need those bindings
@@ -4015,10 +4090,9 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
extract_comment fmt [ "[" ^ Print.global_name_to_string global.name ^ "]" ];
F.pp_print_space fmt ();
- let with_opaque_pre = false in
- let decl_name = ctx_get_global with_opaque_pre global.def_id ctx in
+ let decl_name = ctx_get_global global.def_id ctx in
let body_name =
- ctx_get_function with_opaque_pre
+ ctx_get_function
(FromLlbc (Pure.FunId (Regular global.body_id), None, None))
ctx
in
@@ -4056,73 +4130,263 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Add a break to insert lines between declarations *)
F.pp_print_break fmt 0 0
-(** Register the names for one trait method item *)
-let extract_trait_decl_method_register_names (ctx : extraction_ctx)
- (trait_decl : trait_decl) (name : string) (id : fun_decl_id) :
+(** Similar to {!extract_trait_decl_register_names} *)
+let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
+ (trait_decl : trait_decl)
+ (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
extraction_ctx =
- (* We add one field per required forward/backward function *)
- let trans = A.FunDeclId.Map.find id ctx.trans_funs in
-
- let register_fun ctx f = ctx_add_trait_method trait_decl name f.f ctx in
+ let generics = trait_decl.generics in
+ (* Compute the clause names *)
+ let clause_names =
+ match builtin_info with
+ | None ->
+ List.map
+ (fun (c : trait_clause) ->
+ let name = ctx.fmt.trait_parent_clause_name trait_decl c in
+ (* Add a prefix if necessary *)
+ let name =
+ if !Config.record_fields_short_names then name
+ else ctx.fmt.trait_decl_name trait_decl ^ name
+ in
+ (c.clause_id, name))
+ generics.trait_clauses
+ | Some info ->
+ List.map
+ (fun (c, name) -> (c.clause_id, name))
+ (List.combine generics.trait_clauses info.parent_clauses)
+ in
+ (* Register the names *)
+ List.fold_left
+ (fun ctx (cid, cname) ->
+ ctx_add (TraitParentClauseId (trait_decl.def_id, cid)) cname ctx)
+ ctx clause_names
+
+(** Similar to {!extract_trait_decl_register_names} *)
+let extract_trait_decl_register_constant_names (ctx : extraction_ctx)
+ (trait_decl : trait_decl)
+ (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
+ extraction_ctx =
+ let consts = trait_decl.consts in
+ (* Compute the names *)
+ let constant_names =
+ match builtin_info with
+ | None ->
+ List.map
+ (fun (item_name, _) ->
+ let name = ctx.fmt.trait_const_name trait_decl item_name in
+ (* Add a prefix if necessary *)
+ let name =
+ if !Config.record_fields_short_names then name
+ else ctx.fmt.trait_decl_name trait_decl ^ name
+ in
+ (item_name, name))
+ consts
+ | Some info ->
+ let const_map = StringMap.of_list info.consts in
+ List.map
+ (fun (item_name, _) ->
+ (item_name, StringMap.find item_name const_map))
+ consts
+ in
+ (* Register the names *)
+ List.fold_left
+ (fun ctx (item_name, name) ->
+ ctx_add (TraitItemId (trait_decl.def_id, item_name)) name ctx)
+ ctx constant_names
+
+(** Similar to {!extract_trait_decl_register_names} *)
+let extract_trait_decl_type_names (ctx : extraction_ctx)
+ (trait_decl : trait_decl)
+ (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
+ extraction_ctx =
+ let types = trait_decl.types in
+ (* Compute the names *)
+ let type_names =
+ match builtin_info with
+ | None ->
+ let compute_type_name (item_name : string) : string =
+ let type_name = ctx.fmt.trait_type_name trait_decl item_name in
+ if !Config.record_fields_short_names then type_name
+ else ctx.fmt.trait_decl_name trait_decl ^ type_name
+ in
+ let compute_clause_name (item_name : string) (clause : trait_clause) :
+ TraitClauseId.id * string =
+ let name =
+ ctx.fmt.trait_type_clause_name trait_decl item_name clause
+ in
+ (* Add a prefix if necessary *)
+ let name =
+ if !Config.record_fields_short_names then name
+ else ctx.fmt.trait_decl_name trait_decl ^ name
+ in
+ (clause.clause_id, name)
+ in
+ List.map
+ (fun (item_name, (item_clauses, _)) ->
+ (* Type name *)
+ let type_name = compute_type_name item_name in
+ (* Clause names *)
+ let clauses =
+ List.map (compute_clause_name item_name) item_clauses
+ in
+ (item_name, (type_name, clauses)))
+ types
+ | Some info ->
+ let type_map = StringMap.of_list info.types in
+ List.map
+ (fun (item_name, (item_clauses, _)) ->
+ let type_name, clauses_info = StringMap.find item_name type_map in
+ let clauses =
+ List.map
+ (fun (clause, clause_name) -> (clause.clause_id, clause_name))
+ (List.combine item_clauses clauses_info)
+ in
+ (item_name, (type_name, clauses)))
+ types
+ in
+ (* Register the names *)
+ List.fold_left
+ (fun ctx (item_name, (type_name, clauses)) ->
+ let ctx =
+ ctx_add (TraitItemId (trait_decl.def_id, item_name)) type_name ctx
+ in
+ List.fold_left
+ (fun ctx (clause_id, clause_name) ->
+ ctx_add
+ (TraitItemClauseId (trait_decl.def_id, item_name, clause_id))
+ clause_name ctx)
+ ctx clauses)
+ ctx type_names
+
+(** Similar to {!extract_trait_decl_register_names} *)
+let extract_trait_decl_method_names (ctx : extraction_ctx)
+ (trait_decl : trait_decl)
+ (builtin_info : ExtractBuiltin.builtin_trait_decl_info option) :
+ extraction_ctx =
+ let required_methods = trait_decl.required_methods in
+ (* Compute the names *)
+ let method_names =
+ (* We add one field per required forward/backward function *)
+ let get_funs_for_id (id : fun_decl_id) : fun_decl list =
+ let trans : pure_fun_translation = FunDeclId.Map.find id ctx.trans_funs in
+ List.map (fun f -> f.f) (trans.fwd :: trans.backs)
+ in
+ match builtin_info with
+ | None ->
+ (* We add one field per required forward/backward function *)
+ let compute_item_names (item_name : string) (id : fun_decl_id) :
+ string * (RegionGroupId.id option * string) list =
+ let compute_fun_name (f : fun_decl) : RegionGroupId.id option * string
+ =
+ (* We do something special: we use the base name but remove everything
+ but the crate (because [get_name] removes it) and the last ident.
+ This allows us to reuse the [ctx_compute_fun_decl] function.
+ *)
+ let basename : name =
+ match (f.basename : name) with
+ | Ident crate :: name ->
+ Ident crate :: [ Collections.List.last name ]
+ | _ -> raise (Failure "Unexpected")
+ in
+ let f = { f with basename } in
+ let trans = A.FunDeclId.Map.find f.def_id ctx.trans_funs in
+ let name = ctx_compute_fun_name trans f ctx in
+ (* Add a prefix if necessary *)
+ let name =
+ if !Config.record_fields_short_names then name
+ else ctx.fmt.trait_decl_name trait_decl ^ "_" ^ name
+ in
+ (f.back_id, name)
+ in
+ let funs = get_funs_for_id id in
+ (item_name, List.map compute_fun_name funs)
+ in
+ List.map (fun (name, id) -> compute_item_names name id) required_methods
+ | Some info ->
+ let funs_map = StringMap.of_list info.funs in
+ List.map
+ (fun (item_name, fun_id) ->
+ let info = StringMap.find item_name funs_map in
+ let trans_funs = get_funs_for_id fun_id in
+ let rg_with_name_list =
+ List.map
+ (fun (trans_fun : fun_decl) ->
+ List.find (fun (rg, _) -> rg = trans_fun.back_id) info)
+ trans_funs
+ in
+ (item_name, rg_with_name_list))
+ required_methods
+ in
(* Register the names *)
- let funs = trans.fwd :: trans.backs in
- List.fold_left register_fun ctx funs
+ List.fold_left
+ (fun ctx (item_name, funs) ->
+ (* We add one field per required forward/backward function *)
+ List.fold_left
+ (fun ctx (rg, fun_name) ->
+ ctx_add
+ (TraitMethodId (trait_decl.def_id, item_name, rg))
+ fun_name ctx)
+ ctx funs)
+ ctx method_names
(** Similar to {!extract_type_decl_register_names} *)
let extract_trait_decl_register_names (ctx : extraction_ctx)
(trait_decl : trait_decl) : extraction_ctx =
- let {
- def_id = _;
- name = _;
- generics;
- preds = _;
- all_trait_clauses = _;
- consts;
- types;
- required_methods;
- provided_methods = _;
- } =
- trait_decl
+ (* Lookup the information if this is a builtin trait *)
+ let open ExtractBuiltin in
+ let sname = name_to_simple_name trait_decl.name in
+ let builtin_info =
+ SimpleNameMap.find_opt sname (builtin_trait_decls_map ())
+ in
+ let ctx =
+ let trait_name =
+ match builtin_info with
+ | None -> ctx.fmt.trait_decl_name trait_decl
+ | Some info -> info.extract_name
+ in
+ ctx_add (TraitDeclId trait_decl.def_id) trait_name ctx
in
- let ctx = ctx_add_trait_decl trait_decl ctx in
(* Parent clauses *)
let ctx =
- List.fold_left
- (fun ctx clause -> ctx_add_trait_parent_clause trait_decl clause ctx)
- ctx generics.trait_clauses
+ extract_trait_decl_register_parent_clause_names ctx trait_decl builtin_info
in
(* Constants *)
let ctx =
- List.fold_left
- (fun ctx (name, (_, _)) -> ctx_add_trait_const trait_decl name ctx)
- ctx consts
+ extract_trait_decl_register_constant_names ctx trait_decl builtin_info
in
(* Types *)
- let ctx =
- List.fold_left
- (fun ctx (name, (clauses, _)) ->
- let ctx = ctx_add_trait_type trait_decl name ctx in
- List.fold_left
- (fun ctx clause ->
- ctx_add_trait_type_clause trait_decl name clause ctx)
- ctx clauses)
- ctx types
- in
+ let ctx = extract_trait_decl_type_names ctx trait_decl builtin_info in
(* Required methods *)
- List.fold_left
- (fun ctx (name, id) ->
- (* We add one field per required forward/backward function *)
- extract_trait_decl_method_register_names ctx trait_decl name id)
- ctx required_methods
+ let ctx = extract_trait_decl_method_names ctx trait_decl builtin_info in
+ ctx
(** Similar to {!extract_type_decl_register_names} *)
let extract_trait_impl_register_names (ctx : extraction_ctx)
(trait_impl : trait_impl) : extraction_ctx =
+ let trait_decl =
+ TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id
+ ctx.trans_trait_decls
+ in
+ (* Check if the trait implementation is builtin *)
+ let builtin_info =
+ let open ExtractBuiltin in
+ let type_sname = name_to_simple_name trait_impl.name in
+ let trait_sname = name_to_simple_name trait_decl.name in
+ SimpleNamePairMap.find_opt (type_sname, trait_sname)
+ (builtin_trait_impls_map ())
+ in
+
(* For now we do not support overriding provided methods *)
assert (trait_impl.provided_methods = []);
(* Everything is taken care of by {!extract_trait_decl_register_names} *but*
the name of the implementation itself *)
- ctx_add_trait_impl trait_impl ctx
+ (* Compute the name *)
+ let name =
+ match builtin_info with
+ | None -> ctx.fmt.trait_impl_name trait_decl trait_impl
+ | Some name -> name
+ in
+ ctx_add (TraitImplId trait_impl.def_id) name ctx
(** Small helper.
@@ -4198,8 +4462,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
(decl : trait_decl) : unit =
(* Retrieve the trait name *)
- let with_opaque_pre = false in
- let decl_name = ctx_get_trait_decl with_opaque_pre decl.def_id ctx in
+ let decl_name = ctx_get_trait_decl decl.def_id ctx in
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
@@ -4344,7 +4607,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
if use_forall then F.pp_print_string fmt ",";
(* Extract the function call *)
F.pp_print_space fmt ();
- let id = ctx_get_local_function false f.def_id None f.back_id ctx in
+ let id = ctx_get_local_function f.def_id None f.back_id ctx in
F.pp_print_string fmt id;
let all_generics =
let i_tys, i_cgs, i_tcs = impl_generics in
@@ -4363,9 +4626,9 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
(** Extract a trait implementation *)
let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(impl : trait_impl) : unit =
+ log#ldebug (lazy ("extract_trait_impl: " ^ Names.name_to_string impl.name));
(* Retrieve the impl name *)
- let with_opaque_pre = false in
- let impl_name = ctx_get_trait_impl with_opaque_pre impl.def_id ctx in
+ let impl_name = ctx_get_trait_impl impl.def_id ctx in
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
@@ -4389,9 +4652,11 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(* `let (....) : Trait ... =` *)
(* Open the box for the name + generics *)
F.pp_open_hovbox fmt ctx.indent_incr;
- let qualif = Option.get (ctx.fmt.fun_decl_kind_to_qualif SingleNonRec) in
- F.pp_print_string fmt qualif;
- F.pp_print_space fmt ();
+ (match ctx.fmt.fun_decl_kind_to_qualif SingleNonRec with
+ | Some qualif ->
+ F.pp_print_string fmt qualif;
+ F.pp_print_space fmt ()
+ | None -> ());
F.pp_print_string fmt impl_name;
(* Print the generics *)
@@ -4439,7 +4704,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
let item_name = ctx_get_trait_const trait_decl_id name ctx in
let ty () =
F.pp_print_space fmt ();
- F.pp_print_string fmt (ctx_get_global false id ctx)
+ F.pp_print_string fmt (ctx_get_global id ctx)
in
extract_trait_impl_item ctx fmt item_name ty)
@@ -4525,12 +4790,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "assert_norm";
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
- (* Note that if the function is opaque, the unit test will fail
- because the normalizer will get stuck *)
- let with_opaque_pre = ctx.use_opaque_pre in
let fun_name =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id
- def.back_id ctx
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx
in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
@@ -4545,12 +4806,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "Check";
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
- (* Note that if the function is opaque, the unit test will fail
- because the normalizer will get stuck *)
- let with_opaque_pre = ctx.use_opaque_pre in
let fun_name =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id
- def.back_id ctx
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx
in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
@@ -4562,12 +4819,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "#assert";
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
- (* Note that if the function is opaque, the unit test will fail
- because the normalizer will get stuck *)
- let with_opaque_pre = ctx.use_opaque_pre in
let fun_name =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id
- def.back_id ctx
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx
in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
@@ -4581,12 +4834,8 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
| HOL4 ->
F.pp_print_string fmt "val _ = assert_return (";
F.pp_print_string fmt "“";
- (* Note that if the function is opaque, the unit test will fail
- because the normalizer will get stuck *)
- let with_opaque_pre = ctx.use_opaque_pre in
let fun_name =
- ctx_get_local_function with_opaque_pre def.def_id def.loop_id
- def.back_id ctx
+ ctx_get_local_function def.def_id def.loop_id def.back_id ctx
in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
diff --git a/compiler/ExtractAssumed.ml b/compiler/ExtractAssumed.ml
deleted file mode 100644
index 7f094b24..00000000
--- a/compiler/ExtractAssumed.ml
+++ /dev/null
@@ -1,61 +0,0 @@
-(** This file declares external identifiers that we catch to map them to
- definitions coming from the standard libraries in our backends. *)
-
-open Names
-
-type simple_name = string list [@@deriving show, ord]
-
-let name_to_simple_name (s : name) : simple_name =
- (* We simply ignore the disambiguators *)
- List.filter_map (function Ident id -> Some id | Disambiguator _ -> None) s
-
-(** Small helper which cuts a string at the occurrences of "::" *)
-let string_to_simple_name (s : string) : simple_name =
- (* No function to split by using string separator?? *)
- let name = String.split_on_char ':' s in
- List.filter (fun s -> s <> "") name
-
-module SimpleNameOrd = struct
- type t = simple_name
-
- let compare = compare_simple_name
- let to_string = show_simple_name
- let pp_t = pp_simple_name
- let show_t = show_simple_name
-end
-
-module SimpleNameMap = Collections.MakeMap (SimpleNameOrd)
-
-let assumed_globals : (string * string) list =
- [
- (* Min *)
- ("core::num::usize::MIN", "core_usize_min");
- ("core::num::u8::MIN", "core_u8_min");
- ("core::num::u16::MIN", "core_u16_min");
- ("core::num::u32::MIN", "core_u32_min");
- ("core::num::u64::MIN", "core_u64_min");
- ("core::num::u128::MIN", "core_u128_min");
- ("core::num::isize::MIN", "core_isize_min");
- ("core::num::i8::MIN", "core_i8_min");
- ("core::num::i16::MIN", "core_i16_min");
- ("core::num::i32::MIN", "core_i32_min");
- ("core::num::i64::MIN", "core_i64_min");
- ("core::num::i128::MIN", "core_i128_min");
- (* Max *)
- ("core::num::usize::MAX", "core_usize_max");
- ("core::num::u8::MAX", "core_u8_max");
- ("core::num::u16::MAX", "core_u16_max");
- ("core::num::u32::MAX", "core_u32_max");
- ("core::num::u64::MAX", "core_u64_max");
- ("core::num::u128::MAX", "core_u128_max");
- ("core::num::isize::MAX", "core_isize_max");
- ("core::num::i8::MAX", "core_i8_max");
- ("core::num::i16::MAX", "core_i16_max");
- ("core::num::i32::MAX", "core_i32_max");
- ("core::num::i64::MAX", "core_i64_max");
- ("core::num::i128::MAX", "core_i128_max");
- ]
-
-let assumed_globals_map : string SimpleNameMap.t =
- SimpleNameMap.of_list
- (List.map (fun (x, y) -> (string_to_simple_name x, y)) assumed_globals)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index a921515b..e004aba8 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -5,7 +5,7 @@ open TranslateCore
module C = Contexts
module RegionVarId = T.RegionVarId
module F = Format
-open ExtractAssumed
+open ExtractBuiltin
(** The local logger *)
let log = L.pure_to_extract_log
@@ -251,37 +251,6 @@ type formatter = {
trait_type_name : trait_decl -> string -> string;
trait_method_name : trait_decl -> string -> string;
trait_type_clause_name : trait_decl -> string -> trait_clause -> string;
- opaque_pre : unit -> string;
- (** TODO: obsolete, remove.
-
- The prefix to use for opaque definitions.
-
- We need this because for some backends like Lean and Coq, we group
- opaque definitions in module signatures, meaning that using those
- definitions requires to prefix them with a module parameter name (such
- as "opaque_defs.").
-
- For instance, if we have an opaque function [f : int -> int], which
- is used by the non-opaque function [g], we would generate (in Coq):
- {[
- (* The module signature declaring the opaque definitions *)
- module type OpaqueDefs = {
- f_fwd : int -> int
- ... (* Other definitions *)
- }
-
- (* The definitions generated for the non-opaque definitions *)
- module Funs (opaque: OpaqueDefs) = {
- let g ... =
- ...
- opaque_defs.f_fwd
- ...
- }
- ]}
-
- Upon using [f] in [g], we don't directly use the the name "f_fwd",
- but prefix it with the "opaque_defs." identifier.
- *)
var_basename : StringSet.t -> string option -> ty -> string;
(** Generates a variable basename.
@@ -498,20 +467,6 @@ type names_map = {
precisely which identifiers are mapped to the same name...
*)
names_set : StringSet.t;
- opaque_ids : IdSet.t;
- (** TODO: this is obsolete. Remove.
-
- The set of opaque definitions.
-
- See {!formatter.opaque_pre} for detailed explanations about why
- we need to know which definitions are opaque to compute names.
-
- Also note that the opaque ids don't contain the ids of the assumed
- definitions. In practice, assumed definitions are opaque_defs. However, they
- are not grouped in the opaque module, meaning we never need to
- prefix them (with, say, "opaque_defs."): we thus consider them as non-opaque
- with regards to the names map.
- *)
}
let empty_names_map : names_map =
@@ -519,7 +474,6 @@ let empty_names_map : names_map =
id_to_name = IdMap.empty;
name_to_id = StringMap.empty;
names_set = StringSet.empty;
- opaque_ids = IdSet.empty;
}
(** Small helper to report name collision *)
@@ -547,8 +501,8 @@ let names_map_check_collision (id_to_string : id -> string) (id : id)
(* There is a clash: print a nice debugging message for the user *)
report_name_collision id_to_string clash id name
-let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id)
- (name : string) (nm : names_map) : names_map =
+let names_map_add (id_to_string : id -> string) (id : id) (name : string)
+ (nm : names_map) : names_map =
(* Check if there is a clash *)
names_map_check_collision id_to_string id name nm;
(* Sanity check *)
@@ -564,32 +518,24 @@ let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id)
let id_to_name = IdMap.add id name nm.id_to_name in
let name_to_id = StringMap.add name id nm.name_to_id in
let names_set = StringSet.add name nm.names_set in
- let opaque_ids =
- if is_opaque then IdSet.add id nm.opaque_ids else nm.opaque_ids
- in
- { id_to_name; name_to_id; names_set; opaque_ids }
+ { id_to_name; name_to_id; names_set }
let names_map_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
(name : string) (nm : names_map) : names_map =
- let is_opaque = false in
- names_map_add id_to_string is_opaque (TypeId (Assumed id)) name nm
+ names_map_add id_to_string (TypeId (Assumed id)) name nm
let names_map_add_assumed_struct (id_to_string : id -> string) (id : assumed_ty)
(name : string) (nm : names_map) : names_map =
- let is_opaque = false in
- names_map_add id_to_string is_opaque (StructId (Assumed id)) name nm
+ names_map_add id_to_string (StructId (Assumed id)) name nm
let names_map_add_assumed_variant (id_to_string : id -> string)
(id : assumed_ty) (variant_id : VariantId.id) (name : string)
(nm : names_map) : names_map =
- let is_opaque = false in
- names_map_add id_to_string is_opaque
- (VariantId (Assumed id, variant_id))
- name nm
+ names_map_add id_to_string (VariantId (Assumed id, variant_id)) name nm
-let names_map_add_function (id_to_string : id -> string) (is_opaque : bool)
- (fid : fun_id) (name : string) (nm : names_map) : names_map =
- names_map_add id_to_string is_opaque (FunId fid) name nm
+let names_map_add_function (id_to_string : id -> string) (fid : fun_id)
+ (name : string) (nm : names_map) : names_map =
+ names_map_add id_to_string (FunId fid) name nm
(** The unsafe names map stores mappings from identifiers to names which might
collide. For some backends and some names, it might be acceptable to have
@@ -667,14 +613,6 @@ type extraction_ctx = {
fmt : formatter;
indent_incr : int;
(** The indent increment we insert whenever we need to indent more *)
- use_opaque_pre : bool;
- (** Do we use the "opaque_defs." prefix for the opaque definitions?
-
- Opaque function definitions might refer opaque types: if we are in the
- opaque module, we musn't use the "opaque_defs." prefix, otherwise we
- use it.
- Also see {!names_map.opaque_ids}.
- *)
use_dep_ite : bool;
(** For Lean: do we use dependent-if then else expressions?
@@ -702,6 +640,19 @@ type extraction_ctx = {
functions_with_decreases_clause : PureUtils.FunLoopIdSet.t;
trans_trait_decls : Pure.trait_decl Pure.TraitDeclId.Map.t;
trans_trait_impls : Pure.trait_impl Pure.TraitImplId.Map.t;
+ types_filter_type_args_map : bool list TypeDeclId.Map.t;
+ (** The map to filter the type arguments for the builtin type
+ definitions.
+
+ We need this for type `Vec`, for instance, which takes a useless
+ (in the context of the type translation) type argument for the
+ allocator which is used, and which we want to remove.
+
+ TODO: it would be cleaner to filter those types in a micro-pass,
+ rather than at code generation time.
+ *)
+ funs_filter_type_args_map : bool list FunDeclId.Map.t;
+ (** Same as {!types_filter_type_args_map}, but for functions *)
}
(** Debugging function, used when communicating name collisions to the user,
@@ -803,15 +754,11 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
if variant_id = error_failure_id then "@error::Failure"
else if variant_id = error_out_of_fuel_id then "@error::OutOfFuel"
else raise (Failure "Unreachable")
- | Assumed Option ->
- if variant_id = option_some_id then "@option::Some"
- else if variant_id = option_none_id then "@option::None"
- else raise (Failure "Unreachable")
| Assumed Fuel ->
if variant_id = fuel_zero_id then "@fuel::0"
else if variant_id = fuel_succ_id then "@fuel::Succ"
else raise (Failure "Unreachable")
- | Assumed (State | Vec | Array | Slice | Str | Range) ->
+ | Assumed (State | Array | Slice | Str) ->
raise
(Failure
("Unreachable: variant id ("
@@ -830,9 +777,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
let field_name =
match id with
| Tuple -> raise (Failure "Unreachable")
- | Assumed
- ( State | Result | Error | Fuel | Option | Vec | Array | Slice | Str
- | Range ) ->
+ | Assumed (State | Result | Error | Fuel | Array | Slice | Str) ->
(* We can't directly have access to the fields of those types *)
raise (Failure "Unreachable")
| AdtId id -> (
@@ -890,8 +835,7 @@ let allow_collisions (id : id) : bool =
!Config.record_fields_short_names
| _ -> false
-let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx)
- : extraction_ctx =
+let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
(* The id_to_string function to print nice debugging messages if there are
* collisions *)
let id_to_string (id : id) : string = id_to_string id ctx in
@@ -908,7 +852,6 @@ let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx)
others (ex.: fields and keywords).
*)
if allow_collisions id then (
- assert (not is_opaque);
(* Check with the ids which are considered to be strict on collisions *)
names_map_check_collision id_to_string id name ctx.strict_names_map;
{
@@ -922,16 +865,13 @@ let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx)
*)
let strict_names_map =
if strict_collisions id then
- names_map_add id_to_string is_opaque id name ctx.strict_names_map
+ names_map_add id_to_string id name ctx.strict_names_map
else ctx.strict_names_map
in
- let names_map =
- names_map_add id_to_string is_opaque id name ctx.names_map
- in
+ let names_map = names_map_add id_to_string id name ctx.names_map in
{ ctx with strict_names_map; names_map }
-(** [with_opaque_pre]: if [true] and the definition is opaque, add the opaque prefix *)
-let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string =
+let ctx_get (id : id) (ctx : extraction_ctx) : string =
(* We do not use the same name map if we allow/disallow collisions *)
let map_to_string (m : string IdMap.t) : string =
"[\n"
@@ -957,9 +897,7 @@ let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string =
else
let m = ctx.names_map.id_to_name in
match IdMap.find_opt id m with
- | Some s ->
- let is_opaque = IdSet.mem id ctx.names_map.opaque_ids in
- if with_opaque_pre && is_opaque then ctx.fmt.opaque_pre () ^ s else s
+ | Some s -> s
| None ->
let err =
"Could not find: " ^ id_to_string id ctx ^ "\nNames map:\n"
@@ -969,53 +907,38 @@ let ctx_get (with_opaque_pre : bool) (id : id) (ctx : extraction_ctx) : string =
if !Config.extract_fail_hard then raise (Failure err)
else "(ERROR: \"" ^ id_to_string id ctx ^ "\")"
-let ctx_get_global (with_opaque_pre : bool) (id : A.GlobalDeclId.id)
- (ctx : extraction_ctx) : string =
- ctx_get with_opaque_pre (GlobalId id) ctx
+let ctx_get_global (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string =
+ ctx_get (GlobalId id) ctx
-let ctx_get_function (with_opaque_pre : bool) (id : fun_id)
- (ctx : extraction_ctx) : string =
- ctx_get with_opaque_pre (FunId id) ctx
+let ctx_get_function (id : fun_id) (ctx : extraction_ctx) : string =
+ ctx_get (FunId id) ctx
-let ctx_get_local_function (with_opaque_pre : bool) (id : A.FunDeclId.id)
- (lp : LoopId.id option) (rg : RegionGroupId.id option)
- (ctx : extraction_ctx) : string =
- ctx_get_function with_opaque_pre (FromLlbc (FunId (Regular id), lp, rg)) ctx
+let ctx_get_local_function (id : A.FunDeclId.id) (lp : LoopId.id option)
+ (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string =
+ ctx_get_function (FromLlbc (FunId (Regular id), lp, rg)) ctx
-let ctx_get_type (with_opaque_pre : bool) (id : type_id) (ctx : extraction_ctx)
- : string =
+let ctx_get_type (id : type_id) (ctx : extraction_ctx) : string =
assert (id <> Tuple);
- ctx_get with_opaque_pre (TypeId id) ctx
+ ctx_get (TypeId id) ctx
-let ctx_get_local_type (with_opaque_pre : bool) (id : TypeDeclId.id)
- (ctx : extraction_ctx) : string =
- ctx_get_type with_opaque_pre (AdtId id) ctx
+let ctx_get_local_type (id : TypeDeclId.id) (ctx : extraction_ctx) : string =
+ ctx_get_type (AdtId id) ctx
let ctx_get_assumed_type (id : assumed_ty) (ctx : extraction_ctx) : string =
- (* In practice, the assumed types are opaque. However, assumed types
- are never grouped in the opaque module, meaning we never need to
- prefix them: we thus consider them as non-opaque with regards to the
- names map.
- *)
- let is_opaque = false in
- ctx_get_type is_opaque (Assumed id) ctx
+ ctx_get_type (Assumed id) ctx
let ctx_get_trait_self_clause (ctx : extraction_ctx) : string =
- let with_opaque_pre = false in
- ctx_get with_opaque_pre TraitSelfClauseId ctx
+ ctx_get TraitSelfClauseId ctx
-let ctx_get_trait_decl (with_opaque_pre : bool) (id : trait_decl_id)
- (ctx : extraction_ctx) : string =
- ctx_get with_opaque_pre (TraitDeclId id) ctx
+let ctx_get_trait_decl (id : trait_decl_id) (ctx : extraction_ctx) : string =
+ ctx_get (TraitDeclId id) ctx
-let ctx_get_trait_impl (with_opaque_pre : bool) (id : trait_impl_id)
- (ctx : extraction_ctx) : string =
- ctx_get with_opaque_pre (TraitImplId id) ctx
+let ctx_get_trait_impl (id : trait_impl_id) (ctx : extraction_ctx) : string =
+ ctx_get (TraitImplId id) ctx
let ctx_get_trait_item (id : trait_decl_id) (item_name : string)
(ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (TraitItemId (id, item_name)) ctx
+ ctx_get (TraitItemId (id, item_name)) ctx
let ctx_get_trait_const (id : trait_decl_id) (item_name : string)
(ctx : extraction_ctx) : string =
@@ -1027,83 +950,69 @@ let ctx_get_trait_type (id : trait_decl_id) (item_name : string)
let ctx_get_trait_method (id : trait_decl_id) (item_name : string)
(rg_id : T.RegionGroupId.id option) (ctx : extraction_ctx) : string =
- let with_opaque_pre = false in
- ctx_get with_opaque_pre (TraitMethodId (id, item_name, rg_id)) ctx
+ ctx_get (TraitMethodId (id, item_name, rg_id)) ctx
let ctx_get_trait_parent_clause (id : trait_decl_id) (clause : trait_clause_id)
(ctx : extraction_ctx) : string =
- let with_opaque_pre = false in
- ctx_get with_opaque_pre (TraitParentClauseId (id, clause)) ctx
+ ctx_get (TraitParentClauseId (id, clause)) ctx
let ctx_get_trait_item_clause (id : trait_decl_id) (item : string)
(clause : trait_clause_id) (ctx : extraction_ctx) : string =
- let with_opaque_pre = false in
- ctx_get with_opaque_pre (TraitItemClauseId (id, item, clause)) ctx
+ ctx_get (TraitItemClauseId (id, item, clause)) ctx
let ctx_get_var (id : VarId.id) (ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (VarId id) ctx
+ ctx_get (VarId id) ctx
let ctx_get_type_var (id : TypeVarId.id) (ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (TypeVarId id) ctx
+ ctx_get (TypeVarId id) ctx
let ctx_get_const_generic_var (id : ConstGenericVarId.id) (ctx : extraction_ctx)
: string =
- let is_opaque = false in
- ctx_get is_opaque (ConstGenericVarId id) ctx
+ ctx_get (ConstGenericVarId id) ctx
let ctx_get_local_trait_clause (id : TraitClauseId.id) (ctx : extraction_ctx) :
string =
- let is_opaque = false in
- ctx_get is_opaque (LocalTraitClauseId id) ctx
+ ctx_get (LocalTraitClauseId id) ctx
let ctx_get_field (type_id : type_id) (field_id : FieldId.id)
(ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (FieldId (type_id, field_id)) ctx
+ ctx_get (FieldId (type_id, field_id)) ctx
-let ctx_get_struct (with_opaque_pre : bool) (def_id : type_id)
- (ctx : extraction_ctx) : string =
- ctx_get with_opaque_pre (StructId def_id) ctx
+let ctx_get_struct (def_id : type_id) (ctx : extraction_ctx) : string =
+ ctx_get (StructId def_id) ctx
let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id)
(ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (VariantId (def_id, variant_id)) ctx
+ ctx_get (VariantId (def_id, variant_id)) ctx
let ctx_get_decreases_proof (def_id : A.FunDeclId.id)
(loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (DecreasesProofId (Regular def_id, loop_id)) ctx
+ ctx_get (DecreasesProofId (Regular def_id, loop_id)) ctx
let ctx_get_termination_measure (def_id : A.FunDeclId.id)
(loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
- let is_opaque = false in
- ctx_get is_opaque (TerminationMeasureId (Regular def_id, loop_id)) ctx
+ ctx_get (TerminationMeasureId (Regular def_id, loop_id)) ctx
(** Generate a unique type variable name and add it to the context *)
let ctx_add_type_var (basename : string) (id : TypeVarId.id)
(ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
let name = ctx.fmt.type_var_basename ctx.names_map.names_set basename in
let name =
basename_to_unique ctx.names_map.names_set ctx.fmt.append_index name
in
- let ctx = ctx_add is_opaque (TypeVarId id) name ctx in
+ let ctx = ctx_add (TypeVarId id) name ctx in
(ctx, name)
(** Generate a unique const generic variable name and add it to the context *)
let ctx_add_const_generic_var (basename : string) (id : ConstGenericVarId.id)
(ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
let name =
ctx.fmt.const_generic_var_basename ctx.names_map.names_set basename
in
let name =
basename_to_unique ctx.names_map.names_set ctx.fmt.append_index name
in
- let ctx = ctx_add is_opaque (ConstGenericVarId id) name ctx in
+ let ctx = ctx_add (ConstGenericVarId id) name ctx in
(ctx, name)
(** See {!ctx_add_type_var} *)
@@ -1116,31 +1025,28 @@ let ctx_add_type_vars (vars : (string * TypeVarId.id) list)
(** Generate a unique variable name and add it to the context *)
let ctx_add_var (basename : string) (id : VarId.id) (ctx : extraction_ctx) :
extraction_ctx * string =
- let is_opaque = false in
let name =
basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename
in
- let ctx = ctx_add is_opaque (VarId id) name ctx in
+ let ctx = ctx_add (VarId id) name ctx in
(ctx, name)
(** Generate a unique variable name for the trait self clause and add it to the context *)
let ctx_add_trait_self_clause (ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
let basename = ctx.fmt.trait_self_clause_basename in
let name =
basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename
in
- let ctx = ctx_add is_opaque TraitSelfClauseId name ctx in
+ let ctx = ctx_add TraitSelfClauseId name ctx in
(ctx, name)
(** Generate a unique trait clause name and add it to the context *)
let ctx_add_local_trait_clause (basename : string) (id : TraitClauseId.id)
(ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
let name =
basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename
in
- let ctx = ctx_add is_opaque (LocalTraitClauseId id) name ctx in
+ let ctx = ctx_add (LocalTraitClauseId id) name ctx in
(ctx, name)
(** See {!ctx_add_var} *)
@@ -1186,107 +1092,41 @@ let ctx_add_generic_params (generics : generic_params) (ctx : extraction_ctx) :
let ctx, tcs = ctx_add_local_trait_clauses trait_clauses ctx in
(ctx, tys, cgs, tcs)
-let ctx_add_type_decl_struct (def : type_decl) (ctx : extraction_ctx) :
- extraction_ctx * string =
- assert (match def.kind with Struct _ -> true | _ -> false);
- let is_opaque = false in
- let cons_name = ctx.fmt.struct_constructor def.name in
- let ctx = ctx_add is_opaque (StructId (AdtId def.def_id)) cons_name ctx in
- (ctx, cons_name)
-
-let ctx_add_type_decl (def : type_decl) (ctx : extraction_ctx) : extraction_ctx
- =
- let is_opaque = def.kind = Opaque in
- let def_name = ctx.fmt.type_name def.name in
- let ctx = ctx_add is_opaque (TypeId (AdtId def.def_id)) def_name ctx in
- ctx
-
-let ctx_add_field (def : type_decl) (field_id : FieldId.id) (field : field)
- (ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
- let name = ctx.fmt.field_name def.name field_id field.field_name in
- let ctx = ctx_add is_opaque (FieldId (AdtId def.def_id, field_id)) name ctx in
- (ctx, name)
-
-let ctx_add_fields (def : type_decl) (fields : (FieldId.id * field) list)
- (ctx : extraction_ctx) : extraction_ctx * string list =
- List.fold_left_map
- (fun ctx (vid, v) -> ctx_add_field def vid v ctx)
- ctx fields
-
-let ctx_add_variant (def : type_decl) (variant_id : VariantId.id)
- (variant : variant) (ctx : extraction_ctx) : extraction_ctx * string =
- let is_opaque = false in
- let name = ctx.fmt.variant_name def.name variant.variant_name in
- (* Add the type name prefix for Lean *)
- let name =
- if !Config.backend = Lean then
- let type_name = ctx.fmt.type_name def.name in
- type_name ^ "." ^ name
- else name
- in
- let ctx =
- ctx_add is_opaque (VariantId (AdtId def.def_id, variant_id)) name ctx
- in
- (ctx, name)
-
-let ctx_add_variants (def : type_decl)
- (variants : (VariantId.id * variant) list) (ctx : extraction_ctx) :
- extraction_ctx * string list =
- List.fold_left_map
- (fun ctx (vid, v) -> ctx_add_variant def vid v ctx)
- ctx variants
-
-let ctx_add_struct (def : type_decl) (ctx : extraction_ctx) :
- extraction_ctx * string =
- assert (match def.kind with Struct _ -> true | _ -> false);
- let is_opaque = false in
- let name = ctx.fmt.struct_constructor def.name in
- let ctx = ctx_add is_opaque (StructId (AdtId def.def_id)) name ctx in
- (ctx, name)
-
let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
- let is_opaque = false in
let name =
ctx.fmt.decreases_proof_name def.def_id def.basename def.num_loops
def.loop_id
in
- ctx_add is_opaque
- (DecreasesProofId (Regular def.def_id, def.loop_id))
- name ctx
+ ctx_add (DecreasesProofId (Regular def.def_id, def.loop_id)) name ctx
let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
- let is_opaque = false in
let name =
ctx.fmt.termination_measure_name def.def_id def.basename def.num_loops
def.loop_id
in
- ctx_add is_opaque
- (TerminationMeasureId (Regular def.def_id, def.loop_id))
- name ctx
+ ctx_add (TerminationMeasureId (Regular def.def_id, def.loop_id)) name ctx
let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
extraction_ctx =
(* TODO: update once the body id can be an option *)
- let is_opaque = false in
let decl = GlobalId def.def_id in
(* Check if the global corresponds to an assumed global that we should map
to a custom definition in our standard library (for instance, happens
with "core::num::usize::MAX") *)
let sname = name_to_simple_name def.name in
- match SimpleNameMap.find_opt sname assumed_globals_map with
+ match SimpleNameMap.find_opt sname builtin_globals_map with
| Some name ->
(* Yes: register the custom binding *)
- ctx_add is_opaque decl name ctx
+ ctx_add decl name ctx
| None ->
(* Not the case: "standard" registration *)
let name = ctx.fmt.global_name def.name in
let body = FunId (FromLlbc (FunId (Regular def.body_id), None, None)) in
- let ctx = ctx_add is_opaque decl (name ^ "_c") ctx in
- let ctx = ctx_add is_opaque body (name ^ "_body") ctx in
+ let ctx = ctx_add decl (name ^ "_c") ctx in
+ let ctx = ctx_add body (name ^ "_body") ctx in
ctx
let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl)
@@ -1314,6 +1154,7 @@ let ctx_compute_fun_name (trans_group : pure_fun_translation) (def : fun_decl)
ctx.fmt.fun_name def.basename def.num_loops def.loop_id num_rgs rg_info
(keep_fwd, num_backs)
+(* TODO: move to Extract *)
let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl)
(ctx : extraction_ctx) : extraction_ctx =
(* Sanity check: the function should not be a global body - those are handled
@@ -1323,11 +1164,10 @@ let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl)
let def_id = def.def_id in
let { keep_fwd; fwd = _; backs } = trans_group in
let num_backs = List.length backs in
- let is_opaque = def.body = None in
(* Add the function name *)
let def_name = ctx_compute_fun_name trans_group def ctx in
let fun_id = (Pure.FunId (Regular def_id), def.loop_id, def.back_id) in
- let ctx = ctx_add is_opaque (FunId (FromLlbc fun_id)) def_name ctx in
+ let ctx = ctx_add (FunId (FromLlbc fun_id)) def_name ctx in
(* Add the name info *)
{
ctx with
@@ -1336,91 +1176,6 @@ let ctx_add_fun_decl (trans_group : pure_fun_translation) (def : fun_decl)
ctx.fun_name_info;
}
-let ctx_add_trait_decl (d : trait_decl) (ctx : extraction_ctx) : extraction_ctx
- =
- let is_opaque = false in
- let name = ctx.fmt.trait_decl_name d in
- ctx_add is_opaque (TraitDeclId d.def_id) name ctx
-
-let ctx_add_trait_impl (d : trait_impl) (ctx : extraction_ctx) : extraction_ctx
- =
- (* We need to lookup the trait decl that is implemented by the trait impl *)
- let decl =
- Pure.TraitDeclId.Map.find d.impl_trait.trait_decl_id ctx.trans_trait_decls
- in
- (* Compute the name *)
- let is_opaque = false in
- let name = ctx.fmt.trait_impl_name decl d in
- ctx_add is_opaque (TraitImplId d.def_id) name ctx
-
-let ctx_add_trait_const (d : trait_decl) (item : string) (ctx : extraction_ctx)
- : extraction_ctx =
- let is_opaque = false in
- let name = ctx.fmt.trait_const_name d item in
- (* Add a prefix if necessary *)
- let name =
- if !Config.record_fields_short_names then name
- else ctx.fmt.trait_decl_name d ^ name
- in
- ctx_add is_opaque (TraitItemId (d.def_id, item)) name ctx
-
-let ctx_add_trait_type (d : trait_decl) (item : string) (ctx : extraction_ctx) :
- extraction_ctx =
- let is_opaque = false in
- let name = ctx.fmt.trait_type_name d item in
- (* Add a prefix if necessary *)
- let name =
- if !Config.record_fields_short_names then name
- else ctx.fmt.trait_decl_name d ^ name
- in
- ctx_add is_opaque (TraitItemId (d.def_id, item)) name ctx
-
-let ctx_add_trait_method (d : trait_decl) (item_name : string) (f : fun_decl)
- (ctx : extraction_ctx) : extraction_ctx =
- (* We do something special: we use the base name but remove everything
- but the crate (because [get_name] removes it) and the last ident.
- This allows us to reuse the [ctx_compute_fun_decl] function.
- *)
- let basename : name =
- match (f.basename : name) with
- | Ident crate :: name -> Ident crate :: [ Collections.List.last name ]
- | _ -> raise (Failure "Unexpected")
- in
- let f = { f with basename } in
- let trans = A.FunDeclId.Map.find f.def_id ctx.trans_funs in
- let name = ctx_compute_fun_name trans f ctx in
- (* Add a prefix if necessary *)
- let name =
- if !Config.record_fields_short_names then name
- else ctx.fmt.trait_decl_name d ^ "_" ^ name
- in
- let is_opaque = false in
- ctx_add is_opaque (TraitMethodId (d.def_id, item_name, f.back_id)) name ctx
-
-let ctx_add_trait_parent_clause (d : trait_decl) (clause : trait_clause)
- (ctx : extraction_ctx) : extraction_ctx =
- let is_opaque = false in
- let name = ctx.fmt.trait_parent_clause_name d clause in
- (* Add a prefix if necessary *)
- let name =
- if !Config.record_fields_short_names then name
- else ctx.fmt.trait_decl_name d ^ name
- in
- ctx_add is_opaque (TraitParentClauseId (d.def_id, clause.clause_id)) name ctx
-
-let ctx_add_trait_type_clause (d : trait_decl) (item : string)
- (clause : trait_clause) (ctx : extraction_ctx) : extraction_ctx =
- let is_opaque = false in
- let name = ctx.fmt.trait_type_clause_name d item clause in
- (* Add a prefix if necessary *)
- let name =
- if !Config.record_fields_short_names then name
- else ctx.fmt.trait_decl_name d ^ name
- in
- ctx_add is_opaque
- (TraitItemClauseId (d.def_id, item, clause.clause_id))
- name ctx
-
type names_map_init = {
keywords : string list;
assumed_adts : (assumed_ty * string) list;
@@ -1445,12 +1200,11 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map =
let name_to_id =
StringMap.of_list (List.map (fun x -> (x, UnknownId)) keywords)
in
- let opaque_ids = IdSet.empty in
(* We fist initialize [id_to_name] as empty, because the id of a keyword is [UnknownId].
* Also note that we don't need this mapping for keywords: we insert keywords only
* to check collisions. *)
let id_to_name = IdMap.empty in
- let nm = { id_to_name; name_to_id; names_set; opaque_ids } in
+ let nm = { id_to_name; name_to_id; names_set } in
(* For debugging - we are creating bindings for assumed types and functions, so
* it is ok if we simply use the "show" function (those aren't simply identified
* by numbers) *)
@@ -1487,15 +1241,8 @@ let initialize_names_map (fmt : formatter) (init : names_map_init) : names_map =
@ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions
in
let nm =
- (* In practice, the assumed function are opaque. However, assumed functions
- are never grouped in the opaque module, meaning we never need to
- prefix them: we thus consider them as non-opaque with regards to the
- names map.
- *)
- let is_opaque = false in
List.fold_left
- (fun nm (fid, name) ->
- names_map_add_function id_to_string is_opaque fid name nm)
+ (fun nm (fid, name) -> names_map_add_function id_to_string fid name nm)
nm assumed_functions
in
(* Return *)
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
new file mode 100644
index 00000000..9cc7c226
--- /dev/null
+++ b/compiler/ExtractBuiltin.ml
@@ -0,0 +1,560 @@
+(** This file declares external identifiers that we catch to map them to
+ definitions coming from the standard libraries in our backends.
+
+ TODO: there misses trait **implementations**
+ *)
+
+open Names
+open Config
+
+type simple_name = string list [@@deriving show, ord]
+
+let name_to_simple_name (s : name) : simple_name =
+ (* We simply ignore the disambiguators *)
+ List.filter_map (function Ident id -> Some id | Disambiguator _ -> None) s
+
+(** Small helper which cuts a string at the occurrences of "::" *)
+let string_to_simple_name (s : string) : simple_name =
+ (* No function to split by using string separator?? *)
+ let name = String.split_on_char ':' s in
+ List.filter (fun s -> s <> "") name
+
+module SimpleNameOrd = struct
+ type t = simple_name
+
+ let compare = compare_simple_name
+ let to_string = show_simple_name
+ let pp_t = pp_simple_name
+ let show_t = show_simple_name
+end
+
+module SimpleNameMap = Collections.MakeMap (SimpleNameOrd)
+module SimpleNameSet = Collections.MakeSet (SimpleNameOrd)
+
+(** Small utility to memoize some computations *)
+let mk_memoized (f : unit -> 'a) : unit -> 'a =
+ let r = ref None in
+ let g () =
+ match !r with
+ | Some x -> x
+ | None ->
+ let x = f () in
+ r := Some x;
+ x
+ in
+ g
+
+let builtin_globals : (string * string) list =
+ [
+ (* Min *)
+ ("core::num::usize::MIN", "core_usize_min");
+ ("core::num::u8::MIN", "core_u8_min");
+ ("core::num::u16::MIN", "core_u16_min");
+ ("core::num::u32::MIN", "core_u32_min");
+ ("core::num::u64::MIN", "core_u64_min");
+ ("core::num::u128::MIN", "core_u128_min");
+ ("core::num::isize::MIN", "core_isize_min");
+ ("core::num::i8::MIN", "core_i8_min");
+ ("core::num::i16::MIN", "core_i16_min");
+ ("core::num::i32::MIN", "core_i32_min");
+ ("core::num::i64::MIN", "core_i64_min");
+ ("core::num::i128::MIN", "core_i128_min");
+ (* Max *)
+ ("core::num::usize::MAX", "core_usize_max");
+ ("core::num::u8::MAX", "core_u8_max");
+ ("core::num::u16::MAX", "core_u16_max");
+ ("core::num::u32::MAX", "core_u32_max");
+ ("core::num::u64::MAX", "core_u64_max");
+ ("core::num::u128::MAX", "core_u128_max");
+ ("core::num::isize::MAX", "core_isize_max");
+ ("core::num::i8::MAX", "core_i8_max");
+ ("core::num::i16::MAX", "core_i16_max");
+ ("core::num::i32::MAX", "core_i32_max");
+ ("core::num::i64::MAX", "core_i64_max");
+ ("core::num::i128::MAX", "core_i128_max");
+ ]
+
+let builtin_globals_map : string SimpleNameMap.t =
+ SimpleNameMap.of_list
+ (List.map (fun (x, y) -> (string_to_simple_name x, y)) builtin_globals)
+
+type builtin_variant_info = { fields : (string * string) list }
+[@@deriving show]
+
+type builtin_enum_variant_info = {
+ rust_variant_name : string;
+ extract_variant_name : string;
+ fields : string list option;
+}
+[@@deriving show]
+
+type builtin_type_body_info =
+ | Struct of string * string list
+ (* The constructor name and the map for the field names *)
+ | Enum of builtin_enum_variant_info list
+(* For every variant, a map for the field names *)
+[@@deriving show]
+
+type builtin_type_info = {
+ rust_name : string list;
+ extract_name : string;
+ keep_params : bool list option;
+ (** We might want to filter some of the type parameters.
+
+ For instance, `Vec` type takes a type parameter for the allocator,
+ which we want to ignore.
+ *)
+ body_info : builtin_type_body_info option;
+}
+[@@deriving show]
+
+(** The assumed types.
+
+ The optional list of booleans is filtering information for the type
+ parameters. For instance, in the case of the `Vec` functions, there is
+ a type parameter for the allocator to use, which we want to filter.
+ *)
+let builtin_types () : builtin_type_info list =
+ [
+ (* Alloc *)
+ {
+ rust_name = [ "alloc"; "alloc"; "Global" ];
+ extract_name =
+ (match !backend with
+ | Lean -> "AllocGlobal"
+ | Coq | FStar | HOL4 -> "alloc_global");
+ keep_params = None;
+ body_info = None;
+ };
+ (* Vec *)
+ {
+ rust_name = [ "alloc"; "vec"; "Vec" ];
+ extract_name =
+ (match !backend with Lean -> "Vec" | Coq | FStar | HOL4 -> "vec");
+ keep_params = Some [ true; false ];
+ body_info = None;
+ };
+ (* Option *)
+ {
+ rust_name = [ "core"; "option"; "Option" ];
+ extract_name =
+ (match !backend with
+ | Lean -> "Option"
+ | Coq | FStar | HOL4 -> "option");
+ keep_params = None;
+ body_info =
+ Some
+ (Enum
+ [
+ {
+ rust_variant_name = "None";
+ extract_variant_name =
+ (match !backend with
+ | FStar | Coq -> "None"
+ | Lean -> "none"
+ | HOL4 -> "NONE");
+ fields = None;
+ };
+ {
+ rust_variant_name = "Some";
+ extract_variant_name =
+ (match !backend with
+ | FStar | Coq -> "Some"
+ | Lean -> "some"
+ | HOL4 -> "SOME");
+ fields = None;
+ };
+ ]);
+ };
+ (* Range *)
+ {
+ rust_name = [ "core"; "ops"; "range"; "Range" ];
+ extract_name =
+ (match !backend with Lean -> "Range" | Coq | FStar | HOL4 -> "range");
+ keep_params = None;
+ body_info =
+ Some
+ (Struct
+ ( (match !backend with
+ | Lean -> "Range.mk"
+ | Coq | HOL4 -> "mk_range"
+ | FStar -> "Mkrange"),
+ [ "start"; "end_" ] ));
+ };
+ ]
+
+let mk_builtin_types_map () =
+ SimpleNameMap.of_list
+ (List.map (fun info -> (info.rust_name, info)) (builtin_types ()))
+
+let builtin_types_map = mk_memoized mk_builtin_types_map
+
+type builtin_fun_info = {
+ rg : Types.RegionGroupId.id option;
+ extract_name : string;
+}
+[@@deriving show]
+
+(** The assumed functions.
+
+ The optional list of booleans is filtering information for the type
+ parameters. For instance, in the case of the `Vec` functions, there is
+ a type parameter for the allocator to use, which we want to filter.
+ *)
+let builtin_funs () :
+ (string list * bool list option * builtin_fun_info list) list =
+ let rg0 = Some Types.RegionGroupId.zero in
+ [
+ ( [ "core"; "mem"; "replace" ],
+ None,
+ [
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "core_mem_replace_fwd"
+ | Lean -> "core.mem.replace");
+ };
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "core_mem_replace_back"
+ | Lean -> "core.mem.replace_back");
+ };
+ ] );
+ ( [ "alloc"; "vec"; "Vec"; "new" ],
+ Some [ true; false ],
+ [
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_new"
+ | Lean -> "Vec.new");
+ };
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_new_back"
+ | Lean -> "Vec.new_back");
+ };
+ ] );
+ ( [ "alloc"; "vec"; "Vec"; "push" ],
+ Some [ true; false ],
+ [
+ (* The forward function shouldn't be used *)
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_push_fwd"
+ | Lean -> "Vec.push_fwd");
+ };
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_push_back"
+ | Lean -> "Vec.push");
+ };
+ ] );
+ ( [ "alloc"; "vec"; "Vec"; "insert" ],
+ Some [ true; false ],
+ [
+ (* The forward function shouldn't be used *)
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_insert_fwd"
+ | Lean -> "Vec.insert_fwd");
+ };
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_insert_back"
+ | Lean -> "Vec.insert");
+ };
+ ] );
+ ( [ "alloc"; "vec"; "Vec"; "len" ],
+ Some [ true; false ],
+ [
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_len"
+ | Lean -> "Vec.len");
+ };
+ ] );
+ ( [ "alloc"; "vec"; "Vec"; "index" ],
+ Some [ true; false ],
+ [
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_index_fwd"
+ | Lean -> "Vec.index_shared");
+ };
+ (* The backward function shouldn't be used *)
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_index_back"
+ | Lean -> "Vec.index_shared_back");
+ };
+ ] );
+ ( [ "alloc"; "vec"; "Vec"; "index_mut" ],
+ Some [ true; false ],
+ [
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_index_mut_fwd"
+ | Lean -> "Vec.index_mut");
+ };
+ (* The backward function shouldn't be used *)
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "vec_index_mut_back"
+ | Lean -> "Vec.index_mut_back");
+ };
+ ] );
+ ( [ "alloc"; "boxed"; "Box"; "deref" ],
+ Some [ true; false ],
+ [
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "alloc_boxed_box_deref"
+ | Lean -> "alloc.boxed.Box.deref");
+ };
+ (* The backward function shouldn't be used *)
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_back"
+ | Lean -> "alloc.boxed.Box.deref_back");
+ };
+ ] );
+ ( [ "alloc"; "boxed"; "Box"; "deref_mut" ],
+ Some [ true; false ],
+ [
+ {
+ rg = None;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_mut"
+ | Lean -> "alloc.boxed.Box.deref_mut");
+ };
+ {
+ rg = rg0;
+ extract_name =
+ (match !backend with
+ | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_mut_back"
+ | Lean -> "alloc.boxed.Box.deref_mut_back");
+ };
+ ] );
+ ]
+
+let mk_builtin_funs_map () =
+ SimpleNameMap.of_list
+ (List.map
+ (fun (name, filter, info) -> (name, (filter, info)))
+ (builtin_funs ()))
+
+let builtin_funs_map = mk_memoized mk_builtin_funs_map
+
+let builtin_non_fallible_funs =
+ [ "alloc::boxed::Box::deref"; "alloc::boxed::Box::deref_mut" ]
+
+let builtin_non_fallible_funs_set =
+ SimpleNameSet.of_list
+ (List.map string_to_simple_name builtin_non_fallible_funs)
+
+type builtin_trait_decl_info = {
+ rust_name : string;
+ extract_name : string;
+ parent_clauses : string list;
+ consts : (string * string) list;
+ types : (string * (string * string list)) list;
+ (** Every type has:
+ - a Rust name
+ - an extraction name
+ - a list of clauses *)
+ funs : (string * (Types.RegionGroupId.id option * string) list) list;
+}
+[@@deriving show]
+
+let builtin_trait_decls_info () =
+ let rg0 = Some Types.RegionGroupId.zero in
+ [
+ {
+ (* Deref *)
+ rust_name = "core::ops::deref::Deref";
+ extract_name =
+ (match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_deref_Deref"
+ | Lean -> "core.ops.deref.Deref");
+ parent_clauses = [];
+ consts = [];
+ types =
+ [
+ ( "Target",
+ ( (match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_deref_Deref_Target"
+ | Lean -> "Target"),
+ [] ) );
+ ];
+ funs =
+ [
+ ( "deref",
+ [
+ ( None,
+ match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_deref_Deref_deref"
+ | Lean -> "deref" );
+ ] );
+ ];
+ };
+ {
+ (* DerefMut *)
+ rust_name = "core::ops::deref::DerefMut";
+ extract_name =
+ (match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut"
+ | Lean -> "core.ops.deref.DerefMut");
+ parent_clauses =
+ [
+ (match !backend with
+ | Coq | FStar | HOL4 -> "deref_inst"
+ | Lean -> "derefInst");
+ ];
+ consts = [];
+ types = [];
+ funs =
+ [
+ ( "deref_mut",
+ [
+ ( None,
+ match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut"
+ | Lean -> "deref_mut" );
+ ( rg0,
+ match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut_back"
+ | Lean -> "deref_mut_back" );
+ ] );
+ ];
+ };
+ {
+ (* Index *)
+ rust_name = "core::ops::index::Index";
+ extract_name =
+ (match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_index_Index"
+ | Lean -> "core.ops.index.Index");
+ parent_clauses = [];
+ consts = [];
+ types =
+ [
+ ( "Output",
+ ( (match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_index_Index_Output"
+ | Lean -> "Output"),
+ [] ) );
+ ];
+ funs =
+ [
+ ( "index",
+ [
+ ( None,
+ match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_index_Index_index"
+ | Lean -> "index" );
+ ] );
+ ];
+ };
+ {
+ (* IndexMut *)
+ rust_name = "core::ops::index::IndexMut";
+ extract_name =
+ (match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_index_IndexMut"
+ | Lean -> "core.ops.index.IndexMut");
+ parent_clauses =
+ [
+ (match !backend with
+ | Coq | FStar | HOL4 -> "index_inst"
+ | Lean -> "IndexInst");
+ ];
+ consts = [];
+ types = [];
+ funs =
+ [
+ ( "index_mut",
+ [
+ ( None,
+ match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut"
+ | Lean -> "index_mut" );
+ ( rg0,
+ match !backend with
+ | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut_back"
+ | Lean -> "index_mut_back" );
+ ] );
+ ];
+ };
+ ]
+
+let mk_builtin_trait_decls_map () =
+ SimpleNameMap.of_list
+ (List.map
+ (fun info -> (string_to_simple_name info.rust_name, info))
+ (builtin_trait_decls_info ()))
+
+let builtin_trait_decls_map = mk_memoized mk_builtin_trait_decls_map
+
+(* TODO: generalize this.
+
+ For now, the key is:
+ - name of the impl (ex.: "alloc.boxed.Boxed")
+ - name of the implemented trait (ex.: "core.ops.deref.Deref"
+*)
+type simple_name_pair = simple_name * simple_name [@@deriving show, ord]
+
+module SimpleNamePairOrd = struct
+ type t = simple_name_pair
+
+ let compare = compare_simple_name_pair
+ let to_string = show_simple_name_pair
+ let pp_t = pp_simple_name_pair
+ let show_t = show_simple_name_pair
+end
+
+module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd)
+
+let builtin_trait_impls_info () : ((string list * string list) * string) list =
+ [
+ (* core::ops::Deref<alloc::boxed::Box<T>> *)
+ ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "Deref" ]),
+ "alloc.boxed.Box.coreOpsDerefInst" );
+ (* core::ops::DerefMut<alloc::boxed::Box<T>> *)
+ ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "DerefMut" ]),
+ "alloc.boxed.Box.coreOpsDerefMutInst" );
+ ]
+
+let mk_builtin_trait_impls_map () =
+ SimpleNamePairMap.of_list (builtin_trait_impls_info ())
+
+let builtin_trait_impls_map = mk_memoized mk_builtin_trait_impls_map
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 9f82b5c9..1273f57d 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -106,7 +106,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
can_diverge := !can_diverge || info.can_diverge
| FunId (Assumed id) ->
(* None of the assumed functions can diverge nor are considered stateful *)
- can_fail := !can_fail || Assumed.assumed_can_fail id
+ can_fail := !can_fail || Assumed.assumed_fun_can_fail id
| TraitMethod _ ->
(* We consider trait functions can fail, diverge, and are not stateful *)
can_fail := true;
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index c1041fa3..167e3d58 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -241,17 +241,6 @@ let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
(* Initialize all the expanded values of all the variants *)
List.map initialize variants_fields_types
-(** Compute the expansion of an Option value.
- *)
-let compute_expanded_symbolic_option_value (expand_enumerations : bool)
- (kind : V.sv_kind) (ty : T.rty) : V.symbolic_expansion list =
- assert expand_enumerations;
- let some_se =
- V.SeAdt (Some T.option_some_id, [ mk_fresh_symbolic_value kind ty ])
- in
- let none_se = V.SeAdt (Some T.option_none_id, []) in
- [ none_se; some_se ]
-
let compute_expanded_symbolic_tuple_value (kind : V.sv_kind)
(field_types : T.rty list) : V.symbolic_expansion =
(* Generate the field values *)
@@ -286,8 +275,6 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
def_id generics ctx
| T.Tuple, [], _ ->
[ compute_expanded_symbolic_tuple_value kind generics.types ]
- | T.Assumed T.Option, [], [ ty ] ->
- compute_expanded_symbolic_option_value expand_enumerations kind ty
| T.Assumed T.Box, [], [ boxed_ty ] ->
[ compute_expanded_symbolic_box_value kind boxed_ty ]
| _ ->
@@ -704,7 +691,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
| T.Adt ((Tuple | Assumed Box), _) | T.Ref (_, _, _) ->
(* Ok *)
expand_symbolic_value_no_branching config sv None
- | T.Adt (Assumed (Vec | Option | Array | Slice | Str | Range), _) ->
+ | T.Adt (Assumed (Array | Slice | Str), _) ->
(* We can't expand those *)
raise
(Failure
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index a42c552a..341e97eb 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -142,10 +142,10 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
| V.Adt av ->
(* Sanity check *)
(match v.V.ty with
- | T.Adt (T.Assumed (T.Box | Vec), _) ->
+ | T.Adt (T.Assumed T.Box, _) ->
raise (Failure "Can't copy an assumed value other than Option")
| T.Adt (T.AdtId _, _) -> assert allow_adt_copy
- | T.Adt ((T.Assumed Option | T.Tuple), _) -> () (* Ok *)
+ | T.Adt (T.Tuple, _) -> () (* Ok *)
| T.Adt
( T.Assumed (Slice | T.Array),
{
@@ -722,70 +722,38 @@ let eval_rvalue_aggregate (config : C.config)
fun ctx ->
(* Match on the aggregate kind *)
match aggregate_kind with
- | E.AggregatedTuple ->
- let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
- let v = V.Adt { variant_id = None; field_values = values } in
- let generics = TypesUtils.mk_generic_args [] tys [] [] in
- let ty = T.Adt (T.Tuple, generics) in
- let aggregated : V.typed_value = { V.value = v; ty } in
- (* Call the continuation *)
- cf aggregated ctx
- | E.AggregatedOption (variant_id, ty) ->
- (* Sanity check *)
- if variant_id = T.option_none_id then assert (values = [])
- else if variant_id = T.option_some_id then
- assert (List.length values = 1)
- else raise (Failure "Unreachable");
- (* Construt the value *)
- let generics = TypesUtils.mk_generic_args [] [ ty ] [] [] in
- let aty = T.Adt (T.Assumed T.Option, generics) in
- let av : V.adt_value =
- { V.variant_id = Some variant_id; V.field_values = values }
- in
- let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
- (* Call the continuation *)
- cf aggregated ctx
- | E.AggregatedAdt (def_id, opt_variant_id, generics) ->
- (* Sanity checks *)
- let type_decl = C.ctx_lookup_type_decl ctx def_id in
- assert (
- List.length type_decl.generics.regions = List.length generics.regions);
- let expected_field_types =
- Assoc.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id
- generics
- in
- assert (
- expected_field_types
- = List.map (fun (v : V.typed_value) -> v.V.ty) values);
- (* Construct the value *)
- let av : V.adt_value =
- { V.variant_id = opt_variant_id; V.field_values = values }
- in
- let aty = T.Adt (T.AdtId def_id, generics) in
- let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
- (* Call the continuation *)
- cf aggregated ctx
- | E.AggregatedRange ety ->
- (* There should be two fields exactly *)
- let v0, v1 =
- match values with
- | [ v0; v1 ] -> (v0, v1)
- | _ -> raise (Failure "Unreachable")
- in
- (* Ranges are parametric over the type of indices. For now we only
- support scalars, which can be of any type *)
- assert (literal_type_is_integer (ty_as_literal ety));
- assert (v0.ty = ety);
- assert (v1.ty = ety);
- (* Construct the value *)
- let av : V.adt_value =
- { V.variant_id = None; V.field_values = values }
- in
- let generics = TypesUtils.mk_generic_args_from_types [ ety ] in
- let aty = T.Adt (T.Assumed T.Range, generics) in
- let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
- (* Call the continuation *)
- cf aggregated ctx
+ | E.AggregatedAdt (type_id, opt_variant_id, generics) -> (
+ match type_id with
+ | Tuple ->
+ let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
+ let v = V.Adt { variant_id = None; field_values = values } in
+ let generics = TypesUtils.mk_generic_args [] tys [] [] in
+ let ty = T.Adt (T.Tuple, generics) in
+ let aggregated : V.typed_value = { V.value = v; ty } in
+ (* Call the continuation *)
+ cf aggregated ctx
+ | AdtId def_id ->
+ (* Sanity checks *)
+ let type_decl = C.ctx_lookup_type_decl ctx def_id in
+ assert (
+ List.length type_decl.generics.regions
+ = List.length generics.regions);
+ let expected_field_types =
+ Assoc.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id
+ generics
+ in
+ assert (
+ expected_field_types
+ = List.map (fun (v : V.typed_value) -> v.V.ty) values);
+ (* Construct the value *)
+ let av : V.adt_value =
+ { V.variant_id = opt_variant_id; V.field_values = values }
+ in
+ let aty = T.Adt (T.AdtId def_id, generics) in
+ let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
+ (* Call the continuation *)
+ cf aggregated ctx
+ | Assumed _ -> raise (Failure "Unreachable"))
| E.AggregatedArray (ety, cg) -> (
(* Sanity check: all the values have the proper type *)
assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values);
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 465d0028..2a277c91 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -96,7 +96,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
| pe :: p' -> (
(* Match on the projection element and the value *)
match (pe, v.V.value, v.V.ty) with
- | ( Field (((ProjAdt (_, _) | ProjOption _) as proj_kind), field_id),
+ | ( Field ((ProjAdt (_, _) as proj_kind), field_id),
V.Adt adt,
T.Adt (type_id, _) ) -> (
(* Check consistency *)
@@ -104,8 +104,6 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
| ProjAdt (def_id, opt_variant_id), T.AdtId def_id' ->
assert (def_id = def_id');
assert (opt_variant_id = adt.variant_id)
- | ProjOption variant_id, T.Assumed T.Option ->
- assert (Some variant_id = adt.variant_id)
| _ -> raise (Failure "Unreachable"));
(* Actually project *)
let fv = T.FieldId.nth adt.field_values field_id in
@@ -136,7 +134,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
Ok (ctx, { res with updated })
(* If we reach Bottom, it may mean we need to expand an uninitialized
* enumeration value *))
- | Field ((ProjAdt (_, _) | ProjTuple _ | ProjOption _), _), V.Bottom, _ ->
+ | Field ((ProjAdt (_, _) | ProjTuple _), _), V.Bottom, _ ->
Error (FailBottom (1 + List.length p', pe, v.ty))
(* Symbolic value: needs to be expanded *)
| _, Symbolic sp, _ ->
@@ -376,20 +374,6 @@ let compute_expanded_bottom_adt_value (ctx : C.eval_ctx)
let ty = T.Adt (T.AdtId def_id, generics) in
{ V.value = av; V.ty }
-let compute_expanded_bottom_option_value (variant_id : T.VariantId.id)
- (param_ty : T.ety) : V.typed_value =
- (* Note that the variant can be [Some] or [None]: we expand bottom values
- * when writing to fields or setting discriminants *)
- let field_values =
- if variant_id = T.option_some_id then [ mk_bottom param_ty ]
- else if variant_id = T.option_none_id then []
- else raise (Failure "Unreachable")
- in
- let av = V.Adt { variant_id = Some variant_id; field_values } in
- let generics = TypesUtils.mk_generic_args [] [ param_ty ] [] [] in
- let ty = T.Adt (T.Assumed T.Option, generics) in
- { V.value = av; ty }
-
let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
V.typed_value =
(* Generate the field values *)
@@ -451,17 +435,6 @@ let expand_bottom_value_from_projection (access : access_kind) (p : E.place)
T.Adt (T.AdtId def_id', generics) ) ->
assert (def_id = def_id');
compute_expanded_bottom_adt_value ctx def_id opt_variant_id generics
- (* Option *)
- | ( Field (ProjOption variant_id, _),
- T.Adt
- ( T.Assumed T.Option,
- {
- T.regions = [];
- types = [ ty ];
- const_generics = [];
- trait_refs = [];
- } ) ) ->
- compute_expanded_bottom_option_value variant_id ty
(* Tuples *)
| ( Field (ProjTuple arity, _),
T.Adt
diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli
index 041b0a97..0ff8063f 100644
--- a/compiler/InterpreterPaths.mli
+++ b/compiler/InterpreterPaths.mli
@@ -63,10 +63,6 @@ val compute_expanded_bottom_adt_value :
T.egeneric_args ->
V.typed_value
-(** Compute an expanded [Option] ⊥ value *)
-val compute_expanded_bottom_option_value :
- T.VariantId.id -> T.ety -> V.typed_value
-
(** Drop (end) outer loans at a given place, which should be seen as an l-value
(we will write to it later, but need to drop the loans before writing).
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 9f35c6f2..e0c4703b 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -10,7 +10,6 @@ open TypesUtils
open ValuesUtils
module Inv = Invariants
module S = SynthesizeSymbolic
-open Utils
open Cps
open InterpreterUtils
open InterpreterProjectors
@@ -233,8 +232,7 @@ let set_discriminant (config : C.config) (p : E.place)
let update_value cf (v : V.typed_value) : m_fun =
fun ctx ->
match (v.V.ty, v.V.value) with
- | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Adt av
- -> (
+ | T.Adt ((T.AdtId _ as type_id), generics), V.Adt av -> (
(* There are two situations:
- either the discriminant is already the proper one (in which case we
don't do anything)
@@ -253,24 +251,15 @@ let set_discriminant (config : C.config) (p : E.place)
| T.AdtId def_id ->
compute_expanded_bottom_adt_value ctx def_id
(Some variant_id) generics
- | T.Assumed T.Option ->
- assert (generics.regions = []);
- compute_expanded_bottom_option_value variant_id
- (Collections.List.to_cons_nil generics.types)
| _ -> raise (Failure "Unreachable")
in
assign_to_place config bottom_v p (cf Unit) ctx)
- | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Bottom
- ->
+ | T.Adt ((T.AdtId _ as type_id), generics), V.Bottom ->
let bottom_v =
match type_id with
| T.AdtId def_id ->
compute_expanded_bottom_adt_value ctx def_id (Some variant_id)
generics
- | T.Assumed T.Option ->
- assert (generics.regions = []);
- compute_expanded_bottom_option_value variant_id
- (Collections.List.to_cons_nil generics.types)
| _ -> raise (Failure "Unreachable")
in
assign_to_place config bottom_v p (cf Unit) ctx
@@ -313,7 +302,7 @@ let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id)
mk_unit_ty
| _ ->
(* Retrieve the function's signature *)
- let sg = Assumed.get_assumed_sig fid in
+ let sg = Assumed.get_assumed_fun_sig fid in
(* Instantiate the return type *)
(* There shouldn't be any reference to Self *)
let tr_self : T.erased_region T.trait_instance_id =
@@ -427,11 +416,6 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
comp cf_pop cf_assign
(** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_replace_concrete (_config : C.config) (_generics : T.egeneric_args) :
- cm_fun =
- fun _cf _ctx -> raise Unimplemented
-
-(** Auxiliary function - see {!eval_assumed_function_call} *)
let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) :
cm_fun =
fun cf ctx ->
@@ -475,67 +459,6 @@ let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) :
comp cf_move cf_create cf ctx
| _ -> raise (Failure "Inconsistent state")
-(** Auxiliary function which factorizes code to evaluate [std::Deref::deref]
- and [std::DerefMut::deref_mut] - see {!eval_assumed_function_call} *)
-let eval_box_deref_mut_or_shared_concrete (config : C.config)
- (generics : T.egeneric_args) (is_mut : bool) : cm_fun =
- fun cf ctx ->
- (* Check the arguments *)
- match
- (generics.regions, generics.types, generics.const_generics, ctx.env)
- with
- | ( [],
- [ boxed_ty ],
- [],
- Var (VarBinder input_var, input_value)
- :: Var (_ret_var, _)
- :: C.Frame :: _ ) ->
- (* Required type checking. We must have:
- - input_value.ty = & (mut) Box<ty>
- - boxed_ty = ty
- for some ty
- *)
- (let _, input_ty, ref_kind = ty_get_ref input_value.V.ty in
- assert (match ref_kind with T.Shared -> not is_mut | T.Mut -> is_mut);
- let input_ty = ty_get_box input_ty in
- assert (input_ty = boxed_ty));
-
- (* Borrow the boxed value *)
- let p =
- { E.var_id = input_var.C.index; projection = [ E.Deref; E.DerefBox ] }
- in
- let borrow_kind = if is_mut then E.Mut else E.Shared in
- let rv = E.RvRef (p, borrow_kind) in
- let cf_borrow = eval_rvalue_not_global config rv in
-
- (* Move the borrow to its destination *)
- let cf_move cf res : m_fun =
- match res with
- | Error EPanic ->
- (* We can't get there by borrowing a value *)
- raise (Failure "Unreachable")
- | Ok borrowed_value ->
- (* Move and continue *)
- let destp = mk_place_from_var_id E.VarId.zero in
- assign_to_place config borrowed_value destp cf
- in
-
- (* Compose and apply *)
- comp cf_borrow cf_move cf ctx
- | _ -> raise (Failure "Inconsistent state")
-
-(** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_box_deref_concrete (config : C.config) (generics : T.egeneric_args) :
- cm_fun =
- let is_mut = false in
- eval_box_deref_mut_or_shared_concrete config generics is_mut
-
-(** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_box_deref_mut_concrete (config : C.config) (generics : T.egeneric_args)
- : cm_fun =
- let is_mut = true in
- eval_box_deref_mut_or_shared_concrete config generics is_mut
-
(** Auxiliary function - see {!eval_assumed_function_call}.
[Box::free] is not handled the same way as the other assumed functions:
@@ -575,11 +498,6 @@ let eval_box_free (config : C.config) (generics : T.egeneric_args)
cc cf ctx
| _ -> raise (Failure "Inconsistent state")
-(** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id)
- (_generics : T.egeneric_args) : cm_fun =
- fun _cf _ctx -> raise Unimplemented
-
(** Evaluate a non-local function call in concrete mode *)
let eval_assumed_function_call_concrete (config : C.config)
(fid : A.assumed_fun_id) (call : A.call) : cm_fun =
@@ -636,18 +554,12 @@ let eval_assumed_function_call_concrete (config : C.config)
* access to a body. *)
let cf_eval_body : cm_fun =
match fid with
- | Replace -> eval_replace_concrete config generics
| BoxNew -> eval_box_new_concrete config generics
- | BoxDeref -> eval_box_deref_concrete config generics
- | BoxDerefMut -> eval_box_deref_mut_concrete config generics
| BoxFree ->
(* Should have been treated above *) raise (Failure "Unreachable")
- | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut ->
- eval_vec_function_concrete config fid generics
| ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared
- | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut
- | ArrayRepeat | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
- | SliceSubsliceMut | SliceLen ->
+ | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut
+ | SliceLen ->
raise (Failure "Unimplemented")
in
@@ -1196,6 +1108,13 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
match call.func.func with
| FunId (Regular fid) ->
let def = C.ctx_lookup_fun_decl ctx fid in
+ log#ldebug
+ (lazy
+ ("fun call:\n- call: " ^ call_to_string ctx call
+ ^ "\n- call.generics:\n"
+ ^ egeneric_args_to_string ctx call.func.generics
+ ^ "\n- def.signature:\n"
+ ^ fun_sig_to_string ctx def.A.signature));
let tr_self = T.UnknownTrait __FUNCTION__ in
let inst_sg =
instantiate_fun_sig ctx call.func.generics tr_self def.A.signature
@@ -1531,7 +1450,7 @@ and eval_assumed_function_call_symbolic (config : C.config)
(* There shouldn't be any reference to Self *)
let tr_self = T.UnknownTrait __FUNCTION__ in
instantiate_fun_sig ctx generics tr_self
- (Assumed.get_assumed_sig fid)
+ (Assumed.get_assumed_fun_sig fid)
in
(* Evaluate the function call *)
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 9ac5ce13..5c8ec7af 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -447,7 +447,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
fields_with_types
(* Assumed type case *)
| V.Adt av, T.Adt (T.Assumed aty_id, generics) -> (
- assert (av.V.variant_id = None || aty_id = T.Option);
+ assert (av.V.variant_id = None);
match
( aty_id,
av.V.field_values,
@@ -456,19 +456,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
generics.const_generics )
with
(* Box *)
- | T.Box, [ inner_value ], [], [ inner_ty ], []
- | T.Option, [ inner_value ], [], [ inner_ty ], [] ->
+ | T.Box, [ inner_value ], [], [ inner_ty ], [] ->
assert (inner_value.V.ty = inner_ty)
- | T.Option, _, [], [ _ ], [] ->
- (* Option::None: nothing to check *)
- ()
- | T.Vec, fvs, [], [ vec_ty ], [] ->
- List.iter
- (fun (v : V.typed_value) -> assert (v.ty = vec_ty))
- fvs
- | T.Range, [ v0; v1 ], [], [ inner_ty ], [] ->
- assert (v0.V.ty = inner_ty);
- assert (v1.V.ty = inner_ty)
| T.Array, inner_values, _, [ inner_ty ], [ cg ] ->
(* *)
assert (
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index a982af30..2553127a 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -5,13 +5,13 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
fun_sig =
match fun_id with
| Regular id -> (FunDeclId.Map.find id fun_decls).signature
- | Assumed aid -> Assumed.get_assumed_sig aid
+ | Assumed aid -> Assumed.get_assumed_fun_sig aid
let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
Names.fun_name =
match fun_id with
| Regular id -> (FunDeclId.Map.find id fun_decls).name
- | Assumed aid -> Assumed.get_assumed_name aid
+ | Assumed aid -> Assumed.get_assumed_fun_name aid
(** Return the opaque declarations found in the crate.
@@ -22,7 +22,7 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
*)
let crate_get_opaque_decls (k : crate) (filter_assumed : bool) :
T.type_decl list * fun_decl list =
- let open ExtractAssumed in
+ let open ExtractBuiltin in
let is_opaque_fun (d : fun_decl) : bool =
let sname = name_to_simple_name d.name in
d.body = None
@@ -30,7 +30,7 @@ let crate_get_opaque_decls (k : crate) (filter_assumed : bool) :
(which don't have a body but must not be considered as opaque) *)
&& (match d.kind with TraitMethodDecl _ -> false | _ -> true)
&& ((not filter_assumed)
- || not (SimpleNameMap.mem sname assumed_globals_map))
+ || not (SimpleNameMap.mem sname builtin_globals_map))
in
let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in
(* Note that by checking the function bodies we also the globals *)
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 1058fab0..ee06fa07 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -108,7 +108,7 @@ let remove_useless_cf_merges (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
| Assign (_, rv) -> (
match rv with
| Use _ | RvRef _ -> not must_end_with_exit
- | Aggregate (AggregatedTuple, []) -> not must_end_with_exit
+ | Aggregate (AggregatedAdt (Tuple, _, _), []) -> not must_end_with_exit
| _ -> false)
| FakeRead _ | Drop _ | Nop -> not must_end_with_exit
| Panic | Return -> true
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 1d5ddc50..aeacfbf0 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -127,17 +127,6 @@ module Values = struct
(* Assumed type *)
match (aty, field_values) with
| Box, [ bv ] -> "@Box(" ^ bv ^ ")"
- | Option, _ ->
- if av.variant_id = Some T.option_some_id then
- "@Option::Some("
- ^ Collections.List.to_cons_nil field_values
- ^ ")"
- else if av.variant_id = Some T.option_none_id then (
- assert (field_values = []);
- "@Option::None")
- else raise (Failure "Unreachable")
- | Range, _ -> "@Range{ " ^ String.concat ", " field_values ^ "}"
- | Vec, _ -> "@Vec[" ^ String.concat ", " field_values ^ "]"
| Array, _ ->
(* Happens when we aggregate values *)
"@Array[" ^ String.concat ", " field_values ^ "]"
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index be7b3cb4..6396fe96 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -195,12 +195,9 @@ let assumed_ty_to_string (aty : assumed_ty) : string =
| Result -> "Result"
| Error -> "Error"
| Fuel -> "Fuel"
- | Option -> "Option"
- | Vec -> "Vec"
| Array -> "Array"
| Slice -> "Slice"
| Str -> "Str"
- | Range -> "Range"
let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
match id with
@@ -354,10 +351,6 @@ let rec mprojection_to_string (fmt : ast_formatter) (inside : string)
| pe :: p' -> (
let s = mprojection_to_string fmt inside p' in
match pe.pkind with
- | E.ProjOption variant_id ->
- assert (variant_id = T.option_some_id);
- assert (pe.field_id = T.FieldId.zero);
- "(" ^ s ^ "as Option::Some)." ^ T.FieldId.to_string pe.field_id
| E.ProjTuple _ -> "(" ^ s ^ ")." ^ T.FieldId.to_string pe.field_id
| E.ProjAdt (adt_id, opt_variant_id) -> (
let field_name =
@@ -395,8 +388,6 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
| State | Array | Slice | Str ->
(* Those types are opaque: we can't get there *)
raise (Failure "Unreachable")
- | Vec -> "@Vec"
- | Range -> "@Range"
| Result ->
let variant_id = Option.get variant_id in
if variant_id = result_return_id then "@Result::Return"
@@ -412,13 +403,7 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
let variant_id = Option.get variant_id in
if variant_id = fuel_zero_id then "@Fuel::Zero"
else if variant_id = fuel_succ_id then "@Fuel::Succ"
- else raise (Failure "Unreachable: improper variant id for fuel type")
- | Option ->
- let variant_id = Option.get variant_id in
- if variant_id = option_some_id then "@Option::Some "
- else if variant_id = option_none_id then "@Option::None"
- else
- raise (Failure "Unreachable: improper variant id for result type"))
+ else raise (Failure "Unreachable: improper variant id for fuel type"))
let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
(field_id : FieldId.id) : string =
@@ -435,11 +420,10 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
| Assumed aty -> (
(* Assumed type *)
match aty with
- | Range -> FieldId.to_string field_id
- | State | Fuel | Vec | Array | Slice | Str ->
+ | State | Fuel | Array | Slice | Str ->
(* Opaque types: we can't get there *)
raise (Failure "Unreachable")
- | Result | Error | Option ->
+ | Result | Error ->
(* Enumerations: we can't get there *)
raise (Failure "Unreachable"))
@@ -510,31 +494,13 @@ let adt_g_value_to_string (fmt : value_formatter)
| [ v ] -> "@Fuel::Succ " ^ v
| _ -> raise (Failure "@Fuel::Succ takes exactly one value")
else raise (Failure "Unreachable: improper variant id for fuel type")
- | Option ->
- let variant_id = Option.get variant_id in
- if variant_id = option_some_id then
- match field_values with
- | [ v ] -> "@Option::Some " ^ v
- | _ -> raise (Failure "Option::Some takes exactly one value")
- else if variant_id = option_none_id then (
- assert (field_values = []);
- "@Option::None")
- else
- raise (Failure "Unreachable: improper variant id for result type")
- | Vec | Array | Slice | Str ->
- assert (variant_id = None);
- let field_values =
- List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
- in
- let id = assumed_ty_to_string aty in
- id ^ " [" ^ String.concat "; " field_values ^ "]"
- | Range ->
+ | Array | Slice | Str ->
assert (variant_id = None);
let field_values =
List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
in
let id = assumed_ty_to_string aty in
- id ^ " {" ^ String.concat "; " field_values ^ "}")
+ id ^ " [" ^ String.concat "; " field_values ^ "]")
| _ ->
let fmt = value_to_type_formatter fmt in
raise
@@ -593,29 +559,16 @@ let fun_suffix (lp_id : LoopId.id option) (rg_id : T.RegionGroupId.id option) :
let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string =
match fid with
- | Replace -> "core::mem::replace"
| BoxNew -> "alloc::boxed::Box::new"
- | BoxDeref -> "core::ops::deref::Deref::deref"
- | BoxDerefMut -> "core::ops::deref::DerefMut::deref_mut"
| BoxFree -> "alloc::alloc::box_free"
- | VecNew -> "alloc::vec::Vec::new"
- | VecPush -> "alloc::vec::Vec::push"
- | VecInsert -> "alloc::vec::Vec::insert"
- | VecLen -> "alloc::vec::Vec::len"
- | VecIndex -> "core::ops::index::Index<alloc::vec::Vec>::index"
- | VecIndexMut -> "core::ops::index::IndexMut<alloc::vec::Vec>::index_mut"
| ArrayIndexShared -> "@ArrayIndexShared"
| ArrayIndexMut -> "@ArrayIndexMut"
| ArrayToSliceShared -> "@ArrayToSliceShared"
| ArrayToSliceMut -> "@ArrayToSliceMut"
- | ArraySubsliceShared -> "@ArraySubsliceShared"
- | ArraySubsliceMut -> "@ArraySubsliceMut"
| ArrayRepeat -> "@ArrayRepeat"
| SliceLen -> "@SliceLen"
| SliceIndexShared -> "@SliceIndexShared"
| SliceIndexMut -> "@SliceIndexMut"
- | SliceSubsliceShared -> "@SliceSubsliceShared"
- | SliceSubsliceMut -> "@SliceSubsliceMut"
let pure_assumed_fun_id_to_string (fid : pure_assumed_fun_id) : string =
match fid with
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 47c7beb4..81e13af7 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -64,17 +64,7 @@ type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
this state is opaque to Aeneas (the user can define it, or leave it as
assumed)
*)
-type assumed_ty =
- | State
- | Result
- | Error
- | Fuel
- | Vec
- | Option
- | Array
- | Slice
- | Str
- | Range
+type assumed_ty = State | Result | Error | Fuel | Array | Slice | Str
[@@deriving show, ord]
(* TODO: we should never directly manipulate [Return] and [Fail], but rather
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index b00509a6..f3e6cbe2 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1513,7 +1513,7 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl =
function calls, and when translating end abstractions. Here, we can do
something simpler, in one micro-pass.
*)
-let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
+let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
(* The map visitor *)
let obj =
object
@@ -1522,30 +1522,44 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
method! visit_texpression env e =
match opt_destruct_function_call e with
| Some (fun_id, _tys, args) -> (
+ (* Below, when dealing with the arguments: we consider the very
+ * general case, where functions could be boxed (meaning we
+ * could have: [box_new f x])
+ * *)
match fun_id with
| Fun (FromLlbc (FunId (Assumed aid), _lp_id, rg_id)) -> (
- (* Below, when dealing with the arguments: we consider the very
- * general case, where functions could be boxed (meaning we
- * could have: [box_new f x])
- * *)
match (aid, rg_id) with
| BoxNew, _ ->
assert (rg_id = None);
let arg, args = Collections.List.pop args in
mk_apps arg args
- | BoxDeref, None ->
+ | BoxFree, _ ->
+ assert (args = []);
+ mk_unit_rvalue
+ | ( ( SliceIndexShared | SliceIndexMut | ArrayIndexShared
+ | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
+ | ArrayRepeat | SliceLen ),
+ _ ) ->
+ super#visit_texpression env e)
+ | Fun (FromLlbc (FunId (Regular fid), _lp_id, rg_id)) -> (
+ (* Lookup the function name *)
+ let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in
+ match
+ (Names.name_no_disambiguators_to_string def.name, rg_id)
+ with
+ | "alloc::boxed::Box::deref", None ->
(* [Box::deref] forward is the identity *)
let arg, args = Collections.List.pop args in
mk_apps arg args
- | BoxDeref, Some _ ->
+ | "alloc::boxed::Box::deref", Some _ ->
(* [Box::deref] backward is [()] (doesn't give back anything) *)
assert (args = []);
mk_unit_rvalue
- | BoxDerefMut, None ->
+ | "alloc::boxed::Box::deref_mut", None ->
(* [Box::deref_mut] forward is the identity *)
let arg, args = Collections.List.pop args in
mk_apps arg args
- | BoxDerefMut, Some _ ->
+ | "alloc::boxed::Box::deref_mut", Some _ ->
(* [Box::deref_mut] back is almost the identity:
* let box_deref_mut (x_init : t) (x_back : t) : t = x_back
* *)
@@ -1555,17 +1569,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
| _ -> raise (Failure "Unreachable")
in
mk_apps arg args
- | BoxFree, _ ->
- assert (args = []);
- mk_unit_rvalue
- | ( ( Replace | VecNew | VecPush | VecInsert | VecLen | VecIndex
- | VecIndexMut | ArraySubsliceShared | ArraySubsliceMut
- | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
- | SliceSubsliceMut | ArrayIndexShared | ArrayIndexMut
- | ArrayToSliceShared | ArrayToSliceMut | ArrayRepeat
- | SliceLen ),
- _ ) ->
- super#visit_texpression env e)
+ | _ -> super#visit_texpression env e)
| _ -> super#visit_texpression env e)
| _ -> super#visit_texpression env e
end
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index b80ff72f..d31f0cf9 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -46,18 +46,7 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
if variant_id = fuel_zero_id then []
else if variant_id = fuel_succ_id then [ mk_fuel_ty ]
else raise (Failure "Unreachable: improper variant id for fuel type")
- | Option ->
- let ty = Collections.List.to_cons_nil generics.types in
- let variant_id = Option.get variant_id in
- if variant_id = option_some_id then [ ty ]
- else if variant_id = option_none_id then []
- else
- raise (Failure "Unreachable: improper variant id for option type")
- | Range ->
- let ty = Collections.List.to_cons_nil generics.types in
- assert (variant_id = None);
- [ ty; ty ]
- | Vec | Array | Slice | Str ->
+ | Array | Slice | Str ->
(* Array: when not symbolic values (for instance, because of aggregates),
the array expressions are introduced as struct updates *)
raise (Failure "Attempting to access the fields of an opaque type"))
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index b1680282..6d9b9e15 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -305,19 +305,7 @@ let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
generics.types
| T.Assumed aty -> (
match aty with
- | T.Box | T.Vec ->
- assert (generics.regions = []);
- assert (List.length generics.types = 1);
- assert (generics.const_generics = []);
- generics.types
- | T.Option ->
- assert (generics.regions = []);
- assert (List.length generics.types = 1);
- assert (generics.const_generics = []);
- if adt.V.variant_id = Some T.option_some_id then generics.types
- else if adt.V.variant_id = Some T.option_none_id then []
- else raise (Failure "Unreachable")
- | T.Range ->
+ | T.Box ->
assert (generics.regions = []);
assert (List.length generics.types = 1);
assert (generics.const_generics = []);
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 54221cb1..9c698b51 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -405,8 +405,6 @@ let rec translate_sty (ty : T.sty) : ty =
mk_simpl_tuple_ty generics.types
| T.Assumed aty -> (
match aty with
- | T.Vec -> Adt (Assumed Vec, generics)
- | T.Option -> Adt (Assumed Option, generics)
| T.Box -> (
(* Eliminate the boxes *)
match generics.types with
@@ -418,8 +416,7 @@ let rec translate_sty (ty : T.sty) : ty =
)
| T.Array -> Adt (Assumed Array, generics)
| T.Slice -> Adt (Assumed Slice, generics)
- | T.Str -> Adt (Assumed Str, generics)
- | T.Range -> Adt (Assumed Range, generics)))
+ | T.Str -> Adt (Assumed Str, generics)))
| TypeVar vid -> TypeVar vid
| Literal ty -> Literal ty
| Never -> raise (Failure "Unreachable")
@@ -510,12 +507,9 @@ let translate_type_id (id : T.type_id) : type_id =
| T.Assumed aty ->
let aty =
match aty with
- | T.Vec -> Vec
- | T.Option -> Option
| T.Array -> Array
| T.Slice -> Slice
| T.Str -> Str
- | T.Range -> Range
| T.Box ->
(* Boxes have to be eliminated: this type id shouldn't
be translated *)
@@ -534,8 +528,7 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
let t_generics = translate_fwd_generic_args type_infos generics in
(* Eliminate boxes and simplify tuples *)
match type_id with
- | AdtId _
- | T.Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+ | AdtId _ | T.Assumed (T.Array | T.Slice | T.Str) ->
(* No general parametricity for now *)
assert (
not
@@ -610,8 +603,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
match ty with
| T.Adt (type_id, generics) -> (
match type_id with
- | T.AdtId _
- | Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+ | T.AdtId _ | Assumed (T.Array | T.Slice | T.Str) ->
(* Don't accept ADTs (which are not tuples) with borrows for now *)
assert (not (TypesUtils.ty_has_borrows type_infos ty));
let type_id = translate_type_id type_id in
@@ -815,7 +807,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
| FunId (Assumed aid) ->
assert (lid = None);
{
- can_fail = Assumed.assumed_can_fail aid;
+ can_fail = Assumed.assumed_fun_can_fail aid;
stateful_group = false;
stateful = false;
can_diverge = false;
@@ -1221,9 +1213,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
(* For now, only tuples can contain borrows *)
let adt_id, _ = TypesUtils.ty_as_adt av.ty in
match adt_id with
- | T.AdtId _
- | T.Assumed
- (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+ | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
assert (field_values = []);
None
| T.Tuple ->
@@ -1368,9 +1358,7 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
* vector value upon visiting the "abstraction borrow" node *)
let adt_id, _ = TypesUtils.ty_as_adt av.ty in
match adt_id with
- | T.AdtId _
- | T.Assumed
- (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+ | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
assert (field_values = []);
(ctx, None)
| T.Tuple ->
@@ -2441,17 +2429,12 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
(mk_typed_pattern_from_var var None)
(mk_opt_mplace_texpression scrutinee_mplace scrutinee)
branch
- | T.Assumed (T.Vec | T.Array | T.Slice | T.Str) ->
+ | T.Assumed (T.Array | T.Slice | T.Str) ->
(* We can't expand those values: we can access the fields only
* through the functions provided by the API (note that we don't
* know how to expand values like vectors or arrays, because they have a variable number
* of fields!) *)
raise (Failure "Attempt to expand a non-expandable value")
- | T.Assumed Range -> raise (Failure "Unimplemented")
- | T.Assumed T.Option ->
- (* We shouldn't get there in the "one-branch" case: options have
- * two variants *)
- raise (Failure "Unreachable")
and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
(sv : V.symbolic_value) (v : S.value_aggregate) (e : S.expression)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 8e01c869..35dff9e6 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -297,9 +297,11 @@ let translate_crate_to_pure (crate : A.crate) :
(* Translate all the function *signatures* *)
let assumed_sigs =
List.map
- (fun (id, sg, _, _) ->
- (E.Assumed id, List.map (fun _ -> None) (sg : A.fun_sig).inputs, sg))
- Assumed.assumed_infos
+ (fun (info : Assumed.assumed_fun_info) ->
+ ( E.Assumed info.fun_id,
+ List.map (fun _ -> None) info.fun_sig.inputs,
+ info.fun_sig ))
+ Assumed.assumed_fun_infos
in
let local_sigs =
List.map
@@ -425,11 +427,15 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
(true, kind)
in
(* Extract, if the config instructs to do so (depending on whether the type
- * is opaque or not) *)
- if
+ is opaque or not). Remark: we don't check if the definitions are builtin
+ here but in the function [export_types_group]: the reason is that if one
+ definition in the group is builtin, then we must check that all the
+ definitions are marked builtin *)
+ let extract =
(is_opaque && config.extract_opaque)
|| ((not is_opaque) && config.extract_transparent)
- then (
+ in
+ if extract then (
if extract_decl then
Extract.extract_type_decl ctx fmt type_decl_group kind def;
if extract_extra_info then
@@ -464,41 +470,58 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
List.map (fun id -> Pure.TypeDeclId.Map.find id ctx.trans_types) ids
in
- (* Extract the type declarations.
-
- Because some declaration groups are delimited, we wrap the declarations
- between [{start,end}_type_decl_group].
+ (* Check if the definition are builtin - if yes they must be ignored.
+ Note that if one definition in the group is builtin, then all the
+ definitions must be builtin *)
+ let builtin =
+ let open ExtractBuiltin in
+ let types_map = builtin_types_map () in
+ List.map
+ (fun (def : Pure.type_decl) ->
+ let sname = name_to_simple_name def.name in
+ SimpleNameMap.find_opt sname types_map <> None)
+ defs
+ in
- Ex.:
- ====
- When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate
- the [Datatype] and [End] delimiters in the snippet of code below:
+ if List.exists (fun b -> b) builtin then
+ (* Sanity check *)
+ assert (List.for_all (fun b -> b) builtin)
+ else (
+ (* Extract the type declarations.
+
+ Because some declaration groups are delimited, we wrap the declarations
+ between [{start,end}_type_decl_group].
+
+ Ex.:
+ ====
+ When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate
+ the [Datatype] and [End] delimiters in the snippet of code below:
+
+ {[
+ Datatype:
+ tree =
+ TLeaf 'a
+ | TNode node ;
+
+ node =
+ Node (tree list)
+ End
+ ]}
+ *)
+ Extract.start_type_decl_group ctx fmt is_rec defs;
+ List.iteri
+ (fun i def ->
+ let kind = kind_from_index i in
+ export_type_decl kind def)
+ defs;
+ Extract.end_type_decl_group fmt is_rec defs;
- {[
- Datatype:
- tree =
- TLeaf 'a
- | TNode node ;
-
- node =
- Node (tree list)
- End
- ]}
- *)
- Extract.start_type_decl_group ctx fmt is_rec defs;
- List.iteri
- (fun i def ->
- let kind = kind_from_index i in
- export_type_decl kind def)
- defs;
- Extract.end_type_decl_group fmt is_rec defs;
-
- (* Export the extra information (ex.: [Arguments] instructions in Coq) *)
- List.iteri
- (fun i def ->
- let kind = kind_from_index i in
- export_type_extra_info kind def)
- defs
+ (* Export the extra information (ex.: [Arguments] instructions in Coq) *)
+ List.iteri
+ (fun i def ->
+ let kind = kind_from_index i in
+ export_type_extra_info kind def)
+ defs)
(** Export a global declaration.
@@ -520,12 +543,12 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
&& (((not is_opaque) && config.extract_transparent)
|| (is_opaque && config.extract_opaque))
in
- (* Check if it is an assumed global - if yes, we ignore it because we
+ (* Check if it is a builtin global - if yes, we ignore it because we
map the definition to one in the standard library *)
- let open ExtractAssumed in
+ let open ExtractBuiltin in
let sname = name_to_simple_name global.name in
let extract =
- extract && SimpleNameMap.find_opt sname assumed_globals_map = None
+ extract && SimpleNameMap.find_opt sname builtin_globals_map = None
in
if extract then
(* We don't wrap global declaration groups between calls to functions
@@ -631,91 +654,133 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config)
*)
let export_functions_group (fmt : Format.formatter) (config : gen_config)
(ctx : gen_ctx) (pure_ls : pure_fun_translation list) : unit =
- (* Utility to check a function has a decrease clause *)
- let has_decreases_clause (def : Pure.fun_decl) : bool =
- PureUtils.FunLoopIdSet.mem (def.def_id, def.loop_id)
- ctx.functions_with_decreases_clause
+ (* Check if the definition are builtin - if yes they must be ignored.
+ Note that if one definition in the group is builtin, then all the
+ definitions must be builtin *)
+ let builtin =
+ let open ExtractBuiltin in
+ let funs_map = builtin_funs_map () in
+ List.map
+ (fun (trans : pure_fun_translation) ->
+ let sname = name_to_simple_name trans.fwd.f.basename in
+ SimpleNameMap.find_opt sname funs_map <> None)
+ pure_ls
in
- (* Extract the decrease clauses template bodies *)
- if config.extract_template_decreases_clauses then
- List.iter
- (fun { fwd; _ } ->
- (* We only generate decreases clauses for the forward functions, because
- the termination argument should only depend on the forward inputs.
- The backward functions thus use the same decreases clauses as the
- forward function.
-
- Rem.: we might filter backward functions in {!PureMicroPasses}, but
- we don't remove forward functions. Instead, we remember if we should
- filter those functions at extraction time with a boolean (see the
- type of the [pure_ls] input parameter).
- *)
- let extract_decrease decl =
- let has_decr_clause = has_decreases_clause decl in
- if has_decr_clause then
- match !Config.backend with
- | Lean ->
- Extract.extract_template_lean_termination_and_decreasing ctx fmt
- decl
- | FStar ->
- Extract.extract_template_fstar_decreases_clause ctx fmt decl
- | Coq ->
- raise (Failure "Coq doesn't have decreases/termination clauses")
- | HOL4 ->
- raise
- (Failure "HOL4 doesn't have decreases/termination clauses")
- in
- extract_decrease fwd.f;
- List.iter extract_decrease fwd.loops)
- pure_ls;
-
- (* Concatenate the function definitions, filtering the useless forward
- * functions. *)
- let decls =
- List.concat
- (List.map
- (fun { keep_fwd; fwd; backs } ->
- let fwd = if keep_fwd then List.append fwd.loops [ fwd.f ] else [] in
- let backs : Pure.fun_decl list =
- List.concat
- (List.map (fun back -> List.append back.loops [ back.f ]) backs)
- in
- List.append fwd backs)
- pure_ls)
- in
+ if List.exists (fun b -> b) builtin then
+ (* Sanity check *)
+ assert (List.for_all (fun b -> b) builtin)
+ else
+ (* Utility to check a function has a decrease clause *)
+ let has_decreases_clause (def : Pure.fun_decl) : bool =
+ PureUtils.FunLoopIdSet.mem (def.def_id, def.loop_id)
+ ctx.functions_with_decreases_clause
+ in
- (* Extract the function definitions *)
- (if config.extract_fun_decls then
- (* Group the mutually recursive definitions *)
- let subgroups = ReorderDecls.group_reorder_fun_decls decls in
+ (* Extract the decrease clauses template bodies *)
+ if config.extract_template_decreases_clauses then
+ List.iter
+ (fun { fwd; _ } ->
+ (* We only generate decreases clauses for the forward functions, because
+ the termination argument should only depend on the forward inputs.
+ The backward functions thus use the same decreases clauses as the
+ forward function.
+
+ Rem.: we might filter backward functions in {!PureMicroPasses}, but
+ we don't remove forward functions. Instead, we remember if we should
+ filter those functions at extraction time with a boolean (see the
+ type of the [pure_ls] input parameter).
+ *)
+ let extract_decrease decl =
+ let has_decr_clause = has_decreases_clause decl in
+ if has_decr_clause then
+ match !Config.backend with
+ | Lean ->
+ Extract.extract_template_lean_termination_and_decreasing ctx
+ fmt decl
+ | FStar ->
+ Extract.extract_template_fstar_decreases_clause ctx fmt decl
+ | Coq ->
+ raise
+ (Failure "Coq doesn't have decreases/termination clauses")
+ | HOL4 ->
+ raise
+ (Failure "HOL4 doesn't have decreases/termination clauses")
+ in
+ extract_decrease fwd.f;
+ List.iter extract_decrease fwd.loops)
+ pure_ls;
+
+ (* Concatenate the function definitions, filtering the useless forward
+ * functions. *)
+ let decls =
+ List.concat
+ (List.map
+ (fun { keep_fwd; fwd; backs } ->
+ let fwd =
+ if keep_fwd then List.append fwd.loops [ fwd.f ] else []
+ in
+ let backs : Pure.fun_decl list =
+ List.concat
+ (List.map
+ (fun back -> List.append back.loops [ back.f ])
+ backs)
+ in
+ List.append fwd backs)
+ pure_ls)
+ in
- (* Extract the subgroups *)
- let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit =
- export_functions_group_scc fmt config ctx is_rec decls
- in
- List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups);
-
- (* Insert unit tests if necessary *)
- if config.test_trans_unit_functions then
- List.iter
- (fun trans ->
- if trans.keep_fwd then
- Extract.extract_unit_test_if_unit_fun ctx fmt trans.fwd.f)
- pure_ls
+ (* Extract the function definitions *)
+ (if config.extract_fun_decls then
+ (* Group the mutually recursive definitions *)
+ let subgroups = ReorderDecls.group_reorder_fun_decls decls in
+
+ (* Extract the subgroups *)
+ let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit =
+ export_functions_group_scc fmt config ctx is_rec decls
+ in
+ List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups);
+
+ (* Insert unit tests if necessary *)
+ if config.test_trans_unit_functions then
+ List.iter
+ (fun trans ->
+ if trans.keep_fwd then
+ Extract.extract_unit_test_if_unit_fun ctx fmt trans.fwd.f)
+ pure_ls
(** Export a trait declaration. *)
let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
(ctx : gen_ctx) (trait_decl_id : Pure.trait_decl_id) : unit =
let trait_decl = T.TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in
- let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
- Extract.extract_trait_decl ctx fmt trait_decl
+ (* Check if the trait declaration is builtin, in which case we ignore it *)
+ let open ExtractBuiltin in
+ let sname = name_to_simple_name trait_decl.name in
+ if SimpleNameMap.find_opt sname (builtin_trait_decls_map ()) = None then
+ let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in
+ Extract.extract_trait_decl ctx fmt trait_decl
+ else ()
(** Export a trait implementation. *)
let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
(ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit =
+ (* Lookup the definition *)
let trait_impl = T.TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in
- Extract.extract_trait_impl ctx fmt trait_impl
+ let trait_decl =
+ Pure.TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id
+ ctx.trans_trait_decls
+ in
+ (* Check if the trait implementation is builtin *)
+ let builtin_info =
+ let open ExtractBuiltin in
+ let type_sname = name_to_simple_name trait_impl.name in
+ let trait_sname = name_to_simple_name trait_decl.name in
+ SimpleNamePairMap.find_opt (type_sname, trait_sname)
+ (builtin_trait_impls_map ())
+ in
+ match builtin_info with
+ | None -> Extract.extract_trait_impl ctx fmt trait_impl
+ | Some _ -> ()
(** A generic utility to generate the extracted definitions: as we may want to
split the definitions between different files (or not), we can control
@@ -786,37 +851,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
if config.extract_state_type && config.extract_fun_decls then
export_state_type ();
- (* Obsolete: (TODO: remove) For Lean we parameterize the entire development by a section
- variable called opaque_defs, of type OpaqueDefs. The code below emits the type
- definition for OpaqueDefs, which is a structure, in which each field is one of the
- functions marked as Opaque. We emit the `structure ...` bit here, then rely on
- `extract_fun_decl` to be aware of this, and skip the keyword (e.g. "axiom" or "val")
- so as to generate valid syntax for records.
-
- We also generate such a structure only if there actually are opaque definitions. *)
- let wrap_in_sig =
- config.extract_opaque && config.extract_fun_decls
- && !Config.wrap_opaque_in_sig
- &&
- let _, opaque_funs = crate_has_opaque_decls ctx true in
- opaque_funs
- in
- if wrap_in_sig then (
- (* We change the name of the structure depending on whether we *only*
- extract opaque definitions, or if we extract all definitions *)
- let struct_name =
- if config.extract_transparent then "Definitions" else "OpaqueDefs"
- in
- Format.pp_print_break fmt 0 0;
- Format.pp_open_vbox fmt ctx.indent_incr;
- Format.pp_print_string fmt ("structure " ^ struct_name ^ " where");
- Format.pp_print_break fmt 0 0);
List.iter export_decl_group ctx.crate.declarations;
if config.extract_state_type && not config.extract_fun_decls then
- export_state_type ();
-
- if wrap_in_sig then Format.pp_close_box fmt ()
+ export_state_type ()
type extract_file_info = {
filename : string;
@@ -964,10 +1002,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
(fun (id, _) -> strict_collisions id)
(IdMap.bindings names_map.id_to_name)
in
- let is_opaque = false in
List.fold_left
(* id_to_string: we shouldn't need to use it *)
- (fun m (id, n) -> names_map_add show_id is_opaque id n m)
+ (fun m (id, n) -> names_map_add show_id id n m)
empty_names_map ids
in
@@ -1028,7 +1065,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
strict_names_map;
fmt;
indent_incr = 2;
- use_opaque_pre = !Config.split_files;
use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
fun_name_info = PureUtils.RegularFunIdMap.empty;
trait_decl_id = None (* None by default *);
@@ -1038,6 +1074,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
trans_types;
trans_funs;
functions_with_decreases_clause = rec_functions;
+ types_filter_type_args_map = Pure.TypeDeclId.Map.empty;
+ funs_filter_type_args_map = Pure.FunDeclId.Map.empty;
}
in
@@ -1324,7 +1362,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
interface = true;
}
in
- let ctx = { ctx with use_opaque_pre = false } in
let file_info =
{
filename = opaque_filename;
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 4a187893..16f8c5f9 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -168,9 +168,7 @@ 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 | Slice | Array | Str | Range)),
- generics ) ->
+ | Adt ((Tuple | Assumed (Box | Slice | Array | Str)), generics) ->
(* Nothing to update: just explore the type parameters *)
List.fold_left
(fun ty_info ty -> analyze expl_info ty_info ty)
diff --git a/compiler/dune b/compiler/dune
index 2f5a0a44..4ec46b70 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -22,8 +22,8 @@
Expressions
ExpressionsUtils
Extract
- ExtractAssumed
ExtractBase
+ ExtractBuiltin
FunsAnalysis
Identifiers
InterpreterBorrowsCore
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-12 09:10:39 +0000