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 From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 19:28:56 +0100 Subject: Remove the 'r type variable from the ty type definition --- compiler/Assumed.ml | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) (limited to 'compiler/Assumed.ml') diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 79f6b0d4..d8f19173 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -37,11 +37,11 @@ module A = LlbcAst module Sig = struct (** A few utilities *) - let rvar_id_0 = T.RegionVarId.of_int 0 - let rvar_0 : T.RegionVarId.id T.region = T.Var rvar_id_0 + let rvar_id_0 = T.RegionId.of_int 0 + let rvar_0 : T.region = T.RVar rvar_id_0 let rg_id_0 = T.RegionGroupId.of_int 0 let tvar_id_0 = T.TypeVarId.of_int 0 - let tvar_0 : T.sty = T.TypeVar tvar_id_0 + let tvar_0 : T.ty = T.TypeVar tvar_id_0 let cgvar_id_0 = T.ConstGenericVarId.of_int 0 let cgvar_0 : T.const_generic = T.ConstGenericVar cgvar_id_0 @@ -49,36 +49,35 @@ module Sig = struct let region_param_0 : T.region_var = { T.index = rvar_id_0; name = Some "'a" } (** Region group: [{ parent={}; regions:{'a of id 0} }] *) - let region_group_0 : T.region_var_group = + let region_group_0 : T.region_group = { T.id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] } (** Type parameter [T] of id 0 *) let type_param_0 : T.type_var = { T.index = tvar_id_0; name = "T" } - let usize_ty : T.sty = T.Literal (Integer Usize) + let usize_ty : T.ty = T.TLiteral (TInteger Usize) (** Const generic parameter [const N : usize] of id 0 *) let cg_param_0 : T.const_generic_var = - { T.index = cgvar_id_0; name = "N"; ty = Integer Usize } + { T.index = cgvar_id_0; name = "N"; ty = TInteger Usize } let empty_const_generic_params : T.const_generic_var list = [] - let mk_generic_args regions types const_generics : T.sgeneric_args = + let mk_generic_args regions types const_generics : T.generic_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 mk_ref_ty (r : T.region) (ty : T.ty) (is_mut : bool) : T.ty = 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, mk_generic_args [] [ ty ] [ cg ]) + let mk_array_ty (ty : T.ty) (cg : T.const_generic) : T.ty = + TAdt (TAssumed TArray, 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.ty) : T.ty = + TAdt (TAssumed TSlice, mk_generic_args [] [ ty ] []) let mk_sig generics regions_hierarchy inputs output : A.fun_sig = let preds : T.predicates = @@ -125,8 +124,8 @@ module Sig = struct borrow. *) 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 = + (input_ty : T.TypeVarId.id -> T.ty) (index_ty : T.ty option) + (output_ty : T.TypeVarId.id -> T.ty) (is_mut : bool) : A.fun_sig = let generics = mk_generic_params [ region_param_0 ] [ type_param_0 ] cgs (* <'a, T> *) in -- cgit v1.2.3 From 0a5859fbb7bcd99bfa221eaf1af029ff660bf963 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 19:35:24 +0100 Subject: Rename some variants --- 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 d8f19173..5622ef26 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -43,7 +43,7 @@ module Sig = struct let tvar_id_0 = T.TypeVarId.of_int 0 let tvar_0 : T.ty = T.TypeVar tvar_id_0 let cgvar_id_0 = T.ConstGenericVarId.of_int 0 - let cgvar_0 : T.const_generic = T.ConstGenericVar cgvar_id_0 + let cgvar_0 : T.const_generic = T.CGVar cgvar_id_0 (** Region 'a of id 0 *) let region_param_0 : T.region_var = { T.index = rvar_id_0; name = Some "'a" } -- cgit v1.2.3 From 6ef68fa9ffd4caec09677ee2800a778080d6da34 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 20:04:11 +0100 Subject: Prefix variants related to types with "T" --- compiler/Assumed.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'compiler/Assumed.ml') diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index 5622ef26..cf81502c 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -41,7 +41,7 @@ module Sig = struct let rvar_0 : T.region = T.RVar rvar_id_0 let rg_id_0 = T.RegionGroupId.of_int 0 let tvar_id_0 = T.TypeVarId.of_int 0 - let tvar_0 : T.ty = T.TypeVar tvar_id_0 + let tvar_0 : T.ty = T.TVar tvar_id_0 let cgvar_id_0 = T.ConstGenericVarId.of_int 0 let cgvar_0 : T.const_generic = T.CGVar cgvar_id_0 @@ -150,13 +150,13 @@ module Sig = struct let mk_array_slice_index_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) + if is_array then mk_array_ty (T.TVar id) cgvar_0 + else mk_slice_ty (T.TVar id) in (* usize *) let index_ty = usize_ty in (* T *) - let output_ty id = T.TypeVar id in + let output_ty id = T.TVar 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 @@ -165,9 +165,9 @@ module Sig = struct let array_to_slice_sig (is_mut : bool) : A.fun_sig = (* Array *) - let input_ty id = mk_array_ty (T.TypeVar id) cgvar_0 in + let input_ty id = mk_array_ty (T.TVar id) cgvar_0 in (* Slice *) - let output_ty id = mk_slice_ty (T.TypeVar id) in + let output_ty id = mk_slice_ty (T.TVar id) in let cgs = [ cg_param_0 ] in mk_array_slice_borrow_sig cgs input_ty None output_ty is_mut -- cgit v1.2.3 From 6c88d30031255c0ac612b67bb5b3c20c2f07e563 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 13 Nov 2023 13:27:02 +0100 Subject: Add RegionsHierarchy.ml --- compiler/Assumed.ml | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) (limited to 'compiler/Assumed.ml') diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index cf81502c..aa0cfccf 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -79,7 +79,7 @@ module Sig = struct let mk_slice_ty (ty : T.ty) : T.ty = TAdt (TAssumed TSlice, mk_generic_args [] [ ty ] []) - let mk_sig generics regions_hierarchy inputs output : A.fun_sig = + let mk_sig generics inputs output : A.fun_sig = let preds : T.predicates = { regions_outlive = []; types_outlive = []; trait_type_constraints = [] } in @@ -88,7 +88,6 @@ module Sig = struct generics; preds; parent_params_info = None; - regions_hierarchy; inputs; output; } @@ -96,18 +95,16 @@ module Sig = struct (** [fn(T) -> Box] *) let box_new_sig : A.fun_sig = 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 + mk_sig generics inputs output (** [fn(Box) -> ()] *) let box_free_sig : A.fun_sig = 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 + mk_sig generics inputs output (** Array/slice functions *) @@ -129,7 +126,6 @@ module Sig = struct let generics = mk_generic_params [ region_param_0 ] [ type_param_0 ] cgs (* <'a, T> *) in - let regions_hierarchy = [ region_group_0 ] (* <'a> *) in let inputs = [ mk_ref_ty rvar_0 @@ -145,7 +141,7 @@ module Sig = struct (output_ty type_param_0.index) is_mut (* &'a (mut) output_ty *) in - mk_sig generics regions_hierarchy inputs output + mk_sig generics inputs output let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : A.fun_sig = (* Array *) @@ -176,13 +172,12 @@ module Sig = struct (* *) 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 + mk_sig generics inputs output (** Helper: [fn(&'a [T]) -> usize] @@ -191,12 +186,11 @@ module Sig = struct 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_slice_ty tvar_0) false (* &'a [T] *) ] in let output = mk_usize_ty (* usize *) in - mk_sig generics regions_hierarchy inputs output + mk_sig generics inputs output end type raw_assumed_fun_info = -- cgit v1.2.3 From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 15 Nov 2023 22:03:21 +0100 Subject: Start updating the name type, cleanup the names and the module abbrevs --- compiler/Assumed.ml | 123 ++++++++++++++++++++++++---------------------------- 1 file changed, 57 insertions(+), 66 deletions(-) (limited to 'compiler/Assumed.ml') diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml index aa0cfccf..6aec626a 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -29,58 +29,57 @@ ]} *) -open Names +open Types open TypesUtils -module T = Types -module A = LlbcAst +open LlbcAst module Sig = struct (** A few utilities *) - let rvar_id_0 = T.RegionId.of_int 0 - let rvar_0 : T.region = T.RVar rvar_id_0 - let rg_id_0 = T.RegionGroupId.of_int 0 - let tvar_id_0 = T.TypeVarId.of_int 0 - let tvar_0 : T.ty = T.TVar tvar_id_0 - let cgvar_id_0 = T.ConstGenericVarId.of_int 0 - let cgvar_0 : T.const_generic = T.CGVar cgvar_id_0 + let rvar_id_0 = RegionId.of_int 0 + let rvar_0 : region = RVar rvar_id_0 + let rg_id_0 = RegionGroupId.of_int 0 + let tvar_id_0 = TypeVarId.of_int 0 + let tvar_0 : ty = TVar tvar_id_0 + let cgvar_id_0 = ConstGenericVarId.of_int 0 + let cgvar_0 : const_generic = CGVar cgvar_id_0 (** Region 'a of id 0 *) - let region_param_0 : T.region_var = { T.index = rvar_id_0; name = Some "'a" } + let region_param_0 : region_var = { index = rvar_id_0; name = Some "'a" } (** Region group: [{ parent={}; regions:{'a of id 0} }] *) - let region_group_0 : T.region_group = - { T.id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] } + let region_group_0 : region_group = + { id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] } (** Type parameter [T] of id 0 *) - let type_param_0 : T.type_var = { T.index = tvar_id_0; name = "T" } + let type_param_0 : type_var = { index = tvar_id_0; name = "T" } - let usize_ty : T.ty = T.TLiteral (TInteger Usize) + let usize_ty : ty = TLiteral (TInteger Usize) (** Const generic parameter [const N : usize] of id 0 *) - let cg_param_0 : T.const_generic_var = - { T.index = cgvar_id_0; name = "N"; ty = TInteger Usize } + let cg_param_0 : const_generic_var = + { index = cgvar_id_0; name = "N"; ty = TInteger Usize } - let empty_const_generic_params : T.const_generic_var list = [] + let empty_const_generic_params : const_generic_var list = [] - let mk_generic_args regions types const_generics : T.generic_args = + let mk_generic_args regions types const_generics : generic_args = { regions; types; const_generics; trait_refs = [] } - let mk_generic_params regions types const_generics : T.generic_params = + let mk_generic_params regions types const_generics : generic_params = { regions; types; const_generics; trait_clauses = [] } - let mk_ref_ty (r : T.region) (ty : T.ty) (is_mut : bool) : T.ty = - let ref_kind = if is_mut then T.Mut else T.Shared in + let mk_ref_ty (r : region) (ty : ty) (is_mut : bool) : ty = + let ref_kind = if is_mut then RMut else RShared in mk_ref_ty r ty ref_kind - let mk_array_ty (ty : T.ty) (cg : T.const_generic) : T.ty = + let mk_array_ty (ty : ty) (cg : const_generic) : ty = TAdt (TAssumed TArray, mk_generic_args [] [ ty ] [ cg ]) - let mk_slice_ty (ty : T.ty) : T.ty = + let mk_slice_ty (ty : ty) : ty = TAdt (TAssumed TSlice, mk_generic_args [] [ ty ] []) - let mk_sig generics inputs output : A.fun_sig = - let preds : T.predicates = + let mk_sig generics inputs output : fun_sig = + let preds : predicates = { regions_outlive = []; types_outlive = []; trait_type_constraints = [] } in { @@ -93,14 +92,14 @@ module Sig = struct } (** [fn(T) -> Box] *) - let box_new_sig : A.fun_sig = + let box_new_sig : fun_sig = let generics = mk_generic_params [] [ type_param_0 ] [] (* *) in let inputs = [ tvar_0 (* T *) ] in let output = mk_box_ty tvar_0 (* Box *) in mk_sig generics inputs output (** [fn(Box) -> ()] *) - let box_free_sig : A.fun_sig = + let box_free_sig : fun_sig = let generics = mk_generic_params [] [ type_param_0 ] [] (* *) in let inputs = [ mk_box_ty tvar_0 (* Box *) ] in let output = mk_unit_ty (* () *) in @@ -120,9 +119,9 @@ module Sig = struct The [mut_borrow] boolean controls whether we use a shared or a mutable borrow. *) - let mk_array_slice_borrow_sig (cgs : T.const_generic_var list) - (input_ty : T.TypeVarId.id -> T.ty) (index_ty : T.ty option) - (output_ty : T.TypeVarId.id -> T.ty) (is_mut : bool) : A.fun_sig = + let mk_array_slice_borrow_sig (cgs : const_generic_var list) + (input_ty : TypeVarId.id -> ty) (index_ty : ty option) + (output_ty : TypeVarId.id -> ty) (is_mut : bool) : fun_sig = let generics = mk_generic_params [ region_param_0 ] [ type_param_0 ] cgs (* <'a, T> *) in @@ -143,27 +142,26 @@ module Sig = struct in mk_sig generics inputs output - let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : A.fun_sig = + let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : fun_sig = (* Array *) let input_ty id = - if is_array then mk_array_ty (T.TVar id) cgvar_0 - else mk_slice_ty (T.TVar id) + if is_array then mk_array_ty (TVar id) cgvar_0 else mk_slice_ty (TVar id) in (* usize *) let index_ty = usize_ty in (* T *) - let output_ty id = T.TVar id in + let output_ty id = TVar 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_index_sig (is_mut : bool) = mk_array_slice_index_sig true is_mut let slice_index_sig (is_mut : bool) = mk_array_slice_index_sig false is_mut - let array_to_slice_sig (is_mut : bool) : A.fun_sig = + let array_to_slice_sig (is_mut : bool) : fun_sig = (* Array *) - let input_ty id = mk_array_ty (T.TVar id) cgvar_0 in + let input_ty id = mk_array_ty (TVar id) cgvar_0 in (* Slice *) - let output_ty id = mk_slice_ty (T.TVar id) in + let output_ty id = mk_slice_ty (TVar id) in let cgs = [ cg_param_0 ] in mk_array_slice_borrow_sig cgs input_ty None output_ty is_mut @@ -182,7 +180,7 @@ module Sig = struct (** Helper: [fn(&'a [T]) -> usize] *) - let slice_len_sig : A.fun_sig = + let slice_len_sig : fun_sig = let generics = mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *) in @@ -194,13 +192,13 @@ module Sig = struct end type raw_assumed_fun_info = - A.assumed_fun_id * A.fun_sig * bool * name * bool list option + assumed_fun_id * fun_sig * bool * string * bool list option type assumed_fun_info = { - fun_id : A.assumed_fun_id; - fun_sig : A.fun_sig; + fun_id : assumed_fun_id; + fun_sig : fun_sig; can_fail : bool; - name : name; + name : string; keep_types : bool list option; (** We may want to filter some type arguments. @@ -226,70 +224,63 @@ let mk_assumed_fun_info (raw : raw_assumed_fun_info) : assumed_fun_info = *) let raw_assumed_fun_infos : raw_assumed_fun_info list = [ + (* TODO: the names are not correct ("Box" should be an impl elem for instance) + but it's not important) *) ( BoxNew, Sig.box_new_sig, false, - to_name [ "alloc"; "boxed"; "Box"; "new" ], + "alloc::boxed::Box::new", Some [ true; false ] ); (* BoxFree shouldn't be used *) ( BoxFree, Sig.box_free_sig, false, - to_name [ "alloc"; "boxed"; "Box"; "free" ], + "alloc::boxed::Box::free", Some [ true; false ] ); (* Array Index *) ( ArrayIndexShared, Sig.array_index_sig false, true, - to_name [ "@ArrayIndexShared" ], - None ); - ( ArrayIndexMut, - Sig.array_index_sig true, - true, - to_name [ "@ArrayIndexMut" ], + "@ArrayIndexShared", None ); + (ArrayIndexMut, Sig.array_index_sig true, true, "@ArrayIndexMut", None); (* Array to slice*) ( ArrayToSliceShared, Sig.array_to_slice_sig false, true, - to_name [ "@ArrayToSliceShared" ], + "@ArrayToSliceShared", None ); ( ArrayToSliceMut, Sig.array_to_slice_sig true, true, - to_name [ "@ArrayToSliceMut" ], + "@ArrayToSliceMut", None ); (* Array Repeat *) - (ArrayRepeat, Sig.array_repeat_sig, false, to_name [ "@ArrayRepeat" ], None); + (ArrayRepeat, Sig.array_repeat_sig, false, "@ArrayRepeat", None); (* Slice Index *) ( SliceIndexShared, Sig.slice_index_sig false, true, - to_name [ "@SliceIndexShared" ], - None ); - ( SliceIndexMut, - Sig.slice_index_sig true, - true, - to_name [ "@SliceIndexMut" ], + "@SliceIndexShared", None ); - (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ], None); + (SliceIndexMut, Sig.slice_index_sig true, true, "@SliceIndexMut", None); ] 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 = +let get_assumed_fun_info (id : 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_fun_info: not found: " ^ A.show_assumed_fun_id id)) + (Failure ("get_assumed_fun_info: not found: " ^ show_assumed_fun_id id)) -let get_assumed_fun_sig (id : A.assumed_fun_id) : A.fun_sig = +let get_assumed_fun_sig (id : assumed_fun_id) : fun_sig = (get_assumed_fun_info id).fun_sig -let get_assumed_fun_name (id : A.assumed_fun_id) : fun_name = +let get_assumed_fun_name (id : assumed_fun_id) : string = (get_assumed_fun_info id).name -let assumed_fun_can_fail (id : A.assumed_fun_id) : bool = +let assumed_fun_can_fail (id : assumed_fun_id) : bool = (get_assumed_fun_info id).can_fail -- cgit v1.2.3 From 672ceef25203ebd5fcf5a55e294a4ebfe65648d6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 20 Nov 2023 21:58:25 +0100 Subject: Use the name matcher implemented in Charon --- 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 6aec626a..48b7ee2b 100644 --- a/compiler/Assumed.ml +++ b/compiler/Assumed.ml @@ -42,7 +42,7 @@ module Sig = struct let tvar_id_0 = TypeVarId.of_int 0 let tvar_0 : ty = TVar tvar_id_0 let cgvar_id_0 = ConstGenericVarId.of_int 0 - let cgvar_0 : const_generic = CGVar cgvar_id_0 + let cgvar_0 : const_generic = CgVar cgvar_id_0 (** Region 'a of id 0 *) let region_param_0 : region_var = { index = rvar_id_0; name = Some "'a" } -- cgit v1.2.3