Regenerate the tests

AeneasVerif · Dec 4, 2024 · e70f981 · e70f981
1 parent 14194d8
commit e70f981
Show file tree

Hide file tree

Showing 10 changed files with 3 additions and 55 deletions.
diff --git 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<u32> *)
-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
@@ -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
@@ -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
@@ -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<u32> *)
-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
@@ -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<T>}#11::get_mut]:

diff --git 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
@@ -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<u32> -/
-@[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
@@ -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
@@ -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<T, U>}#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
@@ -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