From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- kernel/vm.ml | 176 ++++++++++++++++++++++++++++++----------------------------- 1 file changed, 89 insertions(+), 87 deletions(-) (limited to 'kernel/vm.ml') diff --git a/kernel/vm.ml b/kernel/vm.ml index 4ed0592d..33893625 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vm.ml 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id$ *) open Names open Term @@ -39,11 +39,11 @@ external set_transp_values : bool -> unit = "coq_set_transp_value" (* Le code machine ************************) (*******************************************) -type tcode +type tcode let tcode_of_obj v = ((Obj.obj v):tcode) -let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) +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" @@ -57,21 +57,21 @@ let accumulate = accumulate () external is_accumulate : tcode -> bool = "coq_is_accumulate_code" -let popstop_tbl = ref (Array.init 30 mkPopStopCode) +let popstop_tbl = ref (Array.init 30 mkPopStopCode) let popstop_code i = let len = Array.length !popstop_tbl in - if i < len then !popstop_tbl.(i) + if i < len then !popstop_tbl.(i) else begin popstop_tbl := Array.init (i+10) (fun j -> if j < len then !popstop_tbl.(j) else mkPopStopCode j); - !popstop_tbl.(i) + !popstop_tbl.(i) end let stop = popstop_code 0 - + (******************************************************) (* Types de donnees abstraites et fonctions associees *) (******************************************************) @@ -81,23 +81,23 @@ let val_of_obj v = ((Obj.obj v):values) let crasy_val = (val_of_obj (Obj.repr 0)) (* Abstract data *) -type vprod +type vprod type vfun type vfix type vcofix type vblock type arguments -type vm_env +type vm_env type vstack = values array type vswitch = { - sw_type_code : tcode; - sw_code : tcode; + sw_type_code : tcode; + sw_code : tcode; sw_annot : annot_switch; sw_stk : vstack; sw_env : vm_env - } + } (* Representation des types abstraits: *) (* + Les produits : *) @@ -105,10 +105,10 @@ type vswitch = { (* dom : values, codom : vfun *) (* *) (* + Les fonctions ont deux representations possibles : *) -(* - fonction non applique : vf = Ct_[ C | fv1 | ... | fvn] *) +(* - fonction non applique : vf = Ct_[ C | fv1 | ... | fvn] *) (* C:tcode, fvi : values *) (* Remarque : il n'y a pas de difference entre la fct et son *) -(* environnement. *) +(* environnement. *) (* - Application partielle : Ct_[Restart:C| vf | arg1 | ... argn] *) (* *) (* + Les points fixes : *) @@ -138,7 +138,7 @@ type vswitch = { (* -- 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 *) +(* 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 : *) (* tag[ _ | _ |v1|... | vn] *) @@ -146,7 +146,7 @@ type vswitch = { (* Ne pas changer ce type sans modifier le code C, *) (* en particulier le fichier "coq_values.h" *) -type atom = +type atom = | Aid of id_key | Aiddef of id_key * values | Aind of inductive @@ -164,7 +164,7 @@ type to_up = values type whd = | Vsort of sorts - | Vprod of vprod + | Vprod of vprod | Vfun of vfun | Vfix of vfix * arguments option | Vcofix of vcofix * to_up * arguments option @@ -177,16 +177,16 @@ type whd = (*************************************************) let rec whd_accu a stk = - let stk = + let stk = if Obj.size a = 2 then stk else Zapp (Obj.obj a) :: stk in let at = Obj.field a 1 in match Obj.tag at with - | i when i <= 2 -> + | i when i <= 2 -> Vatom_stk(Obj.magic at, stk) | 3 (* fix_app tag *) -> let fa = Obj.field at 1 in - let zfix = + let zfix = Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in whd_accu (Obj.field at 0) (zfix :: stk) | 4 (* switch tag *) -> @@ -194,7 +194,7 @@ let rec whd_accu a stk = whd_accu (Obj.field at 0) (zswitch :: stk) | 5 (* cofix_tag *) -> 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) @@ -210,7 +210,7 @@ let rec whd_accu a stk = let vcofix = Obj.obj (Obj.field at 0) in let res = Obj.obj a in Vcofix(vcofix, res, None) - | [Zapp args] -> + | [Zapp args] -> let vcofix = Obj.obj (Obj.field at 0) in let res = Obj.obj a in Vcofix(vcofix, res, Some args) @@ -221,18 +221,18 @@ let rec whd_accu a stk = external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" let whd_val : values -> whd = - fun v -> - let o = Obj.repr v in + fun v -> + let o = Obj.repr v in if Obj.is_int o then Vconstr_const (Obj.obj o) - else + else let tag = Obj.tag o in if tag = accu_tag then ( if Obj.size o = 1 then Obj.obj o (* sort *) - else + else if is_accumulate (fun_code o) then whd_accu o [] else (Vprod(Obj.obj o))) - else + else if tag = Obj.closure_tag || tag = Obj.infix_tag then ( match kind_of_closure o with | 0 -> Vfun(Obj.obj o) @@ -241,7 +241,7 @@ let whd_val : values -> whd = | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) | _ -> Util.anomaly "Vm.whd : kind_of_closure does not work") else Vconstr_block(Obj.obj o) - + (************************************************) @@ -263,16 +263,16 @@ external interprete : tcode -> values -> vm_env -> int -> values = (* Functions over arguments *) let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 -let arg args i = - if 0 <= i && i < (nargs args) then +let arg args i = + if 0 <= i && i < (nargs args) then val_of_obj (Obj.field (Obj.repr args) (i+2)) - else raise (Invalid_argument + else raise (Invalid_argument ("Vm.arg size = "^(string_of_int (nargs args))^ " acces "^(string_of_int i))) let apply_arguments vf vargs = let n = nargs vargs in - if n = 0 then vf + if n = 0 then vf else begin push_ra stop; @@ -283,7 +283,7 @@ let apply_arguments vf vargs = let apply_vstack vf vstk = let n = Array.length vstk in if n = 0 then vf - else + else begin push_ra stop; push_vstack vstk; @@ -295,23 +295,23 @@ let apply_vstack vf vstk = (**********************************************) let obj_of_atom : atom -> Obj.t = - fun a -> + fun a -> let res = Obj.new_block accu_tag 2 in Obj.set_field res 0 (Obj.repr accumulate); Obj.set_field res 1 (Obj.repr a); - res + res (* obj_of_str_const : structured_constant -> Obj.t *) let rec obj_of_str_const str = - match str with + match str with | Const_sorts s -> Obj.repr (Vsort s) | Const_ind ind -> obj_of_atom (Aind ind) | Const_b0 tag -> Obj.repr tag | Const_bn(tag, args) -> let len = Array.length args in let res = Obj.new_block tag len in - for i = 0 to len - 1 do - Obj.set_field res i (obj_of_str_const args.(i)) + for i = 0 to len - 1 do + Obj.set_field res i (obj_of_str_const args.(i)) done; res @@ -324,8 +324,8 @@ let val_of_atom a = val_of_obj (obj_of_atom a) let idkey_tbl = Hashtbl.create 31 let val_of_idkey key = - try Hashtbl.find idkey_tbl key - with Not_found -> + try Hashtbl.find idkey_tbl key + with Not_found -> let v = val_of_atom (Aid key) in Hashtbl.add idkey_tbl key v; v @@ -335,14 +335,16 @@ let val_of_rel_def k v = val_of_atom(Aiddef(RelKey k, v)) let val_of_named id = val_of_idkey (VarKey id) let val_of_named_def id v = val_of_atom(Aiddef(VarKey id, v)) - + let val_of_constant c = val_of_idkey (ConstKey c) -let val_of_constant_def n c v = +let val_of_constant_def n c v = let res = Obj.new_block accu_tag 2 in Obj.set_field res 0 (Obj.repr (mkAccuCond n)); Obj.set_field res 1 (Obj.repr (Aiddef(ConstKey c, v))); val_of_obj res +external val_of_annot_switch : annot_switch -> values = "%identity" + let mkrel_vstack k arity = let max = k + arity - 1 in Array.init arity (fun i -> val_of_rel (max - i)) @@ -354,7 +356,7 @@ let mkrel_vstack k arity = (* Functions over products *) -let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) +let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1)) (* Functions over vfun *) @@ -383,7 +385,7 @@ let current_fix vf = - (offset (Obj.repr vf) / 2) let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 - + let rec_args vf = let fb = first (Obj.repr vf) in let size = Obj.size (last fb) in @@ -391,7 +393,7 @@ let rec_args vf = exception FALSE -let check_fix f1 f2 = +let check_fix f1 f2 = let i1, i2 = current_fix f1, current_fix f2 in (* Verification du point de depart *) if i1 = i2 then @@ -407,22 +409,22 @@ let check_fix f1 f2 = done; true with FALSE -> false - else false + else false else false (* Functions over vfix *) external atom_rel : unit -> atom array = "get_coq_atom_tbl" external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl" -let relaccu_tbl = +let relaccu_tbl = let atom_rel = atom_rel() in let len = Array.length atom_rel in for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done; - ref (Array.init len mkAccuCode) + ref (Array.init len mkAccuCode) let relaccu_code i = let len = Array.length !relaccu_tbl in - if i < len then !relaccu_tbl.(i) + if i < len then !relaccu_tbl.(i) else begin realloc_atom_rel i; @@ -432,7 +434,7 @@ let relaccu_code i = relaccu_tbl := Array.init nl (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j); - !relaccu_tbl.(i) + !relaccu_tbl.(i) end let reduce_fix k vf = @@ -441,8 +443,8 @@ let reduce_fix k vf = 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 + 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 *) let e = Obj.dup fb in @@ -455,12 +457,12 @@ let reduce_fix k vf = let res = Obj.new_block Obj.closure_tag 2 in Obj.set_field res 0 (Obj.repr c); Obj.set_field res 1 (offset_closure e (2*i)); - ((Obj.obj res) : vfun) in + ((Obj.obj res) : vfun) in (Array.init ndef fix_body, ftyp) - + (* Functions over vcofix *) -let get_fcofix vcf i = +let get_fcofix vcf i = match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with | Vcofix(vcfi, _, _) -> vcfi | _ -> assert false @@ -482,29 +484,29 @@ let check_cofix vcf1 vcf2 = 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 = + 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 *) - let e = Obj.dup (Obj.repr vcf) in + 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))) + Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) done; - + let cofix_body i = let vcfi = get_fcofix vcf i in let c = Obj.field (Obj.repr vcfi) 0 in - Obj.set_field e 0 c; + Obj.set_field e 0 c; let atom = Obj.new_block cofix_tag 1 in let self = Obj.new_block accu_tag 2 in Obj.set_field self 0 (Obj.repr accumulate); Obj.set_field self 1 (Obj.repr atom); - apply_vstack (Obj.obj e) [|Obj.obj self|] in + apply_vstack (Obj.obj e) [|Obj.obj self|] in (Array.init ndef cofix_body, ftyp) (* Functions over vblock *) - + let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b) let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b) let bfield b i = @@ -514,15 +516,15 @@ let bfield b i = (* Functions over vswitch *) -let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl - +let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl + let case_info sw = sw.sw_annot.ci - -let type_of_switch sw = + +let type_of_switch sw = push_vstack sw.sw_stk; - interprete sw.sw_type_code crasy_val sw.sw_env 0 - -let branch_arg k (tag,arity) = + interprete sw.sw_type_code crasy_val sw.sw_env 0 + +let branch_arg k (tag,arity) = if arity = 0 then ((Obj.magic tag):values) else let b = Obj.new_block tag arity in @@ -533,38 +535,38 @@ let branch_arg k (tag,arity) = let apply_switch sw arg = let tc = sw.sw_annot.tailcall in - if tc then + if tc then (push_ra stop;push_vstack sw.sw_stk) - else + else (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk))); interprete sw.sw_code arg sw.sw_env 0 - + let branch_of_switch k sw = let eval_branch (_,arity as ta) = let arg = branch_arg k ta in let v = apply_switch sw arg in (arity, v) - in + in Array.map eval_branch sw.sw_annot.rtbl - + (* Evaluation *) -let is_accu v = +let is_accu v = let o = Obj.repr v in - Obj.is_block o && Obj.tag o = accu_tag && - fun_code v == accumulate && Obj.tag (Obj.field o 1) < cofix_tag + Obj.is_block o && Obj.tag o = accu_tag && + fun_code v == accumulate && Obj.tag (Obj.field o 1) < cofix_tag -let rec whd_stack v stk = +let rec whd_stack v stk = match stk with | [] -> whd_val v | Zapp args :: stkt -> whd_stack (apply_arguments v args) stkt - | Zfix (f,args) :: stkt -> + | Zfix (f,args) :: stkt -> let o = Obj.repr v in if Obj.is_block o && Obj.tag o = accu_tag then whd_accu (Obj.repr v) stk - else + else let v', stkt = match stkt with | Zapp args' :: stkt -> @@ -573,30 +575,30 @@ let rec whd_stack v stk = push_val v; push_arguments args; let v' = - interprete (fun_code f) (Obj.magic f) (Obj.magic f) + interprete (fun_code f) (Obj.magic f) (Obj.magic f) (nargs args+ nargs args') in v', stkt - | _ -> + | _ -> push_ra stop; push_val v; push_arguments args; let v' = - interprete (fun_code f) (Obj.magic f) (Obj.magic f) + interprete (fun_code f) (Obj.magic f) (Obj.magic f) (nargs args) in v', stkt in whd_stack v' stkt - | Zswitch sw :: stkt -> + | Zswitch sw :: stkt -> let o = Obj.repr v in if Obj.is_block o && Obj.tag o = accu_tag then if Obj.tag (Obj.field o 1) < cofix_tag then whd_accu (Obj.repr v) stk else - let to_up = + let to_up = match whd_accu (Obj.repr v) [] with | Vcofix (_, to_up, _) -> to_up | _ -> assert false in whd_stack (apply_switch sw to_up) stkt - else whd_stack (apply_switch sw v) stkt + else whd_stack (apply_switch sw v) stkt let rec force_whd v stk = match whd_stack v stk with -- cgit v1.2.3