diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 37 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 17 | ||||
| -rw-r--r-- | tactics/hints.ml | 14 | ||||
| -rw-r--r-- | tactics/hints.mli | 1 | ||||
| -rw-r--r-- | test-suite/success/Hints.v | 44 |
6 files changed, 94 insertions, 21 deletions
@@ -36,6 +36,8 @@ Tactics of incompatibilities). - Hints costs are now correctly taken into account (potential source of incompatibilities). +- Documented the Hint Cut command that allows control of the + proof-search during typeclass resolution (see reference manual). API diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index a21e5631f..1551b8eef 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3788,12 +3788,47 @@ Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. Goal forall a b:list (nat * nat), {a = b} + {a <> b}. -info_auto with eqdec. +Info 1 auto with eqdec. \end{coq_example} \begin{coq_eval} Abort. \end{coq_eval} +\item \texttt{Cut} {\textit{regexp}} +\label{HintCut} +\comindex{Hint Cut} + + \textit{Warning:} these hints currently only apply to typeclass proof search and + the \texttt{typeclasses eauto} tactic. + + This command can be used to cut the proof-search tree according to a + regular expression matching paths to be cut. The grammar for regular + expressions is the following: +\[\begin{array}{lcll} + e & ::= & \ident & \text{ hint or instance identifier } \\ + & & \texttt{*} & \text{ any hint } \\ + & & e | e' & \text{ disjunction } \\ + & & e ; e' & \text{ sequence } \\ + & & ! e & \text{ Kleene star } \\ + & & \texttt{emp} & \text{ empty } \\ + & & \texttt{eps} & \text{ epsilon } \\ + & & \texttt{(} e \texttt{)} & +\end{array}\] + +The \texttt{emp} regexp does not match any search path while +\texttt{eps} matches the empty path. During proof search, the path of +successive successful hints on a search branch is recorded, as a list of +identifiers for the hints (note \texttt{Hint Extern}'s do not have an +associated identitier). Before applying any hint $\ident$ the current +path $p$ extended with $\ident$ is matched against the current cut +expression $c$ associated to the hint database. If matching succeeds, +the hint is \emph{not} applied. The semantics of \texttt{Hint Cut} $e$ +is to set the cut expression to $c | e$, the initial cut expression +being \texttt{emp}. + + + + \end{itemize} \Rem One can use an \texttt{Extern} hint with no pattern to do diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index aa285fa98..ee7b94b0d 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -632,12 +632,7 @@ TACTIC EXTEND convert_concl_no_check | ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ] END - -let pr_hints_path_atom prc _ _ a = - match a with - | PathAny -> str"." - | PathHints grs -> - pr_sequence Printer.pr_global grs +let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom ARGUMENT EXTEND hints_path_atom TYPED AS hints_path_atom @@ -646,15 +641,7 @@ ARGUMENT EXTEND hints_path_atom | [ "*" ] -> [ PathAny ] END -let pr_hints_path prc prx pry c = - let rec aux = function - | PathAtom a -> pr_hints_path_atom prc prx pry a - | PathStar p -> str"(" ++ aux p ++ str")*" - | PathSeq (p, p') -> aux p ++ spc () ++ aux p' - | PathOr (p, p') -> str "(" ++ aux p ++ str"|" ++ aux p' ++ str")" - | PathEmpty -> str"ø" - | PathEpsilon -> str"ε" - in aux c +let pr_hints_path prc prx pry c = Hints.pp_hints_path c ARGUMENT EXTEND hints_path TYPED AS hints_path diff --git a/tactics/hints.ml b/tactics/hints.ml index 4ba9adafe..5630d20b5 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -382,15 +382,19 @@ let rec normalize_path h = let path_derivate hp hint = normalize_path (path_derivate hp hint) +let pp_hints_path_atom a = + match a with + | PathAny -> str"*" + | PathHints grs -> pr_sequence pr_global grs + let rec pp_hints_path = function - | PathAtom (PathAny) -> str"." - | PathAtom (PathHints grs) -> pr_sequence pr_global grs - | PathStar p -> str "(" ++ pp_hints_path p ++ str")*" + | PathAtom pa -> pp_hints_path_atom pa + | 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"ε" + | PathEmpty -> str"emp" + | PathEpsilon -> str"eps" let subst_path_atom subst p = match p with diff --git a/tactics/hints.mli b/tactics/hints.mli index af4d3d1f6..3a0521f66 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -70,6 +70,7 @@ type hints_path = val normalize_path : hints_path -> hints_path val path_matches : hints_path -> hints_path_atom list -> bool val path_derivate : hints_path -> hints_path_atom -> hints_path +val pp_hints_path_atom : hints_path_atom -> Pp.std_ppcmds val pp_hints_path : hints_path -> Pp.std_ppcmds module Hint_db : diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index cc8cec470..f934a5c74 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -62,3 +62,47 @@ Axiom cast_coalesce : ((e :? pf1) :? pf2) = (e :? trans_eq pf1 pf2). Hint Rewrite cast_coalesce : ltamer. + +Require Import Program. +Module HintCut. +Class A (f : nat -> nat) := a : True. +Class B (f : nat -> nat) := b : True. +Class C (f : nat -> nat) := c : True. +Class D (f : nat -> nat) := d : True. +Class E (f : nat -> nat) := e : True. + +Instance a_is_b f : A f -> B f. +Proof. easy. Qed. +Instance b_is_c f : B f -> C f. +Proof. easy. Qed. +Instance c_is_d f : C f -> D f. +Proof. easy. Qed. +Instance d_is_e f : D f -> E f. +Proof. easy. Qed. + +Instance a_compose f g : A f -> A g -> A (compose f g). +Proof. easy. Qed. +Instance b_compose f g : B f -> B g -> B (compose f g). +Proof. easy. Qed. +Instance c_compose f g : C f -> C g -> C (compose f g). +Proof. easy. Qed. +Instance d_compose f g : D f -> D g -> D (compose f g). +Proof. easy. Qed. +Instance e_compose f g : E f -> E g -> E (compose f g). +Proof. easy. Qed. + +Instance a_id : A id. +Proof. easy. Qed. + +Instance foo f : + E (id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ + id ∘ id ∘ id ∘ id ∘ id ∘ f ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id). +Proof. + Fail Timeout 1 apply _. (* 3.7s *) + +Hint Cut [!*; (a_is_b | b_is_c | c_is_d | d_is_e) ; + (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances. + + Timeout 1 Fail apply _. (* 0.06s *) +Abort. +End HintCut.
\ No newline at end of file |