aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-01 13:02:56 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-01 13:02:56 +0200
commitce34a286bd38eeac7526d175ac0da6112266d93a (patch)
treec98f36253e70f972d7de51654fc8cbfea3da9214 /test-suite
parent783a1d0e94d124d97e2aa5faafb5440195a7c626 (diff)
parent036acae205ff0477dbae3a97b44853dc27d03b93 (diff)
Merge PR #926: test-suite uses Extraction TestCompile
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/2141.v1
-rw-r--r--test-suite/bugs/closed/3287.v9
-rw-r--r--test-suite/bugs/closed/3923.v1
-rw-r--r--test-suite/bugs/closed/4616.v3
-rw-r--r--test-suite/bugs/closed/4710.v3
-rw-r--r--test-suite/bugs/closed/4720.v4
-rw-r--r--test-suite/bugs/closed/5177.v1
-rw-r--r--test-suite/success/extraction.v117
-rw-r--r--test-suite/success/extraction_dep.v5
-rw-r--r--test-suite/success/extraction_impl.v9
-rw-r--r--test-suite/success/primitiveproj.v1
11 files changed, 110 insertions, 44 deletions
diff --git a/test-suite/bugs/closed/2141.v b/test-suite/bugs/closed/2141.v
index 098a7e9e7..c556ff0b2 100644
--- a/test-suite/bugs/closed/2141.v
+++ b/test-suite/bugs/closed/2141.v
@@ -11,5 +11,6 @@ End FSetHide.
Module NatSet' := FSetHide NatSet.
Recursive Extraction NatSet'.fold.
+Extraction TestCompile NatSet'.fold.
(* Extraction "test2141.ml" NatSet'.fold. *) \ No newline at end of file
diff --git a/test-suite/bugs/closed/3287.v b/test-suite/bugs/closed/3287.v
index 1b758acd7..4b3e7ff05 100644
--- a/test-suite/bugs/closed/3287.v
+++ b/test-suite/bugs/closed/3287.v
@@ -6,6 +6,7 @@ Definition bar := true.
End Foo.
Recursive Extraction Foo.bar.
+Extraction TestCompile Foo.bar.
Module Foo'.
Definition foo := (I,I).
@@ -13,10 +14,6 @@ Definition bar := true.
End Foo'.
Recursive Extraction Foo'.bar.
+Extraction TestCompile Foo'.bar.
-Module Foo''.
-Definition foo := (I,I).
-Definition bar := true.
-End Foo''.
-
-Extraction Foo.bar.
+Extraction Foo'.bar.
diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v
index 2fb0a5439..1d9488c6e 100644
--- a/test-suite/bugs/closed/3923.v
+++ b/test-suite/bugs/closed/3923.v
@@ -33,3 +33,4 @@ Axiom empty_fieldstore : cert_fieldstore.
End MkCertRuntimeTypes.
Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *)
+Extraction TestCompile MkCertRuntimeTypes.
diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v
index a59975dbc..d6660e355 100644
--- a/test-suite/bugs/closed/4616.v
+++ b/test-suite/bugs/closed/4616.v
@@ -2,5 +2,6 @@ Require Coq.extraction.Extraction.
Set Primitive Projections.
Record Foo' := Foo { foo : Type }.
-Axiom f : forall t : Foo', foo t.
+Definition f := forall t : Foo', foo t.
Extraction f.
+Extraction TestCompile f.
diff --git a/test-suite/bugs/closed/4710.v b/test-suite/bugs/closed/4710.v
index 5d8ca330a..e792a3623 100644
--- a/test-suite/bugs/closed/4710.v
+++ b/test-suite/bugs/closed/4710.v
@@ -4,7 +4,6 @@ Set Primitive Projections.
Record Foo' := Foo { foo : nat }.
Extraction foo.
Record Foo2 (a : nat) := Foo2c { foo2p : nat; foo2b : bool }.
-Extraction Language Ocaml.
Extraction foo2p.
Definition bla (x : Foo2 0) := foo2p _ x.
@@ -12,3 +11,5 @@ Extraction bla.
Definition bla' (a : nat) (x : Foo2 a) := foo2b _ x.
Extraction bla'.
+
+Extraction TestCompile foo foo2p bla bla'.
diff --git a/test-suite/bugs/closed/4720.v b/test-suite/bugs/closed/4720.v
index 9265b60c1..704331e78 100644
--- a/test-suite/bugs/closed/4720.v
+++ b/test-suite/bugs/closed/4720.v
@@ -44,3 +44,7 @@ Recursive Extraction WithMod.
Recursive Extraction WithDef.
Recursive Extraction WithModPriv.
+
+(* Let's even check that all this extracted code is actually compilable: *)
+
+Extraction TestCompile WithMod WithDef WithModPriv.
diff --git a/test-suite/bugs/closed/5177.v b/test-suite/bugs/closed/5177.v
index 231d103a5..7c8af1e46 100644
--- a/test-suite/bugs/closed/5177.v
+++ b/test-suite/bugs/closed/5177.v
@@ -19,3 +19,4 @@ End MakeA.
Require Extraction.
Recursive Extraction MakeA.
+Extraction TestCompile MakeA.
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 4a509da89..0ee223250 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -545,47 +545,96 @@ Recursive Extraction test_proj.
(*** TO SUM UP: ***)
-(* Was previously producing a "test_extraction.ml" *)
-Recursive Extraction
- idnat id id' test2 test3 test4 test5 test6 test7 d d2
- d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
- test13 test19 test20 nat sumbool_rect c Finite tree
- tree_size test14 test15 eta_c test16 test17 test18 bidon
- tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
- tp1bis Truc oups test24 loop horibilis PropSet natbool
- zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
- f_arity f_normal Boite boite1 boite2 test_boite Box box1
- zarb test_proj.
+Module Everything.
+ Definition idnat := idnat.
+ Definition id := id.
+ Definition id' := id'.
+ Definition test2 := test2.
+ Definition test3 := test3.
+ Definition test4 := test4.
+ Definition test5 := test5.
+ Definition test6 := test6.
+ Definition test7 := test7.
+ Definition d := d.
+ Definition d2 := d2.
+ Definition d3 := d3.
+ Definition d4 := d4.
+ Definition d5 := d5.
+ Definition d6 := d6.
+ Definition test8 := test8.
+ Definition test9 := test9.
+ Definition test10 := test10.
+ Definition test11 := test11.
+ Definition test12 := test12.
+ Definition test13 := test13.
+ Definition test19 := test19.
+ Definition test20 := test20.
+ Definition nat := nat.
+ Definition sumbool_rect := sumbool_rect.
+ Definition c := c.
+ Definition Finite := Finite.
+ Definition tree := tree.
+ Definition tree_size := tree_size.
+ Definition test14 := test14.
+ Definition test15 := test15.
+ Definition eta_c := eta_c.
+ Definition test16 := test16.
+ Definition test17 := test17.
+ Definition test18 := test18.
+ Definition bidon := bidon.
+ Definition tb := tb.
+ Definition fbidon := fbidon.
+ Definition fbidon2 := fbidon2.
+ Definition test_0 := test_0.
+ Definition test_1 := test_1.
+ Definition eq_rect := eq_rect.
+ Definition tp1 := tp1.
+ Definition tp1bis := tp1bis.
+ Definition Truc := Truc.
+ Definition oups := oups.
+ Definition test24 := test24.
+ Definition loop := loop.
+ Definition horibilis := horibilis.
+ Definition PropSet := PropSet.
+ Definition natbool := natbool.
+ Definition zerotrue := zerotrue.
+ Definition zeroTrue := zeroTrue.
+ Definition zeroprop := zeroprop.
+ Definition test21 := test21.
+ Definition test22 := test22.
+ Definition test23 := test23.
+ Definition f := f.
+ Definition f_prop := f_prop.
+ Definition f_arity := f_arity.
+ Definition f_normal := f_normal.
+ Definition Boite := Boite.
+ Definition boite1 := boite1.
+ Definition boite2 := boite2.
+ Definition test_boite := test_boite.
+ Definition Box := Box.
+ Definition box1 := box1.
+ Definition zarb := zarb.
+ Definition test_proj := test_proj.
+End Everything.
+
+(* Extraction "test_extraction.ml" Everything. *)
+Recursive Extraction Everything.
+(* Check that the previous OCaml code is compilable *)
+Extraction TestCompile Everything.
Extraction Language Haskell.
-(* Was previously producing a "Test_extraction.hs" *)
-Recursive Extraction
- idnat id id' test2 test3 test4 test5 test6 test7 d d2
- d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
- test13 test19 test20 nat sumbool_rect c Finite tree
- tree_size test14 test15 eta_c test16 test17 test18 bidon
- tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
- tp1bis Truc oups test24 loop horibilis PropSet natbool
- zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
- f_arity f_normal Boite boite1 boite2 test_boite Box box1
- zarb test_proj.
+(* Extraction "Test_extraction.hs" Everything. *)
+Recursive Extraction Everything.
Extraction Language Scheme.
-(* Was previously producing a "test_extraction.scm" *)
-Recursive Extraction
- idnat id id' test2 test3 test4 test5 test6 test7 d d2
- d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
- test13 test19 test20 nat sumbool_rect c Finite tree
- tree_size test14 test15 eta_c test16 test17 test18 bidon
- tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
- tp1bis Truc oups test24 loop horibilis PropSet natbool
- zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
- f_arity f_normal Boite boite1 boite2 test_boite Box box1
- zarb test_proj.
+(* Extraction "test_extraction.scm" Everything. *)
+Recursive Extraction Everything.
(*** Finally, a test more focused on everyday's life situations ***)
Require Import ZArith.
-Recursive Extraction two_or_two_plus_one Zdiv_eucl_exist.
+Extraction Language Ocaml.
+Recursive Extraction Z_modulo_2 Zdiv_eucl_exist.
+Extraction TestCompile Z_modulo_2 Zdiv_eucl_exist.
diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v
index e770cf779..fb0adabae 100644
--- a/test-suite/success/extraction_dep.v
+++ b/test-suite/success/extraction_dep.v
@@ -4,7 +4,7 @@
Require Coq.extraction.Extraction.
(** NB: we should someday check the produced code instead of
- simply running the commands. *)
+ extracting and just compiling. *)
(** 1) Without signature ... *)
@@ -20,6 +20,7 @@ End A.
Definition testA := A.u + A.B.x.
Recursive Extraction testA. (* without: v w *)
+Extraction TestCompile testA.
(** 1b) Same with an Include *)
@@ -31,6 +32,7 @@ End Abis.
Definition testAbis := Abis.u + Abis.y.
Recursive Extraction testAbis. (* without: A B v w x *)
+Extraction TestCompile testAbis.
(** 2) With signature, we only keep elements mentionned in signature. *)
@@ -46,3 +48,4 @@ End Ater.
Definition testAter := Ater.u.
Recursive Extraction testAter. (* with only: u v *)
+Extraction TestCompile testAter.
diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v
index 5bf807b1c..a38a688fb 100644
--- a/test-suite/success/extraction_impl.v
+++ b/test-suite/success/extraction_impl.v
@@ -2,7 +2,7 @@
(** Examples of extraction with manually-declared implicit arguments *)
(** NB: we should someday check the produced code instead of
- simply running the commands. *)
+ extracting and just compiling. *)
Require Coq.extraction.Extraction.
@@ -22,9 +22,11 @@ Proof.
Defined.
Recursive Extraction dnat_nat.
+Extraction TestCompile dnat_nat.
Extraction Implicit dnat_nat [n].
Recursive Extraction dnat_nat.
+Extraction TestCompile dnat_nat.
(** Same, with a Fixpoint *)
@@ -35,9 +37,11 @@ Fixpoint dnat_nat' n (d:dnat n) :=
end.
Recursive Extraction dnat_nat'.
+Extraction TestCompile dnat_nat'.
Extraction Implicit dnat_nat' [n].
Recursive Extraction dnat_nat'.
+Extraction TestCompile dnat_nat'.
(** Bug #4243, part 2 *)
@@ -56,6 +60,7 @@ Defined.
Extraction Implicit es [n].
Extraction Implicit enat_nat [n].
Recursive Extraction enat_nat.
+Extraction TestCompile enat_nat.
(** Same, with a Fixpoint *)
@@ -67,6 +72,7 @@ Fixpoint enat_nat' n (e:enat n) : nat :=
Extraction Implicit enat_nat' [n].
Recursive Extraction enat_nat'.
+Extraction TestCompile enat_nat'.
(** Bug #4228 *)
@@ -82,3 +88,4 @@ Extraction Implicit two_course [n].
End Food.
Recursive Extraction Food.Meal.
+Extraction TestCompile Food.Meal.
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 789854b2d..576bdbf71 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -184,6 +184,7 @@ Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x.
Require Coq.extraction.Extraction.
Recursive Extraction term term'.
+Extraction TestCompile term term'.
(*Unset Printing Primitive Projection Parameters.*)
(* Primitive projections in the presence of let-ins (was not failing in beta3)*)