use a more compact representation of non-constant constructors

for which there corresponding tag are greater than max_variant_tag.
The code is a merge with the patch proposed by Bruno on 
github barras/coq 
commit/504c753d7bb104ff4453fa0ede21c870ae2bb00c

8 files changed, 60 insertions, 63 deletions

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index a583e2e54..4578a3b33 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -74,14 +74,14 @@ and ppwhd whd =
   | Vfix _ -> print_vfix()
   | Vcofix _ -> print_string "cofix"
   | Vconstr_const i -> print_string "C(";print_int i;print_string")"
-  | Vconstr_block (tag,b) -> ppvblock tag b
+  | Vconstr_block b -> ppvblock b
   | Vatom_stk(a,s) ->
       open_hbox();ppatom a;close_box();
       print_string"@";ppstack s
 
-and ppvblock tag b =
+and ppvblock b =
   open_hbox();
-  print_string "Cb(";print_int tag;
+  print_string "Cb(";print_int (btag b);
   let n = bsize b in
   for i = 0 to n -1 do
     print_string ",";ppvalues (bfield b i)
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 91b701e0e..700de5020 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -24,7 +24,9 @@ let fix_tag = 3
 let switch_tag = 4
 let cofix_tag = 5
 let cofix_evaluated_tag = 6
-let max_tag = Obj.lazy_tag - 1
+(* It could be greate if OCaml export this value,
+   So fixme if this occur in a new version of OCaml *)
+let last_variant_tag = 245 
 
 type structured_constant =
   | Const_sorts of sorts
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 4277b4771..fbb40ffd1 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -20,7 +20,7 @@ val fix_tag : tag
 val switch_tag : tag
 val cofix_tag : tag
 val cofix_evaluated_tag : tag
-val max_tag : tag 
+val last_variant_tag : tag 
 
 type structured_constant =
   | Const_sorts of sorts
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 0cd250113..45808b072 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -331,12 +331,12 @@ let init_fun_code () = fun_code := []
 
 
 (* Limitation due to OCaml's representation of non-constant
-  constructors: limited to 245 cases. *)
+  constructors: limited to 245 + 1 (0 tag) cases. *)
 
 exception TooLargeInductive of Id.t
 
 let max_nb_const = 0x7FFFFF 
-let max_nb_block = 0x7FFFFF + max_tag - 1
+let max_nb_block = 0x7FFFFF + last_variant_tag - 1
 
 let str_max_constructors = 
   Format.sprintf 
@@ -350,19 +350,17 @@ let check_compilable ib =
 (* Inv: arity > 0 *)
 
 let const_bn tag args = 
-  if tag < max_tag then Const_bn(tag, args)
+  if tag < last_variant_tag then Const_bn(tag, args)
   else
-    Const_bn(max_tag,
-             [|Const_b0 (tag - max_tag);
-               Const_bn (0, args) |])
+    Const_bn(last_variant_tag, Array.append [|Const_b0 (tag - last_variant_tag) |] args)
+
   
 let code_makeblock arity tag cont = 
-  if tag < max_tag then
+  if tag < last_variant_tag then
     Kmakeblock(arity, tag) :: cont
   else
-    Kmakeblock(arity, 0) :: Kpush ::     (* Const_bn (0, args) *)
-    Kconst (Const_b0 (tag - max_tag)) :: (* Const_b0  (tag - max_tag)) *)
-    Kmakeblock(2, max_tag) :: cont 
+    Kpush :: Kconst (Const_b0 (tag - last_variant_tag)) ::
+    Kmakeblock(arity+1, last_variant_tag) :: cont
 
 (* Inv : nparam + arity > 0 *)
 let code_construct tag nparams arity cont =
