[native compiler] Encoding of constructors based on tags

This serves two purposes:

1. It makes the native compiler use the same encoding and
   lambda-representation as the bytecode compiler

2. It avoid relying on fragile invariants relating tags and constructor
   indices. For example, previously, the mapping from indices to tags
   had to be increasing.

3 files changed, 232 insertions, 162 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 375f3184de..3f791dfc22 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -377,8 +377,8 @@ type mllambda =
   | MLif           of mllambda * mllambda * mllambda
   | MLmatch        of annot_sw * mllambda * mllambda * mllam_branches
                               (* argument, prefix, accu branch, branches *)
-  | MLconstruct    of string * constructor * mllambda array
-                   (* prefix, constructor name, arguments *)
+  | MLconstruct    of string * inductive * int * mllambda array
+                   (* prefix, inductive name, tag, arguments *)
   | MLint          of int
   | MLuint         of Uint63.t
   | MLsetref       of string * mllambda
@@ -386,7 +386,11 @@ type mllambda =
   | MLarray        of mllambda array
   | MLisaccu       of string * inductive * mllambda
 
-and mllam_branches = ((constructor * lname option array) list * mllambda) array
+and 'a mllam_pattern =
+  | ConstPattern of int
+  | NonConstPattern of tag * 'a array
+
+and mllam_branches = (lname option mllam_pattern list * mllambda) array
 
 let push_lnames n env lns =
   snd (Array.fold_left (fun (i,r) x -> (i+1, LNmap.add x i r)) (n,env) lns)
@@ -439,9 +443,10 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
       eq_mllambda gn1 gn2 n env1 env2 c1 c2 &&
       eq_mllambda gn1 gn2 n env1 env2 accu1 accu2 &&
       eq_mllam_branches gn1 gn2 n env1 env2 br1 br2
-  | MLconstruct (pf1, cs1, args1), MLconstruct (pf2, cs2, args2) ->
+  | MLconstruct (pf1, ind1, tag1, args1), MLconstruct (pf2, ind2, tag2, args2) ->
       String.equal pf1 pf2 &&
-      eq_constructor cs1 cs2 &&
+      eq_ind ind1 ind2 &&
+      Int.equal tag1 tag2 &&
       Array.equal (eq_mllambda gn1 gn2 n env1 env2) args1 args2
   | MLint i1, MLint i2 ->
       Int.equal i1 i2
@@ -474,15 +479,22 @@ and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 =
 
 (* we require here that patterns have the same order, which may be too strong *)
 and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 =
-  let eq_cargs (cs1, args1) (cs2, args2) body1 body2 =
+  let eq_cargs args1 args2 body1 body2 =
     Int.equal (Array.length args1) (Array.length args2) &&
-    eq_constructor cs1 cs2 &&
     let env1 = opush_lnames n env1 args1 in
     let env2 = opush_lnames n env2 args2 in
     eq_mllambda gn1 gn2 (n + Array.length args1) env1 env2 body1 body2
   in
-  let eq_branch (ptl1,body1) (ptl2,body2) =
-   List.equal (fun pt1 pt2 -> eq_cargs pt1 pt2 body1 body2) ptl1 ptl2
+  let eq_pattern pat1 pat2 body1 body2 =
+    match pat1, pat2 with
+    | ConstPattern tag1, ConstPattern tag2 ->
+      Int.equal tag1 tag2 && eq_mllambda gn1 gn2 n env1 env2 body1 body2
+    | NonConstPattern (tag1,args1), NonConstPattern (tag2,args2) ->
+      Int.equal tag1 tag2 && eq_cargs args1 args2 body1 body2
+    | (ConstPattern _ | NonConstPattern _), _ -> false
+  in
+  let eq_branch (patl1,body1) (patl2,body2) =
+    List.equal (fun pt1 pt2 -> eq_pattern pt1 pt2 body1 body2) patl1 patl2
   in
   Array.equal eq_branch br1 br2
 
@@ -518,10 +530,11 @@ let rec hash_mllambda gn n env t =
       let hc = hash_mllambda gn n env c in
       let haccu = hash_mllambda gn n env accu in
       combinesmall 9 (hash_mllam_branches gn n env (combine3 hannot hc haccu) br)
-  | MLconstruct (pf, cs, args) ->
+  | MLconstruct (pf, ind, tag, args) ->
       let hpf = String.hash pf in
