1 files changed, 191 insertions, 44 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index db2524c30..e15c30a3b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -54,10 +54,22 @@ type 'a auto_tactic =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of glob_tactic_expr       (* Hint Extern *)
 
+type hints_path_atom = 
+  | PathHints of global_reference list
+  | PathAny
+
+type hints_path =
+  | PathAtom of hints_path_atom
+  | PathStar of hints_path
+  | PathSeq of hints_path * hints_path
+  | PathOr of hints_path * hints_path
+  | PathEmpty
+  | PathEpsilon
+
 type 'a gen_auto_tactic = {
   pri  : int;            (* A number lower is higher priority *)
   pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
-  name  : global_reference option; (* A potential name to refer to the hint *)
+  name  : hints_path_atom; (* A potential name to refer to the hint *) 
   code : 'a auto_tactic     (* the tactic to apply when the concl matches pat *)
 }
 
@@ -80,18 +92,18 @@ let insert v l =
   insrec l
 
 (* Nov 98 -- Papageno *)
-(* Les Hints sont ré-organisés en plusieurs databases.
+(* Les Hints sont ré-organisés en plusieurs databases.
 
-  La table impérative "searchtable", de type "hint_db_table",
-   associe une database (hint_db) à chaque nom.
+  La table impérative "searchtable", de type "hint_db_table",
+   associe une database (hint_db) à chaque nom.
 
   Une hint_db est une table d'association fonctionelle constr -> search_entry
-  Le constr correspond à la constante de tête de la conclusion.
+  Le constr correspond à la constante de tête de la conclusion.
 
   Une search_entry est un triplet comprenant :
-     - la liste des tactiques qui n'ont pas de pattern associé
+     - la liste des tactiques qui n'ont pas de pattern associé
      - la liste des tactiques qui ont un pattern
-     - un discrimination net borné (Btermdn.t) constitué de tous les
+     - un discrimination net borné (Btermdn.t) constitué de tous les
        patterns de la seconde liste de tactiques *)
 
 type stored_data = int * pri_auto_tactic
@@ -137,7 +149,9 @@ let eq_pri_auto_tactic (_, x) (_, y) =
 let add_tac pat t st (l,l',dn) =
   match pat with
   | None -> if not (List.exists (eq_pri_auto_tactic t) l) then (insert t l, l', dn) else (l, l', dn)
-  | Some pat -> if not (List.exists (eq_pri_auto_tactic t) l') then (l, insert t l', Bounded_net.add st dn (pat,t)) else (l, l', dn)
+  | Some pat -> 
+    if not (List.exists (eq_pri_auto_tactic t) l') 
+    then (l, insert t l', Bounded_net.add st dn (pat,t)) else (l, l', dn)
 
 let rebuild_dn st ((l,l',dn) : search_entry) =
   (l, l', List.fold_left (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
@@ -173,10 +187,119 @@ let translate_hint (go,p) =
   in
   (go,{ p with code = code })
 
+let path_matches hp hints =
+  let rec aux hp hints k =
+    match hp, hints with
+    | PathAtom _, [] -> false
+    | PathAtom PathAny, (_ :: hints') -> k hints'
+    | PathAtom p, (h :: hints') -> 
+      if p = h then k hints' else false
+    | PathStar hp', hints -> 
+      k hints || aux hp' hints (fun hints' -> aux hp hints' k)
+    | PathSeq (hp, hp'), hints -> 
+      aux hp hints (fun hints' -> aux hp' hints' k)
+    | PathOr (hp, hp'), hints ->
+      aux hp hints k || aux hp' hints k
+    | PathEmpty, _ -> false
+    | PathEpsilon, hints -> k hints
+  in aux hp hints (fun hints' -> true)
+
+let rec matches_epsilon = function
+  | PathAtom _ -> false
+  | PathStar _ -> true
+  | PathSeq (p, p') -> matches_epsilon p && matches_epsilon p'
+  | PathOr (p, p') -> matches_epsilon p || matches_epsilon p'
+  | PathEmpty -> false
+  | PathEpsilon -> true
+
+let rec is_empty = function
+  | PathAtom _ -> false
+  | PathStar _ -> false
+  | PathSeq (p, p') -> is_empty p || is_empty p'
+  | PathOr (p, p') -> matches_epsilon p && matches_epsilon p'
+  | PathEmpty -> true
+  | PathEpsilon -> false
+
+let rec path_derivate hp hint =
+  let rec derivate_atoms hints hints' =
+    match hints, hints' with
+    | gr :: grs, gr' :: grs' when gr = gr' -> derivate_atoms grs grs'
+    | [], [] -> PathEpsilon
+    | [], hints -> PathEmpty
+    | grs, [] -> PathAtom (PathHints grs)
+    | _, _ -> PathEmpty 
+  in
+    match hp with
+    | PathAtom PathAny -> PathEpsilon
+    | PathAtom (PathHints grs) -> 
+      (match grs, hint with
+       | h :: hints, PathAny -> PathEmpty
+       | hints, PathHints hints' -> derivate_atoms hints hints'
+       | _, _ -> assert false)
+    | PathStar p -> if path_matches p [hint] then hp else PathEpsilon
+    | PathSeq (hp, hp') ->
+      let hpder = path_derivate hp hint in
+	if matches_epsilon hp then 
+	  PathOr (PathSeq (hpder, hp'), path_derivate hp' hint)
+	else if is_empty hpder then PathEmpty 
+	else PathSeq (hpder, hp')
+    | PathOr (hp, hp') ->
+      PathOr (path_derivate hp hint, path_derivate hp' hint)
+    | PathEmpty -> PathEmpty
+    | PathEpsilon -> PathEmpty
+
+let rec normalize_path h =
+  match h with
+  | PathStar PathEpsilon -> PathEpsilon
+  | PathSeq (PathEmpty, _) | PathSeq (_, PathEmpty) -> PathEmpty
+  | PathSeq (PathEpsilon, p) | PathSeq (p, PathEpsilon) -> normalize_path p
+  | PathOr (PathEmpty, p) | PathOr (p, PathEmpty) -> normalize_path p
+  | PathOr (p, q) -> 
+    let p', q' = normalize_path p, normalize_path q in
+      if p = p' && q = q' then h
+      else normalize_path (PathOr (p', q'))
+  | PathSeq (p, q) -> 
+    let p', q' = normalize_path p, normalize_path q in
+      if p = p' && q = q' then h
+      else normalize_path (PathSeq (p', q'))
+  | _ -> h
+
+let path_derivate hp hint = normalize_path (path_derivate hp hint)
+
+let rec pp_hints_path = function
+  | PathAtom (PathAny) -> str"."
+  | PathAtom (PathHints grs) -> prlist_with_sep pr_spc pr_global grs
+  | 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"ε"
+
+let rec subst_hints_path subst hp =
+  match hp with
+  | PathAtom PathAny -> hp
+  | PathAtom (PathHints grs) -> 
+    let gr' gr = fst (subst_global subst gr) in
+    let grs' = list_smartmap gr' grs in
+      if grs' == grs then hp else PathAtom (PathHints grs')
+  | PathStar p -> let p' = subst_hints_path subst p in
+      if p' == p then hp else PathStar p'
+  | PathSeq (p, q) ->
+    let p' = subst_hints_path subst p in
+    let q' = subst_hints_path subst q in
+      if p' == p && q' == q then hp else PathSeq (p', q')
+  | PathOr (p, q) ->
+    let p' = subst_hints_path subst p in
+    let q' = subst_hints_path subst q in
+      if p' == p && q' == q then hp else PathOr (p', q')
+  | _ -> hp
+
 module Hint_db = struct
 
   type t = {
     hintdb_state : Names.transparent_state;
+    hintdb_cut : hints_path;
     hintdb_unfolds : Idset.t * Cset.t;
     mutable hintdb_max_id : int;
     use_dn : bool;
@@ -190,6 +313,7 @@ module Hint_db = struct
     let h = t.hintdb_max_id in t.hintdb_max_id <- succ t.hintdb_max_id; h
 
   let empty st use_dn = { hintdb_state = st;
+			  hintdb_cut = PathEmpty;
 			  hintdb_unfolds = (Idset.empty, Cset.empty);
 			  hintdb_max_id = 0;
 			  use_dn = use_dn;
@@ -199,7 +323,7 @@ module Hint_db = struct
   let find key db =
     try Constr_map.find key db.hintdb_map
     with Not_found -> empty_se
-
+ 
   let map_none db =
     List.map snd (Sort.merge pri_order (List.map snd db.hintdb_nopat) [])
     
@@ -271,7 +395,7 @@ module Hint_db = struct
       else rebuild_dn st (sl1', sl2', dn)
 
   let remove_list grs db =
-    let filter (_, h) = match h.name with None -> true | Some gr -> not (List.mem gr grs) in
+    let filter (_, h) = match h.name with PathHints [gr] -> not (List.mem gr grs) | _ -> true in
     let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
     let hintnopat = list_smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
       { db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
@@ -279,8 +403,8 @@ module Hint_db = struct
   let remove_one gr db = remove_list [gr] db
 
   let iter f db =
-    f None (List.map snd db.hintdb_nopat);
-    Constr_map.iter (fun k (l,l',_) -> f (Some k) (l@l')) db.hintdb_map
+    f None (List.map (fun x -> snd (snd x)) db.hintdb_nopat);
+    Constr_map.iter (fun k (l,l',_) -> f (Some k) (List.map snd (l@l'))) db.hintdb_map
 
   let transparent_state db = db.hintdb_state
 
@@ -288,6 +412,11 @@ module Hint_db = struct
     if db.use_dn then rebuild_db st db
     else { db with hintdb_state = st }
 
+  let add_cut path db =
+    { db with hintdb_cut = normalize_path (PathOr (db.hintdb_cut, path)) }
+
+  let cut db = db.hintdb_cut
+
   let unfolds db = db.hintdb_unfolds
 
   let use_dn db = db.use_dn
@@ -348,7 +477,7 @@ let try_head_pattern c =
 
 let name_of_constr c = try Some (global_of_constr c) with Not_found -> None
 
-let make_exact_entry sigma pri ?name (c,cty) =
+let make_exact_entry sigma pri ?(name=PathAny) (c,cty) =
   let cty = strip_outer_cast cty in
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
@@ -364,7 +493,7 @@ let make_exact_entry sigma pri ?name (c,cty) =
 	    name = name;
 	    code = Give_exact c })
 
-let make_apply_entry env sigma (eapply,hnf,verbose) pri ?name (c,cty) =
+let make_apply_entry env sigma (eapply,hnf,verbose) pri ?(name=PathAny) (c,cty) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
     match kind_of_term cty with
     | Prod _ ->
@@ -415,7 +544,8 @@ let make_resolves env sigma flags pri ?name c =
 (* used to add an hypothesis to the local hint database *)
 let make_resolve_hyp env sigma (hname,_,htyp) =
   try
-    [make_apply_entry env sigma (true, true, false) None ~name:(VarRef hname)
+    [make_apply_entry env sigma (true, true, false) None 
+       ~name:(PathHints [VarRef hname])
        (mkVar hname, htyp)]
   with
     | Failure _ -> []
@@ -427,7 +557,7 @@ let make_unfold eref =
   (Some g,
    { pri = 4;
      pat = None;
-     name = Some g;
+     name = PathHints [g];
      code = Unfold_nth eref })
 
 let make_extern pri pat tacast =
@@ -435,10 +565,10 @@ let make_extern pri pat tacast =
   (hdconstr,
    { pri = pri;
      pat = pat;
-     name = None;
+     name = PathAny;
      code = Extern tacast })
 
-let make_trivial env sigma ?name c =
+let make_trivial env sigma ?(name=PathAny) c =
   let t = hnf_constr env sigma (type_of env sigma c) in
   let hd = head_of_constr_reference (fst (head_constr t)) in
   let ce = mk_clenv_from dummy_goal (c,t) in
@@ -476,7 +606,7 @@ let add_transparency dbname grs b =
       st grs
   in searchtable_add (dbname, Hint_db.set_transparent_state db st')
 
-let remove_hints dbname hintlist grs =
+let remove_hint dbname grs =
   let db = get_db dbname in
   let db' = Hint_db.remove_list grs db in
     searchtable_add (dbname, db')
@@ -486,6 +616,12 @@ type hint_action =
   | AddTransparency of evaluable_global_reference list * bool
   | AddHints of hint_entry list
   | RemoveHints of global_reference list
+  | AddCut of hints_path
+
+let add_cut dbname path =
+  let db = get_db dbname in
+  let db' = Hint_db.add_cut path db in
+    searchtable_add (dbname, db')
 
 type hint_obj = bool * string * hint_action  (* locality, name, action *)
 
@@ -494,7 +630,8 @@ let cache_autohint (_,(local,name,hints)) =
   | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
   | AddTransparency (grs, b) -> add_transparency name grs b
   | AddHints hints -> add_hint name hints
-  | RemoveHints grs -> remove_hints name hints grs
+  | RemoveHints grs -> remove_hint name grs
+  | AddCut path -> add_cut name path
 
 let forward_subst_tactic =
   ref (fun _ -> failwith "subst_tactic is not installed for auto")
@@ -553,7 +690,9 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
     | RemoveHints grs ->
 	let grs' = list_smartmap (fun x -> fst (subst_global subst x)) grs in
 	  if grs==grs' then obj else (local, name, RemoveHints grs')
-
+    | AddCut path ->
+      let path' = subst_hints_path subst path in
+	if path' == path then obj else (local, name, AddCut path')
 
 let classify_autohint ((local,name,hintlist) as obj) =
   if local or hintlist = (AddHints []) then Dispose else Substitute obj
@@ -563,8 +702,7 @@ let inAutoHint : hint_obj -> obj =
                     cache_function = cache_autohint;
 		    load_function = (fun _ -> cache_autohint);
 		    subst_function = subst_autohint;
-		    classify_function = classify_autohint }
-
+		    classify_function = classify_autohint; }
 
 let create_hint_db l n st b =
   Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st)))
@@ -585,17 +723,22 @@ let add_resolves env sigma clist local dbnames =
        Lib.add_anonymous_leaf
 	 (inAutoHint
 	    (local,dbname, AddHints
-     	      (List.flatten (List.map (fun (x, hnf, name, y) ->
-		make_resolves env sigma (true,hnf,Flags.is_verbose()) x ?name y) clist)))))
+     	      (List.flatten (List.map (fun (x, hnf, path, y) ->
+		make_resolves env sigma (true,hnf,Flags.is_verbose()) x ~name:path y) clist)))))
     dbnames
 
-
 let add_unfolds l local dbnames =
   List.iter
     (fun dbname -> Lib.add_anonymous_leaf
        (inAutoHint (local,dbname, AddHints (List.map make_unfold l))))
     dbnames
 
+let add_cuts l local dbnames =
+  List.iter
+    (fun dbname -> Lib.add_anonymous_leaf
+       (inAutoHint (local,dbname, AddCut l)))
+    dbnames
+
 let add_transparency l b local dbnames =
   List.iter
     (fun dbname -> Lib.add_anonymous_leaf
@@ -626,7 +769,8 @@ let add_trivials env sigma l local dbnames =
   List.iter
     (fun dbname ->
        Lib.add_anonymous_leaf (
-	 inAutoHint(local,dbname, AddHints (List.map (fun (name, c) -> make_trivial env sigma ?name c) l))))
+	 inAutoHint(local,dbname, 
+		    AddHints (List.map (fun (name, c) -> make_trivial env sigma ~name c) l))))
     dbnames
 
 let forward_intern_tac =
@@ -635,8 +779,9 @@ let forward_intern_tac =
 let set_extern_intern_tac f = forward_intern_tac := f
 
 type hints_entry =
-  | HintsResolveEntry of (int option * bool * global_reference option * constr) list
-  | HintsImmediateEntry of (global_reference option * constr) list
+  | HintsResolveEntry of (int option * bool * hints_path_atom * constr) list
+  | HintsImmediateEntry of (hints_path_atom * constr) list
+  | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsExternEntry of
@@ -677,10 +822,10 @@ let prepare_hint env (sigma,c) =
       mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
   iter c
 
-let name_of_constr_expr c =
+let path_of_constr_expr c =
   match c with
-  | Topconstr.CRef r -> (try Some (global r) with _ -> None)
-  | _ -> None 
+  | Topconstr.CRef r -> (try PathHints [global r] with _ -> PathAny)
+  | _ -> PathAny
       
 let interp_hints h =
   let f c =
@@ -693,8 +838,8 @@ let interp_hints h =
     let r' = evaluable_of_global_reference (Global.env()) gr in
     Dumpglob.add_glob (loc_of_reference r) gr;
     r' in
-  let fres (o, b, c) = (o, b, name_of_constr_expr c, f c) in
-  let fi c = name_of_constr_expr c, f c in
+  let fres (o, b, c) = (o, b, path_of_constr_expr c, f c) in
+  let fi c = path_of_constr_expr c, f c in
   let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in
   match h with
   | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
@@ -706,7 +851,7 @@ let interp_hints h =
       let constr_hints_of_ind qid =
         let ind = global_inductive_with_alias qid in
         list_tabulate (fun i -> let c = (ind,i+1) in
-			 None, true, Some (ConstructRef c), mkConstruct c)
+			 None, true, PathHints [ConstructRef c], mkConstruct c)
 	  (nconstructors ind) in
 	HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->
@@ -725,6 +870,7 @@ let add_hints local dbnames0 h =
   match h with
   | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames
   | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames
+  | HintsCutEntry lhints -> add_cuts lhints local dbnames
   | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
   | HintsTransparencyEntry (lhints, b) ->
       add_transparency lhints b local dbnames
@@ -827,17 +973,18 @@ let print_hint_db db =
 	    else str"Non-discriminated database")));
   msgnl (hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids));
   msgnl (hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts));
+  msgnl (hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)));
   Hint_db.iter
     (fun head hintlist ->
       match head with
       | Some head ->
 	  msg (hov 0
 		  (str "For " ++ pr_global head ++ str " -> " ++
-		      pr_hint_list hintlist))
+		      pr_hint_list (List.map (fun x -> (0,x)) hintlist)))
       | None ->
 	  msg (hov 0
 		  (str "For any goal -> " ++
-		      pr_hint_list hintlist)))
+		      pr_hint_list (List.map (fun x -> (0, x)) hintlist))))
     db
 
 let print_hint_db_by_name dbname =
