Correction of a bug in functional scheme. It raised with mutual

functions with imbricated recursive calls. Two bugs in one actually,
one in the building of the set of recursive functions, and one with De
Bruijn indices when looking for recursve calls.


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

2 files changed, 37 insertions, 39 deletions

diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index c2a421e7e..a0b08c805 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -157,11 +157,9 @@ let rec npatternify ltypes c =
   | [] -> c
   | (mv,nme,t)::ltypes' -> 
      let c'= substitterm 0 mv (mkRel 1) c in
-(*      let _ = prconstr c' in *)
      let tlift = lift (List.length ltypes') t in
      let res = 
       npatternify ltypes' (mkLambda (newname_append nme "", tlift, c')) in
-(*      let _ = prconstr res in *)
      res
 
 (* fait une application (c m1 m2...mn, où mi est une evar, on rend également
@@ -510,15 +508,15 @@ let rec proofPrinc mi lst_vars lst_eqs lst_recs:
   | u -> 
      let varrels = List.rev (List.map fst lst_vars) in
      let varnames = List.map snd lst_vars in
-     let nb_vars = (List.length varnames) in
-     let nb_eqs = (List.length lst_eqs) in
+     let nb_vars = List.length varnames in
+     let nb_eqs = List.length lst_eqs in
      let eqrels = List.map fst lst_eqs in
      (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs
         trouvés dans les let in et les Cases avec ceux trouves dans u (ie
         mi.mimick). *)
      (* TODO: il faudra gérer plusieurs pt fixes imbriqués ? *)
-     let terms_recs = lst_recs @ (hdMatchSub_cpl mi.mimick mi.fonc)  in
-     
+     let terms_recs = lst_recs @ hdMatchSub_cpl mi.mimick mi.fonc in
+
      (*c construction du terme: application successive des variables, des
        egalites et des appels rec, a la variable existentielle correspondant a
        l'hypothese de recurrence en cours. *)
@@ -573,7 +571,6 @@ let invfun_proof fonc def_fonc gl_abstr pis env sigma =
  sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false} in
  let princ_proof,levar,lposeq,evararr,absc,parms = proofPrinc mi [] [] [] in
  princ_proof,levar,lposeq,evararr,absc,parms
-
 (* Do intros [i] times, then do rewrite on all introduced hyps which are called
    like [heq_prefix], FIX: have another filter than the name. *)
 let rec iterintro i = 
@@ -596,12 +593,12 @@ let rec iterintro i =
 
 (* 
        (fun hyp gl -> 
-        let _ = print_string ("nthhyp= "^ string_of_int i) in
+        let _ = prstr ("nthhyp= "^ string_of_int i) in
         if isConst hyp && ((name_of_const hyp)==heq_prefix) then
-          let _ = print_string "YES\n" in
+          let _ = prstr "YES\n" in
           rewriteLR hyp gl 
         else 
-          let _ = print_string "NO\n" in
+          let _ = prstr "NO\n" in
           tclIDTAC gl)
  *)
     
@@ -818,9 +815,9 @@ let buildFunscheme fonc mutflist =
     
 (* Declaration of the functional scheme. *)
 let declareFunScheme f fname mutflist =
- let scheme = 
-   buildFunscheme (constr_of f) 
-    (Array.of_list (List.map constr_of (f::mutflist))) in
+ let flist = if mutflist=[] then [f] else mutflist in
+ let fcstrlist = Array.of_list (List.map constr_of flist) in
+ let scheme = buildFunscheme (constr_of f) fcstrlist in
   let _ = prstr "Principe:" in
   let _ = prconstr scheme in
  let ce = { 
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 6f8223575..27f14aedf 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -21,7 +21,7 @@ open Reductionops
 (*s printing of constr -- debugging *)
 
 (* comment this line to see debug msgs *)
-let msg x = () ;; let prterm c = str "" 
+let msg x = () ;; let prterm c = str ""
   (* uncomment this to see debugging *)
 let prconstr c =  msg (str"  " ++ prterm c ++ str"\n")
 let prlistconstr lc = List.iter prconstr lc
@@ -194,52 +194,53 @@ let rec buildrefl_from_eqs eqs =
 
 
 
-(* list of occurrences of a term inside another, no imbricated
-   occurrence are considered (ie we stop looking inside a termthat is
-   an occurrence). *)
+(* list of occurrences of a term inside another *)
+(* Cofix will be wrong, not sure Fix is correct too *)
 let rec hdMatchSub u t=
-  if constr_head_match u t then 
-	 u::(fold_constr (fun l cstr -> l@(hdMatchSub cstr t))
-      [] 
-      u)
-  else
-    fold_constr (fun l cstr -> l@(hdMatchSub cstr t))
-      [] 
-      u
+  let subres = 
+    match kind_of_term u with
+      | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> hdMatchSub (lift 1 cstr) t
+      | Fix (_,(lna,tl,bl))  -> 
+	  Array.fold_left 
+	    (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) t) 
+	    [] bl
+      | LetIn _  -> assert false
+	  (* Correct? *)
+      | _ -> fold_constr (fun l cstr -> l @ hdMatchSub cstr t) [] u
+  in 
+  if constr_head_match u t then u :: subres else subres
+
 
 (* let hdMatchSub_list u lt = List.flatten (List.map (hdMatchSub u) lt) *)
 let hdMatchSub_cpl u (d,f) = 
-	 let res = ref [] in
-	 begin
-	 	for i = d to f do res := (hdMatchSub u (mkRel i)) @ !res done;
-		  !res
-	 end
+  let res = ref [] in
+  begin
+    for i = d to f do res := hdMatchSub u (mkRel i) @ !res done;
+    !res
+  end
 
 
 (* destApplication raises an exception if [t] is not an application *)      
 let exchange_hd_prod subst_hd t =
-    let (hd,args)= destApp t in mkApp (subst_hd,args)
+  let hd,args= destApplication t in mkApp (subst_hd,args)
 
 (* substitute t by by_t in head of products inside in_u, reduces each
 	product found  *)
 let rec substit_red prof t by_t in_u =
   if constr_head_match in_u (lift prof t) 
   then
-	 let _ = prNamedConstr "in_u" in_u in
-	 let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in
-	 let _ = prNamedConstr "xx " x in
-	 let _ = prstr "\n\n" in
-	 x
+    let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in
+    x
   else
-    map_constr_with_binders succ (fun i u -> substit_red i t by_t u)
-    	prof in_u
+    map_constr_with_binders succ (fun i u -> substit_red i t by_t u) prof in_u
 
 (* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each
 	reli by tarr.(f-i). *) 
 let exchange_reli_arrayi tarr (d,f) t =
   let hd,args= destApp t in 
   let i = destRel hd in
-  whd_beta (mkApp (tarr.(f-i) ,args))
+  let res = whd_beta (mkApp (tarr.(f-i) ,args)) in
+  res
 
 let exchange_reli_arrayi_L tarr (d,f) = 
   List.map (exchange_reli_arrayi tarr (d,f))