-      let hcs = constructor_hash cs in
-      combinesmall 10 (hash_mllambda_array gn n env (combine hpf hcs) args)
+      let hcs = ind_hash ind in
+      let htag = Int.hash tag in
+      combinesmall 10 (hash_mllambda_array gn n env (combine3 hpf hcs htag) args)
   | MLint i ->
       combinesmall 11 i
   | MLuint i ->
@@ -551,15 +564,18 @@ and hash_mllambda_array gn n env init arr =
   Array.fold_left (fun acc t -> combine (hash_mllambda gn n env t) acc) init arr
 
 and hash_mllam_branches gn n env init br =
-  let hash_cargs (cs, args) body =
+  let hash_cargs args body =
     let nargs = Array.length args in
-    let hcs = constructor_hash cs in
     let env = opush_lnames n env args in
     let hbody = hash_mllambda gn (n + nargs) env body in
-    combine3 nargs hcs hbody
+    combine nargs hbody
+  in
+  let hash_pattern pat body = match pat with
+    | ConstPattern i -> combinesmall 1 (Int.hash i)
+    | NonConstPattern (tag,args) -> combinesmall 2 (combine (Int.hash tag) (hash_cargs args body))
   in
   let hash_branch acc (ptl,body) =
-    List.fold_left (fun acc t -> combine (hash_cargs t body) acc) acc ptl
+    List.fold_left (fun acc t -> combine (hash_pattern t body) acc) acc ptl
   in
   Array.fold_left hash_branch init br
 
@@ -589,17 +605,20 @@ let fv_lam l =
     | MLmatch(_,a,p,bs) ->
       let fv = aux a bind (aux p bind fv) in
       let fv_bs (cargs, body) fv =
-	let bind = 
-	  List.fold_right (fun (_,args) bind ->
-	    Array.fold_right 
-	      (fun o bind -> match o with 
-	      | Some l -> LNset.add l bind 
-	      | _ -> bind) args bind) 
-	    cargs bind in
-	aux body bind fv in
+        let bind =
+          List.fold_right (fun pat bind ->
+              match pat with
+              | ConstPattern _ -> bind
+              | NonConstPattern(_,args) ->
+                Array.fold_right
+                  (fun o bind -> match o with
+                     | Some l -> LNset.add l bind
+                     | _ -> bind) args bind)
+            cargs bind in
+        aux body bind fv in
       Array.fold_right fv_bs bs fv
-          (* argument, accu branch, branches *)
-    | MLconstruct (_,_,p) ->
+    (* argument, accu branch, branches *)
+    | MLconstruct (_,_,_,p) ->
 	Array.fold_right (fun a fv -> aux a bind fv) p fv
     | MLsetref(_,l) -> aux l bind fv
     | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv)
@@ -647,8 +666,8 @@ type global =
   | Gletcase of 
       gname * lname array * annot_sw * mllambda * mllambda * mllam_branches
   | Gopen of string
-  | Gtype of inductive * int array
-    (* ind name, arities of constructors *)
+  | Gtype of inductive * (tag * int) array
+    (* ind name, tag and arities of constructors *)
   | Gcomment of string
 
 (* Alpha-equivalence on globals *)
@@ -673,7 +692,8 @@ let eq_global g1 g2 =
       eq_mllambda gn1 gn2 (Array.length lns1) env1 env2 t1 t2
   | Gopen s1, Gopen s2 -> String.equal s1 s2
   | Gtype (ind1, arr1), Gtype (ind2, arr2) ->
-      eq_ind ind1 ind2 && Array.equal Int.equal arr1 arr2
+    eq_ind ind1 ind2 &&
+    Array.equal (fun (tag1,ar1) (tag2,ar2) -> Int.equal tag1 tag2 && Int.equal ar1 ar2) arr1 arr2
   | Gcomment s1, Gcomment s2 -> String.equal s1 s2
   | _, _ -> false
 
@@ -700,7 +720,10 @@ let hash_global g =
       combinesmall 4 (combine nlns (hash_mllambda gn nlns env t))
   | Gopen s -> combinesmall 5 (String.hash s)
   | Gtype (ind, arr) ->
