Source file primred.ml
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
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
open Names
open CPrimitives
open Retroknowledge
open Environ
open CErrors
type _ action_kind =
| IncompatTypes : _ prim_type -> Constant.t action_kind
| IncompatInd : _ prim_ind -> inductive action_kind
type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn
let check_same_types typ c1 c2 =
if not (Constant.CanOrd.equal c1 c2)
then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2))
let check_same_inds ind i1 i2 =
if not (Ind.CanOrd.equal i1 i2)
then raise (IncompatibleDeclarations (IncompatInd ind, i1, i2))
let add_retroknowledge retro action =
match action with
| Register_type(typ,c) ->
begin match typ with
| PT_int63 ->
(match retro.retro_int63 with
| None -> { retro with retro_int63 = Some c }
| Some c' -> check_same_types typ c c'; retro)
| PT_float64 ->
(match retro.retro_float64 with
| None -> { retro with retro_float64 = Some c }
| Some c' -> check_same_types typ c c'; retro)
| PT_array ->
(match retro.retro_array with
| None -> { retro with retro_array = Some c }
| Some c' -> check_same_types typ c c'; retro)
end
| Register_ind(pit,ind) ->
begin match pit with
| PIT_bool ->
let r =
match retro.retro_bool with
| None -> ((ind,1), (ind,2))
| Some (((ind',_),_) as t) -> check_same_inds pit 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) -> check_same_inds pit 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) -> check_same_inds pit 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) -> check_same_inds pit ind ind'; t in
{ retro with retro_cmp = Some r }
| PIT_f_cmp ->
let r =
match retro.retro_f_cmp with
| None -> ((ind,1), (ind,2), (ind,3), (ind,4))
| Some (((ind',_),_,_,_) as t) -> check_same_inds pit ind ind'; t in
{ retro with retro_f_cmp = Some r }
| PIT_f_class ->
let r =
match retro.retro_f_class with
| None -> ((ind,1), (ind,2), (ind,3), (ind,4),
(ind,5), (ind,6), (ind,7), (ind,8),
(ind,9))
| Some (((ind',_),_,_,_,_,_,_,_,_) as t) ->
check_same_inds pit ind ind'; t in
{ retro with retro_f_class = Some r }
end
let add_retroknowledge env action =
set_retroknowledge env (add_retroknowledge env.retroknowledge action)
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_float_type env =
match env.retroknowledge.retro_float64 with
| Some c -> c
| None -> anomaly Pp.(str"Reduction of primitive: float64 not registered")
let get_cmp_type env =
match env.retroknowledge.retro_cmp with
| Some (((mindcmp,_),_),_,_) ->
Constant.make (MutInd.user mindcmp) (MutInd.canonical mindcmp)
| None -> anomaly Pp.(str"Reduction of primitive: comparison 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")
let get_f_cmp_constructors env =
match env.retroknowledge.retro_f_cmp with
| Some r -> r
| None -> anomaly Pp.(str"Reduction of primitive: fcmp not registered")
let get_f_class_constructors env =
match env.retroknowledge.retro_f_class with
| Some r -> r
| None -> anomaly Pp.(str"Reduction of primitive: fclass not registered")
exception NativeDestKO
module type RedNativeEntries =
sig
type elem
type args
type evd
type uinstance
val get : args -> int -> elem
val get_int : evd -> elem -> Uint63.t
val get_float : evd -> elem -> Float64.t
val get_parray : evd -> elem -> elem Parray.t
val mkInt : env -> Uint63.t -> elem
val mkFloat : env -> Float64.t -> elem
val mkBool : env -> bool -> elem
val mkCarry : env -> bool -> elem -> elem
val mkIntPair : env -> elem -> elem -> elem
val mkFloatIntPair : env -> elem -> elem -> elem
val mkLt : env -> elem
val mkEq : env -> elem
val mkGt : env -> elem
val mkFLt : env -> elem
val mkFEq : env -> elem
val mkFGt : env -> elem
val mkFNotComparable : env -> elem
val mkPNormal : env -> elem
val mkNNormal : env -> elem
val mkPSubn : env -> elem
val mkNSubn : env -> elem
val mkPZero : env -> elem
val mkNZero : env -> elem
val mkPInf : env -> elem
val mkNInf : env -> elem
val mkNaN : env -> elem
val mkArray : env -> uinstance -> elem Parray.t -> elem -> elem
end
module type RedNative =
sig
type elem
type args
type evd
type uinstance
val red_prim : env -> evd -> CPrimitives.t -> uinstance -> args -> elem option
end
module RedNative (E:RedNativeEntries) :
RedNative with type elem = E.elem
with type args = E.args
with type evd = E.evd
with type uinstance = E.uinstance =
struct
type elem = E.elem
type args = E.args
type evd = E.evd
type uinstance = E.uinstance
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 get_float evd args i = E.get_float evd (E.get args i)
let get_float1 evd args = get_float evd args 0
let get_float2 evd args = get_float evd args 0, get_float evd args 1
let get_parray evd args i = E.get_parray evd (E.get args i)
let red_prim_aux env evd op u 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)
| Int63divs ->
let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.divs i1 i2)
| Int63mods ->
let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.rems 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)
| Int63asr ->
let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.a_sr 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)
| Int63lts ->
let i1, i2 = get_int2 evd args in
E.mkBool env (Uint63.lts i1 i2)
| Int63les ->
let i1, i2 = get_int2 evd args in
E.mkBool env (Uint63.les 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
| Int63compares ->
let i1, i2 = get_int2 evd args in
begin match Uint63.compares i1 i2 with
| x when x < 0 -> E.mkLt env
| 0 -> E.mkEq env
| _ -> E.mkGt env
end
| Float64opp ->
let f = get_float1 evd args in E.mkFloat env (Float64.opp f)
| Float64abs ->
let f = get_float1 evd args in E.mkFloat env (Float64.abs f)
| Float64eq ->
let i1, i2 = get_float2 evd args in
E.mkBool env (Float64.eq i1 i2)
| Float64lt ->
let i1, i2 = get_float2 evd args in
E.mkBool env (Float64.lt i1 i2)
| Float64le ->
let i1, i2 = get_float2 evd args in
E.mkBool env (Float64.le i1 i2)
| Float64compare ->
let f1, f2 = get_float2 evd args in
(match Float64.compare f1 f2 with
| Float64.FEq -> E.mkFEq env
| Float64.FLt -> E.mkFLt env
| Float64.FGt -> E.mkFGt env
| Float64.FNotComparable -> E.mkFNotComparable env)
| Float64equal ->
let f1, f2 = get_float2 evd args in
E.mkBool env (Float64.equal f1 f2)
| Float64classify ->
let f = get_float1 evd args in
(match Float64.classify f with
| Float64.PNormal -> E.mkPNormal env
| Float64.NNormal -> E.mkNNormal env
| Float64.PSubn -> E.mkPSubn env
| Float64.NSubn -> E.mkNSubn env
| Float64.PZero -> E.mkPZero env
| Float64.NZero -> E.mkNZero env
| Float64.PInf -> E.mkPInf env
| Float64.NInf -> E.mkNInf env
| Float64.NaN -> E.mkNaN env)
| Float64add ->
let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.add f1 f2)
| Float64sub ->
let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.sub f1 f2)
| Float64mul ->
let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.mul f1 f2)
| Float64div ->
let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.div f1 f2)
| Float64sqrt ->
let f = get_float1 evd args in E.mkFloat env (Float64.sqrt f)
| Float64ofUint63 ->
let i = get_int1 evd args in E.mkFloat env (Float64.of_uint63 i)
| Float64normfr_mantissa ->
let f = get_float1 evd args in E.mkInt env (Float64.normfr_mantissa f)
| Float64frshiftexp ->
let f = get_float1 evd args in
let (m,e) = Float64.frshiftexp f in
E.mkFloatIntPair env (E.mkFloat env m) (E.mkInt env e)
| Float64ldshiftexp ->
let f = get_float evd args 0 in
let e = get_int evd args 1 in
E.mkFloat env (Float64.ldshiftexp f e)
| Float64next_up ->
let f = get_float1 evd args in E.mkFloat env (Float64.next_up f)
| Float64next_down ->
let f = get_float1 evd args in E.mkFloat env (Float64.next_down f)
| Arraymake ->
let ty = E.get args 0 in
let i = get_int evd args 1 in
let d = E.get args 2 in
E.mkArray env u (Parray.make i d) ty
| Arrayget ->
let t = get_parray evd args 1 in
let i = get_int evd args 2 in
Parray.get t i
| Arraydefault ->
let t = get_parray evd args 1 in
Parray.default t
| Arrayset ->
let ty = E.get args 0 in
let t = get_parray evd args 1 in
let i = get_int evd args 2 in
let a = E.get args 3 in
let t' = Parray.set t i a in
E.mkArray env u t' ty
| Arraycopy ->
let ty = E.get args 0 in
let t = get_parray evd args 1 in
let t' = Parray.copy t in
E.mkArray env u t' ty
| Arraylength ->
let t = get_parray evd args 1 in
E.mkInt env (Parray.length t)
let red_prim env evd p u args =
try
let r =
red_prim_aux env evd p u args
in Some r
with NativeDestKO -> None
end