diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2015-01-16 22:17:03 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2015-01-17 08:02:45 +0100 |
commit | 9f5586d88880cbb98c92edfe9c33c76564f1a19c (patch) | |
tree | 6de2a171eff5706b0e4ce9268554b84a922f12b3 /kernel | |
parent | 4985f0ff99278beb3b934f86edf1398659c611a8 (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.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/declareops.ml | 10 | ||||
-rw-r--r-- | kernel/declareops.mli | 5 | ||||
-rw-r--r-- | kernel/inductive.ml | 15 | ||||
-rw-r--r-- | kernel/inductive.mli | 2 | ||||
-rw-r--r-- | kernel/nativecode.ml | 242 | ||||
-rw-r--r-- | kernel/nativecode.mli | 2 | ||||
-rw-r--r-- | kernel/nativeconv.ml | 81 | ||||
-rw-r--r-- | kernel/nativeinstr.mli | 8 | ||||
-rw-r--r-- | kernel/nativelambda.ml | 26 | ||||
-rw-r--r-- | kernel/nativevalues.ml | 21 | ||||
-rw-r--r-- | kernel/nativevalues.mli | 10 | ||||
-rw-r--r-- | kernel/subtyping.ml | 1 | ||||
-rw-r--r-- | kernel/univ.ml | 4 | ||||
-rw-r--r-- | kernel/univ.mli | 4 |
14 files changed, 277 insertions, 154 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 |