Fix bug 4157,

change the representation of inductive constructor
when there is too many non constant constructors in the inductive type
Conflicts:
	kernel/cbytegen.ml

6 files changed, 87 insertions, 32 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index ae679027d..91b701e0e 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -24,6 +24,7 @@ let fix_tag = 3
 let switch_tag = 4
 let cofix_tag = 5
 let cofix_evaluated_tag = 6
+let max_tag = Obj.lazy_tag - 1
 
 type structured_constant =
   | Const_sorts of sorts
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index b65268f72..4277b4771 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -20,6 +20,7 @@ val fix_tag : tag
 val switch_tag : tag
 val cofix_tag : tag
 val cofix_evaluated_tag : tag
+val max_tag : tag 
 
 type structured_constant =
   | Const_sorts of sorts
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 83f0a3721..95ce2da34 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -329,14 +329,32 @@ let init_fun_code () = fun_code := []
 
 (* Compilation of constructors and inductive types *)
 
+
 (* Limitation due to OCaml's representation of non-constant
   constructors: limited to 245 cases. *)
 
 exception TooLargeInductive of Id.t
 
 let check_compilable ib = 
-  if ib.mind_nb_args < 245 then ()
-  else raise (TooLargeInductive ib.mind_typename)
+  if not (ib.mind_nb_args <= 0xFFFF && ib.mind_nb_constant <= 0xFFFF) then 
+    raise (TooLargeInductive ib.mind_typename)
+
+(* Inv: arity > 0 *)
+
+let const_bn tag args = 
+  if tag < max_tag then Const_bn(tag, args)
+  else
+    Const_bn(max_tag,
+             [|Const_b0 (tag - max_tag);
+               Const_bn (0, args) |])
+  
+let code_makeblock arity tag cont = 
+  if tag < max_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 
 
 (* Inv : nparam + arity > 0 *)
 let code_construct tag nparams arity cont =
@@ -344,7 +362,8 @@ let code_construct tag nparams arity cont =
       add_pop nparams
       (if Int.equal arity 0 then
 	[Kconst (Const_b0 tag); Kreturn 0]
-       else [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0])
+       else 
+          Kacc 0:: Kpop 1 :: code_makeblock arity tag [Kreturn 0])
     in
     let lbl = Label.create() in
     fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)];
@@ -354,7 +373,6 @@ let get_strcst = function
   | Bstrconst sc -> sc
   | _ -> raise Not_found
 
-
 let rec str_const c =
   match kind_of_term c with
   | Sort s -> Bstrconst (Const_sorts s)
@@ -367,7 +385,7 @@ let rec str_const c =
 	    let oib = lookup_mind kn !global_env in
 	    let oip = oib.mind_packets.(j) in
 	    let () = check_compilable oip in
-	    let num,arity = oip.mind_reloc_tbl.(i-1) in
+	    let tag,arity = oip.mind_reloc_tbl.(i-1) in
 	    let nparams = oib.mind_nparams in
 	    if Int.equal (nparams + arity) (Array.length args) then
               (* spiwack: *)
@@ -409,15 +427,15 @@ let rec str_const c =
               with Not_found ->
 		(* 3/ if no special behavior is available, then the compiler
 		      falls back to the normal behavior *)
-		if Int.equal arity 0 then Bstrconst(Const_b0 num)
+		if Int.equal arity 0 then Bstrconst(Const_b0 tag)
 		else
 		  let rargs = Array.sub args nparams arity in
 		  let b_args = Array.map str_const rargs in
 		  try
 		    let sc_args = Array.map get_strcst b_args in
-		    Bstrconst(Const_bn(num, sc_args))
+		    Bstrconst(const_bn tag sc_args)
 		  with Not_found ->
-		    Bmakeblock(num,b_args)
+		    Bmakeblock(tag,b_args)
 	    else
               let b_args = Array.map str_const args in
 	     (* spiwack: tries first to apply the run-time compilation
@@ -428,7 +446,7 @@ let rec str_const c =
                                            f),
                          b_args)
 	      with Not_found ->
-	        Bconstruct_app(num, nparams, arity, b_args)
+	        Bconstruct_app(tag, nparams, arity, b_args)
               end
 	| _ -> Bconstr c
       end
@@ -624,7 +642,11 @@ let rec compile_constr reloc c sz cont =
       let () = check_compilable oib in
       let tbl = oib.mind_reloc_tbl in
       let lbl_consts = Array.make oib.mind_nb_constant Label.no in
