|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * 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) *)
(************************************************************************)
{
open Pp
open Stdarg
open Procq.Prim
open Procq.Constr
open Pltac
open Hints
}
DECLARE PLUGIN "rocq-runtime.plugins.ltac"
(* 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
TYPED AS preident list option
PRINTED BY { pr_hintbases }
| [ "with" "*" ] -> { None }
| [ "with" ne_preident_list(l) ] -> { Some l }
| [ ] -> { Some [] }
END
{
let eval_uconstrs ist cs =
let flags = Pretyping.{
use_coercions = true;
use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
program_mode = false;
polymorphic = false;
undeclared_evars_patvars = false;
patvars_abstract = false;
unconstrained_sorts = false;
} 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 env sigma _ _ _ = Pptactic.pr_auto_using @@ Ppconstr.pr_constr_expr env sigma
let pr_auto_using_glob env sigma _ _ _ = Pptactic.pr_auto_using (fun (c,_) ->
Printer.pr_glob_constr_env env sigma c)
let pr_auto_using env sigma _ _ _ = Pptactic.pr_auto_using @@
Printer.pr_closed_glob_env env sigma
}
ARGUMENT EXTEND auto_using
TYPED AS uconstr list
PRINTED BY { pr_auto_using env sigma }
RAW_PRINTED BY { pr_auto_using_raw env sigma }
GLOB_PRINTED BY { pr_auto_using_glob env sigma }
| [ "using" ne_uconstr_list_sep(l, ",") ] -> { l }
| [ ] -> { [] }
END
(** Auto *)
TACTIC EXTEND trivial
| [ "trivial" auto_using(lems) hintbases(db) ] ->
{ Auto.gen_trivial (eval_uconstrs ist lems) db }
END
TACTIC EXTEND info_trivial
| [ "info_trivial" auto_using(lems) hintbases(db) ] ->
{ Auto.gen_trivial ~debug:Info (eval_uconstrs ist lems) db }
END
TACTIC EXTEND debug_trivial
| [ "debug" "trivial" auto_using(lems) hintbases(db) ] ->
{ Auto.gen_trivial ~debug:Debug (eval_uconstrs ist lems) db }
END
TACTIC EXTEND auto
| [ "auto" nat_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
{ Auto.gen_auto n (eval_uconstrs ist lems) db }
END
TACTIC EXTEND info_auto
| [ "info_auto" nat_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
{ Auto.gen_auto ~debug:Info n (eval_uconstrs ist lems) db }
END
TACTIC EXTEND debug_auto
| [ "debug" "auto" nat_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
{ Auto.gen_auto ~debug:Debug n (eval_uconstrs ist lems) db }
END
(** Eauto *)
TACTIC EXTEND eauto
| [ "eauto" nat_or_var_opt(depth) auto_using(lems) hintbases(db) ] ->
{ Eauto.gen_eauto ?depth (eval_uconstrs ist lems) db }
END
TACTIC EXTEND debug_eauto
| [ "debug" "eauto" nat_or_var_opt(depth) auto_using(lems) hintbases(db) ] ->
{ Eauto.gen_eauto ~debug:Debug ?depth (eval_uconstrs ist lems) db }
END
TACTIC EXTEND info_eauto
| [ "info_eauto" nat_or_var_opt(depth) auto_using(lems) hintbases(db) ] ->
{ Eauto.gen_eauto ~debug:Info ?depth (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.tclZEROMSG msg
| Some t ->
let state = Hints.Hint_db.transparent_state t in
Tactics.unify ~state x y
}
END
TACTIC EXTEND convert
| ["convert" constr(x) constr(y) ] -> { Tactics.convert x y }
END
{
let pr_pre_hints_path c = Hints.pp_hints_path_gen Libnames.pr_qualid c
}
VERNAC ARGUMENT EXTEND hints_path
PRINTED BY { pr_pre_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) }
| [ ne_global_list(g) ] -> { Hints.PathAtom (Hints.PathHints g) }
| [ "_" ] -> { Hints.PathAtom Hints.PathAny }
| [ hints_path(p) hints_path(q) ] -> { Hints.PathSeq (p, q) }
END
ARGUMENT EXTEND opthints
TYPED AS preident list option
PRINTED BY { pr_hintbases }
| [ ":" ne_preident_list(l) ] -> { Some l }
| [ ] -> { None }
END
VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
| #[ locality = Attributes.hint_locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
Hints.add_hints ~locality
(match dbnames with None -> ["core"] | Some l -> l) entry;
}
END
[ Dauer der Verarbeitung: 0.4 Sekunden
(vorverarbeitet)
]
|
