package coq-core

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
(* Reduction of native operators *)
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 (* will be unit in kernel, evar_map outside *)
    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 (* true if carry *)
    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
OCaml

Innovation. Community. Security.