Extend Hint Mode to handle the no-head-evar case

Suggested by R. Krebbers and C. Cohen, this makes modes
more applicable, by allowing to trigger resolution on partially
instantiated indices. This is a rough but fast approximation of the
pattern on which one would like instances to apply.

5 files changed, 39 insertions, 12 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index faa5ba251..45d71e32b 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -118,12 +118,17 @@ type reference_or_constr =
   | HintsReference of reference
   | HintsConstr of constr_expr
 
+type hint_mode =
+  | ModeInput (* No evars *)
+  | ModeNoHeadEvar (* No evar at the head *)
+  | ModeOutput (* Anything *)
+
 type hints_expr =
   | HintsResolve of (int option * bool * reference_or_constr) list
   | HintsImmediate of reference_or_constr list
   | HintsUnfold of reference list
   | HintsTransparency of reference list * bool
-  | HintsMode of reference * bool list
+  | HintsMode of reference * hint_mode list
   | HintsConstructors of reference list
   | HintsExtern of int * constr_expr option * raw_tactic_expr
 
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 422384f3d..b0ff8b64f 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -134,6 +134,8 @@ GEXTEND Gram
       | ":"; t = lconstr; ":="; c = lconstr -> CCast(!@loc,c,CastConv t) ] ]
   ;
   mode:
-    [ [ l = LIST1 ["+" -> true | "-" -> false] -> l ] ]
+    [ [ l = LIST1 [ "+" -> ModeInput
+                  | "!" -> ModeNoHeadEvar
+                  | "-" -> ModeOutput ] -> l ] ]
   ;
 END
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index f3558054b..5b73b054d 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -161,6 +161,11 @@ module Make
     | HintsReference r -> pr_reference r
     | HintsConstr c -> pr_c c
 
+  let pr_hint_mode = function
+    | ModeInput -> str"+"
+    | ModeNoHeadEvar -> str"!"
+    | ModeOutput -> str"-"
+
   let pr_hints db h pr_c pr_pat =
     let opth = pr_opt_hintbases db  in
     let pph =
@@ -182,8 +187,8 @@ module Make
         | HintsMode (m, l) ->
           keyword "Mode"
           ++ spc ()
-          ++ pr_reference m ++ spc() ++ prlist_with_sep spc
-            (fun b -> if b then str"+" else str"-") l
+          ++ pr_reference m ++ spc() ++
+            prlist_with_sep spc pr_hint_mode l
         | HintsConstructors c ->
           keyword "Constructors"
           ++ spc() ++ prlist_with_sep spc pr_reference c
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 565f2e0aa..95bf1babe 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -189,7 +189,7 @@ type search_entry = {
   sentry_nopat : stored_data list;
   sentry_pat : stored_data list;
   sentry_bnet : Bounded_net.t;
-  sentry_mode : bool array list;
+  sentry_mode : hint_mode array list;
 }
 
 let empty_se = {
@@ -442,9 +442,17 @@ module Hint_db = struct
  
   let realize_tac (id,tac) = tac
 
+  let match_mode m arg =
+    match m with
+    | ModeInput -> not (occur_existential arg)
+    | ModeNoHeadEvar ->
+       Evarutil.(try ignore(head_evar arg); false
+                 with NoHeadEvar -> true)
+    | ModeOutput -> true
+                               
   let matches_mode args mode =
-    Array.length args == Array.length mode &&
-      Array.for_all2 (fun arg m -> not (m && occur_existential arg)) args mode
+    Array.length mode == Array.length args &&
+      Array.for_all2 match_mode mode args
       
   let matches_modes args modes =
     if List.is_empty modes then true
@@ -872,7 +880,7 @@ type hint_action =
   | AddHints of hint_entry list
   | RemoveHints of global_reference list
   | AddCut of hints_path
-  | AddMode of global_reference * bool array
+  | AddMode of global_reference * hint_mode array
 
 let add_cut dbname path =
   let db = get_db dbname in
@@ -1078,7 +1086,7 @@ type hints_entry =
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
-  | HintsModeEntry of global_reference * bool list
+  | HintsModeEntry of global_reference * hint_mode list
   | HintsExternEntry of
       int * (patvar list * constr_pattern) option * glob_tactic_expr
 
@@ -1324,9 +1332,14 @@ let pr_applicable_hint () =
   | g::_ ->
     pr_hint_term (Goal.V82.concl glss.Evd.sigma g)
 
+let pp_hint_mode = function
+  | ModeInput -> str"+"
+  | ModeNoHeadEvar -> str"!"
+  | ModeOutput -> str"-"
+
 (* displays the whole hint database db *)
 let pr_hint_db db =
-  let pr_mode = prvect_with_sep spc (fun x -> if x then str"+" else str"-") in
+  let pr_mode = prvect_with_sep spc pp_hint_mode in
   let pr_modes l = 
     if List.is_empty l then mt ()
     else str" (modes " ++ prlist_with_sep pr_comma pr_mode l ++ str")"
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 29a4f4608..6f5ee8ba5 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -72,6 +72,7 @@ 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
+val pp_hint_mode : hint_mode -> Pp.std_ppcmds
 
 module Hint_db :
   sig
@@ -99,7 +100,8 @@ module Hint_db :
     val add_list : env -> evar_map -> hint_entry list -> t -> t
     val remove_one : global_reference -> t -> t
     val remove_list : global_reference list -> t -> t
-    val iter : (global_reference option -> bool array list -> full_hint list -> unit) -> t -> unit
+    val iter : (global_reference option ->
+                hint_mode array list -> full_hint list -> unit) -> t -> unit
 
     val use_dn : t -> bool
     val transparent_state : t -> transparent_state
@@ -128,7 +130,7 @@ type hints_entry =
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
-  | HintsModeEntry of global_reference * bool list      
+  | HintsModeEntry of global_reference * hint_mode list
   | HintsExternEntry of
       int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr