diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v index 7ce37c4c4..cc36ab258 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,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/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index a22d449f0..a7a007f12 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 (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/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean index cce8c2e76..405734a0c 100644 --- a/backends/lean/Base/Primitives/ArraySlice.lean +++ b/backends/lean/Base/Primitives/ArraySlice.lean @@ -577,4 +577,12 @@ 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 + +/- [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 84f1d6d9f..f792e8126 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,69 @@ 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) +} + +/- [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/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean index ad54c5c3f..e5e08a5a7 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 6ae14027d..c4ebf15de 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/charon-pin b/charon-pin index 0afbf6477..c1830e843 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 +7744bf94275e2ba3e7a2e4163c1fa062225d7a75 diff --git a/flake.lock b/flake.lock index 19869f91c..3c32186bb 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1733151343, - "narHash": "sha256-LPr2ZWbC3q6GjnCKN3Hsy1xJHR+qmzMZRgrtd55D4AA=", + "lastModified": 1733313551, + "narHash": "sha256-CSaj6Cadz+S/qmiLtoQMWfm3mHSE2cCx3UUxt5JmoAM=", "owner": "aeneasverif", "repo": "charon", - "rev": "e6033230aab5cbff5e3840473844e913b59062af", + "rev": "7744bf94275e2ba3e7a2e4163c1fa062225d7a75", "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": { diff --git a/src/Config.ml b/src/Config.ml index d9fed4083..7d315ca4e 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 e66876c07..36d066d3f 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 a669e748e..fa624b7b4 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 @@ -127,8 +158,12 @@ 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)." ); + ( "-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 688cbe342..25b8b4fc2 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/Extract.ml b/src/extract/Extract.ml index 12f43f4c4..2dfba3bd3 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/ExtractBase.ml b/src/extract/ExtractBase.ml index ca1455775..6729d5c2e 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 7572a81e6..0837bfb59 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,24 @@ 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 -> + 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; + fields = None; + }) + variants + in + Some (Enum variants) in { rust_name; extract_name; keep_params; body_info } in @@ -237,6 +253,13 @@ let builtin_types () : builtin_type_info list = ]); }; ] + @ mk_lean_only + [ + mk_type "core::fmt::Formatter" (); + mk_type "core::result::Result" ~kind:(KEnum [ "Ok"; "Err" ]) (); + mk_type "core::fmt::Error" (); + mk_type "core::array::TryFromSliceError" (); + ] let mk_builtin_types_map () = NameMatcherMap.of_list @@ -490,6 +513,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 +547,23 @@ 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" (); + mk_fun "core::result::{core::result::Result<@T, @E>}::unwrap" (); ] @ List.map (fun ty -> @@ -676,7 +721,19 @@ 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" ] + (); + (* 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 () = NameMatcherMap.of_list @@ -758,6 +815,18 @@ 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") (); + (* TryInto> *) + fmt "core::convert::{core::convert::TryInto<@T, @U>}" + ~extract_name:(Some "core::convert::TryIntoFrom") (); + ] (* From *) @ List.map (fun ty -> @@ -791,6 +860,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/extract/ExtractTypes.ml b/src/extract/ExtractTypes.ml index b853f97d4..6fdda8684 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) -> diff --git a/src/interp/InterpreterStatements.ml b/src/interp/InterpreterStatements.ml index 5ac18af57..6e4354c58 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 56178ad1b..19e9c9f2d 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; } diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml index 6a36d1bb9..574a2ed64 100644 --- a/src/symbolic/SymbolicToPure.ml +++ b/src/symbolic/SymbolicToPure.ml @@ -1181,9 +1181,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/coq/arrays/Primitives.v b/tests/coq/arrays/Primitives.v index 7ce37c4c4..cc36ab258 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 7ce37c4c4..cc36ab258 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 7ce37c4c4..cc36ab258 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 7ce37c4c4..cc36ab258 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_Funs.v b/tests/coq/misc/External_Funs.v index a3275de82..3594e22e2 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.v b/tests/coq/misc/External_FunsExternal.v index e47741d19..af3d589ed 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/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v index 4de5c5c34..c3002326a 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 7601795ac..b42c2ecfe 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/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v index 7ce37c4c4..cc36ab258 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 7ce37c4c4..cc36ab258 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 7ce37c4c4..cc36ab258 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 a22d449f0..a7a007f12 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 a22d449f0..a7a007f12 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 a22d449f0..a7a007f12 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 a22d449f0..a7a007f12 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/External.Funs.fst b/tests/fstar/misc/External.Funs.fst index cba918b91..3208d825e 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 4f1213966..9fca284e1 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 cb4fa57bf..4fbcec476 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/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst index a22d449f0..a7a007f12 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 a22d449f0..a7a007f12 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 a22d449f0..a7a007f12 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 diff --git a/tests/lean/Builtin.lean b/tests/lean/Builtin.lean new file mode 100644 index 000000000..650573443 --- /dev/null +++ b/tests/lean/Builtin.lean @@ -0,0 +1,61 @@ +-- 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 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 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 14:0-16: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 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 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 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 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 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/lean/External/Funs.lean b/tests/lean/External/Funs.lean index 5e2975eca..6df57acf7 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 5e64121ed..789ce2b82 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 77374ce78..93b17b90c 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/builtin.rs b/tests/src/builtin.rs new file mode 100644 index 000000000..6190ae934 --- /dev/null +++ b/tests/src/builtin.rs @@ -0,0 +1,38 @@ +//@ 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. + +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() +} + +fn use_debug_clause(_: T) {} diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index 700af9ce2..a45c2bb0b 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 diff --git a/tests/src/paper.rs b/tests/src/paper.rs index d9fb1032c..fd59295ca 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) {