diff options
author | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-22 17:42:45 +0000 |
---|---|---|
committer | bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-22 17:42:45 +0000 |
commit | fff07f8260867740f1f8d8b09bd26baa5f99e5c6 (patch) | |
tree | c222eddef1770307a3d097faa8d928228ef61629 /kernel/cemitcodes.ml | |
parent | 66b674a1d41d9349f4c64543eda5ef005617e3a0 (diff) |
- Ajout d'un cast vm dans la syntaxe : x <: t
Part contre ces cas sont detruis dans les "Definition"
(pas dans les "Lemma") je comprends pas ou ils sont enlev'e...
Si une id'ee ...
- Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland.
- Meilleur compilation des coinductifs, on utilise maintenant vraimment
du lazy.
- Enfin un peu plus de doc dans le code de la vm.
Benjamin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cemitcodes.ml')
-rw-r--r-- | kernel/cemitcodes.ml | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index cccb18443..71a9aa0eb 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -149,8 +149,6 @@ let emit_instr = function out opGRAB; out_int n | Kgrabrec(rec_arg) -> out opGRABREC; out_int rec_arg - | Kcograb n -> - out opCOGRAB; out_int n | Kclosure(lbl, n) -> out opCLOSURE; out_int n; out_label lbl | Kclosurerec(nfv,init,lbl_types,lbl_bodies) -> @@ -160,6 +158,13 @@ let emit_instr = function Array.iter (out_label_with_orig org) lbl_types; let org = !out_position in Array.iter (out_label_with_orig org) lbl_bodies + | Kclosurecofix(nfv,init,lbl_types,lbl_bodies) -> + out opCLOSURECOFIX;out_int (Array.length lbl_bodies); + out_int nfv; out_int init; + let org = !out_position in + Array.iter (out_label_with_orig org) lbl_types; + let org = !out_position in + Array.iter (out_label_with_orig org) lbl_bodies | Kgetglobal q -> out opGETGLOBAL; slot_for_getglobal q | Kconst((Const_b0 i)) -> @@ -178,16 +183,20 @@ let emit_instr = function out opMAKESWITCHBLOCK; out_label typlbl; out_label swlbl; slot_for_annot annot;out_int sz - | Kforce -> - out opFORCE | Kswitch (tbl_const, tbl_block) -> out opSWITCH; out_int (Array.length tbl_const + (Array.length tbl_block lsl 16)); let org = !out_position in Array.iter (out_label_with_orig org) tbl_const; Array.iter (out_label_with_orig org) tbl_block - | Kpushfield n -> - out opPUSHFIELD;out_int n + | Kpushfields n -> + out opPUSHFIELDS;out_int n + | Kfield n -> + if n <= 1 then out (opGETFIELD0+n) + else (out opGETFIELD;out_int n) + | Ksetfield n -> + if n <= 1 then out (opSETFIELD0+n) + else (out opSETFIELD;out_int n) | Kstop -> out opSTOP | Ksequence _ -> raise (Invalid_argument "Cemitcodes.emit_instr") |