-      combinesmall 6 (combine (ind_hash ind) (Array.fold_left combine 0 arr))
+    let hash_aux acc (tag,ar) =
+      combine3 acc (Int.hash tag) (Int.hash ar)
+    in
+    combinesmall 6 (combine (ind_hash ind) (Array.fold_left hash_aux 0 arr))
   | Gcomment s -> combinesmall 7 (String.hash s)
   
 let global_stack = ref ([] : global list)
@@ -907,26 +930,33 @@ let get_proj_code i =
     [|MLglobal symbols_tbl_name; MLint i|])
 
 type rlist =
-  | Rnil 
-  | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist' 
+  | Rnil
+  | Rcons of lname option mllam_pattern list ref * LNset.t * mllambda * rlist'
 and rlist' = rlist ref
 
-let rm_params fv params = 
-  Array.map (fun l -> if LNset.mem l fv then Some l else None) params 
+let rm_params fv params =
+  Array.map (fun l -> if LNset.mem l fv then Some l else None) params
 
-let rec insert cargs body rl =
+let rec insert pat body rl =
  match !rl with
  | Rnil ->
      let fv = fv_lam body in
-     let (c,params) = cargs in
-     let params = rm_params fv params in
-     rl:= Rcons(ref [(c,params)], fv, body, ref Rnil)
+     begin match pat with
+     | ConstPattern _ as p ->
+       rl:= Rcons(ref [p], fv, body, ref Rnil)
+     | NonConstPattern (tag,args) ->
+       let args = rm_params fv args in
+       rl:= Rcons(ref [NonConstPattern (tag,args)], fv, body, ref Rnil)
+     end
  | Rcons(l,fv,body',rl) ->
-     if eq_mllambda body body' then
-       let (c,params) = cargs in
-       let params = rm_params fv params in
-       l := (c,params)::!l
-     else insert cargs body rl
+   if eq_mllambda body body' then
+     match pat with
+     | ConstPattern _ as p ->
+       l := p::!l
+     | NonConstPattern (tag,args) ->
+       let args = rm_params fv args in
+       l := NonConstPattern (tag,args)::!l
+   else insert pat body rl
 
 let rec to_list rl =
   match !rl with
@@ -935,7 +965,7 @@ let rec to_list rl =
 
 let merge_branches t =
   let newt = ref Rnil in
-  Array.iter (fun (c,args,body) -> insert (c,args) body newt) t;
+  Array.iter (fun (pat,body) -> insert pat body newt) t;
   Array.of_list (to_list newt)
 
 let app_prim p args = MLapp(MLprimitive p, args)
@@ -1092,14 +1122,19 @@ let ml_of_instance instance u =
       let a_uid = fresh_lname Anonymous in
       let la_uid = MLlocal a_uid in
       (* compilation of branches *)
-      let ml_br (c,params, body) = 
-	let lnames, env_c = push_rels env_c params in
-	(c, lnames, ml_of_lam env_c l body)
+      let nbconst = Array.length bs.constant_branches in
+      let nbtotal = nbconst + Array.length bs.nonconstant_branches in
+      let br = Array.init nbtotal (fun i -> if i < Array.length bs.constant_branches then
+                                  (ConstPattern i, ml_of_lam env_c l bs.constant_branches.(i))
+                                else
+                                  let (params, body) = bs.nonconstant_branches.(i-nbconst) in
+                                  let lnames, env_c = push_rels env_c params in
+                                  (NonConstPattern (i-nbconst+1,lnames), ml_of_lam env_c l body)
+                              )
       in
-      let bs = Array.map ml_br bs in
       let cn = fresh_gcase l in
       (* Compilation of accu branch *)
-      let pred = MLapp(MLglobal pn, fv_args env_c pfvn pfvr) in  
+      let pred = MLapp(MLglobal pn, fv_args env_c pfvn pfvr) in
       let (fvn, fvr) = !(env_c.env_named), !(env_c.env_urel) in
       let cn_fv = mkMLapp (MLglobal cn) (fv_args env_c fvn fvr) in
          (* remark : the call to fv_args does not add free variables in env_c *)
@@ -1112,7 +1147,7 @@ let ml_of_instance instance u =
 (*      let body = MLlam([|a_uid|], MLmatch(annot, la_uid, accu, bs)) in
       let case = generalize_fv env_c body in *)
       let cn = push_global_case cn (Array.append (fv_params env_c) [|a_uid|])
-        annot la_uid accu (merge_branches bs)
+        annot la_uid accu (merge_branches br)
       in
       (* Final result *)
       let arg = ml_of_lam env l a in
@@ -1274,9 +1309,9 @@ let ml_of_instance instance u =
 
   | Lint tag -> MLapp(MLprimitive Mk_int, [|MLint tag|])
 
-  | Lmakeblock (prefix,cn,_,args) ->
+  | Lmakeblock (prefix,cn,tag,args) ->
      let args = Array.map (ml_of_lam env l) args in
-     MLconstruct(prefix,cn,args)
+     MLconstruct(prefix,cn,tag,args)
   | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|])
   | Lval v ->
       let i = push_symbol (SymbValue v) in get_value_code i
