aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/extraction_dep.v
blob: e770cf779aeb7642b5c0d3a8190a98c2c0996f64 (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

(** Examples of code elimination inside modules during extraction *)

Require Coq.extraction.Extraction.

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

(** 1) Without signature ... *)

Module A.
 Definition u := 0.
 Definition v := 1.
 Module B.
  Definition w := 2.
  Definition x := 3.
 End B.
End A.

Definition testA := A.u + A.B.x.

Recursive Extraction testA. (* without: v w *)

(** 1b) Same with an Include *)

Module Abis.
 Include A.
 Definition y := 4.
End Abis.

Definition testAbis := Abis.u + Abis.y.

Recursive Extraction testAbis. (* without: A B v w x *)

(** 2) With signature, we only keep elements mentionned in signature. *)

Module Type SIG.
 Parameter u : nat.
 Parameter v : nat.
End SIG.

Module Ater : SIG.
 Include A.
End Ater.

Definition testAter := Ater.u.

Recursive Extraction testAter. (* with only: u v *)