-      let lbl_blocks = Array.make (oib.mind_nb_args+1) Label.no in
+      let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *)
+      let nblock = min nallblock (max_tag + 1) in
+      let lbl_blocks = Array.make nblock Label.no in
+      let neblock = max 0 (nallblock - max_tag) in
+      let lbl_eblocks = Array.make neblock Label.no in 
       let branch1,cont = make_branch cont in
       (* Compiling return type *)
       let lbl_typ,fcode =
@@ -644,6 +666,15 @@ 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) *)
+      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;
+        c := code_b
+      end;  
+      
       (* Compiling regular constructor branches *)
       for i = 0 to Array.length tbl - 1 do
 	let tag, arity = tbl.(i) in
@@ -655,19 +686,22 @@ let rec compile_constr reloc c sz cont =
 	else
 	  let args, body = decompose_lam branchs.(i) in
 	  let nargs = List.length args in
-	  let lbl_b,code_b =
-	    label_code(
-	    if Int.equal nargs arity then
+          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)
-		(Kappterm(arity,sz_appterm) :: !c))
-	  in
-	  lbl_blocks.(tag) <- lbl_b;
+	        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;
 	  c := code_b
       done;
       c :=  Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c;
@@ -692,9 +726,10 @@ and compile_str_cst reloc sc sz cont =
   | Bstrconst sc -> Kconst sc :: cont
   | Bmakeblock(tag,args) ->
       let nargs = Array.length args in
-      comp_args compile_str_cst reloc args sz (Kmakeblock(nargs,tag) :: cont)
+      comp_args compile_str_cst reloc args sz (code_makeblock nargs tag cont)
   | Bconstruct_app(tag,nparams,arity,args) ->
-      if Int.equal (Array.length args) 0 then code_construct tag nparams arity cont
+      if Int.equal (Array.length args) 0 then
+        code_construct tag nparams arity cont
       else
 	comp_app
 	  (fun _ _ _ cont -> code_construct tag nparams arity cont)
@@ -743,7 +778,8 @@ let compile fail_on_error env c =
     let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in
       (Pp.(fn
 	   (str "Cannot compile code for virtual machine as it uses inductive " ++
-	    Id.print tname ++ str " which has more than 245 constructors"));
+	    Id.print tname ++ str 
+          " which has more than 65535 constant constructors or more than 65535 non-constant constructors"));
        None)
 
 let compile_constant_body fail_on_error env = function
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 29315b0a9..6044e1846 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -63,9 +63,9 @@ 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 b1, Vconstr_block b2 ->
+  | Vconstr_block (tag1, b1), Vconstr_block (tag2, b2) ->
       let sz = bsize b1 in
-      if Int.equal (btag b1) (btag b2) && Int.equal sz (bsize b2) then
+      if Int.equal tag1 tag2 && Int.equal sz (bsize b2) then
 	let rcu = ref cu in
 	for i = 0 to sz - 1 do
 	  rcu := conv_val env CONV k (bfield b1 i) (bfield b2 i) !rcu
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 2cc1efe43..65d84e882 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -79,7 +79,7 @@ type vprod
 type vfun
 type vfix
 type vcofix
-type vblock
+type vblock 
 type arguments
 
 type vm_env
@@ -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 vblock
+  | Vconstr_block of int * vblock
   | Vatom_stk of atom * stack
 
 (*************************************************)
@@ -224,7 +224,13 @@ let whd_val : values -> whd =
 	   | 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 
+          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)
 
 
 
@@ -518,10 +524,22 @@ let type_of_switch sw =
 let branch_arg k (tag,arity) =
   if Int.equal arity 0 then  ((Obj.magic tag):values)
   else
-    let b = Obj.new_block tag arity in
-    for i = 0 to arity - 1 do
-      Obj.set_field b i (Obj.repr (val_of_rel (k+i)))
-    done;
+    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
+      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
     val_of_obj b
 
 let apply_switch sw arg =
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 295ea83c4..139202f09 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 vblock
+  | Vconstr_block of int * vblock
   | Vatom_stk of atom * stack
 
 (** Constructors *)
@@ -94,7 +94,6 @@ val reduce_cofix : int -> vcofix -> values array * values array
 
 (** Block *)
 
-val btag : vblock -> int
 val bsize : vblock -> int
 val bfield : vblock -> int -> values