@@ -934,16 +1081,16 @@ let make_local_hint_db ?ts eapply lems gl =
     (Hint_db.add_list hintlist (Hint_db.empty ts false)) gl
 
 (* Serait-ce possible de compiler d'abord la tactique puis de faire la
-   substitution sans passer par bdize dont l'objectif est de préparer un
+   substitution sans passer par bdize dont l'objectif est de préparer un
    terme pour l'affichage ? (HH) *)
 
-(* Si on enlève le dernier argument (gl) conclPattern est calculé une
+(* Si on enlève le dernier argument (gl) conclPattern est calculé une
 fois pour toutes : en particulier si Pattern.somatch produit une UserError
-Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même
-si après Intros la conclusion matche le pattern.
+Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même
+si après Intros la conclusion matche le pattern.
 *)
 
-(* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
+(* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
 
 let forward_interp_tactic =
   ref (fun _ -> failwith "interp_tactic is not installed for auto")
@@ -964,8 +1111,8 @@ let conclPattern concl pat tac gl =
 (**************************************************************************)
 
 (* local_db is a Hint database containing the hypotheses of current goal *)
-(* Papageno : cette fonction a été pas mal simplifiée depuis que la base
-  de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
+(* Papageno : cette fonction a été pas mal simplifiée depuis que la base
+  de Hint impérative a été remplacée par plusieurs bases fonctionnelles *)
 
 let flags_of_state st =
   {auto_unif_flags with