aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2015-01-16 22:17:03 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-01-17 08:02:45 +0100
commit9f5586d88880cbb98c92edfe9c33c76564f1a19c (patch)
tree6de2a171eff5706b0e4ce9268554b84a922f12b3
parent4985f0ff99278beb3b934f86edf1398659c611a8 (diff)
Make native compiler handle universe polymorphic definitions.
One remaining issue: aliased constants raise an anomaly when some unsubstituted universe variables remain. VM may suffer from the same problem.
-rw-r--r--kernel/declareops.ml10
-rw-r--r--kernel/declareops.mli5
-rw-r--r--kernel/inductive.ml15
-rw-r--r--kernel/inductive.mli2
-rw-r--r--kernel/nativecode.ml242
-rw-r--r--kernel/nativecode.mli2
-rw-r--r--kernel/nativeconv.ml81
-rw-r--r--kernel/nativeinstr.mli8
-rw-r--r--kernel/nativelambda.ml26
-rw-r--r--kernel/nativevalues.ml21
-rw-r--r--kernel/nativevalues.mli10
-rw-r--r--kernel/subtyping.ml1
-rw-r--r--kernel/univ.ml4
-rw-r--r--kernel/univ.mli4
-rw-r--r--pretyping/nativenorm.ml8
-rw-r--r--tactics/elimschemes.ml4
-rw-r--r--toplevel/record.ml2
-rw-r--r--toplevel/search.ml2
18 files changed, 285 insertions, 162 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index d5df24a1a..48a6098ee 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -260,6 +260,16 @@ let subst_mind_body sub mib =
mind_universes = mib.mind_universes;
mind_private = mib.mind_private }
+let inductive_instance mib =
+ if mib.mind_polymorphic then
+ Univ.UContext.instance mib.mind_universes
+ else Univ.Instance.empty
+
+let inductive_context mib =
+ if mib.mind_polymorphic then
+ Univ.instantiate_univ_context mib.mind_universes
+ else Univ.UContext.empty
+
(** {6 Hash-consing of inductive declarations } *)
let hcons_regular_ind_arity a =
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 02090ade5..47a82cc6c 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -8,6 +8,8 @@
open Declarations
open Mod_subst
+open Univ
+open Context
(** Operations concerning types in [Declarations] :
[constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -75,6 +77,9 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
+val inductive_instance : mutual_inductive_body -> universe_instance
+val inductive_context : mutual_inductive_body -> universe_context
+
(** {6 Hash-consing} *)
(** Here, strictly speaking, we don't perform true hash-consing
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index fee510e96..bb57ad256 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -53,20 +53,11 @@ let inductive_params (mib,_) = mib.mind_nparams
let inductive_paramdecls (mib,u) =
Vars.subst_instance_context u mib.mind_params_ctxt
-let inductive_instance mib =
- if mib.mind_polymorphic then
- UContext.instance mib.mind_universes
- else Instance.empty
-
-let inductive_context mib =
- if mib.mind_polymorphic then
- instantiate_univ_context mib.mind_universes
- else UContext.empty
-
let instantiate_inductive_constraints mib u =
if mib.mind_polymorphic then
- subst_instance_constraints u (UContext.constraints mib.mind_universes)
- else Constraint.empty
+ Univ.subst_instance_constraints u (Univ.UContext.constraints mib.mind_universes)
+ else Univ.Constraint.empty
+
(************************************************************************)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 9a321e5ca..5847d25f6 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -35,8 +35,6 @@ val lookup_mind_specif : env -> inductive -> mind_specif
(** {6 Functions to build standard types related to inductive } *)
val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list
-val inductive_instance : mutual_inductive_body -> universe_instance
-val inductive_context : mutual_inductive_body -> universe_context
val inductive_paramdecls : mutual_inductive_body puniverses -> rel_context
val instantiate_inductive_constraints :
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 66577fecc..1a4a4b54d 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -45,9 +45,9 @@ let fresh_lname n =
(** Global names **)
type gname =
- | Gind of string * inductive (* prefix, inductive name *)
- | Gconstruct of string * constructor (* prefix, constructor name *)
- | Gconstant of string * constant (* prefix, constant name *)
+ | Gind of string * pinductive (* prefix, inductive name *)
+ | Gconstruct of string * pconstructor (* prefix, constructor name *)
+ | Gconstant of string * pconstant (* prefix, constant name *)
| Gproj of string * constant (* prefix, constant name *)
| Gcase of label option * int
| Gpred of label option * int
@@ -60,11 +60,12 @@ type gname =
let eq_gname gn1 gn2 =
match gn1, gn2 with
- | Gind (s1, ind1), Gind (s2, ind2) -> String.equal s1 s2 && eq_ind ind1 ind2
+ | Gind (s1, ind1), Gind (s2, ind2) ->
+ String.equal s1 s2 && Univ.eq_puniverses eq_ind ind1 ind2
| Gconstruct (s1, c1), Gconstruct (s2, c2) ->
- String.equal s1 s2 && eq_constructor c1 c2
+ String.equal s1 s2 && Univ.eq_puniverses eq_constructor c1 c2
| Gconstant (s1, c1), Gconstant (s2, c2) ->
- String.equal s1 s2 && Constant.equal c1 c2
+ String.equal s1 s2 && Univ.eq_puniverses 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
@@ -85,9 +86,12 @@ let eq_gname gn1 gn2 =
open Hashset.Combine
let gname_hash gn = match gn with
-| Gind (s, i) -> combinesmall 1 (combine (String.hash s) (ind_hash i))
-| Gconstruct (s, c) -> combinesmall 2 (combine (String.hash s) (constructor_hash c))
-| Gconstant (s, c) -> combinesmall 3 (combine (String.hash s) (Constant.hash c))
+| 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))
| 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))
@@ -149,6 +153,7 @@ type symbol =
| SymbInd of inductive
| SymbMeta of metavariable
| SymbEvar of existential
+ | SymbLevel of Univ.Level.t
let dummy_symb = SymbValue (dummy_value ())
@@ -163,6 +168,7 @@ let eq_symbol sy1 sy2 =
| SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2
| SymbEvar (evk1,args1), SymbEvar (evk2,args2) ->
Evar.equal evk1 evk2 && Array.for_all2 eq_constr args1 args2
+ | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2
| _, _ -> false
let hash_symbol symb =
@@ -178,6 +184,7 @@ let hash_symbol symb =
let evh = Evar.hash evk in
let hl = Array.fold_left (fun h t -> combine h (Constr.hash t)) evh args in
combinesmall 8 hl
+ | SymbLevel l -> combinesmall 9 (Univ.Level.hash l)
module HashedTypeSymbol = struct
type t = symbol
@@ -231,6 +238,11 @@ let get_evar tbl i =
| SymbEvar ev -> ev
| _ -> anomaly (Pp.str "get_evar failed")
+let get_level tbl i =
+ match tbl.(i) with
+ | SymbLevel u -> u
+ | _ -> anomaly (Pp.str "get_level failed")
+
let push_symbol x =
try HashtblSymbol.find symb_tbl x
with Not_found ->
@@ -282,6 +294,8 @@ type primitive =
| MLsub
| MLmul
| MLmagic
+ | MLarrayget
+ | Mk_empty_instance
| Coq_primitive of Primitives.t * (prefix * constant) option
let eq_primitive p1 p2 =
@@ -302,6 +316,7 @@ let eq_primitive p1 p2 =
| Mk_meta, Mk_meta -> true
| Mk_evar, Mk_evar -> true
| Mk_proj, Mk_proj -> true
+ | MLarrayget, MLarrayget -> true
| _ -> false
@@ -350,6 +365,8 @@ let primitive_hash = function
| Coq_primitive (prim, Some (prefix,kn)) ->
combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (Primitives.hash prim))
| Mk_proj -> 38
+ | MLarrayget -> 39
+ | Mk_empty_instance -> 40
type mllambda =
| MLlocal of lname
@@ -368,6 +385,7 @@ type mllambda =
| MLuint of Uint31.t
| MLsetref of string * mllambda
| MLsequence of mllambda * mllambda
+ | MLarray of mllambda array
and mllam_branches = ((constructor * lname option array) list * mllambda) array
@@ -429,10 +447,13 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
| MLsetref (id1, ml1), MLsetref (id2, ml2) ->
String.equal id1 id2 &&
eq_mllambda gn1 gn2 n env1 env2 ml1 ml2
- | MLsequence (ml1, ml'1), MLsequence (ml2, ml'2) ->
- eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 &&
- eq_mllambda gn1 gn2 n env1 env2 ml'1 ml'2
- | _, _ -> false
+ | MLsequence (ml1, ml'1), MLsequence (ml2, ml'2) ->
+ eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 &&
+ eq_mllambda gn1 gn2 n env1 env2 ml'1 ml'2
+ | MLarray arr1, MLarray arr2 ->
+ Array.equal (eq_mllambda gn1 gn2 n env1 env2) arr1 arr2
+
+ | _, _ -> false
and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 =
let eq_def (_,args1,ml1) (_,args2,ml2) =
@@ -505,6 +526,8 @@ let rec hash_mllambda gn n env t =
let hml = hash_mllambda gn n env ml in
let hml' = hash_mllambda gn n env ml' in
combinesmall 14 (combine hml hml')
+ | MLarray arr ->
+ combinesmall 15 (hash_mllambda_array gn n env 1 arr)
and hash_mllambda_letrec gn n env init defs =
let hash_def (_,args,ml) =
@@ -569,7 +592,9 @@ let fv_lam l =
| 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) in
+ | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv)
+ | MLarray arr -> Array.fold_right (fun a fv -> aux a bind fv) arr fv
+ in
aux l LNset.empty LNset.empty
@@ -698,13 +723,15 @@ type env =
env_bound : int; (* length of env_rel *)
(* free variables *)
env_urel : (int * mllambda) list ref; (* list of unbound rel *)
- env_named : (identifier * mllambda) list ref }
+ env_named : (identifier * mllambda) list ref;
+ env_univ : lname option}
-let empty_env () =
+let empty_env univ () =
{ env_rel = [];
env_bound = 0;
env_urel = ref [];
- env_named = ref []
+ env_named = ref [];
+ env_univ = univ
}
let push_rel env id =
@@ -741,7 +768,10 @@ let get_var env id =
let local = MLlocal (fresh_lname (Name id)) in
env.env_named := (id, local)::!(env.env_named);
local
-
+
+let fresh_univ () =
+ fresh_lname (Name (Id.of_string "univ"))
+
(*s Traduction of lambda to mllambda *)
let get_prod_name codom =
@@ -754,14 +784,18 @@ let get_lname (_,l) =
| MLlocal id -> id
| _ -> invalid_arg "Nativecode.get_lname"
+(* Collects free variables from env in an array of local names *)
let fv_params env =
let fvn, fvr = !(env.env_named), !(env.env_urel) in
let size = List.length fvn + List.length fvr in
- if Int.equal size 0 then empty_params
+ let start,params = match env.env_univ with
+ | None -> 0, Array.make size dummy_lname
+ | Some u -> 1, let t = Array.make (size + 1) dummy_lname in t.(0) <- u; t
+ in
+ if Array.is_empty params then empty_params
else begin
- let params = Array.make size dummy_lname in
let fvn = ref fvn in
- let i = ref 0 in
+ let i = ref start in
while not (List.is_empty !fvn) do
params.(!i) <- get_lname (List.hd !fvn);
fvn := List.tl !fvn;
@@ -783,12 +817,15 @@ let empty_args = [||]
let fv_args env fvn fvr =
let size = List.length fvn + List.length fvr in
- if Int.equal size 0 then empty_args
+ let start,args = match env.env_univ with
+ | None -> 0, Array.make size (MLint 0)
+ | Some u -> 1, let t = Array.make (size + 1) (MLint 0) in t.(0) <- MLlocal u; t
+ in
+ if Array.is_empty args then empty_args
else
begin
- let args = Array.make size (MLint 0) in
let fvn = ref fvn in
- let i = ref 0 in
+ let i = ref start in
while not (List.is_empty !fvn) do
args.(!i) <- get_var env (fst (List.hd !fvn));
fvn := List.tl !fvn;
@@ -837,6 +874,10 @@ let get_evar_code i =
MLapp (MLglobal (Ginternal "get_evar"),
[|MLglobal symbols_tbl_name; MLint i|])
+let get_level_code i =
+ MLapp (MLglobal (Ginternal "get_level"),
+ [|MLglobal symbols_tbl_name; MLint i|])
+
type rlist =
| Rnil
| Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist'
@@ -978,6 +1019,19 @@ let compile_prim decl cond paux =
List.fold_left (fun body (x,d) -> MLlet(x,d,body)) body decl in
add_decl decl (compile_cond cond paux)
+let ml_of_instance instance u =
+ let ml_of_level l =
+ match Univ.Level.var_index l with
+ | Some i ->
+ let univ = MLapp(MLprimitive MLmagic, [|MLlocal (Option.get instance)|]) in
+ mkMLapp (MLprimitive MLarrayget) [|univ; MLint i|]
+ | None -> let i = push_symbol (SymbLevel l) in get_level_code i
+ in
+ let u = Univ.Instance.to_array u in
+ if Array.is_empty u then [||]
+ else let u = Array.map ml_of_level u in
+ [|MLapp (MLprimitive MLmagic, [|MLarray u|])|]
+
let rec ml_of_lam env l t =
match t with
| Lrel(id ,i) -> get_rel env id i
@@ -1007,7 +1061,9 @@ let compile_prim decl cond paux =
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) -> MLglobal(Gconstant (prefix,c))
+ | Lconst (prefix,c) ->
+ let args = ml_of_instance env.env_univ (snd c) 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
@@ -1023,20 +1079,21 @@ let compile_prim decl cond paux =
(* Remark: if we do not want to compile the predicate we
should a least compute the fv, then store the lambda representation
of the predicate (not the mllambda) *)
- let env_p = empty_env () in
+ let env_p = empty_env env.env_univ () in
let pn = fresh_gpred l in
let mlp = ml_of_lam env_p l p in
let mlp = generalize_fv env_p mlp in
let (pfvn,pfvr) = !(env_p.env_named), !(env_p.env_urel) in
let pn = push_global_let pn mlp in
(* Compilation of the case *)
- let env_c = empty_env () in
+ let env_c = empty_env env.env_univ () in
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 = push_rels env_c params in
- (c, lnames, ml_of_lam env l body) in
+ let lnames, env_c = push_rels env_c params in
+ (c, 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 *)
@@ -1080,7 +1137,7 @@ let compile_prim decl cond paux =
start
*)
(* Compilation of type *)
- let env_t = empty_env () in
+ let env_t = empty_env env.env_univ () in
let ml_t = Array.map (ml_of_lam env_t l) tt in
let params_t = fv_params env_t in
let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in
@@ -1089,7 +1146,7 @@ let compile_prim decl cond paux =
let mk_type = MLapp(MLglobal gft, args_t) in
(* Compilation of norm_i *)
let ndef = Array.length ids in
- let lf,env_n = push_rels (empty_env ()) ids in
+ let lf,env_n = push_rels (empty_env env.env_univ ()) ids in
let t_params = Array.make ndef [||] in
let t_norm_f = Array.make ndef (Gnorm (l,-1)) in
let mk_let envi (id,def) t = MLlet (id,def,t) in
@@ -1145,7 +1202,7 @@ let compile_prim decl cond paux =
MLletrec(Array.mapi mkrec lf, lf_args.(start))
| Lcofix (start, (ids, tt, tb)) ->
(* Compilation of type *)
- let env_t = empty_env () in
+ let env_t = empty_env env.env_univ () in
let ml_t = Array.map (ml_of_lam env_t l) tt in
let params_t = fv_params env_t in
let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in
@@ -1154,7 +1211,7 @@ let compile_prim decl cond paux =
let mk_type = MLapp(MLglobal gft, args_t) in
(* Compilation of norm_i *)
let ndef = Array.length ids in
- let lf,env_n = push_rels (empty_env ()) ids in
+ let lf,env_n = push_rels (empty_env env.env_univ ()) ids in
let t_params = Array.make ndef [||] in
let t_norm_f = Array.make ndef (Gnorm (l,-1)) in
let ml_of_fix i body =
@@ -1212,33 +1269,42 @@ let compile_prim decl cond paux =
(lname, paramsi, body) in
MLletrec(Array.mapi mkrec lf, lf_args.(start)) *)
- | Lmakeblock (prefix,cn,_,args) ->
- MLconstruct(prefix,cn,Array.map (ml_of_lam env l) args)
- | Lconstruct (prefix, cn) ->
- MLglobal (Gconstruct (prefix, cn))
+ | Lmakeblock (prefix,(cn,u),_,args) ->
+ let args = Array.map (ml_of_lam env l) args in
+ 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
| Luint v ->
(match v with
| UintVal i -> MLapp(MLprimitive Mk_uint, [|MLuint i|])
| UintDigits (prefix,cn,ds) ->
- let c = MLglobal (Gconstruct (prefix, cn)) in
+ let c = MLglobal (Gconstruct (prefix, (cn, Univ.Instance.empty))) 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)) in
+ let c = MLglobal (Gconstruct (prefix, (cn, Univ.Instance.empty))) in
let t = ml_of_lam env l t in
MLapp (MLprimitive Decomp_uint, [|c;t|]))
| Lval v ->
let i = push_symbol (SymbValue v) in get_value_code i
| Lsort s ->
let i = push_symbol (SymbSort s) in
- MLapp(MLprimitive Mk_sort, [|get_sort_code i|])
- | Lind (prefix, ind) -> MLglobal (Gind (prefix, ind))
+ let uarg = match env.env_univ with
+ | None -> MLarray [||]
+ | Some u -> MLlocal 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
| Llazy -> MLglobal (Ginternal "lazy")
| Lforce -> MLglobal (Ginternal "Lazy.force")
-let mllambda_of_lambda auxdefs l t =
- let env = empty_env () in
+let mllambda_of_lambda univ auxdefs l t =
+ let env = empty_env univ () in
global_stack := auxdefs;
let ml = ml_of_lam env l t in
let fv_rel = !(env.env_urel) in
@@ -1285,6 +1351,7 @@ let subst s l =
| MLconstruct(prefix,c,args) -> MLconstruct(prefix,c,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)
in
aux l
@@ -1391,6 +1458,7 @@ let optimize gdef l =
MLconstruct(prefix,c,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)
in
optimize LNmap.empty l
@@ -1462,11 +1530,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)
@@ -1544,6 +1612,17 @@ let pp_mllam fmt l =
Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body
| MLsequence(l1,l2) ->
Format.fprintf fmt "@[%a;@\n%a@]" pp_mllam l1 pp_mllam l2
+ | MLarray arr ->
+ let len = Array.length arr in
+ Format.fprintf fmt "@[[|";
+ if 0 < len then begin
+ for i = 0 to len - 2 do
+ Format.fprintf fmt "%a;" pp_mllam arr.(i)
+ done;
+ pp_mllam fmt arr.(len-1)
+ end;
+ Format.fprintf fmt "|]@]"
+
and pp_letrec fmt defs =
let len = Array.length defs in
@@ -1662,11 +1741,14 @@ let pp_mllam fmt l =
| MLsub -> Format.fprintf fmt "(-)"
| MLmul -> Format.fprintf fmt "( * )"
| MLmagic -> Format.fprintf fmt "Obj.magic"
+ | MLarrayget -> Format.fprintf fmt "Array.get"
+ | Mk_empty_instance -> Format.fprintf fmt "Univ.Instance.empty"
| 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)))
+ pp_mllam (MLglobal (Gconstant (prefix,(kn,u))))
in
Format.fprintf fmt "@[%a@]" pp_mllam l
@@ -1717,18 +1799,18 @@ let pp_global fmt g =
Format.fprintf fmt "@[(* %s *)@]@." s
(** Compilation of elements in environment **)
-let rec compile_with_fv env sigma auxdefs l t =
- let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda auxdefs l t in
+let rec compile_with_fv env sigma univ auxdefs l t =
+ let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda univ auxdefs l t in
if List.is_empty fv_named && List.is_empty fv_rel then (auxdefs,ml)
- else apply_fv env sigma (fv_named,fv_rel) auxdefs ml
+ else apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml
-and apply_fv env sigma (fv_named,fv_rel) auxdefs ml =
+and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
let get_rel_val (n,_) auxdefs =
(*
match !(lookup_rel_native_val n env) with
| NVKnone ->
*)
- compile_rel env sigma auxdefs n
+ compile_rel env sigma univ auxdefs n
(* | NVKvalue (v,d) -> assert false *)
in
let get_named_val (id,_) auxdefs =
@@ -1736,7 +1818,7 @@ and apply_fv env sigma (fv_named,fv_rel) auxdefs ml =
match !(lookup_named_native_val id env) with
| NVKnone ->
*)
- compile_named env sigma auxdefs id
+ compile_named env sigma univ auxdefs id
(* | NVKvalue (v,d) -> assert false *)
in
let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in
@@ -1747,23 +1829,23 @@ and apply_fv env sigma (fv_named,fv_rel) auxdefs ml =
let aux_name = fresh_lname Anonymous in
auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named)))
-and compile_rel env sigma auxdefs n =
+and compile_rel env sigma univ auxdefs n =
let (_,body,_) = lookup_rel n env.env_rel_context in
let n = rel_context_length env.env_rel_context - n in
match body with
| Some t ->
let code = lambda_of_constr env sigma t in
- let auxdefs,code = compile_with_fv env sigma auxdefs None code in
+ let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in
Glet(Grel n, code)::auxdefs
| None ->
Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs
-and compile_named env sigma auxdefs id =
+and compile_named env sigma univ auxdefs id =
let (_,body,_) = lookup_named id env.env_named_context in
match body with
| Some t ->
let code = lambda_of_constr env sigma t in
- let auxdefs,code = compile_with_fv env sigma auxdefs None code in
+ let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in
Glet(Gnamed id, code)::auxdefs
| None ->
Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
@@ -1771,8 +1853,12 @@ and compile_named env sigma auxdefs id =
let compile_constant env sigma prefix ~interactive con cb =
match cb.const_proj with
| None ->
+ let u =
+ if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
+ else Univ.Instance.empty
+ in
begin match cb.const_body with
- | Def t when not cb.const_polymorphic ->
+ | Def t ->
let t = Mod_subst.force_constr t in
let code = lambda_of_constr env sigma t in
if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code");
@@ -1783,20 +1869,34 @@ let compile_constant env sigma prefix ~interactive con cb =
else Linked prefix
in
let l = con_label con in
- let auxdefs,code = compile_with_fv env sigma [] (Some l) code in
+ let auxdefs,code =
+ if Univ.Instance.is_empty u then compile_with_fv env sigma None [] (Some l) code
+ else
+ let univ = fresh_univ () in
+ let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in
+ (auxdefs,mkMLlam [|univ|] code)
+ in
if !Flags.debug then Pp.msg_debug (Pp.str "Generated mllambda code");
let code =
- optimize_stk (Glet(Gconstant ("",con),code)::auxdefs)
+ optimize_stk (Glet(Gconstant ("",(con,u)),code)::auxdefs)
in
if !Flags.debug then Pp.msg_debug (Pp.str "Optimized mllambda code");
code, name
| _ ->
let i = push_symbol (SymbConst con) in
- [Glet(Gconstant ("",con), MLapp (MLprimitive Mk_const, [|get_const_code i|]))],
+ let args =
+ if Univ.Instance.is_empty u then [|get_const_code i; MLarray [||]|]
+ else [|get_const_code i|]
+ in
+ (*
+ let t = mkMLlam [|univ|] (mkMLapp (MLprimitive Mk_const)
+ *)
+ [Glet(Gconstant ("",(con,u)), 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
@@ -1823,7 +1923,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), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal
+ Glet(Gconstant ("",(con,u)), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal
arg|])))::
[Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix
@@ -1849,12 +1949,18 @@ let param_name = Name (id_of_string "params")
let arg_name = Name (id_of_string "arg")
let compile_mind prefix ~interactive mb mind stack =
+ let u = Declareops.inductive_instance mb in
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)) in
+ let name = Gind ("", ((mind, i), u)) in
let accu =
- Glet(name, MLapp (MLprimitive Mk_ind, [|get_ind_code j|]))
+ let args =
+ if Univ.Instance.is_empty u then
+ [|get_ind_code j; MLarray [||]|]
+ else [|get_ind_code j|]
+ in
+ Glet(name, MLapp (MLprimitive Mk_ind, args))
in
let nparams = mb.mind_nparams in
let params =
@@ -1862,7 +1968,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),
+ Glet(Gconstruct ("",(c,u)),
mkMLlam (Array.append params args)
(MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc
in
@@ -1961,8 +2067,8 @@ let mk_conv_code env sigma prefix t1 t2 =
in
let code1 = lambda_of_constr env sigma t1 in
let code2 = lambda_of_constr env sigma t2 in
- let (gl,code1) = compile_with_fv env sigma gl None code1 in
- let (gl,code2) = compile_with_fv env sigma gl None code2 in
+ let (gl,code1) = compile_with_fv env sigma None gl None code1 in
+ let (gl,code2) = compile_with_fv env sigma None gl None code2 in
let t1 = mk_internal_let "t1" code1 in
let t2 = mk_internal_let "t2" code2 in
let g1 = MLglobal (Ginternal "t1") in
@@ -1983,7 +2089,7 @@ let mk_norm_code env sigma prefix t =
compile_deps env sigma prefix ~interactive:true init t
in
let code = lambda_of_constr env sigma t in
- let (gl,code) = compile_with_fv env sigma gl None code in
+ let (gl,code) = compile_with_fv env sigma None gl None code in
let t1 = mk_internal_let "t1" code in
let g1 = MLglobal (Ginternal "t1") in
let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 385c77283..893db92dd 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -42,6 +42,8 @@ val get_meta : symbol array -> int -> metavariable
val get_evar : symbol array -> int -> existential
+val get_level : symbol array -> int -> Univ.Level.t
+
val get_symbols_tbl : unit -> symbol array
type code_location_update
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 8930250fc..75a3fc458 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -16,17 +16,17 @@ open Nativecode
(** This module implements the conversion test by compiling to OCaml code *)
-let rec conv_val env pb lvl v1 v2 cu =
- if v1 == v2 then cu
+let rec conv_val env pb lvl cu v1 v2 =
+ if v1 == v2 then ()
else
match kind_of_value v1, kind_of_value v2 with
| Vaccu k1, Vaccu k2 ->
- conv_accu env pb lvl k1 k2 cu
+ conv_accu env pb lvl cu k1 k2
| Vfun f1, Vfun f2 ->
let v = mk_rel_accu lvl in
- conv_val env CONV (lvl+1) (f1 v) (f2 v) cu
+ conv_val env CONV (lvl+1) cu (f1 v) (f2 v)
| Vconst i1, Vconst i2 ->
- if Int.equal i1 i2 then cu else raise NotConvertible
+ if not (Int.equal i1 i2) then raise NotConvertible
| Vblock b1, Vblock b2 ->
let n1 = block_size b1 in
let n2 = block_size b2 in
@@ -34,79 +34,76 @@ let rec conv_val env pb lvl v1 v2 cu =
raise NotConvertible;
let rec aux lvl max b1 b2 i cu =
if Int.equal i max then
- conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu
+ conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i)
else
- let cu =
- conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in
- aux lvl max b1 b2 (i+1) cu in
+ (conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i);
+ aux lvl max b1 b2 (i+1) cu)
+ in
aux lvl (n1-1) b1 b2 0 cu
| Vfun f1, _ ->
- conv_val env CONV lvl v1 (fun x -> v2 x) cu
+ conv_val env CONV lvl cu v1 (fun x -> v2 x)
| _, Vfun f2 ->
- conv_val env CONV lvl (fun x -> v1 x) v2 cu
+ conv_val env CONV lvl cu (fun x -> v1 x) v2
| _, _ -> raise NotConvertible
-and conv_accu env pb lvl k1 k2 cu =
+and conv_accu env pb lvl cu k1 k2 =
let n1 = accu_nargs k1 in
let n2 = accu_nargs k2 in
if not (Int.equal n1 n2) then raise NotConvertible;
if Int.equal n1 0 then
conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
else
- let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
- List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu
+ (conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu;
+ List.iter2 (conv_val env CONV lvl cu) (args_of_accu k1) (args_of_accu k2))
and conv_atom env pb lvl a1 a2 cu =
- if a1 == a2 then cu
+ if a1 == a2 then ()
else
match a1, a2 with
| Arel i1, Arel i2 ->
- if not (Int.equal i1 i2) then raise NotConvertible;
- cu
+ if not (Int.equal i1 i2) then raise NotConvertible
| Aind ind1, Aind ind2 ->
- if not (eq_ind ind1 ind2) then raise NotConvertible;
- cu
+ if not (eq_puniverses eq_ind ind1 ind2) then raise NotConvertible
| Aconstant c1, Aconstant c2 ->
- if not (eq_constant c1 c2) then raise NotConvertible;
- cu
+ if not (eq_puniverses eq_constant c1 c2) then raise NotConvertible
| Asort s1, Asort s2 ->
- check_sort_cmp_universes env pb s1 s2 cu; cu
+ check_sort_cmp_universes env pb s1 s2 cu
| Avar id1, Avar id2 ->
- if not (Id.equal id1 id2) then raise NotConvertible;
- cu
+ if not (Id.equal id1 id2) then raise NotConvertible
| Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
- let cu = conv_accu env CONV lvl ac1 ac2 cu in
+ conv_accu env CONV lvl cu ac1 ac2;
let tbl = a1.asw_reloc in
let len = Array.length tbl in
- if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu
- else
- let cu = conv_val env CONV lvl p1 p2 cu in
+ if Int.equal len 0 then conv_val env CONV lvl cu p1 p2
+ else begin
+ conv_val env CONV lvl cu p1 p2;
let max = len - 1 in
- let rec aux i cu =
+ let rec aux i =
let tag,arity = tbl.(i) in
let ci =
if Int.equal arity 0 then mk_const tag
else mk_block tag (mk_rels_accu lvl arity) in
let bi1 = bs1 ci and bi2 = bs2 ci in
- if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu
- else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in
- aux 0 cu
+ if Int.equal i max then conv_val env CONV (lvl + arity) cu bi1 bi2
+ else (conv_val env CONV (lvl + arity) cu bi1 bi2; aux (i+1)) in
+ aux 0
+ end
| Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) ->
if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible;
- if f1 == f2 then cu
+ if f1 == f2 then ()
else conv_fix env lvl t1 f1 t2 f2 cu
| (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)),
(Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) ->
if not (Int.equal s1 s2) then raise NotConvertible;
- if f1 == f2 then cu
+ if f1 == f2 then ()
else
if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
else conv_fix env lvl t1 f1 t2 f2 cu
| Aprod(_,d1,c1), Aprod(_,d2,c2) ->
- let cu = conv_val env CONV lvl d1 d2 cu in
+ conv_val env CONV lvl cu d1 d2;
let v = mk_rel_accu lvl in
- conv_val env pb (lvl + 1) (d1 v) (d2 v) cu
+ conv_val env pb (lvl + 1) cu (d1 v) (d2 v)
| _, _ -> raise NotConvertible
(* Precondition length t1 = length f1 = length f2 = length t2 *)
@@ -115,13 +112,13 @@ and conv_fix env lvl t1 f1 t2 f2 cu =
let max = len - 1 in
let fargs = mk_rels_accu lvl len in
let flvl = lvl + len in
- let rec aux i cu =
- let cu = conv_val env CONV lvl t1.(i) t2.(i) cu in
+ let rec aux i =
+ conv_val env CONV lvl cu t1.(i) t2.(i);
let fi1 = napply f1.(i) fargs in
let fi2 = napply f2.(i) fargs in
- if Int.equal i max then conv_val env CONV flvl fi1 fi2 cu
- else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in
- aux 0 cu
+ if Int.equal i max then conv_val env CONV flvl cu fi1 fi2
+ else (conv_val env CONV flvl cu fi1 fi2; aux (i+1)) in
+ aux 0
let native_conv pb sigma env t1 t2 =
if !Flags.no_native_compiler then begin
@@ -144,7 +141,7 @@ let native_conv pb sigma env t1 t2 =
let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
if !Flags.debug then Pp.msg_debug (Pp.str time_info);
(* TODO change 0 when we can have deBruijn *)
- ignore(conv_val env pb 0 !rt1 !rt2 (Environ.universes env))
+ conv_val env pb 0 (Environ.universes env) !rt1 !rt2
end
| _ -> anomaly (Pp.str "Compilation failure")
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index ad541ad73..b7d3dadcd 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -28,7 +28,7 @@ and lambda =
| Llam of name array * lambda
| Llet of name * lambda * lambda
| Lapp of lambda * lambda array
- | Lconst of prefix * constant
+ | Lconst of prefix * pconstant
| Lproj of prefix * constant (* prefix, projection name *)
| Lprim of prefix * constant * Primitives.t * lambda array
| Lcase of annot_sw * lambda * lambda * lam_branches
@@ -36,15 +36,15 @@ and lambda =
| Lif of lambda * lambda * lambda
| Lfix of (int array * int) * fix_decl
| Lcofix of int * fix_decl
- | Lmakeblock of prefix * constructor * int * lambda array
+ | Lmakeblock of prefix * pconstructor * int * lambda array
(* prefix, constructor name, constructor tag, arguments *)
(* A fully applied constructor *)
- | Lconstruct of prefix * constructor
+ | Lconstruct of prefix * pconstructor
(* A partially applied constructor *)
| Luint of uint
| Lval of Nativevalues.t
| Lsort of sorts
- | Lind of prefix * inductive
+ | Lind of prefix * pinductive
| Llazy
| Lforce
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 947e0a148..543397df5 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -363,13 +363,13 @@ let make_args start _end =
(* Translation of constructors *)
-let makeblock env cn tag args =
+let makeblock env cn u tag args =
if Array.for_all is_value args && Array.length args > 0 then
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)
+ Lmakeblock(prefix, (cn,u), tag, args)
(* Translation of constants *)
@@ -553,9 +553,9 @@ let rec lambda_of_constr env sigma c =
| Sort s -> Lsort s
- | Ind (ind,u) ->
+ | Ind (ind,u as pind) ->
let prefix = get_mind_prefix !global_env (fst ind) in
- Lind (prefix, ind)
+ Lind (prefix, pind)
| Prod(id, dom, codom) ->
let ld = lambda_of_constr env sigma dom in
@@ -666,13 +666,13 @@ and lambda_of_app env sigma f args =
let prefix = get_const_prefix !global_env kn in
let t =
if is_lazy prefix (Mod_subst.force_constr csubst) then
- mkLapp Lforce [|Lconst (prefix, kn)|]
- else Lconst (prefix, kn)
+ mkLapp Lforce [|Lconst (prefix, (kn,u))|]
+ else Lconst (prefix, (kn,u))
in
mkLapp t (lambda_of_args env sigma 0 args)
| OpaqueDef _ | Undef _ ->
let prefix = get_const_prefix !global_env kn in
- mkLapp (Lconst (prefix, kn)) (lambda_of_args env sigma 0 args)
+ mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args env sigma 0 args)
end)
| Construct (c,u) ->
let tag, nparams, arity = Renv.get_construct_info env c in
@@ -692,14 +692,14 @@ and lambda_of_app env sigma f args =
(!global_env).retroknowledge f prefix c args
with Not_found ->
let args = lambda_of_args env sigma nparams args in
- makeblock !global_env c tag args
+ makeblock !global_env c u tag args
else
let args = lambda_of_args env sigma 0 args in
(try
Retroknowledge.get_native_constant_dynamic_info
(!global_env).retroknowledge f prefix c args
with Not_found ->
- mkLapp (Lconstruct (prefix, c)) args)
+ mkLapp (Lconstruct (prefix, (c,u))) args)
| _ ->
let f = lambda_of_constr env sigma f in
let args = lambda_of_args env sigma 0 args in
@@ -752,8 +752,8 @@ let compile_dynamic_int31 fc prefix c args =
(* We are relying here on the order of digits constructors *)
let digits_from_uint digits_ind prefix i =
- let d0 = Lconstruct (prefix, (digits_ind, 1)) in
- let d1 = Lconstruct (prefix, (digits_ind, 2)) in
+ let d0 = Lconstruct (prefix, ((digits_ind, 1), Univ.Instance.empty)) in
+ let d1 = Lconstruct (prefix, ((digits_ind, 2), Univ.Instance.empty)) in
let digits = Array.make 31 d0 in
for k = 0 to 30 do
if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then
@@ -768,9 +768,9 @@ let before_match_int31 digits_ind fc prefix c t =
match t with
| Luint (UintVal i) ->
let digits = digits_from_uint digits_ind prefix i in
- mkLapp (Lconstruct (prefix,c)) digits
+ mkLapp (Lconstruct (prefix,(c, Univ.Instance.empty))) digits
| Luint (UintDigits (prefix,c,args)) ->
- mkLapp (Lconstruct (prefix,c)) args
+ mkLapp (Lconstruct (prefix,(c, Univ.Instance.empty))) args
| _ -> Luint (UintDecomp (prefix,c,t))
let compile_prim prim kn fc prefix args =
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 098c59e82..d7a219505 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -49,8 +49,8 @@ let eq_rec_pos = Array.equal Int.equal
type atom =
| Arel of int
- | Aconstant of constant
- | Aind of inductive
+ | Aconstant of pconstant
+ | Aind of pinductive
| Asort of sorts
| Avar of identifier
| Acase of annot_sw * accumulator * t * (t -> t)
@@ -106,14 +106,19 @@ let mk_rels_accu lvl len =
let napply (f:t) (args: t array) =
Array.fold_left (fun f a -> f a) f args
-let mk_constant_accu kn =
- mk_accu (Aconstant kn)
+let mk_constant_accu kn u =
+ mk_accu (Aconstant (kn,Univ.Instance.of_array u))
-let mk_ind_accu s =
- mk_accu (Aind s)
+let mk_ind_accu ind u =
+ mk_accu (Aind (ind,Univ.Instance.of_array u))
-let mk_sort_accu s =
- mk_accu (Asort s)
+let mk_sort_accu s u =
+ match s with
+ | Prop _ -> mk_accu (Asort s)
+ | Type s ->
+ let u = Univ.Instance.of_array u in
+ let s = Univ.subst_instance_universe u s in
+ mk_accu (Asort (Type s))
let mk_var_accu id =
mk_accu (Avar id)
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 983e7588d..79e35d4a0 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -41,8 +41,8 @@ val eq_rec_pos : rec_pos -> rec_pos -> bool
type atom =
| Arel of int
- | Aconstant of constant
- | Aind of inductive
+ | Aconstant of pconstant
+ | Aind of pinductive
| Asort of sorts
| Avar of identifier
| Acase of annot_sw * accumulator * t * (t -> t)
@@ -59,9 +59,9 @@ type atom =
val mk_accu : atom -> t
val mk_rel_accu : int -> t
val mk_rels_accu : int -> int -> t array
-val mk_constant_accu : constant -> t
-val mk_ind_accu : inductive -> t
-val mk_sort_accu : sorts -> t
+val mk_constant_accu : constant -> Univ.Level.t array -> t
+val mk_ind_accu : inductive -> Univ.Level.t array -> t
+val mk_sort_accu : sorts -> Univ.Level.t array -> t
val mk_var_accu : identifier -> t
val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t)
val mk_prod_accu : name -> t -> t -> t
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index fa4f1c7c9..db155e6c8 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -17,6 +17,7 @@ open Names
open Univ
open Term
open Declarations
+open Declareops
open Reduction
open Inductive
open Modops
diff --git a/kernel/univ.ml b/kernel/univ.ml
index e2a19b0e8..7d64e894d 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -303,6 +303,10 @@ module Level = struct
let var n =
if n < 20 then vars.(n) else make (Var n)
+ let var_index u =
+ match data u with
+ | Var n -> Some n | _ -> None
+
let make m n = make (Level (n, Names.DirPath.hcons m))
end
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 454134f21..490ec0369 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -27,6 +27,8 @@ sig
val equal : t -> t -> bool
(** Equality function *)
+ val hash : t -> int
+
val make : Names.DirPath.t -> int -> t
(** Create a new universe level from a unique identifier and an associated
module path. *)
@@ -35,6 +37,8 @@ sig
(** Pretty-printing *)
val var : int -> t
+
+ val var_index : t -> int option
end
type universe_level = Level.t
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index ff48119ba..bd427ecd0 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -257,8 +257,8 @@ and nf_bargs env b t =
and nf_atom env atom =
match atom with
| Arel i -> mkRel (nb_rel env - i)
- | Aconstant cst -> mkConst cst
- | Aind ind -> mkInd ind
+ | Aconstant cst -> mkConstU cst
+ | Aind ind -> mkIndU ind
| Asort s -> mkSort s
| Avar id -> mkVar id
| Aprod(n,dom,codom) ->
@@ -280,9 +280,9 @@ and nf_atom_type env atom =
let n = (nb_rel env - i) in
mkRel n, type_of_rel env n
| Aconstant cst ->
- mkConst cst, fst (Typeops.type_of_constant env (cst,Univ.Instance.empty)) (* FIXME *)
+ mkConstU cst, Typeops.type_of_constant_in env cst
| Aind ind ->
- mkInd ind, Inductiveops.type_of_inductive env (ind,Univ.Instance.empty)
+ mkIndU ind, Inductiveops.type_of_inductive env ind
| Asort s ->
mkSort s, type_of_sort s
| Avar id ->
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 9914ff341..749e0d2b5 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -47,7 +47,7 @@ let optimize_non_type_induction_scheme kind dep sort ind =
(nf c', Evd.evar_universe_context sigma), eff
else
let mib,mip = Inductive.lookup_mind_specif env ind in
- let ctx = Inductive.inductive_context mib in
+ let ctx = Declareops.inductive_context mib in
let u = Univ.UContext.instance ctx in
let ctxset = Univ.ContextSet.of_context ctx in
let ectx = Evd.evar_universe_context_of ctxset in
@@ -58,7 +58,7 @@ let build_induction_scheme_in_type dep sort ind =
let env = Global.env () in
let ctx =
let mib,mip = Inductive.lookup_mind_specif env ind in
- Inductive.inductive_context mib
+ Declareops.inductive_context mib
in
let u = Univ.UContext.instance ctx in
let ctxset = Univ.ContextSet.of_context ctx in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index e34206a41..55f533512 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -230,7 +230,7 @@ let instantiate_possibly_recursive_type indu paramdecls fields =
let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
- let u = Inductive.inductive_instance mib in
+ let u = Declareops.inductive_instance mib in
let paramdecls = Inductive.inductive_paramdecls (mib, u) in
let poly = mib.mind_polymorphic and ctx = Univ.instantiate_univ_context mib.mind_universes in
let indu = indsp, u in
diff --git a/toplevel/search.ml b/toplevel/search.ml
index bb0c2a2e7..59283edf9 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -78,7 +78,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
let mib = Global.lookup_mind mind in
let iter_packet i mip =
let ind = (mind, i) in
- let u = Inductive.inductive_instance mib in
+ let u = Declareops.inductive_instance mib in
let i = (ind, u) in
let typ = Inductiveops.type_of_inductive env i in
let () = fn (IndRef ind) env typ in