aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/extraction_impl.v
blob: dfdeff82ffda72cfc80f7a142f07ceb2aefc15bf (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

(** Examples of extraction with manually-declared implicit arguments *)

(** NB: we should someday check the produced code instead of
    simply running the commands. *)

(** Bug #4243, part 1 *)

Inductive dnat : nat -> Type :=
| d0 : dnat 0
| ds : forall n m, n = m -> dnat n ->  dnat (S n).

Extraction Implicit ds [m].

Lemma dnat_nat: forall n, dnat n -> nat.
Proof.
  intros n d.
  induction d as [| n m Heq d IHn].
  exact 0. exact (S IHn).
Defined.

Recursive Extraction dnat_nat.

Extraction Implicit dnat_nat [n].
Recursive Extraction dnat_nat.

(** Same, with a Fixpoint *)

Fixpoint dnat_nat' n (d:dnat n) :=
 match d with
 | d0 => 0
 | ds n m _ d => S (dnat_nat' n d)
 end.

Recursive Extraction dnat_nat'.

Extraction Implicit dnat_nat' [n].
Recursive Extraction dnat_nat'.

(** Bug #4243, part 2 *)

Inductive enat: nat -> Type :=
  e0: enat 0
| es: forall n, enat n -> enat (S n).

Lemma enat_nat: forall n, enat n -> nat.
Proof.
  intros n e.
  induction e as [| n e IHe].
  exact (O).
  exact (S IHe).
Defined.

Extraction Implicit es [n].
Extraction Implicit enat_nat [n].
Recursive Extraction enat_nat.

(** Same, with a Fixpoint *)

Fixpoint enat_nat' n (e:enat n) : nat :=
 match e with
 | e0 => 0
 | es n e => S (enat_nat' n e)
 end.

Extraction Implicit enat_nat' [n].
Recursive Extraction enat_nat'.

(** Bug #4228 *)

Module Food.
Inductive Course :=
| main:    nat -> Course
| dessert: nat -> Course.

Inductive Meal : Course -> Type :=
| one_course : forall n:nat, Meal (main n)
| two_course : forall n m, Meal (main n) -> Meal (dessert m).
Extraction Implicit two_course [n].
End Food.

Recursive Extraction Food.Meal.