Reductionops reduction machine can refold constant

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

4 files changed, 136 insertions, 85 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 8238a3c94..614f99ee8 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -184,13 +184,13 @@ let ise_stack2 no_app env evd f sk1 sk2 =
       else None, (evd, false) in
     match sk1, sk2 with
     | [], [] -> None, (i,true)
-    | Zcase (_,t1,c1)::q1, Zcase (_,t2,c2)::q2 ->
+    | Zcase (_,t1,c1,_)::q1, Zcase (_,t2,c2,_)::q2 ->
       let (i',b') = f env i CONV t1 t2 in
       if b' then
 	let (i'',b'') = ise_array2 i' (fun ii -> f env ii CONV) c1 c2 in
 	if b'' then ise_stack2 true i'' q1 q2 else fal ()
       else fal ()
-    | Zfix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1, Zfix (((li2, i2),(_,tys2,bds2)),a2)::q2 ->
+    | Zfix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, Zfix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 ->
       if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
         let (i',b') = ise_and i [
 	  (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2);
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f2366ea02..0b89830ef 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -25,8 +25,8 @@ exception Elimconst
 
 type 'a stack_member =
   | Zapp of 'a list
-  | Zcase of case_info * 'a * 'a array
-  | Zfix of fixpoint * 'a list
+  | Zcase of case_info * 'a * 'a array * ('a * 'a list) option
+  | Zfix of fixpoint * 'a list * ('a * 'a list) option
   | Zshift of int
   | Zupdate of 'a
 
@@ -73,15 +73,20 @@ let list_of_app_stack s =
   Option.init init out
 let array_of_app_stack s =
   Option.map Array.of_list (list_of_app_stack s)
-let rec zip = function
+let rec zip ?(refold=false) = function
   | f, [] -> f
-  | f, (Zapp [] :: s) -> zip (f, s)
+  | f, (Zapp [] :: s) -> zip ~refold (f, s)
   | f, (Zapp args :: s) ->
-      zip (applist (f, args), s)
-  | f, (Zcase (ci,rt,br)::s) -> zip (mkCase (ci,rt,f,br), s)
-  | f, (Zfix (fix,st)::s) -> zip
+      zip ~refold (applist (f, args), s)
+  | f, (Zcase (ci,rt,br,Some(cst, params))::s) when refold ->
+    zip ~refold (cst, append_stack_app_list (List.rev params) s)
+  | f, (Zcase (ci,rt,br,_)::s) -> zip ~refold (mkCase (ci,rt,f,br), s)
+  | f, (Zfix (fix,st,Some(cst, params))::s) when refold -> zip ~refold
+    (cst, append_stack_app_list (List.rev params)
+      (append_stack_app_list st (append_stack_app_list [f] s)))
+  | f, (Zfix (fix,st,_)::s) -> zip ~refold
     (mkFix fix, append_stack_app_list st (append_stack_app_list [f] s))
-  | f, (Zshift n::s) -> zip (lift n f, s)
+  | f, (Zshift n::s) -> zip ~refold (lift n f, s)
   | _ -> assert false
 let rec stack_assign s p c = match s with
   | Zapp args :: s ->
@@ -180,10 +185,18 @@ let betadeltaiotaeta = Closure.RedFlags.red_add betadeltaiota Closure.RedFlags.f
 
 (* Beta Reduction tools *)
 
+let apply_subst recfun env cst_l t stack =
+  let rec aux env cst_l t stack =
+    match (decomp_stack stack,kind_of_term t) with
+    | Some (h,stacktl), Lambda (_,_,c) ->
+      let append2cst (c,params,nb_skip) =
+	if nb_skip <= 0 then (c, h::params, nb_skip) else (c, params, pred nb_skip) in
+      aux (h::env) (List.map append2cst cst_l) c stacktl
+    | _ -> recfun cst_l (substl env t, stack)
+  in aux env cst_l t stack
+
 let rec stacklam recfun env t stack =
-  match (decomp_stack stack,kind_of_term t) with
-    | Some (h,stacktl), Lambda (_,_,c) -> stacklam recfun (h::env) c stacktl
-    | _ -> recfun (substl env t, stack)
+apply_subst (fun _ -> recfun) env [] t stack
 
 let beta_applist (c,l) =
   stacklam zip [] c (append_stack_app_list l empty_stack)
@@ -201,10 +214,17 @@ let reducible_mind_case c = match kind_of_term c with
   | Construct _ | CoFix _ -> true
   | _  -> false
 
-let contract_cofix (bodynum,(types,names,bodies as typedbodies)) =
+let contract_cofix (bodynum,(types,names,bodies as typedbodies)) cst =
   let nbodies = Array.length bodies in
-  let make_Fi j = mkCoFix (nbodies-j-1,typedbodies) in
-  substl (List.tabulate make_Fi nbodies) bodies.(bodynum)
+    let make_Fi j =
+      let ind = nbodies-j-1 in
+      if bodynum = ind && not (Option.is_empty cst) then
+	let (c,params) = Option.get cst in
+	applist(c, List.rev params)
+      else
+	mkCoFix (ind,typedbodies) in
+    let closure = List.tabulate make_Fi nbodies in
+    substl closure bodies.(bodynum)
 
 let reduce_mind_case mia =
   match kind_of_term mia.mconstr with
@@ -213,17 +233,24 @@ let reduce_mind_case mia =
 	let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
         applist (mia.mlf.(i-1),real_cargs)
     | CoFix cofix ->
-	let cofix_def = contract_cofix cofix in
+	let cofix_def = contract_cofix cofix None in
 	mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
 (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
    Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
 
-let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) =
-  let nbodies = Array.length recindices in
-  let make_Fi j = mkFix ((recindices,nbodies-j-1),typedbodies) in
-  substl (List.tabulate make_Fi nbodies) bodies.(bodynum)
+let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) cst =
+    let nbodies = Array.length recindices in
+    let make_Fi j =
+      let ind = nbodies-j-1 in
+      if bodynum = ind && not (Option.is_empty cst) then
+	let (c,params) = Option.get cst in
+	applist(c, List.rev params)
+      else
+	mkFix ((recindices,ind),typedbodies) in
+    let closure = List.tabulate make_Fi nbodies in
+    substl closure bodies.(bodynum)
 
 let fix_recarg ((recindices,bodynum),_) stack =
   assert (0 <= bodynum & bodynum < Array.length recindices);
