diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2015-10-09 13:04:56 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-09 17:40:56 +0200 |
commit | c47b205206d832430fa80a3386be80149e281d33 (patch) | |
tree | a0556d85855e068235c5d91d2e909bf0a048a472 /kernel | |
parent | 7c82718f18afa3b317873f756a8801774ef64061 (diff) |
Code cleaning in VM (with Benjamin).
Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/byterun/coq_memory.c | 14 | ||||
-rw-r--r-- | kernel/byterun/coq_values.h | 13 | ||||
-rw-r--r-- | kernel/vconv.ml | 22 | ||||
-rw-r--r-- | kernel/vm.ml | 110 | ||||
-rw-r--r-- | kernel/vm.mli | 14 |
5 files changed, 40 insertions, 133 deletions
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 8d03829ab..416e5e532 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -26,7 +26,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size; value coq_global_data; -int coq_all_transp; value coq_atom_tbl; int drawinstr; @@ -117,7 +116,6 @@ value init_coq_vm(value unit) /* ML */ init_coq_global_data(Coq_global_data_Size); init_coq_atom_tbl(40); /* Initialing the interpreter */ - coq_all_transp = 0; init_coq_interpreter(); /* Some predefined pointer code */ @@ -207,18 +205,6 @@ value realloc_coq_atom_tbl(value size) /* ML */ return Val_unit; } - -value coq_set_transp_value(value transp) -{ - coq_all_transp = (transp == Val_true); - return Val_unit; -} - -value get_coq_transp_value(value unit) -{ - return Val_bool(coq_all_transp); -} - value coq_set_drawinstr(value unit) { drawinstr = 1; diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 1590a2141..80100da71 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -20,13 +20,12 @@ #define ATOM_ID_TAG 0 -#define ATOM_IDDEF_TAG 1 -#define ATOM_INDUCTIVE_TAG 2 -#define ATOM_PROJ_TAG 3 -#define ATOM_FIX_TAG 4 -#define ATOM_SWITCH_TAG 5 -#define ATOM_COFIX_TAG 6 -#define ATOM_COFIXEVALUATED_TAG 7 +#define ATOM_INDUCTIVE_TAG 1 +#define ATOM_PROJ_TAG 2 +#define ATOM_FIX_TAG 3 +#define ATOM_SWITCH_TAG 4 +#define ATOM_COFIX_TAG 5 +#define ATOM_COFIXEVALUATED_TAG 6 diff --git a/kernel/vconv.ml b/kernel/vconv.ml index a03a67db8..8af2efc58 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -76,11 +76,7 @@ and conv_whd env pb k whd1 whd2 cu = | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> conv_atom env pb k a1 stk1 a2 stk2 cu | Vfun _, _ | _, Vfun _ -> - conv_val env CONV (k+1) (eta_whd k whd1) (eta_whd k whd2) cu - | _, Vatom_stk(Aiddef(_,v),stk) -> - conv_whd env pb k whd1 (force_whd v stk) cu - | Vatom_stk(Aiddef(_,v),stk), _ -> - conv_whd env pb k (force_whd v stk) whd2 cu + conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible @@ -97,22 +93,6 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible - | Aiddef(ik1,v1), Aiddef(ik2,v2) -> - begin - try - if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then - conv_stack env k stk1 stk2 cu - else raise NotConvertible - with NotConvertible -> - if oracle_order Univ.out_punivs (oracle_of_infos !infos) - false ik1 ik2 then - conv_whd env pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu - else conv_whd env pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu - end - | Aiddef(ik1,v1), _ -> - conv_whd env pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu - | _, Aiddef(ik2,v2) -> - conv_whd env pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu | Aind _, _ | Aid _, _ -> raise NotConvertible and conv_stack env k stk1 stk2 cu = diff --git a/kernel/vm.ml b/kernel/vm.ml index a822f92eb..4607ad716 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -20,6 +20,12 @@ external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" external offset : Obj.t -> int = "coq_offset" let accu_tag = 0 +let max_atom_tag = 1 +let proj_tag = 2 +let fix_app_tag = 3 +let switch_tag = 4 +let cofix_tag = 5 +let cofix_evaluated_tag = 6 (*******************************************) (* Initalization of the abstract machine ***) @@ -29,9 +35,6 @@ external init_vm : unit -> unit = "init_coq_vm" let _ = init_vm () -external transp_values : unit -> bool = "get_coq_transp_value" -external set_transp_values : bool -> unit = "coq_set_transp_value" - (*******************************************) (* Machine code *** ************************) (*******************************************) @@ -141,7 +144,6 @@ type vswitch = { type atom = | Aid of Vars.id_key - | Aiddef of Vars.id_key * values | Aind of pinductive (* Zippers *) @@ -176,20 +178,20 @@ let rec whd_accu a 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 <= max_atom_tag -> Vatom_stk(Obj.magic at, stk) - | 3 (* proj tag *) -> + | i when Int.equal i proj_tag -> let zproj = Zproj (Obj.obj (Obj.field at 0)) in whd_accu (Obj.field at 1) (zproj :: stk) - | 4 (* fix_app tag *) -> + | i when Int.equal i fix_app_tag -> let fa = Obj.field at 1 in let zfix = Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in whd_accu (Obj.field at 0) (zfix :: stk) - | 5 (* switch tag *) -> + | i when Int.equal i switch_tag -> let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in whd_accu (Obj.field at 0) (zswitch :: stk) - | 6 (* cofix_tag *) -> + | i when Int.equal i cofix_tag -> let vcfx = Obj.obj (Obj.field at 0) in let to_up = Obj.obj a in begin match stk with @@ -197,7 +199,7 @@ let rec whd_accu a stk = | [Zapp args] -> Vcofix(vcfx, to_up, Some args) | _ -> assert false end - | 7 (* cofix_evaluated_tag *) -> + | i when Int.equal i cofix_evaluated_tag -> let vcofix = Obj.obj (Obj.field at 0) in let res = Obj.obj a in begin match stk with @@ -258,6 +260,7 @@ let arg args i = ("Vm.arg size = "^(string_of_int (nargs args))^ " acces "^(string_of_int i)) +(* Apply a value to arguments contained in [vargs] *) let apply_arguments vf vargs = let n = nargs vargs in if Int.equal n 0 then vf @@ -268,13 +271,14 @@ let apply_arguments vf vargs = interprete (fun_code vf) vf (Obj.magic vf) (n - 1) end -let apply_vstack vf vstk = - let n = Array.length vstk in +(* Apply value [vf] to an array of argument values [varray] *) +let apply_varray vf varray = + let n = Array.length varray in if Int.equal n 0 then vf else begin push_ra stop; - push_vstack vstk; + push_vstack varray; interprete (fun_code vf) vf (Obj.magic vf) (n - 1) end @@ -360,14 +364,14 @@ external closure_arity : vfun -> int = "coq_closure_arity" let body_of_vfun k vf = let vargs = mkrel_vstack k 1 in - apply_vstack (Obj.magic vf) vargs + apply_varray (Obj.magic vf) vargs let decompose_vfun2 k vf1 vf2 = let arity = min (closure_arity vf1) (closure_arity vf2) in assert (0 < arity && arity < Sys.max_array_length); let vargs = mkrel_vstack k arity in - let v1 = apply_vstack (Obj.magic vf1) vargs in - let v2 = apply_vstack (Obj.magic vf2) vargs in + let v1 = apply_varray (Obj.magic vf1) vargs in + let v2 = apply_varray (Obj.magic vf2) vargs in arity, v1, v2 (* Functions over fixpoint *) @@ -497,7 +501,7 @@ let reduce_cofix k vcf = 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_varray (Obj.obj e) [|Obj.obj self|] in (Array.init ndef cofix_body, ftyp) @@ -550,62 +554,12 @@ let branch_of_switch k sw = in Array.map eval_branch sw.sw_annot.rtbl - - -(* Evaluation *) - -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 -> - let o = Obj.repr v in - if Obj.is_block o && Obj.tag o = accu_tag then - whd_accu (Obj.repr v) stk - else - let v', stkt = - match stkt with - | Zapp args' :: stkt -> - push_ra stop; - push_arguments args'; - push_val v; - push_arguments args; - let v' = - 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) - (nargs args) in - v', stkt - in - whd_stack v' 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 = - 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 - -let rec force_whd v stk = - match whd_stack v stk with - | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk - | res -> res - - -let rec eta_stack a stk v = +(* Apply the term represented by a under stack stk to argument v *) +(* t = a stk --> t v *) +let rec apply_stack a stk v = match stk with - | [] -> apply_vstack a [|v|] - | Zapp args :: stk -> eta_stack (apply_arguments a args) stk v + | [] -> apply_varray a [|v|] + | Zapp args :: stk -> apply_stack (apply_arguments a args) stk v | Zfix(f,args) :: stk -> let a,stk = match stk with @@ -626,11 +580,11 @@ let rec eta_stack a stk v = interprete (fun_code f) (Obj.magic f) (Obj.magic f) (nargs args) in a, stk in - eta_stack a stk v + apply_stack a stk v | Zswitch sw :: stk -> - eta_stack (apply_switch sw a) stk v + apply_stack (apply_switch sw a) stk v -let eta_whd k whd = +let apply_whd k whd = let v = val_of_rel k in match whd with | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false @@ -649,8 +603,4 @@ let eta_whd k whd = push_val v; interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0 | Vatom_stk(a,stk) -> - eta_stack (val_of_atom a) stk v - - - - + apply_stack (val_of_atom a) stk v diff --git a/kernel/vm.mli b/kernel/vm.mli index d31448ee1..045d02333 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -2,13 +2,10 @@ open Names open Term open Cbytecodes -(** Efficient Virtual Machine *) +(** Debug printing *) val set_drawinstr : unit -> unit -val transp_values : unit -> bool -val set_transp_values : bool -> unit - (** Machine code *) type tcode @@ -25,7 +22,6 @@ type arguments type atom = | Aid of Vars.id_key - | Aiddef of Vars.id_key * values | Aind of pinductive (** Zippers *) @@ -106,10 +102,6 @@ val case_info : vswitch -> case_info val type_of_switch : vswitch -> values val branch_of_switch : int -> vswitch -> (int * values) array -(** Evaluation *) - -val whd_stack : values -> stack -> whd -val force_whd : values -> stack -> whd - -val eta_whd : int -> whd -> values +(** Apply a value *) +val apply_whd : int -> whd -> values |