diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-05-30 20:55:48 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-04 15:48:31 +0200 |
commit | dd96b1e5e8d0eb9f93cff423b6f9cf900aee49d7 (patch) | |
tree | 70a184062496f64841ca013929a0622600ac1b2f | |
parent | 0bbaba7bde67a8673692356c3b3b401b4f820eb7 (diff) |
- 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.
-rw-r--r-- | interp/constrintern.ml | 22 | ||||
-rw-r--r-- | intf/constrexpr.mli | 6 | ||||
-rw-r--r-- | intf/glob_term.mli | 2 | ||||
-rw-r--r-- | kernel/environ.ml | 12 | ||||
-rw-r--r-- | kernel/fast_typeops.ml | 4 | ||||
-rw-r--r-- | kernel/inductive.ml | 12 | ||||
-rw-r--r-- | kernel/inductive.mli | 5 | ||||
-rw-r--r-- | kernel/typeops.ml | 4 | ||||
-rw-r--r-- | kernel/univ.ml | 12 | ||||
-rw-r--r-- | kernel/univ.mli | 9 | ||||
-rw-r--r-- | kernel/vars.ml | 4 | ||||
-rw-r--r-- | kernel/vars.mli | 6 | ||||
-rw-r--r-- | library/universes.ml | 73 | ||||
-rw-r--r-- | library/universes.mli | 14 | ||||
-rw-r--r-- | parsing/g_constr.ml4 | 10 | ||||
-rw-r--r-- | pretyping/detyping.ml | 15 | ||||
-rw-r--r-- | pretyping/evd.ml | 77 | ||||
-rw-r--r-- | pretyping/evd.mli | 13 | ||||
-rw-r--r-- | pretyping/indrec.ml | 4 | ||||
-rw-r--r-- | pretyping/inductiveops.ml | 10 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 42 | ||||
-rw-r--r-- | pretyping/vnorm.ml | 2 | ||||
-rw-r--r-- | printing/ppconstr.ml | 2 | ||||
-rw-r--r-- | tactics/eqschemes.ml | 14 | ||||
-rw-r--r-- | test-suite/success/polymorphism.v | 27 |
25 files changed, 275 insertions, 126 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d8cf9fd16..7f13fff2c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -748,9 +748,9 @@ let intern_reference ref = Smartlocate.global_of_extended_global r (* Is it a global reference or a syntactic definition? *) -let intern_qualid loc qid intern env lvar args = +let intern_qualid loc qid intern env lvar us args = match intern_extended_global_of_qualid (loc,qid) with - | TrueGlobal ref -> GRef (loc, ref, None), args + | TrueGlobal ref -> GRef (loc, ref, us), args | SynDef sp -> let (ids,c) = Syntax_def.search_syntactic_definition sp in let nids = List.length ids in @@ -763,15 +763,15 @@ let intern_qualid loc qid intern env lvar args = subst_aconstr_in_glob_constr loc intern lvar subst infos c, args2 (* Rule out section vars since these should have been found by intern_var *) -let intern_non_secvar_qualid loc qid intern env lvar args = - match intern_qualid loc qid intern env lvar args with +let intern_non_secvar_qualid loc qid intern env lvar us args = + match intern_qualid loc qid intern env lvar us args with | GRef (_, VarRef _, _),_ -> raise Not_found | r -> r -let intern_applied_reference intern env namedctx lvar args = function +let intern_applied_reference intern env namedctx lvar us args = function | Qualid (loc, qid) -> let r,args2 = - try intern_qualid loc qid intern env lvar args + try intern_qualid loc qid intern env lvar us args with Not_found -> error_global_not_found_loc loc qid in let x, isproj, imp, scopes, l = find_appl_head_data r in @@ -781,7 +781,7 @@ let intern_applied_reference intern env namedctx lvar args = function with Not_found -> let qid = qualid_of_ident id in try - let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in + let r,args2 = intern_non_secvar_qualid loc qid intern env lvar us args in let x, isproj, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), isproj, args2 with Not_found -> @@ -795,7 +795,7 @@ let interp_reference vars r = intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost) {ids = Id.Set.empty; unb = false ; tmp_scope = None; scopes = []; impls = empty_internalization_env} [] - (vars, Id.Map.empty) [] r + (vars, Id.Map.empty) None [] r in r (**********************************************************************) @@ -1368,7 +1368,7 @@ let internalize globalenv env allow_patvar lvar c = let rec intern env = function | CRef (ref,us) as x -> let (c,imp,subscopes,l),isproj,_ = - intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in + intern_applied_reference intern env (Environ.named_context globalenv) lvar us [] ref in apply_impargs (None, isproj) c env imp subscopes l (constr_loc x) | CFix (loc, (locid,iddef), dl) -> @@ -1467,7 +1467,7 @@ let internalize globalenv env allow_patvar lvar c = let (f,_,args_scopes,_),_,args = let args = List.map (fun a -> (a,None)) args in intern_applied_reference intern env (Environ.named_context globalenv) - lvar args ref in + lvar us args ref in (* check_projection isproj (List.length args) f; *) (* Rem: GApp(_,f,[]) stands for @f *) GApp (loc, f, intern_args env args_scopes (List.map fst args)) @@ -1483,7 +1483,7 @@ let internalize globalenv env allow_patvar lvar c = match f with | CRef (ref,us) -> intern_applied_reference intern env - (Environ.named_context globalenv) lvar args ref + (Environ.named_context globalenv) lvar us args ref | CNotation (loc,ntn,([],[],[])) -> let c = intern_notation intern env lvar loc ntn ([],[],[]) in let x, isproj, impl, scopes, l = find_appl_head_data c in diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index af6aea164..c28c4dcb1 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -61,14 +61,16 @@ and cases_pattern_notation_substitution = cases_pattern_expr list * (** for constr subterms *) cases_pattern_expr list list (** for recursive notations *) +type instance_expr = Misctypes.glob_sort list + type constr_expr = - | CRef of reference * Univ.universe_instance option + | CRef of reference * instance_expr option | CFix of Loc.t * Id.t located * fix_expr list | CCoFix of Loc.t * Id.t located * cofix_expr list | CProdN of Loc.t * binder_expr list * constr_expr | CLambdaN of Loc.t * binder_expr list * constr_expr | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr - | CAppExpl of Loc.t * (proj_flag * reference * Univ.universe_instance option) * constr_expr list + | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list | CApp of Loc.t * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list diff --git a/intf/glob_term.mli b/intf/glob_term.mli index d07766e18..d37955225 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -28,7 +28,7 @@ type cases_pattern = (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) type glob_constr = - | GRef of (Loc.t * global_reference * Univ.universe_instance option) + | GRef of (Loc.t * global_reference * glob_sort list option) | GVar of (Loc.t * Id.t) | GEvar of Loc.t * existential_key * glob_constr list option | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 7a90f3675..f4420c489 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -229,7 +229,7 @@ let constant_type env (kn,u) = let cb = lookup_constant kn env in if cb.const_polymorphic then let subst, csts = universes_and_subst_of cb u in - (map_regular_arity (subst_univs_constr subst) cb.const_type, csts) + (map_regular_arity (subst_univs_level_constr subst) cb.const_type, csts) else cb.const_type, Univ.Constraint.empty let constant_context env kn = @@ -248,7 +248,7 @@ let constant_value env (kn,u) = | Def l_body -> if cb.const_polymorphic then let subst, csts = universes_and_subst_of cb u in - (subst_univs_constr subst (Mod_subst.force_constr l_body), csts) + (subst_univs_level_constr subst (Mod_subst.force_constr l_body), csts) else Mod_subst.force_constr l_body, Univ.Constraint.empty | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) @@ -263,11 +263,11 @@ let constant_value_and_type env (kn, u) = if cb.const_polymorphic then let subst, cst = universes_and_subst_of cb u in let b' = match cb.const_body with - | Def l_body -> Some (subst_univs_constr subst (Mod_subst.force_constr l_body)) + | Def l_body -> Some (subst_univs_level_constr subst (Mod_subst.force_constr l_body)) | OpaqueDef _ -> None | Undef _ -> None in - b', map_regular_arity (subst_univs_constr subst) cb.const_type, cst + b', map_regular_arity (subst_univs_level_constr subst) cb.const_type, cst else let b' = match cb.const_body with | Def l_body -> Some (Mod_subst.force_constr l_body) @@ -284,7 +284,7 @@ let constant_type_in env (kn,u) = let cb = lookup_constant kn env in if cb.const_polymorphic then let subst = Univ.make_universe_subst u cb.const_universes in - map_regular_arity (subst_univs_constr subst) cb.const_type + map_regular_arity (subst_univs_level_constr subst) cb.const_type else cb.const_type let constant_value_in env (kn,u) = @@ -294,7 +294,7 @@ let constant_value_in env (kn,u) = let b = Mod_subst.force_constr l_body in if cb.const_polymorphic then let subst = Univ.make_universe_subst u cb.const_universes in - subst_univs_constr subst b + subst_univs_level_constr subst b else b | OpaqueDef _ -> raise (NotEvaluableConst Opaque) | Undef _ -> raise (NotEvaluableConst NoBody) diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 6d48aaa4e..94e4479d2 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -149,7 +149,7 @@ let type_of_projection env (cst,u) = if cb.const_polymorphic then let mib,_ = lookup_mind_specif env (pb.proj_ind,0) in let subst = make_inductive_subst mib u in - Vars.subst_univs_constr subst pb.proj_type + Vars.subst_univs_level_constr subst pb.proj_type else pb.proj_type | None -> raise (Invalid_argument "type_of_projection: not a projection") @@ -333,7 +333,7 @@ let judge_of_projection env p c ct = in assert(eq_mind pb.proj_ind (fst ind)); let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in - let ty = Vars.subst_univs_constr usubst pb.Declarations.proj_type in + let ty = Vars.subst_univs_level_constr usubst pb.Declarations.proj_type in substl (c :: List.rev args) ty diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 3f1c4e75f..f07217ac0 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -56,11 +56,11 @@ let inductive_params (mib,_) = mib.mind_nparams let make_inductive_subst mib u = if mib.mind_polymorphic then make_universe_subst u mib.mind_universes - else Univ.empty_subst + else Univ.empty_level_subst let inductive_params_ctxt (mib,u) = let subst = make_inductive_subst mib u in - Vars.subst_univs_context subst mib.mind_params_ctxt + Vars.subst_univs_level_context subst mib.mind_params_ctxt let inductive_instance mib = if mib.mind_polymorphic then @@ -89,7 +89,7 @@ let ind_subst mind mib u = (* Instantiate inductives in constructor type *) let constructor_instantiate mind u subst mib c = let s = ind_subst mind mib u in - substl s (subst_univs_constr subst c) + substl s (subst_univs_level_constr subst c) let instantiate_params full t args sign = let fail () = @@ -113,7 +113,7 @@ let full_inductive_instantiate mib u params sign = let t = mkArity (sign,dummy) in let subst = make_inductive_subst mib u in let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in - Vars.subst_univs_context subst ar + Vars.subst_univs_level_context subst ar let full_constructor_instantiate ((mind,_),u,(mib,_),params) = let subst = make_inductive_subst mib u in @@ -217,7 +217,7 @@ let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps = if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty) else let subst = make_inductive_subst mib u in - (subst_univs_constr subst a.mind_user_arity, subst) + (subst_univs_level_constr subst a.mind_user_arity, subst) | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in let ctx,s = instantiate_universes env ctx ar paramtyps in @@ -234,7 +234,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = if not mib.mind_polymorphic then a.mind_user_arity else let subst = make_inductive_subst mib u in - (subst_univs_constr subst a.mind_user_arity) + (subst_univs_level_constr subst a.mind_user_arity) | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in let ctx,s = instantiate_universes env ctx ar paramtyps in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index a23d170f5..497c06417 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -35,13 +35,14 @@ 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 make_inductive_subst : mutual_inductive_body -> universe_instance -> universe_subst +val make_inductive_subst : mutual_inductive_body -> universe_instance -> universe_level_subst val inductive_instance : mutual_inductive_body -> universe_instance val inductive_context : mutual_inductive_body -> universe_context val inductive_params_ctxt : mutual_inductive_body puniverses -> rel_context -val instantiate_inductive_constraints : mutual_inductive_body -> universe_subst -> constraints +val instantiate_inductive_constraints : + mutual_inductive_body -> universe_level_subst -> constraints val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained val constrained_type_of_inductive_knowing_parameters : diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 49f883628..98c0dfc20 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -176,7 +176,7 @@ let type_of_projection env (cst,u) = if cb.const_polymorphic then let mib,_ = lookup_mind_specif env (pb.proj_ind,0) in let subst = make_inductive_subst mib u in - Vars.subst_univs_constr subst pb.proj_type + Vars.subst_univs_level_constr subst pb.proj_type else pb.proj_type | None -> raise (Invalid_argument "type_of_projection: not a projection") @@ -374,7 +374,7 @@ let judge_of_projection env p cj = in assert(eq_mind pb.proj_ind (fst ind)); let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in - let ty = Vars.subst_univs_constr usubst pb.Declarations.proj_type in + let ty = Vars.subst_univs_level_constr usubst pb.Declarations.proj_type in let ty = substl (cj.uj_val :: List.rev args) ty in (* TODO: Universe polymorphism for projections *) {uj_val = mkProj (p,cj.uj_val); diff --git a/kernel/univ.ml b/kernel/univ.ml index 8984938d3..147efe86b 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -454,7 +454,13 @@ module Level = struct let hcons = hashcons let equal = deep_equal (* Not shallow as serialization breaks sharing *) - let hash = Hashtbl.hash + + open Hashset.Combine + + let hash = function + | Prop -> combinesmall 1 0 + | Set -> combinesmall 1 1 + | Level (n, d) -> combinesmall 2 (combine n (Names.DirPath.hash d)) end (* let hcons = Hashcons.simple_hcons Hunivlevel.generate Names.DirPath.hcons *) @@ -1898,7 +1904,7 @@ let check_context_subset (univs, cst) (univs', cst') = (** Substitutions. *) let make_universe_subst inst (ctx, csts) = - try Array.fold_left2 (fun acc c i -> LMap.add c (Universe.make i) acc) + try Array.fold_left2 (fun acc c i -> LMap.add c i acc) LMap.empty (Instance.to_array ctx) (Instance.to_array inst) with Invalid_argument _ -> anomaly (Pp.str "Mismatched instance and context when building universe substitution") @@ -2115,7 +2121,7 @@ let subst_univs_universe_constraints subst csts = (** Substitute instance inst for ctx in csts *) let instantiate_univ_context subst (_, csts) = - subst_univs_constraints (make_subst subst) csts + subst_univs_level_constraints subst csts let check_consistent_constraints (ctx,cstrs) cstrs' = (* TODO *) () diff --git a/kernel/univ.mli b/kernel/univ.mli index cc5eedefb..bf04c62e2 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -355,15 +355,13 @@ val constraints_of : 'a constrained -> constraints val check_context_subset : universe_context_set -> universe_context -> universe_context (** Make a universe level substitution: the list must match the context variables. *) -val make_universe_subst : Instance.t -> universe_context -> universe_subst -val empty_subst : universe_subst -val is_empty_subst : universe_subst -> bool +val make_universe_subst : Instance.t -> universe_context -> universe_level_subst val empty_level_subst : universe_level_subst val is_empty_level_subst : universe_level_subst -> bool (** Get the instantiated graph. *) -val instantiate_univ_context : universe_subst -> universe_context -> constraints +val instantiate_univ_context : universe_level_subst -> universe_context -> constraints (** Substitution of universes. *) val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level @@ -372,6 +370,9 @@ val subst_univs_level_constraints : universe_level_subst -> constraints -> const val normalize_univs_level_level : universe_level_subst -> universe_level -> universe_level + +val empty_subst : universe_subst +val is_empty_subst : universe_subst -> bool val make_subst : universe_subst -> universe_subst_fn (* val subst_univs_level_fail : universe_subst_fn -> universe_level -> universe_level *) diff --git a/kernel/vars.ml b/kernel/vars.ml index 40a797a90..120c07d30 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -299,5 +299,5 @@ let subst_univs_level_constr subst c = let c' = aux c in if !changed then c' else c -let subst_univs_context s = - map_rel_context (subst_univs_constr s) +let subst_univs_level_context s = + map_rel_context (subst_univs_level_constr s) diff --git a/kernel/vars.mli b/kernel/vars.mli index 9d5d16d0c..b4f616b13 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -78,7 +78,9 @@ val subst_univs_fn_puniverses : universe_level_subst_fn -> 'a puniverses -> 'a puniverses val subst_univs_constr : universe_subst -> constr -> constr + +(** Level substitutions for polymorphism. *) + val subst_univs_puniverses : universe_level_subst -> 'a puniverses -> 'a puniverses val subst_univs_level_constr : universe_level_subst -> constr -> constr - -val subst_univs_context : Univ.universe_subst -> rel_context -> rel_context +val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context diff --git a/library/universes.ml b/library/universes.ml index dd5331fa7..f6922e495 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -41,43 +41,56 @@ let fresh_instance_from_context ctx = (inst, subst), constraints let fresh_instance ctx = - let s = ref LSet.empty in + let ctx' = ref LSet.empty in + let s = ref LMap.empty in let inst = - Instance.subst_fn (fun _ -> - let u = new_univ_level (Global.current_dirpath ()) in - s := LSet.add u !s; u) + Instance.subst_fn (fun v -> + let u = new_univ_level (Global.current_dirpath ()) in + ctx' := LSet.add u !ctx'; + s := LMap.add v u !s; u) (UContext.instance ctx) - in !s, inst - -let fresh_instance_from ctx = - let ctx', inst = fresh_instance ctx in - let subst = make_universe_subst inst ctx in + in !ctx', !s, inst + +let existing_instance ctx inst = + let s = ref LMap.empty in + let () = + Array.iter2 (fun u v -> + s := LMap.add v u !s) + (Instance.to_array inst) (Instance.to_array (UContext.instance ctx)) + in LSet.empty, !s, inst + +let fresh_instance_from ctx inst = + let ctx', subst, inst = + match inst with + | Some inst -> existing_instance ctx inst + | None -> fresh_instance ctx + in let constraints = instantiate_univ_context subst ctx in (inst, subst), (ctx', constraints) - + let unsafe_instance_from ctx = (Univ.UContext.instance ctx, ctx) - + (** Fresh universe polymorphic construction *) -let fresh_constant_instance env c = +let fresh_constant_instance env c inst = let cb = lookup_constant c env in if cb.Declarations.const_polymorphic then - let (inst,_), ctx = fresh_instance_from (Declareops.universes_of_constant cb) in + let (inst,_), ctx = fresh_instance_from (Declareops.universes_of_constant cb) inst in ((c, inst), ctx) else ((c,Instance.empty), ContextSet.empty) -let fresh_inductive_instance env ind = +let fresh_inductive_instance env ind inst = let mib, mip = Inductive.lookup_mind_specif env ind in if mib.Declarations.mind_polymorphic then - let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes in + let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes inst in ((ind,inst), ctx) else ((ind,Instance.empty), ContextSet.empty) -let fresh_constructor_instance env (ind,i) = +let fresh_constructor_instance env (ind,i) inst = let mib, mip = Inductive.lookup_mind_specif env ind in if mib.Declarations.mind_polymorphic then - let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes in + let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes inst in (((ind,i),inst), ctx) else (((ind,i),Instance.empty), ContextSet.empty) @@ -104,19 +117,28 @@ let unsafe_constructor_instance env (ind,i) = open Globnames -let fresh_global_instance env gr = +let fresh_global_instance ?names env gr = match gr with | VarRef id -> mkVar id, ContextSet.empty | ConstRef sp -> - let c, ctx = fresh_constant_instance env sp in + let c, ctx = fresh_constant_instance env sp names in mkConstU c, ctx | ConstructRef sp -> - let c, ctx = fresh_constructor_instance env sp in + let c, ctx = fresh_constructor_instance env sp names in mkConstructU c, ctx | IndRef sp -> - let c, ctx = fresh_inductive_instance env sp in + let c, ctx = fresh_inductive_instance env sp names in mkIndU c, ctx +let fresh_constant_instance env sp = + fresh_constant_instance env sp None + +let fresh_inductive_instance env sp = + fresh_inductive_instance env sp None + +let fresh_constructor_instance env sp = + fresh_constructor_instance env sp None + let unsafe_global_instance env gr = match gr with | VarRef id -> mkVar id, UContext.empty @@ -185,14 +207,15 @@ let type_of_reference env r = let cb = Environ.lookup_constant c env in let ty = Typeops.type_of_constant_type env cb.const_type in if cb.const_polymorphic then - let (inst, subst), ctx = fresh_instance_from (Declareops.universes_of_constant cb) in - Vars.subst_univs_constr subst ty, ctx + let (inst, subst), ctx = + fresh_instance_from (Declareops.universes_of_constant cb) None in + Vars.subst_univs_level_constr subst ty, ctx else ty, ContextSet.empty | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in if mib.mind_polymorphic then - let (inst, subst), ctx = fresh_instance_from mib.mind_universes in + let (inst, subst), ctx = fresh_instance_from mib.mind_universes None in let ty = Inductive.type_of_inductive env (specif, inst) in ty, ctx else @@ -201,7 +224,7 @@ let type_of_reference env r = | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in if mib.mind_polymorphic then - let (inst, subst), ctx = fresh_instance_from mib.mind_universes in + let (inst, subst), ctx = fresh_instance_from mib.mind_universes None in Inductive.type_of_constructor (cstr,inst) specif, ctx else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty diff --git a/library/universes.mli b/library/universes.mli index 4544bd4d3..e5d3ded58 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -26,24 +26,24 @@ val new_Type_sort : Names.dir_path -> sorts the instantiated constraints. *) val fresh_instance_from_context : universe_context -> - (universe_instance * universe_subst) constrained + (universe_instance * universe_level_subst) constrained -val fresh_instance_from : universe_context -> - (universe_instance * universe_subst) in_universe_context_set +val fresh_instance_from : universe_context -> universe_instance option -> + (universe_instance * universe_level_subst) in_universe_context_set val new_global_univ : unit -> universe in_universe_context_set val new_sort_in_family : sorts_family -> sorts val fresh_sort_in_family : env -> sorts_family -> sorts in_universe_context_set -val fresh_constant_instance : env -> constant -> +val fresh_constant_instance : env -> constant -> pconstant in_universe_context_set -val fresh_inductive_instance : env -> inductive -> +val fresh_inductive_instance : env -> inductive -> pinductive in_universe_context_set -val fresh_constructor_instance : env -> constructor -> +val fresh_constructor_instance : env -> constructor -> pconstructor in_universe_context_set -val fresh_global_instance : env -> Globnames.global_reference -> +val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference -> constr in_universe_context_set val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 499e7b053..81645a580 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -152,7 +152,9 @@ GEXTEND Gram sort: [ [ "Set" -> GSet | "Prop" -> GProp - | "Type" -> GType None ] ] + | "Type" -> GType None + | "Type"; "{"; id = string; "}" -> GType (Some id) + ] ] ; lconstr: [ [ c = operconstr LEVEL "200" -> c ] ] @@ -277,13 +279,17 @@ GEXTEND Gram | c=operconstr LEVEL "9" -> (c,None) ] ] ; atomic_constr: - [ [ g=global -> CRef (g,None) + [ [ g=global; i=instance -> CRef (g,i) | s=sort -> CSort (!@loc,s) | n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n)) | s=string -> CPrim (!@loc, String s) | "_" -> CHole (!@loc, None, None) | id=pattern_ident -> CPatVar(!@loc,(false,id)) ] ] ; + instance: + [ [ "@{"; l = LIST1 sort SEP ","; "}" -> Some l + | -> None ] ] + ; fix_constr: [ [ fx1=single_fix -> mk_single_fix fx1 | (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with"; diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 652c5acf9..65a8f338c 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 42d98cdfe..e8b360b86 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 a360351b7..8a9753e5b 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 bed77e622..9f58b4c80 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 07dacd0cc..43552ef54 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 add47e5b7..31576391b 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 2cf730f11..b21f4e383 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 diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 950594397..019fad0ce 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -119,7 +119,7 @@ let pr_qualid = pr_qualid let pr_patvar = pr_id let pr_universe_instance l = - pr_opt (pr_in_comment Univ.Instance.pr) l + pr_opt (pr_in_comment (prlist_with_sep spc pr_glob_sort)) l let pr_cref ref us = pr_reference ref ++ pr_universe_instance us diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 08c887b77..7a536b35a 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -103,7 +103,7 @@ let get_sym_eq_data env (ind,u) = not (Int.equal (Array.length mip.mind_nf_lc) 1) then error "Not an inductive type with a single constructor."; let subst = Inductive.make_inductive_subst mib u in - let arityctxt = Vars.subst_univs_context subst mip.mind_arity_ctxt in + let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in let realsign,_ = List.chop mip.mind_nrealargs_ctxt arityctxt in if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then error "Inductive equalities with local definitions in arity not supported."; @@ -115,7 +115,7 @@ let get_sym_eq_data env (ind,u) = if mip.mind_nrealargs > mib.mind_nparams then error "Constructors arguments must repeat the parameters."; let _,params2 = List.chop (mib.mind_nparams-mip.mind_nrealargs) params in - let paramsctxt = Vars.subst_univs_context subst mib.mind_params_ctxt in + let paramsctxt = Vars.subst_univs_level_context subst mib.mind_params_ctxt in let paramsctxt1,_ = List.chop (mib.mind_nparams-mip.mind_nrealargs) paramsctxt in if not (List.equal eq_constr params2 constrargs) then @@ -139,7 +139,7 @@ let get_non_sym_eq_data env (ind,u) = not (Int.equal (Array.length mip.mind_nf_lc) 1) then error "Not an inductive type with a single constructor."; let subst = Inductive.make_inductive_subst mib u in - let arityctxt = Vars.subst_univs_context subst mip.mind_arity_ctxt in + let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in let realsign,_ = List.chop mip.mind_nrealargs_ctxt arityctxt in if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then error "Inductive equalities with local definitions in arity not supported"; @@ -148,8 +148,8 @@ let get_non_sym_eq_data env (ind,u) = if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; let _,constrargs = List.chop mib.mind_nparams constrargs in - let constrargs = List.map (Vars.subst_univs_constr subst) constrargs in - let paramsctxt = Vars.subst_univs_context subst mib.mind_params_ctxt in + let constrargs = List.map (Vars.subst_univs_level_constr subst) constrargs in + let paramsctxt = Vars.subst_univs_level_context subst mib.mind_params_ctxt in (specif,constrargs,realsign,paramsctxt,mip.mind_nrealargs) (**********************************************************************) @@ -735,8 +735,8 @@ let build_congr env (eq,refl,ctx) ind = if not (Int.equal mip.mind_nrealargs 1) then error "Expect an inductive type with one predicate parameter."; let i = 1 in - let arityctxt = Vars.subst_univs_context subst mip.mind_arity_ctxt in - let paramsctxt = Vars.subst_univs_context subst mib.mind_params_ctxt in + let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in + let paramsctxt = Vars.subst_univs_level_context subst mib.mind_params_ctxt in let realsign,_ = List.chop mip.mind_nrealargs_ctxt arityctxt in if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then error "Inductive equalities with local definitions in arity not supported."; diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 99284eb54..fd299b43a 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -1,3 +1,28 @@ +Module withoutpoly. + +Inductive empty :=. + +Inductive emptyt : Type :=. +Inductive singleton : Type := + single. +Inductive singletoninfo : Type := + singleinfo : unit -> singletoninfo. +Inductive singletonset : Set := + singleset. + +Inductive singletonnoninfo : Type := + singlenoninfo : empty -> singletonnoninfo. + +Inductive singletoninfononinfo : Prop := + singleinfononinfo : unit -> singletoninfononinfo. + +Inductive bool : Type := + | true | false. + +Inductive smashedbool : Prop := + | trueP | falseP. +End withoutpoly. + Set Universe Polymorphism. Inductive empty :=. @@ -225,7 +250,7 @@ Fail Check fun A : Type => foo A. Check fun A : Prop => foo A. Fail Definition bar := fun A : Set => foo A. -Fail Check (let A := Type in foo (id A)). +Check (let A := Type in foo (id A)). Definition fooS (A : Set) := A. |