@@ -242,41 +269,57 @@ let fix_recarg ((recindices,bodynum),_) stack =
                               -------------------
    qui coute cher *)
 
-let rec whd_state_gen flags env sigma =
-  let rec whrec (x, stack as s) =
+let rec whd_state_gen ?(refold=false) flags env sigma =
+  let noth = [] in
+  let rec whrec cst_l (x, stack as s) =
+    let best_cst () = List.fold_left
+      (fun def (c,params,nb_skip) -> if nb_skip = 0 then Some(c,params) else def)
+      None cst_l in
+    let best_state def (cst,params,nb_skip) =
+      let apps,s' = strip_app stack in
+      try
+	let _,aft = List.chop nb_skip apps in
+	(cst, append_stack_app_list (List.rev params) (append_stack_app_list aft s'))
+      with Failure _ -> def in
+    let fold () =
+      if refold then List.fold_left best_state s cst_l else s
+    in
     match kind_of_term x with
       | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA ->
 	  (match lookup_rel n env with
-	     | (_,Some body,_) -> whrec (lift n body, stack)
-	     | _ -> s)
+	     | (_,Some body,_) -> whrec noth (lift n body, stack)
+	     | _ -> fold ())
       | Var id when Closure.RedFlags.red_set flags (Closure.RedFlags.fVAR id) ->
 	  (match lookup_named id env with
-	     | (_,Some body,_) -> whrec (body, stack)
-	     | _ -> s)
+	     | (_,Some body,_) -> whrec ((mkVar id,[],0)::cst_l) (body, stack)
+	     | _ -> fold ())
       | Evar ev ->
 	  (match safe_evar_value sigma ev with
-	     | Some body -> whrec (body, stack)
-	     | None -> s)
+	     | Some body -> whrec noth (body, stack)
+	     | None -> fold ())
       | Meta ev ->
 	  (match safe_meta_value sigma ev with
-	     | Some body -> whrec (body, stack)
-	     | None -> s)
+	     | Some body -> whrec noth (body, stack)
+	     | None -> fold ())
       | Const const when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST const) ->
 	  (match constant_opt_value env const with
-	     | Some  body -> whrec (body, stack)
-	     | None -> s)
+	     | Some  body -> whrec ((mkConst const,[],0)::cst_l) (body, stack)
+	     | None -> fold ())
       | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA ->
