Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13179 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 191 insertions, 71 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index cf788f36d9..1f944587ea 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -605,6 +605,13 @@ let extract_all_conv_pbs evd =
 let evar_merge evd evars =
   { evd with evars = EvarMap.merge evd.evars evars.evars }
 
+let evar_list evd c =
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (evk, _ as ev) when mem evd evk -> ev :: acc
+    | _ -> fold_constr evrec acc c in
+  evrec [] c
+
 (**********************************************************)
 (* Sort variables *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 24d865beb7..be01561a16 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -195,6 +195,8 @@ val evar_source : existential_key -> evar_map -> hole_kind located
    [evar_merge evd ev1] extends the evars of [evd] with [evd1] *)
 val evar_merge : evar_map -> evar_map -> evar_map
 
+val evar_list : evar_map -> constr -> existential list
+
 (** Unification constraints *)
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * constr * constr
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 784e6b6e0f..fb6bf8545c 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -95,37 +95,55 @@ let cases_predicate_names tml =
     | (tm,(na,None)) -> [na]
     | (tm,(na,Some (_,_,_,nal))) -> na::nal) tml)
 
-(*i - if PRec (_, names, arities, bodies) is in env then arities are
-   typed in env too and bodies are typed in env enriched by the
-   arities incrementally lifted
-
-  [On pourrait plutot mettre les arités aves le type qu'elles auront
-   dans le contexte servant à typer les body ???]
-
-   - boolean in POldCase means it is recursive
-i*)
-let map_rawdecl f (na,k,obd,ty) = (na,k,Option.map f obd,f ty)
-
-let map_rawconstr f = function
-  | RVar (loc,id) -> RVar (loc,id)
-  | RApp (loc,g,args) -> RApp (loc,f g, List.map f args)
-  | RLambda (loc,na,bk,ty,c) -> RLambda (loc,na,bk,f ty,f c)
-  | RProd (loc,na,bk,ty,c) -> RProd (loc,na,bk,f ty,f c)
-  | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
+let map_rawdecl_left_to_right f (na,k,obd,ty) = 
+  let comp1 = Option.map f obd in
+  let comp2 = f ty in
+  (na,k,comp1,comp2)
+
+let map_rawconstr_left_to_right f = function
+  | RApp (loc,g,args) -> 
+      let comp1 = f g in 
+      let comp2 = Util.list_map_left f args in 
+      RApp (loc,comp1,comp2)
+  | RLambda (loc,na,bk,ty,c) -> 
+      let comp1 = f ty in 
+      let comp2 = f c in 
+      RLambda (loc,na,bk,comp1,comp2)
+  | RProd (loc,na,bk,ty,c) -> 
+      let comp1 = f ty in 
+      let comp2 = f c in 
+      RProd (loc,na,bk,comp1,comp2)
+  | RLetIn (loc,na,b,c) -> 
+      let comp1 = f b in 
+      let comp2 = f c in 
+      RLetIn (loc,na,comp1,comp2)
   | RCases (loc,sty,rtntypopt,tml,pl) ->
-      RCases (loc,sty,Option.map f rtntypopt,
-        List.map (fun (tm,x) -> (f tm,x)) tml,
-        List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl)
+      let comp1 = Option.map f rtntypopt in 
+      let comp2 = Util.list_map_left (fun (tm,x) -> (f tm,x)) tml in
+      let comp3 = Util.list_map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in
+      RCases (loc,sty,comp1,comp2,comp3)
   | RLetTuple (loc,nal,(na,po),b,c) ->
-      RLetTuple (loc,nal,(na,Option.map f po),f b,f c)
+      let comp1 = Option.map f po in
+      let comp2 = f b in
+      let comp3 = f c in 
+      RLetTuple (loc,nal,(na,comp1),comp2,comp3)
   | RIf (loc,c,(na,po),b1,b2) ->
-      RIf (loc,f c,(na,Option.map f po),f b1,f b2)
+      let comp1 = Option.map f po in
+      let comp2 = f b1 in
+      let comp3 = f b2 in
+      RIf (loc,f c,(na,comp1),comp2,comp3)
   | RRec (loc,fk,idl,bl,tyl,bv) ->
