Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Page
Library
Module
Module type
Parameter
Class
Class type
Source
wp_auto.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317
(******************************************************************************) (* This file is part of Waterproof-lib. *) (* *) (* Waterproof-lib is free software: you can redistribute it and/or modify *) (* it under the terms of the GNU General Public License as published by *) (* the Free Software Foundation, either version 3 of the License, or *) (* (at your option) any later version. *) (* *) (* Waterproof-lib is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) (* GNU General Public License for more details. *) (* *) (* You should have received a copy of the GNU General Public License *) (* along with Waterproof-lib. If not, see <https://www.gnu.org/licenses/>. *) (* *) (******************************************************************************) open Auto open Hints open Names open Pp open Proofview open Proofview.Notations open Tactics open Termops open Unification open Util open Backtracking open Proofutils (* All the definitions below come from coq-core hidden library (i.e not visible in the API) *) let auto_core_unif_flags_of st1 st2 = { modulo_conv_on_closed_terms = Some st1; use_metas_eagerly_in_conv_on_closed_terms = true; use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = st2; modulo_delta_types = TransparentState.full; check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = true; } let auto_unif_flags_of st1 st2 = let flags = auto_core_unif_flags_of st1 st2 in { core_unify_flags = flags; merge_unify_flags = flags; subterm_unify_flags = { flags with modulo_delta = TransparentState.empty }; allow_K_in_toplevel_higher_order_unification = false; resolve_evars = true } let auto_unif_flags = auto_unif_flags_of TransparentState.full TransparentState.empty let unify_resolve_nodelta (h: hint): unit tactic = Hints.hint_res_pf ~with_evars:true ~flags:auto_unif_flags h let exact (h: hint): unit tactic = Goal.enter begin fun gl -> let env = Goal.env gl in let sigma = Goal.sigma gl in let sigma, c = Hints.fresh_hint env sigma h in let sigma, t = Typing.type_of env sigma c in let concl = Goal.concl gl in if occur_existential sigma t || occur_existential sigma concl then let sigma = Evd.clear_metas sigma in try let sigma = Unification.w_unify env sigma CONV ~flags:auto_unif_flags concl t in Unsafe.tclEVARSADVANCE sigma <*> exact_no_check c with e when CErrors.noncritical e -> tclZERO e else Unsafe.tclEVARS sigma <*> exact_check c end (** Same function as {! Auto.exists_evaluable_reference} *) let exists_evaluable_reference (env: Environ.env) (evaluable_ref: Evaluable.t): bool = match evaluable_ref with | Evaluable.EvalConstRef _ -> true | Evaluable.EvalProjectionRef _ -> true | Evaluable.EvalVarRef v -> try ignore(Environ.lookup_named v env); true with Not_found -> false (* All the definitions below are inspired by the coq-core hidden library (i.e not visible in the API) but modified for Waterproof *) (** Prints "idtac" if the [log] field is [true] *) let pr_info_nop (): unit = Feedback.msg_notice (str "idtac.") (** Prints a debug header if [log] is [true] *) let pr_dbg_header (): unit = Feedback.msg_notice (str "(* info wp_auto: *)") (** Tries the given tactic and calls an info printer if it fails *) let tclTryDbg (debug_header_printer : unit -> unit) (tac: trace tactic): trace tactic = let new_tac = tac >>= fun trace -> if trace.log then begin debug_header_printer (); if trace.trace <> [] then begin pr_trace trace; Feedback.msg_notice @@ str "\nApplied lemmas:"; pr_trace @@ keep_applied trace end; end; tclUNIT trace in let after = tac >>= fun trace -> if trace.log then pr_info_nop (); tclUNIT trace in tclTraceOrElse (tclPROGRESS new_tac) after (** Creates a function that takes a hint database and returns a hint list *) let hintmap_of (env: Environ.env) (sigma: Evd.evar_map) (secvars: Id.Pred.t) (concl: Evd.econstr): hint_db -> FullHint.t list = let hdc = try Some (decompose_app_bound sigma concl) with Bound -> None in match hdc with | None -> Hint_db.map_none ~secvars | Some hdc -> if occur_existential sigma concl then (fun db -> match Hint_db.map_eauto env sigma ~secvars hdc concl db with | ModeMatch (_, l) -> l | ModeMismatch -> [] ) else Hint_db.map_auto env sigma ~secvars hdc concl (** Returns a logged [intro] tactic *) let dbg_intro: Pp.t list -> trace tactic = tclLOG (fun _ _ -> (str "intro", str "")) (intro <*> tclUNIT no_trace) (** Returns a logged [assumption] tactic *) let dbg_assumption: Pp.t list -> trace tactic = tclLOG (fun _ _ -> (str "assumption", str "")) (assumption <*> tclUNIT no_trace) (** Returns a tactic that apply intro then try to solve the goal *) let intro_register (kont: hint_db -> trace tactic) (db: hint_db) (forbidden_tactics: Pp.t list): trace tactic = let nthDecl m gl = let hyps = Proofview.Goal.hyps gl in try List.nth hyps (m-1) with Failure _ -> CErrors.user_err Pp.(str "No such assumption.") in dbg_intro forbidden_tactics >>= fun new_trace -> TraceTactics.typedGoalEnter begin fun gl -> let extend_local_db decl db = let env = Goal.env gl in let sigma = Goal.sigma gl in push_resolve_hyp env sigma (Context.Named.Declaration.get_id decl) db in TraceTactics.typedGoalEnter @@ fun goal -> tclUNIT (nthDecl 1 goal) >>= (fun decl -> TraceTactics.typedThen (tclUNIT new_trace) (kont (extend_local_db decl db)) ) end let rec trivial_fail_db (trace: trace) (db_list: hint_db list) (forbidden_tactics: Pp.t list) (local_db: hint_db): trace tactic = TraceTactics.typedIndependant @@ tclTraceOrElse (dbg_assumption forbidden_tactics) @@ tclTraceOrElse (intro_register (trivial_fail_db trace db_list forbidden_tactics) local_db forbidden_tactics) @@ TraceTactics.typedGoalEnter begin fun gl -> let env = Goal.env gl in let sigma = Goal.sigma gl in let concl = Goal.concl gl in let secvars = compute_secvars gl in let hintmap = hintmap_of env sigma secvars concl in let hinttac = tac_of_hint trace db_list local_db concl forbidden_tactics in (local_db::db_list) |> List.map_append (fun db -> try hintmap db with Not_found -> []) |> List.filter_map begin fun h -> if Int.equal (FullHint.priority h) 0 then Some (Tacticals.tclCOMPLETE (hinttac h)) else None end |> tclTraceFirst end (** Returns a function that converts hints into tactics *) and tac_of_hint (trace: trace) (db_list: hint_db list) (local_db: hint_db) (concl: Evd.econstr) (forbidden_tactics: Pp.t list): FullHint.t -> trace tactic = let tactic = function | Res_pf h -> unify_resolve_nodelta h <*> tclUNIT @@ no_trace | ERes_pf _ -> TraceTactics.typedGoalEnter (fun gl -> let info = Exninfo.reify () in Tacticals.tclZEROMSG ~info (str "eres_pf")) | Give_exact h -> exact h <*> tclUNIT @@ singleton_trace true (str "exact") (str "") | Res_pf_THEN_trivial_fail h -> tclTHEN (unify_resolve_nodelta h) (trivial_fail_db no_trace db_list forbidden_tactics local_db) | Unfold_nth c -> TraceTactics.typedGoalEnter begin fun gl -> if exists_evaluable_reference (Goal.env gl) c then Tacticals.tclPROGRESS (reduce (Genredexpr.Unfold [Locus.AllOccurrences,c]) Locusops.onConcl) <*> tclUNIT @@ singleton_trace true (str "unfold") (str "") else let info = Exninfo.reify () in Tacticals.tclFAIL ~info (str"Unbound reference") end | Extern (p, tacast) -> conclPattern concl p tacast <*> tclUNIT @@ singleton_trace true (str "") (str "extern") in let pr_hint (h: FullHint.t) (env: Environ.env) (sigma: Evd.evar_map): t * t = let origin = match FullHint.database h with | None -> mt () | Some n -> str n in (Proofutils.pr_hint env sigma h, origin) in fun h -> tclLOG (pr_hint h) (FullHint.run h tactic) forbidden_tactics (** Searches a sequence of at most [n] tactics within [db_list] and [lems] that solves the goal The goal cannot contain evars *) let search (trace: trace) (max_depth: int) (lems: Tactypes.delayed_open_constr list) (db_list: hint_db list) (must_use_tactics: Pp.t list) (forbidden_tactics: Pp.t list): trace tactic = let make_local_db (gl: Goal.t): hint_db = let env = Goal.env gl in let sigma = Goal.sigma gl in try make_local_hint_db env sigma false lems with _ -> make_local_hint_db env sigma false [] in let rec inner_search (trace: trace) (n: int) (previous_envs: (EConstr.named_context * EConstr.constr * Evd.evar_map) list) (local_db: hint_db): trace tactic = if Int.equal n 0 then let info = Exninfo.reify () in tclZERO ~info (SearchBound no_trace) else begin tclTraceOrElse (dbg_assumption forbidden_tactics) @@ tclTraceOrElse (intro_register (inner_search trace n previous_envs) local_db forbidden_tactics) @@ TraceTactics.typedGoalEnter begin fun gl -> let env = Goal.env gl in let sigma = Goal.sigma gl in let concl = Goal.concl gl in let new_trace = incr_trace_depth trace in let secvars = compute_secvars gl in let hintmap = hintmap_of env sigma secvars concl in let hinttac = tac_of_hint trace db_list local_db concl forbidden_tactics in (local_db::db_list) |> List.map_append (fun db -> try hintmap db with Not_found -> []) |> List.map begin fun h -> TraceTactics.typedThen (hinttac h) @@ begin TraceTactics.typedGoalEnter begin fun goal -> let local_db' = make_local_db goal in if List.mem (Goal.hyps goal, Goal.concl goal, Goal.sigma goal) previous_envs then tclZERO (SearchBound no_trace) else inner_search new_trace (n-1) ((Goal.hyps goal, Goal.concl goal, Goal.sigma goal)::previous_envs) local_db' end end >>= fun trace -> if n <> max_depth then tclUNIT trace else trace_check_used must_use_tactics trace end |> tclTraceFirst end end in TraceTactics.typedGoalEnter @@ fun goal -> let local_db = make_local_db goal in tclORELSE begin inner_search trace max_depth [] local_db end begin fun _ -> tclUNIT no_trace end (** Generates the {! wp_auto} function *) let gen_wp_auto (log: bool) ?(n: int = 5) (lems: Tactypes.delayed_open_constr list) (dbnames: hint_db_name list option) (must_use_tactics: Pp.t list) (forbidden_tactics: Pp.t list): trace tactic = wrap_hint_warning @@ TraceTactics.typedGoalEnter begin fun gl -> let db_list = match dbnames with | Some dbnames -> make_db_list dbnames | None -> current_pure_db () in tclTryDbg pr_dbg_header @@ TraceTactics.typedThen (tclUNIT @@ new_trace log) @@ search no_trace n lems db_list must_use_tactics forbidden_tactics end (** Waterproof auto This function is a rewrite around {! Auto.auto} with the same arguments to be able to retrieve which hints have been used in case of success. Returns a typed tactic containing the full trace *) let wp_auto (log: bool) (n: int) (lems: Tactypes.delayed_open_constr list) (dbnames: hint_db_name list): trace tactic = gen_wp_auto log ~n lems (Some dbnames) [] [] (** Restricted Waterproof auto This function acts the same as {! wp_auto} but will fail if all proof found contain at least one must-use lemma that is unused or one hint that is in the [forbidden] list. *) let rwp_auto (log: bool) (n: int) (lems: Tactypes.delayed_open_constr list) (dbnames: hint_db_name list) (must_use_tactics: Pp.t list) (forbidden_tactics: Pp.t list): trace tactic = gen_wp_auto log ~n lems (Some dbnames) must_use_tactics forbidden_tactics