Reductionops refactoring

Semantic changes are :
- whd_nored_stack remplaces a defined meta by its value whereas the old whd_stack
  didn't.
- Zcase and Zfix are alwais put on stack. iota_flag is checked by constructors and
  cofix.
- simpl uses its own whd_ function that do not touch at matched term

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

8 files changed, 87 insertions, 58 deletions

diff --git a/lib/option.mli b/lib/option.mli
index 217aa66961..a9899f7428 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -67,7 +67,7 @@ val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
 (** [fold_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *)
 val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option
 
-(** [cata e f x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *)
+(** [cata f e x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *)
 val cata : ('a -> 'b) -> 'b -> 'a option -> 'b
 
 (** {6 More Specific Operations} ***)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a89b2d5458..5680b48aee 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -60,7 +60,7 @@ let evar_apprec ts env evd stack c =
   decompose_app (zip (whd_betaiota_deltazeta_for_iota_state ts env evd (c,append_stack_app_list stack empty_stack)))
 
 let apprec_nohdbeta ts env evd c =
-  match kind_of_term (fst (Reductionops.whd_stack evd c)) with
+  match kind_of_term (fst (Reductionops.whd_nored_stack evd c)) with
     | (Case _ | Fix _) -> applist (evar_apprec ts env evd [] c)
     | _ -> c
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index be2d5e2b7e..29a2b04e0b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -71,9 +71,10 @@ let strip_n_app n s =
 let nfirsts_app_of_stack n s =
   let (args, _) = strip_app s in list_firstn n args
 let list_of_app_stack s =
-  let (out,s') = strip_app s in assert (s' = []); out
+  let (out,s') = strip_app s in
+  Option.init (s' = []) out
 let array_of_app_stack s =
-  Array.of_list (list_of_app_stack s)
+  Option.map Array.of_list (list_of_app_stack s)
 let rec zip = function
   | f, [] -> f
   | f, (Zapp [] :: s) -> zip (f, s)
@@ -136,26 +137,12 @@ let safe_evar_value sigma ev =
   try Some (Evd.existential_value sigma ev)
   with NotInstantiatedEvar | Not_found -> None
 
-let rec whd_app_state sigma (x, stack as s) =
-  match kind_of_term x with
-    | App (f,cl) -> whd_app_state sigma (f, append_stack_app cl stack)
-    | Cast (c,_,_)  -> whd_app_state sigma (c, stack)
-    | Evar ev ->
-        (match safe_evar_value sigma ev with
-            Some c -> whd_app_state sigma (c,stack)
-          | _ -> s)
-    | _             -> s
-
 let safe_meta_value sigma ev =
   try Some (Evd.meta_value sigma ev)
   with Not_found -> None
 
 let appterm_of_stack t = decompose_app (zip t)
 
-let whd_stack sigma x =
-  appterm_of_stack (whd_app_state sigma (x, empty_stack))
-let whd_castapp_stack = whd_stack
-
 let strong whdfun env sigma t =
   let rec strongrec env t =
     map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in
@@ -214,6 +201,7 @@ end : RedFlagsSig)
 open RedFlags
 
 (* Local *)
+let nored = mkflags []
 let beta = mkflags [fbeta]
 let eta = mkflags [feta]
 let zeta = mkflags [fzeta]
@@ -341,30 +329,32 @@ let rec whd_state_gen flags ts env sigma =
 		    | _ -> s)
 	     | _ -> s)
 
-      | Case (ci,p,d,lf) when red_iota flags ->
+      | Case (ci,p,d,lf) ->
 	whrec (d, Zcase (ci,p,lf) :: stack)
 
-      | Fix ((ri,n),_ as f) when red_iota flags ->
+      | 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'))
 
-      | Construct (ind,c) -> begin
-	match strip_app stack with
+      | Construct (ind,c) ->
+	if red_iota flags 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'') ->
 	    let x' = applist(x,args) in
 	    whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
 	  |_ -> s
-      end
+	else s
 
-      | CoFix cofix -> begin
-	match strip_app stack with
+      | CoFix cofix ->
+	if red_iota flags then
+	  match strip_app stack with
 	  |args, (Zcase(ci, _, lf)::s') ->
-	     whrec (contract_cofix cofix, stack)
+	    whrec (contract_cofix cofix, stack)
 	  |_ -> s
-      end
+	else s
 
       | x -> s
   in
@@ -395,10 +385,10 @@ let local_whd_state_gen flags sigma =
 		    | _ -> s)
 	     | _ -> s)
 
-      | Case (ci,p,d,lf) when red_iota flags ->
+      | Case (ci,p,d,lf) ->
 	whrec (d, Zcase (ci,p,lf) :: stack)
 
-      | Fix ((ri,n),_ as f) when red_iota flags ->
+      | 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'))
@@ -413,22 +403,24 @@ let local_whd_state_gen flags sigma =
               Some c -> whrec (c,stack)
             | None -> s)
 
