diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/2141.v | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3287.v | 9 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3923.v | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4616.v | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4710.v | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4720.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5177.v | 1 | ||||
| -rw-r--r-- | test-suite/success/extraction.v | 117 | ||||
| -rw-r--r-- | test-suite/success/extraction_dep.v | 5 | ||||
| -rw-r--r-- | test-suite/success/extraction_impl.v | 9 | ||||
| -rw-r--r-- | test-suite/success/primitiveproj.v | 1 |
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)*) |