From 749197e2e54b4658e66a9f5695e51608402fef32 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 3 Dec 2024 11:46:03 +0000 Subject: [PATCH 01/11] Add definitions to the standard library --- backends/lean/Base/Primitives/ArraySlice.lean | 5 ++ backends/lean/Base/Primitives/Core.lean | 30 ++++++++++ .../lean/Base/Primitives/CoreConvertNum.lean | 16 ++++- backends/lean/Base/Primitives/Scalar.lean | 60 +++++++++++++++++++ src/Main.ml | 4 +- src/extract/Extract.ml | 23 ++++++- src/extract/ExtractBuiltin.ml | 42 ++++++++++++- tests/src/paper.rs | 2 +- 8 files changed, 174 insertions(+), 8 deletions(-) diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean index cce8c2e7..b4251e8d 100644 --- a/backends/lean/Base/Primitives/ArraySlice.lean +++ b/backends/lean/Base/Primitives/ArraySlice.lean @@ -577,4 +577,9 @@ def core.slice.index.SliceIndexUsizeSliceTInst (T : Type) : index_mut := core.slice.index.Usize.index_mut } +def core.slice.Slice.copy_from_slice {T : Type} (_ : core.marker.Copy T) + (s : Slice T) (src: Slice T) : Result (Slice T) := + if s.len = src.len then ok src + else fail panic + end Primitives diff --git a/backends/lean/Base/Primitives/Core.lean b/backends/lean/Base/Primitives/Core.lean index 84f1d6d9..02aff85f 100644 --- a/backends/lean/Base/Primitives/Core.lean +++ b/backends/lean/Base/Primitives/Core.lean @@ -53,6 +53,10 @@ def clone.CloneBool : clone.Clone Bool := { clone := fun b => ok (clone.impls.CloneBool.clone b) } +/- [core::marker::Copy] -/ +structure marker.Copy (Self : Type) where + cloneInst : core.clone.Clone Self + /- [core::mem::replace] This acts like a swap effectively in a functional pure world. @@ -81,3 +85,29 @@ end core @[simp] def core.clone.Clone.clone_from {Self : Type} (cloneInst : core.clone.Clone Self) (_self : Self) (source : Self) : Result Self := cloneInst.clone source + +/- [core::convert::Into] -/ +structure core.convert.Into (Self : Type) (T : Type) where + into : Self → Result T + +/- [core::convert::{core::convert::Into for T}::into] -/ +@[reducible, simp] +def core.convert.IntoFrom.into {T : Type} {U : Type} + (fromInst : core.convert.From U T) (x : T) : Result U := + fromInst.from_ x + +/- Trait implementation: [core::convert::{core::convert::Into for T}] -/ +@[reducible] +def core.convert.IntoFrom {T : Type} {U : Type} (fromInst : core.convert.From U T) + : core.convert.Into T U := { + into := core.convert.IntoFrom.into fromInst +} + +/- [core::convert::{core::convert::From for T}::from] -/ +@[simp] def core.convert.FromSame.from_ {T : Type} (x : T) : T := x + +/- [core::convert::{core::convert::From for T}] -/ +@[reducible] +def core.convert.FromSame (T : Type) : core.convert.From T T := { + from_ := fun x => ok (core.convert.FromSame.from_ x) +} diff --git a/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean index ad54c5c3..e5e08a5a 100644 --- a/backends/lean/Base/Primitives/CoreConvertNum.lean +++ b/backends/lean/Base/Primitives/CoreConvertNum.lean @@ -296,6 +296,8 @@ def FromI128I128 : core.convert.From I128 I128 := { from_ := fun x => ok (num.FromI128I128.from x) } +end core.convert + -- to_le_bytes def core.num.U8.to_le_bytes (x : U8) : Array U8 1#usize := sorry def core.num.U16.to_le_bytes (x : U16) : Array U8 2#usize := sorry @@ -310,6 +312,18 @@ def core.num.U32.to_be_bytes (x : U32) : Array U8 4#usize := sorry def core.num.U64.to_be_bytes (x : U64) : Array U8 8#usize := sorry def core.num.U128.to_be_bytes (x : U128) : Array U8 128#usize := sorry -end core.convert +-- from_le_bytes +def core.num.U8.from_le_bytes (a : Array U8 1#usize) : U8 := sorry +def core.num.U16.from_le_bytes (a : Array U8 2#usize) : U16 := sorry +def core.num.U32.from_le_bytes (a : Array U8 4#usize) : U32 := sorry +def core.num.U64.from_le_bytes (a : Array U8 8#usize) : U64 := sorry +def core.num.U128.from_le_bytes (a : Array U8 128#usize) : U128 := sorry + +-- from_be_bytes +def core.num.U8.from_be_bytes (a : Array U8 1#usize) : I8 := sorry +def core.num.U16.from_be_bytes (a : Array U8 2#usize) : I16 := sorry +def core.num.U32.from_be_bytes (a : Array U8 4#usize) : I32 := sorry +def core.num.U64.from_be_bytes (a : Array U8 8#usize) : I64 := sorry +def core.num.U128.from_be_bytes (a : Array U8 128#usize) : I128 := sorry end Primitives diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 6ae14027..c4ebf15d 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -958,6 +958,66 @@ def core.clone.CloneI128 : core.clone.Clone I128 := { clone := fun x => ok (core.clone.impls.CloneI128.clone x) } +@[reducible] +def core.marker.CopyU8 : core.marker.Copy U8 := { + cloneInst := core.clone.CloneU8 +} + +@[reducible] +def core.marker.CopyU16 : core.marker.Copy U16 := { + cloneInst := core.clone.CloneU16 +} + +@[reducible] +def core.marker.CopyU32 : core.marker.Copy U32 := { + cloneInst := core.clone.CloneU32 +} + +@[reducible] +def core.marker.CopyU64 : core.marker.Copy U64 := { + cloneInst := core.clone.CloneU64 +} + +@[reducible] +def core.marker.CopyU128 : core.marker.Copy U128 := { + cloneInst := core.clone.CloneU128 +} + +@[reducible] +def core.marker.CopyUsize : core.marker.Copy Usize := { + cloneInst := core.clone.CloneUsize +} + +@[reducible] +def core.marker.CopyI8 : core.marker.Copy I8 := { + cloneInst := core.clone.CloneI8 +} + +@[reducible] +def core.marker.CopyI16 : core.marker.Copy I16 := { + cloneInst := core.clone.CloneI16 +} + +@[reducible] +def core.marker.CopyI32 : core.marker.Copy I32 := { + cloneInst := core.clone.CloneI32 +} + +@[reducible] +def core.marker.CopyI64 : core.marker.Copy I64 := { + cloneInst := core.clone.CloneI64 +} + +@[reducible] +def core.marker.CopyI128 : core.marker.Copy I128 := { + cloneInst := core.clone.CloneI128 +} + +@[reducible] +def core.marker.CopyIsize : core.marker.Copy Isize := { + cloneInst := core.clone.CloneIsize +} + -- This is easier defined this way than with the modulo operation (because of the -- unsigned cases). def int_overflowing_add (ty : ScalarTy) (x y : Int) : Int × Bool := diff --git a/src/Main.ml b/src/Main.ml index a669e748..469ec647 100644 --- a/src/Main.ml +++ b/src/Main.ml @@ -127,8 +127,8 @@ let () = " Do not treat warnings as errors" ); ( "-tuple-nested-proj", Arg.Set use_nested_tuple_projectors, - " Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \ - (0, 1).1)." ); + " Use nested projectors for tuples (e.g., (0, 1, 2).snd.fst instead of \ + (0, 1, 2).1)." ); ] in diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml index 12f43f4c..2dfba3bd 100644 --- a/src/extract/Extract.ml +++ b/src/extract/Extract.ml @@ -2206,6 +2206,16 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx) (c.clause_id, name)) trait_decl.parent_clauses | Some info -> + cassert __FILE__ __LINE__ + (List.length trait_decl.parent_clauses + = List.length info.parent_clauses) + trait_decl.item_meta.span + ("Invalid builtin information for trait decl: " + ^ name_to_string ctx trait_decl.item_meta.name + ^ "; expected " + ^ string_of_int (List.length trait_decl.parent_clauses) + ^ " parent clauses, found " + ^ string_of_int (List.length info.parent_clauses)); List.map (fun (c, name) -> (c.clause_id, name)) (List.combine trait_decl.parent_clauses info.parent_clauses) @@ -2306,8 +2316,15 @@ let extract_trait_decl_method_names (ctx : extraction_ctx) let compute_item_name (item_name : string) (id : fun_decl_id) : string * string = let trans : pure_fun_translation = - FunDeclId.Map.find id ctx.trans_funs + match FunDeclId.Map.find_opt id ctx.trans_funs with + | Some decl -> decl + | None -> + craise __FILE__ __LINE__ trait_decl.item_meta.span + ("Unexpected error: could not find the declaration for \ + method " ^ item_name ^ " for trait declaration " + ^ name_to_string ctx trait_decl.item_meta.name) in + let f = trans.f in (* We do something special to reuse the [ctx_compute_fun_decl] function. TODO: make it cleaner. *) @@ -2425,7 +2442,9 @@ let extract_trait_impl_register_names (ctx : extraction_ctx) (trait_impl.provided_methods = []) trait_impl.item_meta.span ("Overriding trait provided methods in trait implementations is not \ - supported yet (overriden methods: " + supported yet (trait impl: " + ^ name_to_string ctx trait_impl.item_meta.name + ^ ", overriden methods: " ^ String.concat ", " (List.map fst trait_impl.provided_methods) ^ ")"); (* Everything is taken care of by {!extract_trait_decl_register_names} *but* diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml index 7572a81e..ea0802ef 100644 --- a/src/extract/ExtractBuiltin.ml +++ b/src/extract/ExtractBuiltin.ml @@ -490,6 +490,18 @@ let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list = (fun ty -> "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_be_bytes") ~can_fail:false () + (* from_le_bytes *) + @ mk_scalar_fun + (fun ty -> "core::num::{" ^ ty ^ "}::from_le_bytes") + (fun ty -> + "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".from_le_bytes") + ~can_fail:false () + (* from_be_bytes *) + @ mk_scalar_fun + (fun ty -> "core::num::{" ^ ty ^ "}::from_be_bytes") + (fun ty -> + "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".from_be_bytes") + ~can_fail:false () (* Clone *) @ [ mk_fun "core::clone::impls::{core::clone::Clone}::clone" @@ -512,13 +524,22 @@ let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list = (); mk_fun "core::mem::swap" ~can_fail:false (); mk_fun "core::option::{core::option::Option<@T>}::take" - ~extract_name:(Some (backend_choice "" "core::option::Option::take")) + ~extract_name: + (backend_choice None (Some "core::option::Option::take")) ~can_fail:false (); mk_fun "core::option::{core::option::Option<@T>}::is_none" ~extract_name: - (Some (backend_choice "" "core::option::Option::is_none")) + (backend_choice None (Some "core::option::Option::is_none")) ~can_fail:false (); mk_fun "core::clone::Clone::clone_from" (); + (* Into> *) + mk_fun "core::convert::{core::convert::Into<@T, @U>}::into" + ~extract_name:(Some "core.convert.IntoFrom.into") (); + (* From *) + mk_fun "core::convert::{core::convert::From<@T, @T>}::from" + ~can_fail:false ~extract_name:(Some "core.convert.FromSame.from_") (); + (* [core::slice::{@Slice}::copy_from_slice] *) + mk_fun "core::slice::{[@T]}::copy_from_slice" (); ] @ List.map (fun ty -> @@ -676,7 +697,15 @@ let builtin_trait_decls_info () = (); (* Clone *) mk_trait "core::clone::Clone" ~methods:[ "clone" ] (); + (* Copy *) + mk_trait "core::marker::Copy" ~parent_clauses:[ "cloneInst" ] (); ] + @ mk_lean_only + [ + (* Into *) + mk_trait "core::convert::Into" ~types:[ "T"; "U" ] ~methods:[ "into" ] + (); + ] let mk_builtin_trait_decls_map () = NameMatcherMap.of_list @@ -758,6 +787,15 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list = ~filter:(Some [ true; false ]) (); ] + @ mk_lean_only + [ + (* Into> *) + fmt "core::convert::Into<@Self, @T>" + ~extract_name:(Some "core::convert::IntoFrom") (); + (* From *) + fmt "core::convert::From<@Self, @Self>" + ~extract_name:(Some "core::convert::FromSame") (); + ] (* From *) @ List.map (fun ty -> diff --git a/tests/src/paper.rs b/tests/src/paper.rs index d9fb1032..fd59295c 100644 --- a/tests/src/paper.rs +++ b/tests/src/paper.rs @@ -1,7 +1,7 @@ //@ charon-args=--no-code-duplication //@ [!borrow-check] aeneas-args=-test-trans-units //@ [coq,fstar] subdir=misc -//! The examples from the ICFP submission, all in one place. +//! The examples from the ICFP 2022 submission, all in one place. // 2.1 pub fn ref_incr(x: &mut i32) { From a1eb64a8aaba98f778edf4afd19fdb102cd2eccf Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 3 Dec 2024 11:46:51 +0000 Subject: [PATCH 02/11] Add tests for the builtin definitions --- tests/lean/Builtin.lean | 55 +++++++++++++++++++++++++++++++++++++++++ tests/src/builtin.rs | 35 ++++++++++++++++++++++++++ 2 files changed, 90 insertions(+) create mode 100644 tests/lean/Builtin.lean create mode 100644 tests/src/builtin.rs diff --git a/tests/lean/Builtin.lean b/tests/lean/Builtin.lean new file mode 100644 index 00000000..4e2cb72d --- /dev/null +++ b/tests/lean/Builtin.lean @@ -0,0 +1,55 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [builtin] +import Base +open Primitives +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false + +namespace builtin + +/- [builtin::clone_bool]: + Source: 'tests/src/builtin.rs', lines 5:0-7:1 -/ +def clone_bool (x : Bool) : Result Bool := + Result.ok (core.clone.impls.CloneBool.clone x) + +/- [builtin::clone_u32]: + Source: 'tests/src/builtin.rs', lines 9:0-11:1 -/ +def clone_u32 (x : U32) : Result U32 := + Result.ok (core.clone.impls.CloneU32.clone x) + +/- [builtin::into_from]: + Source: 'tests/src/builtin.rs', lines 13:0-15:1 -/ +def into_from + {T : Type} {U : Type} (coreconvertFromInst : core.convert.From U T) (x : T) : + Result U + := + core.convert.IntoFrom.into coreconvertFromInst x + +/- [builtin::into_same]: + Source: 'tests/src/builtin.rs', lines 17:0-19:1 -/ +def into_same {T : Type} (x : T) : Result T := + core.convert.IntoFrom.into (core.convert.FromSame T) x + +/- [builtin::from_same]: + Source: 'tests/src/builtin.rs', lines 21:0-23:1 -/ +def from_same {T : Type} (x : T) : Result T := + Result.ok (core.convert.FromSame.from_ x) + +/- [builtin::copy]: + Source: 'tests/src/builtin.rs', lines 25:0-27:1 -/ +def copy + {T : Type} (coremarkerCopyInst : core.marker.Copy T) (x : T) : Result T := + Result.ok x + +/- [builtin::u32_from_le_bytes]: + Source: 'tests/src/builtin.rs', lines 29:0-31:1 -/ +def u32_from_le_bytes (x : Array U8 4#usize) : Result U32 := + Result.ok (core.num.U32.from_le_bytes x) + +/- [builtin::u32_to_le_bytes]: + Source: 'tests/src/builtin.rs', lines 33:0-35:1 -/ +def u32_to_le_bytes (x : U32) : Result (Array U8 4#usize) := + Result.ok (core.num.U32.to_le_bytes x) + +end builtin diff --git a/tests/src/builtin.rs b/tests/src/builtin.rs new file mode 100644 index 00000000..4c70257a --- /dev/null +++ b/tests/src/builtin.rs @@ -0,0 +1,35 @@ +//@[!lean] skip +//! This file uses a list of builtin definitions, to make sure they are properly +//! detected and mapped to definitions in the standard library. + +fn clone_bool(x: bool) -> bool { + x.clone() +} + +fn clone_u32(x: u32) -> u32 { + x.clone() +} + +fn into_from>(x: T) -> U { + x.into() +} + +fn into_same(x: T) -> T { + x.into() +} + +fn from_same(x: T) -> T { + T::from(x) +} + +fn copy(x: &T) -> T { + *x +} + +fn u32_from_le_bytes(x: [u8; 4]) -> u32 { + u32::from_le_bytes(x) +} + +fn u32_to_le_bytes(x: u32) -> [u8; 4] { + x.to_le_bytes() +} From 62e1226ccca575ec3f29769fe825f2cbae19f5dd Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 3 Dec 2024 16:15:49 +0000 Subject: [PATCH 03/11] Add more definitions to the Lean library and add deboguing features --- backends/lean/Base/Primitives/ArraySlice.lean | 3 + backends/lean/Base/Primitives/Core.lean | 40 ++++ src/Config.ml | 3 + src/Errors.ml | 10 + src/Main.ml | 179 +++++++++++++++++- src/TranslateCore.ml | 37 ++++ src/extract/ExtractBase.ml | 11 +- src/extract/ExtractBuiltin.ml | 24 +++ src/symbolic/SymbolicToPure.ml | 10 +- tests/lean/Builtin.lean | 22 ++- tests/src/builtin.rs | 3 + 11 files changed, 325 insertions(+), 17 deletions(-) diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean index b4251e8d..405734a0 100644 --- a/backends/lean/Base/Primitives/ArraySlice.lean +++ b/backends/lean/Base/Primitives/ArraySlice.lean @@ -582,4 +582,7 @@ def core.slice.Slice.copy_from_slice {T : Type} (_ : core.marker.Copy T) if s.len = src.len then ok src else fail panic +/- [core::array::TryFromSliceError] -/ +def core.array.TryFromSliceError := () + end Primitives diff --git a/backends/lean/Base/Primitives/Core.lean b/backends/lean/Base/Primitives/Core.lean index 02aff85f..f792e812 100644 --- a/backends/lean/Base/Primitives/Core.lean +++ b/backends/lean/Base/Primitives/Core.lean @@ -111,3 +111,43 @@ def core.convert.IntoFrom {T : Type} {U : Type} (fromInst : core.convert.From U def core.convert.FromSame (T : Type) : core.convert.From T T := { from_ := fun x => ok (core.convert.FromSame.from_ x) } + +/- [core::result::Result] -/ +inductive core.result.Result (T : Type) (E : Type) := +| Ok : T → core.result.Result T E +| Err : E → core.result.Result T E + +/- [core::fmt::Error] -/ +@[reducible] def core.fmt.Error := Unit + +structure core.convert.TryFrom (Self T : Type) where + Error : Type + try_from : T → Result (core.result.Result Self Error) + +structure core.convert.TryInto (Self T : Type) where + Error : Type + try_into : Self → Result (core.result.Result T Error) + +@[reducible, simp] +def core.convert.TryIntoFrom.try_into {T U : Type} (fromInst : core.convert.TryFrom U T) + (x : T) : Result (core.result.Result U fromInst.Error) := + fromInst.try_from x + +@[reducible] +def core.convert.TryIntoFrom {T U : Type} (fromInst : core.convert.TryFrom U T) : + core.convert.TryInto T U := { + Error := fromInst.Error + try_into := core.convert.TryIntoFrom.try_into fromInst +} + +/- TODO: -/ +axiom Formatter : Type + +structure core.fmt.Debug (T : Type) where + fmt : T → Formatter → Result (Formatter × Formatter → Formatter) + +def core.result.Result.unwrap {T E : Type} + (_ : core.fmt.Debug T) (e : core.result.Result T E) : Primitives.Result T := + match e with + | .Ok x => ok x + | .Err _ => fail .panic diff --git a/src/Config.ml b/src/Config.ml index d9fed408..7d315ca4 100644 --- a/src/Config.ml +++ b/src/Config.ml @@ -45,6 +45,9 @@ let if_backend (f : unit -> 'a) (default : 'a) : 'a = | None -> default | Some _ -> f () +(** Print all the external definitions which are not listed in the builtin functions *) +let print_unknown_externals = ref false + (** {1 Interpreter} *) (** Activate the sanity checks, and in particular the invariant checks diff --git a/src/Errors.ml b/src/Errors.ml index e66876c0..36d066d3 100644 --- a/src/Errors.ml +++ b/src/Errors.ml @@ -57,6 +57,16 @@ let craise_opt_span (file : string) (line : int) (span : Meta.span option) let craise (file : string) (line : int) (span : Meta.span) (msg : string) = craise_opt_span file line (Some span) msg +(** Lazy assert *) +let classert_opt_span (file : string) (line : int) (b : bool) + (span : Meta.span option) (msg : string Lazy.t) = + if not b then craise_opt_span file line span (Lazy.force msg) + +(** Lazy assert *) +let classert (file : string) (line : int) (b : bool) (span : Meta.span) + (msg : string Lazy.t) = + classert_opt_span file line b (Some span) msg + let cassert_opt_span (file : string) (line : int) (b : bool) (span : Meta.span option) (msg : string) = if not b then craise_opt_span file line span msg diff --git a/src/Main.ml b/src/Main.ml index 469ec647..fa624b7b 100644 --- a/src/Main.ml +++ b/src/Main.ml @@ -57,6 +57,37 @@ Usage: %s [OPTIONS] FILE |} Sys.argv.(0) +let matches_name (c : crate) (name : Types.name) + (m : 'a ExtractName.NameMatcherMap.t) : bool = + let open Charon.NameMatcher in + let open ExtractBuiltin in + let mctx : ctx = + { + type_decls = c.type_decls; + global_decls = c.global_decls; + fun_decls = c.fun_decls; + trait_decls = c.trait_decls; + trait_impls = c.trait_impls; + } + in + NameMatcherMap.mem mctx name m + +let matches_name_with_generics (c : crate) (name : Types.name) + (generics : Types.generic_args) (m : 'a ExtractName.NameMatcherMap.t) : bool + = + let open Charon.NameMatcher in + let open ExtractBuiltin in + let mctx : ctx = + { + type_decls = c.type_decls; + global_decls = c.global_decls; + fun_decls = c.fun_decls; + trait_decls = c.trait_decls; + trait_impls = c.trait_impls; + } + in + Option.is_some (NameMatcherMap.find_with_generics_opt mctx name generics m) + let () = (* Measure start time *) let start_time = Unix.gettimeofday () in @@ -129,6 +160,10 @@ let () = Arg.Set use_nested_tuple_projectors, " Use nested projectors for tuples (e.g., (0, 1, 2).snd.fst instead of \ (0, 1, 2).1)." ); + ( "-print-unknown-externals", + Arg.Set print_unknown_externals, + " Print all the external definitions which are not listed in the \ + builtin functions" ); ] in @@ -190,8 +225,6 @@ let () = if cond then fail_with_error msg in - if !print_llbc then main_log#set_level EL.Debug; - (* Sanity check (now that the arguments are parsed!) *) check_arg_implies (not !extract_template_decreases_clauses) @@ -300,7 +333,9 @@ let () = | Ok m -> (* Logging *) log#linfo (lazy ("Imported: " ^ filename)); - log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n")); + if !print_llbc then + log#linfo (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n")) + else log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n")); (* Check the Charon CLI options *) check_no_doc m.options.hide_marker_traits @@ -323,6 +358,144 @@ let () = definitions"; fail true); + (* Print the external definitions which are not listed in the builtin functions *) + if !print_unknown_externals then ( + let open TranslateCore in + let { type_decls; fun_decls; global_decls; trait_decls; trait_impls; _ } + = + m + in + (* Filter the definitions *) + let type_decls = + Types.TypeDeclId.Map.filter + (fun _ (d : Types.type_decl) -> + let names_map = ExtractBuiltin.builtin_types_map () in + (not d.item_meta.is_local) + && not (matches_name m d.item_meta.name names_map)) + type_decls + in + let fun_decls = + LlbcAst.FunDeclId.Map.filter + (fun _ (d : LlbcAst.fun_decl) -> + let names_map = ExtractBuiltin.builtin_funs_map () in + (not d.item_meta.is_local) + && (not (matches_name m d.item_meta.name names_map)) + (* We also ignore the trait method declarations *) + && + match d.kind with + | TraitDeclItem _ -> false + | _ -> true) + fun_decls + in + let global_decls = + LlbcAst.GlobalDeclId.Map.filter + (fun _ (d : LlbcAst.global_decl) -> + let funs_map = ExtractBuiltin.builtin_globals_map in + (not d.item_meta.is_local) + && not (matches_name m d.item_meta.name funs_map)) + global_decls + in + let trait_decls = + LlbcAst.TraitDeclId.Map.filter + (fun _ (d : LlbcAst.trait_decl) -> + let names_map = ExtractBuiltin.builtin_trait_decls_map () in + (not d.item_meta.is_local) + && not (matches_name m d.item_meta.name names_map)) + trait_decls + in + let trait_impls = + List.filter_map + (fun (d : LlbcAst.trait_impl) -> + let names_map = ExtractBuiltin.builtin_trait_impls_map () in + match + LlbcAst.TraitDeclId.Map.find_opt d.impl_trait.trait_decl_id + m.trait_decls + with + | None -> None (* Just ignore it *) + | Some trait_decl -> + if + (not d.item_meta.is_local) + && not + (matches_name_with_generics m trait_decl.item_meta.name + d.impl_trait.decl_generics names_map) + then Some (d, trait_decl) + else None) + (LlbcAst.TraitImplId.Map.values trait_impls) + in + (* Print *) + let fmt_env = Print.Crate.crate_to_fmt_env m in + let type_decls = + List.map + (fun (d : Types.type_decl) -> + let pattern = + TranslateCore.name_with_crate_to_pattern_string m + d.item_meta.name + in + "Type decl (pattern: [" ^ pattern ^ "]]):\n" + ^ Print.type_decl_to_string fmt_env d) + (Types.TypeDeclId.Map.values type_decls) + in + let fun_decls = + List.map + (fun (d : LlbcAst.fun_decl) -> + let pattern = + TranslateCore.name_with_crate_to_pattern_string m + d.item_meta.name + in + let d = + (* FIXME: there is a bug in the formatter when splitting the predicates + and trait clauses between the inherited ones and the others (the + index is sometimes out of bounds). + See: https://github.com/AeneasVerif/charon/issues/482 + *) + try Print.Ast.fun_decl_to_string fmt_env "" " " d + with _ -> "UNKNOWN" + in + "Fun decl (pattern: [" ^ pattern ^ "]]):\n" ^ d) + (LlbcAst.FunDeclId.Map.values fun_decls) + in + let global_decls = + List.map + (fun (d : LlbcAst.global_decl) -> + let pattern = + TranslateCore.name_with_crate_to_pattern_string m + d.item_meta.name + in + "Global decl (pattern: [" ^ pattern ^ "]]):\n" + ^ Print.Ast.global_decl_to_string fmt_env "" " " d) + (LlbcAst.GlobalDeclId.Map.values global_decls) + in + let trait_decls = + List.map + (fun (d : LlbcAst.trait_decl) -> + let pattern = + TranslateCore.name_with_crate_to_pattern_string m + d.item_meta.name + in + "Trait decl (pattern: [" ^ pattern ^ "]]):\n" + ^ Print.Ast.trait_decl_to_string fmt_env "" " " d) + (LlbcAst.TraitDeclId.Map.values trait_decls) + in + let trait_impls = + List.map + (fun ((d, trait_decl) : LlbcAst.trait_impl * LlbcAst.trait_decl) -> + let pattern = + TranslateCore.name_with_generics_crate_to_pattern_string m + trait_decl.item_meta.name trait_decl.generics + d.impl_trait.decl_generics + in + "Trait impl (pattern: [" ^ pattern ^ "]]):\n" + ^ Print.Ast.trait_impl_to_string fmt_env "" " " d) + trait_impls + in + + log#linfo + (lazy + (String.concat "\n\n" + (type_decls @ fun_decls @ global_decls @ trait_decls + @ trait_impls))); + ()); + (* There may be exceptions to catch *) (try (* Apply the pre-passes *) diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml index 688cbe34..25b8b4fc 100644 --- a/src/TranslateCore.ml +++ b/src/TranslateCore.ml @@ -76,6 +76,43 @@ let trait_name_with_generics_to_simple_name (ctx : trans_ctx) in name_with_generics_to_simple_name mctx ~prefix n p g +let name_with_crate_to_pattern_string (ctx : LlbcAst.crate) (n : Types.name) : + string = + let mctx : Charon.NameMatcher.ctx = + { + type_decls = ctx.type_decls; + global_decls = ctx.global_decls; + fun_decls = ctx.fun_decls; + trait_decls = ctx.trait_decls; + trait_impls = ctx.trait_impls; + } + in + let c : Charon.NameMatcher.to_pat_config = + { tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs } + in + let pat = Charon.NameMatcher.name_to_pattern mctx c n in + Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat + +let name_with_generics_crate_to_pattern_string (ctx : LlbcAst.crate) + (n : Types.name) (params : Types.generic_params) (args : Types.generic_args) + : string = + let mctx : Charon.NameMatcher.ctx = + { + type_decls = ctx.type_decls; + global_decls = ctx.global_decls; + fun_decls = ctx.fun_decls; + trait_decls = ctx.trait_decls; + trait_impls = ctx.trait_impls; + } + in + let c : Charon.NameMatcher.to_pat_config = + { tgt = TkPattern; use_trait_decl_refs = match_with_trait_decl_refs } + in + let pat = + Charon.NameMatcher.name_with_generics_to_pattern mctx c params n args + in + Charon.NameMatcher.pattern_to_string { tgt = TkPattern } pat + let name_to_pattern_string (ctx : trans_ctx) (n : Types.name) : string = let mctx : Charon.NameMatcher.ctx = { diff --git a/src/extract/ExtractBase.ml b/src/extract/ExtractBase.ml index ca145577..6729d5c2 100644 --- a/src/extract/ExtractBase.ml +++ b/src/extract/ExtractBase.ml @@ -1680,10 +1680,13 @@ let ctx_compute_trait_clause_name (ctx : extraction_ctx) let clause_trait = clause.trait.binder_value in (* *) let trait_id = clause_trait.trait_decl_id in - let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in - let args = clause_trait.decl_generics in - trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix - impl_trait_decl.item_meta.name params args + (* The declaration may be missing because of an error *) + match TraitDeclId.Map.find_opt trait_id ctx.crate.trait_decls with + | None -> [ "clause" ] + | Some impl_trait_decl -> + let args = clause_trait.decl_generics in + trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix + impl_trait_decl.item_meta.name params args in String.concat "" clause diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml index ea0802ef..c8a91e25 100644 --- a/src/extract/ExtractBuiltin.ml +++ b/src/extract/ExtractBuiltin.ml @@ -237,6 +237,13 @@ let builtin_types () : builtin_type_info list = ]); }; ] + @ mk_lean_only + [ + mk_type "core::fmt::Formatter" (); + mk_type "core::result::Result" (); + mk_type "core::fmt::Error" (); + mk_type "core::array::TryFromSliceError" (); + ] let mk_builtin_types_map () = NameMatcherMap.of_list @@ -540,6 +547,7 @@ let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list = ~can_fail:false ~extract_name:(Some "core.convert.FromSame.from_") (); (* [core::slice::{@Slice}::copy_from_slice] *) mk_fun "core::slice::{[@T]}::copy_from_slice" (); + mk_fun "core::result::{core::result::Result<@T, @E>}::unwrap" (); ] @ List.map (fun ty -> @@ -705,6 +713,10 @@ let builtin_trait_decls_info () = (* Into *) mk_trait "core::convert::Into" ~types:[ "T"; "U" ] ~methods:[ "into" ] (); + (* Debug *) + mk_trait "core::fmt::Debug" ~types:[ "T" ] ~methods:[ "fmt" ] (); + mk_trait "core::convert::TryFrom" ~methods:[ "try_from" ] (); + mk_trait "core::convert::TryInto" ~methods:[ "try_into" ] (); ] let mk_builtin_trait_decls_map () = @@ -795,6 +807,9 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list = (* From *) fmt "core::convert::From<@Self, @Self>" ~extract_name:(Some "core::convert::FromSame") (); + (* TryInto> *) + fmt "core::convert::{core::convert::TryInto<@T, @U>}" + ~extract_name:(Some "core::convert::TryIntoFrom") (); ] (* From *) @ List.map @@ -829,6 +844,15 @@ let builtin_trait_impls_info () : (pattern * (bool list option * string)) list = (Some ("core.clone.Clone" ^ StringUtils.capitalize_first_letter ty)) ()) all_int_names + (* Copy *) + @ List.map + (fun ty -> + fmt + ("core::marker::Copy<" ^ ty ^ ">") + ~extract_name: + (Some ("core.marker.Copy" ^ StringUtils.capitalize_first_letter ty)) + ()) + all_int_names let mk_builtin_trait_impls_map () = let m = NameMatcherMap.of_list (builtin_trait_impls_info ()) in diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml index 01172a1c..1ae92058 100644 --- a/src/symbolic/SymbolicToPure.ml +++ b/src/symbolic/SymbolicToPure.ml @@ -1185,9 +1185,15 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (* For now we don't support nested borrows, so we check that there aren't parent regions *) let parents = list_ancestor_region_groups regions_hierarchy gid in - cassert_opt_span __FILE__ __LINE__ + classert_opt_span __FILE__ __LINE__ (T.RegionGroupId.Set.is_empty parents) - span "Nested borrows are not supported yet"; + span + (lazy + (let ctx = Print.Contexts.decls_ctx_to_fmt_env decls_ctx in + "Nested borrows are not supported yet (found in the signature of: " + ^ Charon.PrintExpressions.fun_id_or_trait_method_ref_to_string ctx + fun_id + ^ ")")); (* For now, we don't allow nested borrows, so the additional inputs to the backward function can only come from borrows that were returned like in (for the backward function we introduce for 'a): diff --git a/tests/lean/Builtin.lean b/tests/lean/Builtin.lean index 4e2cb72d..65057344 100644 --- a/tests/lean/Builtin.lean +++ b/tests/lean/Builtin.lean @@ -9,17 +9,17 @@ set_option linter.unusedVariables false namespace builtin /- [builtin::clone_bool]: - Source: 'tests/src/builtin.rs', lines 5:0-7:1 -/ + Source: 'tests/src/builtin.rs', lines 6:0-8:1 -/ def clone_bool (x : Bool) : Result Bool := Result.ok (core.clone.impls.CloneBool.clone x) /- [builtin::clone_u32]: - Source: 'tests/src/builtin.rs', lines 9:0-11:1 -/ + Source: 'tests/src/builtin.rs', lines 10:0-12:1 -/ def clone_u32 (x : U32) : Result U32 := Result.ok (core.clone.impls.CloneU32.clone x) /- [builtin::into_from]: - Source: 'tests/src/builtin.rs', lines 13:0-15:1 -/ + Source: 'tests/src/builtin.rs', lines 14:0-16:1 -/ def into_from {T : Type} {U : Type} (coreconvertFromInst : core.convert.From U T) (x : T) : Result U @@ -27,29 +27,35 @@ def into_from core.convert.IntoFrom.into coreconvertFromInst x /- [builtin::into_same]: - Source: 'tests/src/builtin.rs', lines 17:0-19:1 -/ + Source: 'tests/src/builtin.rs', lines 18:0-20:1 -/ def into_same {T : Type} (x : T) : Result T := core.convert.IntoFrom.into (core.convert.FromSame T) x /- [builtin::from_same]: - Source: 'tests/src/builtin.rs', lines 21:0-23:1 -/ + Source: 'tests/src/builtin.rs', lines 22:0-24:1 -/ def from_same {T : Type} (x : T) : Result T := Result.ok (core.convert.FromSame.from_ x) /- [builtin::copy]: - Source: 'tests/src/builtin.rs', lines 25:0-27:1 -/ + Source: 'tests/src/builtin.rs', lines 26:0-28:1 -/ def copy {T : Type} (coremarkerCopyInst : core.marker.Copy T) (x : T) : Result T := Result.ok x /- [builtin::u32_from_le_bytes]: - Source: 'tests/src/builtin.rs', lines 29:0-31:1 -/ + Source: 'tests/src/builtin.rs', lines 30:0-32:1 -/ def u32_from_le_bytes (x : Array U8 4#usize) : Result U32 := Result.ok (core.num.U32.from_le_bytes x) /- [builtin::u32_to_le_bytes]: - Source: 'tests/src/builtin.rs', lines 33:0-35:1 -/ + Source: 'tests/src/builtin.rs', lines 34:0-36:1 -/ def u32_to_le_bytes (x : U32) : Result (Array U8 4#usize) := Result.ok (core.num.U32.to_le_bytes x) +/- [builtin::use_debug_clause]: + Source: 'tests/src/builtin.rs', lines 38:0-38:49 -/ +def use_debug_clause + {T : Type} (corefmtDebugInst : core.fmt.Debug T) (t : T) : Result Unit := + Result.ok () + end builtin diff --git a/tests/src/builtin.rs b/tests/src/builtin.rs index 4c70257a..6190ae93 100644 --- a/tests/src/builtin.rs +++ b/tests/src/builtin.rs @@ -1,3 +1,4 @@ +//@ charon-args=--exclude=core::fmt::Debug::fmt --opaque=core::fmt::Formatter //@[!lean] skip //! This file uses a list of builtin definitions, to make sure they are properly //! detected and mapped to definitions in the standard library. @@ -33,3 +34,5 @@ fn u32_from_le_bytes(x: [u8; 4]) -> u32 { fn u32_to_le_bytes(x: u32) -> [u8; 4] { x.to_le_bytes() } + +fn use_debug_clause(_: T) {} From c925bdd116ec9da3c51e04da396f65f6e9816003 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 4 Dec 2024 11:56:44 +0000 Subject: [PATCH 04/11] Update the Charon pin --- charon-pin | 2 +- flake.lock | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/charon-pin b/charon-pin index 0afbf647..1bcb4ae7 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -e6033230aab5cbff5e3840473844e913b59062af +b8f9025f0553dac519c658471e9f89656ac23e2c diff --git a/flake.lock b/flake.lock index 19869f91..7a25d500 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1733151343, - "narHash": "sha256-LPr2ZWbC3q6GjnCKN3Hsy1xJHR+qmzMZRgrtd55D4AA=", + "lastModified": 1733313324, + "narHash": "sha256-Dte1k61M1pcFiU5fEP38DODF9Pr5mg762ejyQJzBiRY=", "owner": "aeneasverif", "repo": "charon", - "rev": "e6033230aab5cbff5e3840473844e913b59062af", + "rev": "b8f9025f0553dac519c658471e9f89656ac23e2c", "type": "github" }, "original": { @@ -177,11 +177,11 @@ ] }, "locked": { - "lastModified": 1733106880, - "narHash": "sha256-aJmAIjZfWfPSWSExwrYBLRgXVvgF5LP1vaeUGOOIQ98=", + "lastModified": 1733279627, + "narHash": "sha256-NCNDAGPkdFdu+DLErbmNbavmVW9AwkgP7azROFFSB0U=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "e66c0d43abf5bdefb664c3583ca8994983c332ae", + "rev": "4da5a80ef76039e80468c902f1e9f5c0eab87d96", "type": "github" }, "original": { From 383108633f1f07865a9359449d592d85a678c566 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 4 Dec 2024 11:59:40 +0000 Subject: [PATCH 05/11] Update the Charon pin --- charon-pin | 2 +- flake.lock | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/charon-pin b/charon-pin index 1bcb4ae7..c1830e84 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -b8f9025f0553dac519c658471e9f89656ac23e2c +7744bf94275e2ba3e7a2e4163c1fa062225d7a75 diff --git a/flake.lock b/flake.lock index 7a25d500..3c32186b 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1733313324, - "narHash": "sha256-Dte1k61M1pcFiU5fEP38DODF9Pr5mg762ejyQJzBiRY=", + "lastModified": 1733313551, + "narHash": "sha256-CSaj6Cadz+S/qmiLtoQMWfm3mHSE2cCx3UUxt5JmoAM=", "owner": "aeneasverif", "repo": "charon", - "rev": "b8f9025f0553dac519c658471e9f89656ac23e2c", + "rev": "7744bf94275e2ba3e7a2e4163c1fa062225d7a75", "type": "github" }, "original": { From f791e9152cfbea227634aabef4736588c6bca66e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 4 Dec 2024 12:01:12 +0000 Subject: [PATCH 06/11] Propagate some changes from Charon --- src/interp/InterpreterStatements.ml | 5 +---- src/llbc/Builtin.ml | 1 - 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/src/interp/InterpreterStatements.ml b/src/interp/InterpreterStatements.ml index 5ac18af5..6e4354c5 100644 --- a/src/interp/InterpreterStatements.ml +++ b/src/interp/InterpreterStatements.ml @@ -780,10 +780,7 @@ let eval_transparent_function_call_symbolic_inst (span : Meta.span) (lazy ("provided method call:" ^ "\n- method name: " ^ method_name ^ "\n- all_generics:\n" - ^ generic_args_to_string ctx all_generics - ^ "\n- parent params info: " - ^ Print.option_to_string show_params_info - method_def.signature.parent_params_info)); + ^ generic_args_to_string ctx all_generics)); let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular method_id) ctx.fun_ctx.regions_hierarchies diff --git a/src/llbc/Builtin.ml b/src/llbc/Builtin.ml index 56178ad1..19e9c9f2 100644 --- a/src/llbc/Builtin.ml +++ b/src/llbc/Builtin.ml @@ -92,7 +92,6 @@ module Sig = struct is_closure = false; closure_info = None; generics; - parent_params_info = None; inputs; output; } From d4ecc1289a729ccc778a0e570da42fe6cc0f138d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 4 Dec 2024 12:13:15 +0000 Subject: [PATCH 07/11] Fix a wrong builtin information --- src/extract/ExtractBuiltin.ml | 18 ++++++++++++++---- src/extract/ExtractTypes.ml | 12 +++++++++--- 2 files changed, 23 insertions(+), 7 deletions(-) diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml index c8a91e25..ea353f17 100644 --- a/src/extract/ExtractBuiltin.ml +++ b/src/extract/ExtractBuiltin.ml @@ -134,8 +134,7 @@ type builtin_type_info = { type type_variant_kind = | KOpaque | KStruct of (string * string) list - (* TODO: handle the tuple case *) - | KEnum (* TODO *) + | KEnum of string list let mk_struct_constructor (type_name : string) : string = let prefix = @@ -182,7 +181,18 @@ let builtin_types () : builtin_type_info list = in let constructor = mk_struct_constructor extract_name in Some (Struct (constructor, fields)) - | KEnum -> raise (Failure "TODO") + | KEnum variants -> + let variants = + List.map + (fun variant -> + { + rust_variant_name = variant; + extract_variant_name = variant; + fields = None; + }) + variants + in + Some (Enum variants) in { rust_name; extract_name; keep_params; body_info } in @@ -240,7 +250,7 @@ let builtin_types () : builtin_type_info list = @ mk_lean_only [ mk_type "core::fmt::Formatter" (); - mk_type "core::result::Result" (); + mk_type "core::result::Result" ~kind:(KEnum [ "Ok"; "Err" ]) (); mk_type "core::fmt::Error" (); mk_type "core::array::TryFromSliceError" (); ] diff --git a/src/extract/ExtractTypes.ml b/src/extract/ExtractTypes.ml index b853f97d..6fdda868 100644 --- a/src/extract/ExtractTypes.ml +++ b/src/extract/ExtractTypes.ml @@ -859,7 +859,10 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : (field_names, cons_name) | Some info -> craise __FILE__ __LINE__ def.item_meta.span - ("Invalid builtin information: " ^ show_builtin_type_info info) + ("Invalid builtin information for type " + ^ name_to_string ctx def.item_meta.name + ^ ": expected builtin information about a structure, got:\n" + ^ show_builtin_type_info info) in (* Add the fields *) let ctx = @@ -902,9 +905,12 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : (fun variant_id (variant : variant) -> (variant_id, StringMap.find variant.variant_name variant_map)) variants - | _ -> + | Some info -> craise __FILE__ __LINE__ def.item_meta.span - "Invalid builtin information" + ("Invalid builtin information for type " + ^ name_to_string ctx def.item_meta.name + ^ ": expected builtin information about an enumeration, got:\n" + ^ show_builtin_type_info info) in List.fold_left (fun ctx (vid, vname) -> From 14194d88d1584afa0abbc12939e7b1d8823b3a78 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 4 Dec 2024 12:20:12 +0000 Subject: [PATCH 08/11] Make a minor modification --- src/extract/ExtractBuiltin.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml index ea353f17..0837bfb5 100644 --- a/src/extract/ExtractBuiltin.ml +++ b/src/extract/ExtractBuiltin.ml @@ -185,9 +185,15 @@ let builtin_types () : builtin_type_info list = let variants = List.map (fun variant -> + let extract_variant_name = + match backend () with + | FStar | Coq -> extract_name ^ "_" ^ variant + | Lean -> extract_name ^ "." ^ variant + | HOL4 -> extract_name ^ variant + in { rust_variant_name = variant; - extract_variant_name = variant; + extract_variant_name; fields = None; }) variants From e70f981801beb6f2eb3c2bde2f7283222fdc4631 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 4 Dec 2024 12:20:48 +0000 Subject: [PATCH 09/11] Regenerate the tests --- tests/coq/misc/External_Funs.v | 7 ------- tests/coq/misc/External_FunsExternal_Template.v | 2 +- tests/coq/misc/External_Types.v | 10 ---------- tests/fstar/misc/External.Funs.fst | 7 ------- tests/fstar/misc/External.FunsExternal.fsti | 2 +- tests/fstar/misc/External.Types.fst | 7 ------- tests/lean/External/Funs.lean | 8 -------- tests/lean/External/Types.lean | 6 ------ tests/lean/Traits.lean | 7 ------- tests/src/mutually-recursive-traits.lean.out | 2 +- 10 files changed, 3 insertions(+), 55 deletions(-) diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v index a3275de8..3594e22e 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -12,13 +12,6 @@ Require Import External_FunsExternal. Include External_FunsExternal. Module External_Funs. -(** Trait implementation: [core::marker::{core::marker::Copy for u32}#40] - Source: '/rustc/library/core/src/marker.rs', lines 48:25-48:62 - Name pattern: core::marker::Copy *) -Definition core_marker_CopyU32 : core_marker_Copy_t u32 := {| - core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst := core_clone_CloneU32; -|}. - (** [external::use_get]: Source: 'tests/src/external.rs', lines 9:0-11:1 *) Definition use_get diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v index 4de5c5c3..c3002326 100644 --- a/tests/coq/misc/External_FunsExternal_Template.v +++ b/tests/coq/misc/External_FunsExternal_Template.v @@ -15,7 +15,7 @@ Module External_FunsExternal_Template. Source: '/rustc/library/core/src/cell.rs', lines 540:4-540:32 Name pattern: core::cell::{core::cell::Cell<@T>}::get *) Axiom core_cell_Cell_get : - forall{T : Type} (markerCopyInst : core_marker_Copy_t T), + forall{T : Type} (markerCopyInst : core_marker_Copy T), core_cell_Cell_t T -> state -> result (state * T) . diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v index 7601795a..b42c2ecf 100644 --- a/tests/coq/misc/External_Types.v +++ b/tests/coq/misc/External_Types.v @@ -10,14 +10,4 @@ Require Import External_TypesExternal. Include External_TypesExternal. Module External_Types. -(** Trait declaration: [core::marker::Copy] - Source: '/rustc/library/core/src/marker.rs', lines 416:0-416:21 - Name pattern: core::marker::Copy *) -Record core_marker_Copy_t (Self : Type) := mkcore_marker_Copy_t { - core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst : core_clone_Clone Self; -}. - -Arguments mkcore_marker_Copy_t { _ }. -Arguments core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst { _ } _. - End External_Types. diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst index cba918b9..3208d825 100644 --- a/tests/fstar/misc/External.Funs.fst +++ b/tests/fstar/misc/External.Funs.fst @@ -7,13 +7,6 @@ include External.FunsExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** Trait implementation: [core::marker::{core::marker::Copy for u32}#40] - Source: '/rustc/library/core/src/marker.rs', lines 48:25-48:62 - Name pattern: core::marker::Copy *) -let core_marker_CopyU32 : core_marker_Copy_t u32 = { - cloneCloneInst = core_clone_CloneU32; -} - (** [external::use_get]: Source: 'tests/src/external.rs', lines 9:0-11:1 *) let use_get (rc : core_cell_Cell_t u32) (st : state) : result (state & u32) = diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti index 4f121396..9fca284e 100644 --- a/tests/fstar/misc/External.FunsExternal.fsti +++ b/tests/fstar/misc/External.FunsExternal.fsti @@ -10,7 +10,7 @@ include External.Types Source: '/rustc/library/core/src/cell.rs', lines 540:4-540:32 Name pattern: core::cell::{core::cell::Cell<@T>}::get *) val core_cell_Cell_get - (#t : Type0) (markerCopyInst : core_marker_Copy_t t) : + (#t : Type0) (markerCopyInst : core_marker_Copy t) : core_cell_Cell_t t -> state -> result (state & t) (** [core::cell::{core::cell::Cell}#11::get_mut]: diff --git a/tests/fstar/misc/External.Types.fst b/tests/fstar/misc/External.Types.fst index cb4fa57b..4fbcec47 100644 --- a/tests/fstar/misc/External.Types.fst +++ b/tests/fstar/misc/External.Types.fst @@ -6,10 +6,3 @@ include External.TypesExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** Trait declaration: [core::marker::Copy] - Source: '/rustc/library/core/src/marker.rs', lines 416:0-416:21 - Name pattern: core::marker::Copy *) -noeq type core_marker_Copy_t (self : Type0) = { - cloneCloneInst : core_clone_Clone self; -} - diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index 5e2975ec..6df57acf 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -10,14 +10,6 @@ set_option linter.unusedVariables false namespace external -/- Trait implementation: [core::marker::{core::marker::Copy for u32}#40] - Source: '/rustc/library/core/src/marker.rs', lines 48:25-48:62 - Name pattern: core::marker::Copy -/ -@[reducible] -def core.marker.CopyU32 : core.marker.Copy U32 := { - cloneCloneInst := core.clone.CloneU32 -} - /- [external::use_get]: Source: 'tests/src/external.rs', lines 9:0-11:1 -/ def use_get (rc : core.cell.Cell U32) (st : State) : Result (State × U32) := diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean index 5e64121e..789ce2b8 100644 --- a/tests/lean/External/Types.lean +++ b/tests/lean/External/Types.lean @@ -9,10 +9,4 @@ set_option linter.unusedVariables false namespace external -/- Trait declaration: [core::marker::Copy] - Source: '/rustc/library/core/src/marker.rs', lines 416:0-416:21 - Name pattern: core::marker::Copy -/ -structure core.marker.Copy (Self : Type) where - cloneCloneInst : core.clone.Clone Self - end external diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 77374ce7..93b17b90 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -518,13 +518,6 @@ structure Foo (T : Type) (U : Type) where x : T y : U -/- [core::result::Result] - Source: '/rustc/library/core/src/result.rs', lines 527:0-527:21 - Name pattern: core::result::Result -/ -inductive core.result.Result (T : Type) (E : Type) := -| Ok : T → core.result.Result T E -| Err : E → core.result.Result T E - /- [traits::{traits::Foo}#16::FOO] Source: 'tests/src/traits.rs', lines 334:4-334:43 -/ def Foo.FOO_body {T : Type} (U : Type) (TraitInst : Trait T) diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index 700af9ce..a45c2bb0 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -13,4 +13,4 @@ Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 879, characters 2-52 Called from Aeneas__Translate.extract_file in file "Translate.ml", line 1006, characters 2-36 Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1576, characters 5-42 -Called from Dune__exe__Main in file "Main.ml", line 336, characters 14-66 +Called from Dune__exe__Main in file "Main.ml", line 509, characters 14-66 From 6ca0aa851d25c46af2b2895f281537fda148c1e4 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 5 Dec 2024 11:54:07 +0000 Subject: [PATCH 10/11] Update the Coq and F* backends --- backends/coq/Primitives.v | 68 +++++++++++++++++++++++++++++++---- backends/fstar/Primitives.fst | 52 +++++++++++++++++++++++++++ 2 files changed, 114 insertions(+), 6 deletions(-) diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v index 7ce37c4c..72122740 100644 --- a/backends/coq/Primitives.v +++ b/backends/coq/Primitives.v @@ -510,12 +510,6 @@ Record core_clone_Clone (self : Type) := { clone : self -> result self }. -Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. - -Definition core_clone_CloneBool : core_clone_Clone bool := {| - clone := fun b => Ok (core_clone_impls_CloneBool_clone b) -|}. - Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x. Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x. Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x. @@ -578,6 +572,68 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {| clone := fun x => Ok (core_clone_impls_CloneI128_clone x) |}. +Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. + +Definition core_clone_CloneBool : core_clone_Clone bool := {| + clone := fun b => Ok (core_clone_impls_CloneBool_clone b) +|}. + +Record core_marker_Copy_t (Self : Type) := mkcore_marker_Copy_t { + coreCloneInst : core_clone_Clone Self; +}. + +Arguments mkcore_marker_Copy_t { _ }. +Arguments coreCloneInst { _ } _. + +Definition core_marker_CopyU8 : core_marker_Copy_t u8 := {| + coreCloneInst := core_clone_CloneU8; +|}. + +Definition core_marker_CopyU16 : core_marker_Copy_t u16 := {| + coreCloneInst := core_clone_CloneU16; +|}. + +Definition core_marker_CopyU32 : core_marker_Copy_t u32 := {| + coreCloneInst := core_clone_CloneU32; +|}. + +Definition core_marker_CopyU64 : core_marker_Copy_t u64 := {| + coreCloneInst := core_clone_CloneU64; +|}. + +Definition core_marker_CopyU128 : core_marker_Copy_t u128 := {| + coreCloneInst := core_clone_CloneU128; +|}. + +Definition core_marker_CopyUsize : core_marker_Copy_t usize := {| + coreCloneInst := core_clone_CloneUsize; +|}. + +Definition core_marker_CopyI8 : core_marker_Copy_t i8 := {| + coreCloneInst := core_clone_CloneI8; +|}. + +Definition core_marker_CopyI16 : core_marker_Copy_t i16 := {| + coreCloneInst := core_clone_CloneI16; +|}. + +Definition core_marker_CopyI32 : core_marker_Copy_t i32 := {| + coreCloneInst := core_clone_CloneI32; +|}. + +Definition core_marker_CopyI64 : core_marker_Copy_t i64 := {| + coreCloneInst := core_clone_CloneI64; +|}. + +Definition core_marker_CopyI128 : core_marker_Copy_t i128 := {| + coreCloneInst := core_clone_CloneI128; +|}. + +Definition core_marker_CopyIsize : core_marker_Copy_t isize := {| + coreCloneInst := core_clone_CloneIsize; +|}. + + (** [core::option::{core::option::Option}::unwrap] *) Definition core_option_Option_unwrap {T : Type} (x : option T) : result T := match x with diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index a22d449f..f9f4b9f0 100644 --- a/backends/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst @@ -556,6 +556,58 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +noeq type core_marker_Copy_t (self : Type0) = { + cloneCloneInst : core_clone_Clone self; +} + +let core_marker_CopyU8 : core_marker_Copy_t u8 = { + cloneCloneInst = core_clone_CloneU8; +} + +let core_marker_CopyU16 : core_marker_Copy_t u16 = { + cloneCloneInst = core_clone_CloneU16; +} + +let core_marker_CopyU32 : core_marker_Copy_t u32 = { + cloneCloneInst = core_clone_CloneU32; +} + +let core_marker_CopyU64 : core_marker_Copy_t u64 = { + cloneCloneInst = core_clone_CloneU64; +} + +let core_marker_CopyU128 : core_marker_Copy_t u128 = { + cloneCloneInst = core_clone_CloneU128; +} + +let core_marker_CopyUsize : core_marker_Copy_t usize = { + cloneCloneInst = core_clone_CloneUsize; +} + +let core_marker_CopyI8 : core_marker_Copy_t i8 = { + cloneCloneInst = core_clone_CloneI8; +} + +let core_marker_CopyI16 : core_marker_Copy_t i16 = { + cloneCloneInst = core_clone_CloneI16; +} + +let core_marker_CopyI32 : core_marker_Copy_t i32 = { + cloneCloneInst = core_clone_CloneI32; +} + +let core_marker_CopyI64 : core_marker_Copy_t i64 = { + cloneCloneInst = core_clone_CloneI64; +} + +let core_marker_CopyI128 : core_marker_Copy_t i128 = { + cloneCloneInst = core_clone_CloneI128; +} + +let core_marker_CopyIsize : core_marker_Copy_t isize = { + cloneCloneInst = core_clone_CloneIsize; +} + (** [core::option::{core::option::Option}::unwrap] *) let core_option_Option_unwrap (#t : Type0) (x : option t) : result t = match x with From 4736339b5c52b69cd280dd98a28d0d5df6f45174 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 5 Dec 2024 12:55:16 +0000 Subject: [PATCH 11/11] Update the F* and Coq backends and regenerate the files --- backends/coq/Primitives.v | 29 +++++---- backends/fstar/Primitives.fst | 26 ++++---- tests/coq/arrays/Primitives.v | 67 +++++++++++++++++++-- tests/coq/betree/Primitives.v | 67 +++++++++++++++++++-- tests/coq/demo/Primitives.v | 67 +++++++++++++++++++-- tests/coq/hashmap/Primitives.v | 67 +++++++++++++++++++-- tests/coq/misc/External_FunsExternal.v | 2 +- tests/coq/misc/Primitives.v | 67 +++++++++++++++++++-- tests/coq/rename_attribute/Primitives.v | 67 +++++++++++++++++++-- tests/coq/traits/Primitives.v | 67 +++++++++++++++++++-- tests/fstar/arrays/Primitives.fst | 52 ++++++++++++++++ tests/fstar/betree/Primitives.fst | 52 ++++++++++++++++ tests/fstar/demo/Primitives.fst | 52 ++++++++++++++++ tests/fstar/hashmap/Primitives.fst | 52 ++++++++++++++++ tests/fstar/misc/Primitives.fst | 52 ++++++++++++++++ tests/fstar/rename_attribute/Primitives.fst | 52 ++++++++++++++++ tests/fstar/traits/Primitives.fst | 52 ++++++++++++++++ 17 files changed, 819 insertions(+), 71 deletions(-) diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v index 72122740..cc36ab25 100644 --- a/backends/coq/Primitives.v +++ b/backends/coq/Primitives.v @@ -578,62 +578,61 @@ Definition core_clone_CloneBool : core_clone_Clone bool := {| clone := fun b => Ok (core_clone_impls_CloneBool_clone b) |}. -Record core_marker_Copy_t (Self : Type) := mkcore_marker_Copy_t { +Record core_marker_Copy (Self : Type) := mkcore_marker_Copy { coreCloneInst : core_clone_Clone Self; }. -Arguments mkcore_marker_Copy_t { _ }. +Arguments mkcore_marker_Copy { _ }. Arguments coreCloneInst { _ } _. -Definition core_marker_CopyU8 : core_marker_Copy_t u8 := {| +Definition core_marker_CopyU8 : core_marker_Copy u8 := {| coreCloneInst := core_clone_CloneU8; |}. -Definition core_marker_CopyU16 : core_marker_Copy_t u16 := {| +Definition core_marker_CopyU16 : core_marker_Copy u16 := {| coreCloneInst := core_clone_CloneU16; |}. -Definition core_marker_CopyU32 : core_marker_Copy_t u32 := {| +Definition core_marker_CopyU32 : core_marker_Copy u32 := {| coreCloneInst := core_clone_CloneU32; |}. -Definition core_marker_CopyU64 : core_marker_Copy_t u64 := {| +Definition core_marker_CopyU64 : core_marker_Copy u64 := {| coreCloneInst := core_clone_CloneU64; |}. -Definition core_marker_CopyU128 : core_marker_Copy_t u128 := {| +Definition core_marker_CopyU128 : core_marker_Copy u128 := {| coreCloneInst := core_clone_CloneU128; |}. -Definition core_marker_CopyUsize : core_marker_Copy_t usize := {| +Definition core_marker_CopyUsize : core_marker_Copy usize := {| coreCloneInst := core_clone_CloneUsize; |}. -Definition core_marker_CopyI8 : core_marker_Copy_t i8 := {| +Definition core_marker_CopyI8 : core_marker_Copy i8 := {| coreCloneInst := core_clone_CloneI8; |}. -Definition core_marker_CopyI16 : core_marker_Copy_t i16 := {| +Definition core_marker_CopyI16 : core_marker_Copy i16 := {| coreCloneInst := core_clone_CloneI16; |}. -Definition core_marker_CopyI32 : core_marker_Copy_t i32 := {| +Definition core_marker_CopyI32 : core_marker_Copy i32 := {| coreCloneInst := core_clone_CloneI32; |}. -Definition core_marker_CopyI64 : core_marker_Copy_t i64 := {| +Definition core_marker_CopyI64 : core_marker_Copy i64 := {| coreCloneInst := core_clone_CloneI64; |}. -Definition core_marker_CopyI128 : core_marker_Copy_t i128 := {| +Definition core_marker_CopyI128 : core_marker_Copy i128 := {| coreCloneInst := core_clone_CloneI128; |}. -Definition core_marker_CopyIsize : core_marker_Copy_t isize := {| +Definition core_marker_CopyIsize : core_marker_Copy isize := {| coreCloneInst := core_clone_CloneIsize; |}. - (** [core::option::{core::option::Option}::unwrap] *) Definition core_option_Option_unwrap {T : Type} (x : option T) : result T := match x with diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index f9f4b9f0..a7a007f1 100644 --- a/backends/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst @@ -556,55 +556,55 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } -noeq type core_marker_Copy_t (self : Type0) = { +noeq type core_marker_Copy (self : Type0) = { cloneCloneInst : core_clone_Clone self; } -let core_marker_CopyU8 : core_marker_Copy_t u8 = { +let core_marker_CopyU8 : core_marker_Copy u8 = { cloneCloneInst = core_clone_CloneU8; } -let core_marker_CopyU16 : core_marker_Copy_t u16 = { +let core_marker_CopyU16 : core_marker_Copy u16 = { cloneCloneInst = core_clone_CloneU16; } -let core_marker_CopyU32 : core_marker_Copy_t u32 = { +let core_marker_CopyU32 : core_marker_Copy u32 = { cloneCloneInst = core_clone_CloneU32; } -let core_marker_CopyU64 : core_marker_Copy_t u64 = { +let core_marker_CopyU64 : core_marker_Copy u64 = { cloneCloneInst = core_clone_CloneU64; } -let core_marker_CopyU128 : core_marker_Copy_t u128 = { +let core_marker_CopyU128 : core_marker_Copy u128 = { cloneCloneInst = core_clone_CloneU128; } -let core_marker_CopyUsize : core_marker_Copy_t usize = { +let core_marker_CopyUsize : core_marker_Copy usize = { cloneCloneInst = core_clone_CloneUsize; } -let core_marker_CopyI8 : core_marker_Copy_t i8 = { +let core_marker_CopyI8 : core_marker_Copy i8 = { cloneCloneInst = core_clone_CloneI8; } -let core_marker_CopyI16 : core_marker_Copy_t i16 = { +let core_marker_CopyI16 : core_marker_Copy i16 = { cloneCloneInst = core_clone_CloneI16; } -let core_marker_CopyI32 : core_marker_Copy_t i32 = { +let core_marker_CopyI32 : core_marker_Copy i32 = { cloneCloneInst = core_clone_CloneI32; } -let core_marker_CopyI64 : core_marker_Copy_t i64 = { +let core_marker_CopyI64 : core_marker_Copy i64 = { cloneCloneInst = core_clone_CloneI64; } -let core_marker_CopyI128 : core_marker_Copy_t i128 = { +let core_marker_CopyI128 : core_marker_Copy i128 = { cloneCloneInst = core_clone_CloneI128; } -let core_marker_CopyIsize : core_marker_Copy_t isize = { +let core_marker_CopyIsize : core_marker_Copy isize = { cloneCloneInst = core_clone_CloneIsize; } diff --git a/tests/coq/arrays/Primitives.v b/tests/coq/arrays/Primitives.v index 7ce37c4c..cc36ab25 100644 --- a/tests/coq/arrays/Primitives.v +++ b/tests/coq/arrays/Primitives.v @@ -510,12 +510,6 @@ Record core_clone_Clone (self : Type) := { clone : self -> result self }. -Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. - -Definition core_clone_CloneBool : core_clone_Clone bool := {| - clone := fun b => Ok (core_clone_impls_CloneBool_clone b) -|}. - Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x. Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x. Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x. @@ -578,6 +572,67 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {| clone := fun x => Ok (core_clone_impls_CloneI128_clone x) |}. +Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. + +Definition core_clone_CloneBool : core_clone_Clone bool := {| + clone := fun b => Ok (core_clone_impls_CloneBool_clone b) +|}. + +Record core_marker_Copy (Self : Type) := mkcore_marker_Copy { + coreCloneInst : core_clone_Clone Self; +}. + +Arguments mkcore_marker_Copy { _ }. +Arguments coreCloneInst { _ } _. + +Definition core_marker_CopyU8 : core_marker_Copy u8 := {| + coreCloneInst := core_clone_CloneU8; +|}. + +Definition core_marker_CopyU16 : core_marker_Copy u16 := {| + coreCloneInst := core_clone_CloneU16; +|}. + +Definition core_marker_CopyU32 : core_marker_Copy u32 := {| + coreCloneInst := core_clone_CloneU32; +|}. + +Definition core_marker_CopyU64 : core_marker_Copy u64 := {| + coreCloneInst := core_clone_CloneU64; +|}. + +Definition core_marker_CopyU128 : core_marker_Copy u128 := {| + coreCloneInst := core_clone_CloneU128; +|}. + +Definition core_marker_CopyUsize : core_marker_Copy usize := {| + coreCloneInst := core_clone_CloneUsize; +|}. + +Definition core_marker_CopyI8 : core_marker_Copy i8 := {| + coreCloneInst := core_clone_CloneI8; +|}. + +Definition core_marker_CopyI16 : core_marker_Copy i16 := {| + coreCloneInst := core_clone_CloneI16; +|}. + +Definition core_marker_CopyI32 : core_marker_Copy i32 := {| + coreCloneInst := core_clone_CloneI32; +|}. + +Definition core_marker_CopyI64 : core_marker_Copy i64 := {| + coreCloneInst := core_clone_CloneI64; +|}. + +Definition core_marker_CopyI128 : core_marker_Copy i128 := {| + coreCloneInst := core_clone_CloneI128; +|}. + +Definition core_marker_CopyIsize : core_marker_Copy isize := {| + coreCloneInst := core_clone_CloneIsize; +|}. + (** [core::option::{core::option::Option}::unwrap] *) Definition core_option_Option_unwrap {T : Type} (x : option T) : result T := match x with diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v index 7ce37c4c..cc36ab25 100644 --- a/tests/coq/betree/Primitives.v +++ b/tests/coq/betree/Primitives.v @@ -510,12 +510,6 @@ Record core_clone_Clone (self : Type) := { clone : self -> result self }. -Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. - -Definition core_clone_CloneBool : core_clone_Clone bool := {| - clone := fun b => Ok (core_clone_impls_CloneBool_clone b) -|}. - Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x. Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x. Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x. @@ -578,6 +572,67 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {| clone := fun x => Ok (core_clone_impls_CloneI128_clone x) |}. +Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. + +Definition core_clone_CloneBool : core_clone_Clone bool := {| + clone := fun b => Ok (core_clone_impls_CloneBool_clone b) +|}. + +Record core_marker_Copy (Self : Type) := mkcore_marker_Copy { + coreCloneInst : core_clone_Clone Self; +}. + +Arguments mkcore_marker_Copy { _ }. +Arguments coreCloneInst { _ } _. + +Definition core_marker_CopyU8 : core_marker_Copy u8 := {| + coreCloneInst := core_clone_CloneU8; +|}. + +Definition core_marker_CopyU16 : core_marker_Copy u16 := {| + coreCloneInst := core_clone_CloneU16; +|}. + +Definition core_marker_CopyU32 : core_marker_Copy u32 := {| + coreCloneInst := core_clone_CloneU32; +|}. + +Definition core_marker_CopyU64 : core_marker_Copy u64 := {| + coreCloneInst := core_clone_CloneU64; +|}. + +Definition core_marker_CopyU128 : core_marker_Copy u128 := {| + coreCloneInst := core_clone_CloneU128; +|}. + +Definition core_marker_CopyUsize : core_marker_Copy usize := {| + coreCloneInst := core_clone_CloneUsize; +|}. + +Definition core_marker_CopyI8 : core_marker_Copy i8 := {| + coreCloneInst := core_clone_CloneI8; +|}. + +Definition core_marker_CopyI16 : core_marker_Copy i16 := {| + coreCloneInst := core_clone_CloneI16; +|}. + +Definition core_marker_CopyI32 : core_marker_Copy i32 := {| + coreCloneInst := core_clone_CloneI32; +|}. + +Definition core_marker_CopyI64 : core_marker_Copy i64 := {| + coreCloneInst := core_clone_CloneI64; +|}. + +Definition core_marker_CopyI128 : core_marker_Copy i128 := {| + coreCloneInst := core_clone_CloneI128; +|}. + +Definition core_marker_CopyIsize : core_marker_Copy isize := {| + coreCloneInst := core_clone_CloneIsize; +|}. + (** [core::option::{core::option::Option}::unwrap] *) Definition core_option_Option_unwrap {T : Type} (x : option T) : result T := match x with diff --git a/tests/coq/demo/Primitives.v b/tests/coq/demo/Primitives.v index 7ce37c4c..cc36ab25 100644 --- a/tests/coq/demo/Primitives.v +++ b/tests/coq/demo/Primitives.v @@ -510,12 +510,6 @@ Record core_clone_Clone (self : Type) := { clone : self -> result self }. -Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. - -Definition core_clone_CloneBool : core_clone_Clone bool := {| - clone := fun b => Ok (core_clone_impls_CloneBool_clone b) -|}. - Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x. Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x. Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x. @@ -578,6 +572,67 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {| clone := fun x => Ok (core_clone_impls_CloneI128_clone x) |}. +Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. + +Definition core_clone_CloneBool : core_clone_Clone bool := {| + clone := fun b => Ok (core_clone_impls_CloneBool_clone b) +|}. + +Record core_marker_Copy (Self : Type) := mkcore_marker_Copy { + coreCloneInst : core_clone_Clone Self; +}. + +Arguments mkcore_marker_Copy { _ }. +Arguments coreCloneInst { _ } _. + +Definition core_marker_CopyU8 : core_marker_Copy u8 := {| + coreCloneInst := core_clone_CloneU8; +|}. + +Definition core_marker_CopyU16 : core_marker_Copy u16 := {| + coreCloneInst := core_clone_CloneU16; +|}. + +Definition core_marker_CopyU32 : core_marker_Copy u32 := {| + coreCloneInst := core_clone_CloneU32; +|}. + +Definition core_marker_CopyU64 : core_marker_Copy u64 := {| + coreCloneInst := core_clone_CloneU64; +|}. + +Definition core_marker_CopyU128 : core_marker_Copy u128 := {| + coreCloneInst := core_clone_CloneU128; +|}. + +Definition core_marker_CopyUsize : core_marker_Copy usize := {| + coreCloneInst := core_clone_CloneUsize; +|}. + +Definition core_marker_CopyI8 : core_marker_Copy i8 := {| + coreCloneInst := core_clone_CloneI8; +|}. + +Definition core_marker_CopyI16 : core_marker_Copy i16 := {| + coreCloneInst := core_clone_CloneI16; +|}. + +Definition core_marker_CopyI32 : core_marker_Copy i32 := {| + coreCloneInst := core_clone_CloneI32; +|}. + +Definition core_marker_CopyI64 : core_marker_Copy i64 := {| + coreCloneInst := core_clone_CloneI64; +|}. + +Definition core_marker_CopyI128 : core_marker_Copy i128 := {| + coreCloneInst := core_clone_CloneI128; +|}. + +Definition core_marker_CopyIsize : core_marker_Copy isize := {| + coreCloneInst := core_clone_CloneIsize; +|}. + (** [core::option::{core::option::Option}::unwrap] *) Definition core_option_Option_unwrap {T : Type} (x : option T) : result T := match x with diff --git a/tests/coq/hashmap/Primitives.v b/tests/coq/hashmap/Primitives.v index 7ce37c4c..cc36ab25 100644 --- a/tests/coq/hashmap/Primitives.v +++ b/tests/coq/hashmap/Primitives.v @@ -510,12 +510,6 @@ Record core_clone_Clone (self : Type) := { clone : self -> result self }. -Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. - -Definition core_clone_CloneBool : core_clone_Clone bool := {| - clone := fun b => Ok (core_clone_impls_CloneBool_clone b) -|}. - Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x. Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x. Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x. @@ -578,6 +572,67 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {| clone := fun x => Ok (core_clone_impls_CloneI128_clone x) |}. +Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. + +Definition core_clone_CloneBool : core_clone_Clone bool := {| + clone := fun b => Ok (core_clone_impls_CloneBool_clone b) +|}. + +Record core_marker_Copy (Self : Type) := mkcore_marker_Copy { + coreCloneInst : core_clone_Clone Self; +}. + +Arguments mkcore_marker_Copy { _ }. +Arguments coreCloneInst { _ } _. + +Definition core_marker_CopyU8 : core_marker_Copy u8 := {| + coreCloneInst := core_clone_CloneU8; +|}. + +Definition core_marker_CopyU16 : core_marker_Copy u16 := {| + coreCloneInst := core_clone_CloneU16; +|}. + +Definition core_marker_CopyU32 : core_marker_Copy u32 := {| + coreCloneInst := core_clone_CloneU32; +|}. + +Definition core_marker_CopyU64 : core_marker_Copy u64 := {| + coreCloneInst := core_clone_CloneU64; +|}. + +Definition core_marker_CopyU128 : core_marker_Copy u128 := {| + coreCloneInst := core_clone_CloneU128; +|}. + +Definition core_marker_CopyUsize : core_marker_Copy usize := {| + coreCloneInst := core_clone_CloneUsize; +|}. + +Definition core_marker_CopyI8 : core_marker_Copy i8 := {| + coreCloneInst := core_clone_CloneI8; +|}. + +Definition core_marker_CopyI16 : core_marker_Copy i16 := {| + coreCloneInst := core_clone_CloneI16; +|}. + +Definition core_marker_CopyI32 : core_marker_Copy i32 := {| + coreCloneInst := core_clone_CloneI32; +|}. + +Definition core_marker_CopyI64 : core_marker_Copy i64 := {| + coreCloneInst := core_clone_CloneI64; +|}. + +Definition core_marker_CopyI128 : core_marker_Copy i128 := {| + coreCloneInst := core_clone_CloneI128; +|}. + +Definition core_marker_CopyIsize : core_marker_Copy isize := {| + coreCloneInst := core_clone_CloneIsize; +|}. + (** [core::option::{core::option::Option}::unwrap] *) Definition core_option_Option_unwrap {T : Type} (x : option T) : result T := match x with diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v index e47741d1..af3d589e 100644 --- a/tests/coq/misc/External_FunsExternal.v +++ b/tests/coq/misc/External_FunsExternal.v @@ -10,7 +10,7 @@ Include External_Types. Module External_FunsExternal. Axiom core_cell_Cell_get : - forall{T : Type} (markerCopyInst : core_marker_Copy_t T), + forall{T : Type} (markerCopyInst : core_marker_Copy T), core_cell_Cell_t T -> state -> result (state * T) . diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v index 7ce37c4c..cc36ab25 100644 --- a/tests/coq/misc/Primitives.v +++ b/tests/coq/misc/Primitives.v @@ -510,12 +510,6 @@ Record core_clone_Clone (self : Type) := { clone : self -> result self }. -Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. - -Definition core_clone_CloneBool : core_clone_Clone bool := {| - clone := fun b => Ok (core_clone_impls_CloneBool_clone b) -|}. - Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x. Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x. Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x. @@ -578,6 +572,67 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {| clone := fun x => Ok (core_clone_impls_CloneI128_clone x) |}. +Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. + +Definition core_clone_CloneBool : core_clone_Clone bool := {| + clone := fun b => Ok (core_clone_impls_CloneBool_clone b) +|}. + +Record core_marker_Copy (Self : Type) := mkcore_marker_Copy { + coreCloneInst : core_clone_Clone Self; +}. + +Arguments mkcore_marker_Copy { _ }. +Arguments coreCloneInst { _ } _. + +Definition core_marker_CopyU8 : core_marker_Copy u8 := {| + coreCloneInst := core_clone_CloneU8; +|}. + +Definition core_marker_CopyU16 : core_marker_Copy u16 := {| + coreCloneInst := core_clone_CloneU16; +|}. + +Definition core_marker_CopyU32 : core_marker_Copy u32 := {| + coreCloneInst := core_clone_CloneU32; +|}. + +Definition core_marker_CopyU64 : core_marker_Copy u64 := {| + coreCloneInst := core_clone_CloneU64; +|}. + +Definition core_marker_CopyU128 : core_marker_Copy u128 := {| + coreCloneInst := core_clone_CloneU128; +|}. + +Definition core_marker_CopyUsize : core_marker_Copy usize := {| + coreCloneInst := core_clone_CloneUsize; +|}. + +Definition core_marker_CopyI8 : core_marker_Copy i8 := {| + coreCloneInst := core_clone_CloneI8; +|}. + +Definition core_marker_CopyI16 : core_marker_Copy i16 := {| + coreCloneInst := core_clone_CloneI16; +|}. + +Definition core_marker_CopyI32 : core_marker_Copy i32 := {| + coreCloneInst := core_clone_CloneI32; +|}. + +Definition core_marker_CopyI64 : core_marker_Copy i64 := {| + coreCloneInst := core_clone_CloneI64; +|}. + +Definition core_marker_CopyI128 : core_marker_Copy i128 := {| + coreCloneInst := core_clone_CloneI128; +|}. + +Definition core_marker_CopyIsize : core_marker_Copy isize := {| + coreCloneInst := core_clone_CloneIsize; +|}. + (** [core::option::{core::option::Option}::unwrap] *) Definition core_option_Option_unwrap {T : Type} (x : option T) : result T := match x with diff --git a/tests/coq/rename_attribute/Primitives.v b/tests/coq/rename_attribute/Primitives.v index 7ce37c4c..cc36ab25 100644 --- a/tests/coq/rename_attribute/Primitives.v +++ b/tests/coq/rename_attribute/Primitives.v @@ -510,12 +510,6 @@ Record core_clone_Clone (self : Type) := { clone : self -> result self }. -Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. - -Definition core_clone_CloneBool : core_clone_Clone bool := {| - clone := fun b => Ok (core_clone_impls_CloneBool_clone b) -|}. - Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x. Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x. Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x. @@ -578,6 +572,67 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {| clone := fun x => Ok (core_clone_impls_CloneI128_clone x) |}. +Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. + +Definition core_clone_CloneBool : core_clone_Clone bool := {| + clone := fun b => Ok (core_clone_impls_CloneBool_clone b) +|}. + +Record core_marker_Copy (Self : Type) := mkcore_marker_Copy { + coreCloneInst : core_clone_Clone Self; +}. + +Arguments mkcore_marker_Copy { _ }. +Arguments coreCloneInst { _ } _. + +Definition core_marker_CopyU8 : core_marker_Copy u8 := {| + coreCloneInst := core_clone_CloneU8; +|}. + +Definition core_marker_CopyU16 : core_marker_Copy u16 := {| + coreCloneInst := core_clone_CloneU16; +|}. + +Definition core_marker_CopyU32 : core_marker_Copy u32 := {| + coreCloneInst := core_clone_CloneU32; +|}. + +Definition core_marker_CopyU64 : core_marker_Copy u64 := {| + coreCloneInst := core_clone_CloneU64; +|}. + +Definition core_marker_CopyU128 : core_marker_Copy u128 := {| + coreCloneInst := core_clone_CloneU128; +|}. + +Definition core_marker_CopyUsize : core_marker_Copy usize := {| + coreCloneInst := core_clone_CloneUsize; +|}. + +Definition core_marker_CopyI8 : core_marker_Copy i8 := {| + coreCloneInst := core_clone_CloneI8; +|}. + +Definition core_marker_CopyI16 : core_marker_Copy i16 := {| + coreCloneInst := core_clone_CloneI16; +|}. + +Definition core_marker_CopyI32 : core_marker_Copy i32 := {| + coreCloneInst := core_clone_CloneI32; +|}. + +Definition core_marker_CopyI64 : core_marker_Copy i64 := {| + coreCloneInst := core_clone_CloneI64; +|}. + +Definition core_marker_CopyI128 : core_marker_Copy i128 := {| + coreCloneInst := core_clone_CloneI128; +|}. + +Definition core_marker_CopyIsize : core_marker_Copy isize := {| + coreCloneInst := core_clone_CloneIsize; +|}. + (** [core::option::{core::option::Option}::unwrap] *) Definition core_option_Option_unwrap {T : Type} (x : option T) : result T := match x with diff --git a/tests/coq/traits/Primitives.v b/tests/coq/traits/Primitives.v index 7ce37c4c..cc36ab25 100644 --- a/tests/coq/traits/Primitives.v +++ b/tests/coq/traits/Primitives.v @@ -510,12 +510,6 @@ Record core_clone_Clone (self : Type) := { clone : self -> result self }. -Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. - -Definition core_clone_CloneBool : core_clone_Clone bool := {| - clone := fun b => Ok (core_clone_impls_CloneBool_clone b) -|}. - Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x. Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x. Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x. @@ -578,6 +572,67 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {| clone := fun x => Ok (core_clone_impls_CloneI128_clone x) |}. +Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. + +Definition core_clone_CloneBool : core_clone_Clone bool := {| + clone := fun b => Ok (core_clone_impls_CloneBool_clone b) +|}. + +Record core_marker_Copy (Self : Type) := mkcore_marker_Copy { + coreCloneInst : core_clone_Clone Self; +}. + +Arguments mkcore_marker_Copy { _ }. +Arguments coreCloneInst { _ } _. + +Definition core_marker_CopyU8 : core_marker_Copy u8 := {| + coreCloneInst := core_clone_CloneU8; +|}. + +Definition core_marker_CopyU16 : core_marker_Copy u16 := {| + coreCloneInst := core_clone_CloneU16; +|}. + +Definition core_marker_CopyU32 : core_marker_Copy u32 := {| + coreCloneInst := core_clone_CloneU32; +|}. + +Definition core_marker_CopyU64 : core_marker_Copy u64 := {| + coreCloneInst := core_clone_CloneU64; +|}. + +Definition core_marker_CopyU128 : core_marker_Copy u128 := {| + coreCloneInst := core_clone_CloneU128; +|}. + +Definition core_marker_CopyUsize : core_marker_Copy usize := {| + coreCloneInst := core_clone_CloneUsize; +|}. + +Definition core_marker_CopyI8 : core_marker_Copy i8 := {| + coreCloneInst := core_clone_CloneI8; +|}. + +Definition core_marker_CopyI16 : core_marker_Copy i16 := {| + coreCloneInst := core_clone_CloneI16; +|}. + +Definition core_marker_CopyI32 : core_marker_Copy i32 := {| + coreCloneInst := core_clone_CloneI32; +|}. + +Definition core_marker_CopyI64 : core_marker_Copy i64 := {| + coreCloneInst := core_clone_CloneI64; +|}. + +Definition core_marker_CopyI128 : core_marker_Copy i128 := {| + coreCloneInst := core_clone_CloneI128; +|}. + +Definition core_marker_CopyIsize : core_marker_Copy isize := {| + coreCloneInst := core_clone_CloneIsize; +|}. + (** [core::option::{core::option::Option}::unwrap] *) Definition core_option_Option_unwrap {T : Type} (x : option T) : result T := match x with diff --git a/tests/fstar/arrays/Primitives.fst b/tests/fstar/arrays/Primitives.fst index a22d449f..a7a007f1 100644 --- a/tests/fstar/arrays/Primitives.fst +++ b/tests/fstar/arrays/Primitives.fst @@ -556,6 +556,58 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +noeq type core_marker_Copy (self : Type0) = { + cloneCloneInst : core_clone_Clone self; +} + +let core_marker_CopyU8 : core_marker_Copy u8 = { + cloneCloneInst = core_clone_CloneU8; +} + +let core_marker_CopyU16 : core_marker_Copy u16 = { + cloneCloneInst = core_clone_CloneU16; +} + +let core_marker_CopyU32 : core_marker_Copy u32 = { + cloneCloneInst = core_clone_CloneU32; +} + +let core_marker_CopyU64 : core_marker_Copy u64 = { + cloneCloneInst = core_clone_CloneU64; +} + +let core_marker_CopyU128 : core_marker_Copy u128 = { + cloneCloneInst = core_clone_CloneU128; +} + +let core_marker_CopyUsize : core_marker_Copy usize = { + cloneCloneInst = core_clone_CloneUsize; +} + +let core_marker_CopyI8 : core_marker_Copy i8 = { + cloneCloneInst = core_clone_CloneI8; +} + +let core_marker_CopyI16 : core_marker_Copy i16 = { + cloneCloneInst = core_clone_CloneI16; +} + +let core_marker_CopyI32 : core_marker_Copy i32 = { + cloneCloneInst = core_clone_CloneI32; +} + +let core_marker_CopyI64 : core_marker_Copy i64 = { + cloneCloneInst = core_clone_CloneI64; +} + +let core_marker_CopyI128 : core_marker_Copy i128 = { + cloneCloneInst = core_clone_CloneI128; +} + +let core_marker_CopyIsize : core_marker_Copy isize = { + cloneCloneInst = core_clone_CloneIsize; +} + (** [core::option::{core::option::Option}::unwrap] *) let core_option_Option_unwrap (#t : Type0) (x : option t) : result t = match x with diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst index a22d449f..a7a007f1 100644 --- a/tests/fstar/betree/Primitives.fst +++ b/tests/fstar/betree/Primitives.fst @@ -556,6 +556,58 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +noeq type core_marker_Copy (self : Type0) = { + cloneCloneInst : core_clone_Clone self; +} + +let core_marker_CopyU8 : core_marker_Copy u8 = { + cloneCloneInst = core_clone_CloneU8; +} + +let core_marker_CopyU16 : core_marker_Copy u16 = { + cloneCloneInst = core_clone_CloneU16; +} + +let core_marker_CopyU32 : core_marker_Copy u32 = { + cloneCloneInst = core_clone_CloneU32; +} + +let core_marker_CopyU64 : core_marker_Copy u64 = { + cloneCloneInst = core_clone_CloneU64; +} + +let core_marker_CopyU128 : core_marker_Copy u128 = { + cloneCloneInst = core_clone_CloneU128; +} + +let core_marker_CopyUsize : core_marker_Copy usize = { + cloneCloneInst = core_clone_CloneUsize; +} + +let core_marker_CopyI8 : core_marker_Copy i8 = { + cloneCloneInst = core_clone_CloneI8; +} + +let core_marker_CopyI16 : core_marker_Copy i16 = { + cloneCloneInst = core_clone_CloneI16; +} + +let core_marker_CopyI32 : core_marker_Copy i32 = { + cloneCloneInst = core_clone_CloneI32; +} + +let core_marker_CopyI64 : core_marker_Copy i64 = { + cloneCloneInst = core_clone_CloneI64; +} + +let core_marker_CopyI128 : core_marker_Copy i128 = { + cloneCloneInst = core_clone_CloneI128; +} + +let core_marker_CopyIsize : core_marker_Copy isize = { + cloneCloneInst = core_clone_CloneIsize; +} + (** [core::option::{core::option::Option}::unwrap] *) let core_option_Option_unwrap (#t : Type0) (x : option t) : result t = match x with diff --git a/tests/fstar/demo/Primitives.fst b/tests/fstar/demo/Primitives.fst index a22d449f..a7a007f1 100644 --- a/tests/fstar/demo/Primitives.fst +++ b/tests/fstar/demo/Primitives.fst @@ -556,6 +556,58 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +noeq type core_marker_Copy (self : Type0) = { + cloneCloneInst : core_clone_Clone self; +} + +let core_marker_CopyU8 : core_marker_Copy u8 = { + cloneCloneInst = core_clone_CloneU8; +} + +let core_marker_CopyU16 : core_marker_Copy u16 = { + cloneCloneInst = core_clone_CloneU16; +} + +let core_marker_CopyU32 : core_marker_Copy u32 = { + cloneCloneInst = core_clone_CloneU32; +} + +let core_marker_CopyU64 : core_marker_Copy u64 = { + cloneCloneInst = core_clone_CloneU64; +} + +let core_marker_CopyU128 : core_marker_Copy u128 = { + cloneCloneInst = core_clone_CloneU128; +} + +let core_marker_CopyUsize : core_marker_Copy usize = { + cloneCloneInst = core_clone_CloneUsize; +} + +let core_marker_CopyI8 : core_marker_Copy i8 = { + cloneCloneInst = core_clone_CloneI8; +} + +let core_marker_CopyI16 : core_marker_Copy i16 = { + cloneCloneInst = core_clone_CloneI16; +} + +let core_marker_CopyI32 : core_marker_Copy i32 = { + cloneCloneInst = core_clone_CloneI32; +} + +let core_marker_CopyI64 : core_marker_Copy i64 = { + cloneCloneInst = core_clone_CloneI64; +} + +let core_marker_CopyI128 : core_marker_Copy i128 = { + cloneCloneInst = core_clone_CloneI128; +} + +let core_marker_CopyIsize : core_marker_Copy isize = { + cloneCloneInst = core_clone_CloneIsize; +} + (** [core::option::{core::option::Option}::unwrap] *) let core_option_Option_unwrap (#t : Type0) (x : option t) : result t = match x with diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst index a22d449f..a7a007f1 100644 --- a/tests/fstar/hashmap/Primitives.fst +++ b/tests/fstar/hashmap/Primitives.fst @@ -556,6 +556,58 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +noeq type core_marker_Copy (self : Type0) = { + cloneCloneInst : core_clone_Clone self; +} + +let core_marker_CopyU8 : core_marker_Copy u8 = { + cloneCloneInst = core_clone_CloneU8; +} + +let core_marker_CopyU16 : core_marker_Copy u16 = { + cloneCloneInst = core_clone_CloneU16; +} + +let core_marker_CopyU32 : core_marker_Copy u32 = { + cloneCloneInst = core_clone_CloneU32; +} + +let core_marker_CopyU64 : core_marker_Copy u64 = { + cloneCloneInst = core_clone_CloneU64; +} + +let core_marker_CopyU128 : core_marker_Copy u128 = { + cloneCloneInst = core_clone_CloneU128; +} + +let core_marker_CopyUsize : core_marker_Copy usize = { + cloneCloneInst = core_clone_CloneUsize; +} + +let core_marker_CopyI8 : core_marker_Copy i8 = { + cloneCloneInst = core_clone_CloneI8; +} + +let core_marker_CopyI16 : core_marker_Copy i16 = { + cloneCloneInst = core_clone_CloneI16; +} + +let core_marker_CopyI32 : core_marker_Copy i32 = { + cloneCloneInst = core_clone_CloneI32; +} + +let core_marker_CopyI64 : core_marker_Copy i64 = { + cloneCloneInst = core_clone_CloneI64; +} + +let core_marker_CopyI128 : core_marker_Copy i128 = { + cloneCloneInst = core_clone_CloneI128; +} + +let core_marker_CopyIsize : core_marker_Copy isize = { + cloneCloneInst = core_clone_CloneIsize; +} + (** [core::option::{core::option::Option}::unwrap] *) let core_option_Option_unwrap (#t : Type0) (x : option t) : result t = match x with diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst index a22d449f..a7a007f1 100644 --- a/tests/fstar/misc/Primitives.fst +++ b/tests/fstar/misc/Primitives.fst @@ -556,6 +556,58 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +noeq type core_marker_Copy (self : Type0) = { + cloneCloneInst : core_clone_Clone self; +} + +let core_marker_CopyU8 : core_marker_Copy u8 = { + cloneCloneInst = core_clone_CloneU8; +} + +let core_marker_CopyU16 : core_marker_Copy u16 = { + cloneCloneInst = core_clone_CloneU16; +} + +let core_marker_CopyU32 : core_marker_Copy u32 = { + cloneCloneInst = core_clone_CloneU32; +} + +let core_marker_CopyU64 : core_marker_Copy u64 = { + cloneCloneInst = core_clone_CloneU64; +} + +let core_marker_CopyU128 : core_marker_Copy u128 = { + cloneCloneInst = core_clone_CloneU128; +} + +let core_marker_CopyUsize : core_marker_Copy usize = { + cloneCloneInst = core_clone_CloneUsize; +} + +let core_marker_CopyI8 : core_marker_Copy i8 = { + cloneCloneInst = core_clone_CloneI8; +} + +let core_marker_CopyI16 : core_marker_Copy i16 = { + cloneCloneInst = core_clone_CloneI16; +} + +let core_marker_CopyI32 : core_marker_Copy i32 = { + cloneCloneInst = core_clone_CloneI32; +} + +let core_marker_CopyI64 : core_marker_Copy i64 = { + cloneCloneInst = core_clone_CloneI64; +} + +let core_marker_CopyI128 : core_marker_Copy i128 = { + cloneCloneInst = core_clone_CloneI128; +} + +let core_marker_CopyIsize : core_marker_Copy isize = { + cloneCloneInst = core_clone_CloneIsize; +} + (** [core::option::{core::option::Option}::unwrap] *) let core_option_Option_unwrap (#t : Type0) (x : option t) : result t = match x with diff --git a/tests/fstar/rename_attribute/Primitives.fst b/tests/fstar/rename_attribute/Primitives.fst index a22d449f..a7a007f1 100644 --- a/tests/fstar/rename_attribute/Primitives.fst +++ b/tests/fstar/rename_attribute/Primitives.fst @@ -556,6 +556,58 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +noeq type core_marker_Copy (self : Type0) = { + cloneCloneInst : core_clone_Clone self; +} + +let core_marker_CopyU8 : core_marker_Copy u8 = { + cloneCloneInst = core_clone_CloneU8; +} + +let core_marker_CopyU16 : core_marker_Copy u16 = { + cloneCloneInst = core_clone_CloneU16; +} + +let core_marker_CopyU32 : core_marker_Copy u32 = { + cloneCloneInst = core_clone_CloneU32; +} + +let core_marker_CopyU64 : core_marker_Copy u64 = { + cloneCloneInst = core_clone_CloneU64; +} + +let core_marker_CopyU128 : core_marker_Copy u128 = { + cloneCloneInst = core_clone_CloneU128; +} + +let core_marker_CopyUsize : core_marker_Copy usize = { + cloneCloneInst = core_clone_CloneUsize; +} + +let core_marker_CopyI8 : core_marker_Copy i8 = { + cloneCloneInst = core_clone_CloneI8; +} + +let core_marker_CopyI16 : core_marker_Copy i16 = { + cloneCloneInst = core_clone_CloneI16; +} + +let core_marker_CopyI32 : core_marker_Copy i32 = { + cloneCloneInst = core_clone_CloneI32; +} + +let core_marker_CopyI64 : core_marker_Copy i64 = { + cloneCloneInst = core_clone_CloneI64; +} + +let core_marker_CopyI128 : core_marker_Copy i128 = { + cloneCloneInst = core_clone_CloneI128; +} + +let core_marker_CopyIsize : core_marker_Copy isize = { + cloneCloneInst = core_clone_CloneIsize; +} + (** [core::option::{core::option::Option}::unwrap] *) let core_option_Option_unwrap (#t : Type0) (x : option t) : result t = match x with diff --git a/tests/fstar/traits/Primitives.fst b/tests/fstar/traits/Primitives.fst index a22d449f..a7a007f1 100644 --- a/tests/fstar/traits/Primitives.fst +++ b/tests/fstar/traits/Primitives.fst @@ -556,6 +556,58 @@ let core_clone_CloneI128 : core_clone_Clone i128 = { clone = fun x -> Ok (core_clone_impls_CloneI128_clone x) } +noeq type core_marker_Copy (self : Type0) = { + cloneCloneInst : core_clone_Clone self; +} + +let core_marker_CopyU8 : core_marker_Copy u8 = { + cloneCloneInst = core_clone_CloneU8; +} + +let core_marker_CopyU16 : core_marker_Copy u16 = { + cloneCloneInst = core_clone_CloneU16; +} + +let core_marker_CopyU32 : core_marker_Copy u32 = { + cloneCloneInst = core_clone_CloneU32; +} + +let core_marker_CopyU64 : core_marker_Copy u64 = { + cloneCloneInst = core_clone_CloneU64; +} + +let core_marker_CopyU128 : core_marker_Copy u128 = { + cloneCloneInst = core_clone_CloneU128; +} + +let core_marker_CopyUsize : core_marker_Copy usize = { + cloneCloneInst = core_clone_CloneUsize; +} + +let core_marker_CopyI8 : core_marker_Copy i8 = { + cloneCloneInst = core_clone_CloneI8; +} + +let core_marker_CopyI16 : core_marker_Copy i16 = { + cloneCloneInst = core_clone_CloneI16; +} + +let core_marker_CopyI32 : core_marker_Copy i32 = { + cloneCloneInst = core_clone_CloneI32; +} + +let core_marker_CopyI64 : core_marker_Copy i64 = { + cloneCloneInst = core_clone_CloneI64; +} + +let core_marker_CopyI128 : core_marker_Copy i128 = { + cloneCloneInst = core_clone_CloneI128; +} + +let core_marker_CopyIsize : core_marker_Copy isize = { + cloneCloneInst = core_clone_CloneIsize; +} + (** [core::option::{core::option::Option}::unwrap] *) let core_option_Option_unwrap (#t : Type0) (x : option t) : result t = match x with