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 *)
|
