- Fix hashing of levels to get the "right" order in universe contexts etc...

- Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}.
These are always rigid.
- Use level-to-level substitutions where the more general level-to-universe substitutions
were previously used.

7 files changed, 123 insertions, 40 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 652c5acf93..65a8f338cb 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -381,9 +381,12 @@ type binder_kind = BProd | BLambda | BLetIn
 let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable"))
 let set_detype_anonymous f = detype_anonymous := f
 
-let option_of_instance l = 
+let detype_level l =
+  GType (Some (Pp.string_of_ppcmds (Univ.Level.pr l)))
+
+let detype_instance l = 
   if Univ.Instance.is_empty l then None
-  else Some l
+  else Some (List.map detype_level (Array.to_list (Univ.Instance.to_array l)))
 
 let rec detype (isgoal:bool) avoid env t =
   match kind_of_term (collapse_appl t) with
@@ -424,18 +427,16 @@ let rec detype (isgoal:bool) avoid env t =
       in
  	mkapp (detype isgoal avoid env f)
  	  (Array.map_to_list (detype isgoal avoid env) args)
-        (* GApp (dl,detype isgoal avoid env f, *)
-        (*       Array.map_to_list (detype isgoal avoid env) args) *)
-    | Const (sp,u) -> GRef (dl, ConstRef sp, option_of_instance u)
+    | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance u)
     | Proj (p,c) ->
         GProj (dl, p, detype isgoal avoid env c)
     | Evar (ev,cl) ->
         GEvar (dl, ev,
                Some (List.map (detype isgoal avoid env) (Array.to_list cl)))
     | Ind (ind_sp,u) ->
-	GRef (dl, IndRef ind_sp, option_of_instance u)
+	GRef (dl, IndRef ind_sp, detype_instance u)
     | Construct (cstr_sp,u) ->
-	GRef (dl, ConstructRef cstr_sp, option_of_instance u)
+	GRef (dl, ConstructRef cstr_sp, detype_instance u)
     | Case (ci,p,c,bl) ->
 	let comp = computable p (ci.ci_pp_info.ind_nargs) in
 	detype_case comp (detype isgoal avoid env)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 42d98cdfef..e8b360b86f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -262,9 +262,29 @@ let instantiate_evar_array info c args =
   | [] -> c
   | _ -> replace_vars inst c
 
+module StringOrd = struct type t = string let compare = String.compare end
+module UNameMap = struct
+
+    include Map.Make(StringOrd)
+
+    let union s t = 
+      merge (fun k l r -> 
+	match l, r with
+	| Some _, _ -> l
+	| _, _ -> r) s t
+
+    let diff ext orig =
+      fold (fun u v acc -> 
+	if mem u orig then acc 
+	else add u v acc)
+	ext empty
+
+end
+
 (* 2nd part used to check consistency on the fly. *)
 type evar_universe_context = 