-      RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl,
-            Array.map f tyl,Array.map f bv)
-  | RCast (loc,c,k) -> RCast (loc,f c, match k with CastConv (k,t) -> CastConv (k, f t) | x -> x)
-  | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
-
+      let comp1 = Array.map (Util.list_map_left (map_rawdecl_left_to_right f)) bl in
+      let comp2 = Array.map f tyl in
+      let comp3 = Array.map f bv in
+      RRec (loc,fk,idl,comp1,comp2,comp3)
+  | RCast (loc,c,k) -> 
+      let comp1 = f c in
+      let comp2 = match k with CastConv (k,t) -> CastConv (k, f t) | x -> x in
+      RCast (loc,comp1,comp2)
+  | (RVar _ | RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
+
+let map_rawconstr = map_rawconstr_left_to_right
 
 (*
 let name_app f e = function
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index d7f8311c79..2498af7b53 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -93,19 +93,12 @@ and cases_clauses = cases_clause list
 
 val cases_predicate_names : tomatch_tuples -> name list
 
-(* - if PRec (_, names, arities, bodies) is in env then arities are
-   typed in env too and bodies are typed in env enriched by the
-   arities incrementally lifted
-
-  [On pourrait plutot mettre les arités aves le type qu'elles auront
-   dans le contexte servant à typer les body ???]
-
-   - boolean in POldCase means it is recursive
-   - option in PHole tell if the "?" was apparent or has been implicitely added
-*)
-
 val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr
 
+(* Ensure traversal from left to right *)
+val map_rawconstr_left_to_right :
+  (rawconstr -> rawconstr) -> rawconstr -> rawconstr
+
 (*
 val map_rawconstr_with_binders_loc : loc ->
   (identifier -> 'a -> identifier * 'a) ->
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 93952a4318..5799f828c8 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -935,6 +935,12 @@ let rec mem_named_context id = function
   | _ :: sign -> mem_named_context id sign
   | [] -> false
 
+let clear_named_body id env =
+  let rec aux _ = function
+  | (id',Some c,t) when id = id' -> push_named (id,None,t)
+  | d -> push_named d in
+  fold_named_context aux env ~init:(reset_context env)
+
 let global_vars env ids = Idset.elements (global_vars_set env ids)
 
 let global_vars_set_of_decl env = function
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index fc227b5fb2..24e605ef4d 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -231,6 +231,8 @@ val fold_named_context_both_sides :
     named_context -> init:'a -> 'a
 val mem_named_context : identifier -> named_context -> bool
 
+val clear_named_body : identifier -> env -> env
+
 val global_vars : env -> constr -> identifier list
 val global_vars_set_of_decl : env -> named_declaration -> Idset.t
 
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index b8552a5aae..8e37c81666 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -19,14 +19,6 @@ open Termops
 
 (* The instantiate tactic *)
 
-let evar_list evc c =
-  let rec evrec acc c =
-    match kind_of_term c with
-    | Evar (n, _) when Evd.mem evc n -> c :: acc
-    | _ -> fold_constr evrec acc c
-  in
-    evrec [] c
-
 let instantiate n (ist,rawc) ido gl =
   let sigma = gl.sigma in
   let evl =
@@ -49,7 +41,7 @@ let instantiate n (ist,rawc) ido gl =
     if List.length evl < n then
       error "Not enough uninstantiated existential variables.";
     if n <= 0 then error "Incorrect existential variable index.";
-    let evk,_ = destEvar (List.nth evl (n-1)) in
+    let evk,_ = List.nth evl (n-1) in
     let evi = Evd.find sigma evk in
     let ltac_vars = Tacinterp.extract_ltac_constr_values ist (Evd.evar_env evi) in
     let sigma' = w_refine (evk,evi) (ltac_vars,rawc) sigma in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a1c1da177e..3d7f77f14f 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -20,10 +20,11 @@ open Tactics
 open Util
 open Termops
 open Evd
-
-(* Equality *)
 open Equality
 
+(**********************************************************************)
+(* replace, discriminate, injection, simplify_eq                      *)
+(* cutrewrite, dependent rewrite                                      *)
 
 TACTIC EXTEND replace
    ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ]
@@ -151,7 +152,9 @@ TACTIC EXTEND cut_rewrite
     -> [ cutRewriteInHyp b eqn id ]
 END
 
-(* Contradiction *)
+(**********************************************************************)
+(* Contradiction                                                      *)
+
 open Contradiction
 
 TACTIC EXTEND absurd
@@ -167,21 +170,10 @@ TACTIC EXTEND contradiction
     [ onSomeWithHoles contradiction c ]
 END
 
-(* AutoRewrite *)
+(**********************************************************************)
+(* AutoRewrite                                                        *)
 
 open Autorewrite
-(* J.F : old version
-TACTIC EXTEND autorewrite
-  [ "autorewrite" "with" ne_preident_list(l) ] ->
-    [ autorewrite Refiner.tclIDTAC l ]
-| [ "autorewrite" "with" ne_preident_list(l) "using" tactic(t) ] ->
-    [ autorewrite (snd t) l ]
-| [ "autorewrite" "with" ne_preident_list(l) "in" hyp(id) ] ->
-    [ autorewrite_in id Refiner.tclIDTAC l ]
-| [ "autorewrite" "with" ne_preident_list(l) "in" hyp(id) "using" tactic(t) ] ->
-    [ autorewrite_in id (snd t) l ]
-END
-*)
 
 TACTIC EXTEND autorewrite
 | [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) ] ->
@@ -202,7 +194,8 @@ TACTIC EXTEND autorewrite_star
 	auto_multi_rewrite_with ~conds:AllMatches (snd t) l cl ]
 END
 
-open Extraargs
+(**********************************************************************)
+(* Rewrite star                                                       *)
 
 let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) =
   let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in
