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

6 files changed, 66 insertions, 38 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