From f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 6 Aug 2010 16:15:08 -0400 Subject: Imported Upstream version 8.3~rc1+dfsg --- kernel/cbytegen.ml | 138 +++++++++++++++++++++++++++-------------------------- 1 file changed, 71 insertions(+), 67 deletions(-) (limited to 'kernel/cbytegen.ml') diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index e7859962..0578c7b4 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -7,49 +7,46 @@ open Declarations open Pre_env -(* Compilation des variables + calcul des variables libres *) +(* Compilation of variables + computing free variables *) -(* Dans la machine virtuel il n'y a pas de difference entre les *) -(* fonctions et leur environnement *) +(* The virtual machine doesn't distinguish closures and their environment *) -(* Representation de l'environnements des fonctions : *) +(* Representation of function environments : *) (* [clos_t | code | fv1 | fv2 | ... | fvn ] *) (* ^ *) -(* l'offset pour l'acces au variable libre est 1 (il faut passer le *) -(* pointeur de code). *) -(* Lors de la compilation, les variables libres sont stock'ees dans *) -(* [in_env] dans l'ordre inverse de la representation machine, ceci *) -(* permet de rajouter des nouvelles variables dans l'environnememt *) -(* facilement. *) -(* Les arguments de la fonction arrive sur la pile dans l'ordre de *) -(* l'application : f arg1 ... argn *) -(* - la pile est alors : *) +(* The offset for accessing free variables is 1 (we must skip the code *) +(* pointer). *) +(* While compiling, free variables are stored in [in_env] in order *) +(* opposite to machine representation, so we can add new free variables *) +(* easily (i.e. without changing the position of previous variables) *) +(* Function arguments are on the stack in the same order as the *) +(* application : f arg1 ... argn *) +(* - the stack is then : *) (* arg1 : ... argn : extra args : return addr : ... *) -(* Dans le corps de la fonction [arg1] est repr'esent'e par le de Bruijn *) -(* [n], [argn] par le de Bruijn [1] *) +(* In the function body [arg1] is represented by de Bruijn [n], and *) +(* [argn] by de Bruijn [1] *) -(* Representation des environnements des points fix mutuels : *) +(* Representation of environements of mutual fixpoints : *) (* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *) (* ^<----------offset---------> *) (* type = [Ct1 | .... | Ctn] *) -(* Ci est le code correspondant au corps du ieme point fix *) -(* Lors de l'evaluation d'un point fix l'environnement est un pointeur *) -(* sur la position correspondante a son code. *) -(* Dans le corps de chaque point fix le de Bruijn [nbr] represente, *) -(* le 1er point fix de la declaration mutuelle, le de Bruijn [1] le *) -(* nbr-ieme. *) -(* L'acces a ces variables se fait par l'instruction [Koffsetclosure] *) -(* (decalage de l'environnement) *) - -(* Ceci permet de representer tout les point fix mutuels en un seul bloc *) -(* [Ct1 | ... | Ctn] est un tableau contant le code d'evaluation des *) -(* types des points fixes, ils sont utilises pour tester la conversion *) -(* Leur environnement d'execution est celui du dernier point fix : *) +(* Ci is the code pointer of the i-th body *) +(* At runtime, a fixpoint environment (which is the same as the fixpoint *) +(* itself) is a pointer to the field holding its code pointer. *) +(* In each fixpoint body, de Bruijn [nbr] represents the first fixpoint *) +(* and de Bruijn [1] the last one. *) +(* Access to these variables is performed by the [Koffsetclosure n] *) +(* instruction that shifts the environment pointer of [n] fields. *) + +(* This allows to represent mutual fixpoints in just one block. *) +(* [Ct1 | ... | Ctn] is an array holding code pointers of the fixpoint *) +(* types. They are used in conversion tests (which requires that *) +(* fixpoint types must be convertible). Their environment is the one of *) +(* the last fixpoint : *) (* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *) (* ^ *) - -(* Representation des cofix mutuels : *) +(* Representation of mutual cofix : *) (* a1 = [A_t | accumulate | [Cfx_t | fcofix1 ] ] *) (* ... *) (* anbr = [A_t | accumulate | [Cfx_t | fcofixnbr ] ] *) @@ -59,29 +56,28 @@ open Pre_env (* ... *) (* fcofixnbr = [clos_t | codenbr | a1 |...| anbr | fv1 |...| fvn | type] *) (* ^ *) -(* Les block [ai] sont des fonctions qui accumulent leurs arguments : *) +(* The [ai] blocks are functions that accumulate their arguments: *) (* ai arg1 argp ---> *) (* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *) -(* Si un tel bloc arrive sur un [match] il faut forcer l'evaluation, *) -(* la fonction [fcofixi] est alors appliqu'ee a [ai'] [arg1] ... [argp] *) -(* A la fin de l'evaluation [ai'] est mis a jour avec le resultat de *) -(* l'evaluation : *) +(* If such a block is matched against, we have to force evaluation, *) +(* function [fcofixi] is then applied to [ai'] [arg1] ... [argp] *) +(* Once evaluation is completed [ai'] is updated with the result: *) (* ai' <-- *) (* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *) -(* L'avantage de cette representation est qu'elle permet d'evaluer qu'une *) -(* fois l'application d'un cofix (evaluation lazy) *) -(* De plus elle permet de creer facilement des cycles quand les cofix ne *) -(* n'ont pas d'aruments, ex: *) +(* This representation is nice because the application of the cofix is *) +(* evaluated only once (it simulates a lazy evaluation) *) +(* Moreover, when cofix don't have arguments, it is possible to create *) +(* a cycle, e.g.: *) (* cofix one := cons 1 one *) (* a1 = [A_t | accumulate | [Cfx_t|fcofix1] ] *) (* fcofix1 = [clos_t | code | a1] *) -(* Quand on force l'evaluation de [a1] le resultat est *) -(* [cons_t | 1 | a1] *) -(* [a1] est mis a jour : *) +(* The result of evaluating [a1] is [cons_t | 1 | a1]. *) +(* When [a1] is updated : *) (* a1 = [A_t | accumulate | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ] *) -(* Le cycle est cree ... *) - -(* On conserve la fct de cofix pour la conversion *) +(* The cycle is created ... *) +(* *) +(* In Cfxe_t accumulators, we need to store [fcofixi] for testing *) +(* conversion of cofixpoints (which is intentional). *) let empty_fv = { size= 0; fv_rev = [] } @@ -112,7 +108,7 @@ let comp_env_fun arity = } -let comp_env_type rfv = +let comp_env_fix_type rfv = { nb_stack = 0; in_stack = []; nb_rec = 0; @@ -134,6 +130,15 @@ let comp_env_fix ndef curr_pos arity rfv = in_env = rfv } +let comp_env_cofix_type ndef rfv = + { nb_stack = 0; + in_stack = []; + nb_rec = 0; + pos_rec = []; + offset = 1+ndef; + in_env = rfv + } + let comp_env_cofix ndef arity rfv = let prec = ref [] in for i = 1 to ndef do @@ -147,14 +152,13 @@ let comp_env_cofix ndef arity rfv = in_env = rfv } -(* [push_param ] ajoute les parametres de fonction dans la pile *) +(* [push_param ] add function parameters on the stack *) let push_param n sz r = { r with nb_stack = r.nb_stack + n; in_stack = add_param n sz r.in_stack } -(* [push_local e sz] ajoute une nouvelle variable dans la pile a la *) -(* position [sz] *) +(* [push_local sz r] add a new variable on the stack at position [sz] *) let push_local sz r = { r with nb_stack = r.nb_stack + 1; @@ -185,7 +189,7 @@ let pos_rel i r sz = let i = i - r.nb_stack in if i <= r.nb_rec then try List.nth r.pos_rec (i-1) - with _ -> assert false + with (Failure _|Invalid_argument _) -> assert false else let i = i - r.nb_rec in let db = FVrel(i) in @@ -297,19 +301,19 @@ let cont_cofix arity = Kreturn (arity+2) ] -(*i Global environment global *) +(*i Global environment *) let global_env = ref empty_env let set_global_env env = global_env := env -(* Code des fermetures *) +(* Code of closures *) let fun_code = ref [] let init_fun_code () = fun_code := [] -(* Compilation des constructeurs et des inductifs *) +(* Compilation of constructors and inductive types *) (* Inv : nparam + arity > 0 *) let code_construct tag nparams arity cont = @@ -424,7 +428,7 @@ let rec str_const c = end | _ -> Bconstr c -(* compilation des applications *) +(* compiling application *) let comp_args comp_expr reloc args sz cont = let nargs_m_1 = Array.length args - 1 in let c = ref (comp_expr reloc args.(0) (sz + nargs_m_1) cont) in @@ -451,7 +455,7 @@ let comp_app comp_fun comp_arg reloc f args sz cont = (comp_args comp_arg reloc args (sz + 3) (Kpush :: (comp_fun reloc f (sz+3+nargs) (Kapply nargs :: cont1)))) -(* Compilation des variables libres *) +(* Compiling free variables *) let compile_fv_elem reloc fv sz cont = match fv with @@ -466,7 +470,7 @@ let rec compile_fv reloc l sz cont = compile_fv_elem reloc fvn sz (Kpush :: compile_fv reloc tl (sz + 1) cont) -(* compilation des constantes *) +(* Compiling constants *) let rec get_allias env kn = let tps = (lookup_constant kn env).const_body_code in @@ -475,7 +479,7 @@ let rec get_allias env kn = | _ -> kn -(* compilation des expressions *) +(* Compiling expressions *) let rec compile_constr reloc c sz cont = match kind_of_term c with @@ -522,7 +526,7 @@ let rec compile_constr reloc c sz cont = let lbl_types = Array.create ndef Label.no in let lbl_bodies = Array.create ndef Label.no in (* Compilation des types *) - let env_type = comp_env_type rfv in + let env_type = comp_env_fix_type rfv in for i = 0 to ndef - 1 do let lbl,fcode = label_code @@ -530,7 +534,7 @@ let rec compile_constr reloc c sz cont = lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; - (* Compilation des corps *) + (* Compiling bodies *) for i = 0 to ndef - 1 do let params,body = decompose_lam rec_bodies.(i) in let arity = List.length params in @@ -550,9 +554,9 @@ let rec compile_constr reloc c sz cont = let ndef = Array.length type_bodies in let lbl_types = Array.create ndef Label.no in let lbl_bodies = Array.create ndef Label.no in - (* Compilation des types *) + (* Compiling types *) let rfv = ref empty_fv in - let env_type = comp_env_type rfv in + let env_type = comp_env_cofix_type ndef rfv in for i = 0 to ndef - 1 do let lbl,fcode = label_code @@ -560,7 +564,7 @@ let rec compile_constr reloc c sz cont = lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; - (* Compilation des corps *) + (* Compiling bodies *) for i = 0 to ndef - 1 do let params,body = decompose_lam rec_bodies.(i) in let arity = List.length params in @@ -585,11 +589,11 @@ let rec compile_constr reloc c sz cont = let lbl_consts = Array.create oib.mind_nb_constant Label.no in let lbl_blocks = Array.create (oib.mind_nb_args+1) Label.no in let branch1,cont = make_branch cont in - (* Compilation du type *) + (* Compiling return type *) let lbl_typ,fcode = label_code (compile_constr reloc t sz [Kpop sz; Kstop]) in fun_code := [Ksequence(fcode,!fun_code)]; - (* Compilation des branches *) + (* Compiling branches *) let lbl_sw = Label.create () in let sz_b,branch,is_tailcall = match branch1 with @@ -597,13 +601,13 @@ let rec compile_constr reloc c sz cont = | _ -> sz+3, Kjump, false in let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in - (* Compilation de la branche accumulate *) + (* Compiling branch for accumulators *) let lbl_accu, code_accu = label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch::cont) in lbl_blocks.(0) <- lbl_accu; let c = ref code_accu in - (* Compilation des branches constructeurs *) + (* Compiling regular constructor branches *) for i = 0 to Array.length tbl - 1 do let tag, arity = tbl.(i) in if arity = 0 then -- cgit v1.2.3