diff options
Diffstat (limited to 'tactics/eauto.ml4')
-rw-r--r-- | tactics/eauto.ml4 | 272 |
1 files changed, 163 insertions, 109 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 144100c9..30c5e686 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -1,40 +1,42 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4deps: "grammar/grammar.cma" i*) open Pp +open Errors open Util open Names open Nameops open Term open Termops -open Sign -open Reduction open Proof_type -open Declarations open Tacticals open Tacmach -open Evar_refiner open Tactics -open Pattern +open Patternops open Clenv open Auto -open Glob_term -open Hiddentac +open Genredexpr open Tacexpr +open Misctypes +open Locus +open Locusops +open Hints -let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state } +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_type_of gl c) and t2 = pf_concl gl in - if occur_existential t1 or occur_existential t2 then - tclTHEN (Clenvtac.unify ~flags t1) (exact_check c) gl - else exact_check c gl + 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 let assumption id = e_give_exact (mkVar id) @@ -42,11 +44,11 @@ let e_assumption gl = tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl TACTIC EXTEND eassumption -| [ "eassumption" ] -> [ e_assumption ] +| [ "eassumption" ] -> [ Proofview.V82.tactic e_assumption ] END TACTIC EXTEND eexact -| [ "eexact" constr(c) ] -> [ e_give_exact c ] +| [ "eexact" constr(c) ] -> [ Proofview.V82.tactic (e_give_exact c) ] END let registered_e_assumption gl = @@ -57,10 +59,29 @@ let registered_e_assumption gl = (* 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 = - [Tactics.intro] - @ (List.map h_simplest_eapply (List.map mkVar (pf_ids_of_hyps gl))) - @ (List.map h_simplest_eapply l) + [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)) let rec prolog l n gl = @@ -68,11 +89,15 @@ let rec prolog l n gl = 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 gl = - let l = List.map (prepare_hint (pf_env gl)) l in + let l = List.map (fun x -> out_term (pf_apply (prepare_hint false) gl x)) l in let n = match n with - | ArgArg n -> n + | ArgArg n -> n | _ -> error "Prolog called with a non closed argument." in try (prolog l n gl) @@ -80,7 +105,7 @@ let prolog_tac l n gl = errorlabstrm "Prolog.prolog" (str "Prolog failed.") TACTIC EXTEND prolog -| [ "prolog" "[" open_constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ] +| [ "prolog" "[" open_constr_list(l) "]" int_or_var(n) ] -> [ Proofview.V82.tactic (prolog_tac l n) ] END open Auto @@ -90,17 +115,26 @@ 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,_) -> pr = 0) l) - -let unify_e_resolve flags (c,clenv) gls = - let clenv' = connect_clenv gls clenv in - let _ = clenv_unique_resolver ~flags clenv' gls in - h_simplest_eapply c gls - +let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l) + +let unify_e_resolve poly flags (c,clenv) gls = + let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv + else clenv, Univ.empty_level_subst in + let clenv' = connect_clenv gls clenv' in + 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 (Vars.subst_univs_level_constr subst c))) gls + +let e_exact poly flags (c,clenv) = + 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 goal = let tacl = registered_e_assumption :: - (tclTHEN Tactics.intro + (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 @@ -108,43 +142,35 @@ let rec e_trivial_fail_db db_list local_db goal = (Hint_db.add_list hintl local_db) g'))) :: (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) in - tclFIRST (List.map tclCOMPLETE tacl) goal + tclFIRST (List.map tclCOMPLETE tacl) goal and e_my_find_search db_list local_db hdc concl = - let hdc = head_of_constr_reference hdc in let hintl = if occur_existential concl then - list_map_append (fun db -> - let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in - List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list) + List.map_append (fun db -> + let flags = auto_flags_of_state (Hint_db.transparent_state db) in + List.map (fun x -> flags, x) (Hint_db.map_existential hdc concl db) + (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)) (local_db::db_list) else - list_map_append (fun db -> - let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in - List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) + List.map_append (fun db -> + let flags = auto_flags_of_state (Hint_db.transparent_state db) in + List.map (fun x -> flags, x) (Hint_db.map_auto hdc concl db)) (local_db::db_list) in let tac_of_hint = - fun (st, {pri=b; pat = p; code=t}) -> + fun (st, {pri = b; pat = p; code = t; poly = poly}) -> (b, let tac = match t with - | Res_pf (term,cl) -> unify_resolve st (term,cl) - | ERes_pf (term,cl) -> unify_e_resolve st (term,cl) - | Give_exact (c) -> e_give_exact c + | Res_pf (term,cl) -> Proofview.V82.of_tactic (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) -> - tclTHEN (unify_e_resolve st (term,cl)) + tclTHEN (unify_e_resolve poly st (term,cl)) (e_trivial_fail_db db_list local_db) - | Unfold_nth c -> h_reduce (Unfold [all_occurrences_expr,c]) onConcl - | Extern tacast -> conclPattern concl p tacast + | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl + | Extern tacast -> Proofview.V82.of_tactic (conclPattern concl p tacast) in (tac,lazy (pr_autotactic t))) - (*i - fun gls -> pPNL (pr_autotactic t); Format.print_flush (); - try tac gls - with e when Logic.catchable_exception(e) -> - (Format.print_string "Fail\n"; - Format.print_flush (); - raise e) - i*) in List.map tac_of_hint hintl @@ -152,13 +178,13 @@ and e_trivial_resolve db_list local_db gl = try priority (e_my_find_search db_list local_db - (fst (head_constr_bound gl)) gl) + (decompose_app_bound gl) gl) with Bound | Not_found -> [] let e_possible_resolve db_list local_db gl = try List.map snd (e_my_find_search db_list local_db - (fst (head_constr_bound gl)) gl) + (decompose_app_bound gl) gl) with Bound | Not_found -> [] let find_first_goal gls = @@ -171,8 +197,8 @@ type search_state = { depth : int; (*r depth of search before failing *) tacres : goal list sigma; last_tactic : std_ppcmds Lazy.t; - dblist : Auto.hint_db list; - localdb : Auto.hint_db list; + dblist : hint_db list; + localdb : hint_db list; prev : prev_search_state } @@ -185,13 +211,9 @@ module SearchProblem = struct type state = search_state - let success s = (sig_it s.tacres) = [] + 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 pr_goals gls = - let evars = Evarutil.nf_evar_map (Refiner.project gls) in - prlist (pr_ev evars) (sig_it gls) +(* 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 *) @@ -206,6 +228,7 @@ module SearchProblem = struct (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) (lgls,pptac) :: aux tacl with e when Errors.noncritical e -> + let e = Errors.push e in Refiner.catch_failerror e; aux tacl in aux l @@ -214,13 +237,13 @@ module SearchProblem = struct let compare s s' = let d = s'.depth - s.depth in let nbgoals s = List.length (sig_it s.tacres) in - if d <> 0 then d else nbgoals s - nbgoals s' + if not (Int.equal d 0) then d else nbgoals s - nbgoals s' let branching s = - if s.depth = 0 then + if Int.equal s.depth 0 then [] else - let ps = if s.prev = Unknown then Unknown else State s in + 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); @@ -249,7 +272,7 @@ module SearchProblem = struct { depth = s.depth; tacres = res; last_tactic = pp; dblist = s.dblist; localdb = ldb :: List.tl s.localdb; prev = ps }) - (filter_tactics s.tacres [Tactics.intro,lazy (str "intro")]) + (filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro,lazy (str "intro")]) in let rec_tacs = let l = @@ -262,10 +285,18 @@ module SearchProblem = struct { depth = s.depth; tacres = res; last_tactic = pp; prev = ps; dblist = s.dblist; localdb = List.tl s.localdb } else - { depth = pred s.depth; tacres = res; - dblist = s.dblist; last_tactic = pp; prev = ps; - localdb = - list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb }) + 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 []) + (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls)) + in + { depth = pred s.depth; tacres = res; + dblist = s.dblist; last_tactic = pp; prev = ps; + localdb = newlocal @ List.tl s.localdb }) l in List.sort compare (assumption_tacs @ intro_tac @ rec_tacs) @@ -301,8 +332,8 @@ let _ = 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 + if d == Debug || !global_debug_eauto then Debug + else if d == Info || !global_info_eauto then Info else Off let pr_info_nop = function @@ -315,7 +346,7 @@ let pr_dbg_header = function | Info -> msg_debug (str "(* info eauto : *)") let pr_info dbg s = - if dbg <> Info then () + if dbg != Info then () else let rec loop s = match s.prev with @@ -336,11 +367,11 @@ let make_initial_state dbg n gl dblist localdb = last_tactic = lazy (mt()); dblist = dblist; localdb = [localdb]; - prev = if dbg=Info then Init else Unknown; + prev = if dbg == Info then Init else Unknown; } let e_search_auto debug (in_depth,p) lems db_list gl = - let local_db = make_local_hint_db ~ts:full_transparent_state true lems gl in + 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 @@ -357,7 +388,8 @@ let e_search_auto debug (in_depth,p) lems db_list gl = pr_info_nop d; error "eauto: search failed" -open Evd +(* 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) @@ -368,8 +400,8 @@ let eauto ?(debug=Off) np lems dbnames = let full_eauto ?(debug=Off) n lems gl = let dbnames = current_db_names () in - let dbnames = list_remove "v62" dbnames in - let db_list = List.map searchtable_map dbnames 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 @@ -422,7 +454,7 @@ END TACTIC EXTEND eauto | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - [ gen_eauto (make_dimension n p) lems db ] + [ Proofview.V82.tactic (gen_eauto (make_dimension n p) lems db) ] END TACTIC EXTEND new_eauto @@ -436,64 +468,70 @@ END TACTIC EXTEND debug_eauto | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - [ gen_eauto ~debug:Debug (make_dimension n p) lems db ] + [ Proofview.V82.tactic (gen_eauto ~debug:Debug (make_dimension n p) lems db) ] END TACTIC EXTEND info_eauto | [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - [ gen_eauto ~debug:Info (make_dimension n p) lems db ] + [ Proofview.V82.tactic (gen_eauto ~debug:Info (make_dimension n p) lems db) ] END TACTIC EXTEND dfs_eauto | [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - [ gen_eauto (true, make_depth p) lems db ] + [ Proofview.V82.tactic (gen_eauto (true, make_depth p) lems db) ] END let cons a l = a :: l -let autounfolds db occs = +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 - Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts - (Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) - in unfold_option unfolds + 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 unfold_option unfolds cls gl let autounfold db cls gl = - let cls = concrete_clause_of cls gl in + 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 -open Extraargs +let autounfold_tac db cls gl = + let dbs = match db with + | None -> String.Set.elements (current_db_names ()) + | Some [] -> ["core"] + | Some l -> l + in + autounfold dbs cls gl TACTIC EXTEND autounfold -| [ "autounfold" hintbases(db) in_arg_hyp(id) ] -> - [ autounfold (match db with None -> Auto.current_db_names () | Some [] -> ["core"] | Some x -> x) - (glob_in_arg_hyp_to_clause id) ] +| [ "autounfold" hintbases(db) clause(cl) ] -> [ Proofview.V82.tactic (autounfold_tac db cl) ] END let unfold_head env (ids, csts) c = let rec aux c = match kind_of_term c with - | Var id when Idset.mem id ids -> + | Var id when Id.Set.mem id ids -> (match Environ.named_body id env with | Some b -> true, b | None -> false, c) - | Const cst when Cset.mem cst csts -> - true, Environ.constant_value env cst + | 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 -> + 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 @@ -511,24 +549,30 @@ let unfold_head env (ids, csts) c = in !done_, c' in aux c -let autounfold_one db cl gl = +let autounfold_one db cl = + Proofview.Goal.nf_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 - (Idset.union ids i, Cset.union csts c)) (Idset.empty, Cset.empty) db + (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 - let did, c' = unfold_head (pf_env gl) st (match cl with Some (id, _) -> pf_get_hyp_typ gl id | None -> pf_concl gl) in if did then match cl with - | Some hyp -> change_in_hyp None c' hyp gl - | None -> convert_concl_no_check c' DEFAULTcast gl - else tclFAIL 0 (str "Nothing to unfold") gl + | Some hyp -> change_in_hyp None (fun sigma -> sigma, c') hyp + | None -> convert_concl_no_check c' DEFAULTcast + else Tacticals.New.tclFAIL 0 (str "Nothing to unfold") + end (* Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *) -(* (Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *) +(* (Id.Set.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *) (* in unfold_option unfolds cl *) (* let db = try searchtable_map dbname *) @@ -536,7 +580,7 @@ let autounfold_one db cl gl = (* in *) (* let (ids, csts) = Hint_db.unfolds db in *) (* Cset.fold (fun cst -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cst)) csts *) -(* (Idset.fold (fun id -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cl) ids acc))) *) +(* (Id.Set.fold (fun id -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cl) ids acc))) *) (* (tclFAIL 0 (mt())) db *) TACTIC EXTEND autounfold_one @@ -548,16 +592,26 @@ TACTIC EXTEND autounfold_one TACTIC EXTEND autounfoldify | [ "autounfoldify" constr(x) ] -> [ + Proofview.V82.tactic ( let db = match kind_of_term x with - | Const c -> string_of_label (con_label c) + | Const (c,_) -> Label.to_string (con_label c) | _ -> assert false - in autounfold ["core";db] onConcl ] + in autounfold ["core";db] onConcl + )] END TACTIC EXTEND unify | ["unify" constr(x) constr(y) ] -> [ unify x y ] | ["unify" constr(x) constr(y) "with" preident(base) ] -> [ - unify ~state:(Hint_db.transparent_state (searchtable_map base)) x y ] + let table = try Some (searchtable_map base) with Not_found -> None in + match table with + | None -> + let msg = str "Hint table " ++ str base ++ str " not found" in + Proofview.tclZERO (UserError ("", msg)) + | Some t -> + let state = Hint_db.transparent_state t in + unify ~state x y + ] END @@ -570,7 +624,7 @@ let pr_hints_path_atom prc _ _ a = match a with | PathAny -> str"." | PathHints grs -> - prlist_with_sep pr_spc Printer.pr_global grs + pr_sequence Printer.pr_global grs ARGUMENT EXTEND hints_path_atom TYPED AS hints_path_atom @@ -610,9 +664,9 @@ ARGUMENT EXTEND opthints | [ ] -> [ None ] END -VERNAC COMMAND EXTEND HintCut +VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ let entry = HintsCutEntry p in - Auto.add_hints (Vernacexpr.use_section_locality ()) + Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ())) (match dbnames with None -> ["core"] | Some l -> l) entry ] END |