fixed bug 1791: simpl was performing eta expansion

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

1 files changed, 54 insertions, 28 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 0dd94d813..cc5f44c83 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -99,10 +99,11 @@ let reference_value sigma env c =
 (* One reuses the name of the function after reduction of the fixpoint  *)
 
 type constant_evaluation = 
-  | EliminationFix of int * (int * (int * constr) list * int)
+  | EliminationFix of int * int * (int * (int * constr) list * int)
   | EliminationMutualFix of
       int * evaluable_reference *
-      (evaluable_reference option array * (int * (int * constr) list * int))
+      ((int*evaluable_reference) option array *
+       (int * (int * constr) list * int))
   | EliminationCases of int
   | NotAnElimination
 
@@ -171,24 +172,33 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
          | _ -> 
 	     raise Elimconst) args
   in
-  if list_distinct (List.map fst li) then 
-    let k = lv.(i) in
-    if k < nargs then
+  if not (list_distinct (List.map fst li)) then 
+    raise Elimconst;
+  (* Recursive calls must be applied enough to avoid eta-expansion *)
+(*  let rec no_partial_app k c =
+    let (h,rcargs) = decompose_app c in
+    if eq_constr h (mkRel (k+nbfix-i)) then
+      if List.length rcargs < nargs then raise Elimconst
+      else List.iter (no_partial_app k) rcargs
+    else iter_constr_with_binders succ no_partial_app k c in
+  Array.iter (no_partial_app 0) bds;
+*)
+  let k = lv.(i) in
+  if k < nargs then
 (*  Such an optimisation would need eta-expansion 
       let p = destRel (List.nth args k) in 
       EliminationFix (n-p+1,(nbfix,li,n))
 *)
-      EliminationFix (n,(nbfix,li,n))
-    else
-      EliminationFix (n-nargs+lv.(i)+1,(nbfix,li,n))
-  else 
-    raise Elimconst
+    EliminationFix (n,nargs,(nbfix,li,n))
+  else
+    EliminationFix (n-nargs+k+1,nargs,(nbfix,li,n))
 
 (* Heuristic to look if global names are associated to other
    components of a mutual fixpoint *)
 
 let invert_name labs l na0 env sigma ref = function
   | Name id -> 
+      let minfxargs = List.length l in
       if na0 <> Name id then
 	let refi = match ref with
 	  | EvalRel _ | EvalEvar _ -> None
@@ -205,9 +215,10 @@ let invert_name labs l na0 env sigma ref = function
 		    let labs',ccl = decompose_lam c in
 		    let _, l' = whd_betalet_stack ccl in
 		    let labs' = List.map snd labs' in
-		    if labs' = labs & l = l' then Some ref else None
+		    if labs' = labs & l = l' then Some (minfxargs,ref)
+                    else None
 	      with Not_found (* Undefined ref *) -> None