-  { uctx_local : Univ.universe_context_set; (** The local context of variables *)
+ { uctx_names : Univ.Level.t UNameMap.t;
+   uctx_local : Univ.universe_context_set; (** The local context of variables *)
     uctx_univ_variables : Universes.universe_opt_subst;
       (** The local universes that are unification variables *)
     uctx_univ_algebraic : Univ.universe_set; 
@@ -277,7 +297,8 @@ type evar_universe_context =
   }
   
 let empty_evar_universe_context = 
-  { uctx_local = Univ.ContextSet.empty;
+  { uctx_names = UNameMap.empty;
+    uctx_local = Univ.ContextSet.empty;
     uctx_univ_variables = Univ.LMap.empty;
     uctx_univ_algebraic = Univ.LSet.empty;
     uctx_univ_template = Univ.LSet.empty;
@@ -301,7 +322,12 @@ let union_evar_universe_context ctx ctx' =
       if ctx.uctx_local == ctx'.uctx_local then ctx.uctx_local 
       else Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local
     in
-      { uctx_local = local;
+    let names =
+      if ctx.uctx_names = ctx.uctx_names then ctx.uctx_names
+      else UNameMap.union ctx.uctx_names ctx'.uctx_names
+    in
+      { uctx_names = names;
+	uctx_local = local;
 	uctx_univ_variables = 
 	  Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
 	uctx_univ_algebraic = 
@@ -323,7 +349,9 @@ let diff_evar_universe_context ctx' ctx  =
   if ctx == ctx' then empty_evar_universe_context
   else
     let local = Univ.ContextSet.diff ctx'.uctx_local ctx.uctx_local in
-      { uctx_local = local;
+    let names = UNameMap.diff ctx'.uctx_names ctx.uctx_names in
+      { uctx_names = names;
+	uctx_local = local;
 	uctx_univ_variables = 
 	  Univ.LMap.diff ctx'.uctx_univ_variables ctx.uctx_univ_variables;
 	uctx_univ_algebraic = 
@@ -964,7 +992,7 @@ let merge_universe_subst evd subst =
 let with_context_set rigid d (a, ctx) = 
   (merge_context_set rigid d ctx, a)
 
-let uctx_new_univ_variable template rigid 
+let uctx_new_univ_variable template rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
   let u = Universes.new_univ_level (Global.current_dirpath ()) in
   let ctx' = Univ.ContextSet.union ctx (Univ.ContextSet.singleton u) in
@@ -980,14 +1008,23 @@ let uctx_new_univ_variable template rigid
       {uctx' with uctx_univ_template = Univ.LSet.add u uctx'.uctx_univ_template}
     else uctx'
   in
-    {uctx'' with uctx_local = ctx'}, u
+  let names = 
+    match name with
+    | Some n -> UNameMap.add n u uctx.uctx_names
+    | None -> uctx.uctx_names
+  in
+    {uctx'' with uctx_names = names; uctx_local = ctx'}, u
+
+let new_univ_level_variable ?(template=false) ?name rigid evd =
+  let uctx', u = uctx_new_univ_variable template rigid name evd.universes in
+    ({evd with universes = uctx'}, u)
 
-let new_univ_variable ?(template=false) rigid evd =
-  let uctx', u = uctx_new_univ_variable template rigid evd.universes in
+let new_univ_variable ?(template=false) ?name rigid evd =
+  let uctx', u = uctx_new_univ_variable template rigid name evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
-let new_sort_variable ?(template=false) rigid d =
-  let (d', u) = new_univ_variable ~template rigid d in
+let new_sort_variable ?(template=false) ?name rigid d =
+  let (d', u) = new_univ_variable ~template rigid ?name d in
     (d', Type u)
 
 let make_flexible_variable evd b u =
@@ -1013,7 +1050,7 @@ let make_flexible_variable evd b u =
 let fresh_sort_in_family env evd s = 
   with_context_set univ_flexible evd (Universes.fresh_sort_in_family env s)
 
-let fresh_constant_instance env evd c = 
+let fresh_constant_instance env evd c =
   with_context_set univ_flexible evd (Universes.fresh_constant_instance env c)
 
 let fresh_inductive_instance env evd i =
@@ -1022,8 +1059,8 @@ let fresh_inductive_instance env evd i =
 let fresh_constructor_instance env evd c =
   with_context_set univ_flexible evd (Universes.fresh_constructor_instance env c)
 
-let fresh_global ?(rigid=univ_flexible) env evd gr =
-  with_context_set rigid evd (Universes.fresh_global_instance env gr)
+let fresh_global ?(rigid=univ_flexible) ?names env evd gr =
+  with_context_set rigid evd (Universes.fresh_global_instance ?names env gr)
 
 let whd_sort_variable evd t = t
 
@@ -1203,7 +1240,8 @@ let refresh_undefined_univ_variables uctx =
           (Option.map (Univ.subst_univs_level_universe subst) v) acc)
       uctx.uctx_univ_variables Univ.LMap.empty
   in 
-  let uctx' = {uctx_local = ctx'; 
+  let uctx' = {uctx_names = uctx.uctx_names;
+	       uctx_local = ctx'; 
 	       uctx_univ_variables = vars; uctx_univ_algebraic = alg;
 	       uctx_univ_template = uctx.uctx_univ_template;
 	       uctx_universes = Univ.initial_universes;
@@ -1236,7 +1274,8 @@ let normalize_evar_universe_context uctx =
       else
 	let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in
 	let uctx' = 
-	  { uctx_local = us'; 
+	  { uctx_names = uctx.uctx_names;
+	    uctx_local = us'; 
 	    uctx_univ_variables = vars'; 
 	    uctx_univ_algebraic = algs';
 	    uctx_univ_template = uctx.uctx_univ_template;
@@ -1265,6 +1304,14 @@ let nf_constraints =
       Profile.profile1 nfconstrkey nf_constraints
   else nf_constraints
 
+let universe_of_name evd s = 
+  UNameMap.find s evd.universes.uctx_names
+
+let add_universe_name evd s l =
+  let names = evd.universes.uctx_names in
+  let names' = UNameMap.add s l names in
+    {evd with universes = {evd.universes with uctx_names = names'}}
+
 let universes evd = evd.universes.uctx_universes
 let constraints evd = evd.universes.uctx_universes
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index a360351b74..8a9753e5b3 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -258,8 +258,6 @@ val drop_side_effects : evar_map -> evar_map
     Evar maps also keep track of the universe constraints defined at a given
     point. This section defines the relevant manipulation functions. *)
 
-val new_univ_variable : evar_map -> evar_map * Univ.universe
-val new_sort_variable : evar_map -> evar_map * sorts
 val is_sort_variable : evar_map -> sorts -> bool
 val whd_sort_variable : evar_map -> constr -> constr
 val set_leq_sort : evar_map -> sorts -> sorts -> evar_map
@@ -424,6 +422,10 @@ val union_evar_universe_context : evar_universe_context -> evar_universe_context
   evar_universe_context
 val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
 
+(** Raises Not_found if not a name for a universe in this map. *)
+val universe_of_name : evar_map -> string -> Univ.universe_level
+val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map
+
 val universes : evar_map -> Univ.universes
 
 val add_constraints_context : evar_universe_context -> 
@@ -436,8 +438,9 @@ val normalize_evar_universe_context_variables : evar_universe_context ->
 val normalize_evar_universe_context : evar_universe_context -> 
   evar_universe_context
 
-val new_univ_variable : ?template:bool -> rigid -> evar_map -> evar_map * Univ.universe
-val new_sort_variable : ?template:bool -> rigid -> evar_map -> evar_map * sorts
+val new_univ_level_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level
+val new_univ_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe
+val new_sort_variable : ?template:bool -> ?name:string -> rigid -> evar_map -> evar_map * sorts
 val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
 val is_sort_variable : evar_map -> sorts -> (Univ.universe_level * bool) option 
 (** [is_sort_variable evm s] returns [Some (u, is_rigid)] or [None] if [s] is 
@@ -489,7 +492,7 @@ val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstan
 val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive
 val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor
 
-val fresh_global : ?rigid:rigid -> env -> evar_map -> 
+val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> 
   Globnames.global_reference -> evar_map * constr
 
 (********************************************************************
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index bed77e6223..9f58b4c80d 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -60,7 +60,7 @@ let check_privacy_block mib =
 
 let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
   let usubst = Inductive.make_inductive_subst mib u in
-  let lnamespar = Vars.subst_univs_context usubst
+  let lnamespar = Vars.subst_univs_level_context usubst
     mib.mind_params_ctxt
   in
   let () = check_privacy_block mib in
@@ -284,7 +284,7 @@ let mis_make_indrec env sigma listdepkind mib u =
   let evdref = ref sigma in
   let usubst = Inductive.make_inductive_subst mib u in
   let lnonparrec,lnamesparrec =
-    context_chop (nparams-nparrec) (Vars.subst_univs_context usubst mib.mind_params_ctxt) in
+    context_chop (nparams-nparrec) (Vars.subst_univs_level_context usubst mib.mind_params_ctxt) in
   let nrec = List.length listdepkind in
   let depPvec =
     Array.make mib.mind_ntypes (None : (bool * constr) option) in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 07dacd0ccc..43552ef542 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -101,7 +101,7 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j =
   let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in
   if j > nconstr then error "Not enough constructors in the type.";
   let univsubst = make_inductive_subst mib u in
-    substl (List.init ntypes make_Ik) (subst_univs_constr univsubst specif.(j-1))
+    substl (List.init ntypes make_Ik) (subst_univs_level_constr univsubst specif.(j-1))
 
 (* Arity of constructors excluding parameters and local defs *)
 
@@ -149,7 +149,7 @@ let constructor_nrealhyps (ind,j) =
 let get_full_arity_sign env (ind,u) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let subst = Inductive.make_inductive_subst mib u in
-    Vars.subst_univs_context subst mip.mind_arity_ctxt
+    Vars.subst_univs_level_context subst mip.mind_arity_ctxt
 
 let nconstructors ind =
   let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
@@ -280,11 +280,11 @@ let get_arity env ((ind,u),params) =
       snd (List.chop nnonrecparams mib.mind_params_ctxt)
     else
       parsign in
-  let parsign = Vars.subst_univs_context univsubst parsign in
+  let parsign = Vars.subst_univs_level_context univsubst parsign in
   let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
   let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in
   let subst = instantiate_context parsign params in
-  let arsign = Vars.subst_univs_context univsubst arsign in
+  let arsign = Vars.subst_univs_level_context univsubst arsign in
   (substl_rel_context subst arsign, Inductive.inductive_sort_family mip)
 
 (* Functions to build standard types related to inductive *)
@@ -499,7 +499,7 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
   match mip.mind_arity with
   | RegularArity s ->
     let subst = Inductive.make_inductive_subst mib u in
-      sigma, subst_univs_constr subst s.mind_user_arity
+      sigma, subst_univs_level_constr subst s.mind_user_arity
   | TemplateArity ar ->
     let _,scl = Reduction.dest_arity env conclty in
     let ctx = List.rev mip.mind_arity_ctxt in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index add47e5b73..31576391b1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -93,10 +93,20 @@ let ((constr_in : constr -> Dyn.t),
 
 (** Miscellaneous interpretation functions *)
 
+let interp_universe_name evd = function
+  | None -> new_univ_level_variable univ_rigid evd
+  | Some s ->
+    try let level = Evd.universe_of_name evd s in
+	  evd, level
+    with Not_found -> 
+      new_univ_level_variable ~name:s univ_rigid evd
+	
 let interp_sort evd = function
   | GProp -> evd, Prop Null
   | GSet -> evd, Prop Pos
-  | GType _ -> new_sort_variable univ_rigid evd
+  | GType n -> 
+    let evd, l = interp_universe_name evd n in
+      evd, Type (Univ.Universe.make l)
 
 let interp_elimination_sort = function
   | GProp -> InProp
@@ -260,8 +270,23 @@ let evar_kind_of_term sigma c =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
-(* Check with universe list? *)
-let pretype_global rigid env evd gr us = Evd.fresh_global ~rigid env evd gr
+let interp_universe_level_name evd = function
+  | GProp -> evd, Univ.Level.prop
+  | GSet -> evd, Univ.Level.set
+  | GType s -> interp_universe_name evd s
+
+let pretype_global rigid env evd gr us = 
+  let evd, instance = 
+    match us with
+    | None -> evd, None
+    | Some l -> 
+      let evd, l' = List.fold_left (fun (evd, univs) l -> 
+	let evd, l = interp_universe_level_name evd l in
+	  (evd, l :: univs)) (evd, []) l
+      in 
+	evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+  in
+    Evd.fresh_global ~rigid ?names:instance env evd gr
 
 let is_template_polymorphic_constructor env c =
   match kind_of_term c with
@@ -292,10 +317,17 @@ let pretype_ref loc evdref env ref us =
     let ty = Retyping.get_type_of env evd c in
       make_judge c ty
 
+let judge_of_Type evd s =
+  let judge s = 
+    { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
+  in
+  let evd, l = interp_universe_name evd s in
+    evd, judge (Univ.Universe.make l)
+
 let pretype_sort evdref = function
   | GProp -> judge_of_prop
   | GSet -> judge_of_set
-  | GType _ -> evd_comb0 judge_of_new_Type evdref
+  | GType s -> evd_comb1 judge_of_Type evdref s
 
 let new_type_evar evdref env loc =
   let e, s = 
@@ -500,7 +532,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 	    j', (ind, args))
     in
     let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in
-    let ty = Vars.subst_univs_constr usubst ty in
+    let ty = Vars.subst_univs_level_constr usubst ty in
     let ty = substl (recty.uj_val :: List.rev pars) ty in
     let j = {uj_val = mkProj (cst,recty.uj_val); uj_type = ty} in
       inh_conv_coerce_to_tycon loc env evdref j tycon
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 2cf730f112..b21f4e383c 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -59,7 +59,7 @@ let type_constructor mind mib u typ params =
   let s = ind_subst mind mib u in
   let ctyp = substl s typ in
   let usubst = make_inductive_subst mib u in
-  let ctyp = subst_univs_constr usubst ctyp in
+  let ctyp = subst_univs_level_constr usubst ctyp in
   let nparams = Array.length params in
   if Int.equal nparams 0 then ctyp
   else