Introduction d'un type constr_pattern pour les différents filtrages

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

3 files changed, 119 insertions, 19 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 844e364316..737f6a2e1a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -117,7 +117,7 @@ type rhs =
 
 type equation =
     { dependencies : constr lifted list;
-      patterns     : pattern list; 
+      patterns     : cases_pattern list; 
       rhs          : rhs;
       tag          : pattern_source }
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index ec43265658..ab3075f453 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -2,6 +2,7 @@
 (* $Id$ *)
 
 (*i*)
+open Util
 open Names
 open Sign
 open Type_errors
@@ -13,29 +14,30 @@ type loc = int * int
 
 (* locs here refers to the ident's location, not whole pat *)
 (* the last argument of PatCstr is a possible alias ident for the pattern *)
-type pattern =
+type cases_pattern =
   | PatVar of loc * name
-  | PatCstr of loc * (constructor_path * identifier list) * pattern list * name
+  | PatCstr of
+      loc * (constructor_path * identifier list) * cases_pattern list * name
 
 type binder_kind = BProd | BLambda
 type fix_kind = RFix of int array * int | RCofix of int
 type rawsort = RProp of Term.contents | RType
 
-type reference =
-  | RConst of section_path * identifier list
-  | RInd of inductive_path * identifier list
-  | RConstruct of constructor_path * identifier list
+type 'ctxt reference =
+  | RConst of section_path * 'ctxt
+  | RInd of inductive_path * 'ctxt
+  | RConstruct of constructor_path * 'ctxt
   | RAbst of section_path
   | RVar of identifier
-  | REVar of int * identifier list
+  | REVar of int * 'ctxt
   | RMeta of int
 
 type rawconstr = 
-  | RRef of loc * reference
+  | RRef of loc * rawconstr array reference
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr
   | RCases of loc * Term.case_style * rawconstr option * rawconstr list * 
-      (identifier list * pattern list * rawconstr) list
+      (identifier list * cases_pattern list * rawconstr) list
   | ROldCase of loc * bool * rawconstr option * rawconstr * 
       rawconstr array
   | RRec of loc * fix_kind * identifier array * 
@@ -69,3 +71,70 @@ let loc_of_rawconstr = function
   | RHole (Some loc) -> loc
   | RHole (None) -> dummy_loc
   | RCast (loc,_,_) -> loc
+
+type constr_pattern =
+  | PRef of constr_pattern array reference
+  | PRel of int
+  | PApp of constr_pattern * constr_pattern array
+  | PSoApp of int * int list
+  | PBinder of binder_kind * name * constr_pattern * constr_pattern
+  | PSort of rawsort
+  | PMeta of int
+(*
+  | PCast of loc * constr_pattern * constr_pattern
+  | PCases of loc * Term.case_style * constr_pattern option * constr_pattern list * 
+      (identifier list * pattern list * constr_pattern) list
+  | POldCase of loc * bool * constr_pattern option * constr_pattern * 
+      constr_pattern array
+  | Pec of loc * fix_kind * identifier array * 
+      constr_pattern array * constr_pattern array
+*)
+
+let rec occur_meta_pattern = function
+  | PApp (f,args) ->
+      (occur_meta_pattern f) or (array_exists occur_meta_pattern args)
+  | PBinder(_,na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
+  | PMeta _ | PSoApp _ -> true
+  | PRel _ | PSort _   -> false
+
+  (* On suppose que les ctxt des cstes ne contient pas de meta *)
+  | PRef _             -> false
+
+type constr_label =
+  | ConstNode of section_path
+  | IndNode of inductive_path
+  | CstrNode of constructor_path
+  | VarNode of identifier
+(*
+  | ... 
+*)
+
+exception BoundPattern;;
+
+let label_of_ref = function
+  | RConst (sp,_)     -> ConstNode sp
+  | RInd (sp,_)       -> IndNode sp
+  | RConstruct (sp,_) -> CstrNode sp
+  | RVar id           -> VarNode id
+  | RAbst _           -> error "Obsolète"
+  | REVar _ | RMeta _ -> raise BoundPattern
+
+let rec head_pattern_bound t =
+  match t with
+    | PBinder (BProd,_,_,b) -> head_pattern_bound b 
+    | PApp (f,args)         -> head_pattern_bound f
+    | PRef r                -> label_of_ref r
+    | PRel _ | PMeta _ | PSoApp _  | PSort _ -> raise BoundPattern
+    | PBinder(BLambda,_,_,_) -> anomaly "head_pattern_bound: not a type"
+
+open Generic
+open Term
+
+let head_of_constr_reference = function
+  | DOPN (Const sp,_) -> ConstNode sp
+  | DOPN (MutConstruct sp,_) -> CstrNode sp
+  | DOPN (MutInd sp,_) -> IndNode sp
+  | VAR id -> VarNode id
+  | _ -> anomaly "Not a rigid reference"
+
+
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index c31691046d..f78520a16f 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -13,29 +13,30 @@ type loc = int * int
 
 (* locs here refers to the ident's location, not whole pat *)
 (* the last argument of PatCstr is a possible alias ident for the pattern *)
-type pattern =
+type cases_pattern =
   | PatVar of loc * name
-  | PatCstr of loc * (constructor_path * identifier list) * pattern list * name
+  | PatCstr of
+      loc * (constructor_path * identifier list) * cases_pattern list * name
 
 type binder_kind = BProd | BLambda
 type fix_kind = RFix of int array * int | RCofix of int
 type rawsort = RProp of Term.contents | RType
 
-type reference =
-  | RConst of section_path * identifier list
-  | RInd of inductive_path * identifier list
-  | RConstruct of constructor_path * identifier list
+type 'ctxt reference =
+  | RConst of section_path * 'ctxt
+  | RInd of inductive_path * 'ctxt
+  | RConstruct of constructor_path * 'ctxt
   | RAbst of section_path
   | RVar of identifier
-  | REVar of int * identifier list
+  | REVar of int * 'ctxt
   | RMeta of int
 
 type rawconstr = 
-  | RRef of loc * reference
+  | RRef of loc * rawconstr array reference
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr
   | RCases of loc * Term.case_style * rawconstr option * rawconstr list * 
-      (identifier list * pattern list * rawconstr) list
+      (identifier list * cases_pattern list * rawconstr) list
   | ROldCase of loc * bool * rawconstr option * rawconstr * 
       rawconstr array
   | RRec of loc * fix_kind * identifier array * 
@@ -58,3 +59,33 @@ i*)
 
 val dummy_loc : loc
 val loc_of_rawconstr : rawconstr -> loc
+
+type constr_pattern =
+  | PRef of constr_pattern array reference
+  | PRel of int
+  | PApp of constr_pattern * constr_pattern array
+  | PSoApp of int * int list
+  | PBinder of binder_kind * name * constr_pattern * constr_pattern
+  | PSort of rawsort
+  | PMeta of int
+
+val occur_meta_pattern : constr_pattern -> bool
+
+type constr_label =
+  | ConstNode of section_path
+  | IndNode of inductive_path
+  | CstrNode of constructor_path
+  | VarNode of identifier
+
+(* [head_pattern_bound t] extracts the head variable/constant of the
+   type [t] or raises [BoundPattern] (even if a sort); it raises an anomaly
+   if [t] is an abstraction *)
+
+exception BoundPattern
+val head_pattern_bound : constr_pattern -> constr_label
+
+(* [head_of_constr_reference c] assumes [r] denotes a reference and
+   returns its label; raises an anomaly otherwise *)
+
+val head_of_constr_reference : Term.constr -> constr_label
+