Fixup and comment reductionops

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

1 files changed, 172 insertions, 165 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0b89830ef..1cae8ca47 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -19,17 +19,21 @@ open Reduction
 
 exception Elimconst
 
+(** This module implements a call by name reduction used by (at
+    least) evarconv unification and cbn tactic.
+
+    It has an ability to "refold" constants by storing constants and
+    their parameters in its stack.
+*)
 
-(**********************************************************************)
-(* The type of (machine) stacks (= lambda-bar-calculus' contexts)     *)
 
+(** The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
 type 'a stack_member =
   | Zapp of '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
-
 and 'a stack = 'a stack_member list
 
 let empty_stack = []
@@ -46,7 +50,6 @@ let rec stack_args_size = function
   | Zupdate(_)::s -> stack_args_size s
   | _ -> 0
 
-(* When used as an argument stack (only Zapp can appear) *)
 let rec decomp_stack = function
   | Zapp[v]::s -> Some (v, s)
   | Zapp(v::l)::s -> Some (v, (Zapp l :: s))
@@ -73,21 +76,6 @@ 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 ?(refold=false) = function
-  | f, [] -> f
-  | f, (Zapp [] :: s) -> zip ~refold (f, s)
-  | f, (Zapp args :: s) ->
-      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 ~refold (lift n f, s)
-  | _ -> assert false
 let rec stack_assign s p c = match s with
   | Zapp args :: s ->
       let q = List.length args in
@@ -113,8 +101,23 @@ let rec stack_nth s p = match s with
       else List.nth args p
   | _ -> raise Not_found
 
-(**************************************************************)
-(* The type of (machine) states (= lambda-bar-calculus' cuts) *)
+let rec zip ?(refold=false) = function
+  | f, [] -> f
+  | f, (Zapp [] :: s) -> zip ~refold (f, s)
+  | f, (Zapp args :: s) ->
+      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 ~refold (lift n f, s)
+  | _ -> assert false
+
+(** The type of (machine) states (= lambda-bar-calculus' cuts) *)
 type state = constr * constr stack
 
 type  contextual_reduction_function = env ->  evar_map -> constr -> constr
@@ -260,21 +263,23 @@ let fix_recarg ((recindices,bodynum),_) stack =
   with Not_found ->
     None
 
-(* Generic reduction function *)
+(** Generic reduction function with environment
 
-(* Y avait un commentaire pour whd_betadeltaiota :
-
-   NB : Cette fonction alloue peu c'est l'appel
-     ``let (c,cargs) = whfun (recarg, empty_stack)''
-                              -------------------
-   qui coute cher *)
+    Here is where unfolded constant are stored in order to be
+    eventualy refolded.
 
+    It uses the flag refold when it reaches a value and because it
+    substitutes fix and cofix by the constant they come from in
+    contract_*.
+*)
 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_cst () =
+      if refold then List.fold_left
+	(fun def (c,params,nb_skip) -> if nb_skip = 0 then Some(c,params) else def)
+	None cst_l
+      else None in
     let best_state def (cst,params,nb_skip) =
       let apps,s' = strip_app stack in
       try
@@ -285,152 +290,154 @@ let rec whd_state_gen ?(refold=false) flags env sigma =
       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 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 ((mkVar id,[],0)::cst_l) (body, stack)
-	     | _ -> fold ())
-      | Evar ev ->
-	  (match safe_evar_value sigma ev with
-	     | Some body -> whrec noth (body, stack)
-	     | None -> fold ())
-      | Meta ev ->
-	  (match safe_meta_value sigma ev with
-	     | 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 ((mkConst const,[],0)::cst_l) (body, stack)
-	     | None -> fold ())
-      | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA ->
-	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 _ 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 ~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
-			  let x', l' = whrec' (Array.last cl, empty_stack) in
-                          match kind_of_term x', l' with
-                            | 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 fold ()
-                            | _ -> fold ()
-			else fold ()
-		    | _ -> fold ())
-	     | _ -> fold ())
-
-      | Case (ci,p,d,lf) ->
-	whrec noth (d, Zcase (ci,p,lf,best_cst ()) :: stack)
-
-      | Fix ((ri,n),_ as f) ->
-	(match strip_n_app ri.(n) stack with
-	  |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 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 noth (contract_fix f cst, append_stack_app_list s' (append_stack_app_list [x'] s''))
-	  |_ -> fold ()
-	else fold ()
+    | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA ->
+      (match lookup_rel n env with
+      | (_,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 ((mkVar id,[],0)::cst_l) (body, stack)
+      | _ -> fold ())
+    | Evar ev ->
+      (match safe_evar_value sigma ev with
+      | Some body -> whrec noth (body, stack)
+      | None -> fold ())
+    | Meta ev ->
+      (match safe_meta_value sigma ev with
+      | 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 ((mkConst const,[],0)::cst_l) (body, stack)
+      | None -> fold ())
+    | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA ->
+      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 _ 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 ~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
+	    let x', l' = whrec' (Array.last cl, empty_stack) in
+            match kind_of_term x', l' with
+            | 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 fold ()
+            | _ -> fold ()
+	  else fold ()
+	| _ -> fold ())
+      | _ -> fold ())
+
+    | Case (ci,p,d,lf) ->
+      whrec noth (d, Zcase (ci,p,lf,best_cst ()) :: stack)
+
+    | Fix ((ri,n),_ as f) ->
+      (match strip_n_app ri.(n) stack with
+      |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 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 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 noth (contract_cofix cofix (best_cst ()), stack)
-	  |_ -> 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 noth (contract_cofix cofix (best_cst ()), stack)
+	|_ -> fold ()
+      else fold ()
 
-      | Rel _ | Var _ | Const _ | LetIn _ -> fold ()
-      | Sort _ | Ind _ | Prod _ -> fold ()
+    | Rel _ | Var _ | Const _ | LetIn _ -> fold ()
+    | Sort _ | Ind _ | Prod _ -> fold ()
   in
   whrec noth
 
+(** reduction machine without global env and refold machinery *)
 let local_whd_state_gen flags sigma =
   let rec whrec (x, stack as s) =
     match kind_of_term x with
-      | 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)
-      | Lambda (_,_,c) ->
-          (match decomp_stack stack with
-             | Some (a,m) when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA ->
-	       stacklam whrec [a] c m
-             | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA ->
-                 (match kind_of_term (zip (whrec (c, empty_stack))) with
-                    | App (f,cl) ->
-			let napp = Array.length cl in
-			if napp > 0 then
-			  let x', l' = whrec (Array.last cl, empty_stack) in
-                          match kind_of_term x', l' with
-                            | 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)
-
-      | Case (ci,p,d,lf) ->
-	whrec (d, Zcase (ci,p,lf,None) :: stack)
+    | 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)
+    | Lambda (_,_,c) ->
+      (match decomp_stack stack with
+      | Some (a,m) when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA ->
+	stacklam whrec [a] c m
+      | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA ->
+        (match kind_of_term (zip (whrec (c, empty_stack))) with
+        | App (f,cl) ->
+	  let napp = Array.length cl in
+	  if napp > 0 then
+	    let x', l' = whrec (Array.last cl, empty_stack) in
+            match kind_of_term x', l' with
+            | 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)
+
+    | Case (ci,p,d,lf) ->
+      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,None)::s'))
 
-      | Fix ((ri,n),_ as f) ->
-	(match strip_n_app ri.(n) stack with
-	  |None -> s
-	  |Some (bef,arg,s') -> whrec (arg, Zfix(f,bef,None)::s'))
-
-      | Evar ev ->
-          (match safe_evar_value sigma ev with
-              Some c -> whrec (c,stack)
-            | None -> s)
+    | Evar ev ->
+      (match safe_evar_value sigma ev with
+        Some c -> whrec (c,stack)
+      | None -> s)
 
-      | Meta ev ->
-          (match safe_meta_value sigma ev with
-              Some c -> whrec (c,stack)
-            | None -> s)
+    | Meta ev ->
+      (match safe_meta_value sigma ev with
+        Some c -> whrec (c,stack)
+      | None -> 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',cst)::s'') ->
-	    let x' = applist(x,args) in
-	    whrec (contract_fix f cst,append_stack_app_list s' (append_stack_app_list [x'] s''))
-	  |_ -> s
-	else 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',cst)::s'') ->
+	  let x' = applist(x,args) in
+	  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 None, stack)
-	  |_ -> 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 None, stack)
+	|_ -> s
+      else s
 
-      | x -> s
+    | x -> s
   in
   whrec
 
@@ -548,7 +555,7 @@ let clos_norm_flags flgs env sigma t =
     norm_val
       (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
       (inject t)
-  with Anomaly _ -> error "Tried to normalized ill-typed term" 
+  with Anomaly _ -> error "Tried to normalized ill-typed term"
 
 let nf_beta = clos_norm_flags Closure.beta empty_env
 let nf_betaiota = clos_norm_flags Closure.betaiota empty_env