-	stacklam whrec [b] c stack
-      | Cast (c,_,_) -> whrec (c, stack)
-      | App (f,cl)  -> whrec (f, append_stack_app cl stack)
+	apply_subst whrec [b] cst_l c stack
+      | Cast (c,_,_) -> whrec cst_l (c, stack)
+      | App (f,cl)  ->
+	whrec
+	  (List.map (fun (a,b,nb_skip) -> (a,b,nb_skip+Array.length cl)) cst_l)
+	  (f, append_stack_app cl stack)
       | Lambda (na,t,c) ->
           (match decomp_stack stack with
-             | Some (a,m) when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA ->
-	       stacklam whrec [a] c m
+             | Some _ when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA ->
+	       apply_subst whrec [] cst_l x stack
              | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA ->
 		 let env' = push_rel (na,None,t) env in
-		 let whrec' = whd_state_gen flags env' sigma in
-                 (match kind_of_term (zip (whrec' (c, empty_stack))) with
+		 let whrec' = whd_state_gen ~refold flags env' sigma in
+                 (match kind_of_term (zip ~refold (whrec' (c, empty_stack))) with
                     | App (f,cl) ->
 			let napp = Array.length cl in
 			if napp > 0 then
@@ -285,42 +328,43 @@ let rec whd_state_gen flags env sigma =
                             | Rel 1, [] ->
 				let lc = Array.sub cl 0 (napp-1) in
 				let u = if Int.equal napp 1 then f else appvect (f,lc) in
-				if noccurn 1 u then (pop u,empty_stack) else s
-                            | _ -> s
-			else s
-		    | _ -> s)
-	     | _ -> s)
+				if noccurn 1 u then (pop u,empty_stack) else fold ()
+                            | _ -> fold ()
+			else fold ()
+		    | _ -> fold ())
+	     | _ -> fold ())
 
       | Case (ci,p,d,lf) ->
-	whrec (d, Zcase (ci,p,lf) :: stack)
+	whrec noth (d, Zcase (ci,p,lf,best_cst ()) :: stack)
 
       | Fix ((ri,n),_ as f) ->
 	(match strip_n_app ri.(n) stack with
-	  |None -> s
-	  |Some (bef,arg,s') -> whrec (arg, Zfix(f,bef)::s'))
+	  |None -> fold ()
+	  |Some (bef,arg,s') -> whrec noth (arg, Zfix(f,bef,best_cst ())::s'))
 
       | Construct (ind,c) ->
 	if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	  match strip_app stack with
-	  |args, (Zcase(ci, _, lf)::s') ->
-	    whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
-	  |args, (Zfix (f,s')::s'') ->
+	  |args, (Zcase(ci, _, lf,_)::s') ->
+	    whrec noth (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
+	  |args, (Zfix (f,s',cst)::s'') ->
 	    let x' = applist(x,args) in
-	    whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
-	  |_ -> s
-	else s
+	    whrec noth (contract_fix f cst, append_stack_app_list s' (append_stack_app_list [x'] s''))
+	  |_ -> fold ()
+	else fold ()
 
       | CoFix cofix ->
 	if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	  match strip_app stack with
-	  |args, (Zcase(ci, _, lf)::s') ->
-	    whrec (contract_cofix cofix, stack)
-	  |_ -> s
-	else s
+	  |args, (Zcase(ci, _, lf,_)::s') ->
+	    whrec noth (contract_cofix cofix (best_cst ()), stack)
+	  |_ -> fold ()
+	else fold ()
 
-      | x -> s
+      | Rel _ | Var _ | Const _ | LetIn _ -> fold ()
+      | Sort _ | Ind _ | Prod _ -> fold ()
   in
-  whrec
+  whrec noth
 
 let local_whd_state_gen flags sigma =
   let rec whrec (x, stack as s) =
@@ -350,12 +394,12 @@ let local_whd_state_gen flags sigma =
 	     | _ -> s)
 
       | Case (ci,p,d,lf) ->
-	whrec (d, Zcase (ci,p,lf) :: stack)
+	whrec (d, Zcase (ci,p,lf,None) :: stack)
 
       | Fix ((ri,n),_ as f) ->
 	(match strip_n_app ri.(n) stack with
 	  |None -> s
-	  |Some (bef,arg,s') -> whrec (arg, Zfix(f,bef)::s'))
+	  |Some (bef,arg,s') -> whrec (arg, Zfix(f,bef,None)::s'))
 
       | Evar ev ->
           (match safe_evar_value sigma ev with
@@ -370,19 +414,19 @@ let local_whd_state_gen flags sigma =
       | Construct (ind,c) ->
 	if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	  match strip_app stack with
-	  |args, (Zcase(ci, _, lf)::s') ->
+	  |args, (Zcase(ci, _, lf,_)::s') ->
 	    whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
-	  |args, (Zfix (f,s')::s'') ->
+	  |args, (Zfix (f,s',cst)::s'') ->
 	    let x' = applist(x,args) in
-	    whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
+	    whrec (contract_fix f cst,append_stack_app_list s' (append_stack_app_list [x'] s''))
 	  |_ -> s
 	else s
 
       | CoFix cofix ->
 	if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	  match strip_app stack with
-	  |args, (Zcase(ci, _, lf)::s') ->
-	    whrec (contract_cofix cofix, stack)
+	  |args, (Zcase(ci, _, lf,_)::s') ->
+	    whrec (contract_cofix cofix None, stack)
 	  |_ -> s
 	else s
 
@@ -548,22 +592,22 @@ let whd_betaiota_preserving_vm_cast env sigma t =
             | Some (a,m) -> stacklam_var [a] c m
             | _ -> s)
        | Case (ci,p,d,lf) ->
-	 whrec (d, Zcase (ci,p,lf) :: stack)
+	 whrec (d, Zcase (ci,p,lf,None) :: stack)
 
        | Construct (ind,c) -> begin
 	 match strip_app stack with
-	   |args, (Zcase(ci, _, lf)::s') ->
+	   |args, (Zcase(ci, _, lf,_)::s') ->
 	     whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
-	   |args, (Zfix (f,s')::s'') ->
+	   |args, (Zfix (f,s',cst)::s'') ->
 	     let x' = applist(x,args) in
-	     whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
+	     whrec (contract_fix f cst,append_stack_app_list s' (append_stack_app_list [x'] s''))
 	   |_ -> s
        end
 
        | CoFix cofix -> begin
 	 match strip_app stack with
-	   |args, (Zcase(ci, _, lf)::s') ->
-	     whrec (contract_cofix cofix, stack)
+	   |args, (Zcase(ci, _, lf,_)::s') ->
+	     whrec (contract_cofix cofix None, stack)
 	   |_ -> s
        end
 
@@ -846,24 +890,24 @@ let whd_programs_stack env sigma =
 	  if occur_existential d then
 	    s
 	  else
-	    whrec (d, Zcase (ci,p,lf) :: stack)
+	    whrec (d, Zcase (ci,p,lf,None) :: stack)
       | Fix ((ri,n),_ as f) ->
 	(match strip_n_app ri.(n) stack with
 	  |None -> s
-	  |Some (bef,arg,s') -> whrec (arg, Zfix(f,bef)::s'))
+	  |Some (bef,arg,s') -> whrec (arg, Zfix(f,bef,None)::s'))
       | Construct (ind,c) -> begin
 	match strip_app stack with
-	  |args, (Zcase(ci, _, lf)::s') ->
+	  |args, (Zcase(ci, _, lf,_)::s') ->
 	    whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s')
-	  |args, (Zfix (f,s')::s'') ->
+	  |args, (Zfix (f,s',cst)::s'') ->
 	    let x' = applist(x,args) in
-	    whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
+	    whrec (contract_fix f cst,append_stack_app_list s' (append_stack_app_list [x'] s''))
 	  |_ -> s
       end
       | CoFix cofix -> begin
 	match strip_app stack with
-	  |args, (Zcase(ci, _, lf)::s') ->
-	     whrec (contract_cofix cofix, stack)
+	  |args, (Zcase(ci, _, lf,_)::s') ->
+	     whrec (contract_cofix cofix None, stack)
 	  |_ -> s
       end
       | _ -> s
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 60c111370..7a80f9121 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -24,8 +24,8 @@ exception Elimconst
 
 type 'a stack_member =
   | Zapp of 'a list
-  | Zcase of case_info * 'a * 'a array
-  | Zfix of fixpoint * 'a list
+  | Zcase of case_info * 'a * 'a array * ('a * 'a list) option
+  | Zfix of fixpoint * 'a list * ('a * 'a list) option
   | Zshift of int
   | Zupdate of 'a
 
@@ -46,7 +46,7 @@ val list_of_app_stack : 'a stack -> 'a list option
 val array_of_app_stack : 'a stack -> 'a array option
 val stack_assign : 'a stack -> int -> 'a -> 'a stack
 val stack_args_size : 'a stack -> int
-val zip : constr * constr stack -> constr
+val zip : ?refold:bool -> constr * constr stack -> constr
 val stack_tail : int -> 'a stack -> 'a stack
 val stack_nth : 'a stack -> int -> 'a
 
@@ -80,6 +80,13 @@ val stack_reduction_of_reduction :
 i*)
 val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a
 
+val whd_state_gen : ?refold:bool ->
+  Closure.RedFlags.reds ->
+  Environ.env ->
+  Evd.evar_map ->
+  Term.constr * Term.constr stack_member list ->
+  Term.constr * Term.constr stack_member list
+
 (** {6 Generic Optimized Reduction Function using Closures } *)
 
 val clos_norm_flags : Closure.RedFlags.reds -> reduction_function
@@ -180,7 +187,7 @@ val is_arity : env ->  evar_map -> constr -> bool
 
 val whd_programs :  reduction_function
 
-val contract_fix : fixpoint -> Term.constr
+val contract_fix : fixpoint -> (constr * constr list) option -> constr
 val fix_recarg : fixpoint -> constr stack -> (int * constr) option
 
 (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 78b01a42a..b265d636e 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -450,7 +450,7 @@ let reduce_fix whdfun sigma fix stack =
         let (recarg'hd,_ as recarg') = whdfun sigma recarg in
         let stack' = List.assign stack recargnum (applist recarg') in
 	(match kind_of_term recarg'hd with
-           | Construct _ -> Reduced (contract_fix fix, stack')
+           | Construct _ -> Reduced (contract_fix fix None, stack')
 	   | _ -> NotReducible)
 
 let contract_fix_use_function env sigma f