OCaml now exports the min and max non-constant tags, let's use it

4 files changed, 23 insertions, 25 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 6dabfee4ef..5362f9a814 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -396,17 +396,17 @@ let init_fun_code () = fun_code := []
 (*
 If [tag] hits the OCaml limitation for non constant constructors, we switch to
 another representation for the remaining constructors:
-[last_variant_tag|tag - last_variant_tag|args]
+[last_variant_tag|tag - Obj.last_non_constant_constructor_tag|args]
 
-We subtract last_variant_tag for efficiency of match interpretation.
+We subtract Obj.last_non_constant_constructor_tag for efficiency of match interpretation.
  *)
 
 let nest_block tag arity cont =
-  Kconst (Const_b0 (tag - last_variant_tag)) ::
-    Kmakeblock(arity+1, last_variant_tag) :: cont
+  Kconst (Const_b0 (tag - Obj.last_non_constant_constructor_tag)) ::
+    Kmakeblock(arity+1, Obj.last_non_constant_constructor_tag) :: cont
 
 let code_makeblock ~stack_size ~arity ~tag cont = 
-  if tag < last_variant_tag then
+  if tag < Obj.last_non_constant_constructor_tag then
     Kmakeblock(arity, tag) :: cont
   else begin
     set_max_stack_size (stack_size + 1);
@@ -637,9 +637,9 @@ let rec compile_lam env cenv lam sz cont =
       let lbl_consts = Array.make oib.mind_nb_constant Label.no in
       let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *)
       let nconst = Array.length branches.constant_branches in
-      let nblock = min nallblock (last_variant_tag + 1) in
+      let nblock = min nallblock (Obj.last_non_constant_constructor_tag + 1) in
       let lbl_blocks = Array.make nblock Label.no in
-      let neblock = max 0 (nallblock - last_variant_tag) in
+      let neblock = max 0 (nallblock - Obj.last_non_constant_constructor_tag) in
       let lbl_eblocks = Array.make neblock Label.no in 
       let branch1, cont = make_branch cont in
       (* Compilation of the return type *)
@@ -665,7 +665,7 @@ let rec compile_lam env cenv lam sz cont =
         let lbl_b, code_b = 
           label_code (
             Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in
-        lbl_blocks.(last_variant_tag) <- lbl_b;
+        lbl_blocks.(Obj.last_non_constant_constructor_tag) <- lbl_b;
         c := code_b
       end;
 
@@ -687,7 +687,7 @@ let rec compile_lam env cenv lam sz cont =
           compile_lam env (push_param arity sz_b cenv)
             body (sz_b+arity) (add_pop arity (branch::!c)) in
         let code_b =
-            if tag < last_variant_tag then begin
+            if tag < Obj.last_non_constant_constructor_tag then begin
                 set_max_stack_size (sz_b + arity);
                 Kpushfields arity :: code_b
               end
@@ -697,8 +697,8 @@ let rec compile_lam env cenv lam sz cont =
               end
         in
         let lbl_b, code_b = label_code code_b in
-        if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b
-          else lbl_eblocks.(tag - last_variant_tag) <- lbl_b;
+        if tag < Obj.last_non_constant_constructor_tag then lbl_blocks.(tag) <- lbl_b
+          else lbl_eblocks.(tag - Obj.last_non_constant_constructor_tag) <- lbl_b;
         c := code_b
       done;
 
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 0a3fb44cbe..ff977416df 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -422,7 +422,7 @@ let rec remove_let subst lam =
 exception TooLargeInductive of Pp.t
 
 let max_nb_const = 0x1000000
-let max_nb_block = 0x1000000 + last_variant_tag - 1
+let max_nb_block = 0x1000000 + Obj.last_non_constant_constructor_tag - 1
 
 let str_max_constructors =
   Format.sprintf
@@ -468,12 +468,12 @@ let makeblock tag nparams arity args =
   if arity = 0 then Lint tag
   else
   if Array.for_all is_value args then
-    if tag < last_variant_tag then
+    if tag < Obj.last_non_constant_constructor_tag then
       Lval(val_of_block tag (Array.map get_value args))
     else
       let args = Array.map get_value args in
-      let args = Array.append [| val_of_int (tag - last_variant_tag) |] args in
-      Lval(val_of_block last_variant_tag args)
+      let args = Array.append [| val_of_int (tag - Obj.last_non_constant_constructor_tag) |] args in
+      Lval(val_of_block Obj.last_non_constant_constructor_tag args)
   else Lmakeblock(tag, args)
 
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index a972803ce4..8edd49f77f 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -25,6 +25,9 @@ let _ = init_vm ()
 (* Abstract data types and utility functions **********)
 (******************************************************)
 
+(* The representation of values relies on this assertion *)
+let _ = assert (Int.equal Obj.first_non_constant_constructor_tag 0)
+
 (* Values of the abstract machine *)
 type values
 type structured_values = values
@@ -43,10 +46,6 @@ let switch_tag = 5
 let cofix_tag = 6
 let cofix_evaluated_tag = 7
 
-(* It would be great if OCaml exported this value,
-   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
@@ -75,7 +74,8 @@ let rec eq_structured_values v1 v2 =
     if Int.equal t1 t2 &&
        Int.equal (Obj.size o1) (Obj.size o2)
     then begin
-      assert (t1 <= last_variant_tag && t2 <= last_variant_tag);
+      assert (t1 <= Obj.last_non_constant_constructor_tag &&
+              t2 <= Obj.last_non_constant_constructor_tag);
       let i = ref 0 in
       while (!i < Obj.size o1 && eq_structured_values
                (Obj.magic (Obj.field o1 !i) : structured_values)
@@ -631,10 +631,10 @@ let branch_arg k (tag,arity) =
   if Int.equal arity 0 then  ((Obj.magic tag):values)
   else
     let b, ofs =
-      if tag < last_variant_tag then Obj.new_block tag arity, 0
+      if tag < Obj.last_non_constant_constructor_tag then Obj.new_block tag arity, 0
       else
-        let b = Obj.new_block last_variant_tag (arity+1) in
-        Obj.set_field b 0 (Obj.repr (tag-last_variant_tag));
+        let b = Obj.new_block Obj.last_non_constant_constructor_tag (arity+1) in
+        Obj.set_field b 0 (Obj.repr (tag-Obj.last_non_constant_constructor_tag));
         b,1 in
     for i = ofs to ofs + arity - 1 do
       Obj.set_field b i (Obj.repr (val_of_rel (k+i)))
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index c7540ae249..ae1d416ed5 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -38,8 +38,6 @@ val switch_tag : tag
 val cofix_tag : tag
 val cofix_evaluated_tag : tag
 
-val last_variant_tag : tag
-
 type structured_constant =
   | Const_sort of Sorts.t
   | Const_ind of inductive