@@ -229,6 +222,9 @@ TACTIC EXTEND rewrite_star
     [ rewrite_star None o all_occurrences c tac ]
     END
 
+(**********************************************************************)
+(* Hint Rewrite                                                       *)
+
 let add_rewrite_hint name ort t lcsr =
   let env = Global.env() and sigma = Evd.empty in
   let f c = Topconstr.constr_loc c, Constrintern.interp_constr sigma env c, ort, t in
@@ -246,6 +242,9 @@ VERNAC COMMAND EXTEND HintRewrite
   [ add_rewrite_hint "core" o t l ]
 END
 
+(**********************************************************************)
+(* Hint Resolve                                                       *)
+
 open Term
 open Coqlib
 
@@ -285,8 +284,8 @@ VERNAC COMMAND EXTEND HintResolveIffRL
   [ add_hints_iff false lc n ["core"] ]
 END
 
-
-(* Refine *)
+(**********************************************************************)
+(* Refine                                                             *)
 
 open Refine
 
@@ -296,7 +295,8 @@ END
 
 let refine_tac = h_refine
 
-(* Inversion lemmas (Leminv) *)
+(**********************************************************************)
+(* Inversion lemmas (Leminv)                                          *)
 
 open Inv
 open Leminv
@@ -342,7 +342,8 @@ VERNAC COMMAND EXTEND DeriveDependentInversionClear
   -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ]
 END
 
-(* Subst *)
+(**********************************************************************)
+(* Subst                                                              *)
 
 TACTIC EXTEND subst
 | [ "subst" ne_var_list(l) ] -> [ subst l ]
@@ -358,7 +359,8 @@ END
 
 open Evar_tactics
 
