From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- plugins/ltac/g_auto.ml4 | 228 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 228 insertions(+) create mode 100644 plugins/ltac/g_auto.ml4 (limited to 'plugins/ltac/g_auto.ml4') diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 new file mode 100644 index 00000000..643f7e99 --- /dev/null +++ b/plugins/ltac/g_auto.ml4 @@ -0,0 +1,228 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* [ 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 + TYPED AS preident_list_opt + PRINTED BY pr_hintbases +| [ "with" "*" ] -> [ None ] +| [ "with" ne_preident_list(l) ] -> [ Some l ] +| [ ] -> [ Some [] ] +END + +let eval_uconstrs ist cs = + let flags = { + Pretyping.use_typeclasses = false; + solve_unification_constraints = true; + use_hook = Pfedit.solve_by_implicit_tactic (); + fail_evar = false; + expand_evars = true + } in + let map c env sigma = c env sigma in + List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs + +let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr +let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env c) +let pr_auto_using _ _ _ = Pptactic.pr_auto_using + (let sigma, env = Pfedit.get_current_context () in + Printer.pr_closed_glob_env env sigma) + +ARGUMENT EXTEND auto_using + TYPED AS uconstr_list + PRINTED BY pr_auto_using + RAW_TYPED AS uconstr_list + RAW_PRINTED BY pr_auto_using_raw + GLOB_TYPED AS uconstr_list + GLOB_PRINTED BY pr_auto_using_glob +| [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ] +| [ ] -> [ [] ] +END + +(** Auto *) + +TACTIC EXTEND trivial +| [ "trivial" auto_using(lems) hintbases(db) ] -> + [ Auto.h_trivial (eval_uconstrs ist lems) db ] +END + +TACTIC EXTEND info_trivial +| [ "info_trivial" auto_using(lems) hintbases(db) ] -> + [ Auto.h_trivial ~debug:Info (eval_uconstrs ist lems) db ] +END + +TACTIC EXTEND debug_trivial +| [ "debug" "trivial" auto_using(lems) hintbases(db) ] -> + [ Auto.h_trivial ~debug:Debug (eval_uconstrs ist lems) db ] +END + +TACTIC EXTEND auto +| [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> + [ Auto.h_auto n (eval_uconstrs ist lems) db ] +END + +TACTIC EXTEND info_auto +| [ "info_auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> + [ Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db ] +END + +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_dft_concl(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 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_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference +let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global +let glob_hints_path_atom ist = Hints.glob_hints_path_atom + +ARGUMENT EXTEND hints_path_atom + PRINTED BY pr_hints_path_atom + + GLOBALIZED BY glob_hints_path_atom + + RAW_PRINTED BY pr_pre_hints_path_atom + GLOB_PRINTED BY pr_hints_path_atom +| [ ne_global_list(g) ] -> [ Hints.PathHints g ] +| [ "_" ] -> [ Hints.PathAny ] +END + +let pr_hints_path prc prx pry c = Hints.pp_hints_path c +let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c +let glob_hints_path ist = Hints.glob_hints_path + +ARGUMENT EXTEND hints_path +PRINTED BY pr_hints_path + +GLOBALIZED BY glob_hints_path +RAW_PRINTED BY pr_pre_hints_path +GLOB_PRINTED BY pr_hints_path + +| [ "(" hints_path(p) ")" ] -> [ p ] +| [ hints_path(p) "*" ] -> [ Hints.PathStar p ] +| [ "emp" ] -> [ Hints.PathEmpty ] +| [ "eps" ] -> [ Hints.PathEpsilon ] +| [ hints_path(p) "|" hints_path(q) ] -> [ Hints.PathOr (p, q) ] +| [ hints_path_atom(a) ] -> [ Hints.PathAtom a ] +| [ hints_path(p) hints_path(q) ] -> [ Hints.PathSeq (p, q) ] +END + +ARGUMENT EXTEND opthints + TYPED AS preident_list_opt + PRINTED BY pr_hintbases +| [ ":" ne_preident_list(l) ] -> [ Some l ] +| [ ] -> [ None ] +END + +VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF +| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ + fun ~atts ~st -> begin + let open Vernacinterp in + let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in + Hints.add_hints (Locality.make_section_locality atts.locality) + (match dbnames with None -> ["core"] | Some l -> l) entry; + st + end + ] +END + -- cgit v1.2.3