From 959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 09:37:31 +0100
Subject: Update the generation of files for external definitions and
 regenerate the tests

---
 tests/coq/misc/External_Funs.v                  |  4 +--
 tests/coq/misc/External_FunsExternal.v          | 43 ++++++++++++++++++++++++
 tests/coq/misc/External_FunsExternal_Template.v | 44 +++++++++++++++++++++++++
 tests/coq/misc/External_Opaque.v                | 43 ------------------------
 tests/coq/misc/_CoqProject                      |  3 +-
 5 files changed, 91 insertions(+), 46 deletions(-)
 create mode 100644 tests/coq/misc/External_FunsExternal.v
 create mode 100644 tests/coq/misc/External_FunsExternal_Template.v
 delete mode 100644 tests/coq/misc/External_Opaque.v

(limited to 'tests/coq/misc')

diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 0a14c7d1..8a3360bb 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -8,8 +8,8 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export External_Types.
 Import External_Types.
-Require Export External_Opaque.
-Import External_Opaque.
+Require Export External_FunsExternal.
+Import External_FunsExternal.
 Module External_Funs.
 
 (** [external::swap]: forward function
diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v
new file mode 100644
index 00000000..07d43061
--- /dev/null
+++ b/tests/coq/misc/External_FunsExternal.v
@@ -0,0 +1,43 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external function declarations *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Require Export External_Types.
+Import External_Types.
+Module External_FunsExternal.
+
+(** [core::mem::swap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+Axiom core_mem_swap :
+  forall(T : Type), T -> T -> state -> result (state * unit)
+.
+
+(** [core::mem::swap]: backward function 0
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+Axiom core_mem_swap_back0 :
+  forall(T : Type), T -> T -> state -> state -> result (state * T)
+.
+
+(** [core::mem::swap]: backward function 1
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+Axiom core_mem_swap_back1 :
+  forall(T : Type), T -> T -> state -> state -> result (state * T)
+.
+
+(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
+Axiom core_num_nonzero_NonZeroU32_new
+  : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
+.
+
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+Axiom core_option_Option_unwrap :
+  forall(T : Type), option T -> state -> result (state * T)
+.
+
+End External_FunsExternal.
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
new file mode 100644
index 00000000..0977c3ae
--- /dev/null
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -0,0 +1,44 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external functions.
+-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Require Export External_Types.
+Import External_Types.
+Module External_FunsExternal_Template.
+
+(** [core::mem::swap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+Axiom core_mem_swap :
+  forall(T : Type), T -> T -> state -> result (state * unit)
+.
+
+(** [core::mem::swap]: backward function 0
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+Axiom core_mem_swap_back0 :
+  forall(T : Type), T -> T -> state -> state -> result (state * T)
+.
+
+(** [core::mem::swap]: backward function 1
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+Axiom core_mem_swap_back1 :
+  forall(T : Type), T -> T -> state -> state -> result (state * T)
+.
+
+(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
+Axiom core_num_nonzero_NonZeroU32_new
+  : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
+.
+
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+Axiom core_option_Option_unwrap :
+  forall(T : Type), option T -> state -> result (state * T)
+.
+
+End External_FunsExternal_Template .
diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_Opaque.v
deleted file mode 100644
index b482431f..00000000
--- a/tests/coq/misc/External_Opaque.v
+++ /dev/null
@@ -1,43 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: external function declarations *)
-Require Import Primitives.
-Import Primitives.
-Require Import Coq.ZArith.ZArith.
-Require Import List.
-Import ListNotations.
-Local Open Scope Primitives_scope.
-Require Export External_Types.
-Import External_Types.
-Module External_Opaque.
-
-(** [core::mem::swap]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-Axiom core_mem_swap :
-  forall(T : Type), T -> T -> state -> result (state * unit)
-.
-
-(** [core::mem::swap]: backward function 0
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-Axiom core_mem_swap_back0 :
-  forall(T : Type), T -> T -> state -> state -> result (state * T)
-.
-
-(** [core::mem::swap]: backward function 1
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-Axiom core_mem_swap_back1 :
-  forall(T : Type), T -> T -> state -> state -> result (state * T)
-.
-
-(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
-Axiom core_num_nonzero_NonZeroU32_new
-  : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
-.
-
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
-Axiom core_option_Option_unwrap :
-  forall(T : Type), option T -> state -> result (state * T)
-.
-
-End External_Opaque .
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index db6c2742..6884d5d9 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -10,5 +10,6 @@ Constants.v
 PoloniusList.v
 External_Types.v
 NoNestedBorrows.v
-External_Opaque.v
+External_FunsExternal.v
+External_FunsExternal_Template.v
 Paper.v
-- 
cgit v1.2.3


From bef2bd34fcb0817f1b7d16b95122bcc3c6f05c72 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 10:29:25 +0100
Subject: Generate a dedicated file for the external types

---
 tests/coq/misc/Constants.v                       |  2 +-
 tests/coq/misc/External_Funs.v                   | 10 +++++-----
 tests/coq/misc/External_FunsExternal.v           |  2 +-
 tests/coq/misc/External_FunsExternal_Template.v  |  6 +++---
 tests/coq/misc/External_Types.v                  | 11 +++--------
 tests/coq/misc/External_TypesExternal.v          | 19 +++++++++++++++++++
 tests/coq/misc/External_TypesExternal_Template.v | 19 +++++++++++++++++++
 tests/coq/misc/Loops.v                           |  2 +-
 tests/coq/misc/NoNestedBorrows.v                 |  2 +-
 tests/coq/misc/Paper.v                           |  2 +-
 tests/coq/misc/PoloniusList.v                    |  2 +-
 tests/coq/misc/_CoqProject                       |  6 ++++--
 12 files changed, 59 insertions(+), 24 deletions(-)
 create mode 100644 tests/coq/misc/External_TypesExternal.v
 create mode 100644 tests/coq/misc/External_TypesExternal_Template.v

(limited to 'tests/coq/misc')

diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 20edb2b1..ad899f25 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -157,4 +157,4 @@ Definition s3_c : Pair_t u32 u32 := s3_body%global.
 Definition s4_body : result (Pair_t u32 u32) := mk_pair1 7%u32 8%u32.
 Definition s4_c : Pair_t u32 u32 := s4_body%global.
 
-End Constants .
+End Constants.
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 8a3360bb..e9d39f66 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -6,10 +6,10 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export External_Types.
-Import External_Types.
-Require Export External_FunsExternal.
-Import External_FunsExternal.
+Require Import External_Types.
+Include External_Types.
+Require Import External_FunsExternal.
+Include External_FunsExternal.
 Module External_Funs.
 
 (** [external::swap]: forward function
@@ -115,4 +115,4 @@ Definition test_swap_non_zero (x : u32) (st : state) : result (state * u32) :=
   if x0 s= 0%u32 then Fail_ Failure else Return (st1, x0)
 .
 
-End External_Funs .
+End External_Funs.
diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v
index 07d43061..a8c5756a 100644
--- a/tests/coq/misc/External_FunsExternal.v
+++ b/tests/coq/misc/External_FunsExternal.v
@@ -7,7 +7,7 @@ Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
 Require Export External_Types.
-Import External_Types.
+Include External_Types.
 Module External_FunsExternal.
 
 (** [core::mem::swap]: forward function
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index 0977c3ae..31e69c39 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -7,8 +7,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
-Require Export External_Types.
-Import External_Types.
+Require Import External_Types.
+Include External_Types.
 Module External_FunsExternal_Template.
 
 (** [core::mem::swap]: forward function
@@ -41,4 +41,4 @@ Axiom core_option_Option_unwrap :
   forall(T : Type), option T -> state -> result (state * T)
 .
 
-End External_FunsExternal_Template .
+End External_FunsExternal_Template.
diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v
index c638670c..b42c2ecf 100644
--- a/tests/coq/misc/External_Types.v
+++ b/tests/coq/misc/External_Types.v
@@ -6,13 +6,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import List.
 Import ListNotations.
 Local Open Scope Primitives_scope.
+Require Import External_TypesExternal.
+Include External_TypesExternal.
 Module External_Types.
 
-(** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
-Axiom core_num_nonzero_NonZeroU32_t : Type.
-
-(** The state type used in the state-error monad *)
-Axiom state : Type.
-
-End External_Types .
+End External_Types.
diff --git a/tests/coq/misc/External_TypesExternal.v b/tests/coq/misc/External_TypesExternal.v
new file mode 100644
index 00000000..3f02b839
--- /dev/null
+++ b/tests/coq/misc/External_TypesExternal.v
@@ -0,0 +1,19 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module External_TypesExternal.
+
+(** [core::num::nonzero::NonZeroU32]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+Axiom core_num_nonzero_NonZeroU32_t : Type.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End External_TypesExternal.
diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v
new file mode 100644
index 00000000..7ba79d8e
--- /dev/null
+++ b/tests/coq/misc/External_TypesExternal_Template.v
@@ -0,0 +1,19 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module External_TypesExternal_Template.
+
+(** [core::num::nonzero::NonZeroU32]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+Axiom core_num_nonzero_NonZeroU32_t : Type.
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End External_TypesExternal_Template.
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 4929ddd0..83c249c1 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -914,4 +914,4 @@ Definition list_nth_shared_mut_loop_pair_merge_back
   list_nth_shared_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret
 .
 
-End Loops .
+End Loops.
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index b044d24f..16a2e816 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -586,4 +586,4 @@ Definition test_shared_borrow_enum1 (l : List_t u32) : result u32 :=
 Definition test_shared_borrow_enum2 : result u32 :=
   Return 0%u32.
 
-End NoNestedBorrows .
+End NoNestedBorrows.
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index 4a49096f..6b110193 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -128,4 +128,4 @@ Definition call_choose (p : (u32 * u32)) : result u32 :=
   Return px0
 .
 
-End Paper .
+End Paper.
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index a0820e40..2371b1cc 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -41,4 +41,4 @@ Fixpoint get_list_at_x_back
   end
 .
 
-End PoloniusList .
+End PoloniusList.
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index 6884d5d9..0828bced 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -4,12 +4,14 @@
 -arg all
 
 Loops.v
+External_Types.v
 Primitives.v
 External_Funs.v
+Paper.v
+External_TypesExternal.v
 Constants.v
 PoloniusList.v
-External_Types.v
 NoNestedBorrows.v
 External_FunsExternal.v
+External_TypesExternal_Template.v
 External_FunsExternal_Template.v
-Paper.v
-- 
cgit v1.2.3