1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
12
(**** A few tests for the extraction mechanism ****)
14
(* Ideally, we should monitor the extracted output
15
for changes, but this is painful. For the moment,
16
we just check for failures of this script. *)
18
(*** STANDARD EXAMPLES *)
22
Definition idnat (x:nat) := x.
26
Definition id (X:Type) (x:X) := x.
27
Extraction id. (* let id x = x *)
28
Definition id' := id Set nat.
29
Extraction id'. (* type id' = nat *)
31
Definition test2 (f:nat -> nat) (x:nat) := f x.
33
(* let test2 f x = f x *)
35
Definition test3 (f:nat -> Set -> nat) (x:nat) := f x nat.
37
(* let test3 f x = f x __ *)
39
Definition test4 (f:(nat -> nat) -> nat) (x:nat) (g:nat -> nat) := f g.
41
(* let test4 f x g = f g *)
43
Definition test5 := (1, 0).
45
(* let test5 = Pair ((S O), O) *)
47
Definition cf (x:nat) (_:x <= 0) := S x.
48
Extraction NoInline cf.
49
Definition test6 := cf 0 (le_n 0).
51
(* let test6 = cf O *)
53
Definition test7 := (fun (X:Set) (x:X) => x) nat.
57
Definition d (X:Type) := X.
58
Extraction d. (* type 'x d = 'x *)
59
Definition d2 := d Set.
60
Extraction d2. (* type d2 = __ d *)
61
Definition d3 (x:d Set) := 0.
62
Extraction d3. (* let d3 _ = O *)
63
Definition d4 := d nat.
64
Extraction d4. (* type d4 = nat d *)
65
Definition d5 := (fun x:d Type => 0) Type.
66
Extraction d5. (* let d5 = O *)
67
Definition d6 (x:d Type) := x.
68
Extraction d6. (* type 'x d6 = 'x *)
70
Definition test8 := (fun (X:Type) (x:X) => x) Set nat.
71
Extraction test8. (* type test8 = nat *)
73
Definition test9 := let t := nat in id Set t.
74
Extraction test9. (* type test9 = nat *)
76
Definition test10 := (fun (X:Type) (x:X) => 0) Type Type.
77
Extraction test10. (* let test10 = O *)
79
Definition test11 := let n := 0 in let p := S n in S p.
80
Extraction test11. (* let test11 = S (S O) *)
82
Definition test12 := forall x:forall X:Type, X -> X, x Type Type.
84
(* type test12 = (__ -> __ -> __) -> __ *)
87
Definition test13 := match @left True True I with
91
Extraction test13. (* let test13 = S O *)
94
(** example with more arguments that given by the type *)
97
nat_rec (fun n:nat => nat -> nat) (fun n:nat => 0)
98
(fun (n:nat) (f:nat -> nat) => f) 0 0.
110
Definition test20 := True:Type.
112
(* type test20 = __ *)
115
(** Simple inductive type and recursor. *)
124
Extraction sumbool_rect.
126
let sumbool_rect f f0 = function
131
(** Less simple inductive type. *)
133
Inductive c (x:nat) : nat -> Set :=
135
| trans : forall y z:nat, c x y -> y <= z -> c x z.
140
| Trans of nat * nat * c
143
Definition Ensemble (U:Type) := U -> Prop.
144
Definition Empty_set (U:Type) (x:U) := False.
145
Definition Add (U:Type) (A:Ensemble U) (x y:U) := A y \/ x = y.
147
Inductive Finite (U:Type) : Ensemble U -> Type :=
148
| Empty_is_finite : Finite U (Empty_set U)
151
Finite U A -> forall x:U, ~ A x -> Finite U (Add U A x).
156
| Union_is_finite of 'u finite * 'u
160
(** Mutual Inductive *)
162
Inductive tree : Set :=
163
Node : nat -> forest -> tree
165
| Leaf : nat -> forest
166
| Cons : tree -> forest -> forest.
171
| Node of nat * forest
174
| Cons of tree * forest
177
Fixpoint tree_size (t:tree) : nat :=
179
| Node a f => S (forest_size f)
182
with forest_size (f:forest) : nat :=
185
| Cons t f' => tree_size t + forest_size f'
188
Extraction tree_size.
190
let rec tree_size = function
191
| Node (a, f) -> S (forest_size f)
192
and forest_size = function
194
| Cons (t, f') -> plus (tree_size t) (forest_size f')
198
(** Eta-expansions of inductive constructor *)
200
Inductive titi : Set :=
201
tata : nat -> nat -> nat -> nat -> titi.
202
Definition test14 := tata 0.
204
(* let test14 x x0 x1 = Tata (O, x, x0, x1) *)
205
Definition test15 := tata 0 1.
207
(* let test15 x x0 = Tata (O, (S O), x, x0) *)
209
Inductive eta : Type :=
210
eta_c : nat -> Prop -> nat -> Prop -> eta.
216
Definition test16 := eta_c 0.
218
(* let test16 x = Eta_c (O, x) *)
219
Definition test17 := eta_c 0 True.
221
(* let test17 x = Eta_c (O, x) *)
222
Definition test18 := eta_c 0 True 0.
224
(* let test18 _ = Eta_c (O, O) *)
227
(** Example of singleton inductive type *)
229
Inductive bidon (A:Prop) (B:Type) : Type :=
230
tb : forall (x:A) (y:B), bidon A B.
231
Definition fbidon (A B:Type) (f:A -> B -> bidon True nat)
232
(x:A) (y:B) := f x y.
234
(* type 'b bidon = 'b *)
236
(* tb : singleton inductive constructor *)
238
(* let fbidon f x y =
242
Definition fbidon2 := fbidon True nat (tb True nat).
243
Extraction fbidon2. (* let fbidon2 y = y *)
244
Extraction NoInline fbidon.
246
(* let fbidon2 y = fbidon (fun _ x -> x) __ y *)
248
(* NB: first argument of fbidon2 has type [True], so it disappears. *)
250
(** mutual inductive on many sorts *)
252
Inductive test_0 : Prop :=
255
ctest1 : test_0 -> test_1.
257
(* test0 : logical inductive *)
264
(** logical singleton *)
267
(* eq : logical inductive *)
269
(* let eq_rect x f y =
273
(** No more propagation of type parameters. Obj.t instead. *)
275
Inductive tp1 : Type :=
276
T : forall (C:Set) (c:C), tp2 -> tp1
287
Inductive tp1bis : Type :=
288
Tbis : tp2bis -> tp1bis
289
with tp2bis : Type :=
290
T'bis : forall (C:Set) (c:C), tp1bis -> tp2bis.
296
| T'bis of __ * tp1bis
300
(** Strange inductive type. *)
302
Inductive Truc : Set -> Type :=
303
| chose : forall A:Set, Truc A
304
| machin : forall A:Set, A -> Truc bool -> Truc A.
309
| Machin of 'x * bool truc
313
(** Dependant type over Type *)
315
Definition test24 := sigT (fun a:Set => option a).
317
(* type test24 = (__, __ option) sigT *)
320
(** Coq term non strongly-normalizable after extraction *)
323
Definition loop (Ax:Acc gt 0) :=
324
(fix F (a:nat) (b:Acc gt a) {struct b} : nat :=
325
F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax.
333
(*** EXAMPLES NEEDING OBJ.MAGIC *)
335
(** False conversion of type: *)
337
Lemma oups : forall H:nat = list nat, nat -> nat.
339
generalize H0; intros.
349
match Obj.magic h0 with
357
Definition horibilis (b:bool) :=
358
if b as b return (if b then Type else nat) then Set else 0.
359
Extraction horibilis.
361
let horibilis = function
362
| True -> Obj.magic __
363
| False -> Obj.magic O
366
Definition PropSet (b:bool) := if b then Prop else Set.
367
Extraction PropSet. (* type propSet = __ *)
369
Definition natbool (b:bool) := if b then nat else bool.
370
Extraction natbool. (* type natbool = __ *)
372
Definition zerotrue (b:bool) := if b as x return natbool x then 0 else true.
375
let zerotrue = function
376
| True -> Obj.magic O
377
| False -> Obj.magic True
380
Definition natProp (b:bool) := if b return Type then nat else Prop.
382
Definition natTrue (b:bool) := if b return Type then nat else True.
384
Definition zeroTrue (b:bool) := if b as x return natProp x then 0 else True.
387
let zeroTrue = function
388
| True -> Obj.magic O
389
| False -> Obj.magic __
392
Definition natTrue2 (b:bool) := if b return Type then nat else True.
394
Definition zeroprop (b:bool) := if b as x return natTrue x then 0 else I.
397
let zeroprop = function
398
| True -> Obj.magic O
399
| False -> Obj.magic __
402
(** polymorphic f applied several times *)
404
Definition test21 := (id nat 0, id bool true).
406
(* let test21 = Pair ((id O), (id True)) *)
411
(fun f:forall X:Type, X -> X => (f nat 0, f bool true))
412
(fun (X:Type) (x:X) => x).
415
let f = fun x -> x in Pair ((f O), (f True)) *)
417
(* still ok via optim beta -> let *)
419
Definition test23 (f:forall X:Type, X -> X) := (f nat 0, f bool true).
421
(* let test23 f = Pair ((Obj.magic f __ O), (Obj.magic f __ True)) *)
423
(* problem: fun f -> (f 0, f true) not legal in ocaml *)
424
(* solution: magic ... *)
427
(** Dummy constant __ can be applied.... *)
429
Definition f (X:Type) (x:nat -> X) (y:X -> bool) : bool := y (x 0).
435
Definition f_prop := f (0 = 0) (fun _ => refl_equal 0) (fun _ => true).
436
Extraction NoInline f.
439
f (Obj.magic __) (fun _ -> True)
442
Definition f_arity := f Set (fun _:nat => nat) (fun _:Set => true).
445
f (Obj.magic __) (fun _ -> True)
448
Definition f_normal :=
449
f nat (fun x => x) (fun x => match x with
455
f (fun x -> x) (fun x -> match x with
461
(* inductive with magic needed *)
463
Inductive Boite : Set :=
464
boite : forall b:bool, (if b then nat else (nat * nat)%type) -> Boite.
472
Definition boite1 := boite true 0.
474
(* let boite1 = Boite (True, (Obj.magic O)) *)
476
Definition boite2 := boite false (0, 0).
478
(* let boite2 = Boite (False, (Obj.magic (Pair (O, O)))) *)
480
Definition test_boite (B:Boite) :=
481
match B return nat with
483
| boite false n => fst n + snd n
485
Extraction test_boite.
487
let test_boite = function
490
| True -> Obj.magic n
491
| False -> plus (fst (Obj.magic n)) (snd (Obj.magic n)))
494
(* singleton inductive with magic needed *)
496
Inductive Box : Type :=
497
box : forall A:Set, A -> Box.
501
Definition box1 := box nat 0.
502
Extraction box1. (* let box1 = Obj.magic O *)
504
(* applied constant, magic needed *)
506
Definition idzarb (b:bool) (x:if b then nat else bool) := x.
507
Definition zarb := idzarb true 0.
508
Extraction NoInline idzarb.
510
(* let zarb = Obj.magic idzarb True (Obj.magic O) *)
512
(** function of variable arity. *)
513
(** Fun n = nat -> nat -> ... -> nat *)
515
Fixpoint Fun (n:nat) : Set :=
518
| S n => nat -> Fun n
521
Fixpoint Const (k n:nat) {struct n} : Fun n :=
522
match n as x return Fun x with
524
| S n => fun p:nat => Const k n
527
Fixpoint proj (k n:nat) {struct n} : Fun n :=
528
match n as x return Fun x with
529
| O => 0 (* ou assert false ....*)
532
| O => fun x => Const x n
533
| S k => fun x => proj k n
537
Definition test_proj := proj 2 4 0 1 2 3.
539
Eval compute in test_proj.
541
Recursive Extraction test_proj.
547
(* Was previously producing a "test_extraction.ml" *)
549
idnat id id' test2 test3 test4 test5 test6 test7 d d2
550
d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
551
test13 test19 test20 nat sumbool_rect c Finite tree
552
tree_size test14 test15 eta_c test16 test17 test18 bidon
553
tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
554
tp1bis Truc oups test24 loop horibilis PropSet natbool
555
zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
556
f_arity f_normal Boite boite1 boite2 test_boite Box box1
559
Extraction Language Haskell.
560
(* Was previously producing a "Test_extraction.hs" *)
562
idnat id id' test2 test3 test4 test5 test6 test7 d d2
563
d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
564
test13 test19 test20 nat sumbool_rect c Finite tree
565
tree_size test14 test15 eta_c test16 test17 test18 bidon
566
tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
567
tp1bis Truc oups test24 loop horibilis PropSet natbool
568
zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
569
f_arity f_normal Boite boite1 boite2 test_boite Box box1
572
Extraction Language Scheme.
573
(* Was previously producing a "test_extraction.scm" *)
575
idnat id id' test2 test3 test4 test5 test6 test7 d d2
576
d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
577
test13 test19 test20 nat sumbool_rect c Finite tree
578
tree_size test14 test15 eta_c test16 test17 test18 bidon
579
tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1
580
tp1bis Truc oups test24 loop horibilis PropSet natbool
581
zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
582
f_arity f_normal Boite boite1 boite2 test_boite Box box1
586
(*** Finally, a test more focused on everyday's life situations ***)
588
Require Import ZArith.
590
Recursive Extraction two_or_two_plus_one Zdiv_eucl_exist.
added
removed
test-suite/success/extraction.v
