aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativecode.ml')
-rw-r--r--kernel/nativecode.ml62
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 16:02:23 +0000