@@ -370,8 +368,11 @@ let code_construct tag nparams arity cont =
       add_pop nparams
       (if Int.equal arity 0 then
 	[Kconst (Const_b0 tag); Kreturn 0]
+       else if tag < last_variant_tag then
+         [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0]
        else 
-          Kacc 0:: Kpop 1 :: code_makeblock arity tag [Kreturn 0])
+         [Kconst (Const_b0 (tag - last_variant_tag)); 
+          Kmakeblock(arity+1, last_variant_tag); Kreturn 0])
     in
     let lbl = Label.create() in
     fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)];
@@ -651,9 +652,9 @@ let rec compile_constr reloc c sz cont =
       let tbl = oib.mind_reloc_tbl in
       let lbl_consts = Array.make oib.mind_nb_constant Label.no in
       let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *)
-      let nblock = min nallblock (max_tag + 1) in
+      let nblock = min nallblock (last_variant_tag + 1) in
       let lbl_blocks = Array.make nblock Label.no in
-      let neblock = max 0 (nallblock - max_tag) in
+      let neblock = max 0 (nallblock - last_variant_tag) in
       let lbl_eblocks = Array.make neblock Label.no in 
       let branch1,cont = make_branch cont in
       (* Compiling return type *)
@@ -674,12 +675,12 @@ let rec compile_constr reloc c sz cont =
       in
       lbl_blocks.(0) <- lbl_accu;
       let c = ref code_accu in
