blob: bbe564d8e7bf00864415ee13d036326c07d91bcf (
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
|
open Names
open Environ
(** {5 Reduction of primitives} *)
val add_retroknowledge : env -> Retroknowledge.action -> env
val get_int_type : env -> Constant.t
val get_float_type : env -> Constant.t
val get_cmp_type : env -> Constant.t
val get_bool_constructors : env -> constructor * constructor
val get_carry_constructors : env -> constructor * constructor
val get_pair_constructor : env -> constructor
val get_cmp_constructors : env -> constructor * constructor * constructor
val get_f_cmp_constructors : env -> constructor * constructor * constructor * constructor
val get_f_class_constructors :
env -> constructor * constructor * constructor * constructor
* constructor * constructor * constructor * constructor
* constructor
exception NativeDestKO (* Should be raised by get_* functions on failure *)
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 get_float : evd -> elem -> Float64.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
end
module type RedNative =
sig
type elem
type args
type evd
val red_prim : env -> evd -> CPrimitives.t -> args -> elem option
end
module RedNative :
functor (E:RedNativeEntries) ->
RedNative with type elem = E.elem
with type args = E.args
with type evd = E.evd
|
