Adding the example referenced in issue ocaml#3437.

Mbodin · Apr 30, 2020 · 1d5ca26 · 1d5ca26
1 parent 4348e72
commit 1d5ca26
Show file tree

Hide file tree

Showing 10 changed files with 120 additions and 0 deletions.
diff --git a/test/blackbox-tests/test-cases/coq-extraction/Bug_Coq.opam b/test/blackbox-tests/test-cases/coq-extraction/Bug_Coq.opam
@@ -0,0 +1,20 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Coq files"
+depends: [
+  "dune" {>= "2.5"}
+]
+build: [
+  ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
diff --git a/test/blackbox-tests/test-cases/coq-extraction/Bug_OCaml.opam b/test/blackbox-tests/test-cases/coq-extraction/Bug_OCaml.opam
@@ -0,0 +1,20 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "OCaml files"
+depends: [
+  "dune" {>= "2.5"}
+]
+build: [
+  ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
diff --git a/test/blackbox-tests/test-cases/coq-extraction/_CoqProject b/test/blackbox-tests/test-cases/coq-extraction/_CoqProject
@@ -0,0 +1,5 @@
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -abstract-large-number
+
+-R _build/default/theories Bug_Coq
diff --git a/test/blackbox-tests/test-cases/coq-extraction/dune-project b/test/blackbox-tests/test-cases/coq-extraction/dune-project
@@ -0,0 +1,14 @@
+(lang dune 2.5)
+(using coq 0.2)
+(name Bug_Coq)
+
+(generate_opam_files true)
+
+(package
+  (name Bug_Coq)
+  (synopsis "Coq files"))
+
+(package
+  (name Bug_OCaml)
+  (synopsis "OCaml files"))
+
diff --git a/test/blackbox-tests/test-cases/coq-extraction/src/Bug_OCaml.ml b/test/blackbox-tests/test-cases/coq-extraction/src/Bug_OCaml.ml
@@ -0,0 +1,5 @@
+
+let _ =
+  ignore Extract.v ;
+  print_endline "OK"
+
diff --git a/test/blackbox-tests/test-cases/coq-extraction/src/dune b/test/blackbox-tests/test-cases/coq-extraction/src/dune
@@ -0,0 +1,14 @@
+(executable
+  (name Bug_OCaml)
+  (modes (best exe)))
+
+; (install
+;  (package Bug_OCaml)
+;  (section bin)
+;  (files (bug.exe as bug)))
+
+(coq.extraction
+	(theories Bug_Coq)
+	(prelude extraction)
+	(extracted_modules Extract))
+
diff --git a/test/blackbox-tests/test-cases/coq-extraction/src/extraction.v b/test/blackbox-tests/test-cases/coq-extraction/src/extraction.v
@@ -0,0 +1,8 @@
+
+Require Import Extraction.
+From Bug_Coq Require Import value common.
+
+Extraction Language OCaml.
+
+Extraction "Extract" v.
+
diff --git a/test/blackbox-tests/test-cases/coq-extraction/theories/common.v b/test/blackbox-tests/test-cases/coq-extraction/theories/common.v
@@ -0,0 +1,15 @@
+
+Require Import Ascii.
+
+Axiom axiom : Prop.
+Axiom axiom_valid : axiom.
+
+Lemma test : forall a b, eqb a b = eqb b a.
+Proof.
+  intros. destruct (eqb a b) eqn: E.
+  - rewrite eqb_eq in E. symmetry. now rewrite eqb_eq.
+  - rewrite eqb_neq in E. symmetry. rewrite eqb_neq. now auto.
+Qed.
+
+Definition v2 := 18.
+
diff --git a/test/blackbox-tests/test-cases/coq-extraction/theories/dune b/test/blackbox-tests/test-cases/coq-extraction/theories/dune
@@ -0,0 +1,4 @@
+(coq.theory
+  (name Bug_Coq)
+	(package Bug_Coq))
+
diff --git a/test/blackbox-tests/test-cases/coq-extraction/theories/value.v b/test/blackbox-tests/test-cases/coq-extraction/theories/value.v
@@ -0,0 +1,15 @@
+
+Set Implicit Arguments.
+Require Export common.
+
+Definition k (A B : Type) (_ : A) (b : B) := b.
+
+Definition v3 := k axiom_valid v2.
+
+Definition v : nat.
+Proof.
+  eapply k.
+  - exact test.
+  - exact v3.
+Defined.
+