-      (* perform the extra match if needed (to many block constructor) *)
+      (* perform the extra match if needed (to many block constructors) *)
       if neblock <> 0 then begin
         let lbl_b, code_b = 
           label_code (
-            Kpushfields 2 :: Kacc 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in
-        lbl_blocks.(max_tag) <- lbl_b;
+            Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in
+        lbl_blocks.(last_variant_tag) <- lbl_b;
         c := code_b
       end;  
       
@@ -694,25 +695,24 @@ let rec compile_constr reloc c sz cont =
 	else
 	  let args, body = decompose_lam branchs.(i) in
 	  let nargs = List.length args in
+         
           let code_b =  
             if Int.equal nargs arity then
-	      Kpushfields arity ::
-	        compile_constr (push_param arity sz_b reloc)
+	      compile_constr (push_param arity sz_b reloc)
 		body (sz_b+arity) (add_pop arity (branch :: !c))
 	    else
 	      let sz_appterm = if is_tailcall then sz_b + arity else arity in
-	      Kpushfields arity ::
-	        compile_constr reloc branchs.(i) (sz_b+arity)
+	      compile_constr reloc branchs.(i) (sz_b+arity)
 		(Kappterm(arity,sz_appterm) :: !c) in
           let code_b = 
-            if tag < max_tag then code_b
-            else Kacc 1::Kpop 2::code_b in
-	  let lbl_b,code_b = label_code code_b in
-          if tag < max_tag then lbl_blocks.(tag) <- lbl_b
-          else lbl_eblocks.(tag - max_tag) <- lbl_b;
+            if tag < last_variant_tag then Kpushfields arity :: code_b
+            else Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b 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;
 	  c := code_b
       done;
-      c :=  Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c;
+      c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c;
       let code_sw =
  	match branch1 with
         (* spiwack : branch1 can't be a lbl anymore it's a Branch instead
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 6044e1846..1c31cc041 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -63,7 +63,8 @@ and conv_whd env pb k whd1 whd2 cu =
       else conv_arguments env k args1 args2 (conv_cofix env k cf1 cf2 cu)
   | Vconstr_const i1, Vconstr_const i2 ->
       if Int.equal i1 i2 then cu else raise NotConvertible
-  | Vconstr_block (tag1, b1), Vconstr_block (tag2, b2) ->
+  | Vconstr_block b1, Vconstr_block b2 ->
+      let tag1 = btag b1 and tag2 = btag b2 in
       let sz = bsize b1 in
       if Int.equal tag1 tag2 && Int.equal sz (bsize b2) then
 	let rcu = ref cu in
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 65d84e882..d4bf461b3 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -161,7 +161,7 @@ type whd =
   | Vfix of vfix * arguments option
   | Vcofix of vcofix * to_up * arguments option
   | Vconstr_const of int
-  | Vconstr_block of int * vblock
+  | Vconstr_block of vblock
   | Vatom_stk of atom * stack
 
 (*************************************************)
@@ -225,15 +225,8 @@ let whd_val : values -> whd =
 	   | 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 
-          if tag = max_tag then
-            let tag = Obj.obj (Obj.field o 0) + max_tag in
-            let block = Obj.obj (Obj.field o 1) in
-             Vconstr_block(tag, block)
-          else
-            Vconstr_block(tag, Obj.obj o)
-
-
-
+          Vconstr_block(Obj.obj o)
+         
 (************************************************)
 (* Abstrct machine ******************************)
 (************************************************)
@@ -524,22 +517,15 @@ let type_of_switch sw =
 let branch_arg k (tag,arity) =
   if Int.equal arity 0 then  ((Obj.magic tag):values)
   else
-    let init b = 
-      for i = 0 to arity - 1 do
-        Obj.set_field b i (Obj.repr (val_of_rel (k+i)))
-      done in
-    let b =
-      if tag < max_tag then
-        let b = Obj.new_block tag arity in
-        init b;
-        b
+    let b, ofs = 
+      if tag < last_variant_tag then Obj.new_block tag arity, 0
       else
-        let b0 = Obj.new_block 0 arity in
-        init b0;
-        let b = Obj.new_block max_tag 2 in
-        Obj.set_field b 0 (Obj.repr (tag - max_tag));
-        Obj.set_field b 1 (Obj.repr b0);
-        b in
+        let b = Obj.new_block last_variant_tag (arity+1) in
+        Obj.set_field b 0 (Obj.repr (tag-last_variant_tag));
+        b,1 in
+    for i = ofs to ofs + arity - 1 do
+      Obj.set_field b i (Obj.repr (val_of_rel (k+i)))
+    done;
     val_of_obj b
 
 let apply_switch sw arg =
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 139202f09..519035682 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -46,7 +46,7 @@ type whd =
   | Vfix of vfix * arguments option
   | Vcofix of vcofix * to_up * arguments option
   | Vconstr_const of int
-  | Vconstr_block of int * vblock
+  | Vconstr_block of vblock
   | Vatom_stk of atom * stack
 
 (** Constructors *)
@@ -94,6 +94,7 @@ val reduce_cofix : int -> vcofix -> values array * values array
 
 (** Block *)
 
+val btag  : vblock -> int
 val bsize : vblock -> int
 val bfield : vblock -> int -> values
 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 3c302f8da..8198db1b8 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -165,9 +165,16 @@ and nf_whd env whd typ =
       let _, args = nf_args env vargs t in
       mkApp(cfd,args)
   | Vconstr_const n -> construct_of_constr_const env n typ
-  | Vconstr_block (tag,b) ->
+  | Vconstr_block b ->
+      let tag = btag b in
+      let (tag,ofs) =
+        if tag = Cbytecodes.last_variant_tag then
+	  match whd_val (bfield b 0) with
+	  | Vconstr_const tag -> (tag+Cbytecodes.last_variant_tag, 1)
+	  | _ -> assert false
+        else (tag, 0) in
       let capp,ctyp = construct_of_constr_block env tag typ in
-      let args = nf_bargs env b ctyp in
+      let args = nf_bargs env b ofs ctyp in
       mkApp(capp,args)
   | Vatom_stk(Aid idkey, stk) ->
       let c,typ = constr_type_of_idkey env idkey in
@@ -242,14 +249,14 @@ and nf_args env vargs t =
 	t := subst1 c codom; c) in
   !t,args
 
-and nf_bargs env b t =
+and nf_bargs env b ofs t =
   let t = ref t in
-  let len = bsize b in
+  let len = bsize b - ofs in
   let args =
     Array.init len
       (fun i ->
 	let _,dom,codom = decompose_prod env !t in
-	let c = nf_val env (bfield b i) dom in
+	let c = nf_val env (bfield b (i+ofs)) dom in
 	t := subst1 c codom; c) in
   args