From fff07f8260867740f1f8d8b09bd26baa5f99e5c6 Mon Sep 17 00:00:00 2001 From: bgregoir Date: Sat, 22 Jul 2006 17:42:45 +0000 Subject: - 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 --- kernel/cbytecodes.ml | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) (limited to 'kernel/cbytecodes.ml') diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 499554746..a9b16f29c 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -3,6 +3,14 @@ open Term type tag = int +let id_tag = 0 +let iddef_tag = 1 +let ind_tag = 2 +let fix_tag = 3 +let switch_tag = 4 +let cofix_tag = 5 +let cofix_evaluated_tag = 6 + type structured_constant = | Const_sorts of sorts | Const_ind of inductive @@ -39,18 +47,20 @@ type instruction = | Krestart | Kgrab of int (* number of arguments *) | Kgrabrec of int (* rec arg *) - | Kcograb of int (* number of arguments *) | Kclosure of Label.t * int (* label, number of free variables *) | Kclosurerec of int * int * Label.t array * Label.t array (* nb fv, init, lbl types, lbl bodies *) + | Kclosurecofix of int * int * Label.t array * Label.t array + (* nb fv, init, lbl types, lbl bodies *) | Kgetglobal of constant | Kconst of structured_constant | Kmakeblock of int * tag (* size, tag *) | Kmakeprod | Kmakeswitchblock of Label.t * Label.t * annot_switch * int - | Kforce | Kswitch of Label.t array * Label.t array (* consts,blocks *) - | Kpushfield of int + | Kpushfields of int + | Kfield of int + | Ksetfield of int | Kstop | Ksequence of bytecodes * bytecodes @@ -79,7 +89,6 @@ let rec instruction ppf = function | Krestart -> fprintf ppf "\trestart" | Kgrab n -> fprintf ppf "\tgrab %i" n | Kgrabrec n -> fprintf ppf "\tgrabrec %i" n - | Kcograb n -> fprintf ppf "\tcograb %i" n | Kclosure(lbl, n) -> fprintf ppf "\tclosure L%i, %i" lbl n | Kclosurerec(fv,init,lblt,lblb) -> @@ -89,7 +98,13 @@ let rec instruction ppf = function Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt; print_string " bodies = "; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; - (* nb fv, init, lbl types, lbl bodies *) + | Kclosurecofix (fv,init,lblt,lblb) -> + fprintf ppf "\tclosurecofix"; + fprintf ppf " %i , %i, " fv init; + print_string "types = "; + Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt; + print_string " bodies = "; + Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id) | Kconst cst -> fprintf ppf "\tconst" @@ -98,13 +113,13 @@ let rec instruction ppf = function | Kmakeprod -> fprintf ppf "\tmakeprod" | Kmakeswitchblock(lblt,lbls,_,sz) -> fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz - | Kforce -> fprintf ppf "\tforce" | Kswitch(lblc,lblb) -> fprintf ppf "\tswitch"; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; - | Kpushfield n -> - fprintf ppf "\tpushfield %i" n + | Kpushfields n -> fprintf ppf "\tpushfields %i" n + | Ksetfield n -> fprintf ppf "\tsetfield %i" n + | Kfield n -> fprintf ppf "\tgetfield %i" n | Kstop -> fprintf ppf "\tstop" | Ksequence (c1,c2) -> fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2 -- cgit v1.2.3