summaryrefslogtreecommitdiff
path: root/tactics/auto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r--tactics/auto.ml197
1 files changed, 99 insertions, 98 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index bc644857..0c0d9bcf 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1,26 +1,24 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(*
-*)
+module CVars = Vars
+
open Pp
open Util
-open CErrors
open Names
-open Vars
open Termops
+open EConstr
open Environ
-open Tacmach
open Genredexpr
open Tactics
-open Tacticals
open Clenv
-open Tacexpr
open Locus
open Proofview.Notations
open Hints
@@ -36,7 +34,7 @@ open Hints
let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l
let compute_secvars gl =
- let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+ let hyps = Proofview.Goal.hyps gl in
secvars_of_hyps hyps
(* tell auto not to reuse already instantiated metas in unification (for
@@ -44,9 +42,9 @@ let compute_secvars gl =
open Unification
-let auto_core_unif_flags_of st1 st2 useeager = {
+let auto_core_unif_flags_of st1 st2 = {
modulo_conv_on_closed_terms = Some st1;
- use_metas_eagerly_in_conv_on_closed_terms = useeager;
+ use_metas_eagerly_in_conv_on_closed_terms = false;
use_evars_eagerly_in_conv_on_closed_terms = false;
modulo_delta = st2;
modulo_delta_types = full_transparent_state;
@@ -59,8 +57,8 @@ let auto_core_unif_flags_of st1 st2 useeager = {
modulo_eta = true;
}
-let auto_unif_flags_of st1 st2 useeager =
- let flags = auto_core_unif_flags_of st1 st2 useeager in {
+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 = empty_transparent_state };
@@ -69,7 +67,7 @@ let auto_unif_flags_of st1 st2 useeager =
}
let auto_unif_flags =
- auto_unif_flags_of full_transparent_state empty_transparent_state false
+ auto_unif_flags_of full_transparent_state empty_transparent_state
(* Try unification with the precompiled clause, then use registered Apply *)
@@ -84,27 +82,28 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
if poly then
(** Refresh the instance of the hint *)
let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
- let map c = Vars.subst_univs_level_constr subst c in
+ let map c = CVars.subst_univs_level_constr subst c in
+ let emap c = Vars.subst_univs_level_constr subst c in
let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
(** Only metas are mentioning the old universes. *)
let clenv = {
- templval = Evd.map_fl map clenv.templval;
- templtyp = Evd.map_fl map clenv.templtyp;
+ templval = Evd.map_fl emap clenv.templval;
+ templtyp = Evd.map_fl emap clenv.templtyp;
evd = Evd.map_metas map evd;
env = Proofview.Goal.env gl;
} in
- clenv, map c
+ clenv, emap c
else
let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
{ clenv with evd = evd ; env = Proofview.Goal.env gl }, c
in clenv, c
let unify_resolve poly flags ((c : raw_hint), clenv) =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let clenv, c = connect_hint_clenv poly c clenv gl in
- let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in
+ let clenv = clenv_unique_resolver ~flags clenv gl in
Clenvtac.clenv_refine false clenv
- end }
+ end
let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
@@ -113,12 +112,12 @@ let unify_resolve_gen poly = function
| Some flags -> unify_resolve poly flags
let exact poly (c,clenv) =
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.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))
(exact_check c)
- end }
+ end
(* Util *)
@@ -142,15 +141,15 @@ let conclPattern concl pat tac =
try
Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
with Constr_matching.PatternMatchingFailure ->
- Tacticals.New.tclZEROMSG (str "conclPattern")
+ Tacticals.New.tclZEROMSG (str "pattern-matching failed")
in
- Proofview.Goal.enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
constr_bindings env sigma >>= fun constr_bindings ->
let open Genarg in
let open Geninterp in
- let inj c = match val_tag (topwit Constrarg.wit_constr) with
+ let inj c = match val_tag (topwit Stdarg.wit_constr) with
| Val.Base tag -> Val.Dyn (tag, c)
| _ -> assert false
in
@@ -160,7 +159,7 @@ let conclPattern concl pat tac =
match tac with
| GenArg (Glbwit wit, tac) ->
Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
- end }
+ end
(***********************************************************)
(** A debugging / verbosity framework for trivial and auto *)
@@ -177,8 +176,7 @@ let global_info_auto = ref false
let add_option ls refe =
let _ = Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
+ { Goptions.optdepr = false;
Goptions.optname = String.concat " " ls;
Goptions.optkey = ls;
Goptions.optread = (fun () -> !refe);
@@ -191,35 +189,34 @@ let _ =
add_option ["Info";"Trivial"] global_info_trivial;
add_option ["Info";"Auto"] global_info_auto
-let no_dbg () = (Off,0,ref [])
+type debug_kind = ReportForTrivial | ReportForAuto
+
+let no_dbg (_,whatfor,_,_) = (Off,whatfor,0,ref [])
let mk_trivial_dbg debug =
let d =
if debug == Debug || !global_debug_trivial then Debug
else if debug == Info || !global_info_trivial then Info
else Off
- in (d,0,ref [])
-
-(** Note : we start the debug depth of auto at 1 to distinguish it
- for trivial (whose depth is 0). *)
+ in (d,ReportForTrivial,0,ref [])
let mk_auto_dbg debug =
let d =
if debug == Debug || !global_debug_auto then Debug
else if debug == Info || !global_info_auto then Info
else Off
- in (d,1,ref [])
+ in (d,ReportForAuto,0,ref [])
-let incr_dbg = function (dbg,depth,trace) -> (dbg,depth+1,trace)
+let incr_dbg = function (dbg,whatfor,depth,trace) -> (dbg,whatfor,depth+1,trace)
(** A tracing tactic for debug/info trivial/auto *)
-let tclLOG (dbg,depth,trace) pp tac =
+let tclLOG (dbg,_,depth,trace) pp tac =
match dbg with
| Off -> tac
| Debug ->
(* For "debug (trivial/auto)", we directly output messages *)
- let s = String.make depth '*' in
+ let s = String.make (depth+1) '*' in
Proofview.V82.tactic begin fun gl ->
try
let out = Proofview.V82.of_tactic tac gl in
@@ -263,20 +260,20 @@ let pr_info_atom (d,pp) =
str (String.make d ' ') ++ pp () ++ str "."
let pr_info_trace = function
- | (Info,_,{contents=(d,Some pp)::l}) ->
+ | (Info,_,_,{contents=(d,Some pp)::l}) ->
Feedback.msg_info (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l))
| _ -> ()
let pr_info_nop = function
- | (Info,_,_) -> Feedback.msg_info (str "idtac.")
+ | (Info,_,_,_) -> Feedback.msg_info (str "idtac.")
| _ -> ()
let pr_dbg_header = function
- | (Off,_,_) -> ()
- | (Debug,0,_) -> Feedback.msg_debug (str "(* debug trivial: *)")
- | (Debug,_,_) -> Feedback.msg_debug (str "(* debug auto: *)")
- | (Info,0,_) -> Feedback.msg_info (str "(* info trivial: *)")
- | (Info,_,_) -> Feedback.msg_info (str "(* info auto: *)")
+ | (Off,_,_,_) -> ()
+ | (Debug,ReportForTrivial,_,_) -> Feedback.msg_debug (str "(* debug trivial: *)")
+ | (Debug,ReportForAuto,_,_) -> Feedback.msg_debug (str "(* debug auto: *)")
+ | (Info,ReportForTrivial,_,_) -> Feedback.msg_info (str "(* info trivial: *)")
+ | (Info,ReportForAuto,_,_) -> Feedback.msg_info (str "(* info auto: *)")
let tclTRY_dbg d tac =
let delay f = Proofview.tclUNIT () >>= fun () -> f () in
@@ -294,18 +291,18 @@ let tclTRY_dbg d tac =
de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
let flags_of_state st =
- auto_unif_flags_of st st false
+ auto_unif_flags_of st st
let auto_flags_of_state st =
- auto_unif_flags_of full_transparent_state st false
+ auto_unif_flags_of full_transparent_state st
-let hintmap_of secvars hdc concl =
+let hintmap_of sigma secvars hdc concl =
match hdc with
| None -> Hint_db.map_none ~secvars
| Some hdc ->
- if occur_existential concl then
- Hint_db.map_existential ~secvars hdc concl
- else Hint_db.map_auto ~secvars hdc concl
+ if occur_existential sigma concl then
+ Hint_db.map_existential sigma ~secvars hdc concl
+ else Hint_db.map_auto sigma ~secvars hdc concl
let exists_evaluable_reference env = function
| EvalConstRef _ -> true
@@ -317,37 +314,38 @@ let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
let rec trivial_fail_db dbg mod_delta db_list local_db =
let intro_tac =
Tacticals.New.tclTHEN (dbg_intro dbg)
- ( Proofview.Goal.enter { enter = begin fun gl ->
+ ( Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let nf c = Evarutil.nf_evar sigma c in
- let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
+ let decl = Tacmach.New.pf_last_hyp gl in
let hyp = Context.Named.Declaration.map_constr nf decl in
let hintl = make_resolve_hyp env sigma hyp
in trivial_fail_db dbg mod_delta db_list
(Hint_db.add_list env sigma hintl local_db)
- end })
+ end)
in
- Proofview.Goal.enter { enter = begin fun gl ->
- let concl = Tacmach.New.pf_nf_concl gl in
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Tacmach.New.pf_concl gl in
+ let sigma = Tacmach.New.project gl in
let secvars = compute_secvars gl in
Tacticals.New.tclFIRST
((dbg_assumption dbg)::intro_tac::
(List.map Tacticals.New.tclCOMPLETE
- (trivial_resolve dbg mod_delta db_list local_db secvars concl)))
- end }
+ (trivial_resolve sigma dbg mod_delta db_list local_db secvars concl)))
+ end
-and my_find_search_nodelta db_list local_db secvars hdc concl =
+and my_find_search_nodelta sigma db_list local_db secvars hdc concl =
List.map (fun hint -> (None,hint))
- (List.map_append (hintmap_of secvars hdc concl) (local_db::db_list))
+ (List.map_append (hintmap_of sigma secvars hdc concl) (local_db::db_list))
and my_find_search mod_delta =
if mod_delta then my_find_search_delta
else my_find_search_nodelta
-and my_find_search_delta db_list local_db secvars hdc concl =
- let f = hintmap_of secvars hdc concl in
- if occur_existential concl then
+and my_find_search_delta sigma db_list local_db secvars hdc concl =
+ let f = hintmap_of sigma secvars hdc concl in
+ if occur_existential sigma concl then
List.map_append
(fun db ->
if Hint_db.use_dn db then
@@ -369,8 +367,8 @@ and my_find_search_delta db_list local_db secvars hdc concl =
match hdc with None -> Hint_db.map_none ~secvars db
| Some hdc ->
if (Id.Pred.is_empty ids && Cpred.is_empty csts)
- then Hint_db.map_auto ~secvars hdc concl db
- else Hint_db.map_existential ~secvars hdc concl db
+ then Hint_db.map_auto sigma ~secvars hdc concl db
+ else Hint_db.map_existential sigma ~secvars hdc concl db
in auto_flags_of_state st, l
in List.map (fun x -> (Some flags,x)) l)
(local_db::db_list)
@@ -378,20 +376,21 @@ and my_find_search_delta db_list local_db secvars hdc concl =
and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
let tactic = function
| Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
- | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
+ | ERes_pf _ -> Proofview.Goal.enter (fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf"))
| Give_exact (c, cl) -> exact poly (c, cl)
| Res_pf_THEN_trivial_fail (c,cl) ->
Tacticals.New.tclTHEN
(unify_resolve_gen poly flags (c,cl))
(* With "(debug) trivial", we shouldn't end here, and
with "debug auto" we don't display the details of inner trivial *)
- (trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db)
+ (trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db)
| Unfold_nth c ->
- Proofview.V82.tactic (fun gl ->
- if exists_evaluable_reference (pf_env gl) c then
- tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl
- else tclFAIL 0 (str"Unbound reference") gl)
- | Extern tacast ->
+ Proofview.Goal.enter begin fun gl ->
+ if exists_evaluable_reference (Tacmach.New.pf_env gl) c then
+ Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
+ else Tacticals.New.tclFAIL 0 (str"Unbound reference")
+ end
+ | Extern tacast ->
conclPattern concl p tacast
in
let pr_hint () =
@@ -399,27 +398,28 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
| None -> mt ()
| Some n -> str " (in " ++ str n ++ str ")"
in
- pr_hint t ++ origin
+ let sigma, env = Pfedit.get_current_context () in
+ pr_hint env sigma t ++ origin
in
tclLOG dbg pr_hint (run_hint t tactic)
-and trivial_resolve dbg mod_delta db_list local_db secvars cl =
+and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
try
let head =
- try let hdconstr = decompose_app_bound cl in
+ try let hdconstr = decompose_app_bound sigma cl in
Some hdconstr
with Bound -> None
in
List.map (tac_of_hint dbg db_list local_db cl)
(priority
- (my_find_search mod_delta db_list local_db secvars head cl))
+ (my_find_search mod_delta sigma db_list local_db secvars head cl))
with Not_found -> []
(** The use of the "core" database can be de-activated by passing
"nocore" amongst the databases. *)
let trivial ?(debug=Off) lems dbnames =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let db_list = make_db_list dbnames in
@@ -427,10 +427,10 @@ let trivial ?(debug=Off) lems dbnames =
let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
(trivial_fail_db d false db_list hints)
- end }
+ end
let full_trivial ?(debug=Off) lems =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let db_list = current_pure_db () in
@@ -438,7 +438,7 @@ let full_trivial ?(debug=Off) lems =
let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
(trivial_fail_db d false db_list hints)
- end }
+ end
let gen_trivial ?(debug=Off) lems = function
| None -> full_trivial ~debug lems
@@ -450,15 +450,15 @@ let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l
(* The classical Auto tactic *)
(**************************************************************************)
-let possible_resolve dbg mod_delta db_list local_db secvars cl =
+let possible_resolve sigma dbg mod_delta db_list local_db secvars cl =
try
let head =
- try let hdconstr = decompose_app_bound cl in
+ try let hdconstr = decompose_app_bound sigma cl in
Some hdconstr
with Bound -> None
in
List.map (tac_of_hint dbg db_list local_db cl)
- (my_find_search mod_delta db_list local_db secvars head cl)
+ (my_find_search mod_delta sigma db_list local_db secvars head cl)
with Not_found -> []
let extend_local_db decl db gl =
@@ -471,10 +471,10 @@ let extend_local_db decl db gl =
let intro_register dbg kont db =
Tacticals.New.tclTHEN (dbg_intro dbg)
- (Proofview.Goal.enter { enter = begin fun gl ->
+ (Proofview.Goal.enter begin fun gl ->
let extend_local_db decl db = extend_local_db decl db gl in
Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db))
- end })
+ end)
(* n is the max depth of search *)
(* local_db contains the local Hypotheses *)
@@ -487,15 +487,16 @@ let search d n mod_delta db_list local_db =
if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else
Tacticals.New.tclORELSE0 (dbg_assumption d)
(Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
- ( Proofview.Goal.enter { enter = begin fun gl ->
- let concl = Tacmach.New.pf_nf_concl gl in
+ ( Proofview.Goal.enter begin fun gl ->
+ let concl = Tacmach.New.pf_concl gl in
+ let sigma = Tacmach.New.project gl in
let secvars = compute_secvars gl in
let d' = incr_dbg d in
Tacticals.New.tclFIRST
(List.map
(fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
- (possible_resolve d mod_delta db_list local_db secvars concl))
- end }))
+ (possible_resolve sigma d mod_delta db_list local_db secvars concl))
+ end))
end []
in
search d n local_db
@@ -503,7 +504,7 @@ let search d n mod_delta db_list local_db =
let default_search_depth = ref 5
let delta_auto debug mod_delta n lems dbnames =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let db_list = make_db_list dbnames in
@@ -511,12 +512,12 @@ let delta_auto debug mod_delta n lems dbnames =
let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
(search d n mod_delta db_list hints)
- end }
+ end
let delta_auto =
if Flags.profile then
- let key = Profile.declare_profile "delta_auto" in
- Profile.profile5 key delta_auto
+ let key = CProfile.declare_profile "delta_auto" in
+ CProfile.profile5 key delta_auto
else delta_auto
let auto ?(debug=Off) n = delta_auto debug false n
@@ -526,7 +527,7 @@ let new_auto ?(debug=Off) n = delta_auto debug true n
let default_auto = auto !default_search_depth [] []
let delta_full_auto ?(debug=Off) mod_delta n lems =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let db_list = current_pure_db () in
@@ -534,7 +535,7 @@ let delta_full_auto ?(debug=Off) mod_delta n lems =
let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
(search d n mod_delta db_list hints)
- end }
+ end
let full_auto ?(debug=Off) n = delta_full_auto ~debug false n
let new_full_auto ?(debug=Off) n = delta_full_auto ~debug true n
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 07:35:06 +0000