Vraie substitutivite de autohints

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

6 files changed, 143 insertions, 32 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c552be7d6e..4c6e5bb014 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1148,7 +1148,7 @@ let specialize_predicate tomatchs deps cs = function
       let pred'' = subst_predicate (argsi, copti) pred' in
       (* We adjust pred st: gamma, x1..xn, x1..xn |- pred'' *)
       let pred''' = liftn_predicate n (n+1) pred'' in
-      (* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred'''*)
+      (* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred''' *)
       snd (List.fold_right2 (expand_arg n) tomatchs deps (n,pred'''))
 
 
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index bde1f31bd3..6d79b9d28d 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -49,6 +49,57 @@ let rec occur_meta_pattern = function
   | PMeta _ | PSoApp _ -> true
   | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
 
+let rec subst_pattern subst pat = match pat with
+  | PRef ref ->
+      let ref' = subst_global subst ref in
+	if ref' == ref then pat else 
+	  PRef ref'
+  | PVar _ 
+  | PEvar _
+  | PRel _ -> pat
+  | PApp (f,args) ->
+      let f' = subst_pattern subst f in 
+      let args' = array_smartmap (subst_pattern subst) args in
+	if f' == f && args' == args then pat else
+	  PApp (f',args')
+  | PSoApp (i,args) ->
+      let args' = list_smartmap (subst_pattern subst) args in
+	if args' == args then pat else
+	  PSoApp (i,args')
+  | PLambda (name,c1,c2) ->
+      let c1' = subst_pattern subst c1 in
+      let c2' = subst_pattern subst c2 in
+	if c1' == c1 && c2' == c2 then pat else
+	  PLambda (name,c1',c2')
+  | PProd (name,c1,c2) ->
+      let c1' = subst_pattern subst c1 in
+      let c2' = subst_pattern subst c2 in
+	if c1' == c1 && c2' == c2 then pat else
+	  PProd (name,c1',c2')
+  | PLetIn (name,c1,c2) ->
+      let c1' = subst_pattern subst c1 in
+      let c2' = subst_pattern subst c2 in
+	if c1' == c1 && c2' == c2 then pat else
+	  PLetIn (name,c1',c2')
+  | PSort _ 
+  | PMeta _ -> pat
+  | PCase (typ, c, branches) -> 
+      let typ' = option_smartmap (subst_pattern subst) typ in 
+      let c' = subst_pattern subst c in
+      let branches' = array_smartmap (subst_pattern subst) branches in
+	if typ' == typ && c' == c && branches' == branches then pat else
+	  PCase(typ', c', branches') 
+  | PFix fixpoint ->
+      let cstr = mkFix fixpoint in
+      let fixpoint' = destFix (subst_mps subst cstr) in
+	if fixpoint' == fixpoint then pat else
+	  PFix fixpoint'
+  | PCoFix cofixpoint ->
+      let cstr = mkCoFix cofixpoint in
+      let cofixpoint' = destCoFix (subst_mps subst cstr) in
+	if cofixpoint' == cofixpoint then pat else
+	  PCoFix cofixpoint'
+
 type constr_label =
   | ConstNode of constant
   | IndNode of inductive
@@ -63,6 +114,19 @@ let label_of_ref = function
   | ConstructRef sp -> CstrNode sp
   | VarRef id       -> VarNode id
 
+let ref_of_label = function
+  | ConstNode sp     -> ConstRef sp
+  | IndNode sp       -> IndRef sp
+  | CstrNode sp      -> ConstructRef sp
+  | VarNode id       -> VarRef id
+
+let subst_label subst cstl = 
+  let ref = ref_of_label cstl in
+  let ref' = subst_global subst ref in
+    if ref' == ref then cstl else
+      label_of_ref ref'
+      
+  
 let rec head_pattern_bound t =
   match t with
     | PProd (_,_,b)  -> head_pattern_bound b 
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 5ff667f90b..943a8d8c3d 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -35,6 +35,8 @@ type constr_pattern =
 
 val occur_meta_pattern : constr_pattern -> bool
 
+val subst_pattern : substitution -> constr_pattern -> constr_pattern
+
 type constr_label =
   | ConstNode of constant
   | IndNode of inductive
@@ -43,6 +45,8 @@ type constr_label =
 
 val label_of_ref : global_reference -> constr_label
 
+val subst_label : substitution -> constr_label -> constr_label
+
 exception BoundPattern
 
 (* [head_pattern_bound t] extracts the head variable/constant of the
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 44c5aafb08..1a527cbeaa 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -377,6 +377,20 @@ let mk_clenv_from_n wc n (c,cty) =
 
 let mk_clenv_from wc = mk_clenv_from_n wc None
 
+let map_fl f cfl = { cfl with rebus=f cfl.rebus }
+
+let map_clb f = function
+  | Cltyp cfl -> Cltyp (map_fl f cfl)
+  | Clval (cfl1,cfl2) -> Clval (map_fl f cfl1,map_fl f cfl2)
+
+let subst_clenv f sub clenv = 
+  { templval = map_fl (subst_mps sub) clenv.templval;
+    templtyp = map_fl (subst_mps sub) clenv.templtyp;
+    namenv = clenv.namenv;
+    env = Intmap.map (map_clb (subst_mps sub)) clenv.env;
+    hook = f sub clenv.hook }
+
+
 let connect_clenv wc clenv =
   { templval = clenv.templval;
     templtyp = clenv.templtyp;
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 54334c45a0..efd8dc302c 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -67,6 +67,9 @@ val mk_clenv_rename_from_n : wc -> int option -> constr * constr -> wc clausenv
 val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv
 val mk_clenv_type_of : wc -> constr -> wc clausenv
 
+val subst_clenv : (substitution -> 'a -> 'a) -> 
+  substitution -> 'a clausenv -> 'a clausenv
+
 val connect_clenv : wc -> 'a clausenv -> wc clausenv
 val clenv_change_head : constr * constr -> 'a clausenv -> 'a clausenv
 val clenv_assign : int -> constr -> 'a clausenv -> 'a clausenv
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4f8c81c704..ade0b02212 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -266,8 +266,6 @@ open Vernacexpr
 (*               declaration of the AUTOHINT library object               *)
 (**************************************************************************)
 
-let eager = Lazy.lazy_from_val
-
 (* If the database does not exist, it is created *)
 (* TODO: should a warning be printed in this case ?? *)
 let add_hint dbname hintlist = 
@@ -279,11 +277,9 @@ let add_hint dbname hintlist =
     let db = Hint_db.add_list hintlist Hint_db.empty in
     searchtable_add (dbname,db)
 
-let cache_autohint (_,(name,l_hintlist)) =
-  try add_hint name (Lazy.force l_hintlist) with _ -> anomaly "Auto.add_hint"
+let cache_autohint (_,(name,hintlist)) = add_hint name hintlist
 
-let subst_autohint (_,subst,((name,l_hintlist) as obj)) = 
-  let recalc_hints hintlist =
+(*  let recalc_hints hintlist =
     let env = Global.env() and sigma = Evd.empty in
     let recalc_hint ((_,data) as hint) =
       match data.code with
@@ -313,19 +309,52 @@ let subst_autohint (_,subst,((name,l_hintlist) as obj)) =
 	    anomaly "Extern hints cannot be substituted!!!"
     in
       list_smartmap recalc_hint hintlist
+*)
+
+let subst_autohint (_,subst,(name,hintlist as obj)) = 
+  let trans_clenv clenv = Clenv.subst_clenv (fun _ a -> a) subst clenv in
+  let trans_data data code = 	      
+    { data with
+	pat = option_smartmap (subst_pattern subst) data.pat ;
+	code = code ;
+    }
   in
-  let hintlist = Lazy.force l_hintlist in
-    try
-      let hintlist' = recalc_hints hintlist in
-	if hintlist'==hintlist then
-	  obj
-	else
-	  (name,eager hintlist')
-    with
-	_ -> (name,lazy (recalc_hints hintlist))
-
-let classify_autohint (_,((name,l_hintlist) as obj)) =
-  match Lazy.force l_hintlist with
+  let subst_hint (lab,data as hint) =
+    let lab' = subst_label subst lab in
+    let data' = match data.code with
+      | Res_pf (c, clenv) ->
+	  let c' = Term.subst_mps subst c in
+	    if c==c' then data else
+	      trans_data data (Res_pf (c', trans_clenv clenv))
+      | ERes_pf (c, clenv) ->
+	  let c' = Term.subst_mps subst c in
+	    if c==c' then data else
+	      trans_data data (ERes_pf (c', trans_clenv clenv))
+      | Give_exact c ->
+	  let c' = Term.subst_mps subst c in
+	    if c==c' then data else
+	      trans_data data (Give_exact c')
+      | Res_pf_THEN_trivial_fail (c, clenv) ->
+	  let c' = Term.subst_mps subst c in
+	    if c==c' then data else
+	      let code' = Res_pf_THEN_trivial_fail (c', trans_clenv clenv) in
+		trans_data data code'
+      | Unfold_nth ref -> 
+	  let ref' = subst_global subst ref in
+	    if ref==ref' then data else
+	      trans_data data (Unfold_nth ref')
+      | Extern _ ->
+	  anomaly "Extern hints cannot be substituted!!!"
+    in
+      if lab' == lab && data' == data then hint else
+	(lab',data')
+  in
+  let hintlist' = list_smartmap subst_hint hintlist in
+    if hintlist' == hintlist then obj else
+      (name,hintlist')
+
+let classify_autohint (_,((name,hintlist) as obj)) =
+  match hintlist with
       [] -> Dispose   
     | (_,{code=Extern _})::_ -> Keep obj (* TODO! should be changed *)
     | _ -> Substitute obj
@@ -350,16 +379,13 @@ let add_resolves env sigma clist dbnames =
        Lib.add_anonymous_leaf
 	 (inAutoHint
 	    (dbname,
-	     let l =
-     	       List.flatten
-		 (List.map
-		    (fun (name,c) -> 
-		       let ty = type_of env sigma c in
-		       let verbose = Options.is_verbose() in
-			 make_resolves env sigma name (true,verbose) (c,ty)) clist
-		 )
-	     in
-	       eager l
+     	     List.flatten
+	       (List.map
+		  (fun (name,c) -> 
+		     let ty = type_of env sigma c in
+		     let verbose = Options.is_verbose() in
+		       make_resolves env sigma name (true,verbose) (c,ty)) clist
+	       )
 	    )))
     dbnames
 
@@ -367,7 +393,7 @@ let add_resolves env sigma clist dbnames =
 let add_unfolds l dbnames =
   List.iter 
     (fun dbname -> Lib.add_anonymous_leaf 
-       (inAutoHint (dbname, eager (List.map make_unfold l))))
+       (inAutoHint (dbname, List.map make_unfold l)))
     dbnames
 
 
@@ -384,7 +410,7 @@ let add_extern name pri (patmetas,pat) tacast dbname =
 	  (str "The meta-variable ?" ++ int i ++ str" is not bound")
     | []  ->
 	Lib.add_anonymous_leaf
-	  (inAutoHint(dbname, eager [make_extern name pri pat tacast]))
+	  (inAutoHint(dbname, [make_extern name pri pat tacast]))
 
 let add_externs name pri pat tacast dbnames = 
   List.iter (add_extern name pri pat tacast) dbnames
@@ -394,7 +420,7 @@ let add_trivials env sigma l dbnames =
   List.iter
     (fun dbname ->
        Lib.add_anonymous_leaf (
-	 inAutoHint(dbname, eager (List.map (make_trivial env sigma) l))))
+	 inAutoHint(dbname, List.map (make_trivial env sigma) l)))
     dbnames