@@ -1339,7 +1374,7 @@ let subst s l =
       | MLmatch(annot,a,accu,bs) ->
 	  let auxb (cargs,body) = (cargs,aux body) in
 	  MLmatch(annot,a,aux accu, Array.map auxb bs)
-      | MLconstruct(prefix,c,args) -> MLconstruct(prefix,c,Array.map aux args)
+      | MLconstruct(prefix,c,tag,args) -> MLconstruct(prefix,c,tag,Array.map aux args)
       | MLsetref(s,l1) -> MLsetref(s,aux l1) 
       | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2)
       | MLarray arr -> MLarray (Array.map aux arr)
@@ -1448,8 +1483,8 @@ let optimize gdef l =
     | MLmatch(annot,a,accu,bs) ->
 	let opt_b (cargs,body) = (cargs,optimize s body) in
 	MLmatch(annot, optimize s a, subst s accu, Array.map opt_b bs)
-    | MLconstruct(prefix,c,args) ->
-        MLconstruct(prefix,c,Array.map (optimize s) args)
+    | MLconstruct(prefix,c,tag,args) ->
+        MLconstruct(prefix,c,tag,Array.map (optimize s) args)
     | MLsetref(r,l) -> MLsetref(r, optimize s l) 
     | MLsequence(l1,l2) -> MLsequence(optimize s l1, optimize s l2)
     | MLarray arr -> MLarray (Array.map (optimize s) arr)
@@ -1522,6 +1557,7 @@ let string_of_kn kn =
 
 let string_of_con c = string_of_kn (Constant.user c)
 let string_of_mind mind = string_of_kn (MutInd.user mind)
+let string_of_ind (mind,i) = string_of_kn (MutInd.user mind) ^ "_" ^ string_of_int i
 
 let string_of_gname g =
   match g with
@@ -1559,10 +1595,13 @@ let pp_ldecls fmt ids =
     Format.fprintf fmt " (%a : Nativevalues.t)" pp_lname ids.(i)
   done
 
-let string_of_construct prefix ((mind,i),j) =
-  let id = Format.sprintf "Construct_%s_%i_%i" (string_of_mind mind) i (j-1) in
-  prefix ^ id
-   
+let string_of_construct prefix ~constant ind tag =
+  let base = if constant then "Int" else "Construct" in
+  Format.sprintf "%s%s_%s_%i" prefix base (string_of_ind ind) tag
+
+let string_of_accu_construct prefix ind =
+  Format.sprintf "%sAccu_%s" prefix (string_of_ind ind)
+
 let pp_int fmt i =
   if i < 0 then Format.fprintf fmt "(%i)" i else Format.fprintf fmt "%i" i
 
@@ -1588,16 +1627,16 @@ let pp_mllam fmt l =
 	Format.fprintf fmt "@[(if %a then@\n  %a@\nelse@\n  %a)@]"
 	  pp_mllam t pp_mllam l1 pp_mllam l2 
     | MLmatch (annot, c, accu_br, br) ->
-	  let mind,i = annot.asw_ind in
+      let ind = annot.asw_ind in
       let prefix = annot.asw_prefix in
-	  let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in
-	  Format.fprintf fmt 
-	    "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n  %a@\n%aend@]"
-	  pp_mllam c accu pp_mllam accu_br (pp_branches prefix) br
-	  
-    | MLconstruct(prefix,c,args) ->
+      let accu = string_of_accu_construct prefix ind in
+      Format.fprintf fmt
+        "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n  %a@\n%aend@]"
+        pp_mllam c accu pp_mllam accu_br (pp_branches prefix ind) br
+
+    | MLconstruct(prefix,ind,tag,args) ->
         Format.fprintf fmt "@[(Obj.magic (%s%a) : Nativevalues.t)@]" 
