From 265be83a546b0bec6d01f6650f7489442293cb0e Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 23 May 2016 18:02:08 +0200 Subject: Hints/Univs: fix bug #4628 anomalies Fix handling of non-polymorphic hints built from polymorphic values, or simply producing new universes. We have to record the side effects of global hints built from constrs which are not polymorphic when they declare global universes, which might need to be discharged at the end of sections too. Also issue a warning when a Hint is declared for a polymorphic reference but the Hint isn't polymorphic itself (this used to produce an anomaly). For [using] hints, treat all lemmas as polymorphic, refreshing their universes at each use, as is done for their existentials (also used to produce an anomaly). --- tactics/hints.ml | 63 ++++++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 48 insertions(+), 15 deletions(-) (limited to 'tactics') diff --git a/tactics/hints.ml b/tactics/hints.ml index 42e5067c9d..1da464e6f4 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -726,10 +726,43 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, c is a constr cty is the type of constr *) +let pr_hint_term env sigma ctx = function + | IsGlobRef gr -> pr_global gr + | IsConstr (c, ctx) -> + let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in + pr_constr_env env sigma c + +(** We need an object to record the side-effect of registering + global universes associated with a hint. *) +let cache_context_set (_,c) = + Global.push_context_set false c + +let input_context_set : Univ.ContextSet.t -> Libobject.obj = + let open Libobject in + declare_object + { (default_object "Global universe context") with + cache_function = cache_context_set; + load_function = (fun _ -> cache_context_set); + discharge_function = (fun (_,a) -> Some a); + classify_function = (fun a -> Keep a) } + let fresh_global_or_constr env sigma poly cr = - match cr with - | IsGlobRef gr -> Universes.fresh_global_instance env gr - | IsConstr (c, ctx) -> (c, ctx) + let isgr, (c, ctx) = + match cr with + | IsGlobRef gr -> + true, Universes.fresh_global_instance env gr + | IsConstr (c, ctx) -> false, (c, ctx) + in + if poly then (c, ctx) + else if Univ.ContextSet.is_empty ctx then (c, ctx) + else begin + if isgr then + msg_warning (str"Using polymorphic hint " ++ + pr_hint_term env sigma ctx cr ++ str" monomorphically" ++ + str" use Polymorphic Hint to use it polymorphically."); + Lib.add_anonymous_leaf (input_context_set ctx); + (c, Univ.ContextSet.empty) + end let make_resolves env sigma flags pri poly ?name cr = let c, ctx = fresh_global_or_constr env sigma poly cr in @@ -1094,7 +1127,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in if poly then IsConstr (c', diff) else if local then IsConstr (c', diff) - else (Global.push_context_set false diff; + else (Lib.add_anonymous_leaf (input_context_set diff); IsConstr (c', Univ.ContextSet.empty)) let interp_hints poly = @@ -1169,18 +1202,24 @@ let expand_constructor_hints env sigma lems = match kind_of_term lem with | Ind (ind,u) -> List.init (nconstructors ind) - (fun i -> IsConstr (mkConstructU ((ind,i+1),u), - Univ.ContextSet.empty)) + (fun i -> + let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd) + (Evd.universe_context_set sigma) in + not (Univ.ContextSet.is_empty ctx), + IsConstr (mkConstructU ((ind,i+1),u),ctx)) | _ -> - [prepare_hint false (false,true) env sigma (evd,lem)]) lems - + [match prepare_hint false (false,true) env sigma (evd,lem) with + | IsConstr (c, ctx) -> + not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx) + | IsGlobRef _ -> assert false (* Impossible return value *) ]) lems (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types *) let add_hint_lemmas env sigma eapply lems hint_db = let lems = expand_constructor_hints env sigma lems in let hintlist' = - List.map_append (make_resolves env sigma (eapply,true,false) None false) lems in + List.map_append (fun (poly, lem) -> + make_resolves env sigma (eapply,true,false) None poly lem) lems in Hint_db.add_list env sigma hintlist' hint_db let make_local_hint_db env sigma ts eapply lems = @@ -1193,12 +1232,6 @@ let make_local_hint_db env sigma ts eapply lems = add_hint_lemmas env sigma eapply lems (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false)) -let make_local_hint_db = - if Flags.profile then - let key = Profile.declare_profile "make_local_hint_db" in - Profile.profile4 key make_local_hint_db - else make_local_hint_db - let make_local_hint_db env sigma ?ts eapply lems = make_local_hint_db env sigma ts eapply lems -- cgit v1.2.3 From 9de5a59aa6994e8023b9e551b232a73aab3521fa Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 May 2016 11:32:51 +0200 Subject: rewrite/Univs: Fix bug # 4498. --- tactics/rewrite.ml | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) (limited to 'tactics') diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 9d70c177b4..c7cfc4dc72 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1799,10 +1799,10 @@ let declare_projection n instance_id r = let poly = Global.is_polymorphic r in let env = Global.env () in let sigma = Evd.from_env env in - let evd,c = Evd.fresh_global env sigma r in + let sigma,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 env sigma term in + let sigma, typ = Typing.type_of env sigma term in let ctx, typ = decompose_prod_assum typ in let typ = let n = @@ -1831,9 +1831,7 @@ let declare_projection n instance_id r = 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 sigma = Evd.from_env env in +let build_morphism_signature env sigma m = 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 @@ -1858,8 +1856,10 @@ let build_morphism_signature m = in let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in let evd = solve_constraints env !evd in - let m = Evarutil.nf_evar evd morph in - Evarutil.check_evars env Evd.empty evd m; m + let evd = Evd.nf_constraints evd in + let m = Evarutil.nf_evars_universes evd morph in + Evarutil.check_evars env Evd.empty evd m; + Evd.evar_universe_context evd, m let default_morphism sign m = let env = Global.env () in @@ -1896,12 +1896,13 @@ let add_morphism_infer glob m n = init_setoid (); 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.from_env (Global.env ()) in + let env = Global.env () in + let evd = Evd.from_env env in + let uctx, instance = build_morphism_signature env evd m in if Lib.is_modtype () then let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry - (None,poly,(instance,Univ.UContext.empty),None), + (None,poly,(instance,Evd.evar_context_universe_context uctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance @@ -1924,7 +1925,7 @@ let add_morphism_infer glob m n = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - Lemmas.start_proof instance_id kind evd instance hook; + Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) instance hook; ignore (Pfedit.by (Tacinterp.interp tac))) () let add_morphism glob binders m s n = -- cgit v1.2.3 From 35fb7ad402fee1e3e247ccf37438d3a7a5230629 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 29 May 2016 15:58:21 +0200 Subject: Fix bug #4746: Anomaly: Evar ?X10 was not declared. Some dubious evarmap manipulation is going on in destruct because of the use of clenv primitives. Here, building a clenv was introducing new evars that were not taken into account in the remainder of the tactic. We plug them back using a local workaround. Eventually, this code should be replaced by an evar-based one, but meanwhile, we rely on what is probably a hack. --- tactics/tactics.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 63d3c694ea..4562e25184 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1224,6 +1224,8 @@ let general_elim with_evars clear_flag (c, lbindc) elim = let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in let elimtac = elimination_clause_scheme with_evars in let indclause = make_clenv_binding env sigma (c, t) lbindc in + let sigma = meta_merge sigma (clear_metas indclause.evd) in + Proofview.Unsafe.tclEVARS sigma <*> Tacticals.New.tclTHEN (general_elim_clause_gen elimtac indclause elim) (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) -- cgit v1.2.3 From 27dffdea5b46f6282c1584db0555213e744352fa Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 31 May 2016 13:33:01 +0200 Subject: Revert "Rename Lexer -> CLexer." This reverts commit a66b57ba4bba866bb626bde2b6fe3b762347eb3e. --- tactics/tacinterp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a7acdf7594..5ecc46d670 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -491,7 +491,7 @@ let interp_fresh_id ist env sigma l = String.concat "" (List.map (function | ArgArg s -> s | ArgVar (_,id) -> Id.to_string (interp_ident ist env sigma id)) l) in - let s = if CLexer.is_keyword s then s^"0" else s in + let s = if Lexer.is_keyword s then s^"0" else s in Id.of_string s in Tactics.fresh_id_in_env avoid id env -- cgit v1.2.3