-(* evar creation *)
+(**********************************************************************)
+(* Evar creation                                                      *)
 
 TACTIC EXTEND evar
   [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
@@ -375,7 +377,8 @@ TACTIC EXTEND instantiate
 END
 
 
-(** Nijmegen "step" tactic for setoid rewriting *)
+(**********************************************************************)
+(** Nijmegen "step" tactic for setoid rewriting                       *)
 
 open Tactics
 open Tactics
@@ -477,7 +480,8 @@ END
 
 
 
-(*spiwack : Vernac commands for retroknowledge *)
+(**********************************************************************)
+(*spiwack : Vernac commands for retroknowledge                        *)
 
 VERNAC COMMAND EXTEND RetroknowledgeRegister
  | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
@@ -488,6 +492,7 @@ END
 
 
 
+(**********************************************************************)
 (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
   defined by Conor McBride *)
 TACTIC EXTEND generalize_eqs
@@ -510,3 +515,98 @@ END
 TACTIC EXTEND specialize_eqs
 [ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ]
 END
+
+(**********************************************************************)
+(* A tactic that considers a given occurrence of [c] in [t] and       *)
+(* abstract the minimal set of all the occurrences of [c] so that the *)
+(* abstraction [fun x -> t[x/c]] is well-typed                        *)
+(*                                                                    *)
+(* Contributed by Chung-Kil Hur (Winter 2009)                         *)
+(**********************************************************************)
+
+let subst_var_with_hole occ tid t = 
+  let occref = if occ > 0 then ref occ else error_invalid_occurrence [occ] in
+  let locref = ref 0 in
+  let rec substrec = function
+    | RVar (_,id) as x -> 
+        if id = tid 
+        then (decr occref; if !occref = 0 then x
+                           else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true))))
+        else x
+    | c -> map_rawconstr_left_to_right substrec c in
+  let t' = substrec t
+  in
+  if !occref > 0 then error_invalid_occurrence [occ] else t'
+
+let subst_hole_with_term occ tc t =
+  let locref = ref 0 in
+  let occref = ref occ in
+  let rec substrec = function
+    | RHole (_,Evd.QuestionMark(Evd.Define true)) -> 
+        decr occref; if !occref = 0 then tc
+                     else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true)))
+    | c -> map_rawconstr_left_to_right substrec c
+  in
+  substrec t
+
+open Tacmach
+
+let out_arg = function
+  | ArgVar _ -> anomaly "Unevaluated or_var variable"
+  | ArgArg x -> x
+
+let hResolve id c occ t gl = 
+  let sigma = project gl in 
+  let env = clear_named_body id (pf_env gl) in
+  let env_ids = ids_of_context env in
+  let env_names = names_of_rel_context env in
+  let c_raw = Detyping.detype true env_ids env_names c in 
+  let t_raw = Detyping.detype true env_ids env_names t in 
+  let rec resolve_hole t_hole =
+    try 
+      Pretyping.Default.understand sigma env t_hole
+    with 
+    | Ploc.Exc (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> 
+        resolve_hole (subst_hole_with_term (Ploc.line_nb loc) c_raw t_hole)
+  in
+  let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
+  let t_constr_type = Retyping.get_type_of env sigma t_constr in
+  change_in_concl None (mkLetIn (Anonymous,t_constr,t_constr_type,pf_concl gl)) gl
+
+let hResolve_auto id c t gl =
+  let rec resolve_auto n = 
+    try
+      hResolve id c n t gl
+    with
+    | UserError _ as e -> raise e
+    | _ -> resolve_auto (n+1)
+  in
+  resolve_auto 1
+
+TACTIC EXTEND hresolve_core
+| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> [ hResolve id c (out_arg occ) t ]
+| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> [ hResolve_auto id c t ]
+END
+
+(**
+   hget_evar
+*)
+
+open Evar_refiner
+open Sign
+
+let hget_evar n gl =
+  let sigma = project gl in
+  let evl = evar_list sigma (pf_concl gl) in
+  if List.length evl < n then
+    error "Not enough uninstantiated existential variables.";
+  if n <= 0 then error "Incorrect existential variable index.";
+  let ev = List.nth evl (n-1) in
+  let ev_type = existential_type sigma ev in
+  change_in_concl None (mkLetIn (Anonymous,mkEvar ev,ev_type,pf_concl gl)) gl
+
+TACTIC EXTEND hget_evar
+| [ "hget_evar" int_or_var(n) ] -> [ hget_evar (out_arg n) ]
+END
+
+(**********************************************************************)