-          (string_of_construct prefix c) pp_cargs args
+          (string_of_construct prefix ~constant:false ind tag) pp_cargs args
     | MLint i -> pp_int fmt i
     | MLuint i -> Format.fprintf fmt "(%s)" (Uint63.compile i)
     | MLsetref (s, body) ->
@@ -1614,8 +1653,8 @@ let pp_mllam fmt l =
          pp_mllam fmt arr.(len-1)
        end;
        Format.fprintf fmt "|]@]"
-    | MLisaccu (prefix, (mind, i), c) ->
-        let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in
+    | MLisaccu (prefix, ind, c) ->
+        let accu = string_of_accu_construct prefix ind in
         Format.fprintf fmt
           "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n  true@\n| _ ->@\n  false@\nend@]"
         pp_mllam c accu
@@ -1638,7 +1677,7 @@ let pp_mllam fmt l =
     | MLprimitive (Mk_prod | Mk_sort) (* FIXME: why this special case? *)
     | MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ ->
 	Format.fprintf fmt "(%a)" pp_mllam l
-    | MLconstruct(_,_,args) when Array.length args > 0 ->
+    | MLconstruct(_,_,_,args) when Array.length args > 0 ->
 	Format.fprintf fmt "(%a)" pp_mllam l
     | _ -> pp_mllam fmt l
 
@@ -1677,19 +1716,23 @@ let pp_mllam fmt l =
 	  done in 
 	Format.fprintf fmt "(%a)" aux params
 
-  and pp_branches prefix fmt bs =
+  and pp_branches prefix ind fmt bs =
     let pp_branch (cargs,body) =
-      let pp_c fmt (cn,args) = 
-        Format.fprintf fmt "| %s%a " 
-      (string_of_construct prefix cn) pp_cparams args in
-      let rec pp_cargs fmt cargs =
-        match cargs with
-    | [] -> ()
-    | cargs::cargs' -> 
-        Format.fprintf fmt "%a%a" pp_c cargs pp_cargs cargs' in
-      Format.fprintf fmt "%a ->@\n  %a@\n" 
-    pp_cargs cargs pp_mllam body
+      let pp_pat fmt = function
+        | ConstPattern i ->
+          Format.fprintf fmt "| %s "
+            (string_of_construct prefix ~constant:true ind i)
+        | NonConstPattern (tag,args) ->
+          Format.fprintf fmt "| %s%a "
+            (string_of_construct prefix ~constant:false ind tag) pp_cparams args in
+      let rec pp_pats fmt pats =
+        match pats with
+        | [] -> ()
+        | pat::pats ->
+          Format.fprintf fmt "%a%a" pp_pat pat pp_pats pats
       in
+      Format.fprintf fmt "%a ->@\n  %a@\n" pp_pats cargs pp_mllam body
+    in
     Array.iter pp_branch bs
 
   and pp_primitive fmt = function
@@ -1763,19 +1806,24 @@ let pp_global fmt g =
 	pp_mllam c
   | Gopen s ->
       Format.fprintf fmt "@[open %s@]@." s
