diff options
Diffstat (limited to 'kernel/vm.ml')
| -rw-r--r-- | kernel/vm.ml | 138 |
1 files changed, 63 insertions, 75 deletions
diff --git a/kernel/vm.ml b/kernel/vm.ml index 35032c6b..ceb8ea9c 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: vm.ml 13363 2010-07-30 16:17:24Z barras $ *) open Names open Term @@ -16,7 +16,7 @@ open Cbytecodes external set_drawinstr : unit -> unit = "coq_set_drawinstr" (******************************************) -(* Fonctions en plus du module Obj ********) +(* Utility Functions about Obj ************) (******************************************) external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" @@ -25,7 +25,7 @@ external offset : Obj.t -> int = "coq_offset" let accu_tag = 0 (*******************************************) -(* Initalisation de la machine abstraite ***) +(* Initalization of the abstract machine ***) (*******************************************) external init_vm : unit -> unit = "init_coq_vm" @@ -36,15 +36,13 @@ external transp_values : unit -> bool = "get_coq_transp_value" external set_transp_values : bool -> unit = "coq_set_transp_value" (*******************************************) -(* Le code machine ************************) +(* Machine code *** ************************) (*******************************************) type tcode let tcode_of_obj v = ((Obj.obj v):tcode) let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) - - external mkAccuCode : int -> tcode = "coq_makeaccu" external mkPopStopCode : int -> tcode = "coq_pushpop" external mkAccuCond : int -> tcode = "coq_accucond" @@ -73,12 +71,12 @@ let popstop_code i = let stop = popstop_code 0 (******************************************************) -(* Types de donnees abstraites et fonctions associees *) +(* Abstract data types and utility functions **********) (******************************************************) (* Values of the abstract machine *) let val_of_obj v = ((Obj.obj v):values) -let crasy_val = (val_of_obj (Obj.repr 0)) +let crazy_val = (val_of_obj (Obj.repr 0)) (* Abstract data *) type vprod @@ -99,63 +97,60 @@ type vswitch = { sw_env : vm_env } -(* Representation des types abstraits: *) -(* + Les produits : *) +(* Representation of values *) +(* + Products : *) (* - vprod = 0_[ dom | codom] *) (* dom : values, codom : vfun *) (* *) -(* + Les fonctions ont deux representations possibles : *) -(* - fonction non applique : vf = Ct_[ C | fv1 | ... | fvn] *) +(* + Functions have two representations : *) +(* - unapplied fun : vf = Ct_[ C | fv1 | ... | fvn] *) (* C:tcode, fvi : values *) -(* Remarque : il n'y a pas de difference entre la fct et son *) -(* environnement. *) -(* - Application partielle : Ct_[Restart:C| vf | arg1 | ... argn] *) +(* Remark : a function and its environment is the same value. *) +(* - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn] *) (* *) -(* + Les points fixes : *) +(* + Fixpoints : *) (* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *) -(* Remarque il n'y a qu'un seul block pour representer tout les *) -(* points fixes d'une declaration mutuelle, chaque point fixe *) -(* pointe sur la position de son code dans le block. *) -(* - L'application partielle d'un point fixe suit le meme schema *) -(* que celui des fonctions *) -(* Remarque seul les points fixes qui n'ont pas encore recu leur *) -(* argument recursif sont encode de cette maniere (si l'argument *) -(* recursif etait un constructeur le point fixe se serait reduit *) -(* sinon il est represente par un accumulateur) *) +(* One single block to represent all of the fixpoints, each fixpoint *) +(* is the pointer to the field holding the pointer to its code, and *) +(* the infix tag is used to know where the block starts. *) +(* - Partial application follows the scheme of partially applied *) +(* functions. Note: only fixpoints not having been applied to its *) +(* recursive argument are coded this way. When the rec. arg. is *) +(* applied, either it's a constructor and the fix reduces, or it's *) +(* and the fix is coded as an accumulator. *) (* *) -(* + Les cofix sont expliques dans cbytegen.ml *) +(* + Cofixpoints : see cbytegen.ml *) (* *) -(* + Les vblock encodent les constructeurs (non constant) de caml, *) -(* la difference est que leur tag commence a 1 (0 est reserve pour les *) -(* accumulateurs : accu_tag) *) +(* + vblock's encode (non constant) constructors as in Ocaml, but *) +(* starting from 0 up. tag 0 ( = accu_tag) is reserved for *) +(* accumulators. *) (* *) -(* + vm_env est le type des environnement machine (une fct ou un pt fixe) *) +(* + vm_env is the type of the machine environments (i.e. a function or *) +(* a fixpoint) *) (* *) -(* + Les accumulateurs : At_[accumulate| accu | arg1 | ... | argn ] *) -(* - representation des [accu] : tag_[....] *) -(* -- tag <= 2 : encodage du type atom *) -(* -- 3_[accu|fix_app] : un point fixe bloque par un accu *) -(* -- 4_[accu|vswitch] : un case bloque par un accu *) -(* -- 5_[fcofix] : une fonction de cofix *) -(* -- 6_[fcofix|val] : une fonction de cofix, val represente *) -(* la valeur de la reduction de la fct applique a arg1 ... argn *) -(* Le type [arguments] est utiliser de maniere abstraite comme un *) -(* tableau, il represente la structure de donnee suivante : *) +(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *) +(* - representation of [accu] : tag_[....] *) +(* -- tag <= 2 : encoding atom type (sorts, free vars, etc.) *) +(* -- 3_[accu|fix_app] : a fixpoint blocked by an accu *) +(* -- 4_[accu|vswitch] : a match blocked by an accu *) +(* -- 5_[fcofix] : a cofix function *) +(* -- 6_[fcofix|val] : a cofix function, val represent the value *) +(* of the function applied to arg1 ... argn *) +(* The [arguments] type, which is abstracted as an array, represents : *) (* tag[ _ | _ |v1|... | vn] *) -(* Generalement le 1er champs est un pointeur de code *) +(* Generally the first field is a code pointer. *) -(* Ne pas changer ce type sans modifier le code C, *) -(* en particulier le fichier "coq_values.h" *) +(* Do not edit this type without editing C code, especially "coq_values.h" *) type atom = | Aid of id_key | Aiddef of id_key * values | Aind of inductive -(* Les zippers *) +(* Zippers *) type zipper = | Zapp of arguments - | Zfix of vfix*arguments (* Peut-etre vide *) + | Zfix of vfix*arguments (* Possibly empty *) | Zswitch of vswitch type stack = zipper list @@ -193,28 +188,20 @@ let rec whd_accu a stk = let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in whd_accu (Obj.field at 0) (zswitch :: stk) | 5 (* cofix_tag *) -> + let vcfx = Obj.obj (Obj.field at 0) in + let to_up = Obj.obj a in begin match stk with - | [] -> - let vcfx = Obj.obj (Obj.field at 0) in - let to_up = Obj.obj a in - Vcofix(vcfx, to_up, None) - | [Zapp args] -> - let vcfx = Obj.obj (Obj.field at 0) in - let to_up = Obj.obj a in - Vcofix(vcfx, to_up, Some args) + | [] -> Vcofix(vcfx, to_up, None) + | [Zapp args] -> Vcofix(vcfx, to_up, Some args) | _ -> assert false end | 6 (* cofix_evaluated_tag *) -> + let vcofix = Obj.obj (Obj.field at 0) in + let res = Obj.obj a in begin match stk with - | [] -> - let vcofix = Obj.obj (Obj.field at 0) in - let res = Obj.obj a in - Vcofix(vcofix, res, None) - | [Zapp args] -> - let vcofix = Obj.obj (Obj.field at 0) in - let res = Obj.obj a in - Vcofix(vcofix, res, Some args) - | _ -> assert false + | [] -> Vcofix(vcofix, res, None) + | [Zapp args] -> Vcofix(vcofix, res, Some args) + | _ -> assert false end | _ -> assert false @@ -245,7 +232,7 @@ let whd_val : values -> whd = (************************************************) -(* La machine abstraite *************************) +(* Abstrct machine ******************************) (************************************************) (* gestion de la pile *) @@ -291,7 +278,7 @@ let apply_vstack vf vstk = end (**********************************************) -(* Constructeurs ******************************) +(* Constructors *******************************) (**********************************************) let obj_of_atom : atom -> Obj.t = @@ -349,11 +336,11 @@ let mkrel_vstack k arity = let max = k + arity - 1 in Array.init arity (fun i -> val_of_rel (max - i)) + (*************************************************) -(** Operations pour la manipulation des donnees **) +(** Operations manipulating data types ***********) (*************************************************) - (* Functions over products *) let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) @@ -395,13 +382,13 @@ exception FALSE let check_fix f1 f2 = let i1, i2 = current_fix f1, current_fix f2 in - (* Verification du point de depart *) + (* Checking starting point *) if i1 = i2 then let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in let n = Obj.size (last fb1) in - (* Verification du nombre de definition *) + (* Checking number of definitions *) if n = Obj.size (last fb2) then - (* Verification des arguments recursifs *) + (* Checking recursive arguments *) try for i = 0 to n - 1 do if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i @@ -439,14 +426,14 @@ let relaccu_code i = let reduce_fix k vf = let fb = first (Obj.repr vf) in - (* calcul des types *) + (* computing types *) let fc_typ = ((Obj.obj (last fb)) : tcode array) in let ndef = Array.length fc_typ in let et = offset_closure fb (2*(ndef - 1)) in let ftyp = Array.map - (fun c -> interprete c crasy_val (Obj.magic et) 0) fc_typ in - (* Construction de l' environnement des corps des points fixes *) + (fun c -> interprete c crazy_val (Obj.magic et) 0) fc_typ in + (* Construction of the environment of fix bodies *) let e = Obj.dup fb in for i = 0 to ndef - 1 do Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) @@ -485,9 +472,10 @@ let reduce_cofix k vcf = let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in let ndef = Array.length fc_typ in let ftyp = - Array.map (fun c -> interprete c crasy_val (Obj.magic vcf) 0) fc_typ in - (* Construction de l'environnement des corps des cofix *) + (* Evaluate types *) + Array.map (fun c -> interprete c crazy_val (Obj.magic vcf) 0) fc_typ in + (* Construction of the environment of cofix bodies *) let e = Obj.dup (Obj.repr vcf) in for i = 0 to ndef - 1 do Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) @@ -522,7 +510,7 @@ let case_info sw = sw.sw_annot.ci let type_of_switch sw = push_vstack sw.sw_stk; - interprete sw.sw_type_code crasy_val sw.sw_env 0 + interprete sw.sw_type_code crazy_val sw.sw_env 0 let branch_arg k (tag,arity) = if arity = 0 then ((Obj.magic tag):values) |