Extension du case_info : ajout du nombre de vrais args de chaque constr pour la iota-réduction et d'autres informations pour l'affichage dans l'argument du cases

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

2 files changed, 19 insertions, 11 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 72ab35f12..576a92182 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -13,6 +13,13 @@ open Univ
 
 type existential_key = int
 
+type pattern_source = DefaultPat of int | RegularPat
+type case_style = PrintLet | PrintIf | PrintCases
+type case_printing =
+    inductive_path * identifier array * int
+    * case_style option * pattern_source array
+type case_info = int array * case_printing
+
 type 'a oper = 
   (* DOP0 *)
   | Meta of int
@@ -32,8 +39,6 @@ type 'a oper =
       (* an extra slot, for putting in whatever sort of
          operator we need for whatever sort of application *)
 
-and case_info = inductive_path
-
 (* Sorts. *)
 
 type contents = Pos | Null
@@ -458,8 +463,6 @@ let args_of_mind = function
   | DOPN(MutInd _,args) -> args
   | _ -> anomaly "args_of_mind called with bad args"
 
-let ci_of_mind = op_of_mind
-
 (* Destructs a constructor *)
 let destMutConstruct = function
   | DOPN (MutConstruct cstr_sp,l) -> (cstr_sp,l)
@@ -1325,8 +1328,8 @@ module Hoper =
         | Abst sp -> Abst (hsp sp)
         | MutInd (sp,i) -> MutInd (hsp sp, i)
         | MutConstruct ((sp,i),j) -> MutConstruct ((hsp sp,i),j)
-        | MutCase(sp,i) -> MutCase(hsp sp, i)
-        | t -> t 
+        | MutCase ci as t -> t (* TO DO: extract ind_sp *)
+        | t -> t
       let equal o1 o2 =
         match (o1,o2) with
           | (XTRA s1, XTRA s2) -> s1==s2
@@ -1336,10 +1339,10 @@ module Hoper =
           | (MutInd (sp1,i1), MutInd (sp2,i2)) -> sp1==sp2 & i1=i2
           | (MutConstruct((sp1,i1),j1), MutConstruct((sp2,i2),j2)) ->
               sp1==sp2 & i1=i2 & j1=j2
-          | (MutCase(sp1,i1),MutCase(sp2,i2)) -> sp1==sp2 & i1=i2
+          | (MutCase ci1,MutCase ci2) -> ci1==ci2 (* A simplification ?? *)
           | _ -> o1=o2
       let hash = Hashtbl.hash
-    end)
+    end)    
 
 module Hconstr =
   Hashcons.Make(
diff --git a/kernel/term.mli b/kernel/term.mli
index 8e1c40259..d307e8dae 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -13,6 +13,14 @@ open Generic
 
 type existential_key = int
 
+type pattern_source = DefaultPat of int | RegularPat
+type case_style = PrintLet | PrintIf | PrintCases
+type case_printing =
+    inductive_path * identifier array * int
+    * case_style option * pattern_source array
+(* the integer is the number of real args, needed for reduction *)
+type case_info = int array * case_printing
+
 type 'a oper = 
   | Meta of int
   | Sort of 'a
@@ -26,8 +34,6 @@ type 'a oper =
   | CoFix of int
   | XTRA of string
 
-and case_info = inductive_path
-
 (*s The sorts of CCI. *)
 
 type contents = Pos | Null
@@ -300,7 +306,6 @@ val args_of_abst : constr -> constr array
 val destMutInd : constr -> inductive
 val op_of_mind : constr -> inductive_path
 val args_of_mind : constr -> constr array
-val ci_of_mind : constr -> case_info
 
 (* Destructs a constructor *)
 val destMutConstruct : constr -> constructor