diff options
| -rw-r--r-- | kernel/cbytegen.ml | 4 | ||||
| -rw-r--r-- | kernel/cemitcodes.ml | 5 | ||||
| -rw-r--r-- | kernel/cinstr.mli | 3 | ||||
| -rw-r--r-- | kernel/clambda.ml | 25 | ||||
| -rw-r--r-- | kernel/vmvalues.ml | 70 | ||||
| -rw-r--r-- | kernel/vmvalues.mli | 5 |
6 files changed, 72 insertions, 40 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 4c9ffc891e..6dabfee4ef 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -491,7 +491,9 @@ let rec compile_lam env cenv lam sz cont = match lam with | Lrel(_, i) -> pos_rel i cenv sz :: cont - | Lval v -> compile_structured_constant cenv v sz cont + | Lint i -> compile_structured_constant cenv (Const_b0 i) sz cont + + | Lval v -> compile_structured_constant cenv (Const_val v) sz cont | Lproj (p,arg) -> compile_lam env cenv arg sz (Kproj p :: cont) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index d4e35efa78..50f5607e31 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -358,10 +358,9 @@ let rec emit env insns remaining = match insns with type to_patch = emitcodes * patches * fv (* Substitution *) -let rec subst_strcst s sc = +let subst_strcst s sc = match sc with - | Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc - | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) + | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ -> sc | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) let subst_reloc s ri = diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli index 29bfe4c731..dca1757b7d 100644 --- a/kernel/cinstr.mli +++ b/kernel/cinstr.mli @@ -34,10 +34,11 @@ and lambda = | Lfix of (int array * int) * fix_decl | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of int * lambda array - | Lval of structured_constant + | Lval of structured_values | Lsort of Sorts.t | Lind of pinductive | Lproj of Projection.Repr.t * lambda + | Lint of int | Luint of uint (* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation diff --git a/kernel/clambda.ml b/kernel/clambda.ml index eace0ea13d..cc50e375f4 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -116,6 +116,8 @@ let rec pp_lam lam = hov 1 (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg ++ str ")") + | Lint i -> + Pp.(str "(int:" ++ int i ++ str ")") | Luint _ -> str "(uint)" @@ -151,7 +153,7 @@ let shift subst = subs_shft (1, subst) let rec map_lam_with_binders g f n lam = match lam with - | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam + | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ -> lam | Levar (evk, args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else Levar (evk, args') @@ -350,7 +352,7 @@ let rec occurrence k kind lam = if n = k then if kind then false else raise Not_found else kind - | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> kind + | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ -> kind | Levar (_, args) -> occurrence_args k kind args | Lprod(dom, codom) -> @@ -437,23 +439,22 @@ let check_compilable ib = let is_value lc = match lc with - | Lval _ -> true + | Lval _ | Lint _ -> true | _ -> false let get_value lc = match lc with | Lval v -> v + | Lint i -> val_of_int i | _ -> raise Not_found -let mkConst_b0 n = Lval (Const_b0 n) - let make_args start _end = Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i)) (* Translation of constructors *) let expand_constructor tag nparams arity = let ids = Array.make (nparams + arity) Anonymous in - if arity = 0 then mkLlam ids (mkConst_b0 tag) + if arity = 0 then mkLlam ids (Lint tag) else let args = make_args arity 1 in Llam(ids, Lmakeblock (tag, args)) @@ -464,15 +465,15 @@ let makeblock tag nparams arity args = mkLapp (expand_constructor tag nparams arity) args else (* The constructor is fully applied *) - if arity = 0 then mkConst_b0 tag + if arity = 0 then Lint tag else if Array.for_all is_value args then if tag < last_variant_tag then - Lval(Const_bn(tag, Array.map get_value args)) + Lval(val_of_block tag (Array.map get_value args)) else let args = Array.map get_value args in - let args = Array.append [|Const_b0 (tag - last_variant_tag) |] args in - Lval(Const_bn(last_variant_tag, args)) + let args = Array.append [| val_of_int (tag - last_variant_tag) |] args in + Lval(val_of_block last_variant_tag args) else Lmakeblock(tag, args) @@ -837,8 +838,8 @@ let dynamic_int31_compilation fc args = (* We are relying here on the tags of digits constructors *) let digits_from_uint i = - let d0 = mkConst_b0 0 in - let d1 = mkConst_b0 1 in + let d0 = Lint 0 in + let d1 = Lint 1 in let digits = Array.make 31 d0 in for k = 0 to 30 do if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 490fabc6a5..d6970c35aa 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -27,6 +27,7 @@ let _ = init_vm () (* Values of the abstract machine *) type values +type structured_values = values let val_of_obj v = ((Obj.obj v):values) let crazy_val = (val_of_obj (Obj.repr 0)) @@ -46,42 +47,64 @@ let cofix_evaluated_tag = 7 So fixme if this happens in a new version of OCaml *) let last_variant_tag = 245 +(** Structured constants are constants whose construction is done once. Their +occurrences share the same value modulo kernel name substitutions (for functor +application). Structured values have the additional property that no +substitution will need to be performed, so their runtime value can directly be +shared without reallocating a more structured representation. *) type structured_constant = | Const_sort of Sorts.t | Const_ind of inductive | Const_b0 of tag - | Const_bn of tag * structured_constant array | Const_univ_level of Univ.Level.t + | Const_val of structured_values type reloc_table = (tag * int) array type annot_switch = {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} -let rec eq_structured_constant c1 c2 = match c1, c2 with +let rec eq_structured_values v1 v2 = + v1 == v2 || + let o1 = Obj.repr v1 in + let o2 = Obj.repr v2 in + if Obj.is_int o1 && Obj.is_int o2 then o1 == o2 + else if Int.equal (Obj.tag o1) (Obj.tag o2) && + Int.equal (Obj.size o1) (Obj.size o2) + then + let i = ref 0 in + while (!i < Obj.size o1 && eq_structured_values + (Obj.magic (Obj.field o1 !i) : structured_values) + (Obj.magic (Obj.field o2 !i) : structured_values)) do + incr i + done; + !i >= Obj.size o1 + else false + +let hash_structured_values (v : structured_values) = + (* We may want a better hash function here *) + Hashtbl.hash v + +let eq_structured_constant c1 c2 = match c1, c2 with | Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2 | Const_sort _, _ -> false | Const_ind i1, Const_ind i2 -> eq_ind i1 i2 | Const_ind _, _ -> false | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 | Const_b0 _, _ -> false -| Const_bn (t1, a1), Const_bn (t2, a2) -> - Int.equal t1 t2 && CArray.equal eq_structured_constant a1 a2 -| Const_bn _, _ -> false | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 | Const_univ_level _ , _ -> false +| Const_val v1, Const_val v2 -> eq_structured_values v1 v2 +| Const_val v1, _ -> false -let rec hash_structured_constant c = +let hash_structured_constant c = let open Hashset.Combine in match c with | Const_sort s -> combinesmall 1 (Sorts.hash s) | Const_ind i -> combinesmall 2 (ind_hash i) | Const_b0 t -> combinesmall 3 (Int.hash t) - | Const_bn (t, a) -> - let fold h c = combine h (hash_structured_constant c) in - let h = Array.fold_left fold 0 a in - combinesmall 4 (combine (Int.hash t) h) - | Const_univ_level l -> combinesmall 5 (Univ.Level.hash l) + | Const_univ_level l -> combinesmall 4 (Univ.Level.hash l) + | Const_val v -> combinesmall 5 (hash_structured_values v) let eq_annot_switch asw1 asw2 = let eq_ci ci1 ci2 = @@ -108,13 +131,12 @@ let pp_sort s = | Set -> Pp.str "Set" | Type u -> Pp.(str "Type@{" ++ Univ.pr_uni u ++ str "}") -let rec pp_struct_const = function +let pp_struct_const = function | Const_sort s -> pp_sort s | Const_ind (mind, i) -> Pp.(MutInd.print mind ++ str"#" ++ int i) | Const_b0 i -> Pp.int i - | Const_bn (i,t) -> - Pp.(int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)) | Const_univ_level l -> Univ.Level.pr l + | Const_val _ -> Pp.str "(value)" (* Abstract data *) type vprod @@ -379,19 +401,21 @@ let obj_of_atom : atom -> Obj.t = res (* obj_of_str_const : structured_constant -> Obj.t *) -let rec obj_of_str_const str = +let obj_of_str_const str = match str with | Const_sort s -> obj_of_atom (Asort 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)) - done; - res | Const_univ_level l -> Obj.repr (Vuniv_level l) + | Const_val v -> Obj.repr v + +let val_of_block tag (args : structured_values array) = + let nargs = Array.length args in + let r = Obj.new_block tag nargs in + for i = 0 to nargs - 1 do + Obj.set_field r i (Obj.repr args.(i)) + done; + (Obj.magic r : structured_values) let val_of_obj o = ((Obj.obj o) : values) @@ -399,6 +423,8 @@ 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 val_of_int i = (Obj.magic i : values) + let atom_of_proj kn v = let r = Obj.new_block proj_tag 2 in Obj.set_field r 0 (Obj.repr kn); diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 2604d50fe6..c7540ae249 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -14,6 +14,7 @@ open Constr (** Values *) type values +type structured_values type vm_env type vm_global type vprod @@ -43,8 +44,8 @@ type structured_constant = | Const_sort of Sorts.t | Const_ind of inductive | Const_b0 of tag - | Const_bn of tag * structured_constant array | Const_univ_level of Univ.Level.t + | Const_val of structured_values val pp_struct_const : structured_constant -> Pp.t @@ -144,6 +145,8 @@ val val_of_constant : Constant.t -> values val val_of_evar : Evar.t -> values val val_of_proj : Projection.Repr.t -> values -> values val val_of_atom : atom -> values +val val_of_int : int -> structured_values +val val_of_block : tag -> structured_values array -> structured_values external val_of_annot_switch : annot_switch -> values = "%identity" external val_of_proj_name : Projection.Repr.t -> values = "%identity" |