Extraction: discard code unnecessary to fulfill a module signature

1 files changed, 46 insertions, 0 deletions

diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v
new file mode 100644
index 0000000000..11bb25fda0
--- /dev/null
+++ b/test-suite/success/extraction_dep.v
@@ -0,0 +1,46 @@
+
+(** Examples of code elimination inside modules during extraction *)
+
+(** NB: we should someday check the produced code instead of
+    simply running the commands. *)
+
+(** 1) Without signature ... *)
+
+Module A.
+ Definition u := 0.
+ Definition v := 1.
+ Module B.
+  Definition w := 2.
+  Definition x := 3.
+ End B.
+End A.
+
+Definition testA := A.u + A.B.x.
+
+Recursive Extraction testA. (* without: v w *)
+
+(** 1b) Same with an Include *)
+
+Module Abis.
+ Include A.
+ Definition y := 4.
+End Abis.
+
+Definition testAbis := Abis.u + Abis.y.
+
+Recursive Extraction testAbis. (* without: A B v w x *)
+
+(** 2) With signature, we only keep elements mentionned in signature. *)
+
+Module Type SIG.
+ Parameter u : nat.
+ Parameter v : nat.
+End SIG.
+
+Module Ater : SIG.
+ Include A.
+End Ater.
+
+Definition testAter := Ater.u.
+
+Recursive Extraction testAter. (* with only: u v *)