diff options
Diffstat (limited to 'tactics/eauto.ml4')
-rw-r--r-- | tactics/eauto.ml4 | 151 |
1 files changed, 71 insertions, 80 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 568b1d17c..6117c8b43 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -28,33 +28,51 @@ open Misctypes open Locus open Locusops open Hints +open Proofview.Notations DECLARE PLUGIN "eauto" let eauto_unif_flags = auto_flags_of_state full_transparent_state -let e_give_exact ?(flags=eauto_unif_flags) c gl = - let t1 = (pf_unsafe_type_of gl c) and t2 = pf_concl gl in +let e_give_exact ?(flags=eauto_unif_flags) c = + Proofview.Goal.nf_enter { enter = begin fun gl -> + 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 - tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl - else Proofview.V82.of_tactic (exact_check c) gl + 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 gl = - tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl +let e_assumption = + Proofview.Goal.enter { enter = begin fun gl -> + Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl)) + end } TACTIC EXTEND eassumption -| [ "eassumption" ] -> [ Proofview.V82.tactic e_assumption ] +| [ "eassumption" ] -> [ e_assumption ] END TACTIC EXTEND eexact -| [ "eexact" constr(c) ] -> [ Proofview.V82.tactic (e_give_exact c) ] +| [ "eexact" constr(c) ] -> [ e_give_exact c ] END -let registered_e_assumption gl = - tclFIRST (List.map (fun id gl -> e_give_exact (mkVar id) gl) - (pf_ids_of_hyps gl)) gl +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 -> Tacinterp.type_uconstr ~flags ist c) cs (************************************************************************) (* PROLOG tactic *) @@ -83,7 +101,7 @@ 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 assumption (pf_ids_of_hyps gl)) + @ (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"; @@ -95,18 +113,19 @@ let out_term = function | IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr) let prolog_tac l n gl = - let l = List.map (fun x -> out_term (pf_apply (prepare_hint false (false,true)) gl x)) l in - let n = - match n with - | ArgArg n -> n - | _ -> error "Prolog called with a non closed argument." + 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.") TACTIC EXTEND prolog -| [ "prolog" "[" open_constr_list(l) "]" int_or_var(n) ] -> [ Proofview.V82.tactic (prolog_tac l n) ] +| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] -> + [ Proofview.V82.tactic (prolog_tac (eval_uconstrs ist l) n) ] END open Auto @@ -119,15 +138,14 @@ open Unification 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 begin - fun gl -> + 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 + end } let hintmap_of hdc concl = match hdc with @@ -143,19 +161,21 @@ let e_exact poly flags (c,clenv) = 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 goal = + +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 :: - (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 fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) + (Tacticals.New.tclTHEN Tactics.intro next) :: + (List.map fst (e_trivial_resolve db_list local_db (Tacmach.New.pf_nf_concl gl))) in - tclFIRST (List.map tclCOMPLETE tacl) goal + 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 @@ -174,14 +194,14 @@ and e_my_find_search db_list local_db hdc concl = 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) -> Proofview.V82.tactic (e_exact poly st (c,cl)) + | Give_exact (c,cl) -> e_exact poly st (c,cl) | Res_pf_THEN_trivial_fail (term,cl) -> - Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (unify_e_resolve poly st (term,cl))) - (e_trivial_fail_db db_list local_db)) + Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl)) + (e_trivial_fail_db db_list local_db) | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl) | Extern tacast -> conclPattern concl p tacast in - let tac = Proofview.V82.of_tactic (run_hint t tac) in + let tac = run_hint t tac in (tac, lazy (pr_hint t))) in List.map tac_of_hint hintl @@ -210,7 +230,7 @@ type search_state = { dblist : hint_db list; localdb : hint_db list; prev : prev_search_state; - local_lemmas : Evd.open_constr list; + local_lemmas : Tacexpr.delayed_open_constr list; } and prev_search_state = (* for info eauto *) @@ -234,7 +254,7 @@ module SearchProblem = struct | [] -> [] | (tac, cost, pptac) :: tacl -> try - let lgls = apply_tac_list tac glls in + 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 @@ -272,7 +292,7 @@ module SearchProblem = struct prev = ps; local_lemmas = s.local_lemmas}) l in let intro_tac = - let l = filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro, (-1), lazy (str "intro")] in + 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 @@ -427,77 +447,48 @@ let gen_eauto ?(debug=Off) np lems = function let make_depth = function | None -> !default_search_depth - | Some (ArgArg d) -> d - | _ -> error "eauto called with a non closed argument." + | Some d -> d let make_dimension n = function | None -> (true,make_depth n) - | Some (ArgArg d) -> (false,d) - | _ -> error "eauto called with a non closed argument." + | Some d -> (false,d) open Genarg +open G_auto -(* Hint bases *) - -let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases - -ARGUMENT EXTEND hintbases - TYPED AS preident_list_opt - PRINTED BY pr_hintbases -| [ "with" "*" ] -> [ None ] -| [ "with" ne_preident_list(l) ] -> [ Some l ] -| [ ] -> [ Some [] ] -END - -let pr_constr_coma_sequence prc _ _ = - prlist_with_sep pr_comma (fun (_,c) -> prc c) - -ARGUMENT EXTEND constr_coma_sequence - TYPED AS open_constr_list - PRINTED BY pr_constr_coma_sequence -| [ open_constr(c) "," constr_coma_sequence(l) ] -> [ c::l ] -| [ open_constr(c) ] -> [ [c] ] -END - -let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using (fun (_,c) -> prc c) - -ARGUMENT EXTEND auto_using - TYPED AS open_constr_list - PRINTED BY pr_auto_using -| [ "using" constr_coma_sequence(l) ] -> [ l ] -| [ ] -> [ [] ] -END +let hintbases = G_auto.hintbases +let wit_hintbases = G_auto.wit_hintbases TACTIC EXTEND eauto | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - [ Proofview.V82.tactic (gen_eauto (make_dimension n p) lems db) ] + [ Proofview.V82.tactic (gen_eauto (make_dimension n p) (eval_uconstrs ist lems) db) ] END TACTIC EXTEND new_eauto | [ "new" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> [ match db with - | None -> new_full_auto (make_depth n) lems - | Some l -> new_auto (make_depth n) lems l ] + | None -> new_full_auto (make_depth n) (eval_uconstrs ist lems) + | Some l -> new_auto (make_depth n) (eval_uconstrs ist lems) l ] END TACTIC EXTEND debug_eauto | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - [ Proofview.V82.tactic (gen_eauto ~debug:Debug (make_dimension n p) lems db) ] + [ Proofview.V82.tactic (gen_eauto ~debug:Debug (make_dimension n p) (eval_uconstrs ist lems) db) ] END TACTIC EXTEND info_eauto | [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - [ Proofview.V82.tactic (gen_eauto ~debug:Info (make_dimension n p) lems db) ] + [ Proofview.V82.tactic (gen_eauto ~debug:Info (make_dimension n p) (eval_uconstrs ist lems) db) ] END TACTIC EXTEND dfs_eauto | [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - [ Proofview.V82.tactic (gen_eauto (true, make_depth p) lems db) ] + [ Proofview.V82.tactic (gen_eauto (true, make_depth p) (eval_uconstrs ist lems) db) ] END let cons a l = a :: l @@ -567,7 +558,7 @@ let unfold_head env (ids, csts) c = in aux c let autounfold_one db cl = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let st = @@ -586,7 +577,7 @@ let autounfold_one db cl = | 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 + end } (* Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *) (* (Id.Set.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *) |