- module Redinfo dans library/ pour les constantes d'élimination

 - module Tacred : fonctions de reductions utilisees dans les tactiques


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

2 files changed, 30 insertions, 84 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 7119729c7d..93243a4404 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -508,10 +508,9 @@ type 'a miota_args = {
   mcargs  : 'a list;    (* the constructor's arguments *)
   mlf     : 'a array }  (* the branch code vector *)
 		       
-let reducible_mind_case c =
-  match c with 
-    | DOPN(MutConstruct _,_) | DOPN(CoFix _,_) -> true
-    | _  -> false
+let reducible_mind_case = function
+  | DOPN(MutConstruct _,_) | DOPN(CoFix _,_) -> true
+  | _  -> false
 
 let contract_cofix = function
   | DOPN(CoFix(bodynum),bodyvect) ->
@@ -536,10 +535,8 @@ let reduce_mind_case env mia =
     | _ -> 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})] *)
 
-   Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})]
-
- *)
 let contract_fix = function 
   | DOPN(Fix(recindices,bodynum),bodyvect) -> 
       let nbodies = Array.length recindices in
@@ -552,9 +549,12 @@ let fix_recarg fix stack =
     | DOPN(Fix(recindices,bodynum),_) ->
     	if 0 <= bodynum & bodynum < Array.length recindices then
 	  let recargnum = Array.get recindices bodynum in
-          (try Some(recargnum, List.nth stack recargnum)
-           with Failure "nth" | Invalid_argument "List.nth" -> None)
-    	else None
+          (try 
+	     Some (recargnum, List.nth stack recargnum)
+           with Failure "nth" | Invalid_argument "List.nth" -> 
+	     None)
+    	else 
+	  None
     | _ -> assert false
 
 let reduce_fix whfun fix stack =
@@ -1029,79 +1029,6 @@ let decomp_n_prod env sigma n =
   in 
   decrec n []
 
