blob: fb0adabae99ba2281547e94968b9f7cf2e6fa8a7 (
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
|
(** Examples of code elimination inside modules during extraction *)
Require Coq.extraction.Extraction.
(** NB: we should someday check the produced code instead of
extracting and just compiling. *)
(** 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 *)
Extraction TestCompile testA.
(** 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 *)
Extraction TestCompile testAbis.
(** 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 *)
Extraction TestCompile testAter.
|
