Déplacement du type reference dans Term

Découpage de tactics/pattern en proofs/pattern et tactics/hipattern
Renommage des fonctions somatch and co dans Pattern et Tacticals
Divers extensions pour utiliser les constr_pattern


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

2 files changed, 4 insertions, 120 deletions

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 4090e58157..cbafde412f 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -5,7 +5,7 @@
 open Util
 open Names
 open Sign
-open Type_errors
+open Term
 (*i*)
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
@@ -19,22 +19,11 @@ type cases_pattern =
   | 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 '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 * 'ctxt
-  | RMeta of int
-
 (*i Pas beau ce constr dans rawconstr, mais mal compris ce ctxt des ref i*)
 type rawconstr = 
-  | RRef of loc * Term.constr array reference
+  | RRef of loc * constr 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 * 
@@ -73,69 +62,5 @@ let loc_of_rawconstr = function
   | RHole (None) -> dummy_loc
   | RCast (loc,_,_) -> loc
 
-type constr_pattern =
-  | PRef of Term.constr 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 5f67a8a927..6714cb3307 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Names
 open Sign
-open Type_errors
+open Term
 (*i*)
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
@@ -18,21 +18,10 @@ type cases_pattern =
   | 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 '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 * 'ctxt
-  | RMeta of int
-
 type rawconstr = 
-  | RRef of loc * Term.constr array reference
+  | RRef of loc * constr 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 * 
@@ -59,33 +48,3 @@ i*)
 
 val dummy_loc : loc
 val loc_of_rawconstr : rawconstr -> loc
-
-type constr_pattern =
-  | PRef of Term.constr 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
-