diff options
| -rw-r--r-- | contrib/extraction/test/.depend | 94 | ||||
| -rw-r--r-- | contrib/extraction/test_extraction.v | 169 |
2 files changed, 132 insertions, 131 deletions
diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend index edb933104..1580ebf92 100644 --- a/contrib/extraction/test/.depend +++ b/contrib/extraction/test/.depend @@ -1,3 +1,7 @@ +theories/Arith/bool_nat.cmo: theories/Arith/compare_dec.cmo \ + theories/Arith/peano_dec.cmo theories/Bool/sumbool.cmo +theories/Arith/bool_nat.cmx: theories/Arith/compare_dec.cmx \ + theories/Arith/peano_dec.cmx theories/Bool/sumbool.cmx theories/Arith/compare_dec.cmo: theories/Init/datatypes.cmo \ theories/Init/specif.cmo theories/Arith/compare_dec.cmx: theories/Init/datatypes.cmx \ @@ -158,68 +162,6 @@ theories/Lists/theoryList.cmo: theories/Init/datatypes.cmo \ theories/Lists/polyList.cmo theories/Init/specif.cmo theories/Lists/theoryList.cmx: theories/Init/datatypes.cmx \ theories/Lists/polyList.cmx theories/Init/specif.cmx -theories/Reals/addReals.cmo: theories/ZArith/fast_integer.cmo \ - theories/Reals/typeSyntax.cmo -theories/Reals/addReals.cmx: theories/ZArith/fast_integer.cmx \ - theories/Reals/typeSyntax.cmx -theories/Reals/ranalysis.cmo: theories/Reals/rdefinitions.cmo -theories/Reals/ranalysis.cmx: theories/Reals/rdefinitions.cmx -theories/Reals/raxioms.cmo: theories/Init/datatypes.cmo \ - theories/ZArith/fast_integer.cmo theories/Reals/rdefinitions.cmo -theories/Reals/raxioms.cmx: theories/Init/datatypes.cmx \ - theories/ZArith/fast_integer.cmx theories/Reals/rdefinitions.cmx -theories/Reals/rbase.cmo: theories/Reals/addReals.cmo \ - theories/Init/datatypes.cmo theories/Reals/raxioms.cmo \ - theories/Reals/rdefinitions.cmo theories/Reals/typeSyntax.cmo \ - theories/ZArith/zarith_aux.cmo -theories/Reals/rbase.cmx: theories/Reals/addReals.cmx \ - theories/Init/datatypes.cmx theories/Reals/raxioms.cmx \ - theories/Reals/rdefinitions.cmx theories/Reals/typeSyntax.cmx \ - theories/ZArith/zarith_aux.cmx -theories/Reals/rbasic_fun.cmo: theories/Reals/rbase.cmo \ - theories/Reals/rdefinitions.cmo theories/Reals/typeSyntax.cmo -theories/Reals/rbasic_fun.cmx: theories/Reals/rbase.cmx \ - theories/Reals/rdefinitions.cmx theories/Reals/typeSyntax.cmx -theories/Reals/rfunctions.cmo: theories/Init/datatypes.cmo \ - theories/ZArith/fast_integer.cmo theories/Arith/minus.cmo \ - theories/Init/peano.cmo theories/Reals/rdefinitions.cmo -theories/Reals/rfunctions.cmx: theories/Init/datatypes.cmx \ - theories/ZArith/fast_integer.cmx theories/Arith/minus.cmx \ - theories/Init/peano.cmx theories/Reals/rdefinitions.cmx -theories/Reals/rgeom.cmo: theories/Reals/r_sqr.cmo theories/Reals/rbase.cmo \ - theories/Reals/rdefinitions.cmo theories/Reals/rtrigo.cmo -theories/Reals/rgeom.cmx: theories/Reals/r_sqr.cmx theories/Reals/rbase.cmx \ - theories/Reals/rdefinitions.cmx theories/Reals/rtrigo.cmx -theories/Reals/r_Ifp.cmo: theories/Reals/addReals.cmo \ - theories/ZArith/fast_integer.cmo theories/Reals/raxioms.cmo \ - theories/Reals/rdefinitions.cmo theories/ZArith/zarith_aux.cmo -theories/Reals/r_Ifp.cmx: theories/Reals/addReals.cmx \ - theories/ZArith/fast_integer.cmx theories/Reals/raxioms.cmx \ - theories/Reals/rdefinitions.cmx theories/ZArith/zarith_aux.cmx -theories/Reals/rlimit.cmo: theories/Reals/rbasic_fun.cmo \ - theories/Reals/rdefinitions.cmo -theories/Reals/rlimit.cmx: theories/Reals/rbasic_fun.cmx \ - theories/Reals/rdefinitions.cmx -theories/Reals/rseries.cmo: theories/Init/datatypes.cmo \ - theories/Reals/rbasic_fun.cmo -theories/Reals/rseries.cmx: theories/Init/datatypes.cmx \ - theories/Reals/rbasic_fun.cmx -theories/Reals/rsigma.cmo: theories/Init/datatypes.cmo \ - theories/Reals/rdefinitions.cmo -theories/Reals/rsigma.cmx: theories/Init/datatypes.cmx \ - theories/Reals/rdefinitions.cmx -theories/Reals/r_sqr.cmo: theories/Reals/rbase.cmo \ - theories/Reals/rdefinitions.cmo -theories/Reals/r_sqr.cmx: theories/Reals/rbase.cmx \ - theories/Reals/rdefinitions.cmx -theories/Reals/rtrigo.cmo: theories/Init/datatypes.cmo \ - theories/Init/peano.cmo theories/Reals/raxioms.cmo \ - theories/Reals/rdefinitions.cmo theories/Reals/rfunctions.cmo \ - theories/Reals/rsigma.cmo -theories/Reals/rtrigo.cmx: theories/Init/datatypes.cmx \ - theories/Init/peano.cmx theories/Reals/raxioms.cmx \ - theories/Reals/rdefinitions.cmx theories/Reals/rfunctions.cmx \ - theories/Reals/rsigma.cmx theories/Relations/relation_Operators.cmo: theories/Lists/polyList.cmo \ theories/Init/specif.cmo theories/Relations/relation_Operators.cmx: theories/Lists/polyList.cmx \ @@ -232,6 +174,10 @@ theories/Sets/multiset.cmo: theories/Init/datatypes.cmo \ theories/Init/peano.cmo theories/Init/specif.cmo theories/Sets/multiset.cmx: theories/Init/datatypes.cmx \ theories/Init/peano.cmx theories/Init/specif.cmx +theories/Sets/partial_Order.cmo: theories/Sets/ensembles.cmo \ + theories/Sets/relations_1.cmo +theories/Sets/partial_Order.cmx: theories/Sets/ensembles.cmx \ + theories/Sets/relations_1.cmx theories/Sets/powerset.cmo: theories/Sets/partial_Order.cmo theories/Sets/powerset.cmx: theories/Sets/partial_Order.cmx theories/Sets/uniset.cmo: theories/Init/datatypes.cmo \ @@ -274,14 +220,24 @@ theories/ZArith/zArith_dec.cmo: theories/ZArith/fast_integer.cmo \ theories/Init/specif.cmo theories/Bool/sumbool.cmo theories/ZArith/zArith_dec.cmx: theories/ZArith/fast_integer.cmx \ theories/Init/specif.cmx theories/Bool/sumbool.cmx +theories/ZArith/zbool.cmo: theories/Bool/sumbool.cmo \ + theories/ZArith/zArith_dec.cmo theories/ZArith/zmisc.cmo +theories/ZArith/zbool.cmx: theories/Bool/sumbool.cmx \ + theories/ZArith/zArith_dec.cmx theories/ZArith/zmisc.cmx theories/ZArith/zcomplements.cmo: theories/Init/datatypes.cmo \ theories/ZArith/fast_integer.cmo theories/Init/specif.cmo \ - theories/ZArith/wf_Z.cmo theories/ZArith/zArith_dec.cmo \ - theories/ZArith/zarith_aux.cmo + theories/ZArith/wf_Z.cmo theories/ZArith/zarith_aux.cmo theories/ZArith/zcomplements.cmx: theories/Init/datatypes.cmx \ theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \ - theories/ZArith/wf_Z.cmx theories/ZArith/zArith_dec.cmx \ - theories/ZArith/zarith_aux.cmx + theories/ZArith/wf_Z.cmx theories/ZArith/zarith_aux.cmx +theories/ZArith/zdiv.cmo: theories/Init/datatypes.cmo \ + theories/ZArith/fast_integer.cmo theories/Init/specif.cmo \ + theories/ZArith/zArith_dec.cmo theories/ZArith/zarith_aux.cmo \ + theories/ZArith/zmisc.cmo +theories/ZArith/zdiv.cmx: theories/Init/datatypes.cmx \ + theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \ + theories/ZArith/zArith_dec.cmx theories/ZArith/zarith_aux.cmx \ + theories/ZArith/zmisc.cmx theories/ZArith/zlogarithm.cmo: theories/ZArith/fast_integer.cmo \ theories/ZArith/zarith_aux.cmo theories/ZArith/zlogarithm.cmx: theories/ZArith/fast_integer.cmx \ @@ -296,3 +252,9 @@ theories/ZArith/zpower.cmo: theories/Init/datatypes.cmo \ theories/ZArith/zpower.cmx: theories/Init/datatypes.cmx \ theories/ZArith/fast_integer.cmx theories/ZArith/zarith_aux.cmx \ theories/ZArith/zmisc.cmx +theories/ZArith/zsqrt.cmo: theories/ZArith/fast_integer.cmo \ + theories/Init/specif.cmo theories/ZArith/zArith_dec.cmo \ + theories/ZArith/zarith_aux.cmo +theories/ZArith/zsqrt.cmx: theories/ZArith/fast_integer.cmx \ + theories/Init/specif.cmx theories/ZArith/zArith_dec.cmx \ + theories/ZArith/zarith_aux.cmx diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v index 44aeff317..ad95428f1 100644 --- a/contrib/extraction/test_extraction.v +++ b/contrib/extraction/test_extraction.v @@ -13,8 +13,9 @@ type nat = | S of nat *) -Extraction [x:nat]x. -(* fun x -> x *) +Definition test1 := [x:nat]x. +Extraction test1. +(* let test1 x = x *) Inductive c [x:nat] : nat -> Set := refl : (c x x) @@ -26,42 +27,55 @@ type c = | Trans of nat * nat * c *) -Extraction [f:nat->nat][x:nat](f x). -(* fun f x -> f x *) +Definition test2 := [f:nat->nat][x:nat](f x). +Extraction test2. +(* let test2 f x = f x *) -Extraction [f:nat->Set->nat][x:nat](f x nat). -(* fun f x -> f x () *) +Definition test3 := [f:nat->Set->nat][x:nat](f x nat). +Extraction test3. +(* let test3 f x = f x () *) -Extraction [f:(nat->nat)->nat][x:nat][g:nat->nat](f g). -(* fun f x g -> f g *) +Definition test4 := [f:(nat->nat)->nat][x:nat][g:nat->nat](f g). +Extraction test4. +(* let test4 f x g = f g *) -Extraction (pair ? ? (S O) O). -(* Pair ((S O), O) *) +Definition test5 := (pair ? ? (S O) O). +Extraction test5. +(* let test5 = Pair ((S O), O) *) Definition cf := [x:nat][_:(le x O)](S x). -Extraction (cf O (le_n O)). -(* cf O *) +Extraction NoInline cf. +Definition test6 := (cf O (le_n O)). +Extraction test6. +(* let test6 = cf O *) -Extraction ([X:Set][x:X]x nat). -(* fun x -> x *) +Definition test7 := ([X:Set][x:X]x nat). +Extraction test7. +(* let test7 x = x *) Definition d := [X:Type]X. Extraction d. (* type 'x d = 'x *) -Extraction (d Set). (* unit d *) -Extraction [x:(d Set)]O. (* fun _ -> O *) -Extraction (d nat). (* nat d *) - -Extraction ([x:(d Type)]O Type). (* O *) - -Extraction ([x:(d Type)]x). (* 'a1 *) - -Extraction ([X:Type][x:X]x Set nat). (* nat *) +Definition d2 := (d Set). +Extraction d2. (* type d2 = unit d *) +Definition d3 := [x:(d Set)]O. +Extraction d3. (* let d3 _ = O *) +Definition d4 := (d nat). +Extraction d4. (* type d4 = nat d *) +Definition d5 := ([x:(d Type)]O Type). +Extraction d5. (* let d5 = O *) +Definition d6 := ([x:(d Type)]x). +Extraction d6. (* type 'x d6 = 'x *) + +Definition test8 := ([X:Type][x:X]x Set nat). +Extraction test8. (* type test8 = nat *) Definition id' := [X:Type][x:X]x. Extraction id'. (* let id' x = x *) -Extraction (id' Set nat). (* nat *) +Definition id'' := (id' Set nat). +Extraction id''. (* type id'' = Obj.t *) -Extraction let t = nat in (id' Set t). (* nat *) +Definition test9 := let t = nat in (id' Set t). +Extraction test9. (* type test9 = Obj.t *) Definition Ensemble := [U:Type]U->Prop. Definition Empty_set := [U:Type][x:U]False. @@ -79,12 +93,15 @@ type 'u finite = | Union_is_finite of 'u finite * 'u *) -Extraction ([X:Type][x:X]O Type Type). (* O *) +Definition test10 := ([X:Type][x:X]O Type Type). +Extraction test10. (* let test10 = O *) -Extraction let n=O in let p=(S n) in (S p). (* S (S O) *) +Definition test11 := let n=O in let p=(S n) in (S p). +Extraction test11. (* let test11 = S (S O) *) -Extraction (x:(X:Type)X->X)(x Type Type). -(* (unit -> Obj.t -> Obj.t) -> Obj.t *) +Definition test12 := (x:(X:Type)X->X)(x Type Type). +Extraction test12. +(* type test12 = (unit -> Obj.t -> Obj.t) -> Obj.t *) (** Mutual Inductive *) @@ -120,8 +137,8 @@ and forest_size = function | Cons (t, f') -> plus (tree_size t) (forest_size f') *) -Extraction Cases (left True True I) of (left x)=>(S O) | (right x)=>O end. -(* S O *) +Definition test13 := Cases (left True True I) of (left x)=>(S O) | (right x)=>O end. +Extraction test13. (* let test13 = S O *) Extraction sumbool_rect. (* @@ -143,10 +160,12 @@ type predicate = (** Eta-expansions of inductive constructor *) Inductive titi : Set := tata : nat->nat->nat->nat->titi. -Extraction (tata O). -(* fun x x0 x1 -> Tata (O, x, x0, x1) *) -Extraction (tata O (S O)). -(* fun x x0 -> Tata (O, (S O), x, x0) *) +Definition test14 := (tata O). +Extraction test14. +(* let test14 x x0 x1 = Tata (O, x, x0, x1) *) +Definition test15 := (tata O (S O)). +Extraction test15. +(* let test15 x x0 = Tata (O, (S O), x, x0) *) Inductive eta : Set := eta_c : nat->Prop->nat->Prop->eta. Extraction eta_c. @@ -154,12 +173,15 @@ Extraction eta_c. type eta = | Eta_c of nat * nat *) -Extraction (eta_c O). -(* fun _ x _ -> Eta_c (O, x) *) -Extraction (eta_c O True). -(* fun x _ -> Eta_c (O, x) *) -Extraction (eta_c O True O). -(* fun _ -> Eta_c (O, O) *) +Definition test16 := (eta_c O). +Extraction test16. +(* let test16 x = Eta_c (O, x) *) +Definition test17 := (eta_c O True). +Extraction test17. +(* let test17 x = Eta_c (O, x) *) +Definition test18 := (eta_c O True O). +Extraction test18. +(* let test18 _ = Eta_c (O, O) *) (** Example of singleton inductive type *) @@ -174,24 +196,24 @@ Extraction fbidon. (* let fbidon f x y = f x y *) -Extraction (fbidon True nat (tb True nat)). -(* fun x0 x -> fbidon (fun _ x1 -> x1) x0 x *) + Definition fbidon2 := (fbidon True nat (tb True nat)). -Extraction fbidon2. -(* let fbidon2 x = - x -*) +Extraction fbidon2. (* let fbidon2 x = x *) +Extraction NoInline fbidon. +Extraction fbidon2. +(* let test19 x = fbidon (fun x0 x1 -> x1) () x *) + (** NB: first argument of fbidon2 has type [True], so it disappears. *) (** mutual inductive on many sorts *) Inductive - test0 : Prop := ctest0 : test0 + test_0 : Prop := ctest0 : test_0 with - test1 : Set := ctest1 : test0-> test1. -Extraction test0. + test_1 : Set := ctest1 : test_0-> test_1. +Extraction test_0. (* test0 : logical inductive *) -Extraction test1. +Extraction test_1. (* type test1 = | Ctest1 @@ -208,8 +230,14 @@ Extraction eq_rect. (** example with more arguments that given by the type *) -Extraction (nat_rec [n:nat]nat->nat [n:nat]O [n:nat][f:nat->nat]f O O). -(* nat_rec (fun n -> O) (fun n f -> f) O O *) +Definition test19 := (nat_rec [n:nat]nat->nat [n:nat]O [n:nat][f:nat->nat]f O O). +Extraction test19. +(* let test19 = + let rec f = function + | O -> (fun n0 -> O) + | S n0 -> f n0 + in f O O +*) (** No more propagation of type parameters. Obj.t instead. *) @@ -237,8 +265,9 @@ and tp2bis = (** casts *) -Extraction (True :: Type). -(* unit *) +Definition test20 := (True :: Type). +Extraction test20. +(* type t = unit *) (* examples needing Obj.magic *) (* hybrids *) @@ -291,20 +320,23 @@ let zeroprop = function (** polymorphic f applied several times *) -Extraction (pair ? ? (id' nat O) (id' bool true)). -(* Pair ((id' O), (id' True)) *) +Definition test21 := (pair ? ? (id' nat O) (id' bool true)). +Extraction test21. +(* let test21 = Pair ((id' O), (id' True)) *) (** ok *) -Extraction -([i:(X:Type)X->X](pair ? ? (i nat O) (i bool true)) [X:Type][x:X]x). -(* let i = fun x -> x in Pair ((i O), (i True)) *) +Definition test22 := ([i:(X:Type)X->X](pair ? ? (i nat O) (i bool true)) [X:Type][x:X]x). +Extraction test22. +(* let test22 = + let i = fun x -> x in Pair ((i O), (i True)) *) (* still ok via optim beta -> let *) -Extraction [i:(X:Type)X->X](pair ? ? (i nat O) (i bool true)). -(* fun i -> Pair ((i () O), (i () True)) *) +Definition test23 := [i:(X:Type)X->X](pair ? ? (i nat O) (i bool true)). +Extraction test23. +(* let test23 i = Pair ((i () O), (i () True)) *) (* problem: fun f -> (f 0, f true) not legal in ocaml *) (* solution: fun f -> (f 0, Obj.magic f true) *) @@ -385,8 +417,9 @@ let oups h0 = match h0 with (* Dependant type over Type *) -Extraction (sigT Set [a:Set](option a)). -(* (unit, Obj.t option) sigT *) +Definition test24:= (sigT Set [a:Set](option a)). +Extraction test24. +(* type test24 = (unit, Obj.t option) sigT *) (* Coq term non strongly-normalizable after extraction *) @@ -396,4 +429,10 @@ Definition loop := [Ax:(Acc nat gt O)] (Fix F {F [a:nat;b:(Acc nat gt a)] : nat := (F (S a) (Acc_inv nat gt a b (S a) (gt_Sn_n a)))} - O Ax).
\ No newline at end of file + O Ax). +Extraction loop. +(* let loop _ = + let rec f a = + f (S a) + in f O +*)
\ No newline at end of file |