+ timide essai pour le traitement des as dans les patterns lors de la generation des graphes de Function

+ Correction d'un petit bug dans les lemmes d'inversions de Function
+ Nettoyage d'hypotheses inutile dans les obligations de preuve de Function (wf et measure). 



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

5 files changed, 73 insertions, 20 deletions

diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 74db6a54b..a4c379bae 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -424,11 +424,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       let params_bindings,avoid =
 	List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
-	     let id = (* Termops.next_global_ident_away false (Nameops.out_name x) avoid *) 
-	       Nameops.next_ident_away (Nameops.out_name x) avoid in
+	     let id = Nameops.next_ident_away (Nameops.out_name x) avoid in
 	     (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid
 	  )
-	  ([],[])
+	  ([],pf_ids_of_hyps g)
 	  princ_infos.params
 	  (List.rev params)
       in
@@ -436,7 +435,6 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
 	     let id = Nameops.next_ident_away (Nameops.out_name x) avoid in 
-(* Termops.next_global_ident_away false (Nameops.out_name x) avoid in *)
 	     (dummy_loc,Rawterm.NamedHyp id,nf_zeta p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 1b5ed99f5..d58dfba33 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -789,7 +789,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	    avoid
 	    matched_expr
 	in
-	(* We know create the precondition of this branch i.e.
+	(* We now create the precondition of this branch i.e.
 
 	   1- the list of variable appearing in the different patterns of this branch and 
 	      the list of equation stating than el = patl (List.flatten ...)
@@ -1085,7 +1085,7 @@ let build_inductive
   let funsargs = Array.of_list funsargs in 
   let returned_types = Array.of_list returned_types in
   (* alpha_renaming of the body to prevent variable capture during manipulation *)
-  let rtl_alpha = List.map (function rt ->  (alpha_rt [] rt) ) rtl in
+  let rtl_alpha = List.map (function rt ->  expand_as (alpha_rt [] rt)) rtl in
   let rta = Array.of_list rtl_alpha in
   (*i The next call to mk_rel_id is valid since we are constructing the graph
     Ensures by: obvious
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index 14805cf49..a0655d858 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -321,14 +321,6 @@ let rec alpha_rt excluded rt =
 	     List.map (alpha_rt excluded) args
 	    )
   in 
-  if Indfun_common.do_observe ()  && false 
-  then
-    Pp.msgnl (str "debug: alpha_rt(" ++ str "[" ++
-	      prlist_with_sep (fun _ -> str";") Ppconstr.pr_id excluded ++
-	      str "]" ++ spc () ++ str "," ++ spc () ++
-	      Printer.pr_rawconstr rt ++ spc () ++ str ")" ++ spc () ++ str "=" ++
-	      spc () ++ Printer.pr_rawconstr new_rt
-	   );
   new_rt
 
 and alpha_br excluded (loc,ids,patl,res) = 
@@ -339,12 +331,6 @@ and alpha_br excluded (loc,ids,patl,res) =
   let new_res = alpha_rt new_excluded renamed_res in 
   (loc,new_ids,new_patl,new_res)
     
-
-
-
-
-
-
 (* 
    [is_free_in id rt] checks if [id] is a free variable in [rt]
 *)
@@ -601,3 +587,46 @@ let zeta_normalize =
     (loc,idl,patl,zeta_normalize_term res)
   in
   zeta_normalize_term 
+
+
+
+
+let expand_as = 
+  
+  let rec add_as map pat = 
+    match pat with 
+      | PatVar _ -> map 
+      | PatCstr(_,_,patl,Name id) -> 
+	  Idmap.add id (pattern_to_term pat) (List.fold_left add_as map patl)
+      | PatCstr(_,_,patl,_) -> List.fold_left add_as map patl
+  in 
+  let rec expand_as map rt = 
+    match rt with 
+      | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> rt 
+      | RVar(_,id) -> 
+	  begin
+	    try 
+	      Idmap.find id map
+	    with Not_found -> rt 
+	  end
+      | RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args)
+      | RLambda(loc,na,t,b) -> RLambda(loc,na,expand_as map t, expand_as map b)
+      | RProd(loc,na,t,b) -> RProd(loc,na,expand_as map t, expand_as map b)
+      | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b)
+      | RLetTuple(loc,nal,(na,po),v,b) ->
+	  RLetTuple(loc,nal,(na,option_map (expand_as map) po),
+		    expand_as map v, expand_as map b)
+      | RIf(loc,e,(na,po),br1,br2) ->
+	  RIf(loc,expand_as map e,(na,option_map (expand_as map) po),
+	      expand_as map br1, expand_as map br2)
+      | RRec _ ->  error "Not handled RRec"
+      | RDynamic _ -> error "Not handled RDynamic"
+      | RCast(loc,b,kind,t) -> RCast(loc,expand_as map b,kind,expand_as map t)
+      | RCases(loc,po,el,brl) ->
+	  RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
+		List.map (expand_as_br map) brl)
+	    
+  and expand_as_br map (loc,idl,cpl,rt) = 
+    (loc,idl,cpl,    expand_as (List.fold_left add_as map cpl) rt)
+  in
+  expand_as Idmap.empty 
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index aa3554850..7cf7a0eb2 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -112,3 +112,6 @@ val   ids_of_pat : cases_pattern -> Names.Idset.t
    removing let_in construction in a rawterm 
 *)
 val zeta_normalize : Rawterm.rawconstr -> Rawterm.rawconstr
+
+
+val expand_as : rawconstr -> rawconstr
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 93db0eab2..16067e6f3 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -745,8 +745,31 @@ let build_and_l l =
 	  ],nb+1
   in f l
 
+
+let is_rec_res id = 
+  let rec_res_name = string_of_id rec_res_id   in 
+  let id_name = string_of_id id in 
+  try 
+    String.sub id_name 0 (String.length rec_res_name) = rec_res_name 
+  with _ -> false
+
+let clear_goals = 
+  let rec clear_goal t = 
+    match kind_of_term t with 
+      | Prod(Name id as na,t,b) -> 
+	  let b' = clear_goal b in 
+	  if noccurn 1 b' && (is_rec_res id) 
+	  then pop b' 
+	  else if b' == b then t 
+	  else mkProd(na,t,b')
+      | _ -> map_constr clear_goal t
+  in 
+  List.map clear_goal 
+
+
 let build_new_goal_type () = 
   let sub_gls_types = get_current_subgoals_types () in 
+  let sub_gls_types = clear_goals sub_gls_types in 
   let res = build_and_l sub_gls_types in 
   res