From c4d62e3686926c27b172636ca8b746814d13a462 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 23:34:07 +0100 Subject: Moving type_uconstr to Pretyping. --- intf/tacexpr.mli | 2 +- ltac/eauto.ml | 2 +- ltac/extratactics.ml4 | 4 ++-- ltac/g_auto.ml4 | 2 +- ltac/tacinterp.ml | 18 ------------------ ltac/tacinterp.mli | 5 ----- pretyping/pretyping.ml | 25 +++++++++++++++++++++++++ pretyping/pretyping.mli | 8 ++++++++ 8 files changed, 38 insertions(+), 28 deletions(-) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index b1dc174d4b..0aa3b936ca 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -122,7 +122,7 @@ type open_glob_constr = unit * glob_constr_and_expr type binding_bound_vars = Id.Set.t type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern -type 'a delayed_open = +type 'a delayed_open = 'a Pretyping.delayed_open = { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open diff --git a/ltac/eauto.ml b/ltac/eauto.ml index 0449467598..9cfb805d4c 100644 --- a/ltac/eauto.ml +++ b/ltac/eauto.ml @@ -60,7 +60,7 @@ let eval_uconstrs ist cs = fail_evar = false; expand_evars = true } in - List.map (fun c -> Tacinterp.type_uconstr ~flags ist c) cs + List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs (************************************************************************) (* PROLOG tactic *) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 23aa8dcb47..96abc11999 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -44,7 +44,7 @@ let with_delayed_uconstr ist c tac = fail_evar = false; expand_evars = true } in - let c = Tacinterp.type_uconstr ~flags ist c in + let c = Pretyping.type_uconstr ~flags ist c in Tacticals.New.tclDELAYEDWITHHOLES false c tac let replace_in_clause_maybe_by ist c1 c2 cl tac = @@ -368,7 +368,7 @@ let refine_tac ist simple c = let env = Proofview.Goal.env gl in let flags = Pretyping.all_no_fail_flags in let expected_type = Pretyping.OfType concl in - let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in + let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> c.delayed env sigma } in let refine = Refine.refine ~unsafe:false update in if simple then refine diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index 788443944f..bc98b7d6d4 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -48,7 +48,7 @@ let eval_uconstrs ist cs = fail_evar = false; expand_evars = true } in - List.map (fun c -> Tacinterp.type_uconstr ~flags ist c) cs + List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ()) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 4506f81596..4c74984f83 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -723,24 +723,6 @@ let interp_open_constr_list = let pf_interp_type ist env sigma = interp_type ist env sigma -(* Fully evaluate an untyped constr *) -let type_uconstr ?(flags = constr_flags) - ?(expected_type = WithoutTypeConstraint) ist c = - { delayed = begin fun env sigma -> - let open Pretyping in - let { closure; term } = c in - let vars = { - ltac_constrs = closure.typed; - ltac_uconstrs = closure.untyped; - ltac_idents = closure.idents; - ltac_genargs = ist.lfun; - } in - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = understand_ltac flags env sigma vars expected_type term in - Sigma.Unsafe.of_pair (c, sigma) - end } - - (* Interprets a reduction expression *) let interp_unfold ist env sigma (occs,qid) = (interp_occurrences ist occs,interp_evaluable ist env sigma qid) diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli index 31327873e9..92f12fc8f7 100644 --- a/ltac/tacinterp.mli +++ b/ltac/tacinterp.mli @@ -64,11 +64,6 @@ val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tac (** Interprets an expression that evaluates to a constr *) val interp_ltac_constr : interp_sign -> glob_tactic_expr -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic -val type_uconstr : - ?flags:Pretyping.inference_flags -> - ?expected_type:Pretyping.typing_constraint -> - interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open - (** Interprets redexp arguments *) val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a765d30913..8baa668c7b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -58,6 +58,8 @@ type ltac_var_map = { } type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr +type 'a delayed_open = + { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } (************************************************************************) (* This concerns Cases *) @@ -1107,3 +1109,26 @@ let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=W let understand_ltac flags env sigma lvar kind c = ise_pretype_gen flags env sigma lvar kind c + +let constr_flags = { + use_typeclasses = true; + use_unif_heuristics = true; + use_hook = None; + fail_evar = true; + expand_evars = true } + +(* Fully evaluate an untyped constr *) +let type_uconstr ?(flags = constr_flags) + ?(expected_type = WithoutTypeConstraint) ist c = + { delayed = begin fun env sigma -> + let { closure; term } = c in + let vars = { + ltac_constrs = closure.typed; + ltac_uconstrs = closure.untyped; + ltac_idents = closure.idents; + ltac_genargs = ist.Geninterp.lfun; + } in + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = understand_ltac flags env sigma vars expected_type term in + Sigma.Unsafe.of_pair (c, sigma) + end } diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 4c4c535d8c..91320f20a5 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -55,6 +55,9 @@ type inference_flags = { expand_evars : bool } +type 'a delayed_open = + { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } + val default_inference_flags : bool -> inference_flags val no_classes_no_fail_inference_flags : inference_flags @@ -114,6 +117,11 @@ val understand_judgment : env -> evar_map -> val understand_judgment_tcc : env -> evar_map ref -> glob_constr -> unsafe_judgment +val type_uconstr : + ?flags:inference_flags -> + ?expected_type:typing_constraint -> + Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open + (** Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver hook depending on given flags. *) -- cgit v1.2.3 From 9d5ddf9608d110498cc3c259c11cf6958a1a0d2e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Mar 2016 09:28:08 +0100 Subject: Moving Eauto and Class_tactics to tactics/. --- ltac/class_tactics.ml | 903 ---------------------------------------------- ltac/class_tactics.mli | 32 -- ltac/eauto.ml | 526 --------------------------- ltac/eauto.mli | 33 -- ltac/ltac.mllib | 2 - tactics/class_tactics.ml | 903 ++++++++++++++++++++++++++++++++++++++++++++++ tactics/class_tactics.mli | 32 ++ tactics/eauto.ml | 526 +++++++++++++++++++++++++++ tactics/eauto.mli | 33 ++ tactics/tactics.mllib | 2 + 10 files changed, 1496 insertions(+), 1496 deletions(-) delete mode 100644 ltac/class_tactics.ml delete mode 100644 ltac/class_tactics.mli delete mode 100644 ltac/eauto.ml delete mode 100644 ltac/eauto.mli create mode 100644 tactics/class_tactics.ml create mode 100644 tactics/class_tactics.mli create mode 100644 tactics/eauto.ml create mode 100644 tactics/eauto.mli diff --git a/ltac/class_tactics.ml b/ltac/class_tactics.ml deleted file mode 100644 index 4855598989..0000000000 --- a/ltac/class_tactics.ml +++ /dev/null @@ -1,903 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - if Evar.Map.mem ev !tosee then - visit ev (Evar.Map.find ev !tosee)) evs; - tosee := Evar.Map.remove ev !tosee; - l' := ev :: !l'; - in - while not (Evar.Map.is_empty !tosee) do - let ev, evi = Evar.Map.min_binding !tosee in - visit ev evi - done; - List.rev !l' - -let evars_to_goals p evm = - let goals = ref Evar.Map.empty in - let map ev evi = - let evi, goal = p evm ev evi in - let () = if goal then goals := Evar.Map.add ev evi !goals in - evi - in - let evm = Evd.raw_map_undefined map evm in - if Evar.Map.is_empty !goals then None - else Some (!goals, evm) - -(** Typeclasses instance search tactic / eauto *) - -open Auto - -open Unification - -let auto_core_unif_flags st freeze = { - modulo_conv_on_closed_terms = Some st; - use_metas_eagerly_in_conv_on_closed_terms = true; - use_evars_eagerly_in_conv_on_closed_terms = false; - modulo_delta = st; - modulo_delta_types = st; - check_applied_meta_types = false; - use_pattern_unification = true; - use_meta_bound_pattern_unification = true; - frozen_evars = freeze; - restrict_conv_on_strict_subterms = false; (* ? *) - modulo_betaiota = true; - modulo_eta = !typeclasses_modulo_eta; -} - -let auto_unif_flags freeze st = - let fl = auto_core_unif_flags st freeze in - { core_unify_flags = fl; - merge_unify_flags = fl; - subterm_unify_flags = fl; - allow_K_in_toplevel_higher_order_unification = false; - resolve_evars = false -} - -let rec eq_constr_mod_evars x y = - match kind_of_term x, kind_of_term y with - | Evar (e1, l1), Evar (e2, l2) when not (Evar.equal e1 e2) -> true - | _, _ -> compare_constr eq_constr_mod_evars x y - -let progress_evars t = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let concl = Proofview.Goal.concl gl in - let check = - Proofview.Goal.nf_enter { enter = begin fun gl' -> - let newconcl = Proofview.Goal.concl gl' in - if eq_constr_mod_evars concl newconcl - then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)") - else Proofview.tclUNIT () - end } - in t <*> check - end } - - -let e_give_exact flags poly (c,clenv) gl = - let (c, _, _) = c in - let c, gl = - if poly then - let clenv', subst = Clenv.refresh_undefined_univs clenv in - let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in - let c = Vars.subst_univs_level_constr subst c in - c, {gl with sigma = evd} - else c, gl - in - let t1 = pf_unsafe_type_of gl c in - tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl - -let unify_e_resolve poly flags = { enter = begin fun gls (c,clenv) -> - let clenv', c = connect_hint_clenv poly c clenv gls in - let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in - Clenvtac.clenv_refine true ~with_classes:false clenv' - end } - -let unify_resolve poly flags = { enter = begin fun gls (c,clenv) -> - let clenv', _ = connect_hint_clenv poly c clenv gls in - let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in - Clenvtac.clenv_refine false ~with_classes:false clenv' - end } - -let clenv_of_prods poly nprods (c, clenv) gl = - let (c, _, _) = c in - if poly || Int.equal nprods 0 then Some clenv - else - let ty = Tacmach.New.pf_unsafe_type_of gl c in - let diff = nb_prod ty - nprods in - if Pervasives.(>=) diff 0 then - (* Was Some clenv... *) - Some (Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl) - else None - -let with_prods nprods poly (c, clenv) f = - Proofview.Goal.nf_enter { enter = begin fun gl -> - match clenv_of_prods poly nprods (c, clenv) gl with - | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses") - | Some clenv' -> f.enter gl (c, clenv') - end } - -(** Hack to properly solve dependent evars that are typeclasses *) - -let rec e_trivial_fail_db db_list local_db goal = - let tacl = - Proofview.V82.of_tactic Eauto.registered_e_assumption :: - (tclTHEN (Proofview.V82.of_tactic Tactics.intro) - (function g'-> - let d = pf_last_hyp g' in - let hintl = make_resolve_hyp (pf_env g') (project g') d in - (e_trivial_fail_db db_list - (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) :: - (List.map (fun (x,_,_,_,_) -> x) - (e_trivial_resolve db_list local_db (project goal) (pf_concl goal))) - in - tclFIRST (List.map tclCOMPLETE tacl) goal - -and e_my_find_search db_list local_db hdc complete sigma concl = - let prods, concl = decompose_prod_assum concl in - let nprods = List.length prods in - let freeze = - try - let cl = Typeclasses.class_info (fst hdc) in - if cl.cl_strict then - Evd.evars_of_term concl - else Evar.Set.empty - with e when Errors.noncritical e -> Evar.Set.empty - in - let hintl = - List.map_append - (fun db -> - let tacs = - if Hint_db.use_dn db then (* Using dnet *) - Hint_db.map_eauto hdc concl db - else Hint_db.map_existential hdc concl db - in - let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in - List.map (fun x -> (flags, x)) tacs) - (local_db::db_list) - in - let tac_of_hint = - fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) -> - let tac = function - | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags) - | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags) - | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c) - | Res_pf_THEN_trivial_fail (term,cl) -> - Proofview.V82.tactic (tclTHEN - (Proofview.V82.of_tactic ((with_prods nprods poly (term,cl) (unify_e_resolve poly flags)))) - (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)) - | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c]))) - | Extern tacast -> conclPattern concl p tacast - in - let tac = Proofview.V82.of_tactic (run_hint t tac) in - let tac = if complete then tclCOMPLETE tac else tac in - match repr_hint t with - | Extern _ -> (tac,b,true, name, lazy (pr_hint t)) - | _ -> -(* let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *) - (tac,b,false, name, lazy (pr_hint t)) - in List.map tac_of_hint hintl - -and e_trivial_resolve db_list local_db sigma concl = - try - e_my_find_search db_list local_db - (decompose_app_bound concl) true sigma concl - with Bound | Not_found -> [] - -let e_possible_resolve db_list local_db sigma concl = - try - e_my_find_search db_list local_db - (decompose_app_bound concl) false sigma concl - with Bound | Not_found -> [] - -let catchable = function - | Refiner.FailError _ -> true - | e -> Logic.catchable_exception e - -let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) evs (Evarutil.nf_evar evs (Goal.V82.concl evs ev)) - -let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l) - -type autoinfo = { hints : hint_db; is_evar: existential_key option; - only_classes: bool; unique : 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 failure = NotApplicable | ReachedLimit -type 'ans fk = failure -> '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 - -type atac = auto_result tac - -(* Some utility types to avoid the need of -rectypes *) - -type 'a optionk = - | Nonek - | Somek of 'a * 'a optionk fk - -type ('a,'b) optionk2 = - | Nonek2 of failure - | Somek2 of 'a * 'b * ('a,'b) optionk2 fk - -let make_resolve_hyp env sigma st flags only_classes pri decl = - let open Context.Named.Declaration in - let id = get_id decl in - let cty = Evarutil.nf_evar sigma (get_type decl) in - let rec iscl env ty = - let ctx, ar = decompose_prod_assum ty in - match kind_of_term (fst (decompose_app ar)) with - | Const (c,_) -> is_class (ConstRef c) - | Ind (i,_) -> is_class (IndRef i) - | _ -> - let env' = Environ.push_rel_context ctx env in - let ty' = whd_betadeltaiota env' ar in - if not (Term.eq_constr ty' ar) then iscl env' ty' - else false - in - 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 (path,pri, c) -> make_resolves env sigma ~name:(PathHints path) - (true,false,Flags.is_verbose()) pri false - (IsConstr (c,Univ.ContextSet.empty))) - hints) - else [] - in - (hints @ List.map_filter - (fun f -> try Some (f (c, cty, Univ.ContextSet.empty)) - with Failure _ | UserError _ -> None) - [make_exact_entry ~name env sigma pri false; - make_apply_entry ~name env sigma flags pri false]) - else [] - -let pf_filtered_hyps 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 -> - let consider = - let open Context.Named.Declaration in - try let t = Global.lookup_named (get_id hyp) |> get_type in - (* Section variable, reindex only if the type changed *) - not (Term.eq_constr t (get_type hyp)) - with Not_found -> true - in - if consider then - let path, hint = - PathEmpty, pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp - in - (PathOr (paths, path), hint @ hints) - else (paths, hints)) - (PathEmpty, []) sign - in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true) - -let make_autogoal_hints = - let cache = ref (true, Environ.empty_named_context_val, - Hint_db.empty full_transparent_state true) - in - fun only_classes ?(st=full_transparent_state) g -> - let sign = pf_filtered_hyps g in - let (onlyc, sign', cached_hints) = !cache in - if onlyc == only_classes && - (sign == sign' || Environ.eq_named_context_val sign sign') - && Hint_db.transparent_state cached_hints == st - then - cached_hints - else - let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in - cache := (only_classes, 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 -> sk (f gls hints) fk - | None -> fk NotApplicable } - -let intro_tac : atac = - lift_tactic (Proofview.V82.of_tactic Tactics.intro) - (fun {it = gls; sigma = s} info -> - let gls' = - List.map (fun g' -> - 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 context) in - let ldb = Hint_db.add_list env s 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 = - { 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 } - -let merge_failures x y = - match x, y with - | _, ReachedLimit - | ReachedLimit, _ -> ReachedLimit - | NotApplicable, NotApplicable -> NotApplicable - -let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = - { skft = fun sk fk gls -> x.skft sk - (fun f -> y.skft sk (fun f' -> fk (merge_failures f f')) gls) gls } - -let or_else_tac (x : 'a tac) (y : failure -> 'a tac) : 'a tac = - { skft = fun sk fk gls -> x.skft sk - (fun f -> (y f).skft sk fk gls) gls } - -let is_Prop env sigma concl = - let ty = Retyping.get_type_of env sigma concl in - match kind_of_term ty with - | Sort (Prop Null) -> true - | _ -> false - -let is_unique env concl = - try - let (cl,u), args = dest_class_app env concl in - cl.cl_unique - with e when Errors.noncritical e -> false - -let needs_backtrack env evd oev concl = - if Option.is_empty oev || is_Prop env evd concl then - occur_existential concl - else true - -let hints_tac hints = - { skft = fun sk fk {it = gl,info; sigma = s;} -> - let env = Goal.V82.env s gl in - let concl = Goal.V82.concl s gl in - let tacgl = {it = gl; sigma = s;} in - let poss = e_possible_resolve hints info.hints s concl in - let unique = is_unique env concl in - 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 - (match res with - | None -> aux i foundone tl - | Some {it = gls; sigma = s';} -> - if !typeclasses_debug then - msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp - ++ str" on" ++ spc () ++ pr_ev s gl); - let sgls = - evars_to_goals - (fun evm ev evi -> - if Typeclasses.is_resolvable evi && not (Evd.is_undefined s ev) && - (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') -> - if not !typeclasses_dependency_order then - (gls' @ List.map (fun (ev,_) -> (Some ev, ev)) (Evar.Map.bindings evgls), s') - else - (* Reorder with dependent subgoals. *) - let evm = List.fold_left - (fun acc g -> Evar.Map.add g (Evd.find_undefined s' g) acc) evgls gls in - let gls = top_sort s' evm in - (List.map (fun ev -> Some ev, ev) gls, 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 - let fk' = - (fun e -> - let do_backtrack = - if unique then occur_existential concl - else if info.unique then true - else if List.is_empty gls' then - needs_backtrack env s' info.is_evar concl - else true - in - let e' = match foundone with None -> e | Some e' -> merge_failures e e' in - if !typeclasses_debug then - msg_debug - ((if do_backtrack then str"Backtracking after " - else str "Not backtracking after ") - ++ Lazy.force pp); - if do_backtrack then aux (succ i) (Some e') tl - else fk e') - in - sk glsv fk') - | [] -> - if foundone == None && !typeclasses_debug then - msg_debug (pr_depth info.auto_depth ++ str": no match for " ++ - Printer.pr_constr_env (Goal.V82.env s gl) s concl ++ - spc () ++ str ", " ++ int (List.length poss) ++ str" possibilities"); - match foundone with - | Some e -> fk e - | None -> fk NotApplicable - in aux 1 None poss } - -let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk = - let rec aux s (acc : autogoal list list) fk = function - | (gl,info) :: gls -> - Control.check_for_interrupt (); - (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 fk'' = - if not info.unique && List.is_empty gls' && - not (needs_backtrack (Goal.V82.env s gl) s - info.is_evar (Goal.V82.concl s gl)) - then fk - else fk' - in - aux s' (gls'::acc) fk'' gls) - fk {it = (gl,info); sigma = s; }) - | [] -> Somek2 (List.rev acc, s, fk) - in fun {it = gls; sigma = s; } fk -> - let rec aux' = function - | Nonek2 e -> fk e - | Somek2 (res, s', fk') -> - let goals' = List.concat res in - sk {it = goals'; sigma = s'; } (fun e -> aux' (fk' e)) - in aux' (aux s [] (fun e -> Nonek2 e) gls) - -let then_tac (first : atac) (second : atac) : atac = - { skft = fun sk fk -> first.skft (then_list second sk) fk } - -let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option = - t.skft (fun x _ -> Some x) (fun _ -> None) gl - -type run_list_res = auto_result optionk - -let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res = - (then_list t (fun x fk -> Somek (x, fk))) - gl - (fun _ -> Nonek) - -let fail_tac reason : atac = - { skft = fun sk fk _ -> fk reason } - -let rec fix (t : 'a tac) : 'a tac = - then_tac t { skft = fun sk fk -> (fix t).skft sk fk } - -let rec fix_limit limit (t : 'a tac) : 'a tac = - if Int.equal limit 0 then fail_tac ReachedLimit - else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk } - -let fix_iterative t = - let rec aux depth = - or_else_tac (fix_limit depth t) - (function - | NotApplicable as e -> fail_tac e - | ReachedLimit -> aux (succ depth)) - in aux 1 - -let fix_iterative_limit limit (t : 'a tac) : 'a tac = - let rec aux depth = - if Int.equal depth limit then fail_tac ReachedLimit - else or_tac (fix_limit depth t) { skft = fun sk fk -> (aux (succ depth)).skft sk fk } - in aux 1 - -let make_autogoal ?(only_classes=true) ?(unique=false) ?(st=full_transparent_state) cut ev g = - let hints = make_autogoal_hints only_classes ~st g in - (g.it, { hints = hints ; is_evar = ev; unique = unique; - only_classes = only_classes; auto_depth = []; auto_last_tac = lazy (str"none"); - auto_path = []; auto_cut = cut }) - - -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) ?(unique=false) - ?(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 ~unique - ~st cut (Some g) {it = g; sigma = evm'; } in - (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm'; } - -let get_result r = - match r with - | Nonek -> None - | Somek (gls, fk) -> Some (gls.sigma,fk) - -let run_on_evars ?(only_classes=true) ?(unique=false) ?(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 goals = - if !typeclasses_dependency_order then - top_sort evm' goals - else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals) - in - let res = run_list_tac tac p goals - (make_autogoals ~only_classes ~unique ~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 ~with_univs:false evm' evm, fk) - -let eauto_tac hints = - then_tac normevars_tac (or_tac (hints_tac hints) intro_tac) - -let eauto_tac ?limit hints = - if get_typeclasses_iterative_deepening () then - match limit with - | None -> fix_iterative (eauto_tac hints) - | Some limit -> fix_iterative_limit limit (eauto_tac hints) - else - match limit with - | None -> fix (eauto_tac hints) - | Some limit -> fix_limit limit (eauto_tac hints) - -let real_eauto ?limit unique st hints p evd = - let res = - run_on_evars ~st ~unique p evd hints (eauto_tac ?limit hints) - in - match res with - | None -> evd - | Some (evd', fk) -> - if unique then - (match get_result (fk NotApplicable) with - | Some (evd'', fk') -> error "Typeclass resolution gives multiple solutions" - | None -> evd') - else evd' - -let resolve_all_evars_once debug limit unique p evd = - let db = searchtable_map typeclasses_db in - real_eauto ?limit unique (Hint_db.transparent_state db) [db] p evd - -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; } -> - {it = List.map fst goals; sigma = s;} - -(** 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(Evar.Set)(Evar.Map) - -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 (Evar.Set.union evx evy) p) - cstrs - -let evar_dependencies evm p = - Evd.fold_undefined - (fun ev evi _ -> - let evars = Evar.Set.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 unique = - 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' = eauto ?limit:!typeclasses_depth ~st:(Hint_db.transparent_state hints) [hints] gls in - let evd = sig_sig gls' 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_instantiation_problem := - (fun x y z w -> resolve_one_typeclass x ~sigma:y z w) - -(** [split_evars] returns groups of undefined evars according to dependencies *) - -let split_evars evm = - let p = Intpart.create () in - evar_dependencies evm p; - deps_of_constraints (snd (extract_all_conv_pbs evm)) evm p; - Intpart.partition p - -let is_inference_forced p evd ev = - try - 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 - | Evar_kinds.ImplicitArg (_, _, b) -> b - | Evar_kinds.QuestionMark _ -> false - | _ -> true - else true - with Not_found -> assert false - -let is_mandatory p comp evd = - Evar.Set.exists (is_inference_forced p evd) comp - -(** In case of unsatisfiable constraints, build a nice error message *) - -let error_unresolvable env comp evd = - let evd = Evarutil.nf_evar_map_undefined evd in - let is_part ev = match comp with - | None -> true - | Some s -> Evar.Set.mem ev s - in - let fold ev evi (found, accu) = - let ev_class = class_of_constr evi.evar_concl in - if not (Option.is_empty ev_class) && is_part ev then - (* focus on one instance if only one was searched for *) - if not found then (true, Some ev) - else (found, None) - else (found, accu) - in - let (_, ev) = Evd.fold_undefined fold evd (true, None) in - Pretype_errors.unsatisfiable_constraints - (Evarutil.nf_env_evar evd env) evd ev comp - -(** 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 = - let check ev evi = snd (p oevd ev evi) in - Evar.Map.exists check (Evd.undefined_map evd) - -(** Revert the resolvability status of evars after resolution, - potentially unprotecting some evars that were set unresolvable - just for this call to resolution. *) - -let revert_resolvability oevd evd = - let map ev evi = - try - if not (Typeclasses.is_resolvable evi) then - let evi' = Evd.find_undefined oevd ev in - if Typeclasses.is_resolvable evi' then - Typeclasses.mark_resolvable evi - else evi - else evi - with Not_found -> evi - in - Evd.raw_map_undefined map evd - -(** 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 unique env p oevd do_split fail = - let split = if do_split then split_evars oevd else [Evar.Set.empty] in - let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true - in - let rec docomp evd = function - | [] -> revert_resolvability oevd evd - | comp :: comps -> - let p = select_and_update_evars p oevd (in_comp comp) in - try - let evd' = resolve_all_evars_once debug m unique 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. *) - let comp = if do_split then Some comp else None in - error_unresolvable env comp evd - else (* Best effort: do nothing on this component *) - docomp evd comps - in docomp oevd split - -let initial_select_evars filter = - fun evd ev evi -> - filter ev (snd evi.Evd.evar_source) && - Typeclasses.is_class_evar evd evi - -let resolve_typeclass_evars debug m unique env evd filter split fail = - let evd = - try Evarconv.consider_remaining_unif_problems - ~ts:(Typeclasses.classes_transparent_state ()) env evd - with e when Errors.noncritical e -> evd - in - resolve_all_evars debug m unique env (initial_select_evars filter) evd split fail - -let solve_inst debug depth env evd filter unique split fail = - resolve_typeclass_evars debug depth unique env evd filter split fail - -let _ = - Typeclasses.solve_instantiations_problem := - solve_inst false !typeclasses_depth - -let set_typeclasses_debug d = (:=) typeclasses_debug d; - Typeclasses.solve_instantiations_problem := solve_inst d !typeclasses_depth - -let get_typeclasses_debug () = !typeclasses_debug - -let set_typeclasses_depth d = (:=) typeclasses_depth d; - Typeclasses.solve_instantiations_problem := solve_inst !typeclasses_debug !typeclasses_depth - -let get_typeclasses_depth () = !typeclasses_depth - -open Goptions - -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 = - 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 typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl = - try - let dbs = List.map_filter - (fun db -> try Some (searchtable_map db) - with e when Errors.noncritical e -> None) - dbs - in - let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in - eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl - with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl - -(** Take the head of the arity of a constr. - Used in the partial application tactic. *) - -let rec head_of_constr t = - let t = strip_outer_cast(collapse_appl t) in - match kind_of_term t with - | Prod (_,_,c2) -> head_of_constr c2 - | LetIn (_,_,_,c2) -> head_of_constr c2 - | App (f,args) -> head_of_constr f - | _ -> t - -let head_of_constr h c = - let c = head_of_constr c in - letin_tac None (Name h) c None Locusops.allHyps - -let not_evar c = match kind_of_term c with -| Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar") -| _ -> Proofview.tclUNIT () - -let is_ground c gl = - if Evarutil.is_ground_term (project gl) c then tclIDTAC gl - else tclFAIL 0 (str"Not ground") gl - -let autoapply c i gl = - let flags = auto_unif_flags Evar.Set.empty - (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in - let cty = pf_unsafe_type_of gl c in - let ce = mk_clenv_from gl (c,cty) in - let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl ((c,cty,Univ.ContextSet.empty),ce) } in - Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl diff --git a/ltac/class_tactics.mli b/ltac/class_tactics.mli deleted file mode 100644 index f1bcfa7dd4..0000000000 --- a/ltac/class_tactics.mli +++ /dev/null @@ -1,32 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* bool - -val set_typeclasses_debug : bool -> unit -val get_typeclasses_debug : unit -> bool - -val set_typeclasses_depth : int option -> unit -val get_typeclasses_depth : unit -> int option - -val progress_evars : unit Proofview.tactic -> unit Proofview.tactic - -val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> - Hints.hint_db_name list -> tactic - -val head_of_constr : Id.t -> Term.constr -> unit Proofview.tactic - -val not_evar : constr -> unit Proofview.tactic - -val is_ground : constr -> tactic - -val autoapply : constr -> Hints.hint_db_name -> tactic diff --git a/ltac/eauto.ml b/ltac/eauto.ml deleted file mode 100644 index 9cfb805d4c..0000000000 --- a/ltac/eauto.ml +++ /dev/null @@ -1,526 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let t1 = Tacmach.New.pf_unsafe_type_of gl c in - let t2 = Tacmach.New.pf_concl gl in - if occur_existential t1 || occur_existential t2 then - Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c)) - else exact_check c - end } - -let assumption id = e_give_exact (mkVar id) - -let e_assumption = - Proofview.Goal.enter { enter = begin fun gl -> - Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl)) - end } - -let registered_e_assumption = - Proofview.Goal.enter { enter = begin fun gl -> - Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id)) - (Tacmach.New.pf_ids_of_hyps gl)) - end } - -let eval_uconstrs ist cs = - let flags = { - Pretyping.use_typeclasses = false; - use_unif_heuristics = true; - use_hook = Some Pfedit.solve_by_implicit_tactic; - fail_evar = false; - expand_evars = true - } in - List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs - -(************************************************************************) -(* PROLOG tactic *) -(************************************************************************) - -(*s Tactics handling a list of goals. *) - -(* first_goal : goal list sigma -> goal sigma *) - -let first_goal gls = - let gl = gls.Evd.it and sig_0 = gls.Evd.sigma in - if List.is_empty gl then error "first_goal"; - { Evd.it = List.hd gl; Evd.sigma = sig_0; } - -(* tactic -> tactic_list : Apply a tactic to the first goal in the list *) - -let apply_tac_list tac glls = - let (sigr,lg) = unpackage glls in - match lg with - | (g1::rest) -> - let gl = apply_sig_tac sigr tac g1 in - repackage sigr (gl@rest) - | _ -> error "apply_tac_list" - -let one_step l gl = - [Proofview.V82.of_tactic Tactics.intro] - @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl))) - @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l) - @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl)) - -let rec prolog l n gl = - if n <= 0 then error "prolog - failure"; - let prol = (prolog l (n-1)) in - (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl - -let out_term = function - | IsConstr (c, _) -> c - | IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr) - -let prolog_tac l n = - Proofview.V82.tactic begin fun gl -> - let map c = - let (c, sigma) = Tactics.run_delayed (pf_env gl) (project gl) c in - let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in - out_term c - in - let l = List.map map l in - try (prolog l n gl) - with UserError ("Refiner.tclFIRST",_) -> - errorlabstrm "Prolog.prolog" (str "Prolog failed.") - end - -open Auto -open Unification - -(***************************************************************************) -(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) -(***************************************************************************) - -let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l) - -let unify_e_resolve poly flags (c,clenv) = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let clenv', c = connect_hint_clenv poly c clenv gl in - Proofview.V82.tactic - (fun gls -> - let clenv' = clenv_unique_resolver ~flags clenv' gls in - tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) - (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls) - end } - -let hintmap_of hdc concl = - match hdc with - | None -> fun db -> Hint_db.map_none db - | Some hdc -> - if occur_existential concl then (fun db -> Hint_db.map_existential hdc concl db) - else (fun db -> Hint_db.map_auto hdc concl db) - (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) - -let e_exact poly flags (c,clenv) = - let (c, _, _) = c in - let clenv', subst = - if poly then Clenv.refresh_undefined_univs clenv - else clenv, Univ.empty_level_subst - in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c) - -let rec e_trivial_fail_db db_list local_db = - let next = Proofview.Goal.nf_enter { enter = begin fun gl -> - let d = Tacmach.New.pf_last_hyp gl in - let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Tacmach.New.project gl) d in - e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db) - end } in - Proofview.Goal.enter { enter = begin fun gl -> - let tacl = - registered_e_assumption :: - (Tacticals.New.tclTHEN Tactics.intro next) :: - (List.map fst (e_trivial_resolve db_list local_db (Tacmach.New.pf_nf_concl gl))) - in - Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) - end } - -and e_my_find_search db_list local_db hdc concl = - let hint_of_db = hintmap_of hdc concl in - let hintl = - List.map_append (fun db -> - let flags = auto_flags_of_state (Hint_db.transparent_state db) in - List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list) - in - let tac_of_hint = - fun (st, {pri = b; pat = p; code = t; poly = poly}) -> - let b = match Hints.repr_hint t with - | Unfold_nth _ -> 1 - | _ -> b - in - (b, - let tac = function - | Res_pf (term,cl) -> unify_resolve poly st (term,cl) - | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl) - | Give_exact (c,cl) -> e_exact poly st (c,cl) - | Res_pf_THEN_trivial_fail (term,cl) -> - Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl)) - (e_trivial_fail_db db_list local_db) - | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl - | Extern tacast -> conclPattern concl p tacast - in - let tac = run_hint t tac in - (tac, lazy (pr_hint t))) - in - List.map tac_of_hint hintl - -and e_trivial_resolve db_list local_db gl = - let hd = try Some (decompose_app_bound gl) with Bound -> None in - try priority (e_my_find_search db_list local_db hd gl) - with Not_found -> [] - -let e_possible_resolve db_list local_db gl = - let hd = try Some (decompose_app_bound gl) with Bound -> None in - try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) (e_my_find_search db_list local_db hd gl) - with Not_found -> [] - -let find_first_goal gls = - try first_goal gls with UserError _ -> assert false - -(*s The following module [SearchProblem] is used to instantiate the generic - exploration functor [Explore.Make]. *) - -type search_state = { - priority : int; - depth : int; (*r depth of search before failing *) - tacres : goal list sigma; - last_tactic : std_ppcmds Lazy.t; - dblist : hint_db list; - localdb : hint_db list; - prev : prev_search_state; - local_lemmas : Tacexpr.delayed_open_constr list; -} - -and prev_search_state = (* for info eauto *) - | Unknown - | Init - | State of search_state - -module SearchProblem = struct - - type state = search_state - - let success s = List.is_empty (sig_it s.tacres) - -(* let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) *) - - let filter_tactics glls l = -(* let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) -(* let evars = Evarutil.nf_evars (Refiner.project glls) in *) -(* msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *) - let rec aux = function - | [] -> [] - | (tac, cost, pptac) :: tacl -> - try - let lgls = apply_tac_list (Proofview.V82.of_tactic tac) glls in -(* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) -(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) - (lgls, cost, pptac) :: aux tacl - with e when Errors.noncritical e -> - let e = Errors.push e in - Refiner.catch_failerror e; aux tacl - in aux l - - (* Ordering of states is lexicographic on depth (greatest first) then - number of remaining goals. *) - let compare s s' = - let d = s'.depth - s.depth in - let d' = Int.compare s.priority s'.priority in - let nbgoals s = List.length (sig_it s.tacres) in - if not (Int.equal d 0) then d - else if not (Int.equal d' 0) then d' - else Int.compare (nbgoals s) (nbgoals s') - - let branching s = - if Int.equal s.depth 0 then - [] - else - let ps = if s.prev == Unknown then Unknown else State s in - let lg = s.tacres in - let nbgl = List.length (sig_it lg) in - assert (nbgl > 0); - let g = find_first_goal lg in - let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in - let assumption_tacs = - let tacs = List.map map_assum (pf_ids_of_hyps g) in - let l = filter_tactics s.tacres tacs in - List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res; - last_tactic = pp; dblist = s.dblist; - localdb = List.tl s.localdb; - prev = ps; local_lemmas = s.local_lemmas}) l - in - let intro_tac = - let l = filter_tactics s.tacres [Tactics.intro, (-1), lazy (str "intro")] in - List.map - (fun (lgls, cost, pp) -> - let g' = first_goal lgls in - let hintl = - make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') - in - let ldb = Hint_db.add_list (pf_env g') (project g') - hintl (List.hd s.localdb) in - { depth = s.depth; priority = cost; tacres = lgls; - last_tactic = pp; dblist = s.dblist; - localdb = ldb :: List.tl s.localdb; prev = ps; - local_lemmas = s.local_lemmas}) - l - in - let rec_tacs = - let l = - filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) - in - List.map - (fun (lgls, cost, pp) -> - let nbgl' = List.length (sig_it lgls) in - if nbgl' < nbgl then - { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp; - prev = ps; dblist = s.dblist; localdb = List.tl s.localdb; - local_lemmas = s.local_lemmas } - else - let newlocal = - let hyps = pf_hyps g in - List.map (fun gl -> - let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in - let hyps' = pf_hyps gls in - if hyps' == hyps then List.hd s.localdb - else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true s.local_lemmas) - (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls)) - in - { depth = pred s.depth; priority = cost; tacres = lgls; - dblist = s.dblist; last_tactic = pp; prev = ps; - localdb = newlocal @ List.tl s.localdb; - local_lemmas = s.local_lemmas }) - l - in - List.sort compare (assumption_tacs @ intro_tac @ rec_tacs) - - let pp s = hov 0 (str " depth=" ++ int s.depth ++ spc () ++ - (Lazy.force s.last_tactic)) - -end - -module Search = Explore.Make(SearchProblem) - -(** Utilities for debug eauto / info eauto *) - -let global_debug_eauto = ref false -let global_info_eauto = ref false - -let _ = - Goptions.declare_bool_option - { Goptions.optsync = true; - Goptions.optdepr = false; - Goptions.optname = "Debug Eauto"; - Goptions.optkey = ["Debug";"Eauto"]; - Goptions.optread = (fun () -> !global_debug_eauto); - Goptions.optwrite = (:=) global_debug_eauto } - -let _ = - Goptions.declare_bool_option - { Goptions.optsync = true; - Goptions.optdepr = false; - Goptions.optname = "Info Eauto"; - Goptions.optkey = ["Info";"Eauto"]; - Goptions.optread = (fun () -> !global_info_eauto); - Goptions.optwrite = (:=) global_info_eauto } - -let mk_eauto_dbg d = - if d == Debug || !global_debug_eauto then Debug - else if d == Info || !global_info_eauto then Info - else Off - -let pr_info_nop = function - | Info -> msg_debug (str "idtac.") - | _ -> () - -let pr_dbg_header = function - | Off -> () - | Debug -> msg_debug (str "(* debug eauto : *)") - | Info -> msg_debug (str "(* info eauto : *)") - -let pr_info dbg s = - if dbg != Info then () - else - let rec loop s = - match s.prev with - | Unknown | Init -> s.depth - | State sp -> - let mindepth = loop sp in - let indent = String.make (mindepth - sp.depth) ' ' in - msg_debug (str indent ++ Lazy.force s.last_tactic ++ str "."); - mindepth - in - ignore (loop s) - -(** Eauto main code *) - -let make_initial_state dbg n gl dblist localdb lems = - { depth = n; - priority = 0; - tacres = tclIDTAC gl; - last_tactic = lazy (mt()); - dblist = dblist; - localdb = [localdb]; - prev = if dbg == Info then Init else Unknown; - local_lemmas = lems; - } - -let e_search_auto debug (in_depth,p) lems db_list gl = - let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:full_transparent_state true lems in - let d = mk_eauto_dbg debug in - let tac = match in_depth,d with - | (true,Debug) -> Search.debug_depth_first - | (true,_) -> Search.depth_first - | (false,Debug) -> Search.debug_breadth_first - | (false,_) -> Search.breadth_first - in - try - pr_dbg_header d; - let s = tac (make_initial_state d p gl db_list local_db lems) in - pr_info d s; - s.tacres - with Not_found -> - pr_info_nop d; - error "eauto: search failed" - -(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *) -(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *) - -let eauto_with_bases ?(debug=Off) np lems db_list = - tclTRY (e_search_auto debug np lems db_list) - -let eauto ?(debug=Off) np lems dbnames = - let db_list = make_db_list dbnames in - tclTRY (e_search_auto debug np lems db_list) - -let full_eauto ?(debug=Off) n lems gl = - let dbnames = current_db_names () in - let dbnames = String.Set.remove "v62" dbnames in - let db_list = List.map searchtable_map (String.Set.elements dbnames) in - tclTRY (e_search_auto debug n lems db_list) gl - -let gen_eauto ?(debug=Off) np lems = function - | None -> Proofview.V82.tactic (full_eauto ~debug np lems) - | Some l -> Proofview.V82.tactic (eauto ~debug np lems l) - -let make_depth = function - | None -> !default_search_depth - | Some d -> d - -let make_dimension n = function - | None -> (true,make_depth n) - | Some d -> (false,d) - -let cons a l = a :: l - -let autounfolds db occs cls gl = - let unfolds = List.concat (List.map (fun dbname -> - let db = try searchtable_map dbname - with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) - in - let (ids, csts) = Hint_db.unfolds db in - let hyps = pf_ids_of_hyps gl in - let ids = Idset.filter (fun id -> List.mem id hyps) ids in - Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts - (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) - in Proofview.V82.of_tactic (unfold_option unfolds cls) gl - -let autounfold db cls = - Proofview.V82.tactic begin fun gl -> - let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in - let tac = autounfolds db in - tclMAP (function - | OnHyp (id,occs,where) -> tac occs (Some (id,where)) - | OnConcl occs -> tac occs None) - cls gl - end - -let autounfold_tac db cls = - Proofview.tclUNIT () >>= fun () -> - let dbs = match db with - | None -> String.Set.elements (current_db_names ()) - | Some [] -> ["core"] - | Some l -> l - in - autounfold dbs cls - -let unfold_head env (ids, csts) c = - let rec aux c = - match kind_of_term c with - | Var id when Id.Set.mem id ids -> - (match Environ.named_body id env with - | Some b -> true, b - | None -> false, c) - | Const (cst,u as c) when Cset.mem cst csts -> - true, Environ.constant_value_in env c - | App (f, args) -> - (match aux f with - | true, f' -> true, Reductionops.whd_betaiota Evd.empty (mkApp (f', args)) - | false, _ -> - let done_, args' = - Array.fold_left_i (fun i (done_, acc) arg -> - if done_ then done_, arg :: acc - else match aux arg with - | true, arg' -> true, arg' :: acc - | false, arg' -> false, arg :: acc) - (false, []) args - in - if done_ then true, mkApp (f, Array.of_list (List.rev args')) - else false, c) - | _ -> - let done_ = ref false in - let c' = map_constr (fun c -> - if !done_ then c else - let x, c' = aux c in - done_ := x; c') c - in !done_, c' - in aux c - -let autounfold_one db cl = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let concl = Proofview.Goal.concl gl in - let st = - List.fold_left (fun (i,c) dbname -> - let db = try searchtable_map dbname - with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) - in - let (ids, csts) = Hint_db.unfolds db in - (Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db - in - let did, c' = unfold_head env st - (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl) - in - if did then - match cl with - | Some hyp -> change_in_hyp None (make_change_arg c') hyp - | None -> convert_concl_no_check c' DEFAULTcast - else Tacticals.New.tclFAIL 0 (str "Nothing to unfold") - end } diff --git a/ltac/eauto.mli b/ltac/eauto.mli deleted file mode 100644 index 8812093d5f..0000000000 --- a/ltac/eauto.mli +++ /dev/null @@ -1,33 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr -> unit Proofview.tactic - -val prolog_tac : Tacexpr.delayed_open_constr list -> int -> unit Proofview.tactic - -val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> Tacexpr.delayed_open_constr list -> - hint_db_name list option -> unit Proofview.tactic - -val eauto_with_bases : - ?debug:Tacexpr.debug -> - bool * int -> - Tacexpr.delayed_open_constr list -> hint_db list -> Proof_type.tactic - -val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic -val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic -val autounfold_one : hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic - -val make_dimension : int option -> int option -> bool * int diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index 7987d774d1..8e9f992f16 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -11,9 +11,7 @@ G_obligations Coretactics Autorewrite Extratactics -Eauto G_auto -Class_tactics G_class Rewrite G_rewrite diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml new file mode 100644 index 0000000000..4855598989 --- /dev/null +++ b/tactics/class_tactics.ml @@ -0,0 +1,903 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + if Evar.Map.mem ev !tosee then + visit ev (Evar.Map.find ev !tosee)) evs; + tosee := Evar.Map.remove ev !tosee; + l' := ev :: !l'; + in + while not (Evar.Map.is_empty !tosee) do + let ev, evi = Evar.Map.min_binding !tosee in + visit ev evi + done; + List.rev !l' + +let evars_to_goals p evm = + let goals = ref Evar.Map.empty in + let map ev evi = + let evi, goal = p evm ev evi in + let () = if goal then goals := Evar.Map.add ev evi !goals in + evi + in + let evm = Evd.raw_map_undefined map evm in + if Evar.Map.is_empty !goals then None + else Some (!goals, evm) + +(** Typeclasses instance search tactic / eauto *) + +open Auto + +open Unification + +let auto_core_unif_flags st freeze = { + modulo_conv_on_closed_terms = Some st; + use_metas_eagerly_in_conv_on_closed_terms = true; + use_evars_eagerly_in_conv_on_closed_terms = false; + modulo_delta = st; + modulo_delta_types = st; + check_applied_meta_types = false; + use_pattern_unification = true; + use_meta_bound_pattern_unification = true; + frozen_evars = freeze; + restrict_conv_on_strict_subterms = false; (* ? *) + modulo_betaiota = true; + modulo_eta = !typeclasses_modulo_eta; +} + +let auto_unif_flags freeze st = + let fl = auto_core_unif_flags st freeze in + { core_unify_flags = fl; + merge_unify_flags = fl; + subterm_unify_flags = fl; + allow_K_in_toplevel_higher_order_unification = false; + resolve_evars = false +} + +let rec eq_constr_mod_evars x y = + match kind_of_term x, kind_of_term y with + | Evar (e1, l1), Evar (e2, l2) when not (Evar.equal e1 e2) -> true + | _, _ -> compare_constr eq_constr_mod_evars x y + +let progress_evars t = + Proofview.Goal.nf_enter { enter = begin fun gl -> + let concl = Proofview.Goal.concl gl in + let check = + Proofview.Goal.nf_enter { enter = begin fun gl' -> + let newconcl = Proofview.Goal.concl gl' in + if eq_constr_mod_evars concl newconcl + then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)") + else Proofview.tclUNIT () + end } + in t <*> check + end } + + +let e_give_exact flags poly (c,clenv) gl = + let (c, _, _) = c in + let c, gl = + if poly then + let clenv', subst = Clenv.refresh_undefined_univs clenv in + let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in + let c = Vars.subst_univs_level_constr subst c in + c, {gl with sigma = evd} + else c, gl + in + let t1 = pf_unsafe_type_of gl c in + tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl + +let unify_e_resolve poly flags = { enter = begin fun gls (c,clenv) -> + let clenv', c = connect_hint_clenv poly c clenv gls in + let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in + Clenvtac.clenv_refine true ~with_classes:false clenv' + end } + +let unify_resolve poly flags = { enter = begin fun gls (c,clenv) -> + let clenv', _ = connect_hint_clenv poly c clenv gls in + let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in + Clenvtac.clenv_refine false ~with_classes:false clenv' + end } + +let clenv_of_prods poly nprods (c, clenv) gl = + let (c, _, _) = c in + if poly || Int.equal nprods 0 then Some clenv + else + let ty = Tacmach.New.pf_unsafe_type_of gl c in + let diff = nb_prod ty - nprods in + if Pervasives.(>=) diff 0 then + (* Was Some clenv... *) + Some (Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl) + else None + +let with_prods nprods poly (c, clenv) f = + Proofview.Goal.nf_enter { enter = begin fun gl -> + match clenv_of_prods poly nprods (c, clenv) gl with + | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses") + | Some clenv' -> f.enter gl (c, clenv') + end } + +(** Hack to properly solve dependent evars that are typeclasses *) + +let rec e_trivial_fail_db db_list local_db goal = + let tacl = + Proofview.V82.of_tactic Eauto.registered_e_assumption :: + (tclTHEN (Proofview.V82.of_tactic Tactics.intro) + (function g'-> + let d = pf_last_hyp g' in + let hintl = make_resolve_hyp (pf_env g') (project g') d in + (e_trivial_fail_db db_list + (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) :: + (List.map (fun (x,_,_,_,_) -> x) + (e_trivial_resolve db_list local_db (project goal) (pf_concl goal))) + in + tclFIRST (List.map tclCOMPLETE tacl) goal + +and e_my_find_search db_list local_db hdc complete sigma concl = + let prods, concl = decompose_prod_assum concl in + let nprods = List.length prods in + let freeze = + try + let cl = Typeclasses.class_info (fst hdc) in + if cl.cl_strict then + Evd.evars_of_term concl + else Evar.Set.empty + with e when Errors.noncritical e -> Evar.Set.empty + in + let hintl = + List.map_append + (fun db -> + let tacs = + if Hint_db.use_dn db then (* Using dnet *) + Hint_db.map_eauto hdc concl db + else Hint_db.map_existential hdc concl db + in + let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in + List.map (fun x -> (flags, x)) tacs) + (local_db::db_list) + in + let tac_of_hint = + fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) -> + let tac = function + | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags) + | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags) + | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c) + | Res_pf_THEN_trivial_fail (term,cl) -> + Proofview.V82.tactic (tclTHEN + (Proofview.V82.of_tactic ((with_prods nprods poly (term,cl) (unify_e_resolve poly flags)))) + (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)) + | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c]))) + | Extern tacast -> conclPattern concl p tacast + in + let tac = Proofview.V82.of_tactic (run_hint t tac) in + let tac = if complete then tclCOMPLETE tac else tac in + match repr_hint t with + | Extern _ -> (tac,b,true, name, lazy (pr_hint t)) + | _ -> +(* let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *) + (tac,b,false, name, lazy (pr_hint t)) + in List.map tac_of_hint hintl + +and e_trivial_resolve db_list local_db sigma concl = + try + e_my_find_search db_list local_db + (decompose_app_bound concl) true sigma concl + with Bound | Not_found -> [] + +let e_possible_resolve db_list local_db sigma concl = + try + e_my_find_search db_list local_db + (decompose_app_bound concl) false sigma concl + with Bound | Not_found -> [] + +let catchable = function + | Refiner.FailError _ -> true + | e -> Logic.catchable_exception e + +let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) evs (Evarutil.nf_evar evs (Goal.V82.concl evs ev)) + +let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l) + +type autoinfo = { hints : hint_db; is_evar: existential_key option; + only_classes: bool; unique : 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 failure = NotApplicable | ReachedLimit +type 'ans fk = failure -> '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 + +type atac = auto_result tac + +(* Some utility types to avoid the need of -rectypes *) + +type 'a optionk = + | Nonek + | Somek of 'a * 'a optionk fk + +type ('a,'b) optionk2 = + | Nonek2 of failure + | Somek2 of 'a * 'b * ('a,'b) optionk2 fk + +let make_resolve_hyp env sigma st flags only_classes pri decl = + let open Context.Named.Declaration in + let id = get_id decl in + let cty = Evarutil.nf_evar sigma (get_type decl) in + let rec iscl env ty = + let ctx, ar = decompose_prod_assum ty in + match kind_of_term (fst (decompose_app ar)) with + | Const (c,_) -> is_class (ConstRef c) + | Ind (i,_) -> is_class (IndRef i) + | _ -> + let env' = Environ.push_rel_context ctx env in + let ty' = whd_betadeltaiota env' ar in + if not (Term.eq_constr ty' ar) then iscl env' ty' + else false + in + 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 (path,pri, c) -> make_resolves env sigma ~name:(PathHints path) + (true,false,Flags.is_verbose()) pri false + (IsConstr (c,Univ.ContextSet.empty))) + hints) + else [] + in + (hints @ List.map_filter + (fun f -> try Some (f (c, cty, Univ.ContextSet.empty)) + with Failure _ | UserError _ -> None) + [make_exact_entry ~name env sigma pri false; + make_apply_entry ~name env sigma flags pri false]) + else [] + +let pf_filtered_hyps 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 -> + let consider = + let open Context.Named.Declaration in + try let t = Global.lookup_named (get_id hyp) |> get_type in + (* Section variable, reindex only if the type changed *) + not (Term.eq_constr t (get_type hyp)) + with Not_found -> true + in + if consider then + let path, hint = + PathEmpty, pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp + in + (PathOr (paths, path), hint @ hints) + else (paths, hints)) + (PathEmpty, []) sign + in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true) + +let make_autogoal_hints = + let cache = ref (true, Environ.empty_named_context_val, + Hint_db.empty full_transparent_state true) + in + fun only_classes ?(st=full_transparent_state) g -> + let sign = pf_filtered_hyps g in + let (onlyc, sign', cached_hints) = !cache in + if onlyc == only_classes && + (sign == sign' || Environ.eq_named_context_val sign sign') + && Hint_db.transparent_state cached_hints == st + then + cached_hints + else + let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in + cache := (only_classes, 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 -> sk (f gls hints) fk + | None -> fk NotApplicable } + +let intro_tac : atac = + lift_tactic (Proofview.V82.of_tactic Tactics.intro) + (fun {it = gls; sigma = s} info -> + let gls' = + List.map (fun g' -> + 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 context) in + let ldb = Hint_db.add_list env s 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 = + { 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 } + +let merge_failures x y = + match x, y with + | _, ReachedLimit + | ReachedLimit, _ -> ReachedLimit + | NotApplicable, NotApplicable -> NotApplicable + +let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = + { skft = fun sk fk gls -> x.skft sk + (fun f -> y.skft sk (fun f' -> fk (merge_failures f f')) gls) gls } + +let or_else_tac (x : 'a tac) (y : failure -> 'a tac) : 'a tac = + { skft = fun sk fk gls -> x.skft sk + (fun f -> (y f).skft sk fk gls) gls } + +let is_Prop env sigma concl = + let ty = Retyping.get_type_of env sigma concl in + match kind_of_term ty with + | Sort (Prop Null) -> true + | _ -> false + +let is_unique env concl = + try + let (cl,u), args = dest_class_app env concl in + cl.cl_unique + with e when Errors.noncritical e -> false + +let needs_backtrack env evd oev concl = + if Option.is_empty oev || is_Prop env evd concl then + occur_existential concl + else true + +let hints_tac hints = + { skft = fun sk fk {it = gl,info; sigma = s;} -> + let env = Goal.V82.env s gl in + let concl = Goal.V82.concl s gl in + let tacgl = {it = gl; sigma = s;} in + let poss = e_possible_resolve hints info.hints s concl in + let unique = is_unique env concl in + 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 + (match res with + | None -> aux i foundone tl + | Some {it = gls; sigma = s';} -> + if !typeclasses_debug then + msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp + ++ str" on" ++ spc () ++ pr_ev s gl); + let sgls = + evars_to_goals + (fun evm ev evi -> + if Typeclasses.is_resolvable evi && not (Evd.is_undefined s ev) && + (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') -> + if not !typeclasses_dependency_order then + (gls' @ List.map (fun (ev,_) -> (Some ev, ev)) (Evar.Map.bindings evgls), s') + else + (* Reorder with dependent subgoals. *) + let evm = List.fold_left + (fun acc g -> Evar.Map.add g (Evd.find_undefined s' g) acc) evgls gls in + let gls = top_sort s' evm in + (List.map (fun ev -> Some ev, ev) gls, 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 + let fk' = + (fun e -> + let do_backtrack = + if unique then occur_existential concl + else if info.unique then true + else if List.is_empty gls' then + needs_backtrack env s' info.is_evar concl + else true + in + let e' = match foundone with None -> e | Some e' -> merge_failures e e' in + if !typeclasses_debug then + msg_debug + ((if do_backtrack then str"Backtracking after " + else str "Not backtracking after ") + ++ Lazy.force pp); + if do_backtrack then aux (succ i) (Some e') tl + else fk e') + in + sk glsv fk') + | [] -> + if foundone == None && !typeclasses_debug then + msg_debug (pr_depth info.auto_depth ++ str": no match for " ++ + Printer.pr_constr_env (Goal.V82.env s gl) s concl ++ + spc () ++ str ", " ++ int (List.length poss) ++ str" possibilities"); + match foundone with + | Some e -> fk e + | None -> fk NotApplicable + in aux 1 None poss } + +let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk = + let rec aux s (acc : autogoal list list) fk = function + | (gl,info) :: gls -> + Control.check_for_interrupt (); + (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 fk'' = + if not info.unique && List.is_empty gls' && + not (needs_backtrack (Goal.V82.env s gl) s + info.is_evar (Goal.V82.concl s gl)) + then fk + else fk' + in + aux s' (gls'::acc) fk'' gls) + fk {it = (gl,info); sigma = s; }) + | [] -> Somek2 (List.rev acc, s, fk) + in fun {it = gls; sigma = s; } fk -> + let rec aux' = function + | Nonek2 e -> fk e + | Somek2 (res, s', fk') -> + let goals' = List.concat res in + sk {it = goals'; sigma = s'; } (fun e -> aux' (fk' e)) + in aux' (aux s [] (fun e -> Nonek2 e) gls) + +let then_tac (first : atac) (second : atac) : atac = + { skft = fun sk fk -> first.skft (then_list second sk) fk } + +let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option = + t.skft (fun x _ -> Some x) (fun _ -> None) gl + +type run_list_res = auto_result optionk + +let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res = + (then_list t (fun x fk -> Somek (x, fk))) + gl + (fun _ -> Nonek) + +let fail_tac reason : atac = + { skft = fun sk fk _ -> fk reason } + +let rec fix (t : 'a tac) : 'a tac = + then_tac t { skft = fun sk fk -> (fix t).skft sk fk } + +let rec fix_limit limit (t : 'a tac) : 'a tac = + if Int.equal limit 0 then fail_tac ReachedLimit + else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk } + +let fix_iterative t = + let rec aux depth = + or_else_tac (fix_limit depth t) + (function + | NotApplicable as e -> fail_tac e + | ReachedLimit -> aux (succ depth)) + in aux 1 + +let fix_iterative_limit limit (t : 'a tac) : 'a tac = + let rec aux depth = + if Int.equal depth limit then fail_tac ReachedLimit + else or_tac (fix_limit depth t) { skft = fun sk fk -> (aux (succ depth)).skft sk fk } + in aux 1 + +let make_autogoal ?(only_classes=true) ?(unique=false) ?(st=full_transparent_state) cut ev g = + let hints = make_autogoal_hints only_classes ~st g in + (g.it, { hints = hints ; is_evar = ev; unique = unique; + only_classes = only_classes; auto_depth = []; auto_last_tac = lazy (str"none"); + auto_path = []; auto_cut = cut }) + + +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) ?(unique=false) + ?(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 ~unique + ~st cut (Some g) {it = g; sigma = evm'; } in + (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm'; } + +let get_result r = + match r with + | Nonek -> None + | Somek (gls, fk) -> Some (gls.sigma,fk) + +let run_on_evars ?(only_classes=true) ?(unique=false) ?(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 goals = + if !typeclasses_dependency_order then + top_sort evm' goals + else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals) + in + let res = run_list_tac tac p goals + (make_autogoals ~only_classes ~unique ~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 ~with_univs:false evm' evm, fk) + +let eauto_tac hints = + then_tac normevars_tac (or_tac (hints_tac hints) intro_tac) + +let eauto_tac ?limit hints = + if get_typeclasses_iterative_deepening () then + match limit with + | None -> fix_iterative (eauto_tac hints) + | Some limit -> fix_iterative_limit limit (eauto_tac hints) + else + match limit with + | None -> fix (eauto_tac hints) + | Some limit -> fix_limit limit (eauto_tac hints) + +let real_eauto ?limit unique st hints p evd = + let res = + run_on_evars ~st ~unique p evd hints (eauto_tac ?limit hints) + in + match res with + | None -> evd + | Some (evd', fk) -> + if unique then + (match get_result (fk NotApplicable) with + | Some (evd'', fk') -> error "Typeclass resolution gives multiple solutions" + | None -> evd') + else evd' + +let resolve_all_evars_once debug limit unique p evd = + let db = searchtable_map typeclasses_db in + real_eauto ?limit unique (Hint_db.transparent_state db) [db] p evd + +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; } -> + {it = List.map fst goals; sigma = s;} + +(** 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(Evar.Set)(Evar.Map) + +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 (Evar.Set.union evx evy) p) + cstrs + +let evar_dependencies evm p = + Evd.fold_undefined + (fun ev evi _ -> + let evars = Evar.Set.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 unique = + 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' = eauto ?limit:!typeclasses_depth ~st:(Hint_db.transparent_state hints) [hints] gls in + let evd = sig_sig gls' 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_instantiation_problem := + (fun x y z w -> resolve_one_typeclass x ~sigma:y z w) + +(** [split_evars] returns groups of undefined evars according to dependencies *) + +let split_evars evm = + let p = Intpart.create () in + evar_dependencies evm p; + deps_of_constraints (snd (extract_all_conv_pbs evm)) evm p; + Intpart.partition p + +let is_inference_forced p evd ev = + try + 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 + | Evar_kinds.ImplicitArg (_, _, b) -> b + | Evar_kinds.QuestionMark _ -> false + | _ -> true + else true + with Not_found -> assert false + +let is_mandatory p comp evd = + Evar.Set.exists (is_inference_forced p evd) comp + +(** In case of unsatisfiable constraints, build a nice error message *) + +let error_unresolvable env comp evd = + let evd = Evarutil.nf_evar_map_undefined evd in + let is_part ev = match comp with + | None -> true + | Some s -> Evar.Set.mem ev s + in + let fold ev evi (found, accu) = + let ev_class = class_of_constr evi.evar_concl in + if not (Option.is_empty ev_class) && is_part ev then + (* focus on one instance if only one was searched for *) + if not found then (true, Some ev) + else (found, None) + else (found, accu) + in + let (_, ev) = Evd.fold_undefined fold evd (true, None) in + Pretype_errors.unsatisfiable_constraints + (Evarutil.nf_env_evar evd env) evd ev comp + +(** 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 = + let check ev evi = snd (p oevd ev evi) in + Evar.Map.exists check (Evd.undefined_map evd) + +(** Revert the resolvability status of evars after resolution, + potentially unprotecting some evars that were set unresolvable + just for this call to resolution. *) + +let revert_resolvability oevd evd = + let map ev evi = + try + if not (Typeclasses.is_resolvable evi) then + let evi' = Evd.find_undefined oevd ev in + if Typeclasses.is_resolvable evi' then + Typeclasses.mark_resolvable evi + else evi + else evi + with Not_found -> evi + in + Evd.raw_map_undefined map evd + +(** 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 unique env p oevd do_split fail = + let split = if do_split then split_evars oevd else [Evar.Set.empty] in + let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true + in + let rec docomp evd = function + | [] -> revert_resolvability oevd evd + | comp :: comps -> + let p = select_and_update_evars p oevd (in_comp comp) in + try + let evd' = resolve_all_evars_once debug m unique 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. *) + let comp = if do_split then Some comp else None in + error_unresolvable env comp evd + else (* Best effort: do nothing on this component *) + docomp evd comps + in docomp oevd split + +let initial_select_evars filter = + fun evd ev evi -> + filter ev (snd evi.Evd.evar_source) && + Typeclasses.is_class_evar evd evi + +let resolve_typeclass_evars debug m unique env evd filter split fail = + let evd = + try Evarconv.consider_remaining_unif_problems + ~ts:(Typeclasses.classes_transparent_state ()) env evd + with e when Errors.noncritical e -> evd + in + resolve_all_evars debug m unique env (initial_select_evars filter) evd split fail + +let solve_inst debug depth env evd filter unique split fail = + resolve_typeclass_evars debug depth unique env evd filter split fail + +let _ = + Typeclasses.solve_instantiations_problem := + solve_inst false !typeclasses_depth + +let set_typeclasses_debug d = (:=) typeclasses_debug d; + Typeclasses.solve_instantiations_problem := solve_inst d !typeclasses_depth + +let get_typeclasses_debug () = !typeclasses_debug + +let set_typeclasses_depth d = (:=) typeclasses_depth d; + Typeclasses.solve_instantiations_problem := solve_inst !typeclasses_debug !typeclasses_depth + +let get_typeclasses_depth () = !typeclasses_depth + +open Goptions + +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 = + 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 typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl = + try + let dbs = List.map_filter + (fun db -> try Some (searchtable_map db) + with e when Errors.noncritical e -> None) + dbs + in + let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in + eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl + with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl + +(** Take the head of the arity of a constr. + Used in the partial application tactic. *) + +let rec head_of_constr t = + let t = strip_outer_cast(collapse_appl t) in + match kind_of_term t with + | Prod (_,_,c2) -> head_of_constr c2 + | LetIn (_,_,_,c2) -> head_of_constr c2 + | App (f,args) -> head_of_constr f + | _ -> t + +let head_of_constr h c = + let c = head_of_constr c in + letin_tac None (Name h) c None Locusops.allHyps + +let not_evar c = match kind_of_term c with +| Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar") +| _ -> Proofview.tclUNIT () + +let is_ground c gl = + if Evarutil.is_ground_term (project gl) c then tclIDTAC gl + else tclFAIL 0 (str"Not ground") gl + +let autoapply c i gl = + let flags = auto_unif_flags Evar.Set.empty + (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in + let cty = pf_unsafe_type_of gl c in + let ce = mk_clenv_from gl (c,cty) in + let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl ((c,cty,Univ.ContextSet.empty),ce) } in + Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli new file mode 100644 index 0000000000..f1bcfa7dd4 --- /dev/null +++ b/tactics/class_tactics.mli @@ -0,0 +1,32 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool + +val set_typeclasses_debug : bool -> unit +val get_typeclasses_debug : unit -> bool + +val set_typeclasses_depth : int option -> unit +val get_typeclasses_depth : unit -> int option + +val progress_evars : unit Proofview.tactic -> unit Proofview.tactic + +val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> + Hints.hint_db_name list -> tactic + +val head_of_constr : Id.t -> Term.constr -> unit Proofview.tactic + +val not_evar : constr -> unit Proofview.tactic + +val is_ground : constr -> tactic + +val autoapply : constr -> Hints.hint_db_name -> tactic diff --git a/tactics/eauto.ml b/tactics/eauto.ml new file mode 100644 index 0000000000..9cfb805d4c --- /dev/null +++ b/tactics/eauto.ml @@ -0,0 +1,526 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + let t1 = Tacmach.New.pf_unsafe_type_of gl c in + let t2 = Tacmach.New.pf_concl gl in + if occur_existential t1 || occur_existential t2 then + Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c)) + else exact_check c + end } + +let assumption id = e_give_exact (mkVar id) + +let e_assumption = + Proofview.Goal.enter { enter = begin fun gl -> + Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl)) + end } + +let registered_e_assumption = + Proofview.Goal.enter { enter = begin fun gl -> + Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id)) + (Tacmach.New.pf_ids_of_hyps gl)) + end } + +let eval_uconstrs ist cs = + let flags = { + Pretyping.use_typeclasses = false; + use_unif_heuristics = true; + use_hook = Some Pfedit.solve_by_implicit_tactic; + fail_evar = false; + expand_evars = true + } in + List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs + +(************************************************************************) +(* PROLOG tactic *) +(************************************************************************) + +(*s Tactics handling a list of goals. *) + +(* first_goal : goal list sigma -> goal sigma *) + +let first_goal gls = + let gl = gls.Evd.it and sig_0 = gls.Evd.sigma in + if List.is_empty gl then error "first_goal"; + { Evd.it = List.hd gl; Evd.sigma = sig_0; } + +(* tactic -> tactic_list : Apply a tactic to the first goal in the list *) + +let apply_tac_list tac glls = + let (sigr,lg) = unpackage glls in + match lg with + | (g1::rest) -> + let gl = apply_sig_tac sigr tac g1 in + repackage sigr (gl@rest) + | _ -> error "apply_tac_list" + +let one_step l gl = + [Proofview.V82.of_tactic Tactics.intro] + @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl))) + @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l) + @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl)) + +let rec prolog l n gl = + if n <= 0 then error "prolog - failure"; + let prol = (prolog l (n-1)) in + (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl + +let out_term = function + | IsConstr (c, _) -> c + | IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr) + +let prolog_tac l n = + Proofview.V82.tactic begin fun gl -> + let map c = + let (c, sigma) = Tactics.run_delayed (pf_env gl) (project gl) c in + let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in + out_term c + in + let l = List.map map l in + try (prolog l n gl) + with UserError ("Refiner.tclFIRST",_) -> + errorlabstrm "Prolog.prolog" (str "Prolog failed.") + end + +open Auto +open Unification + +(***************************************************************************) +(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) +(***************************************************************************) + +let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l) + +let unify_e_resolve poly flags (c,clenv) = + Proofview.Goal.nf_enter { enter = begin fun gl -> + let clenv', c = connect_hint_clenv poly c clenv gl in + Proofview.V82.tactic + (fun gls -> + let clenv' = clenv_unique_resolver ~flags clenv' gls in + tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) + (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls) + end } + +let hintmap_of hdc concl = + match hdc with + | None -> fun db -> Hint_db.map_none db + | Some hdc -> + if occur_existential concl then (fun db -> Hint_db.map_existential hdc concl db) + else (fun db -> Hint_db.map_auto hdc concl db) + (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) + +let e_exact poly flags (c,clenv) = + let (c, _, _) = c in + let clenv', subst = + if poly then Clenv.refresh_undefined_univs clenv + else clenv, Univ.empty_level_subst + in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c) + +let rec e_trivial_fail_db db_list local_db = + let next = Proofview.Goal.nf_enter { enter = begin fun gl -> + let d = Tacmach.New.pf_last_hyp gl in + let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Tacmach.New.project gl) d in + e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db) + end } in + Proofview.Goal.enter { enter = begin fun gl -> + let tacl = + registered_e_assumption :: + (Tacticals.New.tclTHEN Tactics.intro next) :: + (List.map fst (e_trivial_resolve db_list local_db (Tacmach.New.pf_nf_concl gl))) + in + Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) + end } + +and e_my_find_search db_list local_db hdc concl = + let hint_of_db = hintmap_of hdc concl in + let hintl = + List.map_append (fun db -> + let flags = auto_flags_of_state (Hint_db.transparent_state db) in + List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list) + in + let tac_of_hint = + fun (st, {pri = b; pat = p; code = t; poly = poly}) -> + let b = match Hints.repr_hint t with + | Unfold_nth _ -> 1 + | _ -> b + in + (b, + let tac = function + | Res_pf (term,cl) -> unify_resolve poly st (term,cl) + | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl) + | Give_exact (c,cl) -> e_exact poly st (c,cl) + | Res_pf_THEN_trivial_fail (term,cl) -> + Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl)) + (e_trivial_fail_db db_list local_db) + | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl + | Extern tacast -> conclPattern concl p tacast + in + let tac = run_hint t tac in + (tac, lazy (pr_hint t))) + in + List.map tac_of_hint hintl + +and e_trivial_resolve db_list local_db gl = + let hd = try Some (decompose_app_bound gl) with Bound -> None in + try priority (e_my_find_search db_list local_db hd gl) + with Not_found -> [] + +let e_possible_resolve db_list local_db gl = + let hd = try Some (decompose_app_bound gl) with Bound -> None in + try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) (e_my_find_search db_list local_db hd gl) + with Not_found -> [] + +let find_first_goal gls = + try first_goal gls with UserError _ -> assert false + +(*s The following module [SearchProblem] is used to instantiate the generic + exploration functor [Explore.Make]. *) + +type search_state = { + priority : int; + depth : int; (*r depth of search before failing *) + tacres : goal list sigma; + last_tactic : std_ppcmds Lazy.t; + dblist : hint_db list; + localdb : hint_db list; + prev : prev_search_state; + local_lemmas : Tacexpr.delayed_open_constr list; +} + +and prev_search_state = (* for info eauto *) + | Unknown + | Init + | State of search_state + +module SearchProblem = struct + + type state = search_state + + let success s = List.is_empty (sig_it s.tacres) + +(* let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) *) + + let filter_tactics glls l = +(* let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) +(* let evars = Evarutil.nf_evars (Refiner.project glls) in *) +(* msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *) + let rec aux = function + | [] -> [] + | (tac, cost, pptac) :: tacl -> + try + let lgls = apply_tac_list (Proofview.V82.of_tactic tac) glls in +(* let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) +(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) + (lgls, cost, pptac) :: aux tacl + with e when Errors.noncritical e -> + let e = Errors.push e in + Refiner.catch_failerror e; aux tacl + in aux l + + (* Ordering of states is lexicographic on depth (greatest first) then + number of remaining goals. *) + let compare s s' = + let d = s'.depth - s.depth in + let d' = Int.compare s.priority s'.priority in + let nbgoals s = List.length (sig_it s.tacres) in + if not (Int.equal d 0) then d + else if not (Int.equal d' 0) then d' + else Int.compare (nbgoals s) (nbgoals s') + + let branching s = + if Int.equal s.depth 0 then + [] + else + let ps = if s.prev == Unknown then Unknown else State s in + let lg = s.tacres in + let nbgl = List.length (sig_it lg) in + assert (nbgl > 0); + let g = find_first_goal lg in + let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in + let assumption_tacs = + let tacs = List.map map_assum (pf_ids_of_hyps g) in + let l = filter_tactics s.tacres tacs in + List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res; + last_tactic = pp; dblist = s.dblist; + localdb = List.tl s.localdb; + prev = ps; local_lemmas = s.local_lemmas}) l + in + let intro_tac = + let l = filter_tactics s.tacres [Tactics.intro, (-1), lazy (str "intro")] in + List.map + (fun (lgls, cost, pp) -> + let g' = first_goal lgls in + let hintl = + make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') + in + let ldb = Hint_db.add_list (pf_env g') (project g') + hintl (List.hd s.localdb) in + { depth = s.depth; priority = cost; tacres = lgls; + last_tactic = pp; dblist = s.dblist; + localdb = ldb :: List.tl s.localdb; prev = ps; + local_lemmas = s.local_lemmas}) + l + in + let rec_tacs = + let l = + filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) + in + List.map + (fun (lgls, cost, pp) -> + let nbgl' = List.length (sig_it lgls) in + if nbgl' < nbgl then + { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp; + prev = ps; dblist = s.dblist; localdb = List.tl s.localdb; + local_lemmas = s.local_lemmas } + else + let newlocal = + let hyps = pf_hyps g in + List.map (fun gl -> + let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in + let hyps' = pf_hyps gls in + if hyps' == hyps then List.hd s.localdb + else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true s.local_lemmas) + (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls)) + in + { depth = pred s.depth; priority = cost; tacres = lgls; + dblist = s.dblist; last_tactic = pp; prev = ps; + localdb = newlocal @ List.tl s.localdb; + local_lemmas = s.local_lemmas }) + l + in + List.sort compare (assumption_tacs @ intro_tac @ rec_tacs) + + let pp s = hov 0 (str " depth=" ++ int s.depth ++ spc () ++ + (Lazy.force s.last_tactic)) + +end + +module Search = Explore.Make(SearchProblem) + +(** Utilities for debug eauto / info eauto *) + +let global_debug_eauto = ref false +let global_info_eauto = ref false + +let _ = + Goptions.declare_bool_option + { Goptions.optsync = true; + Goptions.optdepr = false; + Goptions.optname = "Debug Eauto"; + Goptions.optkey = ["Debug";"Eauto"]; + Goptions.optread = (fun () -> !global_debug_eauto); + Goptions.optwrite = (:=) global_debug_eauto } + +let _ = + Goptions.declare_bool_option + { Goptions.optsync = true; + Goptions.optdepr = false; + Goptions.optname = "Info Eauto"; + Goptions.optkey = ["Info";"Eauto"]; + Goptions.optread = (fun () -> !global_info_eauto); + Goptions.optwrite = (:=) global_info_eauto } + +let mk_eauto_dbg d = + if d == Debug || !global_debug_eauto then Debug + else if d == Info || !global_info_eauto then Info + else Off + +let pr_info_nop = function + | Info -> msg_debug (str "idtac.") + | _ -> () + +let pr_dbg_header = function + | Off -> () + | Debug -> msg_debug (str "(* debug eauto : *)") + | Info -> msg_debug (str "(* info eauto : *)") + +let pr_info dbg s = + if dbg != Info then () + else + let rec loop s = + match s.prev with + | Unknown | Init -> s.depth + | State sp -> + let mindepth = loop sp in + let indent = String.make (mindepth - sp.depth) ' ' in + msg_debug (str indent ++ Lazy.force s.last_tactic ++ str "."); + mindepth + in + ignore (loop s) + +(** Eauto main code *) + +let make_initial_state dbg n gl dblist localdb lems = + { depth = n; + priority = 0; + tacres = tclIDTAC gl; + last_tactic = lazy (mt()); + dblist = dblist; + localdb = [localdb]; + prev = if dbg == Info then Init else Unknown; + local_lemmas = lems; + } + +let e_search_auto debug (in_depth,p) lems db_list gl = + let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:full_transparent_state true lems in + let d = mk_eauto_dbg debug in + let tac = match in_depth,d with + | (true,Debug) -> Search.debug_depth_first + | (true,_) -> Search.depth_first + | (false,Debug) -> Search.debug_breadth_first + | (false,_) -> Search.breadth_first + in + try + pr_dbg_header d; + let s = tac (make_initial_state d p gl db_list local_db lems) in + pr_info d s; + s.tacres + with Not_found -> + pr_info_nop d; + error "eauto: search failed" + +(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *) +(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *) + +let eauto_with_bases ?(debug=Off) np lems db_list = + tclTRY (e_search_auto debug np lems db_list) + +let eauto ?(debug=Off) np lems dbnames = + let db_list = make_db_list dbnames in + tclTRY (e_search_auto debug np lems db_list) + +let full_eauto ?(debug=Off) n lems gl = + let dbnames = current_db_names () in + let dbnames = String.Set.remove "v62" dbnames in + let db_list = List.map searchtable_map (String.Set.elements dbnames) in + tclTRY (e_search_auto debug n lems db_list) gl + +let gen_eauto ?(debug=Off) np lems = function + | None -> Proofview.V82.tactic (full_eauto ~debug np lems) + | Some l -> Proofview.V82.tactic (eauto ~debug np lems l) + +let make_depth = function + | None -> !default_search_depth + | Some d -> d + +let make_dimension n = function + | None -> (true,make_depth n) + | Some d -> (false,d) + +let cons a l = a :: l + +let autounfolds db occs cls gl = + let unfolds = List.concat (List.map (fun dbname -> + let db = try searchtable_map dbname + with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) + in + let (ids, csts) = Hint_db.unfolds db in + let hyps = pf_ids_of_hyps gl in + let ids = Idset.filter (fun id -> List.mem id hyps) ids in + Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts + (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) + in Proofview.V82.of_tactic (unfold_option unfolds cls) gl + +let autounfold db cls = + Proofview.V82.tactic begin fun gl -> + let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in + let tac = autounfolds db in + tclMAP (function + | OnHyp (id,occs,where) -> tac occs (Some (id,where)) + | OnConcl occs -> tac occs None) + cls gl + end + +let autounfold_tac db cls = + Proofview.tclUNIT () >>= fun () -> + let dbs = match db with + | None -> String.Set.elements (current_db_names ()) + | Some [] -> ["core"] + | Some l -> l + in + autounfold dbs cls + +let unfold_head env (ids, csts) c = + let rec aux c = + match kind_of_term c with + | Var id when Id.Set.mem id ids -> + (match Environ.named_body id env with + | Some b -> true, b + | None -> false, c) + | Const (cst,u as c) when Cset.mem cst csts -> + true, Environ.constant_value_in env c + | App (f, args) -> + (match aux f with + | true, f' -> true, Reductionops.whd_betaiota Evd.empty (mkApp (f', args)) + | false, _ -> + let done_, args' = + Array.fold_left_i (fun i (done_, acc) arg -> + if done_ then done_, arg :: acc + else match aux arg with + | true, arg' -> true, arg' :: acc + | false, arg' -> false, arg :: acc) + (false, []) args + in + if done_ then true, mkApp (f, Array.of_list (List.rev args')) + else false, c) + | _ -> + let done_ = ref false in + let c' = map_constr (fun c -> + if !done_ then c else + let x, c' = aux c in + done_ := x; c') c + in !done_, c' + in aux c + +let autounfold_one db cl = + Proofview.Goal.nf_enter { enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + let st = + List.fold_left (fun (i,c) dbname -> + let db = try searchtable_map dbname + with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) + in + let (ids, csts) = Hint_db.unfolds db in + (Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db + in + let did, c' = unfold_head env st + (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl) + in + if did then + match cl with + | Some hyp -> change_in_hyp None (make_change_arg c') hyp + | None -> convert_concl_no_check c' DEFAULTcast + else Tacticals.New.tclFAIL 0 (str "Nothing to unfold") + end } diff --git a/tactics/eauto.mli b/tactics/eauto.mli new file mode 100644 index 0000000000..8812093d5f --- /dev/null +++ b/tactics/eauto.mli @@ -0,0 +1,33 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constr -> unit Proofview.tactic + +val prolog_tac : Tacexpr.delayed_open_constr list -> int -> unit Proofview.tactic + +val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> Tacexpr.delayed_open_constr list -> + hint_db_name list option -> unit Proofview.tactic + +val eauto_with_bases : + ?debug:Tacexpr.debug -> + bool * int -> + Tacexpr.delayed_open_constr list -> hint_db list -> Proof_type.tactic + +val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic +val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic +val autounfold_one : hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic + +val make_dimension : int option -> int option -> bool * int diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index cb327e52c1..bbad1d8e64 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -17,5 +17,7 @@ Leminv Taccoerce Hints Auto +Eauto +Class_tactics Tactic_matching Term_dnet -- cgit v1.2.3 From a947e85e88ab0b9a5a4cfea81ecbeec6f52636ea Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Mar 2016 09:38:15 +0100 Subject: Making Eqdecide independent of Extratactics. --- ltac/eqdecide.ml | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/ltac/eqdecide.ml b/ltac/eqdecide.ml index 7d0df2f522..011296a8d0 100644 --- a/ltac/eqdecide.ml +++ b/ltac/eqdecide.ml @@ -22,7 +22,9 @@ open Tactics open Tacticals.New open Auto open Constr_matching +open Misctypes open Hipattern +open Pretyping open Tacmach.New open Coqlib open Proofview.Notations @@ -72,10 +74,15 @@ let mkBranches c1 c2 = clear_last; intros] +let discrHyp id = + let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in + let tac c = Equality.discr_tac false (Some (None, Tacexpr.ElimOnConstr c)) in + Tacticals.New.tclDELAYEDWITHHOLES false c tac + let solveNoteqBranch side = tclTHEN (choose_noteq side) (tclTHEN introf - (onLastHypId (fun id -> Extratactics.discrHyp id))) + (onLastHypId (fun id -> discrHyp id))) (* Constructs the type {c1=c2}+{~c1=c2} *) @@ -115,6 +122,11 @@ let rec rewrite_and_clear hyps = match hyps with let eqCase tac = tclTHEN intro (onLastHypId tac) +let injHyp id = + let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in + let tac c = Equality.injClause None false (Some (None, Tacexpr.ElimOnConstr c)) in + Tacticals.New.tclDELAYEDWITHHOLES false c tac + let diseqCase hyps eqonleft = let diseq = Id.of_string "diseq" in let absurd = Id.of_string "absurd" in @@ -124,7 +136,7 @@ let diseqCase hyps eqonleft = (tclTHEN (red_in_concl) (tclTHEN (intro_using absurd) (tclTHEN (Simple.apply (mkVar diseq)) - (tclTHEN (Extratactics.injHyp absurd) + (tclTHEN (injHyp absurd) (full_trivial [])))))))) open Proofview.Notations -- cgit v1.2.3 From 63b914b51ddc9084bc2e059df266e2345dfe34b5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Mar 2016 09:59:52 +0100 Subject: Moving Eqdecide to tactics/. --- ltac/eqdecide.ml | 237 -------------------------------------------------- ltac/eqdecide.mli | 17 ---- ltac/ltac.mllib | 1 - tactics/eqdecide.ml | 237 ++++++++++++++++++++++++++++++++++++++++++++++++++ tactics/eqdecide.mli | 17 ++++ tactics/tactics.mllib | 1 + 6 files changed, 255 insertions(+), 255 deletions(-) delete mode 100644 ltac/eqdecide.ml delete mode 100644 ltac/eqdecide.mli create mode 100644 tactics/eqdecide.ml create mode 100644 tactics/eqdecide.mli diff --git a/ltac/eqdecide.ml b/ltac/eqdecide.ml deleted file mode 100644 index 011296a8d0..0000000000 --- a/ltac/eqdecide.ml +++ /dev/null @@ -1,237 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (clear [destVar c]))) - -let choose_eq eqonleft = - if eqonleft then - left_with_bindings false Misctypes.NoBindings - else - right_with_bindings false Misctypes.NoBindings -let choose_noteq eqonleft = - if eqonleft then - right_with_bindings false Misctypes.NoBindings - else - left_with_bindings false Misctypes.NoBindings - -let mkBranches c1 c2 = - tclTHENLIST - [Proofview.V82.tactic (generalize [c2]); - Simple.elim c1; - intros; - onLastHyp Simple.case; - clear_last; - intros] - -let discrHyp id = - let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in - let tac c = Equality.discr_tac false (Some (None, Tacexpr.ElimOnConstr c)) in - Tacticals.New.tclDELAYEDWITHHOLES false c tac - -let solveNoteqBranch side = - tclTHEN (choose_noteq side) - (tclTHEN introf - (onLastHypId (fun id -> discrHyp id))) - -(* Constructs the type {c1=c2}+{~c1=c2} *) - -let make_eq () = -(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ()) - -let mkDecideEqGoal eqonleft op rectype c1 c2 = - let equality = mkApp(make_eq(), [|rectype; c1; c2|]) in - let disequality = mkApp(build_coq_not (), [|equality|]) in - if eqonleft then mkApp(op, [|equality; disequality |]) - else mkApp(op, [|disequality; equality |]) - - -(* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *) - -let idx = Id.of_string "x" -let idy = Id.of_string "y" - -let mkGenDecideEqGoal rectype g = - let hypnames = pf_ids_of_hyps g in - let xname = next_ident_away idx hypnames - and yname = next_ident_away idy hypnames in - (mkNamedProd xname rectype - (mkNamedProd yname rectype - (mkDecideEqGoal true (build_coq_sumbool ()) - rectype (mkVar xname) (mkVar yname)))) - -let rec rewrite_and_clear hyps = match hyps with -| [] -> Proofview.tclUNIT () -| id :: hyps -> - tclTHENLIST [ - Equality.rewriteLR (mkVar id); - clear [id]; - rewrite_and_clear hyps; - ] - -let eqCase tac = - tclTHEN intro (onLastHypId tac) - -let injHyp id = - let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in - let tac c = Equality.injClause None false (Some (None, Tacexpr.ElimOnConstr c)) in - Tacticals.New.tclDELAYEDWITHHOLES false c tac - -let diseqCase hyps eqonleft = - let diseq = Id.of_string "diseq" in - let absurd = Id.of_string "absurd" in - (tclTHEN (intro_using diseq) - (tclTHEN (choose_noteq eqonleft) - (tclTHEN (rewrite_and_clear (List.rev hyps)) - (tclTHEN (red_in_concl) - (tclTHEN (intro_using absurd) - (tclTHEN (Simple.apply (mkVar diseq)) - (tclTHEN (injHyp absurd) - (full_trivial [])))))))) - -open Proofview.Notations - -(* spiwack: a small wrapper around [Hipattern]. *) - -let match_eqdec c = - try Proofview.tclUNIT (match_eqdec c) - with PatternMatchingFailure -> Proofview.tclZERO PatternMatchingFailure - -(* /spiwack *) - -let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with -| [], [] -> - tclTHENLIST [ - choose_eq eqonleft; - rewrite_and_clear (List.rev hyps); - intros_reflexivity; - ] -| a1 :: largs, a2 :: rargs -> - Proofview.Goal.enter { enter = begin fun gl -> - let rectype = pf_unsafe_type_of gl a1 in - let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in - let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in - let subtacs = - if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto] - else [diseqCase hyps eqonleft;eqCase tac;default_auto] in - (tclTHENS (elim_type decide) subtacs) - end } -| _ -> invalid_arg "List.fold_right2" - -let solveEqBranch rectype = - Proofview.tclORELSE - begin - Proofview.Goal.enter { enter = begin fun gl -> - let concl = pf_nf_concl gl in - match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) -> - let (mib,mip) = Global.lookup_inductive rectype in - let nparams = mib.mind_nparams in - let getargs l = List.skipn nparams (snd (decompose_app l)) in - let rargs = getargs rhs - and largs = getargs lhs in - solveArg [] eqonleft op largs rargs - end } - end - begin function (e, info) -> match e with - | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!") - | e -> Proofview.tclZERO ~info e - end - -(* The tactic Decide Equality *) - -let hd_app c = match kind_of_term c with - | App (h,_) -> h - | _ -> c - -let decideGralEquality = - Proofview.tclORELSE - begin - Proofview.Goal.enter { enter = begin fun gl -> - let concl = pf_nf_concl gl in - match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) -> - let headtyp = hd_app (pf_compute gl typ) in - begin match kind_of_term headtyp with - | Ind (mi,_) -> Proofview.tclUNIT mi - | _ -> tclZEROMSG (Pp.str"This decision procedure only works for inductive objects.") - end >>= fun rectype -> - (tclTHEN - (mkBranches c1 c2) - (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype))) - end } - end - begin function (e, info) -> match e with - | PatternMatchingFailure -> - Tacticals.New.tclZEROMSG (Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}.") - | e -> Proofview.tclZERO ~info e - end - -let decideEqualityGoal = tclTHEN intros decideGralEquality - -let decideEquality rectype = - Proofview.Goal.enter { enter = begin fun gl -> - let decide = mkGenDecideEqGoal rectype gl in - (tclTHENS (cut decide) [default_auto;decideEqualityGoal]) - end } - - -(* The tactic Compare *) - -let compare c1 c2 = - Proofview.Goal.enter { enter = begin fun gl -> - let rectype = pf_unsafe_type_of gl c1 in - let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in - (tclTHENS (cut decide) - [(tclTHEN intro - (tclTHEN (onLastHyp simplest_case) clear_last)); - decideEquality rectype]) - end } diff --git a/ltac/eqdecide.mli b/ltac/eqdecide.mli deleted file mode 100644 index cb48a5bcc8..0000000000 --- a/ltac/eqdecide.mli +++ /dev/null @@ -1,17 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Constr.t -> unit Proofview.tactic diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index 8e9f992f16..28bfa5aa0a 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -16,6 +16,5 @@ G_class Rewrite G_rewrite Tauto -Eqdecide G_eqdecide G_ltac diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml new file mode 100644 index 0000000000..011296a8d0 --- /dev/null +++ b/tactics/eqdecide.ml @@ -0,0 +1,237 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (clear [destVar c]))) + +let choose_eq eqonleft = + if eqonleft then + left_with_bindings false Misctypes.NoBindings + else + right_with_bindings false Misctypes.NoBindings +let choose_noteq eqonleft = + if eqonleft then + right_with_bindings false Misctypes.NoBindings + else + left_with_bindings false Misctypes.NoBindings + +let mkBranches c1 c2 = + tclTHENLIST + [Proofview.V82.tactic (generalize [c2]); + Simple.elim c1; + intros; + onLastHyp Simple.case; + clear_last; + intros] + +let discrHyp id = + let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in + let tac c = Equality.discr_tac false (Some (None, Tacexpr.ElimOnConstr c)) in + Tacticals.New.tclDELAYEDWITHHOLES false c tac + +let solveNoteqBranch side = + tclTHEN (choose_noteq side) + (tclTHEN introf + (onLastHypId (fun id -> discrHyp id))) + +(* Constructs the type {c1=c2}+{~c1=c2} *) + +let make_eq () = +(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ()) + +let mkDecideEqGoal eqonleft op rectype c1 c2 = + let equality = mkApp(make_eq(), [|rectype; c1; c2|]) in + let disequality = mkApp(build_coq_not (), [|equality|]) in + if eqonleft then mkApp(op, [|equality; disequality |]) + else mkApp(op, [|disequality; equality |]) + + +(* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *) + +let idx = Id.of_string "x" +let idy = Id.of_string "y" + +let mkGenDecideEqGoal rectype g = + let hypnames = pf_ids_of_hyps g in + let xname = next_ident_away idx hypnames + and yname = next_ident_away idy hypnames in + (mkNamedProd xname rectype + (mkNamedProd yname rectype + (mkDecideEqGoal true (build_coq_sumbool ()) + rectype (mkVar xname) (mkVar yname)))) + +let rec rewrite_and_clear hyps = match hyps with +| [] -> Proofview.tclUNIT () +| id :: hyps -> + tclTHENLIST [ + Equality.rewriteLR (mkVar id); + clear [id]; + rewrite_and_clear hyps; + ] + +let eqCase tac = + tclTHEN intro (onLastHypId tac) + +let injHyp id = + let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in + let tac c = Equality.injClause None false (Some (None, Tacexpr.ElimOnConstr c)) in + Tacticals.New.tclDELAYEDWITHHOLES false c tac + +let diseqCase hyps eqonleft = + let diseq = Id.of_string "diseq" in + let absurd = Id.of_string "absurd" in + (tclTHEN (intro_using diseq) + (tclTHEN (choose_noteq eqonleft) + (tclTHEN (rewrite_and_clear (List.rev hyps)) + (tclTHEN (red_in_concl) + (tclTHEN (intro_using absurd) + (tclTHEN (Simple.apply (mkVar diseq)) + (tclTHEN (injHyp absurd) + (full_trivial [])))))))) + +open Proofview.Notations + +(* spiwack: a small wrapper around [Hipattern]. *) + +let match_eqdec c = + try Proofview.tclUNIT (match_eqdec c) + with PatternMatchingFailure -> Proofview.tclZERO PatternMatchingFailure + +(* /spiwack *) + +let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with +| [], [] -> + tclTHENLIST [ + choose_eq eqonleft; + rewrite_and_clear (List.rev hyps); + intros_reflexivity; + ] +| a1 :: largs, a2 :: rargs -> + Proofview.Goal.enter { enter = begin fun gl -> + let rectype = pf_unsafe_type_of gl a1 in + let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in + let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in + let subtacs = + if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto] + else [diseqCase hyps eqonleft;eqCase tac;default_auto] in + (tclTHENS (elim_type decide) subtacs) + end } +| _ -> invalid_arg "List.fold_right2" + +let solveEqBranch rectype = + Proofview.tclORELSE + begin + Proofview.Goal.enter { enter = begin fun gl -> + let concl = pf_nf_concl gl in + match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) -> + let (mib,mip) = Global.lookup_inductive rectype in + let nparams = mib.mind_nparams in + let getargs l = List.skipn nparams (snd (decompose_app l)) in + let rargs = getargs rhs + and largs = getargs lhs in + solveArg [] eqonleft op largs rargs + end } + end + begin function (e, info) -> match e with + | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!") + | e -> Proofview.tclZERO ~info e + end + +(* The tactic Decide Equality *) + +let hd_app c = match kind_of_term c with + | App (h,_) -> h + | _ -> c + +let decideGralEquality = + Proofview.tclORELSE + begin + Proofview.Goal.enter { enter = begin fun gl -> + let concl = pf_nf_concl gl in + match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) -> + let headtyp = hd_app (pf_compute gl typ) in + begin match kind_of_term headtyp with + | Ind (mi,_) -> Proofview.tclUNIT mi + | _ -> tclZEROMSG (Pp.str"This decision procedure only works for inductive objects.") + end >>= fun rectype -> + (tclTHEN + (mkBranches c1 c2) + (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype))) + end } + end + begin function (e, info) -> match e with + | PatternMatchingFailure -> + Tacticals.New.tclZEROMSG (Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}.") + | e -> Proofview.tclZERO ~info e + end + +let decideEqualityGoal = tclTHEN intros decideGralEquality + +let decideEquality rectype = + Proofview.Goal.enter { enter = begin fun gl -> + let decide = mkGenDecideEqGoal rectype gl in + (tclTHENS (cut decide) [default_auto;decideEqualityGoal]) + end } + + +(* The tactic Compare *) + +let compare c1 c2 = + Proofview.Goal.enter { enter = begin fun gl -> + let rectype = pf_unsafe_type_of gl c1 in + let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in + (tclTHENS (cut decide) + [(tclTHEN intro + (tclTHEN (onLastHyp simplest_case) clear_last)); + decideEquality rectype]) + end } diff --git a/tactics/eqdecide.mli b/tactics/eqdecide.mli new file mode 100644 index 0000000000..cb48a5bcc8 --- /dev/null +++ b/tactics/eqdecide.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Constr.t -> unit Proofview.tactic diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index bbad1d8e64..37503decc6 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -21,3 +21,4 @@ Eauto Class_tactics Tactic_matching Term_dnet +Eqdecide -- cgit v1.2.3 From 222c24ff4361f1a35b267f6b406aa7b2da56e689 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Mar 2016 10:06:00 +0100 Subject: Making Autorewrite independent from Ltac. --- ltac/autorewrite.ml | 19 +++++++++++++------ ltac/autorewrite.mli | 4 ++-- ltac/extratactics.ml4 | 2 +- ltac/rewrite.ml | 5 ++++- 4 files changed, 20 insertions(+), 10 deletions(-) diff --git a/ltac/autorewrite.ml b/ltac/autorewrite.ml index ea598b61ca..4816f8a452 100644 --- a/ltac/autorewrite.ml +++ b/ltac/autorewrite.ml @@ -27,13 +27,13 @@ type rew_rule = { rew_lemma: constr; rew_pat: constr; rew_ctx: Univ.universe_context_set; rew_l2r: bool; - rew_tac: glob_tactic_expr option } + rew_tac: Genarg.glob_generic_argument option } let subst_hint subst hint = let cst' = subst_mps subst hint.rew_lemma in let typ' = subst_mps subst hint.rew_type in let pat' = subst_mps subst hint.rew_pat in - let t' = Option.smartmap (Tacsubst.subst_tactic subst) hint.rew_tac in + let t' = Option.smartmap (Genintern.generic_substitute subst) hint.rew_tac in if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else { hint with rew_lemma = cst'; rew_type = typ'; @@ -85,10 +85,10 @@ let print_rewrite_hintdb bas = str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++ Option.cata (fun tac -> str " then use tactic " ++ - Pptactic.pr_glob_tactic (Global.env()) tac) (mt ()) h.rew_tac) + Pptactic.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) (find_rewrites bas)) -type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * raw_tactic_expr option +type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option (* Applies all the rules of one base *) let one_base general_rewrite_maybe_in tac_main bas = @@ -104,7 +104,12 @@ let one_base general_rewrite_maybe_in tac_main bas = Sigma.Unsafe.of_pair (tac, sigma) end } in let lrul = List.map (fun h -> - let tac = match h.rew_tac with None -> Proofview.tclUNIT () | Some t -> Tacinterp.eval_tactic t in + let tac = match h.rew_tac with + | None -> Proofview.tclUNIT () + | Some tac -> + let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in + Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ()) + in (h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac (ctx,csr,dir,tc) -> Tacticals.New.tclTHEN tac @@ -300,6 +305,8 @@ let add_rew_rules base lrul = let counter = ref 0 in let env = Global.env () in let sigma = Evd.from_env env in + let ist = { Genintern.ltacvars = Id.Set.empty; genv = Global.env () } in + let intern tac = snd (Genintern.generic_intern ist tac) in let lrul = List.fold_left (fun dn (loc,(c,ctx),b,t) -> @@ -308,7 +315,7 @@ let add_rew_rules base lrul = let pat = if b then info.hyp_left else info.hyp_right in let rul = { rew_lemma = c; rew_type = info.hyp_ty; rew_pat = pat; rew_ctx = ctx; rew_l2r = b; - rew_tac = Option.map Tacintern.glob_tactic t} + rew_tac = Option.map intern t} in incr counter; HintDN.add pat (!counter, rul) dn) HintDN.empty lrul in Lib.add_anonymous_leaf (inHintRewrite (base,lrul)) diff --git a/ltac/autorewrite.mli b/ltac/autorewrite.mli index 6196b04e18..ac613b57ce 100644 --- a/ltac/autorewrite.mli +++ b/ltac/autorewrite.mli @@ -11,7 +11,7 @@ open Tacexpr open Equality (** Rewriting rules before tactic interpretation *) -type raw_rew_rule = Loc.t * Term.constr Univ.in_universe_context_set * bool * Tacexpr.raw_tactic_expr option +type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option (** To add rewriting rules to a base *) val add_rew_rules : string -> raw_rew_rule list -> unit @@ -29,7 +29,7 @@ type rew_rule = { rew_lemma: constr; rew_pat: constr; rew_ctx: Univ.universe_context_set; rew_l2r: bool; - rew_tac: glob_tactic_expr option } + rew_tac: Genarg.glob_generic_argument option } val find_rewrites : string -> rew_rule list diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 96abc11999..ba9f82fb96 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -290,7 +290,7 @@ let add_rewrite_hint bases ort t lcsr = if poly then ctx else (Global.push_context_set false ctx; Univ.ContextSet.empty) in - Constrexpr_ops.constr_loc ce, (c, ctx), ort, t in + Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in let eqs = List.map f lcsr in let add_hints base = add_rew_rules base eqs in List.iter add_hints bases diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index fb04bee070..2fe2eb42a6 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -612,7 +612,10 @@ let solve_remaining_by env sigma holes by = in (** Only solve independent holes *) let indep = List.map_filter map holes in - let solve_tac = Tacticals.New.tclCOMPLETE (Tacinterp.eval_tactic tac) in + let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in + let solve_tac = Geninterp.generic_interp ist tac in + let solve_tac = Ftactic.run solve_tac (fun _ -> Proofview.tclUNIT ()) in + let solve_tac = Tacticals.New.tclCOMPLETE solve_tac in let solve sigma evk = let evi = try Some (Evd.find_undefined sigma evk) -- cgit v1.2.3 From e8114ee084cae195eb7615293cec0e28dcc0a3d8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Mar 2016 14:24:51 +0100 Subject: Moving Autorewrite back to tactics/. --- ltac/autorewrite.ml | 322 ------------------------------------------------ ltac/autorewrite.mli | 61 --------- ltac/ltac.mllib | 1 - tactics/autorewrite.ml | 322 ++++++++++++++++++++++++++++++++++++++++++++++++ tactics/autorewrite.mli | 61 +++++++++ tactics/tactics.mllib | 1 + 6 files changed, 384 insertions(+), 384 deletions(-) delete mode 100644 ltac/autorewrite.ml delete mode 100644 ltac/autorewrite.mli create mode 100644 tactics/autorewrite.ml create mode 100644 tactics/autorewrite.mli diff --git a/ltac/autorewrite.ml b/ltac/autorewrite.ml deleted file mode 100644 index 4816f8a452..0000000000 --- a/ltac/autorewrite.ml +++ /dev/null @@ -1,322 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - errorlabstrm "AutoRewrite" - (str "Rewriting base " ++ str bas ++ str " does not exist.") - -let find_rewrites bas = - List.rev_map snd (HintDN.find_all (find_base bas)) - -let find_matches bas pat = - let base = find_base bas in - let res = HintDN.search_pattern base pat in - List.map snd res - -let print_rewrite_hintdb bas = - (str "Database " ++ str bas ++ fnl () ++ - prlist_with_sep fnl - (fun h -> - str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ - Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++ - Option.cata (fun tac -> str " then use tactic " ++ - Pptactic.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) - (find_rewrites bas)) - -type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option - -(* Applies all the rules of one base *) -let one_base general_rewrite_maybe_in tac_main bas = - let lrul = find_rewrites bas in - let try_rewrite dir ctx c tc = - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in - let c' = Vars.subst_univs_level_constr subst c in - let sigma = Sigma.to_evar_map sigma in - let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in - let tac = general_rewrite_maybe_in dir c' tc in - Sigma.Unsafe.of_pair (tac, sigma) - end } in - let lrul = List.map (fun h -> - let tac = match h.rew_tac with - | None -> Proofview.tclUNIT () - | Some tac -> - let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in - Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ()) - in - (h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in - Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac (ctx,csr,dir,tc) -> - Tacticals.New.tclTHEN tac - (Tacticals.New.tclREPEAT_MAIN - (Tacticals.New.tclTHENFIRST (try_rewrite dir ctx csr tc) tac_main))) - (Proofview.tclUNIT()) lrul)) - -(* The AutoRewrite tactic *) -let autorewrite ?(conds=Naive) tac_main lbas = - Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS - (List.fold_left (fun tac bas -> - Tacticals.New.tclTHEN tac - (one_base (fun dir c tac -> - let tac = (tac, conds) in - general_rewrite dir AllOccurrences true false ~tac c) - tac_main bas)) - (Proofview.tclUNIT()) lbas)) - -let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = - Proofview.Goal.nf_enter { enter = begin fun gl -> - (* let's check at once if id exists (to raise the appropriate error) *) - let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in - let general_rewrite_in id = - let id = ref id in - let to_be_cleared = ref false in - fun dir cstr tac gl -> - let last_hyp_id = - match Tacmach.pf_hyps gl with - d :: _ -> Context.Named.Declaration.get_id d - | _ -> (* even the hypothesis id is missing *) - raise (Logic.RefinerError (Logic.NoSuchHyp !id)) - in - let gl' = Proofview.V82.of_tactic (general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false !id cstr false) gl in - let gls = gl'.Evd.it in - match gls with - g::_ -> - (match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with - d ::_ -> - let lastid = Context.Named.Declaration.get_id d in - if not (Id.equal last_hyp_id lastid) then - begin - let gl'' = - if !to_be_cleared then - tclTHEN (fun _ -> gl') (tclTRY (clear [!id])) gl - else gl' in - id := lastid ; - to_be_cleared := true ; - gl'' - end - else - begin - to_be_cleared := false ; - gl' - end - | _ -> assert false) (* there must be at least an hypothesis *) - | _ -> assert false (* rewriting cannot complete a proof *) - in - let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y z w) in - Tacticals.New.tclMAP (fun id -> - Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS - (List.fold_left (fun tac bas -> - Tacticals.New.tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) (Proofview.tclUNIT()) lbas))) - idl - end } - -let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id] - -let gen_auto_multi_rewrite conds tac_main lbas cl = - let try_do_hyps treat_id l = - autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas - in - if cl.concl_occs != AllOccurrences && - cl.concl_occs != NoOccurrences - then - Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.") - else - let compose_tac t1 t2 = - match cl.onhyps with - | Some [] -> t1 - | _ -> Tacticals.New.tclTHENFIRST t1 t2 - in - compose_tac - (if cl.concl_occs != NoOccurrences then autorewrite ~conds tac_main lbas else Proofview.tclUNIT ()) - (match cl.onhyps with - | Some l -> try_do_hyps (fun ((_,id),_) -> id) l - | None -> - (* try to rewrite in all hypothesis - (except maybe the rewritten one) *) - Proofview.Goal.nf_enter { enter = begin fun gl -> - let ids = Tacmach.New.pf_ids_of_hyps gl in - try_do_hyps (fun id -> id) ids - end }) - -let auto_multi_rewrite ?(conds=Naive) lems cl = - Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds (Proofview.tclUNIT()) lems cl) - -let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl = - let onconcl = match cl.Locus.concl_occs with NoOccurrences -> false | _ -> true in - match onconcl,cl.Locus.onhyps with - | false,Some [_] | true,Some [] | false,Some [] -> - (* autorewrite with .... in clause using tac n'est sur que - si clause represente soit le but soit UNE hypothese - *) - Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds tac_main lbas cl) - | _ -> - Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.") - -(* Functions necessary to the library object declaration *) -let cache_hintrewrite (_,(rbase,lrl)) = - let base = try raw_find_base rbase with Not_found -> HintDN.empty in - let max = try fst (Util.List.last (HintDN.find_all base)) with Failure _ -> 0 - in - let lrl = HintDN.refresh_metas lrl in - let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in - rewtab:=String.Map.add rbase (HintDN.union lrl base) !rewtab - - -let subst_hintrewrite (subst,(rbase,list as node)) = - let list' = HintDN.subst subst list in - if list' == list then node else - (rbase,list') - -let classify_hintrewrite x = Libobject.Substitute x - - -(* Declaration of the Hint Rewrite library object *) -let inHintRewrite : string * HintDN.t -> Libobject.obj = - Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with - Libobject.cache_function = cache_hintrewrite; - Libobject.load_function = (fun _ -> cache_hintrewrite); - Libobject.subst_function = subst_hintrewrite; - Libobject.classify_function = classify_hintrewrite } - - -open Clenv - -type hypinfo = { - hyp_cl : clausenv; - hyp_prf : constr; - hyp_ty : types; - hyp_car : constr; - hyp_rel : constr; - hyp_l2r : bool; - hyp_left : constr; - hyp_right : constr; -} - -let decompose_applied_relation metas env sigma c ctype left2right = - let find_rel ty = - let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in - let eqclause = - if metas then eqclause - else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd) - in - let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in - let rec split_last_two = function - | [c1;c2] -> [],(c1, c2) - | x::y::z -> - let l,res = split_last_two (y::z) in x::l, res - | _ -> raise Not_found - in - try - let others,(c1,c2) = split_last_two args in - let ty1, ty2 = - Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 - in -(* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) -(* else *) - Some { hyp_cl=eqclause; hyp_prf=(Clenv.clenv_value eqclause); hyp_ty = ty; - hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others); - hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; } - with Not_found -> None - in - match find_rel ctype with - | Some c -> Some c - | None -> - let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *) - match find_rel (it_mkProd_or_LetIn t' ctx) with - | Some c -> Some c - | None -> None - -let find_applied_relation metas loc env sigma c left2right = - let ctype = Typing.unsafe_type_of env sigma c in - match decompose_applied_relation metas env sigma c ctype left2right with - | Some c -> c - | None -> - user_err_loc (loc, "decompose_applied_relation", - str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++ - spc () ++ str"of this term does not end with an applied relation.") - -(* To add rewriting rules to a base *) -let add_rew_rules base lrul = - let counter = ref 0 in - let env = Global.env () in - let sigma = Evd.from_env env in - let ist = { Genintern.ltacvars = Id.Set.empty; genv = Global.env () } in - let intern tac = snd (Genintern.generic_intern ist tac) in - let lrul = - List.fold_left - (fun dn (loc,(c,ctx),b,t) -> - let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in - let info = find_applied_relation false loc env sigma c b in - let pat = if b then info.hyp_left else info.hyp_right in - let rul = { rew_lemma = c; rew_type = info.hyp_ty; - rew_pat = pat; rew_ctx = ctx; rew_l2r = b; - rew_tac = Option.map intern t} - in incr counter; - HintDN.add pat (!counter, rul) dn) HintDN.empty lrul - in Lib.add_anonymous_leaf (inHintRewrite (base,lrul)) - diff --git a/ltac/autorewrite.mli b/ltac/autorewrite.mli deleted file mode 100644 index ac613b57ce..0000000000 --- a/ltac/autorewrite.mli +++ /dev/null @@ -1,61 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* raw_rew_rule list -> unit - -(** The AutoRewrite tactic. - The optional conditions tell rewrite how to handle matching and side-condition solving. - Default is Naive: first match in the clause, don't look at the side-conditions to - tell if the rewrite succeeded. *) -val autorewrite : ?conds:conditions -> unit Proofview.tactic -> string list -> unit Proofview.tactic -val autorewrite_in : ?conds:conditions -> Names.Id.t -> unit Proofview.tactic -> string list -> unit Proofview.tactic - -(** Rewriting rules *) -type rew_rule = { rew_lemma: constr; - rew_type: types; - rew_pat: constr; - rew_ctx: Univ.universe_context_set; - rew_l2r: bool; - rew_tac: Genarg.glob_generic_argument option } - -val find_rewrites : string -> rew_rule list - -val find_matches : string -> constr -> rew_rule list - -val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> unit Proofview.tactic - -val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic - -val print_rewrite_hintdb : string -> Pp.std_ppcmds - -open Clenv - - -type hypinfo = { - hyp_cl : clausenv; - hyp_prf : constr; - hyp_ty : types; - hyp_car : constr; - hyp_rel : constr; - hyp_l2r : bool; - hyp_left : constr; - hyp_right : constr; -} - -val find_applied_relation : bool -> - Loc.t -> - Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo - diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index 28bfa5aa0a..e0c6f3ac0a 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -9,7 +9,6 @@ Tactic_option Extraargs G_obligations Coretactics -Autorewrite Extratactics G_auto G_class diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml new file mode 100644 index 0000000000..4816f8a452 --- /dev/null +++ b/tactics/autorewrite.ml @@ -0,0 +1,322 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + errorlabstrm "AutoRewrite" + (str "Rewriting base " ++ str bas ++ str " does not exist.") + +let find_rewrites bas = + List.rev_map snd (HintDN.find_all (find_base bas)) + +let find_matches bas pat = + let base = find_base bas in + let res = HintDN.search_pattern base pat in + List.map snd res + +let print_rewrite_hintdb bas = + (str "Database " ++ str bas ++ fnl () ++ + prlist_with_sep fnl + (fun h -> + str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ + Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++ + Option.cata (fun tac -> str " then use tactic " ++ + Pptactic.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac) + (find_rewrites bas)) + +type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option + +(* Applies all the rules of one base *) +let one_base general_rewrite_maybe_in tac_main bas = + let lrul = find_rewrites bas in + let try_rewrite dir ctx c tc = + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in + let c' = Vars.subst_univs_level_constr subst c in + let sigma = Sigma.to_evar_map sigma in + let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in + let tac = general_rewrite_maybe_in dir c' tc in + Sigma.Unsafe.of_pair (tac, sigma) + end } in + let lrul = List.map (fun h -> + let tac = match h.rew_tac with + | None -> Proofview.tclUNIT () + | Some tac -> + let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in + Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ()) + in + (h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in + Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac (ctx,csr,dir,tc) -> + Tacticals.New.tclTHEN tac + (Tacticals.New.tclREPEAT_MAIN + (Tacticals.New.tclTHENFIRST (try_rewrite dir ctx csr tc) tac_main))) + (Proofview.tclUNIT()) lrul)) + +(* The AutoRewrite tactic *) +let autorewrite ?(conds=Naive) tac_main lbas = + Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS + (List.fold_left (fun tac bas -> + Tacticals.New.tclTHEN tac + (one_base (fun dir c tac -> + let tac = (tac, conds) in + general_rewrite dir AllOccurrences true false ~tac c) + tac_main bas)) + (Proofview.tclUNIT()) lbas)) + +let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = + Proofview.Goal.nf_enter { enter = begin fun gl -> + (* let's check at once if id exists (to raise the appropriate error) *) + let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in + let general_rewrite_in id = + let id = ref id in + let to_be_cleared = ref false in + fun dir cstr tac gl -> + let last_hyp_id = + match Tacmach.pf_hyps gl with + d :: _ -> Context.Named.Declaration.get_id d + | _ -> (* even the hypothesis id is missing *) + raise (Logic.RefinerError (Logic.NoSuchHyp !id)) + in + let gl' = Proofview.V82.of_tactic (general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false !id cstr false) gl in + let gls = gl'.Evd.it in + match gls with + g::_ -> + (match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with + d ::_ -> + let lastid = Context.Named.Declaration.get_id d in + if not (Id.equal last_hyp_id lastid) then + begin + let gl'' = + if !to_be_cleared then + tclTHEN (fun _ -> gl') (tclTRY (clear [!id])) gl + else gl' in + id := lastid ; + to_be_cleared := true ; + gl'' + end + else + begin + to_be_cleared := false ; + gl' + end + | _ -> assert false) (* there must be at least an hypothesis *) + | _ -> assert false (* rewriting cannot complete a proof *) + in + let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y z w) in + Tacticals.New.tclMAP (fun id -> + Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS + (List.fold_left (fun tac bas -> + Tacticals.New.tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) (Proofview.tclUNIT()) lbas))) + idl + end } + +let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id] + +let gen_auto_multi_rewrite conds tac_main lbas cl = + let try_do_hyps treat_id l = + autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas + in + if cl.concl_occs != AllOccurrences && + cl.concl_occs != NoOccurrences + then + Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.") + else + let compose_tac t1 t2 = + match cl.onhyps with + | Some [] -> t1 + | _ -> Tacticals.New.tclTHENFIRST t1 t2 + in + compose_tac + (if cl.concl_occs != NoOccurrences then autorewrite ~conds tac_main lbas else Proofview.tclUNIT ()) + (match cl.onhyps with + | Some l -> try_do_hyps (fun ((_,id),_) -> id) l + | None -> + (* try to rewrite in all hypothesis + (except maybe the rewritten one) *) + Proofview.Goal.nf_enter { enter = begin fun gl -> + let ids = Tacmach.New.pf_ids_of_hyps gl in + try_do_hyps (fun id -> id) ids + end }) + +let auto_multi_rewrite ?(conds=Naive) lems cl = + Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds (Proofview.tclUNIT()) lems cl) + +let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl = + let onconcl = match cl.Locus.concl_occs with NoOccurrences -> false | _ -> true in + match onconcl,cl.Locus.onhyps with + | false,Some [_] | true,Some [] | false,Some [] -> + (* autorewrite with .... in clause using tac n'est sur que + si clause represente soit le but soit UNE hypothese + *) + Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds tac_main lbas cl) + | _ -> + Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.") + +(* Functions necessary to the library object declaration *) +let cache_hintrewrite (_,(rbase,lrl)) = + let base = try raw_find_base rbase with Not_found -> HintDN.empty in + let max = try fst (Util.List.last (HintDN.find_all base)) with Failure _ -> 0 + in + let lrl = HintDN.refresh_metas lrl in + let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in + rewtab:=String.Map.add rbase (HintDN.union lrl base) !rewtab + + +let subst_hintrewrite (subst,(rbase,list as node)) = + let list' = HintDN.subst subst list in + if list' == list then node else + (rbase,list') + +let classify_hintrewrite x = Libobject.Substitute x + + +(* Declaration of the Hint Rewrite library object *) +let inHintRewrite : string * HintDN.t -> Libobject.obj = + Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with + Libobject.cache_function = cache_hintrewrite; + Libobject.load_function = (fun _ -> cache_hintrewrite); + Libobject.subst_function = subst_hintrewrite; + Libobject.classify_function = classify_hintrewrite } + + +open Clenv + +type hypinfo = { + hyp_cl : clausenv; + hyp_prf : constr; + hyp_ty : types; + hyp_car : constr; + hyp_rel : constr; + hyp_l2r : bool; + hyp_left : constr; + hyp_right : constr; +} + +let decompose_applied_relation metas env sigma c ctype left2right = + let find_rel ty = + let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in + let eqclause = + if metas then eqclause + else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd) + in + let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in + let rec split_last_two = function + | [c1;c2] -> [],(c1, c2) + | x::y::z -> + let l,res = split_last_two (y::z) in x::l, res + | _ -> raise Not_found + in + try + let others,(c1,c2) = split_last_two args in + let ty1, ty2 = + Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 + in +(* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) +(* else *) + Some { hyp_cl=eqclause; hyp_prf=(Clenv.clenv_value eqclause); hyp_ty = ty; + hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others); + hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; } + with Not_found -> None + in + match find_rel ctype with + | Some c -> Some c + | None -> + let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *) + match find_rel (it_mkProd_or_LetIn t' ctx) with + | Some c -> Some c + | None -> None + +let find_applied_relation metas loc env sigma c left2right = + let ctype = Typing.unsafe_type_of env sigma c in + match decompose_applied_relation metas env sigma c ctype left2right with + | Some c -> c + | None -> + user_err_loc (loc, "decompose_applied_relation", + str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++ + spc () ++ str"of this term does not end with an applied relation.") + +(* To add rewriting rules to a base *) +let add_rew_rules base lrul = + let counter = ref 0 in + let env = Global.env () in + let sigma = Evd.from_env env in + let ist = { Genintern.ltacvars = Id.Set.empty; genv = Global.env () } in + let intern tac = snd (Genintern.generic_intern ist tac) in + let lrul = + List.fold_left + (fun dn (loc,(c,ctx),b,t) -> + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in + let info = find_applied_relation false loc env sigma c b in + let pat = if b then info.hyp_left else info.hyp_right in + let rul = { rew_lemma = c; rew_type = info.hyp_ty; + rew_pat = pat; rew_ctx = ctx; rew_l2r = b; + rew_tac = Option.map intern t} + in incr counter; + HintDN.add pat (!counter, rul) dn) HintDN.empty lrul + in Lib.add_anonymous_leaf (inHintRewrite (base,lrul)) + diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli new file mode 100644 index 0000000000..ac613b57ce --- /dev/null +++ b/tactics/autorewrite.mli @@ -0,0 +1,61 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* raw_rew_rule list -> unit + +(** The AutoRewrite tactic. + The optional conditions tell rewrite how to handle matching and side-condition solving. + Default is Naive: first match in the clause, don't look at the side-conditions to + tell if the rewrite succeeded. *) +val autorewrite : ?conds:conditions -> unit Proofview.tactic -> string list -> unit Proofview.tactic +val autorewrite_in : ?conds:conditions -> Names.Id.t -> unit Proofview.tactic -> string list -> unit Proofview.tactic + +(** Rewriting rules *) +type rew_rule = { rew_lemma: constr; + rew_type: types; + rew_pat: constr; + rew_ctx: Univ.universe_context_set; + rew_l2r: bool; + rew_tac: Genarg.glob_generic_argument option } + +val find_rewrites : string -> rew_rule list + +val find_matches : string -> constr -> rew_rule list + +val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> unit Proofview.tactic + +val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic + +val print_rewrite_hintdb : string -> Pp.std_ppcmds + +open Clenv + + +type hypinfo = { + hyp_cl : clausenv; + hyp_prf : constr; + hyp_ty : types; + hyp_car : constr; + hyp_rel : constr; + hyp_l2r : bool; + hyp_left : constr; + hyp_right : constr; +} + +val find_applied_relation : bool -> + Loc.t -> + Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo + diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 37503decc6..ab8069225d 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -22,3 +22,4 @@ Class_tactics Tactic_matching Term_dnet Eqdecide +Autorewrite -- cgit v1.2.3