10
(* Compilation des variables + calcul des variables libres *)
12
(* Dans la machine virtuel il n'y a pas de difference entre les *)
13
(* fonctions et leur environnement *)
15
(* Representation de l'environnements des fonctions : *)
16
(* [clos_t | code | fv1 | fv2 | ... | fvn ] *)
18
(* l'offset pour l'acces au variable libre est 1 (il faut passer le *)
19
(* pointeur de code). *)
20
(* Lors de la compilation, les variables libres sont stock'ees dans *)
21
(* [in_env] dans l'ordre inverse de la representation machine, ceci *)
22
(* permet de rajouter des nouvelles variables dans l'environnememt *)
24
(* Les arguments de la fonction arrive sur la pile dans l'ordre de *)
25
(* l'application : f arg1 ... argn *)
26
(* - la pile est alors : *)
27
(* arg1 : ... argn : extra args : return addr : ... *)
28
(* Dans le corps de la fonction [arg1] est repr'esent'e par le de Bruijn *)
29
(* [n], [argn] par le de Bruijn [1] *)
31
(* Representation des environnements des points fix mutuels : *)
32
(* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *)
33
(* ^<----------offset---------> *)
34
(* type = [Ct1 | .... | Ctn] *)
35
(* Ci est le code correspondant au corps du ieme point fix *)
36
(* Lors de l'evaluation d'un point fix l'environnement est un pointeur *)
37
(* sur la position correspondante a son code. *)
38
(* Dans le corps de chaque point fix le de Bruijn [nbr] represente, *)
39
(* le 1er point fix de la declaration mutuelle, le de Bruijn [1] le *)
41
(* L'acces a ces variables se fait par l'instruction [Koffsetclosure] *)
42
(* (decalage de l'environnement) *)
44
(* Ceci permet de representer tout les point fix mutuels en un seul bloc *)
45
(* [Ct1 | ... | Ctn] est un tableau contant le code d'evaluation des *)
46
(* types des points fixes, ils sont utilises pour tester la conversion *)
47
(* Leur environnement d'execution est celui du dernier point fix : *)
48
(* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *)
52
(* Representation des cofix mutuels : *)
53
(* a1 = [A_t | accumulate | [Cfx_t | fcofix1 ] ] *)
55
(* anbr = [A_t | accumulate | [Cfx_t | fcofixnbr ] ] *)
57
(* fcofix1 = [clos_t | code1 | a1 |...| anbr | fv1 |...| fvn | type] *)
60
(* fcofixnbr = [clos_t | codenbr | a1 |...| anbr | fv1 |...| fvn | type] *)
62
(* Les block [ai] sont des fonctions qui accumulent leurs arguments : *)
63
(* ai arg1 argp ---> *)
64
(* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *)
65
(* Si un tel bloc arrive sur un [match] il faut forcer l'evaluation, *)
66
(* la fonction [fcofixi] est alors appliqu'ee a [ai'] [arg1] ... [argp] *)
67
(* A la fin de l'evaluation [ai'] est mis a jour avec le resultat de *)
70
(* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *)
71
(* L'avantage de cette representation est qu'elle permet d'evaluer qu'une *)
72
(* fois l'application d'un cofix (evaluation lazy) *)
73
(* De plus elle permet de creer facilement des cycles quand les cofix ne *)
74
(* n'ont pas d'aruments, ex: *)
75
(* cofix one := cons 1 one *)
76
(* a1 = [A_t | accumulate | [Cfx_t|fcofix1] ] *)
77
(* fcofix1 = [clos_t | code | a1] *)
78
(* Quand on force l'evaluation de [a1] le resultat est *)
79
(* [cons_t | 1 | a1] *)
80
(* [a1] est mis a jour : *)
81
(* a1 = [A_t | accumulate | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ] *)
82
(* Le cycle est cree ... *)
84
(* On conserve la fct de cofix pour la conversion *)
87
let empty_fv = { size= 0; fv_rev = [] }
89
let fv r = !(r.in_env)
91
let empty_comp_env ()=
97
in_env = ref empty_fv;
100
(*i Creation functions for comp_env *)
102
let rec add_param n sz l =
103
if n = 0 then l else add_param (n - 1) sz (n+sz::l)
105
let comp_env_fun arity =
107
in_stack = add_param arity 0 [];
111
in_env = ref empty_fv
115
let comp_env_type rfv =
124
let comp_env_fix ndef curr_pos arity rfv =
126
for i = ndef downto 1 do
127
prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec
130
in_stack = add_param arity 0 [];
133
offset = 2 * (ndef - curr_pos - 1)+1;
137
let comp_env_cofix ndef arity rfv =
140
prec := Kenvacc i :: !prec
143
in_stack = add_param arity 0 [];
150
(* [push_param ] ajoute les parametres de fonction dans la pile *)
151
let push_param n sz r =
153
nb_stack = r.nb_stack + n;
154
in_stack = add_param n sz r.in_stack }
156
(* [push_local e sz] ajoute une nouvelle variable dans la pile a la *)
158
let push_local sz r =
160
nb_stack = r.nb_stack + 1;
161
in_stack = (sz + 1) :: r.in_stack }
165
(*i Compilation of variables *)
167
let rec aux n = function
168
| [] -> raise Not_found
169
| hd :: tl -> if hd = el then n else aux (n+1) tl
173
let env = !(r.in_env) in
174
let cid = FVnamed id in
175
try Kenvacc(r.offset + env.size - (find_at cid env.fv_rev))
177
let pos = env.size in
178
r.in_env := { size = pos+1; fv_rev = cid:: env.fv_rev};
179
Kenvacc (r.offset + pos)
182
if i <= r.nb_stack then
183
Kacc(sz - (List.nth r.in_stack (i-1)))
185
let i = i - r.nb_stack in
186
if i <= r.nb_rec then
187
try List.nth r.pos_rec (i-1)
188
with _ -> assert false
190
let i = i - r.nb_rec in
192
let env = !(r.in_env) in
193
try Kenvacc(r.offset + env.size - (find_at db env.fv_rev))
195
let pos = env.size in
196
r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev};
197
Kenvacc(r.offset + pos)
199
(*i Examination of the continuation *)
201
(* Discard all instructions up to the next label. *)
202
(* This function is to be applied to the continuation before adding a *)
203
(* non-terminating instruction (branch, raise, return, appterm) *)
204
(* in front of it. *)
206
let rec discard_dead_code cont = cont
209
| (Klabel _ | Krestart ) :: _ as cont -> cont
210
| _ :: cont -> discard_dead_code cont
213
(* Return a label to the beginning of the given continuation. *)
214
(* If the sequence starts with a branch, use the target of that branch *)
215
(* as the label, thus avoiding a jump to a jump. *)
217
let label_code = function
218
| Klabel lbl :: _ as cont -> (lbl, cont)
219
| Kbranch lbl :: _ as cont -> (lbl, cont)
220
| cont -> let lbl = Label.create() in (lbl, Klabel lbl :: cont)
222
(* Return a branch to the continuation. That is, an instruction that,
223
when executed, branches to the continuation or performs what the
224
continuation performs. We avoid generating branches to returns. *)
225
(* spiwack: make_branch was only used once. Changed it back to the ZAM
226
one to match the appropriate semantics (old one avoided the
227
introduction of an unconditional branch operation, which seemed
228
appropriate for the 31-bit integers' code). As a memory, I leave
229
the former version in this comment.
230
let make_branch cont =
232
| (Kreturn _ as return) :: cont' -> return, cont'
233
| Klabel lbl as b :: _ -> b, cont
234
| _ -> let b = Klabel(Label.create()) in b,b::cont
237
let rec make_branch_2 lbl n cont =
239
Kreturn m :: _ -> (Kreturn (n + m), cont)
240
| Klabel _ :: c -> make_branch_2 lbl n cont c
241
| Kpop m :: c -> make_branch_2 lbl (n + m) cont c
244
Some lbl -> (Kbranch lbl, cont)
245
| None -> let lbl = Label.create() in (Kbranch lbl, Klabel lbl :: cont)
247
let make_branch cont =
249
(Kbranch _ as branch) :: _ -> (branch, cont)
250
| (Kreturn _ as return) :: _ -> (return, cont)
251
| Klabel lbl :: _ -> make_branch_2 (Some lbl) 0 cont cont
252
| _ -> make_branch_2 (None) 0 cont cont
254
(* Check if we're in tailcall position *)
256
let rec is_tailcall = function
257
| Kreturn k :: _ -> Some k
258
| Klabel _ :: c -> is_tailcall c
261
(* Extention of the continuation *)
263
(* Add a Kpop n instruction in front of a continuation *)
264
let rec add_pop n = function
265
| Kpop m :: cont -> add_pop (n+m) cont
266
| Kreturn m:: cont -> Kreturn (n+m) ::cont
267
| cont -> if n = 0 then cont else Kpop n :: cont
269
let add_grab arity lbl cont =
270
if arity = 1 then Klabel lbl :: cont
271
else Krestart :: Klabel lbl :: Kgrab (arity - 1) :: cont
273
let add_grabrec rec_arg arity lbl cont =
275
Klabel lbl :: Kgrabrec 0 :: Krestart :: cont
277
Krestart :: Klabel lbl :: Kgrabrec rec_arg ::
278
Krestart :: Kgrab (arity - 1) :: cont
280
(* continuation of a cofix *)
282
let cont_cofix arity =
284
(* stk = ai::args::ra::... *)
285
(* ai = [At|accumulate|[Cfx_t|fcofix]|args] *)
287
Kpush; (* stk = res::res::ai::args::ra::... *)
291
Kmakeblock(2, cofix_evaluated_tag);
292
Kpush; (* stk = [Cfxe_t|fcofix|res]::res::ai::args::ra::...*)
294
Ksetfield 1; (* ai = [At|accumulate|[Cfxe_t|fcofix|res]|args] *)
295
(* stk = res::ai::args::ra::... *)
296
Kacc 0; (* accu = res *)
300
(*i Global environment global *)
302
let global_env = ref empty_env
304
let set_global_env env = global_env := env
307
(* Code des fermetures *)
308
let fun_code = ref []
310
let init_fun_code () = fun_code := []
312
(* Compilation des constructeurs et des inductifs *)
314
(* Inv : nparam + arity > 0 *)
315
let code_construct tag nparams arity cont =
319
[Kconst (Const_b0 tag); Kreturn 0]
320
else [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0])
322
let lbl = Label.create() in
323
fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)];
324
Kclosure(lbl,0) :: cont
326
let get_strcst = function
328
| _ -> raise Not_found
331
let rec str_const c =
332
match kind_of_term c with
333
| Sort s -> Bstrconst (Const_sorts s)
334
| Cast(c,_,_) -> str_const c
337
match kind_of_term f with
338
| Construct((kn,j),i) -> (* arnaud: Construct(((kn,j),i) as cstr) -> *)
340
let oib = lookup_mind kn !global_env in
341
let oip = oib.mind_packets.(j) in
342
let num,arity = oip.mind_reloc_tbl.(i-1) in
343
let nparams = oib.mind_nparams in
344
if nparams + arity = Array.length args then
346
(* 1/ tries to compile the constructor in an optimal way,
347
it is supposed to work only if the arguments are
348
all fully constructed, fails with Cbytecodes.NotClosed.
349
it can also raise Not_found when there is no special
350
treatment for this constructor
351
for instance: tries to to compile an integer of the
352
form I31 D1 D2 ... D31 to [D1D2...D31] as
353
a processor number (a caml number actually) *)
356
Bstrconst (Retroknowledge.get_vm_constant_static_info
357
(!global_env).retroknowledge
358
(kind_of_term f) args)
360
(* 2/ if the arguments are not all closed (this is
361
expectingly (and it is currently the case) the only
362
reason why this exception is raised) tries to
363
give a clever, run-time behavior to the constructor.
364
Raises Not_found if there is no special treatment
366
this is done in a lazy fashion, using the constructor
367
Bspecial because it needs to know the continuation
368
and such, which can't be done at this time.
369
for instance, for int31: if one of the digit is
370
not closed, it's not impossible that the number
371
gets fully instanciated at run-time, thus to ensure
372
uniqueness of the representation in the vm
373
it is necessary to try and build a caml integer
374
during the execution *)
375
let rargs = Array.sub args nparams arity in
376
let b_args = Array.map str_const rargs in
377
Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
378
(!global_env).retroknowledge
382
(* 3/ if no special behavior is available, then the compiler
383
falls back to the normal behavior *)
384
if arity = 0 then Bstrconst(Const_b0 num)
386
let rargs = Array.sub args nparams arity in
387
let b_args = Array.map str_const rargs in
389
let sc_args = Array.map get_strcst b_args in
390
Bstrconst(Const_bn(num, sc_args))
392
Bmakeblock(num,b_args)
394
let b_args = Array.map str_const args in
395
(* spiwack: tries first to apply the run-time compilation
396
behavior of the constructor, as in 2/ above *)
398
Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
399
(!global_env).retroknowledge
403
Bconstruct_app(num, nparams, arity, b_args)
407
| Ind ind -> Bstrconst (Const_ind ind)
408
| Construct ((kn,j),i) -> (*arnaud: Construct ((kn,j),i as cstr) -> *)
410
(* spiwack: tries first to apply the run-time compilation
411
behavior of the constructor, as in 2/ above *)
413
Bspecial ((Retroknowledge.get_vm_constant_dynamic_info
414
(!global_env).retroknowledge
418
let oib = lookup_mind kn !global_env in
419
let oip = oib.mind_packets.(j) in
420
let num,arity = oip.mind_reloc_tbl.(i-1) in
421
let nparams = oib.mind_nparams in
422
if nparams + arity = 0 then Bstrconst(Const_b0 num)
423
else Bconstruct_app(num,nparams,arity,[||])
427
(* compilation des applications *)
428
let comp_args comp_expr reloc args sz cont =
429
let nargs_m_1 = Array.length args - 1 in
430
let c = ref (comp_expr reloc args.(0) (sz + nargs_m_1) cont) in
431
for i = 1 to nargs_m_1 do
432
c := comp_expr reloc args.(i) (sz + nargs_m_1 - i) (Kpush :: !c)
436
let comp_app comp_fun comp_arg reloc f args sz cont =
437
let nargs = Array.length args in
438
match is_tailcall cont with
440
comp_args comp_arg reloc args sz
442
comp_fun reloc f (sz + nargs)
443
(Kappterm(nargs, k + nargs) :: (discard_dead_code cont)))
446
comp_args comp_arg reloc args sz
447
(Kpush :: (comp_fun reloc f (sz+nargs) (Kapply nargs :: cont)))
449
let lbl,cont1 = label_code cont in
451
(comp_args comp_arg reloc args (sz + 3)
452
(Kpush :: (comp_fun reloc f (sz+3+nargs) (Kapply nargs :: cont1))))
454
(* Compilation des variables libres *)
456
let compile_fv_elem reloc fv sz cont =
458
| FVrel i -> pos_rel i reloc sz :: cont
459
| FVnamed id -> pos_named id reloc :: cont
461
let rec compile_fv reloc l sz cont =
464
| [fvn] -> compile_fv_elem reloc fvn sz cont
466
compile_fv_elem reloc fvn sz
467
(Kpush :: compile_fv reloc tl (sz + 1) cont)
469
(* compilation des constantes *)
471
let rec get_allias env kn =
472
let tps = (lookup_constant kn env).const_body_code in
473
match Cemitcodes.force tps with
474
| BCallias kn' -> get_allias env kn'
478
(* compilation des expressions *)
480
let rec compile_constr reloc c sz cont =
481
match kind_of_term c with
482
| Meta _ -> raise (Invalid_argument "Cbytegen.compile_constr : Meta")
483
| Evar _ -> raise (Invalid_argument "Cbytegen.compile_constr : Evar")
485
| Cast(c,_,_) -> compile_constr reloc c sz cont
487
| Rel i -> pos_rel i reloc sz :: cont
488
| Var id -> pos_named id reloc :: cont
489
| Const kn -> compile_const reloc kn [||] sz cont
490
| Sort _ | Ind _ | Construct _ ->
491
compile_str_cst reloc (str_const c) sz cont
493
| LetIn(_,xb,_,body) ->
494
compile_constr reloc xb sz
496
(compile_constr (push_local sz reloc) body (sz+1) (add_pop 1 cont)))
497
| Prod(id,dom,codom) ->
499
Kpush :: compile_constr reloc dom (sz+1) (Kmakeprod :: cont) in
500
compile_constr reloc (mkLambda(id,dom,codom)) sz cont1
502
let params, body = decompose_lam c in
503
let arity = List.length params in
504
let r_fun = comp_env_fun arity in
505
let lbl_fun = Label.create() in
507
compile_constr r_fun body arity [Kreturn arity] in
508
fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)];
510
compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont)
514
match kind_of_term f with
515
| Construct _ -> compile_str_cst reloc (str_const c) sz cont
516
| Const kn -> compile_const reloc kn args sz cont
517
| _ -> comp_app compile_constr compile_constr reloc f args sz cont
519
| Fix ((rec_args,init),(_,type_bodies,rec_bodies)) ->
520
let ndef = Array.length type_bodies in
521
let rfv = ref empty_fv in
522
let lbl_types = Array.create ndef Label.no in
523
let lbl_bodies = Array.create ndef Label.no in
524
(* Compilation des types *)
525
let env_type = comp_env_type rfv in
526
for i = 0 to ndef - 1 do
529
(compile_constr env_type type_bodies.(i) 0 [Kstop]) in
530
lbl_types.(i) <- lbl;
531
fun_code := [Ksequence(fcode,!fun_code)]
533
(* Compilation des corps *)
534
for i = 0 to ndef - 1 do
535
let params,body = decompose_lam rec_bodies.(i) in
536
let arity = List.length params in
537
let env_body = comp_env_fix ndef i arity rfv in
539
compile_constr env_body body arity [Kreturn arity] in
540
let lbl = Label.create () in
541
lbl_bodies.(i) <- lbl;
542
let fcode = add_grabrec rec_args.(i) arity lbl cont1 in
543
fun_code := [Ksequence(fcode,!fun_code)]
546
compile_fv reloc fv.fv_rev sz
547
(Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont)
549
| CoFix(init,(_,type_bodies,rec_bodies)) ->
550
let ndef = Array.length type_bodies in
551
let lbl_types = Array.create ndef Label.no in
552
let lbl_bodies = Array.create ndef Label.no in
553
(* Compilation des types *)
554
let rfv = ref empty_fv in
555
let env_type = comp_env_type rfv in
556
for i = 0 to ndef - 1 do
559
(compile_constr env_type type_bodies.(i) 0 [Kstop]) in
560
lbl_types.(i) <- lbl;
561
fun_code := [Ksequence(fcode,!fun_code)]
563
(* Compilation des corps *)
564
for i = 0 to ndef - 1 do
565
let params,body = decompose_lam rec_bodies.(i) in
566
let arity = List.length params in
567
let env_body = comp_env_cofix ndef arity rfv in
568
let lbl = Label.create () in
570
compile_constr env_body body (arity+1) (cont_cofix arity) in
572
add_grab (arity+1) lbl cont1 in
573
lbl_bodies.(i) <- lbl;
574
fun_code := [Ksequence(cont2,!fun_code)];
577
compile_fv reloc fv.fv_rev sz
578
(Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont)
580
| Case(ci,t,a,branchs) ->
581
let ind = ci.ci_ind in
582
let mib = lookup_mind (fst ind) !global_env in
583
let oib = mib.mind_packets.(snd ind) in
584
let tbl = oib.mind_reloc_tbl in
585
let lbl_consts = Array.create oib.mind_nb_constant Label.no in
586
let lbl_blocks = Array.create (oib.mind_nb_args+1) Label.no in
587
let branch1,cont = make_branch cont in
588
(* Compilation du type *)
590
label_code (compile_constr reloc t sz [Kpop sz; Kstop])
591
in fun_code := [Ksequence(fcode,!fun_code)];
592
(* Compilation des branches *)
593
let lbl_sw = Label.create () in
594
let sz_b,branch,is_tailcall =
596
| Kreturn k -> assert (k = sz); sz, branch1, true
597
| _ -> sz+3, Kjump, false
599
let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in
600
(* Compilation de la branche accumulate *)
601
let lbl_accu, code_accu =
602
label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch::cont)
604
lbl_blocks.(0) <- lbl_accu;
605
let c = ref code_accu in
606
(* Compilation des branches constructeurs *)
607
for i = 0 to Array.length tbl - 1 do
608
let tag, arity = tbl.(i) in
611
label_code(compile_constr reloc branchs.(i) sz_b (branch :: !c)) in
612
lbl_consts.(tag) <- lbl_b;
615
let args, body = decompose_lam branchs.(i) in
616
let nargs = List.length args in
619
if nargs = arity then
621
compile_constr (push_param arity sz_b reloc)
622
body (sz_b+arity) (add_pop arity (branch :: !c))
624
let sz_appterm = if is_tailcall then sz_b + arity else arity in
626
compile_constr reloc branchs.(i) (sz_b+arity)
627
(Kappterm(arity,sz_appterm) :: !c))
629
lbl_blocks.(tag) <- lbl_b;
632
c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c;
635
(* spiwack : branch1 can't be a lbl anymore it's a Branch instead
636
| Klabel lbl -> Kpush_retaddr lbl :: !c *)
637
| Kbranch lbl -> Kpush_retaddr lbl :: !c
640
compile_constr reloc a sz
642
let entry = Term.Ind ind in
643
Retroknowledge.get_vm_before_match_info (!global_env).retroknowledge
648
and compile_str_cst reloc sc sz cont =
650
| Bconstr c -> compile_constr reloc c sz cont
651
| Bstrconst sc -> Kconst sc :: cont
652
| Bmakeblock(tag,args) ->
653
let nargs = Array.length args in
654
comp_args compile_str_cst reloc args sz (Kmakeblock(nargs,tag) :: cont)
655
| Bconstruct_app(tag,nparams,arity,args) ->
656
if Array.length args = 0 then code_construct tag nparams arity cont
659
(fun _ _ _ cont -> code_construct tag nparams arity cont)
660
compile_str_cst reloc () args sz cont
661
| Bspecial (comp_fx, args) -> comp_fx reloc args sz cont
664
(* spiwack : compilation of constants with their arguments.
665
Makes a special treatment with 31-bit integer addition *)
667
(*arnaud: let code_construct kn cont =
669
let else_lbl = Label.create () in
670
Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
671
Kaddint31:: Kreturn 0:: Klabel else_lbl::
672
(* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*)
673
Kgetglobal (get_allias !global_env kn)::
674
Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
676
let lbl = Label.create () in
677
fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)];
678
Kclosure(lbl, 0)::cont
680
fun reloc-> fun kn -> fun args -> fun sz -> fun cont ->
681
let nargs = Array.length args in
682
(* spiwack: checks if there is a specific way to compile the constant
683
if there is not, Not_found is raised, and the function
684
falls back on its normal behavior *)
686
Retroknowledge.get_vm_compiling_info (!global_env).retroknowledge
687
(kind_of_term (mkConst kn)) reloc args sz cont
690
Kgetglobal (get_allias !global_env kn) :: cont
692
comp_app (fun _ _ _ cont ->
693
Kgetglobal (get_allias !global_env kn) :: cont)
694
compile_constr reloc () args sz cont
699
Label.reset_label_counter ();
700
let reloc = empty_comp_env () in
701
let init_code = compile_constr reloc c 0 [Kstop] in
702
let fv = List.rev (!(reloc.in_env).fv_rev) in
703
(* draw_instr init_code;
704
draw_instr !fun_code;
705
Format.print_string "fv = ";
708
| FVnamed id -> Format.print_string ((string_of_id id)^"; ")
709
| FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv; Format
711
Format.print_flush(); *)
712
init_code,!fun_code, Array.of_list fv
714
let compile_constant_body env body opaque boxed =
715
if opaque then BCconstant
719
let body = Declarations.force sb in
721
let res = compile env body in
722
let to_patch = to_memory res in
723
BCdefined(true, to_patch)
725
match kind_of_term body with
726
| Const kn' -> BCallias (get_allias env kn')
728
let res = compile env body in
729
let to_patch = to_memory res in
730
BCdefined (false, to_patch)
733
(* spiwack: additional function which allow different part of compilation of the
736
let make_areconst n else_lbl cont =
740
Kareconst (n, else_lbl)::cont
743
(* try to compile int31 as a const_b0. Succeed if all the arguments are closed
744
fails otherwise by raising NotClosed*)
745
let compile_structured_int31 fc args =
746
if not fc then raise Not_found else
749
(fun temp_i -> fun t -> match kind_of_term t with
750
| Construct (_,d) -> 2*temp_i+d-1
751
| _ -> raise NotClosed)
755
(* this function is used for the compilation of the constructor of
756
the int31, it is used when it appears not fully applied, or
757
applied to at least one non-closed digit *)
758
let dynamic_int31_compilation fc reloc args sz cont =
759
if not fc then raise Not_found else
760
let nargs = Array.length args in
762
let (escape,labeled_cont) = make_branch cont in
763
let else_lbl = Label.create() in
764
comp_args compile_str_cst reloc args sz
765
( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont)
767
let code_construct cont = (* spiwack: variant of the global code_construct
768
which handles dynamic compilation of
771
let else_lbl = Label.create () in
772
[Kacc 0; Kpop 1; Kisconst else_lbl; Kareconst(30,else_lbl);
773
Kcompint31; Kreturn 0; Klabel else_lbl; Kmakeblock(31, 1); Kreturn 0]
775
let lbl = Label.create() in
776
fun_code := [Ksequence (add_grab 31 lbl f_cont,!fun_code)];
777
Kclosure(lbl,0) :: cont
782
comp_app (fun _ _ _ cont -> code_construct cont)
783
compile_str_cst reloc () args sz cont
785
(*(* template compilation for 2ary operation, it probably possible
786
to make a generic such function with arity abstracted *)
787
let op2_compilation op =
788
let code_construct normal cont = (*kn cont =*)
790
let else_lbl = Label.create () in
791
Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
792
op:: Kreturn 0:: Klabel else_lbl::
793
(* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*)
794
(*Kgetglobal (get_allias !global_env kn):: *)
796
Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
798
let lbl = Label.create () in
799
fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)];
800
Kclosure(lbl, 0)::cont
802
fun normal fc _ reloc args sz cont ->
803
if not fc then raise Not_found else
804
let nargs = Array.length args in
805
if nargs=2 then (*if it is a fully applied addition*)
806
let (escape, labeled_cont) = make_branch cont in
807
let else_lbl = Label.create () in
808
comp_args compile_constr reloc args sz
809
(Kisconst else_lbl::(make_areconst 1 else_lbl
810
(*Kaddint31::escape::Klabel else_lbl::Kpush::*)
811
(op::escape::Klabel else_lbl::Kpush::
812
(* works as comp_app with nargs = 2 and non-tailcall cont*)
813
(*Kgetglobal (get_allias !global_env kn):: *)
815
Kapply 2::labeled_cont)))
817
code_construct normal cont
819
comp_app (fun _ _ _ cont -> code_construct normal cont)
820
compile_constr reloc () args sz cont *)
822
(*template for n-ary operation, invariant: n>=1,
823
the operations does the following :
824
1/ checks if all the arguments are constants (i.e. non-block values)
825
2/ if they are, uses the "op" instruction to execute
826
3/ if at least one is not, branches to the normal behavior:
827
Kgetglobal (get_allias !global_env kn) *)
828
let op_compilation n op =
829
let code_construct kn cont =
831
let else_lbl = Label.create () in
832
Kareconst(n, else_lbl):: Kacc 0:: Kpop 1::
833
op:: Kreturn 0:: Klabel else_lbl::
834
(* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*)
835
Kgetglobal (get_allias !global_env kn)::
836
Kappterm(n, n):: [] (* = discard_dead_code [Kreturn 0] *)
838
let lbl = Label.create () in
839
fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)];
840
Kclosure(lbl, 0)::cont
842
fun kn fc reloc args sz cont ->
843
if not fc then raise Not_found else
844
let nargs = Array.length args in
845
if nargs=n then (*if it is a fully applied addition*)
846
let (escape, labeled_cont) = make_branch cont in
847
let else_lbl = Label.create () in
848
comp_args compile_constr reloc args sz
849
(Kisconst else_lbl::(make_areconst (n-1) else_lbl
850
(*Kaddint31::escape::Klabel else_lbl::Kpush::*)
851
(op::escape::Klabel else_lbl::Kpush::
852
(* works as comp_app with nargs = n and non-tailcall cont*)
853
Kgetglobal (get_allias !global_env kn)::
854
Kapply n::labeled_cont)))
856
code_construct kn cont
858
comp_app (fun _ _ _ cont -> code_construct kn cont)
859
compile_constr reloc () args sz cont
861
let int31_escape_before_match fc cont =
865
let escape_lbl, labeled_cont = label_code cont in
866
(Kisconst escape_lbl)::Kdecompint31::labeled_cont
added
removed
kernel/cbytegen.ml