-      else Some ref
+      else Some (minfxargs,ref)
   | Anonymous -> None (* Actually, should not occur *)
 
 (* [compute_consteval_direct] expand all constant in a whole, but
@@ -242,7 +253,7 @@ let compute_consteval_mutual_fix sigma env ref =
 	  (match compute_consteval_direct sigma env ref with
 	     | NotAnElimination -> (*Above const was eliminable but this not!*)
 		 NotAnElimination
-	     | EliminationFix (minarg',infos) ->
+	     | EliminationFix (minarg',minfxargs,infos) ->
 		 let refs =
 		   Array.map
 		     (invert_name labs l names.(i) env sigma ref) names in
@@ -263,7 +274,7 @@ let compute_consteval_mutual_fix sigma env ref =
 
 let compute_consteval sigma env ref =
   match compute_consteval_direct sigma env ref with
-    | EliminationFix (_,(nbfix,_,_)) when nbfix <> 1 ->
+    | EliminationFix (_,_,(nbfix,_,_)) when nbfix <> 1 ->
 	compute_consteval_mutual_fix sigma env ref
     | elim -> elim
 	
@@ -323,26 +334,41 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
   fun i ->
     match names.(i) with
       | None -> None
-      | Some ref ->
+      | Some (minargs,ref) ->
           let body = applistc (mkEvalRef ref) la in
           let g = 
             list_fold_left_i (fun q (* j from comment is n+1-q *) c (ij,tij) ->
               let subst = List.map (lift (-q)) (list_firstn (n-ij) la) in
               let tij' = substl (List.rev subst) tij in
 	      mkLambda (x,tij',c)) 1 body (List.rev lv)
-          in Some g
+          in Some (minargs,g)
 
 (* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]: 
    do so that the reduction uses this extra information *)
 
+let substl_with_arity subst c =
+  let v = Array.of_list subst in
+  let rec subst_total k c =
+    let (h,rcargs) = decompose_app c in
+    match kind_of_term h with
+        Rel i when k<i ->
+          let h' =
+            if i <= k + Array.length v then
+              match v.(i-k-1) with
+                  (_,Some(min,ref)) when List.length rcargs >= min ->
+                    lift k ref
+                | (fx,_) -> lift k fx
+            else mkRel (i - Array.length v) in
+          applist(h',List.map(subst_total k)rcargs)
+      | _ -> map_constr_with_binders succ subst_total k c in
+  subst_total 0 c
+
 let contract_fix_use_function f
   ((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
   let nbodies = Array.length recindices in
-  let make_Fi j = match f j with
-    | None -> mkFix((recindices,j),typedbodies)
-    | Some c -> c in
+  let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
   let lbodies = list_tabulate make_Fi nbodies in
-  substl (List.rev lbodies) bodies.(bodynum)
+  substl_with_arity (List.rev lbodies) bodies.(bodynum)
 
 let reduce_fix_use_function f whfun fix stack =
   match fix_recarg fix stack with
@@ -362,11 +388,9 @@ let reduce_fix_use_function f whfun fix stack =
 
 let contract_cofix_use_function f (bodynum,(_names,_,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
-  let make_Fi j = match f j with
-    | None -> mkCoFix(j,typedbodies)
-    | Some c -> c in
+  let make_Fi j = (mkCoFix(j,typedbodies), f j) in
   let subbodies = list_tabulate make_Fi nbodies in
-  substl (List.rev subbodies) bodies.(bodynum)
+  substl_with_arity (List.rev subbodies) bodies.(bodynum)
 
 let reduce_mind_case_use_function func env mia =
   match kind_of_term mia.mconstr with 
@@ -377,8 +401,9 @@ let reduce_mind_case_use_function func env mia =
 	let build_cofix_name =
 	  if isConst func then
 	    let (mp,dp,_) = repr_con (destConst func) in
+            let minargs = List.length mia.mcargs in
 	    fun i ->
-	      if i = bodynum then Some func
+	      if i = bodynum then Some (minargs,func)
 	      else match names.(i) with
 		| Anonymous -> None
 		| Name id ->
@@ -389,7 +414,8 @@ let reduce_mind_case_use_function func env mia =
 		    let kn = make_con mp dp (label_of_id id) in
 		    try match constant_opt_value env kn with
 		      | None -> None
-		      | Some _ -> Some (mkConst kn)
+                          (* TODO: check kn is correct *)
+		      | Some _ -> Some (minargs,mkConst kn)
 		    with Not_found -> None
 	  else
 	    fun _ -> None in
@@ -432,10 +458,10 @@ let rec red_elim_const env sigma ref largs =
 	let c', lrest = whd_betadelta_state env sigma (c,largs) in
 	let whfun = whd_simpl_state env sigma in
         (special_red_case sigma env whfun (destCase c'), lrest)
-    | EliminationFix (min,infos) when stack_args_size largs >=min ->
+    | EliminationFix (min,minfxargs,infos) when stack_args_size largs >=min ->
 	let c = reference_value sigma env ref in
 	let d, lrest = whd_betadelta_state env sigma (c,largs) in
-	let f = make_elim_fun ([|Some ref|],infos) largs in
+	let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) largs in
 	let whfun = whd_construct_state env sigma in
 	(match reduce_fix_use_function f whfun (destFix d) lrest with
 	   | NotReducible -> raise Redelimination