From dcd34ceed0c52738b1bb8139e7130db9bad1a774 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 21 Nov 2023 10:22:51 +0100 Subject: Fix issues with the builtin names --- compiler/ExtractBuiltin.ml | 131 +++++++++++++++++++++++++--------------- compiler/ExtractName.ml | 8 ++- tests/lean/NoNestedBorrows.lean | 12 ++-- 3 files changed, 95 insertions(+), 56 deletions(-) diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 2c3c8106..f4f34155 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -24,7 +24,11 @@ let mk_memoized (f : unit -> 'a) : unit -> 'a = g let split_on_separator (s : string) : string list = - Str.split (Str.regexp "::") s + Str.split (Str.regexp "\\(::\\|\\.\\)") s + +let () = + assert (split_on_separator "x::y::z" = [ "x"; "y"; "z" ]); + assert (split_on_separator "x.y.z" = [ "x"; "y"; "z" ]) (** Switch between two values depending on the target backend. @@ -243,20 +247,24 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info list) list in [ mk_fun "core::mem::replace" None None true false; - mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::new" None None false false; - mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::push" None + mk_fun "core::slice::{[@T]}::len" + (Some (backend_choice "slice::len" "Slice::len")) + None true false; + mk_fun "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new" + (Some "alloc::vec::Vec::new") None false false; + mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::push" None (Some [ true; false ]) true true; - mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::insert" None + mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::insert" None (Some [ true; false ]) true true; - mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::len" None + mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::len" None (Some [ true; false ]) true false; - mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::index" None + mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::index" None (Some [ true; true; false ]) true false; - mk_fun "alloc::vec::{alloc::vec::Vec<@T>}::index_mut" None + mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::index_mut" None (Some [ true; true; false ]) true false; mk_fun "alloc::boxed::{Box<@T>}::deref" None @@ -269,14 +277,19 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info list) list mk_fun "core::slice::index::{[@T]}::index_mut" None None true false; mk_fun "core::array::{[@T; @C]}::index" None None true false; mk_fun "core::array::{[@T; @C]}::index_mut" None None true false; - mk_fun "core::slice::index::{Range<@T>}::get" None None true false; - mk_fun "core::slice::index::{Range<@T>}::get_mut" None None true false; - mk_fun "core::slice::index::{Range<@T>}::index" None None true false; - mk_fun "core::slice::index::{Range<@T>}::index_mut" None None true false; - mk_fun "core::slice::index::{Range<@T>}::get_unchecked" None None false - false; - mk_fun "core::slice::index::{Range<@T>}::get_unchecked_mut" None None false - false; + mk_fun "core::slice::index::{core::ops::range::Range}::get" + (Some "core::slice::index::Range::get") None true false; + mk_fun "core::slice::index::{core::ops::range::Range}::get_mut" + (Some "core::slice::index::Range::get_mut") None true false; + mk_fun "core::slice::index::{core::ops::range::Range}::index" + (Some "core::slice::index::Range::index") None true false; + mk_fun "core::slice::index::{core::ops::range::Range}::index_mut" + (Some "core::slice::index::Range::index_mut") None true false; + mk_fun "core::slice::index::{core::ops::range::Range}::get_unchecked" + (Some "core::slice::index::Range::get_unchecked") None false false; + mk_fun + "core::slice::index::{core::ops::range::Range}::get_unchecked_mut" + (Some "core::slice::index::Range::get_unchecked_mut") None false false; mk_fun "core::slice::index::{usize}::get" None None true false; mk_fun "core::slice::index::{usize}::get_mut" None None true false; mk_fun "core::slice::index::{usize}::get_unchecked" None None false false; @@ -330,9 +343,10 @@ let builtin_fun_effects = let int_funs = List.concat int_funs in let no_fail_no_state_funs = [ - (* TODO: redundancy with the funs information below *) - "alloc::vec::{alloc::vec::Vec<@T>}::new"; - "alloc::vec::{alloc::vec::Vec<@T>}::len"; + (* TODO: redundancy with the funs information above *) + "core::slice::{[@T]}::len"; + "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new"; + "alloc::vec::{alloc::vec::Vec<@T, @A>}::len"; "core::mem::replace"; "core::mem::take"; ] @@ -345,11 +359,11 @@ let builtin_fun_effects = in let no_state_funs = [ - (* TODO: redundancy with the funs information below *) - "alloc::vec::{alloc::vec::Vec<@T>}::push"; - "alloc::vec::{alloc::vec::Vec<@T>}::index"; - "alloc::vec::{alloc::vec::Vec<@T>}::index_mut"; - "alloc::vec::{alloc::vec::Vec<@T>}::index_mut_back"; + (* TODO: redundancy with the funs information above *) + "alloc::vec::{alloc::vec::Vec<@T, @A>}::push"; + "alloc::vec::{alloc::vec::Vec<@T, @A>}::index"; + "alloc::vec::{alloc::vec::Vec<@T, @A>}::index_mut"; + "alloc::vec::{alloc::vec::Vec<@T, @A>}::index_mut_back"; ] in let no_state_funs = @@ -395,10 +409,14 @@ let builtin_trait_decls_info () = let consts = [] in let types = let mk_type item_name = + let type_name = + if !record_fields_short_names then item_name + else extract_name ^ "_" ^ item_name + in let type_name = match !backend with - | Coq | FStar | HOL4 -> extract_name ^ "_" ^ item_name - | Lean -> item_name + | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter type_name + | Lean -> type_name in let clauses = [] in (item_name, (type_name, clauses)) @@ -409,9 +427,8 @@ let builtin_trait_decls_info () = let mk_method (item_name, with_back) = (* TODO: factor out with builtin_funs_info *) let basename = - match !backend with - | Coq | FStar | HOL4 -> extract_name ^ "_" ^ item_name - | Lean -> item_name + if !record_fields_short_names then item_name + else extract_name ^ "_" ^ item_name in let back_no_suffix = false in let fwd_suffix = if with_back && back_no_suffix then "_fwd" else "" in @@ -442,8 +459,7 @@ let builtin_trait_decls_info () = ~methods:[ ("deref", true) ] (); (* DerefMut *) - mk_trait "core::ops::deref::DerefMut" - ~parent_clauses:[ backend_choice "deref_inst" "derefInst" ] + mk_trait "core::ops::deref::DerefMut" ~parent_clauses:[ "derefInst" ] ~methods:[ ("deref_mut", true) ] (); (* Index *) @@ -451,15 +467,13 @@ let builtin_trait_decls_info () = ~methods:[ ("index", true) ] (); (* IndexMut *) - mk_trait "core::ops::index::IndexMut" - ~parent_clauses:[ backend_choice "index_inst" "indexInst" ] + mk_trait "core::ops::index::IndexMut" ~parent_clauses:[ "indexInst" ] ~methods:[ ("index_mut", true) ] (); (* Sealed *) mk_trait "core::slice::index::private_slice_index::Sealed" (); (* SliceIndex *) - mk_trait "core::slice::index::SliceIndex" - ~parent_clauses:[ backend_choice "sealed_inst" "sealedInst" ] + mk_trait "core::slice::index::SliceIndex" ~parent_clauses:[ "sealedInst" ] ~types:[ "Output" ] ~methods: [ @@ -482,43 +496,64 @@ let mk_builtin_trait_decls_map () = let builtin_trait_decls_map = mk_memoized mk_builtin_trait_decls_map let builtin_trait_impls_info () : (pattern * (bool list option * string)) list = - let fmt (rust_name : string) ?(filter : bool list option = None) () : + let fmt (rust_name : string) ?(extract_name : string option = None) + ?(filter : bool list option = None) () : pattern * (bool list option * string) = let rust_name = parse_pattern rust_name in let name = - let name = pattern_to_trait_impl_extract_name rust_name in let sep = backend_choice "_" "." in + let name = + match extract_name with + | None -> pattern_to_trait_impl_extract_name rust_name + | Some name -> split_on_separator name + in String.concat sep name in (rust_name, (filter, name)) in [ (* core::ops::Deref> *) - fmt "core::ops::deref::Deref>" (); + fmt "core::ops::deref::Deref>" + ~extract_name:(Some "alloc::boxed::Box::coreopsDerefInst") (); (* core::ops::DerefMut> *) - fmt "core::ops::deref::DerefMut>" (); + fmt "core::ops::deref::DerefMut>" + ~extract_name:(Some "alloc::boxed::Box::coreopsDerefMutInst") (); (* core::ops::index::Index<[T], I> *) - fmt "core::ops::index::Index<[@T], @I>" (); + fmt "core::ops::index::Index<[@T], @I>" + ~extract_name:(Some "core::ops::index::IndexSliceTIInst") (); (* core::ops::index::IndexMut<[T], I> *) - fmt "core::ops::index::IndexMut<[@T], @I>" (); + fmt "core::ops::index::IndexMut<[@T], @I>" + ~extract_name:(Some "core::ops::index::IndexMutSliceTIInst") (); (* core::slice::index::private_slice_index::Sealed> *) - fmt "core::slice::index::private_slice_index::Sealed>" (); + fmt + "core::slice::index::private_slice_index::Sealed>" + ~extract_name: + (Some "core.slice.index.private_slice_index.SealedRangeUsizeInst") (); (* core::slice::index::SliceIndex, [T]> *) - fmt "core::slice::index::SliceIndex, [@T]>" (); + fmt "core::slice::index::SliceIndex, [@T]>" + ~extract_name:(Some "core::slice::index::SliceIndexRangeUsizeSliceTInst") + (); (* core::ops::index::Index<[T; N], I> *) - fmt "core::ops::index::Index<[@T; @N], @I>" (); + fmt "core::ops::index::Index<[@T; @N], @I>" + ~extract_name:(Some "core::ops::index::IndexArrayInst") (); (* core::ops::index::IndexMut<[T; N], I> *) - fmt "core::ops::index::IndexMut<[@T; @N], @I>" (); + fmt "core::ops::index::IndexMut<[@T; @N], @I>" + ~extract_name:(Some "core::ops::index::IndexMutArrayIInst") (); (* core::slice::index::private_slice_index::Sealed *) - fmt "core::slice::index::private_slice_index::Sealed" (); + fmt "core::slice::index::private_slice_index::Sealed" + ~extract_name: + (Some "core::slice::index::private_slice_index::SealedUsizeInst") (); (* core::slice::index::SliceIndex *) - fmt "core::slice::index::SliceIndex" (); + fmt "core::slice::index::SliceIndex" + ~extract_name:(Some "core::slice::index::SliceIndexUsizeSliceTInst") (); (* core::ops::index::Index, T> *) - fmt "core::ops::index::Index, @T>" + fmt "core::ops::index::Index, @T>" + ~extract_name:(Some "alloc::vec::Vec::coreopsindexIndexInst") ~filter:(Some [ true; true; false ]) (); (* core::ops::index::IndexMut, T> *) - fmt "core::ops::index::IndexMut, @T>" + fmt "core::ops::index::IndexMut, @T>" + ~extract_name:(Some "alloc::vec::Vec::coreopsindexIndexMutInst") ~filter:(Some [ true; true; false ]) (); ] diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml index 4f5ca0d1..6d50ed73 100644 --- a/compiler/ExtractName.ml +++ b/compiler/ExtractName.ml @@ -35,7 +35,7 @@ end *) let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) : string list = - let c = { tgt_kind = TkName } in + let c = { tgt = TkName } in let is_var (g : generic_arg) : bool = match g with | GExpr (EVar _) -> true @@ -83,11 +83,13 @@ let pattern_to_trait_impl_extract_name = pattern_to_extract_name true names we derive from the patterns (for the builtin definitions) are consistent with the extraction names we derive from the Rust names *) let name_to_simple_name (ctx : ctx) (n : Types.name) : string list = - pattern_to_extract_name false (name_to_pattern ctx n) + let c : to_pat_config = { tgt = TkName } in + pattern_to_extract_name false (name_to_pattern ctx c n) let name_with_generics_to_simple_name (ctx : ctx) (n : Types.name) (p : Types.generic_params) (g : Types.generic_args) : string list = - pattern_to_extract_name true (name_with_generics_to_pattern ctx n p g) + let c : to_pat_config = { tgt = TkName } in + pattern_to_extract_name true (name_with_generics_to_pattern ctx c n p g) (* (* Prepare a name. diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index c4a6a265..79049837 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -151,11 +151,13 @@ def test_list1 : Result Unit := /- [no_nested_borrows::test_box1]: forward function -/ def test_box1 : Result Unit := - let b := 1#i32 - let x := b - if not (x = 1#i32) - then Result.fail Error.panic - else Result.ret () + do + let b := 0#i32 + let b0 ← alloc.boxed.Box.deref_mut_back I32 b 1#i32 + let x ← alloc.boxed.Box.deref I32 b0 + if not (x = 1#i32) + then Result.fail Error.panic + else Result.ret () /- Unit test for [no_nested_borrows::test_box1] -/ #assert (test_box1 == .ret ()) -- cgit v1.2.3