diff options
27 files changed, 523 insertions, 205 deletions
diff --git a/dev/include b/dev/include index 13245eb5df..39d90286e0 100644 --- a/dev/include +++ b/dev/include @@ -37,7 +37,10 @@ #install_printer (* judgement *) ppj;; #install_printer (* hint_db *) print_hint_db;; -#install_printer (* Goal.goal *) ppgoal;; +#install_printer (* hints_path *) pphintspath;; +#install_printer (* goal *) ppgoal;; +#install_printer (* sigma goal *) ppsigmagoal;; +#install_printer (* proof *) pproof;; #install_printer (* Goal.goal *) ppgoalgoal;; #install_printer (* metaset.t *) ppmetas;; #install_printer (* evar_map *) ppevm;; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e27fcca275..07e0d5b5ab 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -332,7 +332,8 @@ GEXTEND Gram *) (* ... with coercions *) record_field: - [ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ] + [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ]; + ntn = decl_notation -> (bd,pri),ntn ] ] ; record_binder_body: [ [ l = binders; oc = of_type_with_opt_coercion; diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 849f67fe68..5435a98720 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -429,7 +429,7 @@ let pr_constrarg c = spc () ++ pr_constr c in let pr_lconstrarg c = spc () ++ pr_lconstr c in let pr_intarg n = spc () ++ int n in (* let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in *) -let pr_record_field (x, ntn) = +let pr_record_field ((x, pri), ntn) = let prx = match x with | (oc,AssumExpr (id,t)) -> hov 1 (pr_lname id ++ @@ -443,7 +443,8 @@ let pr_record_field (x, ntn) = | None -> hov 1 (pr_lname id ++ str" :=" ++ spc() ++ pr_lconstr b)) in - prx ++ prlist (pr_decl_notation pr_constr) ntn + let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in + prx ++ prpri ++ prlist (pr_decl_notation pr_constr) ntn in let pr_record_decl b c fs = pr_opt pr_lident c ++ str"{" ++ diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 571ec4ef34..f75678c60f 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -210,7 +210,7 @@ open Auto let extend_with_auto_hints l seq gl= let seqref=ref seq in - let f (_, p_a_t) = + let f p_a_t = match p_a_t.code with Res_pf (c,_) | Give_exact c | Res_pf_THEN_trivial_fail (c,_) -> diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index 000ffc6226..c08dd16df5 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -179,9 +179,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p Evarutil.check_evars env Evd.empty !evars termtype; let hook vis gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in - let inst = Typeclasses.new_instance k pri global (ConstRef cst) in Impargs.declare_manual_implicits false gr ~enriching:false [imps]; - Typeclasses.add_instance inst + Typeclasses.declare_instance pri (not global) (ConstRef cst) in let evm = Subtac_utils.evars_of_term !evars Evd.empty term in let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index d300a71ccc..d5d427c7a6 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -599,8 +599,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (pretype_type empty_valcon env evdref lvar c).utj_val in if resolve_classes then - evdref := Typeclasses.resolve_typeclasses ~onlyargs:false - ~split:true ~fail:fail_evar env !evdref; + (try + evdref := Typeclasses.resolve_typeclasses ~onlyargs:true + ~split:true ~fail:true env !evdref; + evdref := Typeclasses.resolve_typeclasses ~onlyargs:false + ~split:true ~fail:false env !evdref + with e -> if fail_evar then raise e else ()); evdref := consider_remaining_unif_problems env !evdref; let c = if expand_evar then nf_evar !evdref c' else c' in if fail_evar then check_evars env Evd.empty !evdref c; diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 89e0fc93d7..128d3a6a71 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -41,6 +41,11 @@ let classes_transparent_state_ref = ref (fun () -> assert false) let register_classes_transparent_state = (:=) classes_transparent_state_ref let classes_transparent_state () = !classes_transparent_state_ref () +let solve_instanciation_problem = ref (fun _ _ _ -> assert false) + +let resolve_one_typeclass env evm t = + !solve_instanciation_problem env evm t + type rels = constr list (* This module defines type-classes *) @@ -55,8 +60,9 @@ type typeclass = { cl_props : rel_context; (* The method implementaions as projections. *) - cl_projs : (name * bool * constant option) list; + cl_projs : (name * int option option * constant option) list; } + module Gmap = Fmap.Make(RefOrdered) type typeclasses = typeclass Gmap.t @@ -68,7 +74,7 @@ type instance = { -1 for discard, 0 for none, mutable to avoid redeclarations when multiple rebuild_object happen. *) is_global: int; - is_impl: global_reference; + is_impl: global_reference; } type instances = (instance Gmap.t) Gmap.t @@ -224,6 +230,45 @@ let class_input : typeclass -> obj = let add_class cl = Lib.add_anonymous_leaf (class_input cl) +(** Build the subinstances hints. *) + +let check_instance env sigma c = + try + let (evd, c) = resolve_one_typeclass env sigma + (Retyping.get_type_of env sigma c) in + Evd.is_empty (Evd.undefined_evars evd) + with _ -> false + +let build_subclasses ~check env sigma glob pri = + let rec aux pri c = + let ty = Retyping.get_type_of env sigma c in + match class_of_constr ty with + | None -> [] + | Some (rels, (tc, args)) -> + let instapp = Reductionops.whd_beta sigma (appvectc c (Termops.extended_rel_vect 0 rels)) in + let projargs = Array.of_list (args @ [instapp]) in + let projs = list_map_filter + (fun (n, b, proj) -> + match b with + | None -> None + | Some pri' -> + let proj = Option.get proj in + let body = it_mkLambda_or_LetIn (mkApp (mkConst proj, projargs)) rels in + if check && check_instance env sigma body then None + else + let pri = + match pri, pri' with + | Some p, Some p' -> Some (p + p') + | Some p, None -> Some (p + 1) + | _, _ -> None + in + Some (ConstRef proj, pri, body)) tc.cl_projs + in + let declare_proj hints (cref, pri, body) = + let rest = aux pri body in + hints @ (pri, body) :: rest + in List.fold_left declare_proj [] projs + in aux pri (constr_of_global glob) (* * instances persistent object @@ -268,9 +313,14 @@ let discharge_instance (_, (action, inst)) = let is_local i = i.is_global = -1 +let add_instance check inst = + add_instance_hint (constr_of_global inst.is_impl) (is_local inst) inst.is_pri; + List.iter (fun (pri, c) -> add_instance_hint c (is_local inst) pri) + (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) + (Global.env ()) Evd.empty inst.is_impl inst.is_pri) + let rebuild_instance (action, inst) = - if action = AddInstance then - add_instance_hint inst.is_impl (is_local inst) inst.is_pri; + if action = AddInstance then add_instance true inst; (action, inst) let classify_instance (action, inst) = @@ -280,7 +330,7 @@ let classify_instance (action, inst) = let load_instance (_, (action, inst) as ai) = cache_instance ai; if action = AddInstance then - add_instance_hint inst.is_impl (is_local inst) inst.is_pri + add_instance_hint (constr_of_global inst.is_impl) (is_local inst) inst.is_pri let instance_input : instance_action * instance -> obj = declare_object @@ -295,12 +345,25 @@ let instance_input : instance_action * instance -> obj = let add_instance i = Lib.add_anonymous_leaf (instance_input (AddInstance, i)); - add_instance_hint i.is_impl (is_local i) i.is_pri + add_instance true i let remove_instance i = Lib.add_anonymous_leaf (instance_input (RemoveInstance, i)); remove_instance_hint i.is_impl +let declare_instance pri local glob = + let c = constr_of_global glob in + let ty = Retyping.get_type_of (Global.env ()) Evd.empty c in + match class_of_constr ty with + | Some (rels, (tc, args) as _cl) -> + add_instance (new_instance tc pri (not local) glob) +(* let path, hints = build_subclasses (not local) (Global.env ()) Evd.empty glob in *) +(* let entries = List.map (fun (path, pri, c) -> (pri, local, path, c)) hints in *) +(* Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry entries); *) +(* Auto.add_hints local [typeclasses_db] *) +(* (Auto.HintsCutEntry (PathSeq (PathStar (PathAtom PathAny), path))) *) + | None -> () + open Declarations let add_constant_class cst = @@ -381,6 +444,7 @@ let is_implicit_arg k = | InternalHole -> true | _ -> false + (* To embed a boolean for resolvability status. This is essentially a hack to mark which evars correspond to goals and do not need to be resolved when we have nested [resolve_all_evars] @@ -416,11 +480,7 @@ let has_typeclasses evd = evd false let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false) -let solve_instanciation_problem = ref (fun _ _ _ -> assert false) let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd = if not (has_typeclasses evd) then evd else !solve_instanciations_problem env evd onlyargs split fail - -let resolve_one_typeclass env evm t = - !solve_instanciation_problem env evm t diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index e4db68fbcd..a00d23a9b2 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -34,8 +34,9 @@ type typeclass = { (** The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if - no name is provided. The boolean indicates subclasses. *) - cl_projs : (name * bool * constant option) list; + no name is provided. The [int option option] indicates subclasses whose hint has + the given priority. *) + cl_projs : (name * int option option * constant option) list; } type instance @@ -93,10 +94,20 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u val register_classes_transparent_state : (unit -> transparent_state) -> unit val classes_transparent_state : unit -> transparent_state -val register_add_instance_hint : (global_reference -> bool (* local? *) -> int option -> unit) -> unit +val register_add_instance_hint : (constr -> bool (* local? *) -> int option -> unit) -> unit val register_remove_instance_hint : (global_reference -> unit) -> unit -val add_instance_hint : global_reference -> bool -> int option -> 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_instanciation_problem : (env -> evar_map -> types -> open_constr) ref + +val declare_instance : int option -> bool -> global_reference -> unit + + +(** Build the subinstances hints for a given typeclass object. + check tells if we should check for existence of the + subinstances and add only the missing ones. *) + +val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) -> + (int option * constr) list diff --git a/tactics/auto.ml b/tactics/auto.ml index db2524c30f..e15c30a3b5 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -54,10 +54,22 @@ type 'a auto_tactic = | Unfold_nth of evaluable_global_reference (* Hint Unfold *) | Extern of glob_tactic_expr (* Hint Extern *) +type hints_path_atom = + | PathHints of global_reference list + | PathAny + +type hints_path = + | PathAtom of hints_path_atom + | PathStar of hints_path + | PathSeq of hints_path * hints_path + | PathOr of hints_path * hints_path + | PathEmpty + | PathEpsilon + type 'a gen_auto_tactic = { pri : int; (* A number lower is higher priority *) pat : constr_pattern option; (* A pattern for the concl of the Goal *) - name : global_reference option; (* A potential name to refer to the hint *) + name : hints_path_atom; (* A potential name to refer to the hint *) code : 'a auto_tactic (* the tactic to apply when the concl matches pat *) } @@ -80,18 +92,18 @@ let insert v l = insrec l (* Nov 98 -- Papageno *) -(* Les Hints sont ré-organisés en plusieurs databases. +(* Les Hints sont ré-organisés en plusieurs databases. - La table impérative "searchtable", de type "hint_db_table", - associe une database (hint_db) à chaque nom. + La table impérative "searchtable", de type "hint_db_table", + associe une database (hint_db) à chaque nom. Une hint_db est une table d'association fonctionelle constr -> search_entry - Le constr correspond à la constante de tête de la conclusion. + Le constr correspond à la constante de tête de la conclusion. Une search_entry est un triplet comprenant : - - la liste des tactiques qui n'ont pas de pattern associé + - la liste des tactiques qui n'ont pas de pattern associé - la liste des tactiques qui ont un pattern - - un discrimination net borné (Btermdn.t) constitué de tous les + - un discrimination net borné (Btermdn.t) constitué de tous les patterns de la seconde liste de tactiques *) type stored_data = int * pri_auto_tactic @@ -137,7 +149,9 @@ let eq_pri_auto_tactic (_, x) (_, y) = let add_tac pat t st (l,l',dn) = match pat with | None -> if not (List.exists (eq_pri_auto_tactic t) l) then (insert t l, l', dn) else (l, l', dn) - | Some pat -> if not (List.exists (eq_pri_auto_tactic t) l') then (l, insert t l', Bounded_net.add st dn (pat,t)) else (l, l', dn) + | Some pat -> + if not (List.exists (eq_pri_auto_tactic t) l') + then (l, insert t l', Bounded_net.add st dn (pat,t)) else (l, l', dn) let rebuild_dn st ((l,l',dn) : search_entry) = (l, l', List.fold_left (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t))) @@ -173,10 +187,119 @@ let translate_hint (go,p) = in (go,{ p with code = code }) +let path_matches hp hints = + let rec aux hp hints k = + match hp, hints with + | PathAtom _, [] -> false + | PathAtom PathAny, (_ :: hints') -> k hints' + | PathAtom p, (h :: hints') -> + if p = h then k hints' else false + | PathStar hp', hints -> + k hints || aux hp' hints (fun hints' -> aux hp hints' k) + | PathSeq (hp, hp'), hints -> + aux hp hints (fun hints' -> aux hp' hints' k) + | PathOr (hp, hp'), hints -> + aux hp hints k || aux hp' hints k + | PathEmpty, _ -> false + | PathEpsilon, hints -> k hints + in aux hp hints (fun hints' -> true) + +let rec matches_epsilon = function + | PathAtom _ -> false + | PathStar _ -> true + | PathSeq (p, p') -> matches_epsilon p && matches_epsilon p' + | PathOr (p, p') -> matches_epsilon p || matches_epsilon p' + | PathEmpty -> false + | PathEpsilon -> true + +let rec is_empty = function + | PathAtom _ -> false + | PathStar _ -> false + | PathSeq (p, p') -> is_empty p || is_empty p' + | PathOr (p, p') -> matches_epsilon p && matches_epsilon p' + | PathEmpty -> true + | PathEpsilon -> false + +let rec path_derivate hp hint = + let rec derivate_atoms hints hints' = + match hints, hints' with + | gr :: grs, gr' :: grs' when gr = gr' -> derivate_atoms grs grs' + | [], [] -> PathEpsilon + | [], hints -> PathEmpty + | grs, [] -> PathAtom (PathHints grs) + | _, _ -> PathEmpty + in + match hp with + | PathAtom PathAny -> PathEpsilon + | PathAtom (PathHints grs) -> + (match grs, hint with + | h :: hints, PathAny -> PathEmpty + | hints, PathHints hints' -> derivate_atoms hints hints' + | _, _ -> assert false) + | PathStar p -> if path_matches p [hint] then hp else PathEpsilon + | PathSeq (hp, hp') -> + let hpder = path_derivate hp hint in + if matches_epsilon hp then + PathOr (PathSeq (hpder, hp'), path_derivate hp' hint) + else if is_empty hpder then PathEmpty + else PathSeq (hpder, hp') + | PathOr (hp, hp') -> + PathOr (path_derivate hp hint, path_derivate hp' hint) + | PathEmpty -> PathEmpty + | PathEpsilon -> PathEmpty + +let rec normalize_path h = + match h with + | PathStar PathEpsilon -> PathEpsilon + | PathSeq (PathEmpty, _) | PathSeq (_, PathEmpty) -> PathEmpty + | PathSeq (PathEpsilon, p) | PathSeq (p, PathEpsilon) -> normalize_path p + | PathOr (PathEmpty, p) | PathOr (p, PathEmpty) -> normalize_path p + | PathOr (p, q) -> + let p', q' = normalize_path p, normalize_path q in + if p = p' && q = q' then h + else normalize_path (PathOr (p', q')) + | PathSeq (p, q) -> + let p', q' = normalize_path p, normalize_path q in + if p = p' && q = q' then h + else normalize_path (PathSeq (p', q')) + | _ -> h + +let path_derivate hp hint = normalize_path (path_derivate hp hint) + +let rec pp_hints_path = function + | PathAtom (PathAny) -> str"." + | PathAtom (PathHints grs) -> prlist_with_sep pr_spc pr_global grs + | PathStar p -> str "(" ++ pp_hints_path p ++ str")*" + | PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p' + | PathOr (p, p') -> + str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ spc () ++ pp_hints_path p' ++ str ")" + | PathEmpty -> str"Ø" + | PathEpsilon -> str"ε" + +let rec subst_hints_path subst hp = + match hp with + | PathAtom PathAny -> hp + | PathAtom (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') + | PathStar p -> let p' = subst_hints_path subst p in + if p' == p then hp else PathStar p' + | PathSeq (p, q) -> + let p' = subst_hints_path subst p in + let q' = subst_hints_path subst q in + if p' == p && q' == q then hp else PathSeq (p', q') + | PathOr (p, q) -> + let p' = subst_hints_path subst p in + let q' = subst_hints_path subst q in + if p' == p && q' == q then hp else PathOr (p', q') + | _ -> hp + module Hint_db = struct type t = { hintdb_state : Names.transparent_state; + hintdb_cut : hints_path; hintdb_unfolds : Idset.t * Cset.t; mutable hintdb_max_id : int; use_dn : bool; @@ -190,6 +313,7 @@ module Hint_db = struct let h = t.hintdb_max_id in t.hintdb_max_id <- succ t.hintdb_max_id; h let empty st use_dn = { hintdb_state = st; + hintdb_cut = PathEmpty; hintdb_unfolds = (Idset.empty, Cset.empty); hintdb_max_id = 0; use_dn = use_dn; @@ -199,7 +323,7 @@ module Hint_db = struct let find key db = try Constr_map.find key db.hintdb_map with Not_found -> empty_se - + let map_none db = List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat) []) @@ -271,7 +395,7 @@ module Hint_db = struct else rebuild_dn st (sl1', sl2', dn) let remove_list grs db = - let filter (_, h) = match h.name with None -> true | Some gr -> not (List.mem gr grs) in + let filter (_, h) = match h.name with PathHints [gr] -> not (List.mem gr grs) | _ -> true in let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in let hintnopat = list_smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in { db with hintdb_map = hintmap; hintdb_nopat = hintnopat } @@ -279,8 +403,8 @@ module Hint_db = struct let remove_one gr db = remove_list [gr] db let iter f db = - f None (List.map snd db.hintdb_nopat); - Constr_map.iter (fun k (l,l',_) -> f (Some k) (l@l')) db.hintdb_map + f None (List.map (fun x -> snd (snd x)) db.hintdb_nopat); + Constr_map.iter (fun k (l,l',_) -> f (Some k) (List.map snd (l@l'))) db.hintdb_map let transparent_state db = db.hintdb_state @@ -288,6 +412,11 @@ module Hint_db = struct if db.use_dn then rebuild_db st db else { db with hintdb_state = st } + let add_cut path db = + { db with hintdb_cut = normalize_path (PathOr (db.hintdb_cut, path)) } + + let cut db = db.hintdb_cut + let unfolds db = db.hintdb_unfolds let use_dn db = db.use_dn @@ -348,7 +477,7 @@ let try_head_pattern c = let name_of_constr c = try Some (global_of_constr c) with Not_found -> None -let make_exact_entry sigma pri ?name (c,cty) = +let make_exact_entry sigma pri ?(name=PathAny) (c,cty) = let cty = strip_outer_cast cty in match kind_of_term cty with | Prod _ -> failwith "make_exact_entry" @@ -364,7 +493,7 @@ let make_exact_entry sigma pri ?name (c,cty) = name = name; code = Give_exact c }) -let make_apply_entry env sigma (eapply,hnf,verbose) pri ?name (c,cty) = +let make_apply_entry env sigma (eapply,hnf,verbose) pri ?(name=PathAny) (c,cty) = let cty = if hnf then hnf_constr env sigma cty else cty in match kind_of_term cty with | Prod _ -> @@ -415,7 +544,8 @@ let make_resolves env sigma flags pri ?name c = (* used to add an hypothesis to the local hint database *) let make_resolve_hyp env sigma (hname,_,htyp) = try - [make_apply_entry env sigma (true, true, false) None ~name:(VarRef hname) + [make_apply_entry env sigma (true, true, false) None + ~name:(PathHints [VarRef hname]) (mkVar hname, htyp)] with | Failure _ -> [] @@ -427,7 +557,7 @@ let make_unfold eref = (Some g, { pri = 4; pat = None; - name = Some g; + name = PathHints [g]; code = Unfold_nth eref }) let make_extern pri pat tacast = @@ -435,10 +565,10 @@ let make_extern pri pat tacast = (hdconstr, { pri = pri; pat = pat; - name = None; + name = PathAny; code = Extern tacast }) -let make_trivial env sigma ?name c = +let make_trivial env sigma ?(name=PathAny) c = let t = hnf_constr env sigma (type_of env sigma c) in let hd = head_of_constr_reference (fst (head_constr t)) in let ce = mk_clenv_from dummy_goal (c,t) in @@ -476,7 +606,7 @@ let add_transparency dbname grs b = st grs in searchtable_add (dbname, Hint_db.set_transparent_state db st') -let remove_hints dbname hintlist grs = +let remove_hint dbname grs = let db = get_db dbname in let db' = Hint_db.remove_list grs db in searchtable_add (dbname, db') @@ -486,6 +616,12 @@ type hint_action = | AddTransparency of evaluable_global_reference list * bool | AddHints of hint_entry list | RemoveHints of global_reference list + | AddCut of hints_path + +let add_cut dbname path = + let db = get_db dbname in + let db' = Hint_db.add_cut path db in + searchtable_add (dbname, db') type hint_obj = bool * string * hint_action (* locality, name, action *) @@ -494,7 +630,8 @@ let cache_autohint (_,(local,name,hints)) = | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b) | AddTransparency (grs, b) -> add_transparency name grs b | AddHints hints -> add_hint name hints - | RemoveHints grs -> remove_hints name hints grs + | RemoveHints grs -> remove_hint name grs + | AddCut path -> add_cut name path let forward_subst_tactic = ref (fun _ -> failwith "subst_tactic is not installed for auto") @@ -553,7 +690,9 @@ let subst_autohint (subst,(local,name,hintlist as obj)) = | RemoveHints grs -> let grs' = list_smartmap (fun x -> fst (subst_global subst x)) grs in if grs==grs' then obj else (local, name, RemoveHints grs') - + | AddCut path -> + let path' = subst_hints_path subst path in + if path' == path then obj else (local, name, AddCut path') let classify_autohint ((local,name,hintlist) as obj) = if local or hintlist = (AddHints []) then Dispose else Substitute obj @@ -563,8 +702,7 @@ let inAutoHint : hint_obj -> obj = cache_function = cache_autohint; load_function = (fun _ -> cache_autohint); subst_function = subst_autohint; - classify_function = classify_autohint } - + classify_function = classify_autohint; } let create_hint_db l n st b = Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st))) @@ -585,17 +723,22 @@ let add_resolves env sigma clist local dbnames = Lib.add_anonymous_leaf (inAutoHint (local,dbname, AddHints - (List.flatten (List.map (fun (x, hnf, name, y) -> - make_resolves env sigma (true,hnf,Flags.is_verbose()) x ?name y) clist))))) + (List.flatten (List.map (fun (x, hnf, path, y) -> + make_resolves env sigma (true,hnf,Flags.is_verbose()) x ~name:path y) clist))))) dbnames - let add_unfolds l local dbnames = List.iter (fun dbname -> Lib.add_anonymous_leaf (inAutoHint (local,dbname, AddHints (List.map make_unfold l)))) dbnames +let add_cuts l local dbnames = + List.iter + (fun dbname -> Lib.add_anonymous_leaf + (inAutoHint (local,dbname, AddCut l))) + dbnames + let add_transparency l b local dbnames = List.iter (fun dbname -> Lib.add_anonymous_leaf @@ -626,7 +769,8 @@ let add_trivials env sigma l local dbnames = List.iter (fun dbname -> Lib.add_anonymous_leaf ( - inAutoHint(local,dbname, AddHints (List.map (fun (name, c) -> make_trivial env sigma ?name c) l)))) + inAutoHint(local,dbname, + AddHints (List.map (fun (name, c) -> make_trivial env sigma ~name c) l)))) dbnames let forward_intern_tac = @@ -635,8 +779,9 @@ let forward_intern_tac = let set_extern_intern_tac f = forward_intern_tac := f type hints_entry = - | HintsResolveEntry of (int option * bool * global_reference option * constr) list - | HintsImmediateEntry of (global_reference option * constr) list + | HintsResolveEntry of (int option * bool * hints_path_atom * constr) list + | HintsImmediateEntry of (hints_path_atom * constr) list + | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool | HintsExternEntry of @@ -677,10 +822,10 @@ let prepare_hint env (sigma,c) = mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in iter c -let name_of_constr_expr c = +let path_of_constr_expr c = match c with - | Topconstr.CRef r -> (try Some (global r) with _ -> None) - | _ -> None + | Topconstr.CRef r -> (try PathHints [global r] with _ -> PathAny) + | _ -> PathAny let interp_hints h = let f c = @@ -693,8 +838,8 @@ let interp_hints h = let r' = evaluable_of_global_reference (Global.env()) gr in Dumpglob.add_glob (loc_of_reference r) gr; r' in - let fres (o, b, c) = (o, b, name_of_constr_expr c, f c) in - let fi c = name_of_constr_expr c, f c in + let fres (o, b, c) = (o, b, path_of_constr_expr c, f c) in + let fi c = path_of_constr_expr c, f c in let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in match h with | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) @@ -706,7 +851,7 @@ let interp_hints h = let constr_hints_of_ind qid = let ind = global_inductive_with_alias qid in list_tabulate (fun i -> let c = (ind,i+1) in - None, true, Some (ConstructRef c), mkConstruct c) + None, true, PathHints [ConstructRef c], mkConstruct c) (nconstructors ind) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) | HintsExtern (pri, patcom, tacexp) -> @@ -725,6 +870,7 @@ let add_hints local dbnames0 h = match h with | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames + | HintsCutEntry lhints -> add_cuts lhints local dbnames | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames | HintsTransparencyEntry (lhints, b) -> add_transparency lhints b local dbnames @@ -827,17 +973,18 @@ let print_hint_db db = else str"Non-discriminated database"))); msgnl (hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids)); msgnl (hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts)); + msgnl (hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db))); Hint_db.iter (fun head hintlist -> match head with | Some head -> msg (hov 0 (str "For " ++ pr_global head ++ str " -> " ++ - pr_hint_list hintlist)) + pr_hint_list (List.map (fun x -> (0,x)) hintlist))) | None -> msg (hov 0 (str "For any goal -> " ++ - pr_hint_list hintlist))) + pr_hint_list (List.map (fun x -> (0, x)) hintlist)))) db let print_hint_db_by_name dbname = @@ -934,16 +1081,16 @@ let make_local_hint_db ?ts eapply lems gl = (Hint_db.add_list hintlist (Hint_db.empty ts false)) gl (* Serait-ce possible de compiler d'abord la tactique puis de faire la - substitution sans passer par bdize dont l'objectif est de préparer un + substitution sans passer par bdize dont l'objectif est de préparer un terme pour l'affichage ? (HH) *) -(* Si on enlève le dernier argument (gl) conclPattern est calculé une +(* Si on enlève le dernier argument (gl) conclPattern est calculé une fois pour toutes : en particulier si Pattern.somatch produit une UserError -Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même -si après Intros la conclusion matche le pattern. +Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même +si après Intros la conclusion matche le pattern. *) -(* conclPattern doit échouer avec error car il est rattraper par tclFIRST *) +(* conclPattern doit échouer avec error car il est rattraper par tclFIRST *) let forward_interp_tactic = ref (fun _ -> failwith "interp_tactic is not installed for auto") @@ -964,8 +1111,8 @@ let conclPattern concl pat tac gl = (**************************************************************************) (* local_db is a Hint database containing the hypotheses of current goal *) -(* Papageno : cette fonction a été pas mal simplifiée depuis que la base - de Hint impérative a été remplacée par plusieurs bases fonctionnelles *) +(* Papageno : cette fonction a été pas mal simplifiée depuis que la base + de Hint impérative a été remplacée par plusieurs bases fonctionnelles *) let flags_of_state st = {auto_unif_flags with diff --git a/tactics/auto.mli b/tactics/auto.mli index ce2b33013b..521c5ed240 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -32,16 +32,20 @@ type 'a auto_tactic = open Glob_term +type hints_path_atom = + | PathHints of global_reference list + | PathAny + type 'a gen_auto_tactic = { pri : int; (** A number between 0 and 4, 4 = lower priority *) pat : constr_pattern option; (** A pattern for the concl of the Goal *) - name : global_reference option; (** A potential name to refer to the hint *) + name : hints_path_atom; (** A potential name to refer to the hint *) code : 'a auto_tactic; (** the tactic to apply when the concl matches pat *) } type pri_auto_tactic = clausenv gen_auto_tactic -type stored_data = int * pri_auto_tactic +type stored_data = int * clausenv gen_auto_tactic type search_entry @@ -49,24 +53,40 @@ type search_entry type hint_entry = global_reference option * types gen_auto_tactic +type hints_path = + | PathAtom of hints_path_atom + | PathStar of hints_path + | PathSeq of hints_path * hints_path + | PathOr of hints_path * hints_path + | PathEmpty + | PathEpsilon + +val normalize_path : hints_path -> hints_path +val path_matches : hints_path -> hints_path_atom list -> bool +val path_derivate : hints_path -> hints_path_atom -> hints_path +val pp_hints_path : hints_path -> Pp.std_ppcmds + module Hint_db : sig type t val empty : transparent_state -> bool -> t val find : global_reference -> t -> search_entry - val map_none : t ->pri_auto_tactic list + val map_none : t -> pri_auto_tactic list val map_all : global_reference -> t -> pri_auto_tactic list val map_auto : global_reference * constr -> t -> pri_auto_tactic list val add_one : hint_entry -> t -> t val add_list : (hint_entry) list -> t -> t val remove_one : global_reference -> t -> t val remove_list : global_reference list -> t -> t - val iter : (global_reference option -> stored_data list -> unit) -> t -> unit + val iter : (global_reference option -> pri_auto_tactic list -> unit) -> t -> unit val use_dn : t -> bool val transparent_state : t -> transparent_state val set_transparent_state : t -> transparent_state -> t + val add_cut : hints_path -> t -> t + val cut : t -> hints_path + val unfolds : t -> Idset.t * Cset.t end @@ -75,8 +95,9 @@ type hint_db_name = string type hint_db = Hint_db.t type hints_entry = - | HintsResolveEntry of (int option * bool * global_reference option * constr) list - | HintsImmediateEntry of (global_reference option * constr) list + | HintsResolveEntry of (int option * bool * hints_path_atom * constr) list + | HintsImmediateEntry of (hints_path_atom * constr) list + | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool | HintsExternEntry of @@ -119,7 +140,7 @@ val print_hint_db : Hint_db.t -> unit [c] is the term given as an exact proof to solve the goal; [ctyp] is the type of [c]. *) -val make_exact_entry : evar_map -> int option -> ?name:global_reference -> constr * constr -> hint_entry +val make_exact_entry : evar_map -> int option -> ?name:hints_path_atom -> constr * constr -> hint_entry (** [make_apply_entry (eapply,hnf,verbose) pri (c,cty)]. [eapply] is true if this hint will be used only with EApply; @@ -129,7 +150,7 @@ val make_exact_entry : evar_map -> int option -> ?name:global_reference -> const [cty] is the type of [c]. *) val make_apply_entry : - env -> evar_map -> bool * bool * bool -> int option -> ?name:global_reference -> + env -> evar_map -> bool * bool * bool -> int option -> ?name:hints_path_atom -> constr * constr -> hint_entry (** A constr which is Hint'ed will be: @@ -140,7 +161,7 @@ val make_apply_entry : has missing arguments. *) val make_resolves : - env -> evar_map -> bool * bool * bool -> int option -> ?name:global_reference -> + env -> evar_map -> bool * bool * bool -> int option -> ?name:hints_path_atom -> constr -> hint_entry list (** [make_resolve_hyp hname htyp]. diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index c9951bea2d..a974c76a0c 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -34,7 +34,7 @@ let subst_hint subst hint = let typ' = subst_mps subst hint.rew_type in let pat' = subst_mps subst hint.rew_pat in let t' = Tacinterp.subst_tactic subst hint.rew_tac in - if hint.rew_lemma == cst' && hint.rew_tac == t' then hint else + if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else { hint with rew_lemma = cst'; rew_type = typ'; rew_pat = pat'; rew_tac = t' } diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 184f521e17..1f8ee3af6d 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -146,7 +146,7 @@ let rec e_trivial_fail_db db_list local_db goal = let hintl = make_resolve_hyp (pf_env g') (project g') d in (e_trivial_fail_db db_list (Hint_db.add_list hintl local_db) g'))) :: - (List.map (fun (x,_,_,_) -> x) (e_trivial_resolve db_list local_db (pf_concl goal))) + (List.map (fun (x,_,_,_,_) -> x) (e_trivial_resolve db_list local_db (pf_concl goal))) in tclFIRST (List.map tclCOMPLETE tacl) goal @@ -166,7 +166,7 @@ and e_my_find_search db_list local_db hdc complete concl = (local_db::db_list) in let tac_of_hint = - fun (flags, {pri=b; pat = p; code=t}) -> + fun (flags, {pri = b; pat = p; code = t; name = name}) -> let tac = match t with | Res_pf (term,cl) -> with_prods nprods (term,cl) (unify_resolve flags) @@ -177,14 +177,16 @@ and e_my_find_search db_list local_db hdc complete concl = (if complete then tclIDTAC else e_trivial_fail_db db_list local_db) | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [all_occurrences,c]) | Extern tacast -> - tclTHEN - (fun gl -> Refiner.tclEVARS (mark_unresolvables (project gl)) gl) +(* tclTHEN *) +(* (fun gl -> Refiner.tclEVARS (mark_unresolvables (project gl)) gl) *) (conclPattern concl p tacast) in let tac = if complete then tclCOMPLETE tac else tac in match t with - | Extern _ -> (tac,b,true,lazy (pr_autotactic t)) - | _ -> (tac,b,false,lazy (pr_autotactic t)) + | Extern _ -> (tac,b,true, name, lazy (pr_autotactic t)) + | _ -> +(* let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *) + (tac,b,false, name, lazy (pr_autotactic t)) in List.map tac_of_hint hintl and e_trivial_resolve db_list local_db gl = @@ -212,7 +214,9 @@ let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l) type autoinfo = { hints : Auto.hint_db; is_evar: existential_key option; - only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t} + only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t; + auto_path : global_reference option list; + auto_cut : hints_path } type autogoal = goal * autoinfo type 'ans fk = unit -> 'ans type ('a,'ans) sk = 'a -> 'ans fk -> 'ans @@ -239,24 +243,35 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) = let keep = not only_classes || is_class in if keep then let c = mkVar id in + let name = PathHints [VarRef id] in let hints = if is_class then - let hints = build_subclasses env sigma (mkVar id) in - list_map_append - (make_resolves env sigma (true,false,Flags.is_verbose()) None) hints + let hints = build_subclasses ~check:false env sigma (VarRef id) None in + (list_map_append + (fun (pri, c) -> make_resolves env sigma + (true,false,Flags.is_verbose()) pri c) + hints) else [] in - hints @ map_succeed - (fun f -> try f (c,cty) with UserError _ -> failwith "") - [make_exact_entry sigma pri; make_apply_entry env sigma flags pri] + (hints @ map_succeed + (fun f -> try f (c,cty) with UserError _ -> failwith "") + [make_exact_entry ~name sigma pri; make_apply_entry ~name env sigma flags pri]) else [] let pf_filtered_hyps gls = Goal.V82.hyps gls.Evd.sigma (sig_it gls) let make_hints g st only_classes sign = - let hintlist = list_map_append - (pf_apply make_resolve_hyp g st (true,false,false) only_classes None) sign + let paths, hintlist = + List.fold_left + (fun (paths, hints) hyp -> + if is_section_variable (pi1 hyp) then (paths, hints) + else + let path, hint = + PathEmpty, pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp + in + (PathOr (paths, path), hint @ hints)) + (PathEmpty, []) sign in Hint_db.add_list hintlist (Hint_db.empty st true) let make_autogoal_hints = @@ -289,17 +304,10 @@ let intro_tac : atac = in {it = gls'; sigma = s}) let normevars_tac : atac = - { skft = fun sk fk {it = gl; sigma = s} -> - let gl', sigma' = Goal.V82.nf_evar s (fst gl) in - sk {it = [gl', snd gl]; sigma = sigma'} fk } - - (* lift_tactic tclNORMEVAR *) - (* (fun {it = gls; sigma = s} info -> *) - (* let gls' = *) - (* List.map (fun g' -> *) - (* (g', { info with auto_last_tac = str"NORMEVAR" })) gls *) - (* in {it = gls'; sigma = s}) *) - + { skft = fun sk fk {it = (gl, info); sigma = s} -> + let gl', sigma' = Goal.V82.nf_evar s gl in + let info' = { info with auto_last_tac = lazy (str"normevars") } in + sk {it = [gl', info']; sigma = sigma'} fk } (* Ordering of states is lexicographic on the number of remaining goals. *) let compare (pri, _, _, res) (pri', _, _, res') = @@ -319,20 +327,21 @@ let hints_tac hints = let tacgl = {it = gl; sigma = s} in let poss = e_possible_resolve hints info.hints concl in let rec aux i foundone = function - | (tac, _, b, pp) :: tl -> + | (tac, _, b, name, pp) :: tl -> + let derivs = path_derivate info.auto_cut name in let res = - try Some (tac tacgl) + try + if path_matches derivs [] then None else Some (tac tacgl) with e when catchable e -> None in (match res with - | None -> - aux i foundone tl + | None -> aux i foundone tl | Some {it = gls; sigma = s'} -> if !typeclasses_debug then msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp ++ str" on" ++ spc () ++ pr_ev s gl); let fk = - (fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *) + (fun () -> if !typeclasses_debug then msgnl (str"backtracked after " ++ Lazy.force pp); aux (succ i) true tl) in let sgls = @@ -349,7 +358,7 @@ let hints_tac hints = | None -> gls', s' | Some (evgls, s') -> (* Reorder with dependent subgoals. *) - (List.map (fun (ev, x) -> Some ev, x) evgls @ gls', s') + (gls' @ List.map (fun (ev, x) -> Some ev, x) evgls, s') in let gls' = list_map_i (fun j (evar, g) -> @@ -360,7 +369,8 @@ let hints_tac hints = if b && not (Environ.eq_named_context_val (Goal.V82.hyps s' g) (Goal.V82.hyps s' gl)) then make_autogoal_hints info.only_classes ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'} - else info.hints } + else info.hints; + auto_cut = derivs } in g, info) 1 newgls in let glsv = {it = gls'; sigma = s'} in sk glsv fk) @@ -372,9 +382,14 @@ let hints_tac hints = fk () in aux 1 false poss } -let dependent only_classes evd oev concl = - if oev <> None then true - else not (Intset.is_empty (Evarutil.evars_of_term concl)) +let isProp env sigma concl = + let ty = Retyping.get_type_of env sigma concl in + kind_of_term ty = Sort (Prop Null) + +let needs_backtrack only_classes env evd oev concl = + if oev = None || isProp env evd concl then + not (Intset.is_empty (Evarutil.evars_of_term concl)) + else true let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk = let rec aux s (acc : autogoal list list) fk = function @@ -386,11 +401,15 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk (fun {it=gls';sigma=s'} fk' -> let needs_backtrack = if gls' = [] then - dependent info.only_classes s' info.is_evar (Goal.V82.concl s gl) + needs_backtrack info.only_classes + (Goal.V82.env s gl) s' info.is_evar (Goal.V82.concl s gl) else true in - let fk'' = if not needs_backtrack then - (if !typeclasses_debug then msgnl (str"no backtrack on " ++ pr_ev s gl); fk) else fk' + let fk'' = + if not needs_backtrack then + (if !typeclasses_debug then msgnl (str"no backtrack on " ++ pr_ev s gl ++ + str " after " ++ Lazy.force info.auto_last_tac); fk) + else fk' in aux s' (gls'::acc) fk'' gls) fk {it = (gl,info); sigma = s}) | [] -> Some (List.rev acc, s, fk) @@ -425,14 +444,20 @@ let rec fix_limit limit (t : 'a tac) : 'a tac = if limit = 0 then fail_tac else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk } -let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) ev g = +let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) cut ev g = let hints = make_autogoal_hints only_classes ~st g in (g.it, { hints = hints ; is_evar = ev; - only_classes = only_classes; auto_depth = []; auto_last_tac = lazy (mt()) }) + only_classes = only_classes; auto_depth = []; auto_last_tac = lazy (str"none"); + auto_path = []; auto_cut = cut }) -let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) gs evm' = + +let cut_of_hints h = + List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h + +let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) hints gs evm' = + let cut = cut_of_hints hints in { it = list_map_i (fun i g -> - let (gl, auto) = make_autogoal ~only_classes ~st (Some (fst g)) {it = snd g; sigma = evm'} in + let (gl, auto) = make_autogoal ~only_classes ~st cut (Some (fst g)) {it = snd g; sigma = evm'} in (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' } let get_result r = @@ -440,11 +465,11 @@ let get_result r = | None -> None | Some (gls, fk) -> Some (gls.sigma,fk) -let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac = +let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm hints tac = match evars_to_goals p evm with | None -> None (* This happens only because there's no evar having p *) | Some (goals, evm') -> - let res = run_list_tac tac p goals (make_autogoals ~only_classes ~st goals evm') in + let res = run_list_tac tac p goals (make_autogoals ~only_classes ~st hints goals evm') in match get_result res with | None -> raise Not_found | Some (evm', fk) -> Some (evars_reset_evd ~with_conv_pbs:true evm' evm, fk) @@ -458,7 +483,7 @@ let eauto_tac ?limit hints = | Some limit -> fix_limit limit (eauto_tac hints) let eauto ?(only_classes=true) ?st ?limit hints g = - let gl = { it = make_autogoal ~only_classes ?st None g; sigma = project g } in + let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g } in match run_tac (eauto_tac ?limit hints) gl with | None -> raise Not_found | Some {it = goals; sigma = s} -> @@ -467,7 +492,7 @@ let eauto ?(only_classes=true) ?st ?limit hints g = let real_eauto st ?limit hints p evd = let rec aux evd fails = let res, fails = - try run_on_evars ~st p evd (eauto_tac ?limit hints), fails + try run_on_evars ~st p evd hints (eauto_tac ?limit hints), fails with Not_found -> List.fold_right (fun fk (res, fails) -> match res with diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index a264de3188..9966fb7724 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -499,3 +499,55 @@ END TACTIC EXTEND convert_concl_no_check | ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ] END + + +let pr_hints_path_atom prc _ _ a = + match a with + | PathAny -> str"." + | PathHints grs -> + prlist_with_sep pr_spc Printer.pr_global grs + +ARGUMENT EXTEND hints_path_atom + TYPED AS hints_path_atom + PRINTED BY pr_hints_path_atom +| [ global_list(g) ] -> [ PathHints (List.map Nametab.global g) ] +| [ "*" ] -> [ PathAny ] +END + +let pr_hints_path prc prx pry c = + let rec aux = function + | PathAtom a -> pr_hints_path_atom prc prx pry a + | PathStar p -> str"(" ++ aux p ++ str")*" + | PathSeq (p, p') -> aux p ++ spc () ++ aux p' + | PathOr (p, p') -> str "(" ++ aux p ++ str"|" ++ aux p' ++ str")" + | PathEmpty -> str"ø" + | PathEpsilon -> str"ε" + in aux c + +ARGUMENT EXTEND hints_path + TYPED AS hints_path + PRINTED BY pr_hints_path +| [ "(" hints_path(p) ")" ] -> [ p ] +| [ "!" hints_path(p) ] -> [ PathStar p ] +| [ "emp" ] -> [ PathEmpty ] +| [ "eps" ] -> [ PathEpsilon ] +| [ hints_path_atom(a) ] -> [ PathAtom a ] +| [ hints_path(p) "|" hints_path(q) ] -> [ PathOr (p, q) ] +| [ hints_path(p) ";" hints_path(q) ] -> [ PathSeq (p, q) ] +END + +let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases + +ARGUMENT EXTEND opthints + TYPED AS preident_list_opt + PRINTED BY pr_hintbases +| [ ":" ne_preident_list(l) ] -> [ Some l ] +| [ ] -> [ None ] +END + +VERNAC COMMAND EXTEND HintCut +| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ + let entry = HintsCutEntry p in + Auto.add_hints (Vernacexpr.use_section_locality ()) + (match dbnames with None -> ["core"] | Some l -> l) entry ] +END diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index bae28c7ce8..da35edbedc 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -286,7 +286,7 @@ let project_hint pri l2r c = let c = Reductionops.whd_beta Evd.empty (mkApp (c,Termops.extended_rel_vect 0 sign)) in let c = it_mkLambda_or_LetIn (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in - (pri,true,None,c) + (pri,true,Auto.PathAny,c) let add_hints_iff l2r lc n bl = Auto.add_hints true bl diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 04688b00f9..55199cdead 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -408,41 +408,45 @@ Class PartialApplication. CoInductive normalization_done : Prop := did_normalization. Ltac partial_application_tactic := - let rec do_partial_apps H m := + let rec do_partial_apps H m cont := match m with - | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H] - | _ => idtac + | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; + [(do_partial_apps H m' ltac:idtac)|clear H] + | _ => cont end in - let rec do_partial H ar m := + let rec do_partial H ar m := match ar with - | 0 => do_partial_apps H m + | 0%nat => do_partial_apps H m ltac:(fail 1) | S ?n' => match m with ?m' ?x => do_partial H n' m' end end in - let on_morphism m := - let m' := fresh in head_of_constr m' m ; - let n := fresh in evar (n:nat) ; - let v := eval compute in n in clear n ; - let H := fresh in - assert(H:Params m' v) by typeclasses eauto ; - let v' := eval compute in v in subst m'; - do_partial H v' m - in + let params m sk fk := + (let m' := fresh in head_of_constr m' m ; + let n := fresh in evar (n:nat) ; + let v := eval compute in n in clear n ; + let H := fresh in + assert(H:Params m' v) by typeclasses eauto ; + let v' := eval compute in v in subst m'; + (sk H v' || fail 1)) + || fk + in + let on_morphism m cont := + params m ltac:(fun H n => do_partial H n m) + ltac:(cont) + in match goal with | [ _ : normalization_done |- _ ] => fail 1 | [ _ : @Params _ _ _ |- _ ] => fail 1 | [ |- @Proper ?T _ (?m ?x) ] => match goal with - | [ _ : PartialApplication |- _ ] => - class_apply @Reflexive_partial_app_morphism - | _ => - on_morphism (m x) || - (class_apply @Reflexive_partial_app_morphism ; - [ pose Build_PartialApplication | idtac ]) + | [ H : PartialApplication |- _ ] => + class_apply @Reflexive_partial_app_morphism; [|clear H] + | _ => on_morphism (m x) + ltac:(class_apply @Reflexive_partial_app_morphism) end end. @@ -471,7 +475,7 @@ Qed. Lemma inverse_arrow `(NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R'')) : Normalizes (A -> B) (R ==> R') (inverse (R''' ==> R'')%signature). -Proof. unfold Normalizes in *. intros. +Proof. unfold Normalizes in *. intros. rewrite NA, NB. firstorder. Qed. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 397328a118..3a34e3a119 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -156,14 +156,14 @@ Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A. (** A [PreOrder] is both Reflexive and Transitive. *) Class PreOrder {A} (R : relation A) : Prop := { - PreOrder_Reflexive :> Reflexive R ; - PreOrder_Transitive :> Transitive R }. + PreOrder_Reflexive :> Reflexive R | 2 ; + PreOrder_Transitive :> Transitive R | 2 }. (** A partial equivalence relation is Symmetric and Transitive. *) Class PER {A} (R : relation A) : Prop := { - PER_Symmetric :> Symmetric R ; - PER_Transitive :> Transitive R }. + PER_Symmetric :> Symmetric R | 3 ; + PER_Transitive :> Transitive R | 3 }. (** Equivalence relations. *) diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v index c30d38186a..00a8405200 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v @@ -285,7 +285,7 @@ Section Z_2nZ. (* ** Record of operators on 2 words *) - Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) := + Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) | 1 := ZnZ.MkOps _ww_digits _ww_zdigits to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 @@ -305,7 +305,7 @@ Section Z_2nZ. sqrt2 sqrt. - Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) := + Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) | 2 := ZnZ.MkOps _ww_digits _ww_zdigits to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 39e9f02c53..92afbcb537 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -51,6 +51,8 @@ Qed. Definition b2z (b:bool) := if b then 1 else 0. Local Coercion b2z : bool >-> t. +Instance b2z_wd : Proper (Logic.eq ==> eq) b2z := _. + Lemma exists_div2 a : exists a' (b:bool), a == 2*a' + b. Proof. elim (Even_or_Odd a); [intros (a',H)| intros (a',H)]. @@ -84,8 +86,8 @@ Qed. Lemma testbit_spec' a n : 0<=n -> a.[n] == (a / 2^n) mod 2. Proof. - intro Hn. revert a. apply le_ind with (4:=Hn). - solve_proper. + intro Hn. revert a. apply le_ind with (4:=Hn). + solve_proper. intros a. nzsimpl. destruct (exists_div2 a) as (a' & b & H). rewrite H at 1. rewrite testbit_0_r. apply mod_unique with a'; trivial. diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index ce720c38cf..c66f003ec7 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -48,6 +48,9 @@ Qed. Definition b2n (b:bool) := if b then 1 else 0. Local Coercion b2n : bool >-> t. +Instance b2n_proper : Proper (Logic.eq ==> eq) b2n. +Proof. solve_proper. Qed. + Lemma exists_div2 a : exists a' (b:bool), a == 2*a' + b. Proof. elim (Even_or_Odd a); [intros (a',H)| intros (a',H)]. diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index 33267a5187..995fbb9eea 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -94,6 +94,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Z.spec_gcd N.spec_gcd Zgcd_Zabs Zgcd_1 spec_Z_of_N spec_Zabs_N : nz. + Ltac nzsimpl := autorewrite with nz in *. Ltac qsimpl := try red; unfold to_Q; simpl; intros; diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 55c68d3cef..61d7d31d7e 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -37,10 +37,11 @@ let set_typeclass_transparency c local b = let _ = Typeclasses.register_add_instance_hint (fun inst local pri -> + let path = try Auto.PathHints [global_of_constr inst] with _ -> Auto.PathAny in Flags.silently (fun () -> Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry - [pri, false, Some inst, constr_of_global inst])) ()); + [pri, false, path, inst])) ()); Typeclasses.register_set_typeclass_transparency set_typeclass_transparency; Typeclasses.register_classes_transparent_state (fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db)) @@ -53,7 +54,7 @@ let declare_class g = Pp.str"Unsupported class type, only constants and inductives are allowed") (** TODO: add subinstances *) -let declare_instance glob g = +let existing_instance glob g = let c = global g in let instance = Typing.type_of (Global.env ()) Evd.empty (constr_of_global c) in let _, r = decompose_prod_assum instance in @@ -100,10 +101,9 @@ open Pp let ($$) g f = fun x -> g (f x) let instance_hook k pri global imps ?hook cst = - let inst = Typeclasses.new_instance k pri global cst in - Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps; - Typeclasses.add_instance inst; - (match hook with Some h -> h cst | None -> ()) + Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps; + Typeclasses.declare_instance pri (not global) cst; + (match hook with Some h -> h cst | None -> ()) let declare_instance_constant k pri global imps ?hook id term termtype = let cdecl = @@ -283,29 +283,7 @@ let named_of_rel_context l = let string_of_global r = string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r) - -let rec build_subclasses env sigma c = - let ty = Retyping.get_type_of env sigma c in - match class_of_constr ty with - | None -> [] - | Some (rels, (tc, args)) -> - let projs = list_map_filter - (fun (n, b, proj) -> - if b then Option.map (fun p -> Nameops.out_name n, mkConst p) proj - else None) tc.cl_projs - in - let instapp = appvectc c (Termops.extended_rel_vect 0 rels) in - let projargs = Array.of_list (args @ [instapp]) in - let declare_proj (n, p) = - let body = it_mkLambda_or_LetIn (mkApp (p, projargs)) rels in - body :: build_subclasses env sigma body - in list_map_append declare_proj projs - -let declare_subclasses constr = - let hints = build_subclasses (Global.env ()) Evd.empty constr in - let entry = List.map (fun c -> (None, false, None, c)) hints in - Auto.add_hints true (* local *) [typeclasses_db] (Auto.HintsResolveEntry entry) - + let context l = let env = Global.env() in let evars = ref Evd.empty in @@ -332,7 +310,6 @@ let context l = match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls in Command.declare_assumption false (Local (* global *), Definitional) t - [] impl (* implicit *) None (* inline *) (dummy_loc, id); - declare_subclasses (mkVar id)) + [] impl (* implicit *) None (* inline *) (dummy_loc, id)) in List.iter fn (List.rev ctx) diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 0f842ffe50..68a93a7428 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -32,7 +32,7 @@ val declare_class : reference -> unit (** Instance declaration *) -val declare_instance : bool -> reference -> unit +val existing_instance : bool -> reference -> unit val declare_instance_constant : typeclass -> @@ -72,5 +72,3 @@ val context : local_binder list -> unit (** Forward ref for refine *) val refine_ref : (open_constr -> Proof_type.tactic) ref - -val build_subclasses : env -> evar_map -> constr -> constr list diff --git a/toplevel/command.ml b/toplevel/command.ml index e85c4299b7..fff6eb6fa2 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -136,7 +136,8 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = if is_verbose () & Pfedit.refining () then msgerrnl (str"Warning: Variable " ++ pr_id ident ++ str" is not visible from current goals"); - VarRef ident + let r = VarRef ident in + Typeclasses.declare_instance None true r; r | (Global|Local) -> let kn = declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in @@ -147,8 +148,10 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = msg_warning (pr_id ident ++ str" is declared as a parameter" ++ str" because it is at a global level"); Autoinstance.search_declaration (ConstRef kn); - gr in - if is_coe then Class.try_add_new_coercion r local + Typeclasses.declare_instance None false gr; + gr + in + if is_coe then Class.try_add_new_coercion r local let declare_assumptions_hook = ref ignore let set_declare_assumptions_hook = (:=) declare_assumptions_hook diff --git a/toplevel/record.ml b/toplevel/record.ml index 6d94e9a856..a7f7b24588 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -290,15 +290,15 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map pi1 ctx))) -let declare_instance_cst glob con = +let declare_instance_cst glob con pri = let instance = Typeops.type_of_constant (Global.env ()) con in let _, r = decompose_prod_assum instance in match class_of_constr r with - | Some (_, (tc, _)) -> add_instance (new_instance tc None glob (ConstRef con)) + | Some (_, (tc, _)) -> add_instance (new_instance tc pri glob (ConstRef con)) | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.") let declare_class finite def infer id idbuild paramimpls params arity fieldimpls fields - ?(kind=StructureComponent) ?name is_coe coers sign = + ?(kind=StructureComponent) ?name is_coe coers priorities sign = let fieldimpls = (* Make the class and all params implicits in the projections *) let ctx_impls = implicits_of_context params in @@ -334,13 +334,15 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; Classes.set_typeclass_transparency (EvalConstRef cst) false false; if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign (); - cref, [Name proj_name, List.hd coers, Some proj_cst] + let sub = if List.hd coers then Some (List.hd priorities) else None in + cref, [Name proj_name, sub, Some proj_cst] | _ -> let idarg = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls - params (Option.cata (fun x -> x) (Termops.new_Type ()) arity) fieldimpls fields + params (Option.default (Termops.new_Type ()) arity) fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign in + let coers = List.map2 (fun coe pri -> if coe then Some pri else None) coers priorities in IndRef ind, (list_map3 (fun (id, _, _) b y -> (id, b, y)) (List.rev fields) coers (Recordops.lookup_projections ind)) in @@ -357,9 +359,9 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls cl_props = fields; cl_projs = projs } in - List.iter2 (fun p sub -> - if sub then match p with (_, _, Some p) -> declare_instance_cst true p | _ -> ()) - k.cl_projs coers; +(* list_iter3 (fun p sub pri -> *) +(* if sub then match p with (_, _, Some p) -> declare_instance_cst true p pri | _ -> ()) *) +(* k.cl_projs coers priorities; *) add_class k; impl let interp_and_check_sort sort = @@ -376,6 +378,7 @@ open Autoinstance list telling if the corresponding fields must me declared as coercion *) let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in + let cfs,priorities = List.split cfs in let coers,fs = List.split cfs in let extract_name acc = function Vernacexpr.AssumExpr((_,Name id),_) -> id::acc @@ -383,6 +386,8 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil | _ -> acc in let allnames = idstruc::(List.fold_left extract_name [] fs) in if not (list_distinct allnames) then error "Two objects have the same name"; + if not (kind = Class false) && List.exists ((<>) None) priorities then + error "Priorities only allowed for type class substructures"; (* Now, younger decl in params and fields is on top *) let sc = interp_and_check_sort s in let implpars, params, implfs, fields = @@ -392,7 +397,7 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil match kind with | Class def -> let gr = declare_class finite def infer (loc,idstruc) idbuild - implpars params sc implfs fields is_coe coers sign in + implpars params sc implfs fields is_coe coers priorities sign in if infer then search_record declare_class_instance gr sign; gr | _ -> diff --git a/toplevel/record.mli b/toplevel/record.mli index 96a84c3176..131a5b9e1f 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -35,5 +35,5 @@ val declare_structure : Decl_kinds.recursivity_kind -> val definition_structure : inductive_kind * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list * - (local_decl_expr with_coercion with_notation) list * + (local_decl_expr with_coercion with_priority with_notation) list * identifier * constr_expr option -> global_reference diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0de85a4564..07454337f7 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -392,7 +392,7 @@ let vernac_record k finite infer struc binders sort nameopt cfs = Dumpglob.dump_definition lid false "constr"; id in if Dumpglob.dump () then ( Dumpglob.dump_definition (snd struc) false "rec"; - List.iter (fun ((_, x), _) -> + List.iter (fun (((_, x), _), _) -> match x with | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" | _ -> ()) cfs); @@ -415,7 +415,7 @@ let vernac_inductive finite infer indl = | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> let f = let (coe, ((loc, id), ce)) = l in - ((coe, AssumExpr ((loc, Name id), ce)), []) + (((coe, AssumExpr ((loc, Name id), ce)), None), []) in vernac_record (Class true) finite infer id bl c None [f] | [ ( id , bl , c , Class true, _), _ ] -> Util.error "Definitional classes must have a single method" @@ -632,7 +632,7 @@ let vernac_context l = Classes.context l let vernac_declare_instances glob ids = - List.iter (fun (id) -> Classes.declare_instance glob id) ids + List.iter (fun (id) -> Classes.existing_instance glob id) ids let vernac_declare_class id = Classes.declare_class id diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index a6c304f671..ea7d0c6e2f 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -165,10 +165,11 @@ type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list type 'a with_coercion = coercion_flag * 'a type 'a with_notation = 'a * decl_notation list +type 'a with_priority = 'a * int option type constructor_expr = (lident * constr_expr) with_coercion type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list - | RecordDecl of lident option * local_decl_expr with_coercion with_notation list + | RecordDecl of lident option * local_decl_expr with_coercion with_priority with_notation list type inductive_expr = lident with_coercion * local_binder list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr |