From 316c386bcdbb66accdd65a311ca978b6d4606695 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 17 Aug 2023 14:17:47 +0200 Subject: Make a minor modification --- compiler/Assumed.ml | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'compiler/Assumed.ml') diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 11cd5666..25462504 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -86,7 +86,6 @@ module Sig = struct let output = tvar_0 (* T *) in { region_params; - num_early_bound_regions = 0; regions_hierarchy; type_params; const_generic_params = empty_const_generic_params; @@ -98,7 +97,6 @@ module Sig = struct let box_new_sig : A.fun_sig = { region_params = []; - num_early_bound_regions = 0; regions_hierarchy = []; type_params = [ type_param_0 ] (* *); const_generic_params = empty_const_generic_params; @@ -110,7 +108,6 @@ module Sig = struct let box_free_sig : A.fun_sig = { region_params = []; - num_early_bound_regions = 0; regions_hierarchy = []; type_params = [ type_param_0 ] (* *); const_generic_params = empty_const_generic_params; @@ -128,7 +125,6 @@ module Sig = struct let regions_hierarchy = [ region_group_0 ] (* <'a> *) in { region_params; - num_early_bound_regions = 0; regions_hierarchy; type_params = [ type_param_0 ] (* *); const_generic_params = empty_const_generic_params; @@ -152,7 +148,6 @@ module Sig = struct let output = mk_vec_ty tvar_0 (* Vec *) in { region_params; - num_early_bound_regions = 0; regions_hierarchy; type_params; const_generic_params = empty_const_generic_params; @@ -175,7 +170,6 @@ module Sig = struct let output = mk_unit_ty (* () *) in { region_params; - num_early_bound_regions = 0; regions_hierarchy; type_params; const_generic_params = empty_const_generic_params; @@ -199,7 +193,6 @@ module Sig = struct let output = mk_unit_ty (* () *) in { region_params; - num_early_bound_regions = 0; regions_hierarchy; type_params; const_generic_params = empty_const_generic_params; @@ -219,7 +212,6 @@ module Sig = struct let output = mk_usize_ty (* usize *) in { region_params; - num_early_bound_regions = 0; regions_hierarchy; type_params; const_generic_params = empty_const_generic_params; @@ -244,7 +236,6 @@ module Sig = struct let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in { region_params; - num_early_bound_regions = 0; regions_hierarchy; type_params; const_generic_params = empty_const_generic_params; @@ -296,7 +287,6 @@ module Sig = struct in { region_params; - num_early_bound_regions = 0; regions_hierarchy; type_params; const_generic_params = cgs; @@ -362,7 +352,6 @@ module Sig = struct let output = mk_usize_ty (* usize *) in { region_params; - num_early_bound_regions = 0; regions_hierarchy; type_params; const_generic_params = empty_const_generic_params; -- cgit v1.2.3 From 6f22190cba92a44b6c74bfcce8f5ed142a68e195 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 31 Aug 2023 12:47:43 +0200 Subject: Start adding support for traits --- compiler/Assumed.ml | 188 ++++++++++++++++++++-------------------------------- 1 file changed, 72 insertions(+), 116 deletions(-) (limited to 'compiler/Assumed.ml') diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 25462504..e156c335 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -63,75 +63,81 @@ module Sig = struct let empty_const_generic_params : T.const_generic_var list = [] + let mk_generic_args regions types const_generics : T.sgeneric_args = + { regions; types; const_generics; trait_refs = [] } + + let mk_generic_params regions types const_generics : T.generic_params = + { regions; types; const_generics; trait_clauses = [] } + let mk_ref_ty (r : T.RegionVarId.id T.region) (ty : T.sty) (is_mut : bool) : T.sty = let ref_kind = if is_mut then T.Mut else T.Shared in mk_ref_ty r ty ref_kind let mk_array_ty (ty : T.sty) (cg : T.const_generic) : T.sty = - Adt (Assumed Array, [], [ ty ], [ cg ]) + Adt (Assumed Array, mk_generic_args [] [ ty ] [ cg ]) + + let mk_slice_ty (ty : T.sty) : T.sty = + Adt (Assumed Slice, mk_generic_args [] [ ty ] []) - let mk_slice_ty (ty : T.sty) : T.sty = Adt (Assumed Slice, [], [ ty ], []) - let range_ty : T.sty = Adt (Assumed Range, [], [ usize_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 = [] } + in + { + generics; + preds; + parent_params_info = None; + regions_hierarchy; + inputs; + output; + } (** [fn(&'a mut T, T) -> T] *) let mem_replace_sig : A.fun_sig = (* The signature fields *) - let region_params = [ region_param_0 ] (* <'a> *) in + let regions = [ region_param_0 ] (* <'a> *) in let regions_hierarchy = [ region_group_0 ] (* [{<'a>}] *) in - let type_params = [ type_param_0 ] (* *) in + let types = [ type_param_0 ] (* *) 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 - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output (** [fn(T) -> Box] *) let box_new_sig : A.fun_sig = - { - region_params = []; - regions_hierarchy = []; - type_params = [ type_param_0 ] (* *); - const_generic_params = empty_const_generic_params; - inputs = [ tvar_0 (* T *) ]; - output = mk_box_ty tvar_0 (* Box *); - } + let generics = mk_generic_params [] [ type_param_0 ] [] (* *) in + let regions_hierarchy = [] in + let inputs = [ tvar_0 (* T *) ] in + let output = mk_box_ty tvar_0 (* Box *) in + mk_sig generics regions_hierarchy inputs output (** [fn(Box) -> ()] *) let box_free_sig : A.fun_sig = - { - region_params = []; - regions_hierarchy = []; - type_params = [ type_param_0 ] (* *); - const_generic_params = empty_const_generic_params; - inputs = [ mk_box_ty tvar_0 (* Box *) ]; - output = mk_unit_ty (* () *); - } + let generics = mk_generic_params [] [ type_param_0 ] [] (* *) in + let regions_hierarchy = [] in + let inputs = [ mk_box_ty tvar_0 (* Box *) ] in + 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) -> &'a (mut) T] *) let box_deref_gen_sig (is_mut : bool) : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - { - region_params; - regions_hierarchy; - type_params = [ type_param_0 ] (* *); - const_generic_params = empty_const_generic_params; - inputs = - [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box *) ]; - output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *); - } + let inputs = + [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box *) ] + 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) -> &'a T] *) let box_deref_shared_sig = box_deref_gen_sig false @@ -141,26 +147,18 @@ module Sig = struct (** [fn() -> Vec] *) let vec_new_sig : A.fun_sig = - let region_params = [] in + let generics = mk_generic_params [] [ type_param_0 ] [] (* *) in let regions_hierarchy = [] in - let type_params = [ type_param_0 ] (* *) in let inputs = [] in let output = mk_vec_ty tvar_0 (* Vec *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output (** [fn(&'a mut Vec, T)] *) let vec_push_sig : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* *) in let inputs = [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec *); @@ -168,21 +166,14 @@ module Sig = struct ] in let output = mk_unit_ty (* () *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output (** [fn(&'a mut Vec, usize, T)] *) let vec_insert_sig : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* *) in let inputs = [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec *); @@ -191,42 +182,28 @@ module Sig = struct ] in let output = mk_unit_ty (* () *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output (** [fn(&'a Vec) -> usize] *) let vec_len_sig : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* *) in let inputs = [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) false (* &'a Vec *) ] in let output = mk_usize_ty (* usize *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output (** Helper: [fn(&'a (mut) Vec, usize) -> &'a (mut) T] *) let vec_index_gen_sig (is_mut : bool) : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* *) in let inputs = [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) is_mut (* &'a (mut) Vec *); @@ -234,14 +211,7 @@ module Sig = struct ] in let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output (** [fn(&'a Vec, usize) -> &'a T] *) let vec_index_shared_sig : A.fun_sig = vec_index_gen_sig false @@ -266,10 +236,10 @@ module Sig = struct let mk_array_slice_borrow_sig (cgs : T.const_generic_var list) (input_ty : T.TypeVarId.id -> T.sty) (index_ty : T.sty option) (output_ty : T.TypeVarId.id -> T.sty) (is_mut : bool) : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] cgs (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* *) in let inputs = [ mk_ref_ty rvar_0 @@ -285,14 +255,7 @@ module Sig = struct (output_ty type_param_0.index) is_mut (* &'a (mut) output_ty *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = cgs; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : A.fun_sig = (* Array *) @@ -342,22 +305,15 @@ module Sig = struct [fn(&'a [T]) -> usize] *) let slice_len_sig : A.fun_sig = - (* The signature fields *) - let region_params = [ region_param_0 ] in + let generics = + mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) + in let regions_hierarchy = [ region_group_0 ] (* <'a> *) in - let type_params = [ type_param_0 ] (* *) in let inputs = [ mk_ref_ty rvar_0 (mk_slice_ty tvar_0) false (* &'a [T] *) ] in let output = mk_usize_ty (* usize *) in - { - region_params; - regions_hierarchy; - type_params; - const_generic_params = empty_const_generic_params; - inputs; - output; - } + mk_sig generics regions_hierarchy inputs output end type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name -- cgit v1.2.3 From 0f0e4be7dc746e2676db33f850bbeddf239eaec8 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 13 Oct 2023 00:40:37 +0200 Subject: Add sup --- compiler/Assumed.ml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'compiler/Assumed.ml') diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index e156c335..109175af 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -298,6 +298,19 @@ module Sig = struct let array_subslice_sig (is_mut : bool) = mk_array_slice_subslice_sig true is_mut + let array_repeat_sig = + let generics = + (* *) + mk_generic_params [] [ type_param_0 ] [ cg_param_0 ] + in + let regions_hierarchy = [] (* <> *) in + let inputs = [ tvar_0 (* T *) ] in + let output = + (* [T; N] *) + mk_array_ty tvar_0 cgvar_0 + in + mk_sig generics regions_hierarchy inputs output + let slice_subslice_sig (is_mut : bool) = mk_array_slice_subslice_sig false is_mut @@ -384,6 +397,8 @@ let assumed_infos : assumed_info list = Sig.array_subslice_sig true, true, to_name [ "@ArraySubsliceMut" ] ); + (* Array Repeat *) + (ArrayRepeat, Sig.array_repeat_sig, false, to_name [ "@ArrayRepeat" ]); (* Slice Index *) ( SliceIndexShared, Sig.slice_index_sig false, -- cgit v1.2.3 From f11d5186b467df318f7c09eedf8b5629c165b453 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 20 Oct 2023 15:05:00 +0200 Subject: Start updating to handle function pointers --- compiler/Assumed.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/Assumed.ml') diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 109175af..b1ec0660 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -347,7 +347,7 @@ let assumed_infos : assumed_info list = let vec_pre = [ "alloc"; "vec"; "Vec" ] in let index_pre = [ "core"; "ops"; "index" ] in [ - (A.Replace, Sig.mem_replace_sig, false, to_name [ "core"; "mem"; "replace" ]); + (Replace, Sig.mem_replace_sig, false, to_name [ "core"; "mem"; "replace" ]); (BoxNew, Sig.box_new_sig, false, to_name [ "alloc"; "boxed"; "Box"; "new" ]); ( BoxFree, Sig.box_free_sig, -- cgit v1.2.3 From 838cc86cb2efc8fb64a94a94b58b82d66844e7e4 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 23 Oct 2023 13:47:39 +0200 Subject: Remove some assumed types and add more support for builtin definitions --- compiler/Assumed.ml | 254 ++++++++++++---------------------------------------- 1 file changed, 59 insertions(+), 195 deletions(-) (limited to 'compiler/Assumed.ml') 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(&'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 ] (* *) 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) -> Box] *) let box_new_sig : A.fun_sig = let generics = mk_generic_params [] [ type_param_0 ] [] (* *) 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) -> &'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 *) ] - 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) -> &'a T] *) - let box_deref_shared_sig = box_deref_gen_sig false - - (** [fn<'a, T>(&'a mut Box) -> &'a mut T] *) - let box_deref_mut_sig = box_deref_gen_sig true - - (** [fn() -> Vec] *) - let vec_new_sig : A.fun_sig = - let generics = mk_generic_params [] [ type_param_0 ] [] (* *) in - let regions_hierarchy = [] in - let inputs = [] in - let output = mk_vec_ty tvar_0 (* Vec *) in - mk_sig generics regions_hierarchy inputs output - - (** [fn(&'a mut Vec, 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 *); - tvar_0 (* T *); - ] - in - let output = mk_unit_ty (* () *) in - mk_sig generics regions_hierarchy inputs output - - (** [fn(&'a mut Vec, 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 *); - mk_usize_ty (* usize *); - tvar_0 (* T *); - ] - in - let output = mk_unit_ty (* () *) in - mk_sig generics regions_hierarchy inputs output - - (** [fn(&'a Vec) -> 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 *) ] - in - let output = mk_usize_ty (* usize *) in - mk_sig generics regions_hierarchy inputs output - - (** Helper: - [fn(&'a (mut) Vec, 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 *); - 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(&'a Vec, usize) -> &'a T] *) - let vec_index_shared_sig : A.fun_sig = vec_index_gen_sig false - - (** [fn(&'a mut Vec, 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 *) - 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 *) - 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 = (* *) @@ -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(&'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 -- cgit v1.2.3 From ece74df70f12790bab7ecfe0c590c2c637e89801 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 25 Oct 2023 11:40:31 +0200 Subject: Update following the addition of raw pointers --- compiler/Assumed.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'compiler/Assumed.ml') diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 94fb7a72..79f6b0d4 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -85,6 +85,7 @@ module Sig = struct { regions_outlive = []; types_outlive = []; trait_type_constraints = [] } in { + is_unsafe = false; generics; preds; parent_params_info = None; -- cgit v1.2.3