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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
|
(* Reduction of native operators *)
open Names
open CPrimitives
open Retroknowledge
open Environ
open CErrors
let add_retroknowledge env action =
match action with
| Register_type(PT_int63,c) ->
let retro = env.retroknowledge in
let retro =
match retro.retro_int63 with
| None -> { retro with retro_int63 = Some c }
| Some c' -> assert (Constant.equal c c'); retro in
set_retroknowledge env retro
| Register_ind(pit,ind) ->
let retro = env.retroknowledge in
let retro =
match pit with
| PIT_bool ->
let r =
match retro.retro_bool with
| None -> ((ind,1), (ind,2))
| Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in
{ retro with retro_bool = Some r }
| PIT_carry ->
let r =
match retro.retro_carry with
| None -> ((ind,1), (ind,2))
| Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in
{ retro with retro_carry = Some r }
| PIT_pair ->
let r =
match retro.retro_pair with
| None -> (ind,1)
| Some ((ind',_) as t) -> assert (eq_ind ind ind'); t in
{ retro with retro_pair = Some r }
| PIT_cmp ->
let r =
match retro.retro_cmp with
| None -> ((ind,1), (ind,2), (ind,3))
| Some (((ind',_),_,_) as t) -> assert (eq_ind ind ind'); t in
{ retro with retro_cmp = Some r }
in
set_retroknowledge env retro
let get_int_type env =
match env.retroknowledge.retro_int63 with
| Some c -> c
| None -> anomaly Pp.(str"Reduction of primitive: int63 not registered")
let get_bool_constructors env =
match env.retroknowledge.retro_bool with
| Some r -> r
| None -> anomaly Pp.(str"Reduction of primitive: bool not registered")
let get_carry_constructors env =
match env.retroknowledge.retro_carry with
| Some r -> r
| None -> anomaly Pp.(str"Reduction of primitive: carry not registered")
let get_pair_constructor env =
match env.retroknowledge.retro_pair with
| Some c -> c
| None -> anomaly Pp.(str"Reduction of primitive: pair not registered")
let get_cmp_constructors env =
match env.retroknowledge.retro_cmp with
| Some r -> r
| None -> anomaly Pp.(str"Reduction of primitive: cmp not registered")
exception NativeDestKO
module type RedNativeEntries =
sig
type elem
type args
type evd (* will be unit in kernel, evar_map outside *)
val get : args -> int -> elem
val get_int : evd -> elem -> Uint63.t
val mkInt : env -> Uint63.t -> elem
val mkBool : env -> bool -> elem
val mkCarry : env -> bool -> elem -> elem (* true if carry *)
val mkIntPair : env -> elem -> elem -> elem
val mkLt : env -> elem
val mkEq : env -> elem
val mkGt : env -> elem
end
module type RedNative =
sig
type elem
type args
type evd
val red_prim : env -> evd -> CPrimitives.t -> args -> elem option
end
module RedNative (E:RedNativeEntries) :
RedNative with type elem = E.elem
with type args = E.args
with type evd = E.evd =
struct
type elem = E.elem
type args = E.args
type evd = E.evd
let get_int evd args i = E.get_int evd (E.get args i)
let get_int1 evd args = get_int evd args 0
let get_int2 evd args = get_int evd args 0, get_int evd args 1
let get_int3 evd args =
get_int evd args 0, get_int evd args 1, get_int evd args 2
let red_prim_aux env evd op args =
let open CPrimitives in
match op with
| Int63head0 ->
let i = get_int1 evd args in E.mkInt env (Uint63.head0 i)
| Int63tail0 ->
let i = get_int1 evd args in E.mkInt env (Uint63.tail0 i)
| Int63add ->
let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.add i1 i2)
| Int63sub ->
let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.sub i1 i2)
| Int63mul ->
let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.mul i1 i2)
| Int63div ->
let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.div i1 i2)
| Int63mod ->
let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.rem i1 i2)
| Int63lsr ->
let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sr i1 i2)
| Int63lsl ->
let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sl i1 i2)
| Int63land ->
let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_and i1 i2)
| Int63lor ->
let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_or i1 i2)
| Int63lxor ->
let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_xor i1 i2)
| Int63addc ->
let i1, i2 = get_int2 evd args in
let s = Uint63.add i1 i2 in
E.mkCarry env (Uint63.lt s i1) (E.mkInt env s)
| Int63subc ->
let i1, i2 = get_int2 evd args in
let s = Uint63.sub i1 i2 in
E.mkCarry env (Uint63.lt i1 i2) (E.mkInt env s)
| Int63addCarryC ->
let i1, i2 = get_int2 evd args in
let s = Uint63.add (Uint63.add i1 i2) (Uint63.of_int 1) in
E.mkCarry env (Uint63.le s i1) (E.mkInt env s)
| Int63subCarryC ->
let i1, i2 = get_int2 evd args in
let s = Uint63.sub (Uint63.sub i1 i2) (Uint63.of_int 1) in
E.mkCarry env (Uint63.le i1 i2) (E.mkInt env s)
| Int63mulc ->
let i1, i2 = get_int2 evd args in
let (h, l) = Uint63.mulc i1 i2 in
E.mkIntPair env (E.mkInt env h) (E.mkInt env l)
| Int63diveucl ->
let i1, i2 = get_int2 evd args in
let q,r = Uint63.div i1 i2, Uint63.rem i1 i2 in
E.mkIntPair env (E.mkInt env q) (E.mkInt env r)
| Int63div21 ->
let i1, i2, i3 = get_int3 evd args in
let q,r = Uint63.div21 i1 i2 i3 in
E.mkIntPair env (E.mkInt env q) (E.mkInt env r)
| Int63addMulDiv ->
let p, i, j = get_int3 evd args in
E.mkInt env
(Uint63.l_or
(Uint63.l_sl i p)
(Uint63.l_sr j (Uint63.sub (Uint63.of_int Uint63.uint_size) p)))
| Int63eq ->
let i1, i2 = get_int2 evd args in
E.mkBool env (Uint63.equal i1 i2)
| Int63lt ->
let i1, i2 = get_int2 evd args in
E.mkBool env (Uint63.lt i1 i2)
| Int63le ->
let i1, i2 = get_int2 evd args in
E.mkBool env (Uint63.le i1 i2)
| Int63compare ->
let i1, i2 = get_int2 evd args in
begin match Uint63.compare i1 i2 with
| x when x < 0 -> E.mkLt env
| 0 -> E.mkEq env
| _ -> E.mkGt env
end
let red_prim env evd p args =
try
let r =
red_prim_aux env evd p args
in Some r
with NativeDestKO -> None
end
|