-  | Gtype ((mind, i), lar) ->
-      let l = string_of_mind mind in
-      let rec aux s ar = 
-	if Int.equal ar 0 then s else aux (s^" * Nativevalues.t") (ar-1) in
-      let pp_const_sig i fmt j ar =
-        let sig_str = if ar > 0 then aux "of Nativevalues.t" (ar-1) else "" in
-        Format.fprintf fmt "  | Construct_%s_%i_%i %s@\n" l i j sig_str
-      in
-      let pp_const_sigs i fmt lar =
-        Format.fprintf fmt "  | Accu_%s_%i of Nativevalues.t@\n" l i;
-        Array.iteri (pp_const_sig i fmt) lar
-      in
-      Format.fprintf fmt "@[type ind_%s_%i =@\n%a@]@\n@." l i (pp_const_sigs i) lar
+  | Gtype (ind, lar) ->
+    let rec aux s arity =
+      if Int.equal arity 0 then s else aux (s^" * Nativevalues.t") (arity-1) in
+    let pp_const_sig fmt (tag,arity) =
+      if arity > 0 then
+        let sig_str = aux "of Nativevalues.t" (arity-1) in
+        let cstr = string_of_construct "" ~constant:false ind tag in
+        Format.fprintf fmt "  | %s %s@\n" cstr sig_str
+      else
+        let sig_str = if arity > 0 then aux "of Nativevalues.t" (arity-1) else "" in
+        let cstr = string_of_construct "" ~constant:true ind tag in
+        Format.fprintf fmt "  | %s %s@\n" cstr sig_str
+    in
+    let pp_const_sigs fmt lar =
+      Format.fprintf fmt "  | %s of Nativevalues.t@\n" (string_of_accu_construct "" ind);
+      Array.iter (pp_const_sig fmt) lar
+    in
+    Format.fprintf fmt "@[type ind_%s =@\n%a@]@\n@." (string_of_ind ind) pp_const_sigs lar
   | Gtblfixtype (g, params, t) ->
       Format.fprintf fmt "@[let %a %a =@\n  %a@]@\n@." pp_gname g
 	pp_ldecls params pp_array t
@@ -1912,7 +1960,7 @@ let compile_mind mb mind stack =
   (** Generate data for every block *)
   let f i stack ob =
     let ind = (mind, i) in
-    let gtype = Gtype(ind, Array.map snd ob.mind_reloc_tbl) in
+    let gtype = Gtype(ind, ob.mind_reloc_tbl) in
     let j = push_symbol (SymbInd ind) in
     let name = Gind ("", ind) in
     let accu =
@@ -1935,7 +1983,8 @@ let compile_mind mb mind stack =
                   asw_reloc = tbl; asw_finite = true } in
       let c_uid = fresh_lname Anonymous in
       let cf_uid = fresh_lname Anonymous in
-      let _, arity = tbl.(0) in
+      let tag, arity = tbl.(0) in
+      assert (arity > 0);
       let ci_uid = fresh_lname Anonymous in
       let cargs = Array.init arity
         (fun i -> if Int.equal i proj_arg then Some ci_uid else None)
@@ -1943,7 +1992,7 @@ let compile_mind mb mind stack =
       let i = push_symbol (SymbProj (ind, proj_arg)) in
       let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in
       let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in
-      let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
+      let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[NonConstPattern (tag,cargs)],MLlocal ci_uid|]) in
       let code = MLlet(cf_uid, mkForceCofix "" ind (MLlocal c_uid), code) in
       let gn = Gproj ("", ind, proj_arg) in
       Glet (gn, mkMLlam [|c_uid|] code) :: acc
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 40948244fb..62afd9df68 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -40,8 +40,8 @@ type lambda =
   | Lfix          of (int array * (string * inductive) array * int) * fix_decl
   | Lcofix        of int * fix_decl
   | Lint          of int (* a constant constructor *)
-  | Lmakeblock    of prefix * constructor * int * lambda array
-                  (* prefix, constructor Name.t, constructor tag, arguments *)
+  | Lmakeblock    of prefix * inductive * int * lambda array
+                  (* prefix, inductive name, constructor tag, arguments *)
         (* A fully applied non-constant constructor *)
   | Luint         of Uint63.t
   | Lval          of Nativevalues.t
@@ -50,7 +50,10 @@ type lambda =
   | Llazy
   | Lforce
 
-and lam_branches = (constructor * Name.t Context.binder_annot array * lambda) array
+and lam_branches =
+  { constant_branches : lambda array;
+    nonconstant_branches : (Name.t Context.binder_annot array * lambda) array;
+  }
 
 and fix_decl =  Name.t Context.binder_annot array * lambda array * lambda array
 
@@ -142,17 +145,26 @@ let map_lam_with_binders g f n lam =
   | Lprim(prefix,kn,op,args) ->
       let args' = Array.Smart.map (f n) args in
       if args == args' then lam else Lprim(prefix,kn,op,args')
