blob: 905a05fe532ac10baeb6bc7cdc251e2e50de70f7 (
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
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
open Term
type retroknowledge
(** aliased type for clarity purpose*)
type entry = Constr.t
(** the following types correspond to the different "things"
the kernel can learn about.*)
type nat_field =
| NatType
| NatPlus
| NatTimes
type n_field =
| NPositive
| NType
| NTwice
| NTwicePlusOne
| NPhi
| NPhiInv
| NPlus
| NTimes
type int31_field =
| Int31Bits
| Int31Type
| Int31Constructor
| Int31Twice
| Int31TwicePlusOne
| Int31Phi
| Int31PhiInv
| Int31Plus
| Int31PlusC
| Int31PlusCarryC
| Int31Minus
| Int31MinusC
| Int31MinusCarryC
| Int31Times
| Int31TimesC
| Int31Div21
| Int31Div
| Int31Diveucl
| Int31AddMulDiv
| Int31Compare
| Int31Head0
| Int31Tail0
| Int31Lor
| Int31Land
| Int31Lxor
type field =
(** | KEq
| KNat of nat_field
| KN of n_field *)
| KInt31 of string*int31_field
(** This type represent an atomic action of the retroknowledge. It
is stored in the compiled libraries
As per now, there is only the possibility of registering things
the possibility of unregistering or changing the flag is under study *)
type action =
| RKRegister of field*entry
(** initial value for retroknowledge *)
val initial_retroknowledge : retroknowledge
(** Given an identifier id (usually Const _)
and the continuation cont of the bytecode compilation
returns the compilation of id in cont if it has a specific treatment
or raises Not_found if id should be compiled as usual *)
val get_vm_compiling_info : retroknowledge -> entry -> Cbytecodes.comp_env ->
constr array ->
int -> Cbytecodes.bytecodes-> Cbytecodes.bytecodes
(*Given an identifier id (usually Construct _)
and its argument array, returns a function that tries an ad-hoc optimisated
compilation (in the case of the 31-bit integers it means compiling them
directly into an integer)
raises Not_found if id should be compiled as usual, and expectingly
CBytecodes.NotClosed if the term is not a closed constructor pattern
(a constant for the compiler) *)
val get_vm_constant_static_info : retroknowledge -> entry ->
constr array ->
Cbytecodes.structured_constant
(*Given an identifier id (usually Construct _ )
its argument array and a continuation, returns the compiled version
of id+args+cont when id has a specific treatment (in the case of
31-bit integers, that would be the dynamic compilation into integers)
or raises Not_found if id should be compiled as usual *)
val get_vm_constant_dynamic_info : retroknowledge -> entry ->
Cbytecodes.comp_env ->
Cbytecodes.block array ->
int -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes
(** Given a type identifier, this function is used before compiling a match
over this type. In the case of 31-bit integers for instance, it is used
to add the instruction sequence which would perform a dynamic decompilation
in case the argument of the match is not in coq representation *)
val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes
-> Cbytecodes.bytecodes
(** Given a type identifier, this function is used by pretyping/vnorm.ml to
recover the elements of that type from their compiled form if it's non
standard (it is used (and can be used) only when the compiled form
is not a block *)
val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr
val get_native_compiling_info : retroknowledge -> entry -> Nativeinstr.prefix ->
Nativeinstr.lambda array -> Nativeinstr.lambda
val get_native_constant_static_info : retroknowledge -> entry ->
constr array -> Nativeinstr.lambda
val get_native_constant_dynamic_info : retroknowledge -> entry ->
Nativeinstr.prefix -> constructor ->
Nativeinstr.lambda array ->
Nativeinstr.lambda
val get_native_before_match_info : retroknowledge -> entry ->
Nativeinstr.prefix -> constructor ->
Nativeinstr.lambda -> Nativeinstr.lambda
(** the following functions are solely used in Pre_env and Environ to implement
the functions register and unregister (and mem) of Environ *)
val add_field : retroknowledge -> field -> entry -> retroknowledge
val mem : retroknowledge -> field -> bool
(* val remove : retroknowledge -> field -> retroknowledge *)
val find : retroknowledge -> field -> entry
(** Dispatching type for the above [get_*] functions. *)
type reactive_info = {(*information required by the compiler of the VM *)
vm_compiling :
(*fastcomputation flag -> continuation -> result *)
(bool->Cbytecodes.comp_env->constr array ->
int->Cbytecodes.bytecodes->Cbytecodes.bytecodes)
option;
vm_constant_static :
(*fastcomputation flag -> constructor -> args -> result*)
(bool->constr array->Cbytecodes.structured_constant)
option;
vm_constant_dynamic :
(*fastcomputation flag -> constructor -> reloc -> args -> sz -> cont -> result *)
(bool->Cbytecodes.comp_env->Cbytecodes.block array->int->
Cbytecodes.bytecodes->Cbytecodes.bytecodes)
option;
(* fastcomputation flag -> cont -> result *)
vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option;
(* tag (= compiled int for instance) -> result *)
vm_decompile_const : (int -> Term.constr) option;
native_compiling :
(bool -> Nativeinstr.prefix -> Nativeinstr.lambda array ->
Nativeinstr.lambda) option;
native_constant_static :
(bool -> constr array -> Nativeinstr.lambda) option;
native_constant_dynamic :
(bool -> Nativeinstr.prefix -> constructor ->
Nativeinstr.lambda array -> Nativeinstr.lambda) option;
native_before_match : (bool -> Nativeinstr.prefix -> constructor ->
Nativeinstr.lambda -> Nativeinstr.lambda) option
}
val empty_reactive_info : reactive_info
(** Hook to be set after the compiler are installed to dispatch fields
into the above [get_*] functions. *)
val dispatch_hook : (retroknowledge -> entry -> field -> reactive_info) Hook.t
|