-      | Construct (ind,c) -> begin
-	match strip_app stack with
+      | Construct (ind,c) ->
+	if red_iota flags 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'') ->
 	    let x' = applist(x,args) in
 	    whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s''))
 	  |_ -> s
-      end
+	else s
 
-      | CoFix cofix -> begin
-	match strip_app stack with
-	  |args, (Zcase(ci, _, lf)::s') ->
-	     whrec (contract_cofix cofix, stack)
+      | CoFix cofix ->
+	if red_iota flags then
+	  match strip_app stack with
+	  |args, (Zcase(ci, _, lf)::s') when red_iota flags ->
+	    whrec (contract_cofix cofix, stack)
 	  |_ -> s
-      end
+	else s
 
       | x -> s
   in
@@ -441,6 +433,11 @@ let stack_red_of_state_red f sigma x =
 let red_of_state_red f sigma x =
   zip (f sigma (x,empty_stack))
 
+(* 0. No Reduction Functions *)
+
+let whd_nored_state = local_whd_state_gen nored
+let whd_nored_stack = stack_red_of_state_red whd_nored_state
+
 (* 1. Beta Reduction Functions *)
 
 let whd_beta_state = local_whd_state_gen beta
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 083834218e..ea12dc49b1 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -39,8 +39,10 @@ val decomp_stack : 'a stack -> ('a * 'a stack) option
 (** Takes the n first arguments of application put on the stack. Fails is the
     stack does not start by n arguments of application. *)
 val nfirsts_app_of_stack : int -> 'a stack -> 'a list
-val list_of_app_stack : 'a stack -> 'a list
-val array_of_app_stack : 'a stack -> 'a array
+(** @return (the nth first elements, the (n+1)th element, the remaining stack)  *)
+val strip_n_app : int -> 'a stack -> ('a list * 'a * 'a stack) option
+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
@@ -66,12 +68,6 @@ type contextual_state_reduction_function =
 type state_reduction_function = contextual_state_reduction_function
 type local_state_reduction_function = evar_map -> state -> state
 
-(** Removes cast and put into applicative form *)
-val whd_stack : local_stack_reduction_function
-
-(** For compatibility: alias for whd\_stack *)
-val whd_castapp_stack : local_stack_reduction_function
-
 (** {6 Reduction Function Operators } *)
 
 val strong : reduction_function -> reduction_function
@@ -106,6 +102,8 @@ val whd_betadeltaiota_nolet :  contextual_reduction_function
 val whd_betaetalet : local_reduction_function
 val whd_betalet : local_reduction_function
 
+(** Removes cast and put into applicative form *)
+val whd_nored_stack : local_stack_reduction_function
 val whd_beta_stack : local_stack_reduction_function
 val whd_betaiota_stack : local_stack_reduction_function
 val whd_betaiotazeta_stack : local_stack_reduction_function
@@ -114,6 +112,7 @@ val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function
 val whd_betaetalet_stack : local_stack_reduction_function
 val whd_betalet_stack : local_stack_reduction_function
 
+val whd_nored_state : local_state_reduction_function
 val whd_beta_state : local_state_reduction_function
 val whd_betaiota_state : local_state_reduction_function
 val whd_betaiotazeta_state : local_state_reduction_function
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index fa7ca0eb82..f01cc76d8f 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -617,6 +617,39 @@ let recargs r =
 let dont_expose_case r =
   try (get_behaviour r).b_dont_expose_case with Not_found -> false
 
+let whd_nothing_for_iota env sigma s =
+  let rec whrec (x, stack as s) =
+    match kind_of_term x with
+      | Rel n ->
+	  (match lookup_rel n env with
+	     | (_,Some body,_) -> whrec (lift n body, stack)
+	     | _ -> s)
+      | Var id ->
+	  (match lookup_named id env with
+	     | (_,Some body,_) -> whrec (body, stack)
+	     | _ -> s)
+      | Evar ev ->
+	(try whrec (Evd.existential_value sigma ev, stack)
+	with Evd.NotInstantiatedEvar | Not_found -> s)
+      | Meta ev ->
+	(try whrec (Evd.meta_value sigma ev, stack)
+	with Not_found -> s)
+      | Const const when is_transparent_constant full_transparent_state const ->
+	  (match constant_opt_value env const with
+	     | Some  body -> whrec (body, stack)
+	     | None -> s)
+      | LetIn (_,b,_,c) -> stacklam whrec [b] c stack
+      | Cast (c,_,_) -> whrec (c, stack)
+      | App (f,cl)  -> whrec (f, append_stack_app cl stack)
+      | Lambda (na,t,c) ->
+          (match decomp_stack stack with
+             | Some (a,m) -> stacklam whrec [a] c m
+	     | _ -> s)
+
+      | x -> s
+  in
+  decompose_app (zip (whrec (s,empty_stack)))
+
 (* [red_elim_const] contracts iota/fix/cofix redexes hidden behind
    constants by keeping the name of the constants in the recursive calls;
    it fails if no redex is around *)
@@ -640,12 +673,12 @@ let rec red_elim_const env sigma ref largs =
   try match reference_eval sigma env ref with
     | EliminationCases n when nargs >= n ->
 	let c = reference_value sigma env ref in
-	let c', lrest = whd_betadelta_stack env sigma (applist(c,largs)) in
+	let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
 	let whfun = whd_simpl_stack env sigma in
         (special_red_case env sigma whfun (destCase c'), lrest)
     | EliminationFix (min,minfxargs,infos) when nargs >= min ->
 	let c = reference_value sigma env ref in
-	let d, lrest = whd_betadelta_stack env sigma (applist(c,largs)) in
+	let d, lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
 	let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) largs in
 	let whfun = whd_construct_stack env sigma in
 	(match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
@@ -660,7 +693,7 @@ let rec red_elim_const env sigma ref largs =
 	    let c', lrest = whd_betalet_stack sigma (applist(c,args)) in
 	    descend (destEvalRef c') lrest in
 	let (_, midargs as s) = descend ref largs in
-	let d, lrest = whd_betadelta_stack env sigma (applist s) in
+	let d, lrest = whd_nothing_for_iota env sigma (applist s) in
 	let f = make_elim_fun refinfos midargs in
 	let whfun = whd_construct_stack env sigma in
 	(match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
@@ -1082,7 +1115,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
   else
   (* lazily reduces to match the head of [t] with the expected [ref] *)
   let rec elimrec env t l =
-    let c, _ = Reductionops.whd_stack sigma t in
+    let c, _ = Reductionops.whd_nored_stack sigma t in
     match kind_of_term c with
       | Prod (n,ty,t') ->
 	  if allow_product then
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index cda1621e2f..7bec34078f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -967,12 +967,12 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
    types of metavars are unifiable with the types of their instances    *)
 
 let check_types env flags (sigma,_,_ as subst) m n =
-  if isEvar_or_Meta (fst (whd_stack sigma m)) then
+  if isEvar_or_Meta (fst (whd_nored_stack sigma m)) then
     unify_0_with_initial_metas subst true env CUMUL
       flags
       (get_type_of env sigma n)
       (get_type_of env sigma m)
-  else if isEvar_or_Meta (fst (whd_stack sigma n)) then
+  else if isEvar_or_Meta (fst (whd_nored_stack sigma n)) then
     unify_0_with_initial_metas subst true env CUMUL
       flags
       (get_type_of env sigma m)
@@ -1193,8 +1193,8 @@ let secondOrderAbstractionAlgo dep =
   if dep then secondOrderDependentAbstraction else secondOrderAbstraction
 
 let w_unify2 env evd flags dep cv_pb ty1 ty2 =
-  let c1, oplist1 = whd_stack evd ty1 in
-  let c2, oplist2 = whd_stack evd ty2 in
+  let c1, oplist1 = whd_nored_stack evd ty1 in
+  let c2, oplist2 = whd_nored_stack evd ty2 in
   match kind_of_term c1, kind_of_term c2 with
     | Meta p1, _ ->
         (* Find the predicate *)
@@ -1225,8 +1225,8 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 =
    convertible and first-order otherwise. But if failed if e.g. the type of
    Meta(1) had meta-variables in it. *)
 let w_unify env evd cv_pb ?(flags=default_unify_flags) ty1 ty2 =
-  let hd1,l1 = whd_stack evd ty1 in
-  let hd2,l2 = whd_stack evd ty2 in
+  let hd1,l1 = whd_nored_stack evd ty1 in
+  let hd2,l2 = whd_nored_stack evd ty2 in
     match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
       (* Pattern case *)
       | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index fb1900f2f6..864806f851 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -276,7 +276,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
 
 let clenv_unique_resolver ?(flags=default_unify_flags) clenv gl =
   let concl = Goal.V82.concl clenv.evd (sig_it gl) in
-  if isMeta (fst (whd_stack clenv.evd clenv.templtyp.rebus)) then
+  if isMeta (fst (whd_nored_stack clenv.evd clenv.templtyp.rebus)) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
   else
@@ -429,7 +429,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (whd_stack clenv.evd u)) then
+  if isMeta (fst (whd_nored_stack clenv.evd u)) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 44bda9aace..023df361fd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1163,7 +1163,7 @@ let specialize mopt (c,lbind) g =
       let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
       let flags = { default_unify_flags with resolve_evars = true } in
       let clause = clenv_unify_meta_types ~flags clause in
-      let (thd,tstack) = whd_stack clause.evd (clenv_value clause) in
+      let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
       let nargs = List.length tstack in
       let tstack = match mopt with
 	| Some m ->