blob: 3e2974ea1519ecf79e8a851e4b8332ac052fee53 (
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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
(** * Extraction Directives for [nat] in Haskell *)
(** [nat] is really complicated, so we jump through many hoops to get
code that compiles in 8.4 and 8.5 at the same time. *)
Require Coq.Numbers.Natural.Peano.NPeano.
Require Coq.Arith.Compare_dec Coq.Arith.EqNat Coq.Arith.Peano_dec.
Extract Inductive nat => "Prelude.Integer" [ "0" "Prelude.succ" ]
"(\fO fS n -> {- match_on_nat -} if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
(** We rely on the fact that Coq forbids masking absolute names. Hopefully we can drop support for 8.4 before this is changed. *)
Module Coq.
Module M. Export NPeano.Nat. End M.
Module Init.
Module Nat.
Export M.
End Nat.
End Init.
Module Numbers.
Module Natural.
Module Peano.
Module NPeano.
Module Nat.
Export M.
End Nat.
End NPeano.
End Peano.
End Natural.
End Numbers.
Module Arith.
Module PeanoNat.
Module Nat.
Export M.
End Nat.
End PeanoNat.
End Arith.
End Coq.
Module Export Import_NPeano_Nat.
Import Coq.Numbers.Natural.Peano.NPeano.Nat.
Extract Inlined Constant add => "(Prelude.+)".
Extract Inlined Constant mul => "(Prelude.*)".
Extract Inlined Constant pow => "(Prelude.^)".
Extract Inlined Constant max => "Prelude.max".
Extract Inlined Constant min => "Prelude.min".
Extract Inlined Constant gcd => "Prelude.gcd".
Extract Inlined Constant lcm => "Prelude.lcm".
Extract Inlined Constant land => "(Data.Bits..&.)".
Extract Inlined Constant compare => "Prelude.compare".
Extract Inlined Constant ltb => "(Prelude.<)".
Extract Inlined Constant leb => "(Prelude.<=)".
Extract Inlined Constant eqb => "(Prelude.==)".
Extract Inlined Constant eq_dec => "(Prelude.==)".
Extract Inlined Constant odd => "Prelude.odd".
Extract Inlined Constant even => "Prelude.even".
Extract Constant pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
Extract Constant sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
Extract Constant div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
Extract Constant modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
(* XXX: unsound due to potential overflow in the second argument *)
Extract Constant shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))".
Extract Constant shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))".
Extract Constant testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))".
End Import_NPeano_Nat.
Module Export Import_Init_Nat.
Import Coq.Init.Nat.
Extract Inlined Constant add => "(Prelude.+)".
Extract Inlined Constant mul => "(Prelude.*)".
Extract Inlined Constant max => "Prelude.max".
Extract Inlined Constant min => "Prelude.min".
Extract Constant pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
Extract Constant sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
Extract Constant div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
Extract Constant modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
(* XXX: unsound due to potential overflow in the second argument *)
Extract Constant shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))".
Extract Constant shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))".
Extract Constant testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))".
End Import_Init_Nat.
Module Export Import_PeanoNat_Nat.
Import Coq.Arith.PeanoNat.Nat.
Extract Inlined Constant eq_dec => "(Prelude.==)".
Extract Inlined Constant add => "(Prelude.+)".
Extract Inlined Constant mul => "(Prelude.*)".
Extract Inlined Constant max => "Prelude.max".
Extract Inlined Constant min => "Prelude.min".
Extract Inlined Constant compare => "Prelude.compare".
(* XXX: unsound due to potential overflow in the second argument *)
Extract Constant shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))".
Extract Constant shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))".
Extract Constant testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))".
End Import_PeanoNat_Nat.
Extract Inlined Constant Compare_dec.nat_compare_alt => "Prelude.compare".
Extract Inlined Constant Compare_dec.lt_dec => "(Prelude.<)".
Extract Inlined Constant Compare_dec.leb => "(Prelude.<=)".
Extract Inlined Constant Compare_dec.le_lt_dec => "(Prelude.<=)".
Extract Inlined Constant EqNat.beq_nat => "(Prelude.==)".
Extract Inlined Constant EqNat.eq_nat_decide => "(Prelude.==)".
Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)".
|