-  | Lcase(annot,t,a,br) ->
-      let t' = f n t in
-      let a' = f n a in
-      let on_b b = 
-	let (cn,ids,body) = b in
-	let body' = 
-	  if Array.is_empty ids then f n body 
-	  else f (g (Array.length ids) n) body in
-	if body == body' then b else (cn,ids,body') in
-      let br' = Array.Smart.map on_b br in
-      if t == t' && a == a' && br == br' then lam else Lcase(annot,t',a',br')
+  | Lcase(annot,t,a,branches) ->
+    let const = branches.constant_branches in
+    let nonconst = branches.nonconstant_branches in
+    let t' = f n t in
+    let a' = f n a in
+    let const' = Array.Smart.map (f n) const in
+    let on_b b =
+      let (ids,body) = b in
+      let body' = f (g (Array.length ids) n) body in
+      if body == body' then b else (ids,body') in
+    let nonconst' = Array.Smart.map on_b nonconst in
+    let branches' =
+      if const == const' && nonconst == nonconst' then
+        branches
+      else
+        { constant_branches = const';
+          nonconstant_branches = nonconst' }
+    in
+    if t == t' && a == a' && branches == branches' then lam else
+      Lcase(annot,t',a',branches')
   | Lif(t,bt,bf) ->
       let t' = f n t in
       let bt' = f n bt in
@@ -333,20 +345,20 @@ let make_args start _end =
   Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i))
     
 (* Translation of constructors *)	
-let expand_constructor prefix cstr tag nparams arity =
+let expand_constructor prefix ind tag nparams arity =
   let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *)
   let ids = Array.make (nparams + arity) anon in
   if Int.equal arity 0 then mkLlam ids (Lint tag)
   else
   let args = make_args arity 1 in
-  Llam(ids, Lmakeblock (prefix, cstr, tag, args))
+  Llam(ids, Lmakeblock (prefix, ind, tag, args))
 
 (* [nparams] is the number of parameters still expected *)
-let makeblock env cn tag nparams arity args =
+let makeblock env ind tag nparams arity args =
   let nargs = Array.length args in
   if nparams > 0 || nargs < arity then
-    let prefix = get_mind_prefix env (fst (fst cn)) in
-    mkLapp (expand_constructor prefix cn tag nparams arity) args
+    let prefix = get_mind_prefix env (fst ind) in
+    mkLapp (expand_constructor prefix ind tag nparams arity) args
   else
   (* The constructor is fully applied *)
   if Int.equal arity 0 then Lint tag
@@ -355,8 +367,8 @@ let makeblock env cn tag nparams arity args =
     let args = Array.map get_value args in
     Lval (Nativevalues.mk_block tag args)
   else
-    let prefix = get_mind_prefix env (fst (fst cn)) in
-    Lmakeblock(prefix, cn, tag, args)
+    let prefix = get_mind_prefix env (fst ind) in
+    Lmakeblock(prefix, ind, tag, args)
 
 (* Translation of constants *)
 
@@ -432,8 +444,6 @@ let empty_evars =
   { evars_val = (fun _ -> None);
     evars_metas = (fun _ -> assert false) }
 
-let empty_ids = [||]
-
 (** Extract the inductive type over which a fixpoint is decreasing *)
 let rec get_fix_struct env i t = match kind (Reduction.whd_all env t) with
 | Prod (na, dom, t) ->
@@ -504,43 +514,51 @@ let rec lambda_of_constr cache env sigma c =
     let prefix = get_mind_prefix env (fst ind) in
     mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|]
 
