diff options
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml (renamed from tactics/eauto.ml4) | 161 | ||||
| -rw-r--r-- | tactics/eauto.mli | 14 | ||||
| -rw-r--r-- | tactics/g_auto.ml4 | 130 | ||||
| -rw-r--r-- | tactics/hightactics.mllib | 2 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 1 |
6 files changed, 151 insertions, 159 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c8f8a19e5..02cd819f4 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1407,7 +1407,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = (* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *) (* rewrite *) (* ) *) - Eauto.gen_eauto (false,5) [] (Some []) + Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some [])) ] gls diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml index f2d26ec86..a118f2642 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml @@ -30,8 +30,6 @@ open Locusops open Hints open Proofview.Notations -DECLARE PLUGIN "eauto" - let eauto_unif_flags = auto_flags_of_state full_transparent_state let e_give_exact ?(flags=eauto_unif_flags) c = @@ -50,14 +48,6 @@ let e_assumption = Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl)) end } -TACTIC EXTEND eassumption -| [ "eassumption" ] -> [ e_assumption ] -END - -TACTIC EXTEND eexact -| [ "eexact" constr(c) ] -> [ e_give_exact c ] -END - let registered_e_assumption = Proofview.Goal.enter { enter = begin fun gl -> Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id)) @@ -112,7 +102,8 @@ let out_term = function | IsConstr (c, _) -> c | IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr) -let prolog_tac l n gl = +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 @@ -122,11 +113,7 @@ let prolog_tac l n gl = try (prolog l n gl) with UserError ("Refiner.tclFIRST",_) -> errorlabstrm "Prolog.prolog" (str "Prolog failed.") - -TACTIC EXTEND prolog -| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] -> - [ Proofview.V82.tactic (prolog_tac (eval_uconstrs ist l) n) ] -END + end open Auto open Unification @@ -442,8 +429,8 @@ let full_eauto ?(debug=Off) n lems gl = tclTRY (e_search_auto debug n lems db_list) gl let gen_eauto ?(debug=Off) np lems = function - | None -> full_eauto ~debug np lems - | Some l -> eauto ~debug np lems l + | 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 @@ -453,44 +440,6 @@ let make_dimension n = function | None -> (true,make_depth n) | Some d -> (false,d) -open Genarg -open G_auto - -let hintbases = G_auto.hintbases -let wit_hintbases = G_auto.wit_hintbases - -TACTIC EXTEND eauto -| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) - hintbases(db) ] -> - [ Proofview.V82.tactic (gen_eauto (make_dimension n p) (eval_uconstrs ist lems) db) ] -END - -TACTIC EXTEND new_eauto -| [ "new" "auto" int_or_var_opt(n) auto_using(lems) - hintbases(db) ] -> - [ match db with - | None -> new_full_auto (make_depth n) (eval_uconstrs ist lems) - | Some l -> new_auto (make_depth n) (eval_uconstrs ist lems) l ] -END - -TACTIC EXTEND debug_eauto -| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) - hintbases(db) ] -> - [ Proofview.V82.tactic (gen_eauto ~debug:Debug (make_dimension n p) (eval_uconstrs ist lems) db) ] -END - -TACTIC EXTEND info_eauto -| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) - hintbases(db) ] -> - [ Proofview.V82.tactic (gen_eauto ~debug:Info (make_dimension n p) (eval_uconstrs ist lems) db) ] -END - -TACTIC EXTEND dfs_eauto -| [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems) - hintbases(db) ] -> - [ Proofview.V82.tactic (gen_eauto (true, make_depth p) (eval_uconstrs ist lems) db) ] -END - let cons a l = a :: l let autounfolds db occs cls gl = @@ -505,25 +454,24 @@ let autounfolds db occs cls gl = (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 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 gl = +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 gl - -TACTIC EXTEND autounfold -| [ "autounfold" hintbases(db) clause(cl) ] -> [ Proofview.V82.tactic (autounfold_tac db cl) ] -END + autounfold dbs cls let unfold_head env (ids, csts) c = let rec aux c = @@ -578,90 +526,3 @@ let autounfold_one db cl = | None -> convert_concl_no_check c' DEFAULTcast else Tacticals.New.tclFAIL 0 (str "Nothing to unfold") end } - -(* Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *) -(* (Id.Set.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *) -(* in unfold_option unfolds cl *) - -(* let db = try searchtable_map dbname *) -(* with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) *) -(* in *) -(* let (ids, csts) = Hint_db.unfolds db in *) -(* Cset.fold (fun cst -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cst)) csts *) -(* (Id.Set.fold (fun id -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cl) ids acc))) *) -(* (tclFAIL 0 (mt())) db *) - -TACTIC EXTEND autounfold_one -| [ "autounfold_one" hintbases(db) "in" hyp(id) ] -> - [ autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, InHyp)) ] -| [ "autounfold_one" hintbases(db) ] -> - [ autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ] - END - -TACTIC EXTEND autounfoldify -| [ "autounfoldify" constr(x) ] -> [ - Proofview.V82.tactic ( - let db = match kind_of_term x with - | Const (c,_) -> Label.to_string (con_label c) - | _ -> assert false - in autounfold ["core";db] onConcl - )] -END - -TACTIC EXTEND unify -| ["unify" constr(x) constr(y) ] -> [ unify x y ] -| ["unify" constr(x) constr(y) "with" preident(base) ] -> [ - let table = try Some (searchtable_map base) with Not_found -> None in - match table with - | None -> - let msg = str "Hint table " ++ str base ++ str " not found" in - Tacticals.New.tclZEROMSG msg - | Some t -> - let state = Hint_db.transparent_state t in - unify ~state x y - ] -END - - -TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ] -END - -let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom - -ARGUMENT EXTEND hints_path_atom - TYPED AS hints_path_atom - PRINTED BY pr_hints_path_atom -| [ global_list(g) ] -> [ PathHints (List.map Nametab.global g) ] -| [ "*" ] -> [ PathAny ] -END - -let pr_hints_path prc prx pry c = Hints.pp_hints_path c - -ARGUMENT EXTEND hints_path - TYPED AS hints_path - PRINTED BY pr_hints_path -| [ "(" hints_path(p) ")" ] -> [ p ] -| [ "!" hints_path(p) ] -> [ PathStar p ] -| [ "emp" ] -> [ PathEmpty ] -| [ "eps" ] -> [ PathEpsilon ] -| [ hints_path_atom(a) ] -> [ PathAtom a ] -| [ hints_path(p) "|" hints_path(q) ] -> [ PathOr (p, q) ] -| [ hints_path(p) ";" hints_path(q) ] -> [ PathSeq (p, q) ] -END - -let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases - -ARGUMENT EXTEND opthints - TYPED AS preident_list_opt - PRINTED BY pr_hintbases -| [ ":" ne_preident_list(l) ] -> [ Some l ] -| [ ] -> [ None ] -END - -VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF -| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ - let entry = HintsCutEntry p in - Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ())) - (match dbnames with None -> ["core"] | Some l -> l) entry ] -END diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 0a490c65d..8812093d5 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -10,22 +10,24 @@ open Term open Proof_type open Hints -val hintbases : hint_db_name list option Pcoq.Gram.entry - -val wit_hintbases : hint_db_name list option Genarg.uniform_genarg_type - val e_assumption : unit Proofview.tactic val registered_e_assumption : unit Proofview.tactic val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic +val prolog_tac : Tacexpr.delayed_open_constr list -> int -> unit Proofview.tactic + val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> Tacexpr.delayed_open_constr list -> - hint_db_name list option -> tactic + hint_db_name list option -> unit Proofview.tactic val eauto_with_bases : ?debug:Tacexpr.debug -> bool * int -> Tacexpr.delayed_open_constr list -> hint_db list -> Proof_type.tactic -val autounfold : hint_db_name list -> Locus.clause -> tactic +val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic +val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic +val autounfold_one : hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic + +val make_dimension : int option -> int option -> bool * int diff --git a/tactics/g_auto.ml4 b/tactics/g_auto.ml4 index 3a2cee9f7..f4fae763f 100644 --- a/tactics/g_auto.ml4 +++ b/tactics/g_auto.ml4 @@ -16,6 +16,15 @@ DECLARE PLUGIN "g_auto" (* Hint bases *) + +TACTIC EXTEND eassumption +| [ "eassumption" ] -> [ Eauto.e_assumption ] +END + +TACTIC EXTEND eexact +| [ "eexact" constr(c) ] -> [ Eauto.e_give_exact c ] +END + let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases ARGUMENT EXTEND hintbases @@ -45,6 +54,8 @@ ARGUMENT EXTEND auto_using | [ ] -> [ [] ] END +(** Auto *) + TACTIC EXTEND trivial | [ "trivial" auto_using(lems) hintbases(db) ] -> [ Auto.h_trivial (eval_uconstrs ist lems) db ] @@ -74,3 +85,122 @@ TACTIC EXTEND debug_auto | [ "debug" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> [ Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db ] END + +(** Eauto *) + +TACTIC EXTEND prolog +| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] -> + [ Eauto.prolog_tac (eval_uconstrs ist l) n ] +END + +let make_depth n = snd (Eauto.make_dimension n None) + +TACTIC EXTEND eauto +| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + [ Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ] +END + +TACTIC EXTEND new_eauto +| [ "new" "auto" int_or_var_opt(n) auto_using(lems) + hintbases(db) ] -> + [ match db with + | None -> Auto.new_full_auto (make_depth n) (eval_uconstrs ist lems) + | Some l -> Auto.new_auto (make_depth n) (eval_uconstrs ist lems) l ] +END + +TACTIC EXTEND debug_eauto +| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + [ Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ] +END + +TACTIC EXTEND info_eauto +| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + [ Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ] +END + +TACTIC EXTEND dfs_eauto +| [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + [ Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db ] +END + +TACTIC EXTEND autounfold +| [ "autounfold" hintbases(db) clause(cl) ] -> [ Eauto.autounfold_tac db cl ] +END + +TACTIC EXTEND autounfold_one +| [ "autounfold_one" hintbases(db) "in" hyp(id) ] -> + [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, Locus.InHyp)) ] +| [ "autounfold_one" hintbases(db) ] -> + [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ] + END + +TACTIC EXTEND autounfoldify +| [ "autounfoldify" constr(x) ] -> [ + let db = match Term.kind_of_term x with + | Term.Const (c,_) -> Names.Label.to_string (Names.con_label c) + | _ -> assert false + in Eauto.autounfold ["core";db] Locusops.onConcl + ] +END + +TACTIC EXTEND unify +| ["unify" constr(x) constr(y) ] -> [ Tactics.unify x y ] +| ["unify" constr(x) constr(y) "with" preident(base) ] -> [ + let table = try Some (Hints.searchtable_map base) with Not_found -> None in + match table with + | None -> + let msg = str "Hint table " ++ str base ++ str " not found" in + Tacticals.New.tclZEROMSG msg + | Some t -> + let state = Hints.Hint_db.transparent_state t in + Tactics.unify ~state x y + ] +END + + +TACTIC EXTEND convert_concl_no_check +| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ] +END + +let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom + +ARGUMENT EXTEND hints_path_atom + TYPED AS hints_path_atom + PRINTED BY pr_hints_path_atom +| [ global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ] +| [ "*" ] -> [ Hints.PathAny ] +END + +let pr_hints_path prc prx pry c = Hints.pp_hints_path c + +ARGUMENT EXTEND hints_path + TYPED AS hints_path + PRINTED BY pr_hints_path +| [ "(" hints_path(p) ")" ] -> [ p ] +| [ "!" hints_path(p) ] -> [ Hints.PathStar p ] +| [ "emp" ] -> [ Hints.PathEmpty ] +| [ "eps" ] -> [ Hints.PathEpsilon ] +| [ hints_path_atom(a) ] -> [ Hints.PathAtom a ] +| [ hints_path(p) "|" hints_path(q) ] -> [ Hints.PathOr (p, q) ] +| [ hints_path(p) ";" hints_path(q) ] -> [ Hints.PathSeq (p, q) ] +END + +let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases + +ARGUMENT EXTEND opthints + TYPED AS preident_list_opt + PRINTED BY pr_hintbases +| [ ":" ne_preident_list(l) ] -> [ Some l ] +| [ ] -> [ None ] +END + +VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF +| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ + let entry = Hints.HintsCutEntry p in + Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ())) + (match dbnames with None -> ["core"] | Some l -> l) entry ] +END diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index 30e97f62d..0d73cc27a 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -1,8 +1,8 @@ Extraargs Coretactics Extratactics -G_auto Eauto +G_auto Class_tactics G_class Rewrite diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 55eb699be..65ea8028d 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -86,7 +86,6 @@ Open Scope type_scope. Declare ML Module "coretactics". Declare ML Module "extratactics". Declare ML Module "g_auto". -Declare ML Module "eauto". Declare ML Module "g_class". Declare ML Module "g_eqdecide". Declare ML Module "g_rewrite". |