Removing a redundant universe instance information in native compute.

Global declarations used to carry universe instances with them, but it
turns out this information is not used anywhere. Instead, instances were
already properly encoded as the first argument of polymorphic definitions.

1 files changed, 30 insertions, 32 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index eb238941b..1acede729 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -48,9 +48,9 @@ let fresh_lname n =
 
 (** Global names **)
 type gname = 
-  | Gind of string * pinductive (* prefix, inductive name *)
-  | Gconstruct of string * pconstructor (* prefix, constructor name *)
-  | Gconstant of string * pconstant (* prefix, constant name *)
+  | Gind of string * inductive (* prefix, inductive name *)
+  | Gconstruct of string * constructor (* prefix, constructor name *)
+  | Gconstant of string * constant (* prefix, constant name *)
   | Gproj of string * constant (* prefix, constant name *)
   | Gcase of label option * int
   | Gpred of label option * int
@@ -64,11 +64,11 @@ type gname =
 let eq_gname gn1 gn2 =
   match gn1, gn2 with
   | Gind (s1, ind1), Gind (s2, ind2) ->
-     String.equal s1 s2 && Univ.eq_puniverses eq_ind ind1 ind2
+     String.equal s1 s2 && eq_ind ind1 ind2
   | Gconstruct (s1, c1), Gconstruct (s2, c2) ->
-      String.equal s1 s2 && Univ.eq_puniverses eq_constructor c1 c2
+      String.equal s1 s2 && eq_constructor c1 c2
   | Gconstant (s1, c1), Gconstant (s2, c2) ->
-      String.equal s1 s2 && Univ.eq_puniverses Constant.equal c1 c2
+      String.equal s1 s2 && Constant.equal c1 c2
   | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2
   | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2
   | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2
@@ -92,12 +92,12 @@ let dummy_gname =
 open Hashset.Combine
 
 let gname_hash gn = match gn with
-| Gind (s, (ind,u)) ->
-   combinesmall 1 (combine3 (String.hash s) (ind_hash ind) (Univ.Instance.hash u))
-| Gconstruct (s, (c,u)) ->
-   combinesmall 2 (combine3 (String.hash s) (constructor_hash c) (Univ.Instance.hash u))
-| Gconstant (s, (c,u)) ->
-   combinesmall 3 (combine3 (String.hash s) (Constant.hash c) (Univ.Instance.hash u))
+| Gind (s, ind) ->
+   combinesmall 1 (combine (String.hash s) (ind_hash ind))
+| Gconstruct (s, c) ->
+   combinesmall 2 (combine (String.hash s) (constructor_hash c))
+| Gconstant (s, c) ->
+   combinesmall 3 (combine (String.hash s) (Constant.hash c))
 | Gcase (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i))
 | Gpred (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i))
 | Gfixtype (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i))
@@ -1068,9 +1068,9 @@ let ml_of_instance instance u =
       MLlet(lname,def,body)
   | Lapp(f,args) ->
       MLapp(ml_of_lam env l f, Array.map (ml_of_lam env l) args)
-  | Lconst (prefix,c) ->
-     let args = ml_of_instance env.env_univ (snd c) in
-     mkMLapp (MLglobal(Gconstant (prefix,c))) args
+  | Lconst (prefix, (c, u)) ->
+     let args = ml_of_instance env.env_univ u in
+     mkMLapp (MLglobal(Gconstant (prefix, c))) args
   | Lproj (prefix,c) -> MLglobal(Gproj (prefix,c))
   | Lprim _ ->
       let decl,cond,paux = extract_prim (ml_of_lam env l) t in
@@ -1281,17 +1281,17 @@ let ml_of_instance instance u =
      MLconstruct(prefix,cn,args)
   | Lconstruct (prefix, (cn,u)) ->
      let uargs = ml_of_instance env.env_univ u in
-      mkMLapp (MLglobal (Gconstruct (prefix, (cn,u)))) uargs
+      mkMLapp (MLglobal (Gconstruct (prefix, cn))) uargs
   | Luint v ->
      (match v with
      | UintVal i -> MLapp(MLprimitive Mk_uint, [|MLuint i|])
      | UintDigits (prefix,cn,ds) ->
-	let c = MLglobal (Gconstruct (prefix, (cn, Univ.Instance.empty))) in
+	let c = MLglobal (Gconstruct (prefix, cn)) in
 	let ds = Array.map (ml_of_lam env l) ds in
 	let i31 = MLapp (MLprimitive Mk_I31_accu, [|c|]) in
 	MLapp(i31, ds)
      | UintDecomp (prefix,cn,t) ->
-	let c = MLglobal (Gconstruct (prefix, (cn, Univ.Instance.empty))) in
+	let c = MLglobal (Gconstruct (prefix, cn)) in
 	let t = ml_of_lam env l t in
 	MLapp (MLprimitive Decomp_uint, [|c;t|]))
   | Lval v ->
