diff options
Diffstat (limited to 'tactics/class_tactics.ml4')
| -rw-r--r-- | tactics/class_tactics.ml4 | 810 |
1 files changed, 418 insertions, 392 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 465d1d80..42df244d 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: class_tactics.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names @@ -19,7 +17,6 @@ open Termops open Sign open Reduction open Proof_type -open Proof_trees open Declarations open Tacticals open Tacmach @@ -28,7 +25,7 @@ open Tactics open Pattern open Clenv open Auto -open Rawterm +open Glob_term open Hiddentac open Typeclasses open Typeclasses_errors @@ -38,77 +35,57 @@ open Pfedit open Command open Libnames open Evd +open Compat -let default_eauto_depth = 100 let typeclasses_db = "typeclass_instances" +let typeclasses_debug = ref false +let typeclasses_depth = ref None -let _ = Auto.auto_init := (fun () -> - Auto.create_hint_db false typeclasses_db full_transparent_state true) +let _ = + Auto.add_auto_init + (fun () -> Auto.create_hint_db false typeclasses_db full_transparent_state true) exception Found of evar_map -let is_dependent ev evm = - Evd.fold (fun ev' evi dep -> - if ev = ev' then dep - else dep || occur_evar ev evi.evar_concl) - evm false - -let valid goals p res_sigma l = - let evm = - List.fold_left2 - (fun sigma (ev, evi) prf -> - let cstr, obls = Refiner.extract_open_proof !res_sigma prf in - if not (Evd.is_defined sigma ev) then - Evd.define ev cstr sigma - else sigma) - !res_sigma goals l - in raise (Found evm) - -let evar_filter evi = - let hyps' = evar_filtered_context evi in - { evi with - evar_hyps = Environ.val_of_named_context hyps'; - evar_filter = List.map (fun _ -> true) hyps' } +(** We transform the evars that are concerned by this resolution + (according to predicate p) into goals. + Invariant: function p only manipulates undefined evars *) let evars_to_goals p evm = let goals, evm' = - Evd.fold + Evd.fold_undefined (fun ev evi (gls, evm') -> - if evi.evar_body = Evar_empty then - let evi', goal = p evm ev evi in - if goal then - ((ev, evi') :: gls, Evd.add evm' ev evi') - else (gls, Evd.add evm' ev evi') - else (gls, Evd.add evm' ev evi)) - evm ([], Evd.empty) + let evi', goal = p evm ev evi in + let gls' = if goal then (ev,Goal.V82.build ev) :: gls else gls in + (gls', Evd.add evm' ev evi')) + evm ([], Evd.defined_evars evm) in - if goals = [] then None - else - let goals = List.rev goals in - let evm' = evars_reset_evd ~with_conv_pbs:false evm' evm in - Some (goals, evm') + if goals = [] then None else Some (List.rev goals, evm') (** Typeclasses instance search tactic / eauto *) -let intersects s t = - Intset.exists (fun el -> Intset.mem el t) s - open Auto let e_give_exact flags c gl = let t1 = (pf_type_of gl c) in tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl -let assumption flags id = e_give_exact flags (mkVar id) - open Unification let auto_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = true; + use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = var_full_transparent_state; + modulo_delta_types = full_transparent_state; + check_applied_meta_types = false; resolve_evars = false; - use_evars_pattern_unification = true; + use_pattern_unification = true; + use_meta_bound_pattern_unification = true; + frozen_evars = ExistentialSet.empty; + restrict_conv_on_strict_subterms = false; (* ? *) + modulo_betaiota = true; + modulo_eta = true; + allow_K_in_toplevel_higher_order_unification = false } let rec eq_constr_mod_evars x y = @@ -126,18 +103,18 @@ let progress_evars t gl = in tclTHEN t check gl TACTIC EXTEND progress_evars - [ "progress_evars" tactic(t) ] -> [ progress_evars (snd t) ] + [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.eval_tactic t) ] END let unify_e_resolve flags (c,clenv) gls = let clenv' = connect_clenv gls clenv in - let clenv' = clenv_unique_resolver false ~flags clenv' gls in - tclPROGRESS (Clenvtac.clenv_refine true ~with_classes:false clenv') gls + let clenv' = clenv_unique_resolver ~flags clenv' gls in + Clenvtac.clenv_refine true ~with_classes:false clenv' gls let unify_resolve flags (c,clenv) gls = let clenv' = connect_clenv gls clenv in - let clenv' = clenv_unique_resolver false ~flags clenv' gls in - tclPROGRESS (Clenvtac.clenv_refine false ~with_classes:false clenv') gls + let clenv' = clenv_unique_resolver ~flags clenv' gls in + Clenvtac.clenv_refine false ~with_classes:false clenv' gls let clenv_of_prods nprods (c, clenv) gls = if nprods = 0 then Some clenv @@ -157,7 +134,9 @@ let with_prods nprods (c, clenv) f gls = let flags_of_state st = {auto_unif_flags with - modulo_conv_on_closed_terms = Some st; modulo_delta = st} + modulo_conv_on_closed_terms = Some st; modulo_delta = st; + modulo_delta_types = st; + modulo_eta = false} let rec e_trivial_fail_db db_list local_db goal = let tacl = @@ -168,11 +147,11 @@ 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 -and e_my_find_search db_list local_db hdc concl = +and e_my_find_search db_list local_db hdc complete concl = let hdc = head_of_constr_reference hdc in let prods, concl = decompose_prod_assum concl in let nprods = List.length prods in @@ -188,7 +167,7 @@ and e_my_find_search db_list local_db hdc 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) @@ -196,66 +175,55 @@ and e_my_find_search db_list local_db hdc concl = | Give_exact (c) -> e_give_exact flags c | Res_pf_THEN_trivial_fail (term,cl) -> tclTHEN (with_prods nprods (term,cl) (unify_e_resolve flags)) - (e_trivial_fail_db db_list local_db) + (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 -> conclPattern concl p tacast + | Extern tacast -> +(* 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 = try e_my_find_search db_list local_db - (fst (head_constr_bound gl)) gl + (fst (head_constr_bound gl)) true gl with Bound | Not_found -> [] let e_possible_resolve db_list local_db gl = try e_my_find_search db_list local_db - (fst (head_constr_bound gl)) gl + (fst (head_constr_bound gl)) false gl with Bound | Not_found -> [] let rec catchable = function | Refiner.FailError _ -> true - | Stdpp.Exc_located (_, e) -> catchable e + | Loc.Exc_located (_, e) -> catchable e | e -> Logic.catchable_exception e -let is_dep gl gls = - let evs = Evarutil.evars_of_term gl.evar_concl in - if evs = Intset.empty then false - else - List.fold_left - (fun b gl -> - if b then b - else - let evs' = Evarutil.evars_of_term gl.evar_concl in - intersects evs evs') - false gls - -let is_ground gl = - Evarutil.is_ground_term (project gl) (pf_concl gl) - let nb_empty_evars s = - Evd.fold (fun ev evi acc -> if evi.evar_body = Evar_empty then succ acc else acc) s 0 + Evd.fold_undefined (fun ev evi acc -> succ acc) s 0 -let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) - -let typeclasses_debug = ref false - -type validation = evar_map -> proof_tree list -> proof_tree +let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar evs (Goal.V82.concl evs ev)) 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 type 'a tac = { skft : 'ans. ('a,'ans) sk -> 'ans fk -> autogoal sigma -> 'ans } -type auto_result = autogoal list sigma * validation +type auto_result = autogoal list sigma type atac = auto_result tac @@ -272,26 +240,67 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) = if not (eq_constr ty' ar) then iscl env' ty' else false in - let keep = not only_classes || iscl env cty in - if keep then let c = mkVar id in - map_succeed - (fun f -> try f (c,cty) with UserError _ -> failwith "") - [make_exact_entry sigma pri; make_apply_entry env sigma flags pri] + let is_class = iscl env cty in + 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 ~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 ~name sigma pri; make_apply_entry ~name env sigma flags pri]) else [] let pf_filtered_hyps gls = - evar_filtered_context (sig_it gls) + Goal.V82.hyps gls.Evd.sigma (sig_it gls) + +let make_hints g st only_classes 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 autogoal_hints_cache : (Environ.named_context_val * hint_db) option ref = ref None +let freeze () = !autogoal_hints_cache +let unfreeze v = autogoal_hints_cache := v +let init () = autogoal_hints_cache := None + +let _ = init () -let make_autogoal_hints only_classes ?(st=full_transparent_state) g = - let sign = pf_filtered_hyps g in - let hintlist = list_map_append (pf_apply make_resolve_hyp g st (true,false,false) only_classes None) sign in - Hint_db.add_list hintlist (Hint_db.empty st true) - +let _ = + Summary.declare_summary "autogoal-hints-cache" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init } + +let make_autogoal_hints = + fun only_classes ?(st=full_transparent_state) g -> + let sign = pf_filtered_hyps g in + match freeze () with + | Some (sign', hints) when Environ.eq_named_context_val sign sign' -> hints + | _ -> let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in + unfreeze (Some (sign, hints)); hints + let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac = { skft = fun sk fk {it = gl,hints; sigma=s} -> let res = try Some (tac {it=gl; sigma=s}) with e when catchable e -> None in match res with - | Some (gls,v) -> sk (f gls hints, fun _ -> v) fk + | Some gls -> sk (f gls hints) fk | None -> fk () } let intro_tac : atac = @@ -299,28 +308,22 @@ let intro_tac : atac = (fun {it = gls; sigma = s} info -> let gls' = List.map (fun g' -> - let env = evar_env g' in + let env = Goal.V82.env s g' in + let context = Environ.named_context_of_val (Goal.V82.hyps s g') in let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints) - (true,false,false) info.only_classes None (List.hd (evar_context g')) in + (true,false,false) info.only_classes None (List.hd context) in let ldb = Hint_db.add_list hint info.hints in (g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls in {it = gls'; sigma = s}) let normevars_tac : atac = - lift_tactic tclNORMEVAR - (fun {it = gls; sigma = s} info -> - let gls' = - List.map (fun g' -> - (g', { info with auto_last_tac = lazy (str"NORMEVAR") })) gls - in {it = gls'; sigma = s}) - - -let id_tac : atac = - { skft = fun sk fk {it = gl; sigma = s} -> - sk ({it = [gl]; sigma = s}, fun _ pfs -> List.hd pfs) fk } + { 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', _)) = +let compare (pri, _, _, res) (pri', _, _, res') = let nbgoals s = List.length (sig_it s) + nb_empty_evars (sig_sig s) in @@ -331,131 +334,104 @@ let compare (pri, _, _, (res, _)) (pri', _, _, (res', _)) = let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls } -let solve_tac (x : 'a tac) : 'a tac = - { skft = fun sk fk gls -> x.skft (fun ({it = gls},_ as res) fk -> - if gls = [] then sk res fk else fk ()) fk gls } - -let solve_unif_tac : atac = - { skft = fun sk fk {it = gl; sigma = s} -> - try let s' = Evarconv.consider_remaining_unif_problems (Global.env ()) s in - normevars_tac.skft sk fk ({it=gl; sigma=s'}) - with _ -> fk () } - let hints_tac hints = { skft = fun sk fk {it = gl,info; sigma = s} -> - let possible_resolve ((lgls,v) as res, pri, b, pp) = - (pri, pp, b, res) - in - let tacs = - let concl = gl.evar_concl in + let concl = Goal.V82.concl s gl in + let tacgl = {it = gl; sigma = s} in let poss = e_possible_resolve hints info.hints concl in - let l = - let tacgl = {it = gl; sigma = s} in - Util.list_map_append (fun (tac, pri, b, pptac) -> - try [tac tacgl, pri, b, pptac] with e when catchable e -> []) - poss - in - if l = [] && !typeclasses_debug then - msgnl (pr_depth info.auto_depth ++ str": no match for " ++ - Printer.pr_constr_env (Evd.evar_env gl) concl ++ - spc () ++ int (List.length poss) ++ str" possibilities"); - List.map possible_resolve l - in - let tacs = List.sort compare tacs in - let rec aux i = function - | (_, pp, b, ({it = gls; sigma = s}, v)) :: tl -> - 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); *) - aux (succ i) tl) + let rec aux i foundone = function + | (tac, _, b, name, pp) :: tl -> + let derivs = path_derivate info.auto_cut name in + let res = + try + if path_matches derivs [] then None else Some (tac tacgl) + with e when catchable e -> None in - let sgls = evars_to_goals (fun evm ev evi -> - if Typeclasses.is_resolvable evi && - (not info.only_classes || Typeclasses.is_class_evar evm evi) then - Typeclasses.mark_unresolvable evi, true - else evi, false) s - in - let nbgls, newgls, s' = - let gls' = List.map (fun g -> (None, g)) gls in - match sgls with - | None -> List.length gls', gls', s - | Some (evgls, s') -> - (List.length gls', gls' @ List.map (fun (ev, x) -> (Some ev, x)) evgls, s') - in - let gls' = list_map_i (fun j (evar, g) -> - let info = - { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp; - is_evar = evar; - hints = - if b && g.evar_hyps <> gl.evar_hyps - then make_autogoal_hints info.only_classes - ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'} - else info.hints } - in g, info) 1 newgls in - let glsv = {it = gls'; sigma = s'}, (fun _ pfl -> v (list_firstn nbgls pfl)) in - sk glsv fk - | [] -> fk () - in aux 1 tacs } - -let evars_of_term c = - let rec evrec acc c = - match kind_of_term c with - | Evar (n, _) -> Intset.add n acc - | _ -> fold_constr evrec acc c - in evrec Intset.empty c - -exception Found_evar of int - -let occur_evars evars c = - try - let rec evrec c = - match kind_of_term c with - | Evar (n, _) -> if Intset.mem n evars then raise (Found_evar n) else () - | _ -> iter_constr evrec c - in evrec c; false - with Found_evar _ -> true - -let dependent only_classes evd oev concl = - let concl_evars = Intset.union (evars_of_term concl) - (Option.cata Intset.singleton Intset.empty oev) - in not (Intset.is_empty concl_evars) + (match res with + | 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 " ++ Lazy.force pp); + aux (succ i) true tl) + in + let sgls = + evars_to_goals + (fun evm ev evi -> + if Typeclasses.is_resolvable evi && + (not info.only_classes || Typeclasses.is_class_evar evm evi) + then Typeclasses.mark_unresolvable evi, true + else evi, false) s' + in + let newgls, s' = + let gls' = List.map (fun g -> (None, g)) gls in + match sgls with + | None -> gls', s' + | Some (evgls, s') -> + (* Reorder with dependent subgoals. *) + (gls' @ List.map (fun (ev, x) -> Some ev, x) evgls, s') + in + let gls' = list_map_i + (fun j (evar, g) -> + let info = + { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp; + is_evar = evar; + 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; + auto_cut = derivs } + in g, info) 1 newgls in + let glsv = {it = gls'; sigma = s'} in + sk glsv fk) + | [] -> + if not foundone && !typeclasses_debug then + msgnl (pr_depth info.auto_depth ++ str": no match for " ++ + Printer.pr_constr_env (Goal.V82.env s gl) concl ++ + spc () ++ int (List.length poss) ++ str" possibilities"); + fk () + in aux 1 false poss } + +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 * validation) list) fk = function + let rec aux s (acc : autogoal list list) fk = function | (gl,info) :: gls -> - second.skft (fun ({it=gls';sigma=s'},v') fk' -> - let s', needs_backtrack = - if gls' = [] then - match info.is_evar with - | Some ev -> - let s' = - if Evd.is_defined s' ev then s' - else - let prf = v' s' [] in - let term, _ = Refiner.extract_open_proof s' prf in - Evd.define ev term s' - in s', dependent info.only_classes s' (Some ev) gl.evar_concl - | None -> s', dependent info.only_classes s' None gl.evar_concl - else s', 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' - in aux s' ((gls',v')::acc) fk'' gls) - fk {it = (gl,info); sigma = s} + (match info.is_evar with + | Some ev when Evd.is_defined s ev -> aux s acc fk gls + | _ -> + second.skft + (fun {it=gls';sigma=s'} fk' -> + let needs_backtrack = + if gls' = [] then + 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 ++ + 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) - in fun ({it = gls; sigma = s},v) fk -> + in fun {it = gls; sigma = s} fk -> let rec aux' = function | None -> fk () | Some (res, s', fk') -> - let goals' = List.concat (List.map (fun (gls,v) -> gls) res) in - let v' s' pfs' : proof_tree = - let (newpfs, rest) = List.fold_left (fun (newpfs,pfs') (gls,v) -> - let before, after = list_split_at (List.length gls) pfs' in - (v s' before :: newpfs, after)) - ([], pfs') res - in assert(rest = []); v s' (List.rev newpfs) - in sk ({it = goals'; sigma = s'}, v') (fun () -> aux' (fk' ())) + let goals' = List.concat res in + sk {it = goals'; sigma = s'} (fun () -> aux' (fk' ())) in aux' (aux s [] (fun () -> None) gls) let then_tac (first : atac) (second : atac) : atac = @@ -468,52 +444,68 @@ type run_list_res = (auto_result * run_list_res fk) option let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res = (then_list t (fun x fk -> Some (x, fk))) - (gl, fun s pfs -> valid goals p (ref s) pfs) + gl (fun _ -> None) +let fail_tac : atac = + { skft = fun sk fk _ -> fk () } + let rec fix (t : 'a tac) : 'a tac = then_tac t { skft = fun sk fk -> (fix t).skft sk fk } -let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) ev g = +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) 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 = match r with | None -> None - | Some ((gls, v), fk) -> - try ignore(v (sig_sig gls) []); assert(false) - with Found evm' -> Some (evm', fk) - -let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac = + | Some (gls, fk) -> Some (gls.sigma,fk) + +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 evm' evm, fk) + | Some (evm', fk) -> Some (evars_reset_evd ~with_conv_pbs:true evm' evm, fk) let eauto_tac hints = - fix (or_tac (then_tac normevars_tac (hints_tac hints)) intro_tac) - -let eauto ?(only_classes=true) ?st hints g = - let gl = { it = make_autogoal ~only_classes ?st None g; sigma = project g } in - match run_tac (eauto_tac hints) gl with + then_tac normevars_tac (or_tac (hints_tac hints) intro_tac) + +let eauto_tac ?limit hints = + match limit with + | None -> fix (eauto_tac 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 (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}, valid) -> - {it = List.map fst goals; sigma = s}, valid s + | Some {it = goals; sigma = s} -> + {it = List.map fst goals; sigma = s} -let real_eauto st hints p evd = +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 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 @@ -526,162 +518,209 @@ let real_eauto st hints p evd = | Some (evd', fk) -> aux evd' (fk :: fails) in aux evd [] -let resolve_all_evars_once debug (mode, depth) p evd = +let resolve_all_evars_once debug limit p evd = let db = searchtable_map typeclasses_db in - real_eauto (Hint_db.transparent_state db) [db] p evd + real_eauto ?limit (Hint_db.transparent_state db) [db] p evd + +(** We compute dependencies via a union-find algorithm. + Beware of the imperative effects on the partition structure, + it should not be shared, but only used locally. *) + +module Intpart = Unionfind.Make(Intset)(Intmap) -exception FoundTerm of constr +let deps_of_constraints cstrs evm p = + List.iter (fun (_, _, x, y) -> + let evx = Evarutil.undefined_evars_of_term evm x in + let evy = Evarutil.undefined_evars_of_term evm y in + Intpart.union_set (Intset.union evx evy) p) + cstrs + +let evar_dependencies evm p = + Evd.fold_undefined + (fun ev evi _ -> + let evars = Intset.add ev (Evarutil.undefined_evars_of_evar_info evm evi) + in Intpart.union_set evars p) + evm () let resolve_one_typeclass env ?(sigma=Evd.empty) gl = - let gls = { it = Evd.make_evar (Environ.named_context_val env) gl; sigma = sigma } in + let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env gl in + let (gl,t,sigma) = + Goal.V82.mk_goal sigma nc gl Store.empty in + let gls = { it = gl ; sigma = sigma } in let hints = searchtable_map typeclasses_db in - let gls', v = eauto ~st:(Hint_db.transparent_state hints) [hints] gls in - let term = v [] in + let gls' = eauto ?limit:!typeclasses_depth ~st:(Hint_db.transparent_state hints) [hints] gls in let evd = sig_sig gls' in - let term = fst (Refiner.extract_open_proof evd term) in - let term = Evarutil.nf_evar evd term in + let t' = let (ev, inst) = destEvar t in + mkEvar (ev, Array.of_list subst) + in + let term = Evarutil.nf_evar evd t' in evd, term let _ = Typeclasses.solve_instanciation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z) -let has_undefined p oevd evd = - Evd.fold (fun ev evi has -> has || - (evi.evar_body = Evar_empty && snd (p oevd ev evi))) - evd false - -let rec merge_deps deps = function - | [] -> [deps] - | hd :: tl -> - if intersects deps hd then - merge_deps (Intset.union deps hd) tl - else hd :: merge_deps deps tl - -let evars_of_evi evi = - Intset.union (evars_of_term evi.evar_concl) - (Intset.union - (match evi.evar_body with - | Evar_empty -> Intset.empty - | Evar_defined b -> evars_of_term b) - (Evarutil.evars_of_named_context (evar_filtered_context evi))) - -let deps_of_constraints cstrs deps = - List.fold_right (fun (_, _, x, y) deps -> - let evs = Intset.union (evars_of_term x) (evars_of_term y) in - merge_deps evs deps) - cstrs deps - -let evar_dependencies evm = - Evd.fold - (fun ev evi acc -> - merge_deps (Intset.union (Intset.singleton ev) - (evars_of_evi evi)) acc) - evm [] +(** [split_evars] returns groups of undefined evars according to dependencies *) let split_evars evm = - let _, cstrs = extract_all_conv_pbs evm in - let evmdeps = evar_dependencies evm in - let deps = deps_of_constraints cstrs evmdeps in - List.sort Intset.compare deps + let p = Intpart.create () in + evar_dependencies evm p; + deps_of_constraints (snd (extract_all_conv_pbs evm)) evm p; + Intpart.partition p + +(** [evars_in_comp] filters an [evar_map], keeping only evars + that belongs to a certain component *) -let select_evars evs evm = - Evd.fold (fun ev evi acc -> - if Intset.mem ev evs then Evd.add acc ev evi else acc) - evm Evd.empty +let evars_in_comp comp evm = + try + evars_reset_evd + (Intset.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev)) + comp Evd.empty) evm + with Not_found -> assert false -let is_inference_forced p ev evd = +let is_inference_forced p evd ev = try - let evi = Evd.find evd ev in - if evi.evar_body = Evar_empty then - if Typeclasses.is_resolvable evi - && snd (p ev evi) - then - let (loc, k) = evar_source ev evd in - match k with - | ImplicitArg (_, _, b) -> b - | QuestionMark _ -> false - | _ -> true - else true - else false - with Not_found -> true - -let is_optional p comp evd = - Intset.fold (fun ev acc -> - acc && not (is_inference_forced p ev evd)) - comp true + let evi = Evd.find_undefined evd ev in + if Typeclasses.is_resolvable evi && snd (p ev evi) + then + let (loc, k) = evar_source ev evd in + match k with + | ImplicitArg (_, _, b) -> b + | QuestionMark _ -> false + | _ -> true + else true + with Not_found -> assert false + +let is_mandatory p comp evd = + Intset.exists (is_inference_forced p evd) comp + +(** In case of unsatisfiable constraints, build a nice error message *) + +let error_unresolvable env comp do_split evd = + let evd = Evarutil.nf_evar_map_undefined evd in + let evm = if do_split then evars_in_comp comp evd else evd in + let _, ev = Evd.fold_undefined + (fun ev evi (b,acc) -> + (* focus on one instance if only one was searched for *) + if class_of_constr evi.evar_concl <> None then + if not b (* || do_split *) then + true, Some ev + else b, None + else b, acc) evm (false, None) + in + Typeclasses_errors.unsatisfiable_constraints + (Evarutil.nf_env_evar evm env) evm ev + +(** Check if an evar is concerned by the current resolution attempt, + (and in particular is in the current component), and also update + its evar_info. + Invariant : this should only be applied to undefined evars, + and return undefined evar_info *) + +let select_and_update_evars p oevd in_comp evd ev evi = + assert (evi.evar_body = Evar_empty); + try + let oevi = Evd.find_undefined oevd ev in + if Typeclasses.is_resolvable oevi then + Typeclasses.mark_unresolvable evi, + (in_comp ev && p evd ev evi) + else evi, false + with Not_found -> + Typeclasses.mark_unresolvable evi, p evd ev evi + +(** Do we still have unresolved evars that should be resolved ? *) + +let has_undefined p oevd evd = + Evd.fold_undefined (fun ev evi has -> has || + snd (p oevd ev evi)) + evd false + +(** If [do_split] is [true], we try to separate the problem in + several components and then solve them separately *) + +exception Unresolved let resolve_all_evars debug m env p oevd do_split fail = let split = if do_split then split_evars oevd else [Intset.empty] in - let p = if do_split then - fun comp evd ev evi -> - if evi.evar_body = Evar_empty then - (try let oevi = Evd.find oevd ev in - if Typeclasses.is_resolvable oevi then - Typeclasses.mark_unresolvable evi, (Intset.mem ev comp && - p evd ev evi) - else evi, false - with Not_found -> - Typeclasses.mark_unresolvable evi, p evd ev evi) - else evi, false - else fun _ evd ev evi -> - if evi.evar_body = Evar_empty then - try let oevi = Evd.find oevd ev in - if Typeclasses.is_resolvable oevi then - Typeclasses.mark_unresolvable evi, p evd ev evi - else evi, false - with Not_found -> - Typeclasses.mark_unresolvable evi, p evd ev evi - else evi, false - in - let rec aux p evd = - let evd' = resolve_all_evars_once debug m p evd in - if has_undefined p oevd evd' then None - else Some evd' + let in_comp comp ev = if do_split then Intset.mem ev comp else true in let rec docomp evd = function | [] -> evd | comp :: comps -> - let res = try aux (p comp) evd with Not_found -> None in - match res with - | None -> - if fail && (not do_split || not (is_optional (p comp evd) comp evd)) then - (* Unable to satisfy the constraints. *) - let evd = Evarutil.nf_evars evd in - let evm = if do_split then select_evars comp evd else evd in - let _, ev = Evd.fold - (fun ev evi (b,acc) -> - (* focus on one instance if only one was searched for *) - if class_of_constr evi.evar_concl <> None then - if not b (* || do_split *) then - true, Some ev - else b, None - else b, acc) evm (false, None) - in - Typeclasses_errors.unsatisfiable_constraints (Evarutil.nf_env_evar evm env) evm ev - else (* Best effort: do nothing *) oevd - | Some evd' -> docomp evd' comps + let p = select_and_update_evars p oevd (in_comp comp) in + try + let evd' = resolve_all_evars_once debug m p evd in + if has_undefined p oevd evd' then raise Unresolved; + docomp evd' comps + with Unresolved | Not_found -> + if fail && (not do_split || is_mandatory (p evd) comp evd) + then (* Unable to satisfy the constraints. *) + error_unresolvable env comp do_split evd + else (* Best effort: do nothing on this component *) + docomp evd comps in docomp oevd split -let resolve_typeclass_evars d p env evd onlyargs split fail = - let pred = - if onlyargs then - (fun evd ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) && - Typeclasses.is_class_evar evd evi) - else (fun evd ev evi -> Typeclasses.is_class_evar evd evi) - in resolve_all_evars d p env pred evd split fail +let initial_select_evars onlyargs = + if onlyargs then + (fun evd ev evi -> + Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) + && Typeclasses.is_class_evar evd evi) + else + (fun evd ev evi -> Typeclasses.is_class_evar evd evi) + +let resolve_typeclass_evars debug m env evd onlyargs 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 onlyargs) evd split fail -let solve_inst debug mode depth env evd onlyargs split fail = - resolve_typeclass_evars debug (mode, depth) env evd onlyargs split fail +let solve_inst debug depth env evd onlyargs split fail = + resolve_typeclass_evars debug depth env evd onlyargs split fail let _ = Typeclasses.solve_instanciations_problem := - solve_inst false true default_eauto_depth + solve_inst false !typeclasses_depth + + +(** Options: depth, debug and transparency settings. *) + +open Goptions + +let set_typeclasses_debug d = (:=) typeclasses_debug d; + Typeclasses.solve_instanciations_problem := solve_inst d !typeclasses_depth + +let get_typeclasses_debug () = !typeclasses_debug + +let set_typeclasses_debug = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "debug output for typeclasses proof search"; + optkey = ["Typeclasses";"Debug"]; + optread = get_typeclasses_debug; + optwrite = set_typeclasses_debug; } + + +let set_typeclasses_depth d = (:=) typeclasses_depth d; + Typeclasses.solve_instanciations_problem := solve_inst !typeclasses_debug !typeclasses_depth + +let get_typeclasses_depth () = !typeclasses_depth + +let set_typeclasses_depth = + declare_int_option + { optsync = true; + optdepr = false; + optname = "depth for typeclasses proof search"; + optkey = ["Typeclasses";"Depth"]; + optread = get_typeclasses_depth; + optwrite = set_typeclasses_depth; } let set_transparency cl b = List.iter (fun r -> let gr = Smartlocate.global_with_alias r in let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in - Classes.set_typeclass_transparency ev b) cl + Classes.set_typeclass_transparency ev false b) cl VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings | [ "Typeclasses" "Transparent" reference_list(cl) ] -> [ @@ -704,18 +743,6 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug | [ ] -> [ false ] END -let pr_mode _prc _prlc _prt m = - match m with - Some b -> - if b then Pp.str "depth-first" else Pp.str "breadth-fist" - | None -> Pp.mt() - -ARGUMENT EXTEND search_mode TYPED AS bool option PRINTED BY pr_mode -| [ "dfs" ] -> [ Some true ] -| [ "bfs" ] -> [ Some false ] -| [] -> [ None ] -END - let pr_depth _prc _prlc _prt = function Some i -> Util.pr_int i | None -> Pp.mt() @@ -724,13 +751,12 @@ ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth | [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ] END +(* true = All transparent, false = Opaque if possible *) + VERNAC COMMAND EXTEND Typeclasses_Settings - | [ "Typeclasses" "eauto" ":=" debug(d) search_mode(s) depth(depth) ] -> [ - typeclasses_debug := d; - let mode = match s with Some t -> t | None -> true in - let depth = match depth with Some i -> i | None -> default_eauto_depth in - Typeclasses.solve_instanciations_problem := - solve_inst d mode depth + | [ "Typeclasses" "eauto" ":=" debug(d) depth(depth) ] -> [ + set_typeclasses_debug d; + set_typeclasses_depth depth ] END @@ -738,8 +764,8 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl try let dbs = list_map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in - eauto ~only_classes ~st dbs gl - with Not_found -> tclFAIL 0 (str" typeclasses eauto failed") gl + eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl + with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl TACTIC EXTEND typeclasses_eauto | [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ typeclasses_eauto l ] |