From e759333a8b5c11247c4cc134fdde8c1bd85a6e17 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 11 Sep 2015 18:07:39 +0200 Subject: Universes: enforce Set <= i for all Type occurrences. --- pretyping/evd.ml | 41 +++++++++++++++++++++++++++-------------- pretyping/evd.mli | 6 +++--- 2 files changed, 30 insertions(+), 17 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 632611291..fe5f12dd8 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -453,7 +453,7 @@ let add_constraints_context ctx cstrs = in { ctx with uctx_local = (univs, Univ.Constraint.union local local'); uctx_univ_variables = vars; - uctx_universes = Univ.merge_constraints cstrs ctx.uctx_universes } + uctx_universes = Univ.merge_constraints local' ctx.uctx_universes } (* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) (* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) @@ -1058,36 +1058,49 @@ let with_context_set rigid d (a, ctx) = let add_uctx_names s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l s names_rev) -let uctx_new_univ_variable rigid name +let uctx_new_univ_variable rigid name predicative ({ 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.add_universe u ctx in - let uctx' = + let uctx', pred = match rigid with - | UnivRigid -> uctx + | UnivRigid -> uctx, true | UnivFlexible b -> let uvars' = Univ.LMap.add u None uvars in if b then {uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = Univ.LSet.add u avars} - else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in + uctx_univ_algebraic = Univ.LSet.add u avars}, false + else {uctx with uctx_univ_variables = uvars'}, false + in + (* let ctx' = *) + (* if pred then *) + (* Univ.ContextSet.add_constraints *) + (* (Univ.Constraint.singleton (Univ.Level.set, Univ.Le, u)) ctx' *) + (* else ctx' *) + (* in *) let names = match name with | Some n -> add_uctx_names n u uctx.uctx_names | None -> uctx.uctx_names in + let initial = + Univ.add_universe u pred uctx.uctx_initial_universes + in + let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = Univ.add_universe u uctx.uctx_universes}, u - -let new_univ_level_variable ?name rigid evd = - let uctx', u = uctx_new_univ_variable rigid name evd.universes in + uctx_universes = Univ.add_universe u pred uctx.uctx_universes; + uctx_initial_universes = initial} + in uctx', u + +let new_univ_level_variable ?name ?(predicative=true) rigid evd = + let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in ({evd with universes = uctx'}, u) -let new_univ_variable ?name rigid evd = - let uctx', u = uctx_new_univ_variable rigid name evd.universes in +let new_univ_variable ?name ?(predicative=true) rigid evd = + let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in ({evd with universes = uctx'}, Univ.Universe.make u) -let new_sort_variable ?name rigid d = - let (d', u) = new_univ_variable rigid ?name d in +let new_sort_variable ?name ?(predicative=true) rigid d = + let (d', u) = new_univ_variable rigid ?name ~predicative d in (d', Type u) let make_flexible_variable evd b u = diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 94d9d5f66..c2ccc6d21 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -505,9 +505,9 @@ val normalize_evar_universe_context_variables : evar_universe_context -> val normalize_evar_universe_context : evar_universe_context -> evar_universe_context -val new_univ_level_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?name:string -> rigid -> evar_map -> evar_map * sorts +val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level +val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe +val new_sort_variable : ?name:string -> ?predicative:bool -> 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 option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is -- cgit v1.2.3 From 79163d582abc2e22512f0924675b6b0f0928f0ef Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 15 Sep 2015 18:31:44 +0200 Subject: Univs: Fix part of bug #4161 Rechecking applications built by evarconv's imitation. --- pretyping/evarsolve.ml | 43 +++++++++++++++++++++++++++++++++++++------ 1 file changed, 37 insertions(+), 6 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index ac1692f45..a2189d5e4 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -107,6 +107,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c = let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in refresh_universes (Some false) env sigma ty + (************************) (* Unification results *) @@ -127,6 +128,32 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd | None -> add_conv_pb ~tail (Reduction.CONV,env,t1,t2) evd +(* We retype applications to ensure the universe constraints are collected *) + +let recheck_applications conv_algo env evdref t = + let rec aux env t = + match kind_of_term t with + | App (f, args) -> + let () = aux env f in + let fty = Retyping.get_type_of env !evdref f in + let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in + let rec aux i ty = + if i < Array.length argsty then + match kind_of_term (whd_betadeltaiota env !evdref ty) with + | Prod (na, dom, codom) -> + (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with + | Success evd -> evdref := evd; + aux (succ i) (subst1 args.(i) codom) + | UnifFailure (evd, reason) -> + Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom)) + | _ -> assert false + else () + in aux 0 fty + | _ -> + iter_constr_with_full_binders (fun d env -> push_rel d env) aux env t + in aux env t + + (*------------------------------------* * Restricting existing evars * *------------------------------------*) @@ -1404,10 +1431,10 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = evdref := restrict_evar evd (fst ev'') None (UpdateWith candidates); evar'') | None -> - (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *) - map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) - imitate envk t in - + (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *) + map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) + imitate envk t + in let rhs = whd_beta evd rhs (* heuristic *) in let fast rhs = let filter_ctxt = evar_filtered_context evi in @@ -1426,8 +1453,12 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = in let body = if fast rhs then nf_evar evd rhs - else imitate (env,0) rhs - in (!evdref,body) + else + let t' = imitate (env,0) rhs in + if !progress then + (recheck_applications conv_algo (evar_env evi) evdref t'; t') + else t' + in (!evdref,body) (* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said, -- cgit v1.2.3 From 1cd87577ab85a402fb0482678dfcdbe85b45ce38 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 15 Sep 2015 18:33:04 +0200 Subject: Univs: force all universes to be >= Set. --- pretyping/evd.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evd.ml b/pretyping/evd.ml index fe5f12dd8..9f2d28438 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -385,7 +385,7 @@ let process_universe_constraints univs vars alg cstrs = let levels = Univ.Universe.levels l in Univ.LSet.fold (fun l local -> if Univ.Level.is_small l || Univ.LMap.mem l !vars then - Univ.enforce_eq (Univ.Universe.make l) r local + unify_universes fo (Univ.Universe.make l) Universes.UEq r local else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None))) levels local else @@ -1083,11 +1083,11 @@ let uctx_new_univ_variable rigid name predicative | None -> uctx.uctx_names in let initial = - Univ.add_universe u pred uctx.uctx_initial_universes + Univ.add_universe u true uctx.uctx_initial_universes in let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = Univ.add_universe u pred uctx.uctx_universes; + uctx_universes = Univ.add_universe u true uctx.uctx_universes; uctx_initial_universes = initial} in uctx', u -- cgit v1.2.3 From 4838a3a3c25cc9f7583dd62e4585460aca8ee961 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 21 Sep 2015 11:55:32 +0200 Subject: Forcing i > Set for global universes (incomplete) --- kernel/environ.ml | 39 +++++++++++++++++++++++++++------------ kernel/environ.mli | 4 ++-- kernel/term_typing.ml | 8 ++++---- kernel/univ.ml | 26 ++++++++++++++------------ kernel/univ.mli | 4 ++-- library/universes.ml | 9 +++++++-- pretyping/evd.ml | 4 ++-- test-suite/bugs/closed/3309.v | 6 +++--- 8 files changed, 61 insertions(+), 39 deletions(-) (limited to 'pretyping') diff --git a/kernel/environ.ml b/kernel/environ.ml index 109e3830c..c433c0789 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -181,26 +181,41 @@ let fold_named_context_reverse f ~init env = (* Universe constraints *) -let add_constraints c env = - if Univ.Constraint.is_empty c then - env - else - let s = env.env_stratification in +let map_universes f env = + let s = env.env_stratification in { env with env_stratification = - { s with env_universes = Univ.merge_constraints c s.env_universes } } + { s with env_universes = f s.env_universes } } + +let add_constraints c env = + if Univ.Constraint.is_empty c then env + else map_universes (Univ.merge_constraints c) env let check_constraints c env = Univ.check_constraints c env.env_stratification.env_universes -let set_engagement c env = (* Unsafe *) - { env with env_stratification = - { env.env_stratification with env_engagement = c } } - let push_constraints_to_env (_,univs) env = add_constraints univs env -let push_context ctx env = add_constraints (Univ.UContext.constraints ctx) env -let push_context_set ctx env = add_constraints (Univ.ContextSet.constraints ctx) env +let add_universes strict ctx g = + let g = Array.fold_left (fun g v -> Univ.add_universe v strict g) + g (Univ.Instance.to_array (Univ.UContext.instance ctx)) + in + Univ.merge_constraints (Univ.UContext.constraints ctx) g + +let push_context ?(strict=false) ctx env = + map_universes (add_universes strict ctx) env + +let add_universes_set strict ctx g = + let g = Univ.LSet.fold (fun v g -> Univ.add_universe v strict g) + (Univ.ContextSet.levels ctx) g + in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g + +let push_context_set ?(strict=false) ctx env = + map_universes (add_universes_set strict ctx) env + +let set_engagement c env = (* Unsafe *) + { env with env_stratification = + { env.env_stratification with env_engagement = c } } (* Global constants *) diff --git a/kernel/environ.mli b/kernel/environ.mli index 4ad0327fc..9f6ea522a 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -208,8 +208,8 @@ val add_constraints : Univ.constraints -> env -> env (** Check constraints are satifiable in the environment. *) val check_constraints : Univ.constraints -> env -> bool -val push_context : Univ.universe_context -> env -> env -val push_context_set : Univ.universe_context_set -> env -> env +val push_context : ?strict:bool -> Univ.universe_context -> env -> env +val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env val push_constraints_to_env : 'a Univ.constrained -> env -> env val set_engagement : engagement -> env -> env diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 83e566041..e89b6ef8f 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -100,11 +100,11 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) - + let infer_declaration env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> - let env = push_context uctx env in + let env = push_context ~strict:(not poly) uctx env in let j = infer env t in let abstract = poly && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract uctx in @@ -115,7 +115,7 @@ let infer_declaration env kn dcl = | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; const_entry_polymorphic = false} as c) -> - let env = push_context c.const_entry_universes env in + let env = push_context ~strict:true c.const_entry_universes env in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = @@ -135,7 +135,7 @@ let infer_declaration env kn dcl = c.const_entry_inline_code, c.const_entry_secctx | DefinitionEntry c -> - let env = push_context c.const_entry_universes env in + let env = push_context ~strict:(not c.const_entry_polymorphic) c.const_entry_universes env in let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in diff --git a/kernel/univ.ml b/kernel/univ.ml index 040e9bc27..b61b441d2 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -750,17 +750,6 @@ let get_set_arc g = repr g Level.set let is_set_arc u = Level.is_set u.univ let is_prop_arc u = Level.is_prop u.univ -let add_universe vlev ~predicative g = - let v = terminal ~predicative vlev in - let arc = - let arc = - if predicative then get_set_arc g else get_prop_arc g - in - { arc with le=vlev::arc.le} - in - let g = enter_arc arc g in - enter_arc v g - (* [safe_repr] also search for the canonical representative, but if the graph doesn't contain the searched universe, we add it. *) @@ -777,6 +766,18 @@ let safe_repr g u = let g = enter_arc {setarc with le=u::setarc.le} g in enter_arc can g, can +let add_universe vlev strict g = + let v = terminal ~predicative:true vlev in + let arc = + let arc = get_set_arc g in + if strict then + { arc with lt=vlev::arc.lt} + else + { arc with le=vlev::arc.le} + in + let g = enter_arc arc g in + enter_arc v g + (* reprleq : canonical_arc -> canonical_arc list *) (* All canonical arcv such that arcu<=arcv with arcv#arcu *) let reprleq g arcu = @@ -1145,7 +1146,8 @@ let merge g arcu arcv = (* we find the arc with the biggest rank, and we redirect all others to it *) let arcu, g, v = let best_ranked (max_rank, old_max_rank, best_arc, rest) arc = - if arc.rank >= max_rank && not (Level.is_small best_arc.univ) + if Level.is_small arc.univ || + (arc.rank >= max_rank && not (Level.is_small best_arc.univ)) then (arc.rank, max_rank, arc, best_arc::rest) else (max_rank, old_max_rank, best_arc, arc::rest) in diff --git a/kernel/univ.mli b/kernel/univ.mli index 76453cbb0..fe7fc1ab9 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -163,8 +163,8 @@ val is_initial_universes : universes -> bool val sort_universes : universes -> universes -(** Adds a universe to the graph, ensuring it is >= Prop or Set. *) -val add_universe : universe_level -> predicative:bool -> universes -> universes +(** Adds a universe to the graph, ensuring it is >= or > Set. *) +val add_universe : universe_level -> bool -> universes -> universes (** {6 Constraints. } *) diff --git a/library/universes.ml b/library/universes.ml index c67371e3b..0544585dc 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -830,8 +830,13 @@ let normalize_context_set ctx us algs = (** Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> - if d == Le && Univ.Level.is_small l then - (Constraint.add cstr smallles, noneqs) + if d == Le then + if Univ.Level.is_small l then + (Constraint.add cstr smallles, noneqs) + else if Level.is_small r then + raise (Univ.UniverseInconsistency + (Le,Universe.make l,Universe.make r,None)) + else (smallles, Constraint.add cstr noneqs) else (smallles, Constraint.add cstr noneqs)) csts (Constraint.empty, Constraint.empty) in diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 9f2d28438..a25479d48 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1083,11 +1083,11 @@ let uctx_new_univ_variable rigid name predicative | None -> uctx.uctx_names in let initial = - Univ.add_universe u true uctx.uctx_initial_universes + Univ.add_universe u false uctx.uctx_initial_universes in let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = Univ.add_universe u true uctx.uctx_universes; + uctx_universes = Univ.add_universe u false uctx.uctx_universes; uctx_initial_universes = initial} in uctx', u diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v index 980431576..6e97ed2af 100644 --- a/test-suite/bugs/closed/3309.v +++ b/test-suite/bugs/closed/3309.v @@ -117,7 +117,7 @@ intros. hnf. apply dirprodpair. exact ax0. apply dirprodpair. exact ax1. exact a Defined. Definition eqax0 { X : UU } { R : hrel X } { A : hsubtypes X } : iseqclass R A -> ishinh ( carrier A ) . -intros X R A; exact ( fun is : iseqclass R A => projT1' _ is ). +intros X R A. exact (fun is : iseqclass R A => projT1' _ is ). Defined. Lemma iseqclassdirprod { X Y : UU } { R : hrel X } { Q : hrel Y } { A : hsubtypes X } { B : hsubtypes Y } ( isa : iseqclass R A ) ( isb : iseqclass Q B ) : iseqclass ( hreldirprod R Q ) ( subtypesdirprod A B ) . @@ -141,7 +141,7 @@ Definition prtoimage { X Y : UU } (f : X -> Y) : X -> image f. admit. Defined. -Definition setquot { X : UU } ( R : hrel X ) : Type. +Definition setquot { X : UU } ( R : hrel X ) : Set. intros; exact ( sigT' ( fun A : _ => iseqclass R A ) ). Defined. Definition setquotpair { X : UU } ( R : hrel X ) ( A : hsubtypes X ) ( is : iseqclass R A ) : setquot R. @@ -157,7 +157,7 @@ Definition setquotinset { X : UU } ( R : hrel X ) : hSet. intros; exact ( hSetpair (setquot R) admit) . Defined. -Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ). +Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot@{i j k l m n p Set q r} RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ). intros; exact ( setquotpair _ _ ( iseqclassdirprod ( projT2' _ ( projT1' _ cd ) ) ( projT2' _ ( projT2' _ cd ) ) ) ). Defined. -- cgit v1.2.3 From 91f5467917266a85496fb718dfc30eff3565d4dc Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:20:42 +0200 Subject: Univs (evd): deal with global universes and sideff - Fix union of universe contexts to keep declarations - Fix side-effect handling to register new global universes in the graph. --- pretyping/evd.ml | 137 ++++++++++++++++++++++++++++++++++++------------------ pretyping/evd.mli | 2 + 2 files changed, 95 insertions(+), 44 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evd.ml b/pretyping/evd.ml index a25479d48..8243f96c1 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -310,6 +310,9 @@ let union_evar_universe_context ctx ctx' = else let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in + let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) + (Univ.ContextSet.levels ctx.uctx_local) in + let declarenew g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g in let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); uctx_local = local; @@ -317,12 +320,12 @@ let union_evar_universe_context ctx ctx' = Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; uctx_univ_algebraic = Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic; - uctx_initial_universes = ctx.uctx_initial_universes; + uctx_initial_universes = declarenew ctx.uctx_initial_universes; uctx_universes = if local == ctx.uctx_local then ctx.uctx_universes else let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in - Univ.merge_constraints cstrsr ctx.uctx_universes } + Univ.merge_constraints cstrsr (declarenew ctx.uctx_universes) } (* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *) (* let union_evar_universe_context = *) @@ -935,38 +938,6 @@ let evars_of_filtered_evar_info evi = | Evar_defined b -> evars_of_term b) (evars_of_named_context (evar_filtered_context evi))) -(**********************************************************) -(* Side effects *) - -let emit_side_effects eff evd = - { evd with effects = Declareops.union_side_effects eff evd.effects; } - -let drop_side_effects evd = - { evd with effects = Declareops.no_seff; } - -let eval_side_effects evd = evd.effects - -(* Future goals *) -let declare_future_goal evk evd = - { evd with future_goals = evk::evd.future_goals } - -let declare_principal_goal evk evd = - match evd.principal_future_goal with - | None -> { evd with - future_goals = evk::evd.future_goals; - principal_future_goal=Some evk; } - | Some _ -> Errors.error "Only one main subgoal per instantiation." - -let future_goals evd = evd.future_goals - -let principal_future_goal evd = evd.principal_future_goal - -let reset_future_goals evd = - { evd with future_goals = [] ; principal_future_goal=None } - -let restore_future_goals evd gls pgl = - { evd with future_goals = gls ; principal_future_goal = pgl } - (**********************************************************) (* Sort variables *) @@ -1022,13 +993,13 @@ let restrict_universe_context evd vars = let universe_subst evd = evd.universes.uctx_univ_variables -let merge_uctx rigid uctx ctx' = +let merge_uctx sideff rigid uctx ctx' = let open Univ in - let uctx = + let levels = ContextSet.levels ctx' in + let uctx = if sideff then uctx else match rigid with | UnivRigid -> uctx | UnivFlexible b -> - let levels = ContextSet.levels ctx' in let fold u accu = if LMap.mem u accu then accu else LMap.add u None accu @@ -1039,12 +1010,23 @@ let merge_uctx rigid uctx ctx' = uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels } else { uctx with uctx_univ_variables = uvars' } in - let uctx_local = ContextSet.append ctx' uctx.uctx_local in - let uctx_universes = merge_constraints (ContextSet.constraints ctx') uctx.uctx_universes in - { uctx with uctx_local; uctx_universes } + let uctx_local = + if sideff then uctx.uctx_local + else ContextSet.append ctx' uctx.uctx_local + in + let declare g = + LSet.fold (fun u g -> + try Univ.add_universe u false g + with Univ.AlreadyDeclared when sideff -> g) + levels g + in + let initial = declare uctx.uctx_initial_universes in + let univs = declare uctx.uctx_universes in + let uctx_universes = merge_constraints (ContextSet.constraints ctx') univs in + { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } let merge_context_set rigid evd ctx' = - {evd with universes = merge_uctx rigid evd.universes ctx'} + {evd with universes = merge_uctx false rigid evd.universes ctx'} let merge_uctx_subst uctx s = { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } @@ -1055,6 +1037,24 @@ let merge_universe_subst evd subst = let with_context_set rigid d (a, ctx) = (merge_context_set rigid d ctx, a) +let emit_universe_side_effects eff u = + Declareops.fold_side_effects + (fun acc eff -> + match eff with + | Declarations.SEscheme (l,s) -> + List.fold_left + (fun acc (_,_,cb,c) -> + let acc = match c with + | `Nothing -> acc + | `Opaque (s, ctx) -> merge_uctx true univ_rigid acc ctx + in if cb.Declarations.const_polymorphic then acc + else + merge_uctx true univ_rigid acc + (Univ.ContextSet.of_context cb.Declarations.const_universes)) + acc l + | Declarations.SEsubproof _ -> acc) + u eff + let add_uctx_names s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l s names_rev) @@ -1103,6 +1103,18 @@ let new_sort_variable ?name ?(predicative=true) rigid d = let (d', u) = new_univ_variable rigid ?name ~predicative d in (d', Type u) +let add_global_univ d u = + let uctx = d.universes in + let initial = + Univ.add_universe u true uctx.uctx_initial_universes + in + let univs = + Univ.add_universe u true uctx.uctx_universes + in + { d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local; + uctx_initial_universes = initial; + uctx_universes = univs } } + let make_flexible_variable evd b u = let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as ctx = evd.universes in let uvars' = Univ.LMap.add u None uvars in @@ -1291,12 +1303,16 @@ let refresh_undefined_univ_variables uctx = Univ.LMap.add (Univ.subst_univs_level_level subst u) (Option.map (Univ.subst_univs_level_universe subst) v) acc) uctx.uctx_univ_variables Univ.LMap.empty - in + in + let declare g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g) + (Univ.ContextSet.levels ctx') g in + let initial = declare uctx.uctx_initial_universes in + let univs = declare Univ.initial_universes in let uctx' = {uctx_names = uctx.uctx_names; uctx_local = ctx'; uctx_univ_variables = vars; uctx_univ_algebraic = alg; - uctx_universes = Univ.initial_universes; - uctx_initial_universes = uctx.uctx_initial_universes } in + uctx_universes = univs; + uctx_initial_universes = initial } in uctx', subst let refresh_undefined_universes evd = @@ -1382,6 +1398,39 @@ let e_eq_constr_univs evdref t u = let evd, b = eq_constr_univs !evdref t u in evdref := evd; b +(**********************************************************) +(* Side effects *) + +let emit_side_effects eff evd = + { evd with effects = Declareops.union_side_effects eff evd.effects; + universes = emit_universe_side_effects eff evd.universes } + +let drop_side_effects evd = + { evd with effects = Declareops.no_seff; } + +let eval_side_effects evd = evd.effects + +(* Future goals *) +let declare_future_goal evk evd = + { evd with future_goals = evk::evd.future_goals } + +let declare_principal_goal evk evd = + match evd.principal_future_goal with + | None -> { evd with + future_goals = evk::evd.future_goals; + principal_future_goal=Some evk; } + | Some _ -> Errors.error "Only one main subgoal per instantiation." + +let future_goals evd = evd.future_goals + +let principal_future_goal evd = evd.principal_future_goal + +let reset_future_goals evd = + { evd with future_goals = [] ; principal_future_goal=None } + +let restore_future_goals evd gls pgl = + { evd with future_goals = gls ; principal_future_goal = pgl } + (**********************************************************) (* Accessing metas *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index c2ccc6d21..5a59c1776 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -508,6 +508,8 @@ val normalize_evar_universe_context : evar_universe_context -> val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts +val add_global_univ : evar_map -> Univ.Level.t -> evar_map + val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map val is_sort_variable : evar_map -> sorts -> Univ.universe_level option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is -- cgit v1.2.3 From 02aace9f038d579e9cf32dc2f5b21d415e977c03 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:23:43 +0200 Subject: Univs (pretyping): allow parsing and decl of Top.n This allows pretyping and detyping to be inverses regarding universes, and makes Function's detyping/pretyping manipulations bearable in presence of global universes that must be declared (otherwise an evd would need to be threaded there in many places as well). --- pretyping/pretyping.ml | 29 +++++++++++++++++++++-------- 1 file changed, 21 insertions(+), 8 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2858a5c1f..edb76e52f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -102,14 +102,27 @@ let ((constr_in : constr -> Dyn.t), (** Miscellaneous interpretation functions *) let interp_universe_level_name evd s = let names, _ = Universes.global_universe_names () in - try - let id = try Id.of_string s with _ -> raise Not_found in - evd, Idmap.find id names - with Not_found -> - try let level = Evd.universe_of_name evd s in - evd, level - with Not_found -> - new_univ_level_variable ~name:s univ_rigid evd + if CString.string_contains s "." then + match List.rev (CString.split '.' s) with + | [] -> anomaly (str"Invalid universe name " ++ str s) + | n :: dp -> + let num = int_of_string n in + let dp = DirPath.make (List.map Id.of_string dp) in + let level = Univ.Level.make dp num in + let evd = + try Evd.add_global_univ evd level + with Univ.AlreadyDeclared -> evd + in evd, level + else + try + let id = + try Id.of_string s with _ -> raise Not_found in + evd, Idmap.find id names + with Not_found -> + 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_universe evd = function | [] -> let evd, l = new_univ_level_variable univ_rigid evd in -- cgit v1.2.3 From 91b1808056602f3e26d1eb1bdf7be1e791cb742d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:35:07 +0200 Subject: Univs: fix many evar_map initializations and leaks. --- pretyping/typeclasses.ml | 2 +- stm/lemmas.ml | 3 +- tactics/autorewrite.ml | 5 ++- tactics/equality.ml | 4 ++- tactics/extratactics.ml4 | 7 +++-- tactics/hints.ml | 3 +- tactics/rewrite.ml | 24 ++++++++------ tactics/tacticals.ml | 10 +++--- toplevel/classes.ml | 15 +++++---- toplevel/command.ml | 13 +++++--- toplevel/obligations.ml | 19 +++++++----- toplevel/record.ml | 79 ++++++++++++++++++++++++++--------------------- toplevel/vernacentries.ml | 5 +-- 13 files changed, 112 insertions(+), 77 deletions(-) (limited to 'pretyping') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 18e83056b..2ef289650 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -370,7 +370,7 @@ let add_instance check inst = List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path (is_local inst) pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) - (Global.env ()) Evd.empty inst.is_impl inst.is_pri) + (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_pri) let rebuild_instance (action, inst) = let () = match action with diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 7679b1a66..2bd1c5451 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -503,4 +503,5 @@ let save_proof ?proof = function let get_current_context () = try Pfedit.get_current_goal_context () with e when Logic.catchable_exception e -> - (Evd.empty, Global.env()) + let env = Global.env () in + (Evd.from_env env, env) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 2b3fadf7f..3a9d40de0 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -292,10 +292,13 @@ let find_applied_relation metas loc env sigma c left2right = (* To add rewriting rules to a base *) let add_rew_rules base lrul = let counter = ref 0 in + let env = Global.env () in + let sigma = Evd.from_env env in let lrul = List.fold_left (fun dn (loc,(c,ctx),b,t) -> - let info = find_applied_relation false loc (Global.env ()) Evd.empty c b in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in + let info = find_applied_relation false loc env sigma c b in let pat = if b then info.hyp_left else info.hyp_right in let rul = { rew_lemma = c; rew_type = info.hyp_ty; rew_pat = pat; rew_ctx = ctx; rew_l2r = b; diff --git a/tactics/equality.ml b/tactics/equality.ml index d012427a0..53678aa84 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -335,7 +335,9 @@ let find_elim hdcncl lft2rgt dep cls ot gl = | Ind (ind,u) -> let c, eff = find_scheme scheme_name ind in (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *) - let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in + let sigma, elim = + Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) + in sigma, elim, eff | _ -> assert false diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index af0870bc9..ead26e964 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -262,7 +262,8 @@ TACTIC EXTEND rewrite_star (* Hint Rewrite *) let add_rewrite_hint bases ort t lcsr = - let env = Global.env() and sigma = Evd.empty in + let env = Global.env() in + let sigma = Evd.from_env env in let poly = Flags.is_universe_polymorphism () in let f ce = let c, ctx = Constrintern.interp_constr env sigma ce in @@ -490,7 +491,9 @@ let inTransitivity : bool * constr -> obj = (* Main entry points *) let add_transitivity_lemma left lem = - let lem',ctx (*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty lem in + let env = Global.env () in + let sigma = Evd.from_env env in + let lem',ctx (*FIXME*) = Constrintern.interp_constr env sigma lem in add_anonymous_leaf (inTransitivity (left,lem')) (* Vernacular syntax *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 0df1a35c6..48b450532 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1135,7 +1135,8 @@ let add_hints local dbnames0 h = if String.List.mem "nocore" dbnames0 then error "The hint database \"nocore\" is meant to stay empty."; let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in - let env = Global.env() and sigma = Evd.empty in + let env = Global.env() in + let sigma = Evd.from_env env in match h with | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index c64a1226a..937ad2b9d 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1797,11 +1797,13 @@ let proper_projection r ty = it_mkLambda_or_LetIn app ctx let declare_projection n instance_id r = - let c,uctx = Universes.fresh_global_instance (Global.env()) r in let poly = Global.is_polymorphic r in - let ty = Retyping.get_type_of (Global.env ()) Evd.empty c in + let env = Global.env () in + let sigma = Evd.from_env env in + let evd,c = Evd.fresh_global env sigma r in + let ty = Retyping.get_type_of env sigma c in let term = proper_projection c ty in - let typ = Typing.unsafe_type_of (Global.env ()) Evd.empty term in + let typ = Typing.unsafe_type_of env sigma term in let ctx, typ = decompose_prod_assum typ in let typ = let n = @@ -1824,15 +1826,16 @@ let declare_projection n instance_id r = in let typ = it_mkProd_or_LetIn typ ctx in let cst = - Declare.definition_entry ~types:typ ~poly ~univs:(Univ.ContextSet.to_context uctx) - term + Declare.definition_entry ~types:typ ~poly + ~univs:(Evd.universe_context sigma) term in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) let build_morphism_signature m = let env = Global.env () in - let m,ctx = Constrintern.interp_constr env (Evd.from_env env) m in + let sigma = Evd.from_env env in + let m,ctx = Constrintern.interp_constr env sigma m in let sigma = Evd.from_ctx ctx in let t = Typing.unsafe_type_of env sigma m in let cstrs = @@ -1844,7 +1847,7 @@ let build_morphism_signature m = in aux t in let evars, t', sig_, cstrs = - PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t cstrs None in + PropGlobal.build_signature (sigma, Evar.Set.empty) env t cstrs None in let evd = ref evars in let _ = List.iter (fun (ty, rel) -> @@ -1861,9 +1864,10 @@ let build_morphism_signature m = let default_morphism sign m = let env = Global.env () in - let t = Typing.unsafe_type_of env Evd.empty m in + let sigma = Evd.from_env env in + let t = Typing.unsafe_type_of env sigma m in let evars, _, sign, cstrs = - PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign) + PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign) in let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in let evars, mor = resolve_one_typeclass env (goalevars evars) morph in @@ -1894,7 +1898,7 @@ let add_morphism_infer glob m n = let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in let instance = build_morphism_signature m in - let evd = Evd.empty (*FIXME *) in + let evd = Evd.from_env (Global.env ()) in if Lib.is_modtype () then let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 7d1cc3341..bc82e9ef4 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -593,10 +593,12 @@ module New = struct (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim isrec allnames tac predicate ind (c, t) = - Proofview.Goal.nf_enter begin fun gl -> - let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in - (** FIXME: evar leak. *) + Proofview.Goal.nf_enter + begin fun gl -> let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Proofview.Goal.nf_enter begin fun gl -> + let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in (* applying elimination_scheme just a little modified *) let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in let indmv = @@ -647,7 +649,7 @@ module New = struct Proofview.tclTHEN (Clenvtac.clenv_refine false clenv') (Proofview.tclEXTEND [] tclIDTAC branchtacs) - end + end) end let elimination_then tac c = Proofview.Goal.nf_enter begin fun gl -> diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 7fe79d948..805a29e39 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -347,7 +347,7 @@ let named_of_rel_context l = let context poly l = let env = Global.env() in - let evars = ref Evd.empty in + let evars = ref (Evd.from_env env) in let _, ((env', fullctx), impls) = interp_context_evars env evars l in let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in let fullctx = Context.map_rel_context subst fullctx in @@ -358,11 +358,13 @@ let context poly l = with e when Errors.noncritical e -> error "Anonymous variables not allowed in contexts." in - let uctx = Evd.universe_context_set !evars in + let uctx = ref (Evd.universe_context_set !evars) in let fn status (id, b, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - let uctx = Univ.ContextSet.to_context uctx in - let decl = (ParameterEntry (None,poly,(t,uctx),None), IsAssumption Logical) in + let ctx = Univ.ContextSet.to_context !uctx in + (* Declare the universe context once *) + let () = uctx := Univ.ContextSet.empty in + let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in match class_of_constr t with | Some (rels, ((tc,_), args) as _cl) -> @@ -379,8 +381,9 @@ let context poly l = let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in let nstatus = - pi3 (Command.declare_assumption false decl (t, uctx) [] impl + pi3 (Command.declare_assumption false decl (t, !uctx) [] impl Vernacexpr.NoInline (Loc.ghost, id)) in - status && nstatus + let () = uctx := Univ.ContextSet.empty in + status && nstatus in List.fold_left fn true (List.rev ctx) diff --git a/toplevel/command.ml b/toplevel/command.ml index d397eed61..b65ff73fe 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -241,11 +241,14 @@ let interp_assumption evdref env impls bl c = let ctx = Evd.universe_context_set evd in ((nf ty, ctx), impls) -let declare_assumptions idl is_coe k c imps impl_is_on nl = - let refs, status = - List.fold_left (fun (refs,status) id -> - let ref',u',status' = declare_assumption is_coe k c imps impl_is_on nl id in - (ref',u')::refs, status' && status) ([],true) idl in +let declare_assumptions idl is_coe k (c,ctx) imps impl_is_on nl = + let refs, status, _ = + List.fold_left (fun (refs,status,ctx) id -> + let ref',u',status' = + declare_assumption is_coe k (c,ctx) imps impl_is_on nl id in + (ref',u')::refs, status' && status, Univ.ContextSet.empty) + ([],true,ctx) idl + in List.rev refs, status let do_assumptions (_, poly, _ as kind) nl l = diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 3c0977784..e8682c1b5 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -623,7 +623,7 @@ let declare_obligation prg obl body ty uctx = let body = prg.prg_reduce body in let ty = Option.map prg.prg_reduce ty in match obl.obl_status with - | Evar_kinds.Expand -> { obl with obl_body = Some (TermObl body) } + | Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) } | Evar_kinds.Define opaque -> let opaque = if get_proofs_transparency () then false else opaque in let poly = pi2 prg.prg_kind in @@ -647,7 +647,7 @@ let declare_obligation prg obl body ty uctx = in if not opaque then add_hint false prg constant; definition_message obl.obl_name; - { obl with obl_body = + true, { obl with obl_body = if poly then Some (DefinedObl constant) else @@ -815,9 +815,9 @@ let obligation_hook prg obl num auto ctx' _ gr = let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in let ctx' = if not (pi2 prg.prg_kind) (* Not polymorphic *) then - (* This context is already declared globally, we cannot - instantiate the rigid variables anymore *) - Evd.abstract_undefined_variables ctx' + (* The universe context was declared globally, we continue + from the new global environment. *) + Evd.evar_universe_context (Evd.from_env (Global.env ())) else ctx' in let prg = { prg with prg_ctx = ctx' } in @@ -889,8 +889,13 @@ and solve_obligation_by_tac prg obls i tac = (pi2 !prg.prg_kind) !prg.prg_ctx in let uctx = Evd.evar_context_universe_context ctx in - prg := {!prg with prg_ctx = ctx}; - obls.(i) <- declare_obligation !prg obl t ty uctx; + let () = prg := {!prg with prg_ctx = ctx} in + let def, obl' = declare_obligation !prg obl t ty uctx in + obls.(i) <- obl'; + if def && not (pi2 !prg.prg_kind) then ( + (* Declare the term constraints with the first obligation only *) + let ctx' = Evd.evar_universe_context (Evd.from_env (Global.env ())) in + prg := {!prg with prg_ctx = ctx'}); true else false with e when Errors.noncritical e -> diff --git a/toplevel/record.ml b/toplevel/record.ml index e214f9ca7..ee80101f3 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -233,7 +233,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let (mib,mip) = Global.lookup_inductive indsp in let u = Declareops.inductive_instance mib in let paramdecls = Inductive.inductive_paramdecls (mib, u) in - let poly = mib.mind_polymorphic and ctx = Univ.instantiate_univ_context mib.mind_universes in + let poly = mib.mind_polymorphic in + let ctx = Univ.instantiate_univ_context mib.mind_universes in let indu = indsp, u in let r = mkIndU (indsp,u) in let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in @@ -293,7 +294,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_polymorphic = poly; - const_entry_universes = ctx; + const_entry_universes = + if poly then ctx else Univ.UContext.empty; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None } in @@ -397,44 +399,49 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity let impl, projs = match fields with | [(Name proj_name, _, field)] when def -> - let class_body = it_mkLambda_or_LetIn field params in - let _class_type = it_mkProd_or_LetIn arity params in - let class_entry = - Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in - let cst = Declare.declare_constant (snd id) - (DefinitionEntry class_entry, IsDefinition Definition) - in - let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in - let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in - let proj_type = - it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in - let proj_body = - it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in - let proj_entry = Declare.definition_entry ~types:proj_type ~poly ~univs:ctx proj_body in - let proj_cst = Declare.declare_constant proj_name - (DefinitionEntry proj_entry, IsDefinition Definition) - in - let cref = ConstRef cst in - Impargs.declare_manual_implicits false cref [paramimpls]; - Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; - Classes.set_typeclass_transparency (EvalConstRef cst) false false; - let sub = match List.hd coers with - | Some b -> Some ((if b then Backward else Forward), List.hd priorities) - | None -> None - in - cref, [Name proj_name, sub, Some proj_cst] + let class_body = it_mkLambda_or_LetIn field params in + let _class_type = it_mkProd_or_LetIn arity params in + let class_entry = + Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in + let cst = Declare.declare_constant (snd id) + (DefinitionEntry class_entry, IsDefinition Definition) + in + let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in + let inst_type = appvectc (mkConstU cstu) + (Termops.rel_vect 0 (List.length params)) in + let proj_type = + it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in + let proj_body = + it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in + let proj_entry = + Declare.definition_entry ~types:proj_type ~poly + ~univs:(if poly then ctx else Univ.UContext.empty) proj_body + in + let proj_cst = Declare.declare_constant proj_name + (DefinitionEntry proj_entry, IsDefinition Definition) + in + let cref = ConstRef cst in + Impargs.declare_manual_implicits false cref [paramimpls]; + Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; + Classes.set_typeclass_transparency (EvalConstRef cst) false false; + let sub = match List.hd coers with + | Some b -> Some ((if b then Backward else Forward), List.hd priorities) + | None -> None + in + cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls + let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign - in - let coers = List.map2 (fun coe pri -> - Option.map (fun b -> - if b then Backward, pri else Forward, pri) coe) + in + let coers = List.map2 (fun coe pri -> + Option.map (fun b -> + if b then Backward, pri else Forward, pri) coe) coers priorities - in - IndRef ind, (List.map3 (fun (id, _, _) b y -> (id, b, y)) - (List.rev fields) coers (Recordops.lookup_projections ind)) + in + let l = List.map3 (fun (id, _, _) b y -> (id, b, y)) + (List.rev fields) coers (Recordops.lookup_projections ind) + in IndRef ind, l in let ctx_context = List.map (fun (na, b, t) -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8ae6ac2bc..2946766cb 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1185,8 +1185,9 @@ let default_env () = { let vernac_reserve bl = let sb_decl = (fun (idl,c) -> let env = Global.env() in - let t,ctx = Constrintern.interp_type env Evd.empty c in - let t = Detyping.detype false [] env Evd.empty t in + let sigma = Evd.from_env env in + let t,ctx = Constrintern.interp_type env sigma c in + let t = Detyping.detype false [] env (Evd.from_env ~ctx env) t in let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl -- cgit v1.2.3 From c92946243ccb0b11cd138f040a5297979229c3f5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 19:01:31 +0200 Subject: Univs: fix after rebase (from_ctx/from_env) --- plugins/funind/glob_term_to_relation.ml | 2 +- plugins/funind/indfun.ml | 2 +- pretyping/evd.ml | 7 ++++--- toplevel/vernacentries.ml | 2 +- 4 files changed, 7 insertions(+), 6 deletions(-) (limited to 'pretyping') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 9d3c0b4b4..1b12cd42c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1106,7 +1106,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in - let evd = Evd.from_env ~ctx env in + let evd = Evd.from_ctx ctx in let type_t' = Typing.unsafe_type_of env evd t' in let new_env = Environ.push_rel (n,Some t',type_t') env in let new_b,id_to_exclude = diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 65dc51a84..eadeebd38 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -597,7 +597,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in let ((_,_,typel),ctx,_) = Command.interp_fixpoint fixl ntns in let constr_expr_typel = - with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_env ~ctx (Global.env ())))) typel in + with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) typel in let fixpoint_exprl_with_new_bl = List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 8243f96c1..842b87c57 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1136,9 +1136,10 @@ let make_evar_universe_context e l = match l with | None -> uctx | Some us -> - List.fold_left (fun uctx (loc,id) -> - fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) uctx)) - uctx us + List.fold_left + (fun uctx (loc,id) -> + fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) true uctx)) + uctx us (****************************************) (* Operations on constants *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2946766cb..e51dfbaae 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1187,7 +1187,7 @@ let vernac_reserve bl = let env = Global.env() in let sigma = Evd.from_env env in let t,ctx = Constrintern.interp_type env sigma c in - let t = Detyping.detype false [] env (Evd.from_env ~ctx env) t in + let t = Detyping.detype false [] env (Evd.from_ctx ctx) t in let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl -- cgit v1.2.3 From b3d97c2147418f44fc704807d3812b04921591af Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 15:36:57 +0200 Subject: Univs: fix bug #4251, handling of template polymorphic constants. --- kernel/inductive.ml | 5 ++++- kernel/univ.ml | 4 ++++ kernel/univ.mli | 3 +++ pretyping/pretyping.ml | 2 +- test-suite/bugs/closed/4251.v | 17 +++++++++++++++++ 5 files changed, 29 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/4251.v (limited to 'pretyping') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 87c139f48..a02d5e205 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -165,7 +165,10 @@ let rec make_subst env = (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in - make (cons_subst u s subst) (sign, exp, args) + if Univ.Universe.is_levels s then + make (cons_subst u s subst) (sign, exp, args) + else (* Cannot handle substitution by i+n universes. *) + make subst (sign, exp, args) | (na,None,t)::sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 782778d09..73d323426 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -553,6 +553,10 @@ struct | Cons (l, _, Nil) -> Expr.is_level l | _ -> false + let rec is_levels l = match l with + | Cons (l, _, r) -> Expr.is_level l && is_levels r + | Nil -> true + let level l = match l with | Cons (l, _, Nil) -> Expr.level l | _ -> None diff --git a/kernel/univ.mli b/kernel/univ.mli index ad33d597e..4cc8a2528 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -91,6 +91,9 @@ sig val is_level : t -> bool (** Test if the universe is a level or an algebraic universe. *) + val is_levels : t -> bool + (** Test if the universe is a lub of levels or contains +n's. *) + val level : t -> Level.t option (** Try to get a level out of a universe, returns [None] if it is an algebraic universe. *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index edb76e52f..f18657da8 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -645,7 +645,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match evar_kind_of_term !evdref resj.uj_val with | App (f,args) -> let f = whd_evar !evdref f in - if isInd f && is_template_polymorphic env f then + if is_template_polymorphic env f then (* Special case for inductive type applications that must be refreshed right away. *) let sigma = !evdref in diff --git a/test-suite/bugs/closed/4251.v b/test-suite/bugs/closed/4251.v new file mode 100644 index 000000000..66343d667 --- /dev/null +++ b/test-suite/bugs/closed/4251.v @@ -0,0 +1,17 @@ + +Inductive array : Type -> Type := +| carray : forall A, array A. + +Inductive Mtac : Type -> Prop := +| bind : forall {A B}, Mtac A -> (A -> Mtac B) -> Mtac B +| array_make : forall {A}, A -> Mtac (array A). + +Definition Ref := array. + +Definition ref : forall {A}, A -> Mtac (Ref A) := + fun A x=> array_make x. +Check array Type. +Check fun A : Type => Ref A. + +Definition abs_val (a : Type) := + bind (ref a) (fun r : array Type => array_make tt). \ No newline at end of file -- cgit v1.2.3