Skip to content

Commit

Permalink
Fix issues with the builtin names
Browse files Browse the repository at this point in the history
  • Loading branch information
@sonmarcho
sonmarcho committed Nov 21, 2023
1 parent db58a6b commit dcd34ce
Show file tree
Hide file tree
Showing 3 changed files with 95 additions and 56 deletions.
131 changes: 83 additions & 48 deletions compiler/ExtractBuiltin.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand All @@ -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<usize>}::get"
(Some "core::slice::index::Range::get") None true false;
mk_fun "core::slice::index::{core::ops::range::Range<usize>}::get_mut"
(Some "core::slice::index::Range::get_mut") None true false;
mk_fun "core::slice::index::{core::ops::range::Range<usize>}::index"
(Some "core::slice::index::Range::index") None true false;
mk_fun "core::slice::index::{core::ops::range::Range<usize>}::index_mut"
(Some "core::slice::index::Range::index_mut") None true false;
mk_fun "core::slice::index::{core::ops::range::Range<usize>}::get_unchecked"
(Some "core::slice::index::Range::get_unchecked") None false false;
mk_fun
"core::slice::index::{core::ops::range::Range<usize>}::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;
Expand Down Expand Up @@ -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";
]
Expand All @@ -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 =
Expand Down Expand Up @@ -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))
Expand All @@ -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
Expand Down Expand Up @@ -442,24 +459,21 @@ 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 *)
mk_trait "core::ops::index::Index" ~types:[ "Output" ]
~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:
[
Expand All @@ -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<alloc::boxed::Box<T>> *)
fmt "core::ops::deref::Deref<Box<@T>>" ();
fmt "core::ops::deref::Deref<Box<@T>>"
~extract_name:(Some "alloc::boxed::Box::coreopsDerefInst") ();
(* core::ops::DerefMut<alloc::boxed::Box<T>> *)
fmt "core::ops::deref::DerefMut<Box<@T>>" ();
fmt "core::ops::deref::DerefMut<Box<@T>>"
~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<Range<usize>> *)
fmt "core::slice::index::private_slice_index::Sealed<Range<usize>>" ();
fmt
"core::slice::index::private_slice_index::Sealed<core::ops::range::Range<usize>>"
~extract_name:
(Some "core.slice.index.private_slice_index.SealedRangeUsizeInst") ();
(* core::slice::index::SliceIndex<Range<usize>, [T]> *)
fmt "core::slice::index::SliceIndex<Range<usize>, [@T]>" ();
fmt "core::slice::index::SliceIndex<core::ops::range::Range<usize>, [@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<usize> *)
fmt "core::slice::index::private_slice_index::Sealed<usize>" ();
fmt "core::slice::index::private_slice_index::Sealed<usize>"
~extract_name:
(Some "core::slice::index::private_slice_index::SealedUsizeInst") ();
(* core::slice::index::SliceIndex<usize, [T]> *)
fmt "core::slice::index::SliceIndex<usize, [@T]>" ();
fmt "core::slice::index::SliceIndex<usize, [@T]>"
~extract_name:(Some "core::slice::index::SliceIndexUsizeSliceTInst") ();
(* core::ops::index::Index<alloc::vec::Vec<T>, T> *)
fmt "core::ops::index::Index<alloc::vec::Vec<@T>, @T>"
fmt "core::ops::index::Index<alloc::vec::Vec<@T, @A>, @T>"
~extract_name:(Some "alloc::vec::Vec::coreopsindexIndexInst")
~filter:(Some [ true; true; false ])
();
(* core::ops::index::IndexMut<alloc::vec::Vec<T>, T> *)
fmt "core::ops::index::IndexMut<alloc::vec::Vec<@T>, @T>"
fmt "core::ops::index::IndexMut<alloc::vec::Vec<@T, @A>, @T>"
~extract_name:(Some "alloc::vec::Vec::coreopsindexIndexMutInst")
~filter:(Some [ true; true; false ])
();
]
Expand Down
8 changes: 5 additions & 3 deletions compiler/ExtractName.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down
12 changes: 7 additions & 5 deletions tests/lean/NoNestedBorrows.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ())
Expand Down

0 comments on commit dcd34ce

Please sign in to comment.