From c47b205206d832430fa80a3386be80149e281d33 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 9 Oct 2015 13:04:56 +0200 Subject: Code cleaning in VM (with Benjamin). Rename some functions, remove dead code related to (previously deprecated, now removed) option Set Boxed Values. --- kernel/vm.ml | 110 ++++++++++++++++------------------------------------------- 1 file changed, 30 insertions(+), 80 deletions(-) (limited to 'kernel/vm.ml') diff --git a/kernel/vm.ml b/kernel/vm.ml index a822f92eb3..4607ad7165 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 -- cgit v1.2.3 From db06a1ddee4c79ea8f6903596284df2f2700ddac Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 9 Oct 2015 13:20:45 +0200 Subject: Complete handling of primitive projections in VM. This commit is a follow-up to a51cce369b9c634a93120092d4c7685a242d55b1 --- kernel/vm.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'kernel/vm.ml') diff --git a/kernel/vm.ml b/kernel/vm.ml index 4607ad7165..29e2ee601d 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -314,6 +314,15 @@ let val_of_str_const str = val_of_obj (obj_of_str_const str) let val_of_atom a = val_of_obj (obj_of_atom a) +let atom_of_proj kn v = + let r = Obj.new_block proj_tag 2 in + Obj.set_field r 0 (Obj.repr kn); + Obj.set_field r 1 (Obj.repr v); + ((Obj.obj r) : atom) + +let val_of_proj kn v = + val_of_atom (atom_of_proj kn v) + module IdKeyHash = struct type t = pconstant tableKey @@ -560,6 +569,7 @@ let rec apply_stack a stk v = match stk with | [] -> apply_varray a [|v|] | Zapp args :: stk -> apply_stack (apply_arguments a args) stk v + | Zproj kn :: stk -> apply_stack (val_of_proj kn a) stk v | Zfix(f,args) :: stk -> let a,stk = match stk with -- cgit v1.2.3 From c1ebc07204c65b4570333748b63a3ef60618b026 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 12 Oct 2015 10:51:08 +0200 Subject: Gather VM tags in Cbytecodes. --- kernel/vm.ml | 8 -------- 1 file changed, 8 deletions(-) (limited to 'kernel/vm.ml') diff --git a/kernel/vm.ml b/kernel/vm.ml index 29e2ee601d..eacd803fd4 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -19,14 +19,6 @@ external set_drawinstr : unit -> unit = "coq_set_drawinstr" 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 ***) (*******************************************) -- cgit v1.2.3 From 7d9331a2a188842a98936278d02177f1a6fa7001 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Sat, 17 Oct 2015 21:40:49 -0700 Subject: Adds support for the virtual machine to perform reduction of universe polymorphic definitions. - This implementation passes universes in separate arguments and does not eagerly instanitate polymorphic definitions. - This means that it pays no cost on monomorphic definitions. --- kernel/vm.ml | 112 +++++++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 94 insertions(+), 18 deletions(-) (limited to 'kernel/vm.ml') diff --git a/kernel/vm.ml b/kernel/vm.ml index eacd803fd4..858f546c60 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -121,12 +121,12 @@ type vswitch = { (* *) (* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *) (* - representation of [accu] : tag_[....] *) -(* -- tag <= 2 : encoding atom type (sorts, free vars, etc.) *) -(* -- 3_[accu|proj name] : a projection blocked by an accu *) -(* -- 4_[accu|fix_app] : a fixpoint blocked by an accu *) -(* -- 5_[accu|vswitch] : a match blocked by an accu *) -(* -- 6_[fcofix] : a cofix function *) -(* -- 7_[fcofix|val] : a cofix function, val represent the value *) +(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *) +(* -- 10_[accu|proj name] : a projection blocked by an accu *) +(* -- 11_[accu|fix_app] : a fixpoint blocked by an accu *) +(* -- 12_[accu|vswitch] : a match blocked by an accu *) +(* -- 13_[fcofix] : a cofix function *) +(* -- 14_[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] *) @@ -136,7 +136,8 @@ type vswitch = { type atom = | Aid of Vars.id_key - | Aind of pinductive + | Aind of inductive + | Atype of Univ.universe (* Zippers *) @@ -159,6 +160,7 @@ type whd = | Vconstr_const of int | Vconstr_block of vblock | Vatom_stk of atom * stack + | Vuniv_level of Univ.universe_level (*************************************************) (* Destructors ***********************************) @@ -199,7 +201,9 @@ let rec whd_accu a stk = | [Zapp args] -> Vcofix(vcofix, res, Some args) | _ -> assert false end - | _ -> assert false + | tg -> + Errors.anomaly + Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg) external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" @@ -212,22 +216,45 @@ let whd_val : values -> whd = if tag = accu_tag then ( if Int.equal (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 Vprod(Obj.obj o)) else if tag = Obj.closure_tag || tag = Obj.infix_tag then - ( match kind_of_closure o with + (match kind_of_closure o with | 0 -> Vfun(Obj.obj o) | 1 -> Vfix(Obj.obj o, None) | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) - else - Vconstr_block(Obj.obj o) - + else + Vconstr_block(Obj.obj o) + +let uni_lvl_val : values -> Univ.universe_level = + fun v -> + let whd = Obj.magic v in + match whd with + | Vuniv_level lvl -> lvl + | _ -> + let pr = + let open Pp in + match whd with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk" + | _ -> assert false + in + Errors.anomaly + Pp.( strbrk "Parsing virtual machine value expected universe level, got " + ++ pr) + (************************************************) -(* Abstrct machine ******************************) +(* Abstract machine *****************************) (************************************************) (* gestion de la pile *) @@ -299,6 +326,8 @@ let rec obj_of_str_const str = Obj.set_field res i (obj_of_str_const args.(i)) done; res + | Const_univ_level l -> Obj.repr (Vuniv_level l) + | Const_type u -> obj_of_atom (Atype u) let val_of_obj o = ((Obj.obj o) : values) @@ -317,11 +346,11 @@ let val_of_proj kn v = module IdKeyHash = struct - type t = pconstant tableKey - let equal = Names.eq_table_key (Univ.eq_puniverses Constant.equal) + type t = constant tableKey + let equal = Names.eq_table_key Constant.equal open Hashset.Combine let hash = function - | ConstKey (c,u) -> combinesmall 1 (Constant.hash c) + | ConstKey c -> combinesmall 1 (Constant.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) end @@ -606,3 +635,50 @@ let apply_whd k whd = interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0 | Vatom_stk(a,stk) -> apply_stack (val_of_atom a) stk v + | Vuniv_level lvl -> assert false + +let instantiate_universe (u : Univ.universe) (stk : stack) : Univ.universe = + match stk with + | [] -> u + | [Zapp args] -> + assert (Univ.LSet.cardinal (Univ.Universe.levels u) = nargs args) ; + let _,mp = Univ.LSet.fold (fun key (i,mp) -> + let u = uni_lvl_val (arg args i) in + (i+1, Univ.LMap.add key (Univ.Universe.make u) mp)) + (Univ.Universe.levels u) + (0,Univ.LMap.empty) in + let subst = Univ.make_subst mp in + Univ.subst_univs_universe subst u + | _ -> + Errors.anomaly Pp.(str "ill-formed universe") + + +let rec pr_atom a = + Pp.(match a with + | Aid c -> str "Aid(" ++ (match c with + | ConstKey c -> Names.pr_con c + | RelKey i -> str "#" ++ int i + | _ -> str "...") ++ str ")" + | Aind (mi,i) -> str "Aind(" ++ Names.pr_mind mi ++ str "#" ++ int i ++ str ")" + | Atype _ -> str "Atype(") +and pr_whd w = + Pp.(match w with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" + | Vuniv_level _ -> assert false) +and pr_stack stk = + Pp.(match stk with + | [] -> str "[]" + | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk) +and pr_zipper z = + Pp.(match z with + | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" + | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" + | Zswitch s -> str "Zswitch(...)" + | Zproj c -> str "Zproj(" ++ Names.pr_con c ++ str ")") -- cgit v1.2.3 From 4f8a9d10123bd8aa4d17853a7248d3b3fe8a3625 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 28 Oct 2015 11:16:24 +0100 Subject: Refine Gregory Malecha's patch on VM and universe polymorphism. - Universes are now represented in the VM by a structured constant containing the global levels. This constant is applied to local level variables if any. - When reading back a universe, we perform the union of these levels and return a [Vsort]. - Fixed a bug: structured constants could contain local universe variables in constructor arguments, which has to be prevented. Was showing up for instance when evaluating [cons _ list (nil _)] with a polymorphic [list] type. - Fixed a bug: polymorphic inductive types can have an empty stack. Was showing up when evaluating [bool] with a polymorphic [bool] type. - Made a few cosmetic changes. Patch written with Benjamin Grégoire. --- kernel/vm.ml | 167 ++++++++++++++++++++++++++++------------------------------- 1 file changed, 80 insertions(+), 87 deletions(-) (limited to 'kernel/vm.ml') diff --git a/kernel/vm.ml b/kernel/vm.ml index 858f546c60..64ddc43766 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -162,16 +162,96 @@ type whd = | Vatom_stk of atom * stack | Vuniv_level of Univ.universe_level +(************************************************) +(* Abstract machine *****************************) +(************************************************) + +(* gestion de la pile *) +external push_ra : tcode -> unit = "coq_push_ra" +external push_val : values -> unit = "coq_push_val" +external push_arguments : arguments -> unit = "coq_push_arguments" +external push_vstack : vstack -> unit = "coq_push_vstack" + + +(* interpreteur *) +external interprete : tcode -> values -> vm_env -> int -> values = + "coq_interprete_ml" + + + +(* 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 + val_of_obj (Obj.field (Obj.repr args) (i+2)) + else invalid_arg + ("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 + else + begin + push_ra stop; + push_arguments vargs; + interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + end + +(* 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 varray; + interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + end + (*************************************************) (* Destructors ***********************************) (*************************************************) +let uni_lvl_val (v : values) : Univ.universe_level = + let whd = Obj.magic v in + match whd with + | Vuniv_level lvl -> lvl + | _ -> + let pr = + let open Pp in + match whd with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk" + | _ -> assert false + in + Errors.anomaly + Pp.( strbrk "Parsing virtual machine value expected universe level, got " + ++ pr) + let rec whd_accu a stk = let stk = if Int.equal (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 Int.equal i type_atom_tag -> + begin match stk with + | [Zapp args] -> + let u = ref (Obj.obj (Obj.field at 0)) in + for i = 0 to nargs args - 1 do + u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) + done; + Vsort (Type !u) + | _ -> assert false + end | i when i <= max_atom_tag -> Vatom_stk(Obj.magic at, stk) | i when Int.equal i proj_tag -> @@ -230,77 +310,6 @@ let whd_val : values -> whd = else Vconstr_block(Obj.obj o) -let uni_lvl_val : values -> Univ.universe_level = - fun v -> - let whd = Obj.magic v in - match whd with - | Vuniv_level lvl -> lvl - | _ -> - let pr = - let open Pp in - match whd with - | Vsort _ -> str "Vsort" - | Vprod _ -> str "Vprod" - | Vfun _ -> str "Vfun" - | Vfix _ -> str "Vfix" - | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk" - | _ -> assert false - in - Errors.anomaly - Pp.( strbrk "Parsing virtual machine value expected universe level, got " - ++ pr) - -(************************************************) -(* Abstract machine *****************************) -(************************************************) - -(* gestion de la pile *) -external push_ra : tcode -> unit = "coq_push_ra" -external push_val : values -> unit = "coq_push_val" -external push_arguments : arguments -> unit = "coq_push_arguments" -external push_vstack : vstack -> unit = "coq_push_vstack" - - -(* interpreteur *) -external interprete : tcode -> values -> vm_env -> int -> values = - "coq_interprete_ml" - - - -(* 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 - val_of_obj (Obj.field (Obj.repr args) (i+2)) - else invalid_arg - ("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 - else - begin - push_ra stop; - push_arguments vargs; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) - end - -(* 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 varray; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) - end - (**********************************************) (* Constructors *******************************) (**********************************************) @@ -637,22 +646,6 @@ let apply_whd k whd = apply_stack (val_of_atom a) stk v | Vuniv_level lvl -> assert false -let instantiate_universe (u : Univ.universe) (stk : stack) : Univ.universe = - match stk with - | [] -> u - | [Zapp args] -> - assert (Univ.LSet.cardinal (Univ.Universe.levels u) = nargs args) ; - let _,mp = Univ.LSet.fold (fun key (i,mp) -> - let u = uni_lvl_val (arg args i) in - (i+1, Univ.LMap.add key (Univ.Universe.make u) mp)) - (Univ.Universe.levels u) - (0,Univ.LMap.empty) in - let subst = Univ.make_subst mp in - Univ.subst_univs_universe subst u - | _ -> - Errors.anomaly Pp.(str "ill-formed universe") - - let rec pr_atom a = Pp.(match a with | Aid c -> str "Aid(" ++ (match c with -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/vm.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/vm.ml') diff --git a/kernel/vm.ml b/kernel/vm.ml index 64ddc43766..7029876438 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*