1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: vm.ml 10739 2008-04-01 14:45:20Z herbelin $ *)
16
external set_drawinstr : unit -> unit = "coq_set_drawinstr"
18
(******************************************)
19
(* Fonctions en plus du module Obj ********)
20
(******************************************)
22
external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
23
external offset : Obj.t -> int = "coq_offset"
27
(*******************************************)
28
(* Initalisation de la machine abstraite ***)
29
(*******************************************)
31
external init_vm : unit -> unit = "init_coq_vm"
35
external transp_values : unit -> bool = "get_coq_transp_value"
36
external set_transp_values : bool -> unit = "coq_set_transp_value"
38
(*******************************************)
39
(* Le code machine ************************)
40
(*******************************************)
43
let tcode_of_obj v = ((Obj.obj v):tcode)
44
let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0)
48
external mkAccuCode : int -> tcode = "coq_makeaccu"
49
external mkPopStopCode : int -> tcode = "coq_pushpop"
50
external mkAccuCond : int -> tcode = "coq_accucond"
52
external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode"
53
external int_tcode : tcode -> int -> int = "coq_int_tcode"
55
external accumulate : unit -> tcode = "accumulate_code"
56
let accumulate = accumulate ()
58
external is_accumulate : tcode -> bool = "coq_is_accumulate_code"
60
let popstop_tbl = ref (Array.init 30 mkPopStopCode)
63
let len = Array.length !popstop_tbl in
64
if i < len then !popstop_tbl.(i)
69
(fun j -> if j < len then !popstop_tbl.(j) else mkPopStopCode j);
73
let stop = popstop_code 0
75
(******************************************************)
76
(* Types de donnees abstraites et fonctions associees *)
77
(******************************************************)
79
(* Values of the abstract machine *)
80
let val_of_obj v = ((Obj.obj v):values)
81
let crasy_val = (val_of_obj (Obj.repr 0))
92
type vstack = values array
97
sw_annot : annot_switch;
102
(* Representation des types abstraits: *)
103
(* + Les produits : *)
104
(* - vprod = 0_[ dom | codom] *)
105
(* dom : values, codom : vfun *)
107
(* + Les fonctions ont deux representations possibles : *)
108
(* - fonction non applique : vf = Ct_[ C | fv1 | ... | fvn] *)
109
(* C:tcode, fvi : values *)
110
(* Remarque : il n'y a pas de difference entre la fct et son *)
112
(* - Application partielle : Ct_[Restart:C| vf | arg1 | ... argn] *)
114
(* + Les points fixes : *)
115
(* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *)
116
(* Remarque il n'y a qu'un seul block pour representer tout les *)
117
(* points fixes d'une declaration mutuelle, chaque point fixe *)
118
(* pointe sur la position de son code dans le block. *)
119
(* - L'application partielle d'un point fixe suit le meme schema *)
120
(* que celui des fonctions *)
121
(* Remarque seul les points fixes qui n'ont pas encore recu leur *)
122
(* argument recursif sont encode de cette maniere (si l'argument *)
123
(* recursif etait un constructeur le point fixe se serait reduit *)
124
(* sinon il est represente par un accumulateur) *)
126
(* + Les cofix sont expliques dans cbytegen.ml *)
128
(* + Les vblock encodent les constructeurs (non constant) de caml, *)
129
(* la difference est que leur tag commence a 1 (0 est reserve pour les *)
130
(* accumulateurs : accu_tag) *)
132
(* + vm_env est le type des environnement machine (une fct ou un pt fixe) *)
134
(* + Les accumulateurs : At_[accumulate| accu | arg1 | ... | argn ] *)
135
(* - representation des [accu] : tag_[....] *)
136
(* -- tag <= 2 : encodage du type atom *)
137
(* -- 3_[accu|fix_app] : un point fixe bloque par un accu *)
138
(* -- 4_[accu|vswitch] : un case bloque par un accu *)
139
(* -- 5_[fcofix] : une fonction de cofix *)
140
(* -- 6_[fcofix|val] : une fonction de cofix, val represente *)
141
(* la valeur de la reduction de la fct applique a arg1 ... argn *)
142
(* Le type [arguments] est utiliser de maniere abstraite comme un *)
143
(* tableau, il represente la structure de donnee suivante : *)
144
(* tag[ _ | _ |v1|... | vn] *)
145
(* Generalement le 1er champs est un pointeur de code *)
147
(* Ne pas changer ce type sans modifier le code C, *)
148
(* en particulier le fichier "coq_values.h" *)
151
| Aiddef of id_key * values
158
| Zfix of vfix*arguments (* Peut-etre vide *)
161
type stack = zipper list
169
| Vfix of vfix * arguments option
170
| Vcofix of vcofix * to_up * arguments option
171
| Vconstr_const of int
172
| Vconstr_block of vblock
173
| Vatom_stk of atom * stack
175
(*************************************************)
176
(* Destructors ***********************************)
177
(*************************************************)
179
let rec whd_accu a stk =
181
if Obj.size a = 2 then stk
182
else Zapp (Obj.obj a) :: stk in
183
let at = Obj.field a 1 in
184
match Obj.tag at with
186
Vatom_stk(Obj.magic at, stk)
187
| 3 (* fix_app tag *) ->
188
let fa = Obj.field at 1 in
190
Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
191
whd_accu (Obj.field at 0) (zfix :: stk)
192
| 4 (* switch tag *) ->
193
let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
194
whd_accu (Obj.field at 0) (zswitch :: stk)
195
| 5 (* cofix_tag *) ->
198
let vcfx = Obj.obj (Obj.field at 0) in
199
let to_up = Obj.obj a in
200
Vcofix(vcfx, to_up, None)
202
let vcfx = Obj.obj (Obj.field at 0) in
203
let to_up = Obj.obj a in
204
Vcofix(vcfx, to_up, Some args)
207
| 6 (* cofix_evaluated_tag *) ->
210
let vcofix = Obj.obj (Obj.field at 0) in
211
let res = Obj.obj a in
212
Vcofix(vcofix, res, None)
214
let vcofix = Obj.obj (Obj.field at 0) in
215
let res = Obj.obj a in
216
Vcofix(vcofix, res, Some args)
221
external kind_of_closure : Obj.t -> int = "coq_kind_of_closure"
223
let whd_val : values -> whd =
225
let o = Obj.repr v in
226
if Obj.is_int o then Vconstr_const (Obj.obj o)
228
let tag = Obj.tag o in
229
if tag = accu_tag then
231
if Obj.size o = 1 then Obj.obj o (* sort *)
233
if is_accumulate (fun_code o) then whd_accu o []
234
else (Vprod(Obj.obj o)))
236
if tag = Obj.closure_tag || tag = Obj.infix_tag then
237
( match kind_of_closure o with
238
| 0 -> Vfun(Obj.obj o)
239
| 1 -> Vfix(Obj.obj o, None)
240
| 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
241
| 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
242
| _ -> Util.anomaly "Vm.whd : kind_of_closure does not work")
243
else Vconstr_block(Obj.obj o)
247
(************************************************)
248
(* La machine abstraite *************************)
249
(************************************************)
251
(* gestion de la pile *)
252
external push_ra : tcode -> unit = "coq_push_ra"
253
external push_val : values -> unit = "coq_push_val"
254
external push_arguments : arguments -> unit = "coq_push_arguments"
255
external push_vstack : vstack -> unit = "coq_push_vstack"
259
external interprete : tcode -> values -> vm_env -> int -> values =
264
(* Functions over arguments *)
265
let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
267
if 0 <= i && i < (nargs args) then
268
val_of_obj (Obj.field (Obj.repr args) (i+2))
269
else raise (Invalid_argument
270
("Vm.arg size = "^(string_of_int (nargs args))^
271
" acces "^(string_of_int i)))
273
let apply_arguments vf vargs =
274
let n = nargs vargs in
279
push_arguments vargs;
280
interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
283
let apply_vstack vf vstk =
284
let n = Array.length vstk in
290
interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
293
(**********************************************)
294
(* Constructeurs ******************************)
295
(**********************************************)
297
let obj_of_atom : atom -> Obj.t =
299
let res = Obj.new_block accu_tag 2 in
300
Obj.set_field res 0 (Obj.repr accumulate);
301
Obj.set_field res 1 (Obj.repr a);
304
(* obj_of_str_const : structured_constant -> Obj.t *)
305
let rec obj_of_str_const str =
307
| Const_sorts s -> Obj.repr (Vsort s)
308
| Const_ind ind -> obj_of_atom (Aind ind)
309
| Const_b0 tag -> Obj.repr tag
310
| Const_bn(tag, args) ->
311
let len = Array.length args in
312
let res = Obj.new_block tag len in
313
for i = 0 to len - 1 do
314
Obj.set_field res i (obj_of_str_const args.(i))
318
let val_of_obj o = ((Obj.obj o) : values)
320
let val_of_str_const str = val_of_obj (obj_of_str_const str)
322
let val_of_atom a = val_of_obj (obj_of_atom a)
324
let idkey_tbl = Hashtbl.create 31
326
let val_of_idkey key =
327
try Hashtbl.find idkey_tbl key
329
let v = val_of_atom (Aid key) in
330
Hashtbl.add idkey_tbl key v;
333
let val_of_rel k = val_of_idkey (RelKey k)
334
let val_of_rel_def k v = val_of_atom(Aiddef(RelKey k, v))
336
let val_of_named id = val_of_idkey (VarKey id)
337
let val_of_named_def id v = val_of_atom(Aiddef(VarKey id, v))
339
let val_of_constant c = val_of_idkey (ConstKey c)
340
let val_of_constant_def n c v =
341
let res = Obj.new_block accu_tag 2 in
342
Obj.set_field res 0 (Obj.repr (mkAccuCond n));
343
Obj.set_field res 1 (Obj.repr (Aiddef(ConstKey c, v)));
346
let mkrel_vstack k arity =
347
let max = k + arity - 1 in
348
Array.init arity (fun i -> val_of_rel (max - i))
350
(*************************************************)
351
(** Operations pour la manipulation des donnees **)
352
(*************************************************)
355
(* Functions over products *)
357
let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0)
358
let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1))
360
(* Functions over vfun *)
362
external closure_arity : vfun -> int = "coq_closure_arity"
364
let body_of_vfun k vf =
365
let vargs = mkrel_vstack k 1 in
366
apply_vstack (Obj.magic vf) vargs
368
let decompose_vfun2 k vf1 vf2 =
369
let arity = min (closure_arity vf1) (closure_arity vf2) in
370
assert (0 < arity && arity < Sys.max_array_length);
371
let vargs = mkrel_vstack k arity in
372
let v1 = apply_vstack (Obj.magic vf1) vargs in
373
let v2 = apply_vstack (Obj.magic vf2) vargs in
376
(* Functions over fixpoint *)
378
let first o = (offset_closure o (offset o))
379
let last o = (Obj.field o (Obj.size o - 1))
381
let current_fix vf = - (offset (Obj.repr vf) / 2)
383
let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i))
385
let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1
388
let fb = first (Obj.repr vf) in
389
let size = Obj.size (last fb) in
390
Array.init size (unsafe_rec_arg fb)
394
let check_fix f1 f2 =
395
let i1, i2 = current_fix f1, current_fix f2 in
396
(* Verification du point de depart *)
398
let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in
399
let n = Obj.size (last fb1) in
400
(* Verification du nombre de definition *)
401
if n = Obj.size (last fb2) then
402
(* Verification des arguments recursifs *)
404
for i = 0 to n - 1 do
405
if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i
413
(* Functions over vfix *)
414
external atom_rel : unit -> atom array = "get_coq_atom_tbl"
415
external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl"
418
let atom_rel = atom_rel() in
419
let len = Array.length atom_rel in
420
for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done;
421
ref (Array.init len mkAccuCode)
424
let len = Array.length !relaccu_tbl in
425
if i < len then !relaccu_tbl.(i)
429
let atom_rel = atom_rel () in
430
let nl = Array.length atom_rel in
431
for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done;
434
(fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j);
438
let reduce_fix k vf =
439
let fb = first (Obj.repr vf) in
440
(* calcul des types *)
441
let fc_typ = ((Obj.obj (last fb)) : tcode array) in
442
let ndef = Array.length fc_typ in
443
let et = offset_closure fb (2*(ndef - 1)) in
446
(fun c -> interprete c crasy_val (Obj.magic et) 0) fc_typ in
447
(* Construction de l' environnement des corps des points fixes *)
448
let e = Obj.dup fb in
449
for i = 0 to ndef - 1 do
450
Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i)))
453
let jump_grabrec c = offset_tcode c 2 in
454
let c = jump_grabrec (unsafe_fb_code fb i) in
455
let res = Obj.new_block Obj.closure_tag 2 in
456
Obj.set_field res 0 (Obj.repr c);
457
Obj.set_field res 1 (offset_closure e (2*i));
458
((Obj.obj res) : vfun) in
459
(Array.init ndef fix_body, ftyp)
461
(* Functions over vcofix *)
463
let get_fcofix vcf i =
464
match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with
465
| Vcofix(vcfi, _, _) -> vcfi
468
let current_cofix vcf =
469
let ndef = Obj.size (last (Obj.repr vcf)) in
470
let rec find_cofix pos =
472
if get_fcofix vcf pos == vcf then pos
473
else find_cofix (pos+1)
474
else raise Not_found in
476
with _ -> assert false
478
let check_cofix vcf1 vcf2 =
479
(current_cofix vcf1 = current_cofix vcf2) &&
480
(Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2)))
482
let reduce_cofix k vcf =
483
let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in
484
let ndef = Array.length fc_typ in
486
Array.map (fun c -> interprete c crasy_val (Obj.magic vcf) 0) fc_typ in
487
(* Construction de l'environnement des corps des cofix *)
489
let e = Obj.dup (Obj.repr vcf) in
490
for i = 0 to ndef - 1 do
491
Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i)))
495
let vcfi = get_fcofix vcf i in
496
let c = Obj.field (Obj.repr vcfi) 0 in
498
let atom = Obj.new_block cofix_tag 1 in
499
let self = Obj.new_block accu_tag 2 in
500
Obj.set_field self 0 (Obj.repr accumulate);
501
Obj.set_field self 1 (Obj.repr atom);
502
apply_vstack (Obj.obj e) [|Obj.obj self|] in
503
(Array.init ndef cofix_body, ftyp)
506
(* Functions over vblock *)
508
let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b)
509
let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b)
511
if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i)
512
else raise (Invalid_argument "Vm.bfield")
515
(* Functions over vswitch *)
517
let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl
519
let case_info sw = sw.sw_annot.ci
521
let type_of_switch sw =
522
push_vstack sw.sw_stk;
523
interprete sw.sw_type_code crasy_val sw.sw_env 0
525
let branch_arg k (tag,arity) =
526
if arity = 0 then ((Obj.magic tag):values)
528
let b = Obj.new_block tag arity in
529
for i = 0 to arity - 1 do
530
Obj.set_field b i (Obj.repr (val_of_rel (k+i)))
534
let apply_switch sw arg =
535
let tc = sw.sw_annot.tailcall in
537
(push_ra stop;push_vstack sw.sw_stk)
539
(push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk)));
540
interprete sw.sw_code arg sw.sw_env 0
542
let branch_of_switch k sw =
543
let eval_branch (_,arity as ta) =
544
let arg = branch_arg k ta in
545
let v = apply_switch sw arg in
548
Array.map eval_branch sw.sw_annot.rtbl
555
let o = Obj.repr v in
556
Obj.is_block o && Obj.tag o = accu_tag &&
557
fun_code v == accumulate && Obj.tag (Obj.field o 1) < cofix_tag
559
let rec whd_stack v stk =
562
| Zapp args :: stkt -> whd_stack (apply_arguments v args) stkt
563
| Zfix (f,args) :: stkt ->
564
let o = Obj.repr v in
565
if Obj.is_block o && Obj.tag o = accu_tag then
566
whd_accu (Obj.repr v) stk
570
| Zapp args' :: stkt ->
572
push_arguments args';
576
interprete (fun_code f) (Obj.magic f) (Obj.magic f)
577
(nargs args+ nargs args') in
584
interprete (fun_code f) (Obj.magic f) (Obj.magic f)
589
| Zswitch sw :: stkt ->
590
let o = Obj.repr v in
591
if Obj.is_block o && Obj.tag o = accu_tag then
592
if Obj.tag (Obj.field o 1) < cofix_tag then whd_accu (Obj.repr v) stk
595
match whd_accu (Obj.repr v) [] with
596
| Vcofix (_, to_up, _) -> to_up
597
| _ -> assert false in
598
whd_stack (apply_switch sw to_up) stkt
599
else whd_stack (apply_switch sw v) stkt
601
let rec force_whd v stk =
602
match whd_stack v stk with
603
| Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk
added
removed
kernel/vm.ml