-(* Special iota reduction... *)
-
-let contract_cofix_use_function f cofix =
-  match cofix with 
-    | DOPN(CoFix(bodynum),bodyvect) ->
-  	let nbodies =  (Array.length bodyvect) -1 in
-  	let make_Fi j = DOPN(CoFix(j),bodyvect) in
-  	let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
-  	sAPPViList bodynum (array_last bodyvect) lbodies
-    | _ -> assert false
-
-let reduce_mind_case_use_function env f mia =
-  match mia.mconstr with 
-    | DOPN(MutConstruct((indsp,tyindx),i),_) ->
-	let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in
-	let nparams = mind_nparams env ind in
-	let real_cargs = snd(list_chop nparams mia.mcargs) in
-	applist (mia.mlf.(i-1),real_cargs)
-    | DOPN(CoFix _,_) as cofix ->
-	let cofix_def = contract_cofix_use_function f cofix in
-	mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
-    | _ -> assert false
-	  
-let special_red_case env whfun p c ci lf  =
-  let rec redrec c l = 
-    let (constr,cargs) = whfun c l in 
-    match constr with 
-      | DOPN(Const _,_) as g -> 
-          if evaluable_constant env g then
-            let gvalue = constant_value env g in
-            if reducible_mind_case  gvalue then
-              reduce_mind_case_use_function env g
-                {mP=p; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf}
-            else 
-	      redrec gvalue cargs
-          else 
-	    raise Redelimination
-      | _ ->
-          if reducible_mind_case constr then
-            reduce_mind_case env
-              {mP=p; mconstr=constr; mcargs=cargs; mci=ci; mlf=lf}
-          else 
-	    raise Redelimination
-  in 
-  redrec c []
-
-
-(* F is convertible to DOPN(Fix(recindices,bodynum),bodyvect) make 
-the reduction using this extra information *)
-
-let contract_fix_use_function f fix =
-  match fix with 
-    | DOPN(Fix(recindices,bodynum),bodyvect) ->
-  	let nbodies = Array.length recindices in
-  	let make_Fi j = DOPN(Fix(recindices,j),bodyvect) in
-  	let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
-	  sAPPViList bodynum (array_last bodyvect) lbodies
-    | _ -> assert false
-
-
-let reduce_fix_use_function f whfun fix stack =
-  match fix with 
-    | DOPN (Fix(recindices,bodynum),bodyvect) ->
-	(match fix_recarg fix stack with
-           | None -> (false,(fix,stack))
-	   | Some (recargnum,recarg) ->
-               let (recarg'hd,_ as recarg')= whfun recarg [] in
-               let stack' = list_assign stack recargnum (applist recarg') in
-	       (match recarg'hd with
-                  | DOPN(MutConstruct _,_) ->
-		      (true,(contract_fix_use_function f fix,stack'))
-		  | _ -> (false,(fix,stack'))))
-    | _ -> assert false
 
 
 (* Check that c is an "elimination constant"
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 421aa9aaf2..585a573449 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -25,11 +25,14 @@ type 'a stack_reduction_function =
 val whd_stack : 'a stack_reduction_function
 
 (*s Reduction Function Operators *)
+
 val under_casts : 'a reduction_function -> 'a reduction_function
 val strong : 'a reduction_function -> 'a reduction_function
 val strong_prodspine : 'a reduction_function -> 'a reduction_function
 val stack_reduction_of_reduction : 
   'a reduction_function -> 'a stack_reduction_function
+val stacklam : (constr -> constr list -> 'a) -> constr list -> constr 
+  -> constr list -> 'a 
 
 (*s Generic Optimized Reduction Functions using Closures *)
 
@@ -57,6 +60,7 @@ val whd_betadeltaiota_stack : 'a stack_reduction_function
 
 
 (*s Head normal forms *)
+
 val whd_const_stack : section_path list -> 'a stack_reduction_function
 val whd_const : section_path list -> 'a reduction_function
 val whd_delta_stack : 'a stack_reduction_function
@@ -67,12 +71,13 @@ val whd_betadeltat_stack : 'a stack_reduction_function
 val whd_betadeltat : 'a reduction_function
 val whd_betadeltatiota_stack : 'a stack_reduction_function
 val whd_betadeltatiota : 'a reduction_function
+val whd_betadeltaeta_stack : 'a stack_reduction_function
+val whd_betadeltaeta : 'a reduction_function
 val whd_betadeltaiotaeta_stack : 'a stack_reduction_function
 val whd_betadeltaiotaeta : 'a reduction_function
 
 val beta_applist : (constr * constr list) -> constr
 
-
 val hnf_prod_app : 
   unsafe_env -> 'a evar_map -> string -> constr -> constr -> constr
 val hnf_prod_appvect : 
@@ -91,6 +96,16 @@ val decomp_prod : unsafe_env -> 'a evar_map -> constr -> int * constr
 val decomp_n_prod : 
   unsafe_env -> 'a evar_map -> int -> constr -> ((name * constr) list) * constr
 
+type 'a miota_args = {
+  mP      : constr;     (* the result type *)
+  mconstr : constr;     (* the constructor *)
+  mci     : case_info;  (* special info to re-build pattern *)
+  mcargs  : 'a list;    (* the constructor's arguments *)
+  mlf     : 'a array }  (* the branch code vector *)
+
+val reducible_mind_case : constr -> bool
+val reduce_mind_case : unsafe_env -> constr miota_args -> constr
+
 val is_arity : unsafe_env -> 'a evar_map -> constr -> bool
 val is_info_arity : unsafe_env -> 'a evar_map -> constr -> bool
 val is_info_sort : unsafe_env -> 'a evar_map -> constr -> bool
@@ -111,6 +126,9 @@ val subst_term_occ : int list -> constr -> constr -> constr
 val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
 val compute : 'a reduction_function
 
+val fix_recarg : constr -> 'a list -> (int * 'a) option
+val reduce_fix : (constr -> 'a list -> constr * constr list) -> constr ->
+  constr list -> bool * (constr * constr list)
 
 (*s Conversion Functions (uses closures, lazy strategy) *)
 
@@ -185,4 +203,5 @@ val minductype_spec : unsafe_env -> 'a evar_map -> constr -> constr
 val mrectype_spec : unsafe_env -> 'a evar_map -> constr -> constr
 
 (* Special function, which keep the key casts under Fix and MutCase. *)
+
 val strip_all_casts : constr -> constr