-  | Case(ci,t,a,branches) ->  
-      let (mind,i as ind) = ci.ci_ind in
-      let mib = lookup_mind mind env in
-      let oib = mib.mind_packets.(i) in
-      let tbl = oib.mind_reloc_tbl in 
-      (* Building info *)
-      let prefix = get_mind_prefix env mind in
-      let annot_sw = 
-	    { asw_ind = ind;
-          asw_ci = ci;
-          asw_reloc = tbl; 
-          asw_finite = mib.mind_finite <> CoFinite;
-          asw_prefix = prefix}
-      in
-      (* translation of the argument *)
-      let la = lambda_of_constr cache env sigma a in
-      (* translation of the type *)
-      let lt = lambda_of_constr cache env sigma t in
-      (* translation of branches *)
-      let mk_branch i b =
-	let cn = (ind,i+1) in
-	let _, arity = tbl.(i) in
-        let b = lambda_of_constr cache env sigma b in
-	if Int.equal arity 0 then (cn, empty_ids, b)
-	else 
-	  match b with
-	  | Llam(ids, body) when Int.equal (Array.length ids) arity -> (cn, ids, body)
+  | Case(ci,t,a,branches) ->
+    let (mind,i as ind) = ci.ci_ind in
+    let mib = lookup_mind mind env in
+    let oib = mib.mind_packets.(i) in
+    let tbl = oib.mind_reloc_tbl in
+    (* Building info *)
+    let prefix = get_mind_prefix env mind in
+    let annot_sw =
+      { asw_ind = ind;
+        asw_ci = ci;
+        asw_reloc = tbl;
+        asw_finite = mib.mind_finite <> CoFinite;
+        asw_prefix = prefix}
+    in
+    (* translation of the argument *)
+    let la = lambda_of_constr cache env sigma a in
+    (* translation of the type *)
+    let lt = lambda_of_constr cache env sigma t in
+    (* translation of branches *)
+    let dummy = Lrel(Anonymous,0) in
+    let consts = Array.make oib.mind_nb_constant dummy in
+    let blocks = Array.make oib.mind_nb_args ([||],dummy) in
+    let rtbl = oib.mind_reloc_tbl in
+    for i = 0 to Array.length rtbl - 1 do
+      let tag, arity = rtbl.(i) in
+      let b = lambda_of_constr cache env sigma branches.(i) in
+      if arity = 0 then consts.(tag) <- b
+      else
+        let b =
+          match b with
+          | Llam(ids, body) when Array.length ids = arity -> (ids, body)
           | _ ->
-              (** TODO relevance *)
-              let anon = Context.make_annot Anonymous Sorts.Relevant in
-              let ids = Array.make arity anon in
-	      let args = make_args arity 1 in
-	      let ll = lam_lift arity b in
-	      (cn, ids, mkLapp  ll args) in
-      let bs = Array.mapi mk_branch branches in
-      Lcase(annot_sw, lt, la, bs)
-	
+            let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *)
+            let ids = Array.make arity anon in
+            let args = make_args arity 1 in
+            let ll = lam_lift arity b in
+            (ids, mkLapp  ll args)
+        in blocks.(tag-1) <- b
+    done;
+    let branches =
+      { constant_branches = consts;
+        nonconstant_branches = blocks }
+    in
+    Lcase(annot_sw, lt, la, branches)
+
   | Fix((pos, i), (names,type_bodies,rec_bodies)) ->
       let ltypes = lambda_of_args cache env sigma 0 type_bodies in
       let map i t =
@@ -584,13 +602,13 @@ and lambda_of_app cache env sigma f args =
           let prefix = get_const_prefix env kn in
           mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args cache env sigma 0 args)
       end
-  | Construct (c,_) ->
+  | Construct ((ind,_ as c),_) ->
     let tag, nparams, arity = Cache.get_construct_info cache env c in
     let nargs = Array.length args in
     if nparams < nargs then (* got all parameters *)
       let args = lambda_of_args cache env sigma nparams args in
-      makeblock env c tag 0 arity args
-    else makeblock env c tag (nparams - nargs) arity empty_args
+      makeblock env ind tag 0 arity args
+    else makeblock env ind tag (nparams - nargs) arity empty_args
   | _ -> 
       let f = lambda_of_constr cache env sigma f in
       let args = lambda_of_args cache env sigma 0 args in
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 093665df9b..446df1a1ea 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -34,8 +34,8 @@ type lambda =
   | Lfix          of (int array * (string * inductive) array * int) * fix_decl
   | Lcofix        of int * fix_decl
   | Lint          of int (* a constant constructor *)
-  | Lmakeblock    of prefix * constructor * int * lambda array
-                  (* prefix, constructor Name.t, constructor tag, arguments *)
+  | Lmakeblock    of prefix * inductive * int * lambda array
+                  (* prefix, inductive name, constructor tag, arguments *)
         (* A fully applied non-constant constructor *)
   | Luint         of Uint63.t
   | Lval          of Nativevalues.t
@@ -44,7 +44,10 @@ type lambda =
   | Llazy
   | Lforce
 
-and lam_branches = (constructor * Name.t Context.binder_annot array * lambda) array
+and lam_branches =
+  { constant_branches : lambda array;
+    nonconstant_branches : (Name.t Context.binder_annot array * lambda) array;
+  }
 
 and fix_decl =  Name.t Context.binder_annot array * lambda array * lambda array