@@ -1304,9 +1304,9 @@ let ml_of_instance instance u =
     in
     let uarg = MLapp(MLprimitive MLmagic, [|uarg|]) in
     MLapp(MLprimitive Mk_sort, [|get_sort_code i; uarg|])
-  | Lind (prefix, pind) ->
-     let uargs = ml_of_instance env.env_univ (snd pind) in
-     mkMLapp (MLglobal (Gind (prefix, pind))) uargs
+  | Lind (prefix, (ind, u)) ->
+     let uargs = ml_of_instance env.env_univ u in
+     mkMLapp (MLglobal (Gind (prefix, ind))) uargs
   | Llazy -> MLglobal (Ginternal "lazy")
   | Lforce -> MLglobal (Ginternal "Lazy.force")
 
@@ -1539,11 +1539,11 @@ let string_of_mind mind = string_of_kn (user_mind mind)
 
 let string_of_gname g =
   match g with
-  | Gind (prefix, ((mind,i), _)) ->
+  | Gind (prefix, (mind, i)) ->
       Format.sprintf "%sindaccu_%s_%i" prefix (string_of_mind mind) i
-  | Gconstruct (prefix, (((mind, i), j), _)) ->
+  | Gconstruct (prefix, ((mind, i), j)) ->
       Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1)
-  | Gconstant (prefix, (c,_)) ->
+  | Gconstant (prefix, c) ->
       Format.sprintf "%sconst_%s" prefix (string_of_con c)
   | Gproj (prefix, c) ->
       Format.sprintf "%sproj_%s" prefix (string_of_con c)
@@ -1754,9 +1754,8 @@ let pp_mllam fmt l =
     | Coq_primitive (op,None) ->
        Format.fprintf fmt "no_check_%s" (Primitives.to_string op)
     | Coq_primitive (op, Some (prefix,kn)) ->
-       let u = Univ.Instance.empty in
         Format.fprintf fmt "%s %a" (Primitives.to_string op)
-		       pp_mllam (MLglobal (Gconstant (prefix,(kn,u))))
+		       pp_mllam (MLglobal (Gconstant (prefix, kn)))
   in
   Format.fprintf fmt "@[%a@]" pp_mllam l
   
@@ -1888,7 +1887,7 @@ let compile_constant env sigma prefix ~interactive con cb =
       in
       if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code");
       let code =
-        optimize_stk (Glet(Gconstant ("",(con,u)),code)::auxdefs)
+        optimize_stk (Glet(Gconstant ("", con),code)::auxdefs)
       in
       if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code");
       code, name
@@ -1901,12 +1900,11 @@ let compile_constant env sigma prefix ~interactive con cb =
 	(*
 	let t = mkMLlam [|univ|] (mkMLapp (MLprimitive Mk_const)
 	 *)
-        [Glet(Gconstant ("",(con,u)), mkMLapp (MLprimitive Mk_const) args)],
+        [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)],
 	  if interactive then LinkedInteractive prefix
 	  else Linked prefix
     end
   | Some pb ->
-      let u = Univ.Instance.empty in
       let mind = pb.proj_ind in
       let ind = (mind,0) in
       let mib = lookup_mind mind env in
@@ -1933,7 +1931,7 @@ let compile_constant env sigma prefix ~interactive con cb =
       let gn = Gproj ("",con) in
       let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in
       let arg = fargs.(pb.proj_npars) in
-        Glet(Gconstant ("",(con,u)), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal
+        Glet(Gconstant ("", con), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal
           arg|])))::
             [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix
 
@@ -1965,7 +1963,7 @@ let compile_mind prefix ~interactive mb mind stack =
   let f i stack ob =
     let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in
     let j = push_symbol (SymbInd (mind,i)) in
-    let name = Gind ("", ((mind, i), u)) in
+    let name = Gind ("", (mind, i)) in
     let accu =
       let args =
 	if Univ.Instance.is_empty u then
@@ -1980,7 +1978,7 @@ let compile_mind prefix ~interactive mb mind stack =
     let add_construct j acc (_,arity) = 
       let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in 
       let c = (mind,i), (j+1) in
-	  Glet(Gconstruct ("",(c,u)),
+	  Glet(Gconstruct ("", c),
 	     mkMLlam (Array.append params args)
 	       (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc
     in