summaryrefslogtreecommitdiff
path: root/tactics/eauto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/eauto.ml')
-rw-r--r--tactics/eauto.ml519
1 files changed, 519 insertions, 0 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
new file mode 100644
index 00000000..23ff5822
--- /dev/null
+++ b/tactics/eauto.ml
@@ -0,0 +1,519 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Proof_type
+open Tacticals
+open Tacmach
+open Tactics
+open Clenv
+open Auto
+open Genredexpr
+open Tacexpr
+open Locus
+open Locusops
+open Hints
+open Proofview.Notations
+
+let eauto_unif_flags = auto_flags_of_state full_transparent_state
+
+let e_give_exact ?(flags=eauto_unif_flags) c =
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let t1 = Tacmach.New.pf_unsafe_type_of gl c in
+ let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
+ if occur_existential t1 || occur_existential t2 then
+ Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (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 }
+
+(************************************************************************)
+(* 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
+
+(***************************************************************************)
+(* 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 secvars hdc concl =
+ match hdc with
+ | None -> fun db -> Hint_db.map_none ~secvars db
+ | Some hdc ->
+ if occur_existential concl then
+ (fun db -> Hint_db.map_existential ~secvars hdc concl db)
+ else (fun db -> Hint_db.map_auto ~secvars hdc concl db)
+ (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
+
+let e_exact poly flags (c,clenv) =
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let clenv', c = connect_hint_clenv poly c clenv gl in
+ Tacticals.New.tclTHEN
+ (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+ (e_give_exact c)
+ end }
+
+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 secvars = compute_secvars gl in
+ let tacl =
+ registered_e_assumption ::
+ (Tacticals.New.tclTHEN Tactics.intro next) ::
+ (List.map fst (e_trivial_resolve db_list local_db secvars (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 secvars hdc concl =
+ let hint_of_db = hintmap_of secvars 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 secvars gl =
+ let hd = try Some (decompose_app_bound gl) with Bound -> None in
+ try priority (e_my_find_search db_list local_db secvars hd gl)
+ with Not_found -> []
+
+let e_possible_resolve db_list local_db secvars 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 secvars 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 CErrors.noncritical e ->
+ let e = CErrors.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 hyps = pf_ids_of_hyps g in
+ let secvars = secvars_of_hyps (pf_hyps g) 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 hyps 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 =
+ let concl = Reductionops.nf_evar (project g)(pf_concl g) in
+ filter_tactics s.tacres
+ (e_possible_resolve s.dblist (List.hd s.localdb) secvars concl)
+ 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 -> Feedback.msg_info (str "idtac.")
+ | _ -> ()
+
+let pr_dbg_header = function
+ | Off -> ()
+ | Debug -> Feedback.msg_debug (str "(* debug eauto: *)")
+ | Info -> Feedback.msg_info (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
+ Feedback.msg_info (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 db_list = current_pure_db () 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 }
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 01:22:47 +0000