summaryrefslogtreecommitdiff
path: root/tactics/auto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r--tactics/auto.ml1412
1 files changed, 225 insertions, 1187 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 3451957e..45052685 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1,1011 +1,29 @@
(************************************************************************)
(* 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 *)
(************************************************************************)
+(*
+*)
open Pp
open Util
+open Errors
open Names
-open Nameops
-open Namegen
-open Term
+open Vars
open Termops
-open Inductiveops
-open Sign
open Environ
-open Inductive
-open Evd
-open Reduction
-open Typing
-open Pattern
-open Matching
open Tacmach
-open Proof_type
-open Pfedit
-open Glob_term
-open Evar_refiner
-open Tacred
+open Genredexpr
open Tactics
open Tacticals
open Clenv
-open Hiddentac
-open Libnames
-open Nametab
-open Smartlocate
-open Libobject
-open Library
-open Printer
-open Declarations
open Tacexpr
-open Mod_subst
-
-(****************************************************************************)
-(* The Type of Constructions Autotactic Hints *)
-(****************************************************************************)
-
-type 'a auto_tactic =
- | Res_pf of constr * 'a (* Hint Apply *)
- | ERes_pf of constr * 'a (* Hint EApply *)
- | Give_exact of constr
- | Res_pf_THEN_trivial_fail of constr * 'a (* Hint Immediate *)
- | Unfold_nth of evaluable_global_reference (* Hint Unfold *)
- | Extern of glob_tactic_expr (* Hint Extern *)
-
-type hints_path_atom =
- | PathHints of global_reference list
- | PathAny
-
-type hints_path =
- | PathAtom of hints_path_atom
- | PathStar of hints_path
- | PathSeq of hints_path * hints_path
- | PathOr of hints_path * hints_path
- | PathEmpty
- | PathEpsilon
-
-type 'a gen_auto_tactic = {
- pri : int; (* A number lower is higher priority *)
- pat : constr_pattern option; (* A pattern for the concl of the Goal *)
- name : hints_path_atom; (* A potential name to refer to the hint *)
- code : 'a auto_tactic (* the tactic to apply when the concl matches pat *)
-}
-
-type pri_auto_tactic = clausenv gen_auto_tactic
-
-type hint_entry = global_reference option * types gen_auto_tactic
-
-let pri_order_int (id1, {pri=pri1}) (id2, {pri=pri2}) =
- let d = pri1 - pri2 in
- if d == 0 then id2 - id1
- else d
-
-let pri_order t1 t2 = pri_order_int t1 t2 <= 0
-
-let insert v l =
- let rec insrec = function
- | [] -> [v]
- | h::tl -> if pri_order v h then v::h::tl else h::(insrec tl)
- in
- insrec l
-
-(* Nov 98 -- Papageno *)
-(* Les Hints sont ré-organisés en plusieurs databases.
-
- La table impérative "searchtable", de type "hint_db_table",
- associe une database (hint_db) à chaque nom.
-
- Une hint_db est une table d'association fonctionelle constr -> search_entry
- Le constr correspond à la constante de tête de la conclusion.
-
- Une search_entry est un triplet comprenant :
- - la liste des tactiques qui n'ont pas de pattern associé
- - la liste des tactiques qui ont un pattern
- - un discrimination net borné (Btermdn.t) constitué de tous les
- patterns de la seconde liste de tactiques *)
-
-type stored_data = int * pri_auto_tactic
- (* First component is the index of insertion in the table, to keep most recent first semantics. *)
-
-let auto_tactic_ord code1 code2 =
- match code1, code2 with
- | Res_pf (c1, _), Res_pf (c2, _)
- | ERes_pf (c1, _), ERes_pf (c2, _)
- | Give_exact c1, Give_exact c2
- | Res_pf_THEN_trivial_fail (c1, _), Res_pf_THEN_trivial_fail (c2, _) -> constr_ord c1 c2
- | Unfold_nth (EvalVarRef i1), Unfold_nth (EvalVarRef i2) -> Pervasives.compare i1 i2
- | Unfold_nth (EvalConstRef c1), Unfold_nth (EvalConstRef c2) ->
- kn_ord (canonical_con c1) (canonical_con c2)
- | Extern t1, Extern t2 -> Pervasives.compare t1 t2
- | _ -> Pervasives.compare code1 code2
-
-module Bounded_net = Btermdn.Make(struct
- type t = stored_data
- let compare = pri_order_int
- end)
-
-type search_entry = stored_data list * stored_data list * Bounded_net.t
-
-let empty_se = ([],[],Bounded_net.create ())
-
-let eq_pri_auto_tactic (_, x) (_, y) =
- if x.pri = y.pri && x.pat = y.pat then
- match x.code,y.code with
- | Res_pf(cstr,_),Res_pf(cstr1,_) ->
- eq_constr cstr cstr1
- | ERes_pf(cstr,_),ERes_pf(cstr1,_) ->
- eq_constr cstr cstr1
- | Give_exact cstr,Give_exact cstr1 ->
- eq_constr cstr cstr1
- | Res_pf_THEN_trivial_fail(cstr,_)
- ,Res_pf_THEN_trivial_fail(cstr1,_) ->
- eq_constr cstr cstr1
- | _,_ -> false
- else
- false
-
-let add_tac pat t st (l,l',dn) =
- match pat with
- | None -> if not (List.exists (eq_pri_auto_tactic t) l) then (insert t l, l', dn) else (l, l', dn)
- | Some pat ->
- if not (List.exists (eq_pri_auto_tactic t) l')
- then (l, insert t l', Bounded_net.add st dn (pat,t)) else (l, l', dn)
-
-let rebuild_dn st ((l,l',dn) : search_entry) =
- (l, l', List.fold_left (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
- (Bounded_net.create ()) l')
-
-
-let lookup_tacs (hdc,c) st (l,l',dn) =
- let l' = List.map snd (Bounded_net.lookup st dn c) in
- let sl' = List.stable_sort pri_order_int l' in
- Sort.merge pri_order l sl'
-
-module Constr_map = Map.Make(RefOrdered)
-
-let is_transparent_gr (ids, csts) = function
- | VarRef id -> Idpred.mem id ids
- | ConstRef cst -> Cpred.mem cst csts
- | IndRef _ | ConstructRef _ -> false
-
-let dummy_goal = Goal.V82.dummy_goal
-
-let translate_hint (go,p) =
- let mk_clenv (c,t) =
- let cl = mk_clenv_from dummy_goal (c,t) in {cl with env = empty_env }
- in
- let code = match p.code with
- | Res_pf (c,t) -> Res_pf (c, mk_clenv (c,t))
- | ERes_pf (c,t) -> ERes_pf (c, mk_clenv (c,t))
- | Res_pf_THEN_trivial_fail (c,t) ->
- Res_pf_THEN_trivial_fail (c, mk_clenv (c,t))
- | Give_exact c -> Give_exact c
- | Unfold_nth e -> Unfold_nth e
- | Extern t -> Extern t
- in
- (go,{ p with code = code })
-
-let path_matches hp hints =
- let rec aux hp hints k =
- match hp, hints with
- | PathAtom _, [] -> false
- | PathAtom PathAny, (_ :: hints') -> k hints'
- | PathAtom p, (h :: hints') ->
- if p = h then k hints' else false
- | PathStar hp', hints ->
- k hints || aux hp' hints (fun hints' -> aux hp hints' k)
- | PathSeq (hp, hp'), hints ->
- aux hp hints (fun hints' -> aux hp' hints' k)
- | PathOr (hp, hp'), hints ->
- aux hp hints k || aux hp' hints k
- | PathEmpty, _ -> false
- | PathEpsilon, hints -> k hints
- in aux hp hints (fun hints' -> true)
-
-let rec matches_epsilon = function
- | PathAtom _ -> false
- | PathStar _ -> true
- | PathSeq (p, p') -> matches_epsilon p && matches_epsilon p'
- | PathOr (p, p') -> matches_epsilon p || matches_epsilon p'
- | PathEmpty -> false
- | PathEpsilon -> true
-
-let rec is_empty = function
- | PathAtom _ -> false
- | PathStar _ -> false
- | PathSeq (p, p') -> is_empty p || is_empty p'
- | PathOr (p, p') -> matches_epsilon p && matches_epsilon p'
- | PathEmpty -> true
- | PathEpsilon -> false
-
-let rec path_derivate hp hint =
- let rec derivate_atoms hints hints' =
- match hints, hints' with
- | gr :: grs, gr' :: grs' when gr = gr' -> derivate_atoms grs grs'
- | [], [] -> PathEpsilon
- | [], hints -> PathEmpty
- | grs, [] -> PathAtom (PathHints grs)
- | _, _ -> PathEmpty
- in
- match hp with
- | PathAtom PathAny -> PathEpsilon
- | PathAtom (PathHints grs) ->
- (match grs, hint with
- | h :: hints, PathAny -> PathEmpty
- | hints, PathHints hints' -> derivate_atoms hints hints'
- | _, _ -> assert false)
- | PathStar p -> if path_matches p [hint] then hp else PathEpsilon
- | PathSeq (hp, hp') ->
- let hpder = path_derivate hp hint in
- if matches_epsilon hp then
- PathOr (PathSeq (hpder, hp'), path_derivate hp' hint)
- else if is_empty hpder then PathEmpty
- else PathSeq (hpder, hp')
- | PathOr (hp, hp') ->
- PathOr (path_derivate hp hint, path_derivate hp' hint)
- | PathEmpty -> PathEmpty
- | PathEpsilon -> PathEmpty
-
-let rec normalize_path h =
- match h with
- | PathStar PathEpsilon -> PathEpsilon
- | PathSeq (PathEmpty, _) | PathSeq (_, PathEmpty) -> PathEmpty
- | PathSeq (PathEpsilon, p) | PathSeq (p, PathEpsilon) -> normalize_path p
- | PathOr (PathEmpty, p) | PathOr (p, PathEmpty) -> normalize_path p
- | PathOr (p, q) ->
- let p', q' = normalize_path p, normalize_path q in
- if p = p' && q = q' then h
- else normalize_path (PathOr (p', q'))
- | PathSeq (p, q) ->
- let p', q' = normalize_path p, normalize_path q in
- if p = p' && q = q' then h
- else normalize_path (PathSeq (p', q'))
- | _ -> h
-
-let path_derivate hp hint = normalize_path (path_derivate hp hint)
-
-let rec pp_hints_path = function
- | PathAtom (PathAny) -> str"."
- | PathAtom (PathHints grs) -> prlist_with_sep pr_spc pr_global grs
- | PathStar p -> str "(" ++ pp_hints_path p ++ str")*"
- | PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p'
- | PathOr (p, p') ->
- str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ spc () ++ pp_hints_path p' ++ str ")"
- | PathEmpty -> str"Ø"
- | PathEpsilon -> str"ε"
-
-let subst_path_atom subst p =
- match p with
- | PathAny -> p
- | PathHints grs ->
- let gr' gr = fst (subst_global subst gr) in
- let grs' = list_smartmap gr' grs in
- if grs' == grs then p else PathHints grs'
-
-let rec subst_hints_path subst hp =
- match hp with
- | PathAtom p ->
- let p' = subst_path_atom subst p in
- if p' == p then hp else PathAtom p'
- | PathStar p -> let p' = subst_hints_path subst p in
- if p' == p then hp else PathStar p'
- | PathSeq (p, q) ->
- let p' = subst_hints_path subst p in
- let q' = subst_hints_path subst q in
- if p' == p && q' == q then hp else PathSeq (p', q')
- | PathOr (p, q) ->
- let p' = subst_hints_path subst p in
- let q' = subst_hints_path subst q in
- if p' == p && q' == q then hp else PathOr (p', q')
- | _ -> hp
-
-module Hint_db = struct
-
- type t = {
- hintdb_state : Names.transparent_state;
- hintdb_cut : hints_path;
- hintdb_unfolds : Idset.t * Cset.t;
- mutable hintdb_max_id : int;
- use_dn : bool;
- hintdb_map : search_entry Constr_map.t;
- (* A list of unindexed entries starting with an unfoldable constant
- or with no associated pattern. *)
- hintdb_nopat : (global_reference option * stored_data) list
- }
-
- let next_hint_id t =
- let h = t.hintdb_max_id in t.hintdb_max_id <- succ t.hintdb_max_id; h
-
- let empty st use_dn = { hintdb_state = st;
- hintdb_cut = PathEmpty;
- hintdb_unfolds = (Idset.empty, Cset.empty);
- hintdb_max_id = 0;
- use_dn = use_dn;
- hintdb_map = Constr_map.empty;
- hintdb_nopat = [] }
-
- let find key db =
- try Constr_map.find key db.hintdb_map
- with Not_found -> empty_se
-
- let map_none db =
- List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat) [])
-
- let map_all k db =
- let (l,l',_) = find k db in
- List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l')
-
- let map_auto (k,c) db =
- let st = if db.use_dn then Some db.hintdb_state else None in
- let l' = lookup_tacs (k,c) st (find k db) in
- List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat) l')
-
- let is_exact = function
- | Give_exact _ -> true
- | _ -> false
-
- let is_unfold = function
- | Unfold_nth _ -> true
- | _ -> false
-
- let addkv gr id v db =
- let idv = id, v in
- let k = match gr with
- | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr &&
- is_unfold v.code then None else Some gr
- | None -> None
- in
- let dnst = if db.use_dn then Some db.hintdb_state else None in
- let pat = if not db.use_dn && is_exact v.code then None else v.pat in
- match k with
- | None ->
- if not (List.exists (fun (_, (_, v')) -> v = v') db.hintdb_nopat) then
- { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
- else db
- | Some gr ->
- let oval = find gr db in
- { db with hintdb_map = Constr_map.add gr (add_tac pat idv dnst oval) db.hintdb_map }
-
- let rebuild_db st' db =
- let db' =
- { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map;
- hintdb_state = st'; hintdb_nopat = [] }
- in
- List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat
-
- let add_one kv db =
- let (k,v) = translate_hint kv in
- let st',db,rebuild =
- match v.code with
- | Unfold_nth egr ->
- let addunf (ids,csts) (ids',csts') =
- match egr with
- | EvalVarRef id -> (Idpred.add id ids, csts), (Idset.add id ids', csts')
- | EvalConstRef cst -> (ids, Cpred.add cst csts), (ids', Cset.add cst csts')
- in
- let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in
- state, { db with hintdb_unfolds = unfs }, true
- | _ -> db.hintdb_state, db, false
- in
- let db = if db.use_dn && rebuild then rebuild_db st' db else db
- in addkv k (next_hint_id db) v db
-
- let add_list l db = List.fold_left (fun db k -> add_one k db) db l
-
- let remove_sdl p sdl = list_smartfilter p sdl
- let remove_he st p (sl1, sl2, dn as he) =
- let sl1' = remove_sdl p sl1 and sl2' = remove_sdl p sl2 in
- if sl1' == sl1 && sl2' == sl2 then he
- else rebuild_dn st (sl1', sl2', dn)
-
- let remove_list grs db =
- let filter (_, h) = match h.name with PathHints [gr] -> not (List.mem gr grs) | _ -> true in
- let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
- let hintnopat = list_smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
- { db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
-
- let remove_one gr db = remove_list [gr] db
-
- let iter f db =
- f None (List.map (fun x -> snd (snd x)) db.hintdb_nopat);
- Constr_map.iter (fun k (l,l',_) -> f (Some k) (List.map snd (l@l'))) db.hintdb_map
-
- let transparent_state db = db.hintdb_state
-
- let set_transparent_state db st =
- if db.use_dn then rebuild_db st db
- else { db with hintdb_state = st }
-
- let add_cut path db =
- { db with hintdb_cut = normalize_path (PathOr (db.hintdb_cut, path)) }
-
- let cut db = db.hintdb_cut
-
- let unfolds db = db.hintdb_unfolds
-
- let use_dn db = db.use_dn
-
-end
-
-module Hintdbmap = Gmap
-
-type hint_db = Hint_db.t
-
-type frozen_hint_db_table = (string,hint_db) Hintdbmap.t
-
-type hint_db_table = (string,hint_db) Hintdbmap.t ref
-
-type hint_db_name = string
-
-let searchtable = (ref Hintdbmap.empty : hint_db_table)
-
-let searchtable_map name =
- Hintdbmap.find name !searchtable
-let searchtable_add (name,db) =
- searchtable := Hintdbmap.add name db !searchtable
-let current_db_names () =
- Hintdbmap.dom !searchtable
-
-(**************************************************************************)
-(* Definition of the summary *)
-(**************************************************************************)
-
-let auto_init : (unit -> unit) ref = ref (fun () -> ())
-let add_auto_init f =
- let init = !auto_init in
- auto_init := (fun () -> init (); f ())
-
-let init () = searchtable := Hintdbmap.empty; !auto_init ()
-let freeze () = !searchtable
-let unfreeze fs = searchtable := fs
-
-let _ = Summary.declare_summary "search"
- { Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = init }
-
-
-(**************************************************************************)
-(* Auxiliary functions to prepare AUTOHINT objects *)
-(**************************************************************************)
-
-let rec nb_hyp c = match kind_of_term c with
- | Prod(_,_,c2) -> if noccurn 1 c2 then 1+(nb_hyp c2) else nb_hyp c2
- | _ -> 0
-
-(* adding and removing tactics in the search table *)
-
-let try_head_pattern c =
- try head_pattern_bound c
- with BoundPattern -> error "Bound head variable."
-
-let name_of_constr c = try Some (global_of_constr c) with Not_found -> None
-
-let make_exact_entry sigma pri ?(name=PathAny) (c,cty) =
- let cty = strip_outer_cast cty in
- match kind_of_term cty with
- | Prod _ -> failwith "make_exact_entry"
- | _ ->
- let pat = snd (Pattern.pattern_of_constr sigma cty) in
- let hd =
- try head_pattern_bound pat
- with BoundPattern -> failwith "make_exact_entry"
- in
- (Some hd,
- { pri = (match pri with None -> 0 | Some p -> p);
- pat = Some pat;
- name = name;
- code = Give_exact c })
-
-let make_apply_entry env sigma (eapply,hnf,verbose) pri ?(name=PathAny) (c,cty) =
- let cty = if hnf then hnf_constr env sigma cty else cty in
- match kind_of_term cty with
- | Prod _ ->
- let ce = mk_clenv_from dummy_goal (c,cty) in
- let c' = clenv_type (* ~reduce:false *) ce in
- let pat = snd (Pattern.pattern_of_constr sigma c') in
- let hd =
- try head_pattern_bound pat
- with BoundPattern -> failwith "make_apply_entry" in
- let nmiss = List.length (clenv_missing ce) in
- if nmiss = 0 then
- (Some hd,
- { pri = (match pri with None -> nb_hyp cty | Some p -> p);
- pat = Some pat;
- name = name;
- code = Res_pf(c,cty) })
- else begin
- if not eapply then failwith "make_apply_entry";
- if verbose then
- warn (str "the hint: eapply " ++ pr_lconstr c ++
- str " will only be used by eauto");
- (Some hd,
- { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p);
- pat = Some pat;
- name = name;
- code = ERes_pf(c,cty) })
- end
- | _ -> failwith "make_apply_entry"
-
-(* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose
- c is a constr
- cty is the type of constr *)
-
-let make_resolves env sigma flags pri ?name c =
- let cty = Retyping.get_type_of env sigma c in
- let ents =
- map_succeed
- (fun f -> f (c,cty))
- [make_exact_entry sigma pri ?name; make_apply_entry env sigma flags pri ?name]
- in
- if ents = [] then
- errorlabstrm "Hint"
- (pr_lconstr c ++ spc() ++
- (if pi1 flags then str"cannot be used as a hint."
- else str "can be used as a hint only for eauto."));
- ents
-
-(* used to add an hypothesis to the local hint database *)
-let make_resolve_hyp env sigma (hname,_,htyp) =
- try
- [make_apply_entry env sigma (true, true, false) None
- ~name:(PathHints [VarRef hname])
- (mkVar hname, htyp)]
- with
- | Failure _ -> []
- | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp"
-
-(* REM : in most cases hintname = id *)
-let make_unfold eref =
- let g = global_of_evaluable_reference eref in
- (Some g,
- { pri = 4;
- pat = None;
- name = PathHints [g];
- code = Unfold_nth eref })
-
-let make_extern pri pat tacast =
- let hdconstr = Option.map try_head_pattern pat in
- (hdconstr,
- { pri = pri;
- pat = pat;
- name = PathAny;
- code = Extern tacast })
-
-let make_trivial env sigma ?(name=PathAny) c =
- let t = hnf_constr env sigma (type_of env sigma c) in
- let hd = head_of_constr_reference (fst (head_constr t)) in
- let ce = mk_clenv_from dummy_goal (c,t) in
- (Some hd, { pri=1;
- pat = Some (snd (Pattern.pattern_of_constr sigma (clenv_type ce)));
- name = name;
- code=Res_pf_THEN_trivial_fail(c,t) })
-
-open Vernacexpr
-
-(**************************************************************************)
-(* declaration of the AUTOHINT library object *)
-(**************************************************************************)
-
-(* If the database does not exist, it is created *)
-(* TODO: should a warning be printed in this case ?? *)
-
-let get_db dbname =
- try searchtable_map dbname
- with Not_found -> Hint_db.empty empty_transparent_state false
-
-let add_hint dbname hintlist =
- let db = get_db dbname in
- let db' = Hint_db.add_list hintlist db in
- searchtable_add (dbname,db')
-
-let add_transparency dbname grs b =
- let db = get_db dbname in
- let st = Hint_db.transparent_state db in
- let st' =
- List.fold_left (fun (ids, csts) gr ->
- match gr with
- | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts)
- | EvalVarRef v -> (if b then Idpred.add else Idpred.remove) v ids, csts)
- st grs
- in searchtable_add (dbname, Hint_db.set_transparent_state db st')
-
-let remove_hint dbname grs =
- let db = get_db dbname in
- let db' = Hint_db.remove_list grs db in
- searchtable_add (dbname, db')
-
-type hint_action =
- | CreateDB of bool * transparent_state
- | AddTransparency of evaluable_global_reference list * bool
- | AddHints of hint_entry list
- | RemoveHints of global_reference list
- | AddCut of hints_path
-
-let add_cut dbname path =
- let db = get_db dbname in
- let db' = Hint_db.add_cut path db in
- searchtable_add (dbname, db')
-
-type hint_obj = bool * string * hint_action (* locality, name, action *)
-
-let cache_autohint (_,(local,name,hints)) =
- match hints with
- | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
- | AddTransparency (grs, b) -> add_transparency name grs b
- | AddHints hints -> add_hint name hints
- | RemoveHints grs -> remove_hint name grs
- | AddCut path -> add_cut name path
-
-let forward_subst_tactic =
- ref (fun _ -> failwith "subst_tactic is not installed for auto")
-
-let set_extern_subst_tactic f = forward_subst_tactic := f
-
-let subst_autohint (subst,(local,name,hintlist as obj)) =
- let subst_key gr =
- let (lab'', elab') = subst_global subst gr in
- let gr' =
- (try head_of_constr_reference (fst (head_constr_bound elab'))
- with Tactics.Bound -> lab'')
- in if gr' == gr then gr else gr'
- in
- let subst_hint (k,data as hint) =
- let k' = Option.smartmap subst_key k in
- let pat' = Option.smartmap (subst_pattern subst) data.pat in
- let code' = match data.code with
- | Res_pf (c,t) ->
- let c' = subst_mps subst c in
- let t' = subst_mps subst t in
- if c==c' && t'==t then data.code else Res_pf (c', t')
- | ERes_pf (c,t) ->
- let c' = subst_mps subst c in
- let t' = subst_mps subst t in
- if c==c' && t'==t then data.code else ERes_pf (c',t')
- | Give_exact c ->
- let c' = subst_mps subst c in
- if c==c' then data.code else Give_exact c'
- | Res_pf_THEN_trivial_fail (c,t) ->
- let c' = subst_mps subst c in
- let t' = subst_mps subst t in
- if c==c' && t==t' then data.code else Res_pf_THEN_trivial_fail (c',t')
- | Unfold_nth ref ->
- let ref' = subst_evaluable_reference subst ref in
- if ref==ref' then data.code else Unfold_nth ref'
- | Extern tac ->
- let tac' = !forward_subst_tactic subst tac in
- if tac==tac' then data.code else Extern tac'
- in
- let name' = subst_path_atom subst data.name in
- let data' =
- if data.pat==pat' && data.name == name' && data.code==code' then data
- else { data with pat = pat'; name = name'; code = code' }
- in
- if k' == k && data' == data then hint else (k',data')
- in
- match hintlist with
- | CreateDB _ -> obj
- | AddTransparency (grs, b) ->
- let grs' = list_smartmap (subst_evaluable_reference subst) grs in
- if grs==grs' then obj else (local, name, AddTransparency (grs', b))
- | AddHints hintlist ->
- let hintlist' = list_smartmap subst_hint hintlist in
- if hintlist' == hintlist then obj else
- (local,name,AddHints hintlist')
- | RemoveHints grs ->
- let grs' = list_smartmap (fun x -> fst (subst_global subst x)) grs in
- if grs==grs' then obj else (local, name, RemoveHints grs')
- | AddCut path ->
- let path' = subst_hints_path subst path in
- if path' == path then obj else (local, name, AddCut path')
-
-let classify_autohint ((local,name,hintlist) as obj) =
- if local or hintlist = (AddHints []) then Dispose else Substitute obj
-
-let inAutoHint : hint_obj -> obj =
- declare_object {(default_object "AUTOHINT") with
- cache_function = cache_autohint;
- load_function = (fun _ -> cache_autohint);
- subst_function = subst_autohint;
- classify_function = classify_autohint; }
-
-let create_hint_db l n st b =
- Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st)))
-
-let remove_hints local dbnames grs =
- let dbnames = if dbnames = [] then ["core"] else dbnames in
- List.iter
- (fun dbname ->
- Lib.add_anonymous_leaf (inAutoHint(local, dbname, RemoveHints grs)))
- dbnames
-
-(**************************************************************************)
-(* The "Hint" vernacular command *)
-(**************************************************************************)
-let add_resolves env sigma clist local dbnames =
- List.iter
- (fun dbname ->
- Lib.add_anonymous_leaf
- (inAutoHint
- (local,dbname, AddHints
- (List.flatten (List.map (fun (x, hnf, path, y) ->
- make_resolves env sigma (true,hnf,Flags.is_verbose()) x ~name:path y) clist)))))
- dbnames
-
-let add_unfolds l local dbnames =
- List.iter
- (fun dbname -> Lib.add_anonymous_leaf
- (inAutoHint (local,dbname, AddHints (List.map make_unfold l))))
- dbnames
-
-let add_cuts l local dbnames =
- List.iter
- (fun dbname -> Lib.add_anonymous_leaf
- (inAutoHint (local,dbname, AddCut l)))
- dbnames
-
-let add_transparency l b local dbnames =
- List.iter
- (fun dbname -> Lib.add_anonymous_leaf
- (inAutoHint (local,dbname, AddTransparency (l, b))))
- dbnames
-
-let add_extern pri pat tacast local dbname =
- (* We check that all metas that appear in tacast have at least
- one occurence in the left pattern pat *)
- let tacmetas = [] in
- match pat with
- | Some (patmetas,pat) ->
- (match (list_subtract tacmetas patmetas) with
- | i::_ ->
- errorlabstrm "add_extern"
- (str "The meta-variable ?" ++ Ppconstr.pr_patvar i ++ str" is not bound.")
- | [] ->
- Lib.add_anonymous_leaf
- (inAutoHint(local,dbname, AddHints [make_extern pri (Some pat) tacast])))
- | None ->
- Lib.add_anonymous_leaf
- (inAutoHint(local,dbname, AddHints [make_extern pri None tacast]))
-
-let add_externs pri pat tacast local dbnames =
- List.iter (add_extern pri pat tacast local) dbnames
-
-let add_trivials env sigma l local dbnames =
- List.iter
- (fun dbname ->
- Lib.add_anonymous_leaf (
- inAutoHint(local,dbname,
- AddHints (List.map (fun (name, c) -> make_trivial env sigma ~name c) l))))
- dbnames
-
-let forward_intern_tac =
- ref (fun _ -> failwith "intern_tac is not installed for auto")
-
-let set_extern_intern_tac f = forward_intern_tac := f
-
-type hints_entry =
- | HintsResolveEntry of (int option * bool * hints_path_atom * constr) list
- | HintsImmediateEntry of (hints_path_atom * constr) list
- | HintsCutEntry of hints_path
- | HintsUnfoldEntry of evaluable_global_reference list
- | HintsTransparencyEntry of evaluable_global_reference list * bool
- | HintsExternEntry of
- int * (patvar list * constr_pattern) option * glob_tactic_expr
-
-let h = id_of_string "H"
-
-exception Found of constr * types
-
-let prepare_hint env (sigma,c) =
- let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
- (* We re-abstract over uninstantiated evars.
- It is actually a bit stupid to generalize over evars since the first
- thing make_resolves will do is to re-instantiate the products *)
- let c = drop_extra_implicit_args (Evarutil.nf_evar sigma c) in
- let vars = ref (collect_vars c) in
- let subst = ref [] in
- let rec find_next_evar c = match kind_of_term c with
- | Evar (evk,args as ev) ->
- (* We skip the test whether args is the identity or not *)
- let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
- let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in
- if free_rels t <> Intset.empty then
- error "Hints with holes dependent on a bound variable not supported.";
- if occur_existential t then
- (* Not clever enough to construct dependency graph of evars *)
- error "Not clever enough to deal with evars dependent in other evars.";
- raise (Found (c,t))
- | _ -> iter_constr find_next_evar c in
- let rec iter c =
- try find_next_evar c; c
- with Found (evar,t) ->
- let id = next_ident_away_from h (fun id -> Idset.mem id !vars) in
- vars := Idset.add id !vars;
- subst := (evar,mkVar id)::!subst;
- mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
- iter c
-
-let path_of_constr_expr c =
- match c with
- | Topconstr.CRef r ->
- (try PathHints [global r] with e when Errors.noncritical e -> PathAny)
- | _ -> PathAny
-
-let interp_hints h =
- let f c =
- let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in
- let c = prepare_hint (Global.env()) (evd,c) in
- Evarutil.check_evars (Global.env()) Evd.empty evd c;
- c in
- let fr r =
- let gr = global_with_alias r in
- let r' = evaluable_of_global_reference (Global.env()) gr in
- Dumpglob.add_glob (loc_of_reference r) gr;
- r' in
- let fres (o, b, c) = (o, b, path_of_constr_expr c, f c) in
- let fi c = path_of_constr_expr c, f c in
- let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in
- match h with
- | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
- | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
- | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
- | HintsTransparency (lhints, b) ->
- HintsTransparencyEntry (List.map fr lhints, b)
- | HintsConstructors lqid ->
- let constr_hints_of_ind qid =
- let ind = global_inductive_with_alias qid in
- Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
- list_tabulate (fun i -> let c = (ind,i+1) in
- None, true, PathHints [ConstructRef c], mkConstruct c)
- (nconstructors ind) in
- HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
- | HintsExtern (pri, patcom, tacexp) ->
- let pat = Option.map fp patcom in
- let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in
- HintsExternEntry (pri, pat, tacexp)
-
-let add_hints local dbnames0 h =
- if List.mem "nocore" dbnames0 then
- error "The hint database \"nocore\" is meant to stay empty.";
- let dbnames = if dbnames0 = [] then ["core"] else dbnames0 in
- let env = Global.env() and sigma = Evd.empty in
- match h with
- | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames
- | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames
- | HintsCutEntry lhints -> add_cuts lhints local dbnames
- | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
- | HintsTransparencyEntry (lhints, b) ->
- add_transparency lhints b local dbnames
- | HintsExternEntry (pri, pat, tacexp) ->
- add_externs pri pat tacexp local dbnames
-
-(**************************************************************************)
-(* Functions for printing the hints *)
-(**************************************************************************)
-
-let pr_autotactic =
- function
- | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c)
- | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c)
- | Give_exact c -> (str"exact " ++ pr_constr c)
- | Res_pf_THEN_trivial_fail (c,clenv) ->
- (str"apply " ++ pr_constr c ++ str" ; trivial")
- | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c)
- | Extern tac ->
- let env =
- try
- let (_, env) = Pfedit.get_current_goal_context () in
- env
- with e when Errors.noncritical e -> Global.env ()
- in
- (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac)
-
-let pr_hint (id, v) =
- (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
-
-let pr_hint_list hintlist =
- (str " " ++ hov 0 (prlist pr_hint hintlist) ++ fnl ())
-
-let pr_hints_db (name,db,hintlist) =
- (str "In the database " ++ str name ++ str ":" ++
- if hintlist = [] then (str " nothing" ++ fnl ())
- else (fnl () ++ pr_hint_list hintlist))
-
-(* Print all hints associated to head c in any database *)
-let pr_hint_list_for_head c =
- let dbs = Hintdbmap.to_list !searchtable in
- let valid_dbs =
- map_succeed
- (fun (name,db) -> (name,db, List.map (fun v -> 0, v) (Hint_db.map_all c db)))
- dbs
- in
- if valid_dbs = [] then
- (str "No hint declared for :" ++ pr_global c)
- else
- hov 0
- (str"For " ++ pr_global c ++ str" -> " ++ fnl () ++
- hov 0 (prlist pr_hints_db valid_dbs))
-
-let pr_hint_ref ref = pr_hint_list_for_head ref
-
-(* Print all hints associated to head id in any database *)
-let print_hint_ref ref = ppnl(pr_hint_ref ref)
-
-let pr_hint_term cl =
- try
- let dbs = Hintdbmap.to_list !searchtable in
- let valid_dbs =
- let fn = try
- let (hdc,args) = head_constr_bound cl in
- let hd = head_of_constr_reference hdc in
- if occur_existential cl then
- Hint_db.map_all hd
- else Hint_db.map_auto (hd, applist (hdc,args))
- with Bound -> Hint_db.map_none
- in
- let fn db = List.map (fun x -> 0, x) (fn db) in
- map_succeed (fun (name, db) -> (name, db, fn db)) dbs
- in
- if valid_dbs = [] then
- (str "No hint applicable for current goal")
- else
- (str "Applicable Hints :" ++ fnl () ++
- hov 0 (prlist pr_hints_db valid_dbs))
- with Match_failure _ | Failure _ ->
- (str "No hint applicable for current goal")
-
-let error_no_such_hint_database x =
- error ("No such Hint database: "^x^".")
-
-let print_hint_term cl = ppnl (pr_hint_term cl)
-
-(* print all hints that apply to the concl of the current goal *)
-let print_applicable_hint () =
- let pts = get_pftreestate () in
- let glss = Proof.V82.subgoals pts in
- match glss.Evd.it with
- | [] -> Util.error "No focused goal."
- | g::_ ->
- let gl = { Evd.it = g; sigma = glss.Evd.sigma } in
- print_hint_term (pf_concl gl)
-
-(* displays the whole hint database db *)
-let print_hint_db db =
- let (ids, csts) = Hint_db.transparent_state db in
- msgnl (hov 0
- ((if Hint_db.use_dn db then str"Discriminated database"
- else str"Non-discriminated database")));
- msgnl (hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids));
- msgnl (hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts));
- msgnl (hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)));
- Hint_db.iter
- (fun head hintlist ->
- match head with
- | Some head ->
- msg (hov 0
- (str "For " ++ pr_global head ++ str " -> " ++
- pr_hint_list (List.map (fun x -> (0,x)) hintlist)))
- | None ->
- msg (hov 0
- (str "For any goal -> " ++
- pr_hint_list (List.map (fun x -> (0, x)) hintlist))))
- db
-
-let print_hint_db_by_name dbname =
- try
- let db = searchtable_map dbname in print_hint_db db
- with Not_found ->
- error_no_such_hint_database dbname
-
-(* displays all the hints of all databases *)
-let print_searchtable () =
- Hintdbmap.iter
- (fun name db ->
- msg (str "In the database " ++ str name ++ str ":" ++ fnl ());
- print_hint_db db)
- !searchtable
+open Locus
+open Proofview.Notations
+open Hints
(**************************************************************************)
(* Automatic tactics *)
@@ -1015,79 +33,82 @@ let print_searchtable () =
(* tactics with a trace mechanism for automatic search *)
(**************************************************************************)
-let priority l = List.filter (fun (_, hint) -> hint.pri = 0) l
+let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l
(* tell auto not to reuse already instantiated metas in unification (for
compatibility, since otherwise, apply succeeds oftener) *)
open Unification
-let auto_unif_flags = {
- modulo_conv_on_closed_terms = Some full_transparent_state;
- use_metas_eagerly_in_conv_on_closed_terms = false;
- modulo_delta = empty_transparent_state;
+let auto_core_unif_flags_of st1 st2 useeager = {
+ modulo_conv_on_closed_terms = Some st1;
+ use_metas_eagerly_in_conv_on_closed_terms = useeager;
+ use_evars_eagerly_in_conv_on_closed_terms = false;
+ modulo_delta = st2;
modulo_delta_types = full_transparent_state;
- modulo_delta_in_merge = None;
check_applied_meta_types = false;
- resolve_evars = true;
use_pattern_unification = false;
use_meta_bound_pattern_unification = true;
- frozen_evars = ExistentialSet.empty;
+ frozen_evars = Evar.Set.empty;
restrict_conv_on_strict_subterms = false; (* Compat *)
modulo_betaiota = false;
modulo_eta = true;
- allow_K_in_toplevel_higher_order_unification = false
}
-(* Try unification with the precompiled clause, then use registered Apply *)
+let auto_unif_flags_of st1 st2 useeager =
+ let flags = auto_core_unif_flags_of st1 st2 useeager in {
+ core_unify_flags = flags;
+ merge_unify_flags = flags;
+ subterm_unify_flags = { flags with modulo_delta = empty_transparent_state };
+ allow_K_in_toplevel_higher_order_unification = false;
+ resolve_evars = true
+}
-let h_clenv_refine ev c clenv =
- Refiner.abstract_tactic (TacApply (true,ev,[c,NoBindings],None))
- (Clenvtac.clenv_refine ev clenv)
+let auto_unif_flags =
+ auto_unif_flags_of full_transparent_state empty_transparent_state false
-let unify_resolve_nodelta (c,clenv) gl =
- let clenv' = connect_clenv gl clenv in
- let clenv'' = clenv_unique_resolver ~flags:auto_unif_flags clenv' gl in
- h_clenv_refine false c clenv'' gl
+let auto_flags_of_state st =
+ auto_unif_flags_of full_transparent_state st false
-let unify_resolve flags (c,clenv) gl =
- let clenv' = connect_clenv gl clenv in
- let clenv'' = clenv_unique_resolver ~flags clenv' gl in
- h_clenv_refine false c clenv'' gl
+(* Try unification with the precompiled clause, then use registered Apply *)
-let unify_resolve_gen = function
- | None -> unify_resolve_nodelta
- | Some flags -> unify_resolve flags
+let unify_resolve_nodelta poly (c,clenv) =
+ Proofview.Goal.nf_enter begin fun gl ->
+ let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
+ let clenv' = Tacmach.New.of_old connect_clenv gl clenv' in
+ let clenv'' = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags:auto_unif_flags clenv' gl) gl in
+ Clenvtac.clenv_refine false clenv''
+ end
+
+let unify_resolve poly flags (c,clenv) =
+ Proofview.Goal.nf_enter begin fun gl ->
+ let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
+ let clenv' = Tacmach.New.of_old connect_clenv gl clenv' in
+ let clenv'' = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv' gl) gl in
+ Clenvtac.clenv_refine false clenv''
+ end
+
+let unify_resolve_gen poly = function
+ | None -> unify_resolve_nodelta poly
+ | Some flags -> unify_resolve poly flags
+
+let exact poly (c,clenv) =
+ let ctx, c' =
+ if poly then
+ let evd', subst = Evd.refresh_undefined_universes clenv.evd in
+ let ctx = Evd.evar_universe_context evd' in
+ ctx, subst_univs_level_constr subst c
+ else
+ let ctx = Evd.evar_universe_context clenv.evd in
+ ctx, c
+ in
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in
+ Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (exact_check c')
+ end
(* Util *)
-let expand_constructor_hints env lems =
- list_map_append (fun (sigma,lem) ->
- match kind_of_term lem with
- | Ind ind ->
- list_tabulate (fun i -> mkConstruct (ind,i+1)) (nconstructors ind)
- | _ ->
- [prepare_hint env (sigma,lem)]) lems
-
-(* builds a hint database from a constr signature *)
-(* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
-
-let add_hint_lemmas eapply lems hint_db gl =
- let lems = expand_constructor_hints (pf_env gl) lems in
- let hintlist' =
- list_map_append (pf_apply make_resolves gl (eapply,true,false) None) lems in
- Hint_db.add_list hintlist' hint_db
-
-let make_local_hint_db ?ts eapply lems gl =
- let sign = pf_hyps gl in
- let ts = match ts with
- | None -> Hint_db.transparent_state (searchtable_map "core")
- | Some ts -> ts
- in
- let hintlist = list_map_append (pf_apply make_resolve_hyp gl) sign in
- add_hint_lemmas eapply lems
- (Hint_db.add_list hintlist (Hint_db.empty ts false)) gl
-
(* Serait-ce possible de compiler d'abord la tactique puis de faire la
substitution sans passer par bdize dont l'objectif est de préparer un
terme pour l'affichage ? (HH) *)
@@ -1100,19 +121,23 @@ si après Intros la conclusion matche le pattern.
(* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
-let forward_interp_tactic =
- ref (fun _ -> failwith "interp_tactic is not installed for auto")
-
-let set_extern_interp f = forward_interp_tactic := f
+let (forward_interp_tactic, extern_interp) = Hook.make ()
-let conclPattern concl pat tac gl =
- let constr_bindings =
+let conclPattern concl pat tac =
+ let constr_bindings env sigma =
match pat with
- | None -> []
+ | None -> Proofview.tclUNIT Id.Map.empty
| Some pat ->
- try matches pat concl
- with PatternMatchingFailure -> error "conclPattern" in
- !forward_interp_tactic constr_bindings tac gl
+ try
+ Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
+ with Constr_matching.PatternMatchingFailure ->
+ Proofview.tclZERO (UserError ("conclPattern",str"conclPattern"))
+ in
+ Proofview.Goal.enter (fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ constr_bindings env sigma >>= fun constr_bindings ->
+ Hook.get forward_interp_tactic constr_bindings tac)
(***********************************************************)
(** A debugging / verbosity framework for trivial and auto *)
@@ -1147,8 +172,8 @@ let no_dbg () = (Off,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
+ if debug == Debug || !global_debug_trivial then Debug
+ else if debug == Info || !global_info_trivial then Info
else Off
in (d,0,ref [])
@@ -1157,8 +182,8 @@ let mk_trivial_dbg debug =
let mk_auto_dbg debug =
let d =
- if debug = Debug || !global_debug_auto then Debug
- else if debug = Info || !global_info_auto then Info
+ if debug == Debug || !global_debug_auto then Debug
+ else if debug == Info || !global_info_auto then Info
else Off
in (d,1,ref [])
@@ -1172,25 +197,27 @@ let tclLOG (dbg,depth,trace) pp tac =
| Debug ->
(* For "debug (trivial/auto)", we directly output messages *)
let s = String.make depth '*' in
- begin fun gl ->
+ Proofview.V82.tactic begin fun gl ->
try
- let out = tac gl in
+ let out = Proofview.V82.of_tactic tac gl in
msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
out
with reraise ->
+ let reraise = Errors.push reraise in
msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
- raise reraise
+ iraise reraise
end
| Info ->
(* For "info (trivial/auto)", we store a log trace *)
- begin fun gl ->
+ Proofview.V82.tactic begin fun gl ->
try
- let out = tac gl in
+ let out = Proofview.V82.of_tactic tac gl in
trace := (depth, Some pp) :: !trace;
out
with reraise ->
+ let reraise = Errors.push reraise in
trace := (depth, None) :: !trace;
- raise reraise
+ iraise reraise
end
(** For info, from the linear trace information, we reconstitute the part
@@ -1207,37 +234,39 @@ let rec cleanup_info_trace depth acc = function
and erase_subtree depth = function
| [] -> []
- | (d,_) :: l -> if d = depth then l else erase_subtree depth l
+ | (d,_) :: l -> if Int.equal d depth then l else erase_subtree depth l
let pr_info_atom (d,pp) =
- msg_debug (str (String.make d ' ') ++ pp () ++ str ".")
+ str (String.make d ' ') ++ pp () ++ str "."
let pr_info_trace = function
| (Info,_,{contents=(d,Some pp)::l}) ->
- List.iter pr_info_atom (cleanup_info_trace d [(d,pp)] l)
- | _ -> ()
+ prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)
+ | _ -> mt ()
let pr_info_nop = function
- | (Info,_,_) -> msg_debug (str "idtac.")
- | _ -> ()
+ | (Info,_,_) -> str "idtac."
+ | _ -> mt ()
let pr_dbg_header = function
- | (Off,_,_) -> ()
- | (Debug,0,_) -> msg_debug (str "(* debug trivial : *)")
- | (Debug,_,_) -> msg_debug (str "(* debug auto : *)")
- | (Info,0,_) -> msg_debug (str "(* info trivial : *)")
- | (Info,_,_) -> msg_debug (str "(* info auto : *)")
+ | (Off,_,_) -> mt ()
+ | (Debug,0,_) -> str "(* debug trivial : *)"
+ | (Debug,_,_) -> str "(* debug auto : *)"
+ | (Info,0,_) -> str "(* info trivial : *)"
+ | (Info,_,_) -> str "(* info auto : *)"
let tclTRY_dbg d tac =
- tclORELSE0
- (fun gl ->
- pr_dbg_header d;
- let out = tac gl in
- pr_info_trace d;
- out)
- (fun gl ->
- pr_info_nop d;
- tclIDTAC gl)
+ let (level, _, _) = d in
+ let delay f = Proofview.tclUNIT () >>= fun () -> f () in
+ let tac = match level with
+ | Off -> tac
+ | Debug | Info -> delay (fun () -> msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d); tac)
+ in
+ let after = match level with
+ | Info -> delay (fun () -> msg_debug (pr_info_nop d); Proofview.tclUNIT ())
+ | Off | Debug -> Proofview.tclUNIT ()
+ in
+ Tacticals.New.tclORELSE0 tac after
(**************************************************************************)
(* The Trivial tactic *)
@@ -1247,16 +276,21 @@ let tclTRY_dbg d tac =
(* Papageno : cette fonction a été pas mal simplifiée depuis que la base
de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
+let auto_unif_flags =
+ auto_unif_flags_of full_transparent_state empty_transparent_state false
+
let flags_of_state st =
- {auto_unif_flags with
- modulo_conv_on_closed_terms = Some st; modulo_delta = st}
+ auto_unif_flags_of st st false
+
+let auto_flags_of_state st =
+ auto_unif_flags_of full_transparent_state st false
let hintmap_of hdc concl =
match hdc with
| None -> Hint_db.map_none
| Some hdc ->
- if occur_existential concl then Hint_db.map_all hdc
- else Hint_db.map_auto (hdc,concl)
+ if occur_existential concl then Hint_db.map_existential hdc concl
+ else Hint_db.map_auto hdc concl
let exists_evaluable_reference env = function
| EvalConstRef _ -> true
@@ -1265,41 +299,49 @@ let exists_evaluable_reference env = function
let dbg_intro dbg = tclLOG dbg (fun () -> str "intro") intro
let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
-let rec trivial_fail_db dbg mod_delta db_list local_db gl =
+let rec trivial_fail_db dbg mod_delta db_list local_db =
let intro_tac =
- tclTHEN (dbg_intro dbg)
- (fun g'->
- let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
- in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db) g')
+ Tacticals.New.tclTHEN (dbg_intro dbg)
+ ( Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma 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 hyp = Context.map_named_declaration nf decl in
+ let hintl = make_resolve_hyp env sigma hyp
+ in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db)
+ end)
in
- tclFIRST
- ((dbg_assumption dbg)::intro_tac::
- (List.map tclCOMPLETE
- (trivial_resolve dbg mod_delta db_list local_db (pf_concl gl)))) gl
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Tacmach.New.pf_nf_concl gl in
+ Tacticals.New.tclFIRST
+ ((dbg_assumption dbg)::intro_tac::
+ (List.map Tacticals.New.tclCOMPLETE
+ (trivial_resolve dbg mod_delta db_list local_db concl)))
+ end
and my_find_search_nodelta db_list local_db hdc concl =
List.map (fun hint -> (None,hint))
- (list_map_append (hintmap_of hdc concl) (local_db::db_list))
+ (List.map_append (hintmap_of 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 hdc concl =
- let flags = {auto_unif_flags with use_metas_eagerly_in_conv_on_closed_terms = true} in
let f = hintmap_of hdc concl in
if occur_existential concl then
- list_map_append
+ List.map_append
(fun db ->
if Hint_db.use_dn db then
let flags = flags_of_state (Hint_db.transparent_state db) in
List.map (fun x -> (Some flags,x)) (f db)
else
- let flags = {flags with modulo_delta = Hint_db.transparent_state db} in
+ let flags = auto_flags_of_state (Hint_db.transparent_state db) in
List.map (fun x -> (Some flags,x)) (f db))
(local_db::db_list)
else
- list_map_append (fun db ->
+ List.map_append (fun db ->
if Hint_db.use_dn db then
let flags = flags_of_state (Hint_db.transparent_state db) in
List.map (fun x -> (Some flags, x)) (f db)
@@ -1309,39 +351,40 @@ and my_find_search_delta db_list local_db hdc concl =
let l =
match hdc with None -> Hint_db.map_none db
| Some hdc ->
- if (Idpred.is_empty ids && Cpred.is_empty csts)
- then Hint_db.map_auto (hdc,concl) db
- else Hint_db.map_all hdc db
- in {flags with modulo_delta = st}, l
+ if (Id.Pred.is_empty ids && Cpred.is_empty csts)
+ then Hint_db.map_auto hdc concl db
+ else Hint_db.map_existential hdc concl db
+ in auto_flags_of_state st, l
in List.map (fun x -> (Some flags,x)) l)
(local_db::db_list)
-and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t})) =
+and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) =
let tactic =
match t with
- | Res_pf (c,cl) -> unify_resolve_gen flags (c,cl)
- | ERes_pf _ -> (fun gl -> error "eres_pf")
- | Give_exact c -> exact_check c
+ | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
+ | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
+ | Give_exact (c, cl) -> exact poly (c, cl)
| Res_pf_THEN_trivial_fail (c,cl) ->
- tclTHEN
- (unify_resolve_gen flags (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 ()) (flags <> None) db_list local_db)
+ (trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db)
| Unfold_nth c ->
- (fun gl ->
+ Proofview.V82.tactic (fun gl ->
if exists_evaluable_reference (pf_env gl) c then
- tclPROGRESS (h_reduce (Unfold [all_occurrences_expr,c]) onConcl) gl
+ tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) gl
else tclFAIL 0 (str"Unbound reference") gl)
- | Extern tacast -> conclPattern concl p tacast
+ | Extern tacast ->
+ conclPattern concl p tacast
in
tclLOG dbg (fun () -> pr_autotactic t) tactic
and trivial_resolve dbg mod_delta db_list local_db cl =
try
let head =
- try let hdconstr,_ = head_constr_bound cl in
- Some (head_of_constr_reference hdconstr)
+ try let hdconstr = decompose_app_bound cl in
+ Some hdconstr
with Bound -> None
in
List.map (tac_of_hint dbg db_list local_db cl)
@@ -1352,36 +395,33 @@ and trivial_resolve dbg mod_delta db_list local_db cl =
(** The use of the "core" database can be de-activated by passing
"nocore" amongst the databases. *)
-let make_db_list dbnames =
- let use_core = not (List.mem "nocore" dbnames) in
- let dbnames = list_remove "nocore" dbnames in
- let dbnames = if use_core then "core"::dbnames else dbnames in
- let lookup db =
- try searchtable_map db with Not_found -> error_no_such_hint_database db
- in
- List.map lookup dbnames
-
-let trivial ?(debug=Off) lems dbnames gl =
+let trivial ?(debug=Off) lems dbnames =
+ Proofview.Goal.nf_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
let db_list = make_db_list dbnames in
let d = mk_trivial_dbg debug in
+ let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
- (trivial_fail_db d false db_list (make_local_hint_db false lems gl)) gl
-
-let full_trivial ?(debug=Off) lems gl =
- let dbnames = Hintdbmap.dom !searchtable in
- let dbnames = list_remove "v62" dbnames in
- let db_list = List.map (fun x -> searchtable_map x) dbnames in
+ (trivial_fail_db d false db_list hints)
+ end
+
+let full_trivial ?(debug=Off) lems =
+ Proofview.Goal.nf_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let db_list = current_pure_db () in
let d = mk_trivial_dbg debug in
+ let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
- (trivial_fail_db d false db_list (make_local_hint_db false lems gl)) gl
+ (trivial_fail_db d false db_list hints)
+ end
let gen_trivial ?(debug=Off) lems = function
| None -> full_trivial ~debug lems
| Some l -> trivial ~debug lems l
-let h_trivial ?(debug=Off) lems l =
- Refiner.abstract_tactic (TacTrivial (debug,List.map snd lems,l))
- (gen_trivial ~debug lems l)
+let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l
(**************************************************************************)
(* The classical Auto tactic *)
@@ -1390,88 +430,90 @@ let h_trivial ?(debug=Off) lems l =
let possible_resolve dbg mod_delta db_list local_db cl =
try
let head =
- try let hdconstr,_ = head_constr_bound cl in
- Some (head_of_constr_reference hdconstr)
+ try let hdconstr = decompose_app_bound 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 head cl)
with Not_found -> []
-let dbg_case dbg id =
- tclLOG dbg (fun () -> str "case " ++ pr_id id) (simplest_case (mkVar id))
-
-let decomp_unary_term_then dbg (id,_,typc) kont1 kont2 gl =
- try
- let ccl = applist (head_constr typc) in
- match Hipattern.match_with_conjunction ccl with
- | Some (_,args) ->
- tclTHEN (dbg_case dbg id) (kont1 (List.length args)) gl
- | None ->
- kont2 gl
- with UserError _ -> kont2 gl
-
-let decomp_empty_term dbg (id,_,typc) gl =
- if Hipattern.is_empty_type typc then
- dbg_case dbg id gl
- else
- errorlabstrm "Auto.decomp_empty_term" (str "Not an empty type.")
-
-let extend_local_db gl decl db =
- Hint_db.add_list (make_resolve_hyp (pf_env gl) (project gl) decl) db
+let extend_local_db decl db gl =
+ Hint_db.add_list (make_resolve_hyp (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) decl) db
(* Introduce an hypothesis, then call the continuation tactic [kont]
with the hint db extended with the so-obtained hypothesis *)
let intro_register dbg kont db =
- tclTHEN (dbg_intro dbg)
- (onLastDecl (fun decl gl -> kont (extend_local_db gl decl db) gl))
+ Tacticals.New.tclTHEN (dbg_intro dbg)
+ (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)
(* n is the max depth of search *)
(* local_db contains the local Hypotheses *)
-exception Uplift of tactic list
-
let search d n mod_delta db_list local_db =
let rec search d n local_db =
- if n=0 then (fun gl -> error "BOUND 2") else
- tclORELSE0 (dbg_assumption d)
- (tclORELSE0 (intro_register d (search d n) local_db)
- (fun gl ->
- let d' = incr_dbg d in
- tclFIRST
- (List.map
- (fun ntac -> tclTHEN ntac (search d' (n-1) local_db))
- (possible_resolve d mod_delta db_list local_db (pf_concl gl))) gl))
+ (* spiwack: the test of [n] to 0 must be done independently in
+ each goal. Hence the [tclEXTEND] *)
+ Proofview.tclEXTEND [] begin
+ if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else
+ Tacticals.New.tclORELSE0 (dbg_assumption d)
+ (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
+ ( Proofview.Goal.enter begin fun gl ->
+ let concl = Tacmach.New.pf_nf_concl 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 concl))
+ end))
+ end []
in
search d n local_db
let default_search_depth = ref 5
-let delta_auto ?(debug=Off) mod_delta n lems dbnames gl =
+let delta_auto debug mod_delta n lems dbnames =
+ Proofview.Goal.nf_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
let db_list = make_db_list dbnames in
let d = mk_auto_dbg debug in
+ let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
- (search d n mod_delta db_list (make_local_hint_db false lems gl)) gl
+ (search d n mod_delta db_list hints)
+ end
-let auto ?(debug=Off) n = delta_auto ~debug false n
+let delta_auto =
+ if Flags.profile then
+ let key = Profile.declare_profile "delta_auto" in
+ Profile.profile5 key delta_auto
+ else delta_auto
-let new_auto ?(debug=Off) n = delta_auto ~debug true n
+let auto ?(debug=Off) n = delta_auto debug false n
+
+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 gl =
- let dbnames = Hintdbmap.dom !searchtable in
- let dbnames = list_remove "v62" dbnames in
- let db_list = List.map (fun x -> searchtable_map x) dbnames in
+let delta_full_auto ?(debug=Off) mod_delta n lems =
+ Proofview.Goal.nf_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let db_list = current_pure_db () in
let d = mk_auto_dbg debug in
+ let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
- (search d n mod_delta db_list (make_local_hint_db false lems gl)) gl
+ (search d n mod_delta db_list hints)
+ 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
-let default_full_auto gl = full_auto !default_search_depth [] gl
+let default_full_auto = full_auto !default_search_depth []
let gen_auto ?(debug=Off) n lems dbnames =
let n = match n with None -> !default_search_depth | Some n -> n in
@@ -1479,8 +521,4 @@ let gen_auto ?(debug=Off) n lems dbnames =
| None -> full_auto ~debug n lems
| Some l -> auto ~debug n lems l
-let inj_or_var = Option.map (fun n -> ArgArg n)
-
-let h_auto ?(debug=Off) n lems l =
- Refiner.abstract_tactic (TacAuto (debug,inj_or_var n,List.map snd lems,l))
- (gen_auto ~debug n lems l)
+let h_auto ?(debug=Off) n lems l = gen_auto ~debug n lems l
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-17 02:49:53 +0000