- 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

6 files changed, 135 insertions, 0 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 64445cf5e2..d9d55da7a6 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -172,3 +172,16 @@ let global_reference id =
   let ids =  ids_of_sign hyps in
   DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
 
+let mind_path = function
+  | DOPN(MutInd (sp,0),_) -> sp
+  | DOPN(MutInd (sp,tyi),_) -> 
+      let mib = Global.lookup_mind sp in
+      let mip = mind_nth_type_packet mib tyi in 
+      let (pa,_,k) = repr_path sp in 
+      Names.make_path pa (mip.mind_typename) k 
+  | DOPN(MutConstruct ((sp,tyi),ind),_) -> 
+      let mib = Global.lookup_mind sp in
+      let mip = mind_nth_type_packet mib tyi in 
+      let (pa,_,k) = repr_path sp in 
+      Names.make_path pa (mip.mind_consnames.(ind-1)) k 
+  | _ -> invalid_arg "mind_path"
diff --git a/library/declare.mli b/library/declare.mli
index 41d1e14d3f..2cb576cf1a 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -35,3 +35,5 @@ val declare_mind : mutual_inductive_entry -> unit
   environment of variables. *)
 
 val global_reference : identifier -> constr
+
+val mind_path : constr -> section_path
diff --git a/library/global.ml b/library/global.ml
index 6385e932f4..5e11a36527 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -11,6 +11,8 @@ let global_env = ref empty_environment
 
 let env () = !global_env
 
+let unsafe_env () = unsafe_env_of_env !global_env
+
 let _ = 
   declare_summary "Global environment"
     { freeze_function = (fun () -> !global_env);
diff --git a/library/global.mli b/library/global.mli
index 2e0a541df2..f292766679 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -17,6 +17,7 @@ open Typing
    operating on that global environment. *)
 
 val env : unit -> environment
+val unsafe_env : unit -> unsafe_env
 
 val universes : unit -> universes
 val context : unit -> context
diff --git a/library/redinfo.ml b/library/redinfo.ml
new file mode 100644
index 0000000000..4e6c202156
--- /dev/null
+++ b/library/redinfo.ml
@@ -0,0 +1,98 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Generic
+open Term
+open Constant
+open Reduction
+
+type constant_evaluation = 
+  | Elimination of (int * constr) list * int * bool
+  | NotAnElimination
+
+let eval_table = ref Spmap.empty
+
+(* Check that c is an "elimination constant"
+    [xn:An]..[x1:A1](<P>MutCase (Rel i) of f1..fk end g1 ..gp)
+or  [xn:An]..[x1:A1](Fix(f|t) (Rel i1) ..(Rel ip)) 
+    with i1..ip distinct variables not occuring in t 
+keep relevenant information ([i1,Ai1;..;ip,Aip],n,b)
+with b = true in case of a fixpoint in order to compute 
+an equivalent of Fix(f|t)[xi<-ai] as 
+[yip:Bip]..[yi1:Bi1](F bn..b1) 
+    == [yip:Bip]..[yi1:Bi1](Fix(f|t)[xi<-ai] (Rel 1)..(Rel p))
+with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1] *)
+
+exception Elimconst
+
+let compute_consteval c = 
+  let rec srec n labs c =
+    match whd_betadeltaeta_stack (Global.unsafe_env()) Evd.empty c [] with 
+      | (DOP2(Lambda, t, DLAM(_,g)), []) -> 
+	  srec (n+1) (t::labs) g
+      | (DOPN(Fix (nv,i), bodies), l) -> 
+          if (List.length l) > n then raise Elimconst;
+          let li = 
+            List.map (function
+                        | Rel k ->
+                            if array_for_all (noccurn k) bodies then 
+			      (k, List.nth labs (k-1)) 
+			    else 
+			      raise Elimconst
+                        | _ -> 
+			    raise Elimconst) l
+          in 
+	  if list_distinct (List.map fst li) then 
+	    (li,n,true) 
+          else 
+	    raise Elimconst
+      | (DOPN(MutCase _,_) as mc,lapp) -> 
+          (match destCase mc with
+             | (_,_,Rel _,_) -> ([],n,false)
+             | _ -> raise Elimconst)
+      | _ -> raise Elimconst
+  in
+  try 
+    let (lv,n,b) = srec 0 [] c in 
+    Elimination (lv,n,b) 
+  with Elimconst -> 
+    NotAnElimination
+
+let constant_eval sp =
+  try
+    Spmap.find sp !eval_table
+  with Not_found -> begin
+    let v = 
+      let cb = Global.lookup_constant sp in
+      match cb.const_body with
+	| None -> NotAnElimination
+	| Some c -> compute_consteval c
+    in
+    eval_table := Spmap.add sp v !eval_table;
+    v
+  end
+
+(* Registration as global tables and roolback. *)
+
+type frozen = constant_evaluation Spmap.t
+
+let init () =
+  eval_table := Spmap.empty
+
+let freeze () =
+  !eval_table
+
+let unfreeze ct =
+  eval_table := ct
+
+let _ = 
+  Summary.declare_summary "evaluation"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init }
+
+let rollback f x =
+  let fs = freeze () in
+  try f x with e -> begin unfreeze fs; raise e end
diff --git a/library/redinfo.mli b/library/redinfo.mli
new file mode 100644
index 0000000000..3f71baa982
--- /dev/null
+++ b/library/redinfo.mli
@@ -0,0 +1,19 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+(*i*)
+
+(* Elimination constants. This module implements a table which associates
+   to each constant some reduction informations used by tactics like Simpl. 
+   The following table is mostly used by the module [Tacred] 
+   (section~\refsec{tacred}). *)
+
+type constant_evaluation = 
+  | Elimination of (int * constr) list * int * bool
+  | NotAnElimination
+
+val constant_eval : section_path -> constant_evaluation
+