diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-04 14:45:54 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-04 14:45:54 +0000 |
commit | bb7e5aa54afa577da7661fb43cefc9711ccfe4af (patch) | |
tree | 3cda768748016bf44a47f79c1e35db1a4193c20d | |
parent | eb52433fbf064ae7c6f76178fb142a5e7b9e2dd1 (diff) |
Forward-port fixes from 8.4 (15358, 15353, 15333).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15418 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | interp/constrintern.ml | 2 | ||||
-rw-r--r-- | pretyping/coercion.ml | 2 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 10 | ||||
-rw-r--r-- | pretyping/typeclasses.ml | 13 | ||||
-rw-r--r-- | pretyping/typeclasses.mli | 10 | ||||
-rw-r--r-- | pretyping/unification.ml | 2 | ||||
-rw-r--r-- | proofs/clenvtac.ml | 2 | ||||
-rw-r--r-- | proofs/goal.ml | 4 | ||||
-rw-r--r-- | proofs/goal.mli | 2 | ||||
-rw-r--r-- | tactics/auto.ml | 21 | ||||
-rw-r--r-- | tactics/class_tactics.ml4 | 22 | ||||
-rw-r--r-- | tactics/refine.ml | 2 | ||||
-rw-r--r-- | toplevel/classes.ml | 6 | ||||
-rw-r--r-- | toplevel/command.ml | 7 |
14 files changed, 65 insertions, 40 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 5a8dcac08..304712675 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1854,7 +1854,7 @@ let interp_rawcontext_gen understand_type understand_judgment env bl = (push_rel d env, d::params, succ n, impls) | Some b -> let c = understand_judgment env b in - let d = (na, Some c.uj_val, c.uj_type) in + let d = (na, Some c.uj_val, Termops.refresh_universes c.uj_type) in (push_rel d env, d::params, succ n, impls)) (env,[],1,[]) (List.rev bl) in (env, par), impls diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 34eb92fa0..524d9d058 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -323,7 +323,7 @@ let coerce_itf loc env isevars v t c1 = let saturate_evd env evd = Typeclasses.resolve_typeclasses - ~with_goals:false ~split:true ~fail:false env evd + ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd (* appliquer le chemin de coercions p à hj *) let apply_coercion env sigma p hj typ_cl = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4eeb50cd0..bcd2a1ad1 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -109,8 +109,14 @@ let interp_elimination_sort = function let resolve_evars env evdref fail_evar resolve_classes = if resolve_classes then - (evdref := Typeclasses.resolve_typeclasses ~with_goals:false - ~split:true ~fail:fail_evar env !evdref); + (evdref := Typeclasses.resolve_typeclasses + ~filter:(if Flags.is_program_mode () + then Typeclasses.no_goals_or_obligations else Typeclasses.no_goals) + ~split:true ~fail:fail_evar env !evdref; + if Flags.is_program_mode () then (* Try optionally solving the obligations *) + evdref := Typeclasses.resolve_typeclasses + ~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref; + ); (* Resolve eagerly, potentially making wrong choices *) evdref := (try consider_remaining_unif_problems ~ts:(Typeclasses.classes_transparent_state ()) env !evdref diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d76fdc85d..db03112c2 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -500,6 +500,15 @@ let has_typeclasses evd = let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false) -let resolve_typeclasses ?(with_goals=false) ?(split=true) ?(fail=true) env evd = +open Evar_kinds +type evar_filter = Evar_kinds.t -> bool + +let all_evars _ = true +let no_goals = function GoalEvar -> false | _ -> true +let no_goals_or_obligations = function + | GoalEvar | QuestionMark _ -> false + | _ -> true + +let resolve_typeclasses ?(filter=no_goals) ?(split=true) ?(fail=true) env evd = if not (has_typeclasses evd) then evd - else !solve_instanciations_problem env evd with_goals split fail + else !solve_instanciations_problem env evd filter split fail diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 411651afe..b51732547 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -87,7 +87,13 @@ val mark_resolvable : evar_info -> evar_info val mark_resolvables : evar_map -> evar_map val is_class_evar : evar_map -> evar_info -> bool -val resolve_typeclasses : ?with_goals:bool -> ?split:bool -> ?fail:bool -> +(** Filter which evars to consider for resolution. *) +type evar_filter = Evar_kinds.t -> bool +val all_evars : evar_filter +val no_goals : evar_filter +val no_goals_or_obligations : evar_filter + +val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map val resolve_one_typeclass : env -> evar_map -> types -> open_constr @@ -102,7 +108,7 @@ val register_remove_instance_hint : (global_reference -> unit) -> unit val add_instance_hint : constr -> bool -> int option -> unit val remove_instance_hint : global_reference -> unit -val solve_instanciations_problem : (env -> evar_map -> bool -> bool -> bool -> evar_map) ref +val solve_instanciations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref val declare_instance : int option -> bool -> global_reference -> unit diff --git a/pretyping/unification.ml b/pretyping/unification.ml index fd40cca7c..eec9b0bc3 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -967,7 +967,7 @@ let check_types env flags (sigma,_,_ as subst) m n = let try_resolve_typeclasses env evd flags m n = if flags.resolve_evars then - try Typeclasses.resolve_typeclasses ~with_goals:false ~split:false + try Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:false ~fail:true env evd with e when Typeclasses_errors.unsatisfiable_exception e -> error_cannot_unify env evd (m, n) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 3eb665088..3def44178 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -72,7 +72,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls = let clenv = clenv_pose_dependent_evars with_evars clenv in let evd' = if with_classes then - Typeclasses.resolve_typeclasses ~with_goals:true + Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:(not with_evars) clenv.env clenv.evd else clenv.evd in diff --git a/proofs/goal.ml b/proofs/goal.ml index cef43c443..9b3e90198 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -162,8 +162,8 @@ module Refinable = struct (* spiwack: it is not very fine grain since it solves all typeclasses holes, not only those containing the current goal, or a given term. But it seems to fit our needs so far. *) - let resolve_typeclasses ?with_goals ?split ?(fail=false) () env rdefs _ _ = - rdefs:=Typeclasses.resolve_typeclasses ?with_goals ?split ~fail env !rdefs; + let resolve_typeclasses ?filter ?split ?(fail=false) () env rdefs _ _ = + rdefs:=Typeclasses.resolve_typeclasses ?filter ?split ~fail env !rdefs; () diff --git a/proofs/goal.mli b/proofs/goal.mli index acda9031b..622ceea74 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -72,7 +72,7 @@ module Refinable : sig (* [with_type c typ] constrains term [c] to have type [typ]. *) val with_type : Term.constr -> Term.types -> Term.constr sensitive - val resolve_typeclasses : ?with_goals:bool -> ?split:bool -> ?fail:bool -> unit -> unit sensitive + val resolve_typeclasses : ?filter:Typeclasses.evar_filter -> ?split:bool -> ?fail:bool -> unit -> unit sensitive (* [constr_of_raw h check_type resolve_classes] is a pretyping function. diff --git a/tactics/auto.ml b/tactics/auto.ml index 96cef72b4..0486eec58 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -281,13 +281,19 @@ let rec pp_hints_path = function | PathEmpty -> str"Ø" | PathEpsilon -> str"ε" -let rec subst_hints_path subst hp = - match hp with - | PathAtom PathAny -> hp - | PathAtom (PathHints grs) -> +let subst_path_atom subst p = + match p with + | PathAny -> p + | PathHints grs -> let gr' gr = fst (subst_global subst gr) in let grs' = list_smartmap gr' grs in - if grs' == grs then hp else PathAtom (PathHints grs') + if grs' == grs then p else PathHints grs' + +let rec subst_hints_path subst hp = + match hp with + | PathAtom p -> + let p' = subst_path_atom subst p in + if p' == p then hp else PathAtom p' | PathStar p -> let p' = subst_hints_path subst p in if p' == p then hp else PathStar p' | PathSeq (p, q) -> @@ -681,9 +687,10 @@ let subst_autohint (subst,(local,name,hintlist as obj)) = let tac' = !forward_subst_tactic subst tac in if tac==tac' then data.code else Extern tac' in + let name' = subst_path_atom subst data.name in let data' = - if data.pat==pat' && data.code==code' then data - else { data with pat = pat'; code = code' } + if data.pat==pat' && data.name == name' && data.code==code' then data + else { data with pat = pat'; name = name'; code = code' } in if k' == k && data' == data then hint else (k',data') in diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 4553a8fa5..c8fe1a426 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -680,25 +680,21 @@ let resolve_all_evars debug m env p oevd do_split fail = docomp evd comps in docomp oevd split -let initial_select_evars with_goals = - if with_goals then - (fun evd ev evi -> - Typeclasses.is_class_evar evd evi) - else - (fun evd ev evi -> - (snd (Evd.evar_source ev evd) <> Evar_kinds.GoalEvar) - && Typeclasses.is_class_evar evd evi) - -let resolve_typeclass_evars debug m env evd with_goals split fail = +let initial_select_evars filter = + fun evd ev evi -> + filter (snd evi.Evd.evar_source) && + Typeclasses.is_class_evar evd evi + +let resolve_typeclass_evars debug m env evd filter split fail = let evd = try Evarconv.consider_remaining_unif_problems ~ts:(Typeclasses.classes_transparent_state ()) env evd with _ -> evd in - resolve_all_evars debug m env (initial_select_evars with_goals) evd split fail + resolve_all_evars debug m env (initial_select_evars filter) evd split fail -let solve_inst debug depth env evd with_goals split fail = - resolve_typeclass_evars debug depth env evd with_goals split fail +let solve_inst debug depth env evd filter split fail = + resolve_typeclass_evars debug depth env evd filter split fail let _ = Typeclasses.solve_instanciations_problem := diff --git a/tactics/refine.ml b/tactics/refine.ml index 93c4ea57c..07480fc00 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -389,7 +389,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = let refine (evd,c) gl = let sigma = project gl in - let evd = Typeclasses.resolve_typeclasses ~with_goals:false (pf_env gl) evd in + let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals (pf_env gl) evd in let c = Evarutil.nf_evar evd c in let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise diff --git a/toplevel/classes.ml b/toplevel/classes.ml index b4e44e7d3..dfbc95356 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -172,7 +172,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props in let env' = push_rel_context ctx env in evars := Evarutil.nf_evar_map !evars; - evars := resolve_typeclasses ~with_goals:false ~fail:true env !evars; + evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env !evars; let sigma = !evars in let subst = List.map (Evarutil.nf_evar sigma) subst in if abstract then @@ -262,10 +262,10 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props in let _ = evars := Evarutil.nf_evar_map !evars; - evars := Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true + evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env !evars; (* Try resolving fields that are typeclasses automatically. *) - evars := Typeclasses.resolve_typeclasses ~with_goals:true ~fail:false + evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env !evars in let termtype = Evarutil.nf_evar !evars termtype in diff --git a/toplevel/command.ml b/toplevel/command.ml index 2f5ed1181..3191279ce 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -290,7 +290,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = (* Instantiate evars and check all are resolved *) let evd = consider_remaining_unif_problems env_params !evdref in - let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env_params evd in + let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env_params evd in let sigma = evd in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in @@ -781,7 +781,7 @@ let interp_recursive isfix fixl notations = (env,rec_sign,evd), (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots let check_recursive isfix ((env,rec_sign,evd),(fixnames,fixdefs,fixtypes),info) = - let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env evd in + let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in List.iter (Option.iter (check_evars (push_named_context rec_sign env) Evd.empty evd)) fixdefs; List.iter (check_evars env Evd.empty evd) fixtypes; if not (List.mem None fixdefs) then begin @@ -889,7 +889,8 @@ let do_program_recursive fixkind fixl ntns = in (* Program-specific code *) (* Get the interesting evars, those that were not instanciated *) - let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env evd in + let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env evd in + let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:false env evd in (* Solve remaining evars *) let rec collect_evars id def typ imps = (* Generalize by the recursive prototypes *) |