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

13 files changed, 54 insertions, 144 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index f3afa5e0ae..cfb66fc8b3 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -73,6 +73,20 @@ val incast_type : typed_type -> constr
 
 val outcast_type : constr -> typed_type
 
+(**********************************************************************)
+type binder_kind = BProd | BLambda
+
+type fix_kind = RFix of int array * int | RCofix of int
+
+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
+
 (*s Functions for dealing with constr terms.
   The following functions are intended to simplify and to uniform the 
   manipulation of terms. Some of these functions may be overlapped with
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 70e7ab7a30..1383dc655f 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -8,6 +8,7 @@ open Sign
 open Evd
 open Environ
 open Rawterm
+open Pattern
 (*i*)
 
 (* Translation from AST to terms. *)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 1cc5ceca55..4ab8b33ac2 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -49,7 +49,7 @@ GEXTEND Gram
             <:ast< (PRODLIST $c [$id1][$id2]($SLAM $idl $body)) >>
       | "("; lc1 = lconstr; ")" -> lc1
       | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" ->
-          <:ast< (XTRA"$SOAPP" $lc1 ($LIST $cl)) >>
+          <:ast< (SOAPP $lc1 ($LIST $cl)) >>
       | IDENT "Fix"; id = ident; "{"; fbinders = fixbinders; "}" ->
           <:ast< (FIX $id ($LIST $fbinders)) >>
       | IDENT "CoFix"; id = ident; "{"; fbinders = cofixbinders; "}" ->
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 40a1bdad3b..d6e785c8f4 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -6,12 +6,11 @@ open Pp
 open Names
 open Term
 open Sign
+open Rawterm
+open Pattern
 (*i*)
 
 (* These are the entry points for printing terms, context, tac, ... *)
-val gencompr  : path_kind -> Coqast.t -> std_ppcmds
-val gentermpr : path_kind -> 'a assumptions -> constr -> std_ppcmds
-val gentermpr_at_top : path_kind -> 'a assumptions -> constr -> std_ppcmds
 val gentacpr  : Coqast.t -> std_ppcmds
 
 val prterm_env      : 'a assumptions -> constr -> std_ppcmds
@@ -19,19 +18,17 @@ val prterm_env_at_top : 'a assumptions -> constr -> std_ppcmds
 val prterm          : constr -> std_ppcmds
 val prtype_env      : 'a assumptions -> typed_type -> std_ppcmds
 val prtype          : typed_type -> std_ppcmds
-val fprterm_env     : 'a assumptions -> constr -> std_ppcmds
-val fprterm         : constr -> std_ppcmds
-val fprtype_env     : 'a assumptions -> typed_type -> std_ppcmds
-val fprtype         : typed_type -> std_ppcmds
 
-val prrawterm       : Rawterm.rawconstr -> std_ppcmds
-val prpattern       : Rawterm.cases_pattern -> std_ppcmds
+val pr_rawterm       : Rawterm.rawconstr -> std_ppcmds
+val pr_cases_pattern : Rawterm.cases_pattern -> std_ppcmds
 
 val pr_constant     : constant -> std_ppcmds
 val pr_existential  : existential -> std_ppcmds
 val pr_constructor  : constructor -> std_ppcmds
 val pr_inductive    : inductive -> std_ppcmds
-val pr_ref_label    : Rawterm.constr_label -> std_ppcmds
+val pr_ref_label    : constr_label -> std_ppcmds
+val pr_pattern      : constr_pattern -> std_ppcmds
+val pr_pattern_env  : 'a assumptions -> constr_pattern -> std_ppcmds
 
 val pr_ne_env       : std_ppcmds -> path_kind -> context -> std_ppcmds
 
@@ -41,6 +38,12 @@ val pr_env_opt      : context -> std_ppcmds
 val emacs_str       : string -> string
 
 (* For compatibility *)
-val fterm0          : 'a assumptions -> constr -> std_ppcmds
 val term0           : 'a assumptions -> constr -> std_ppcmds
 
+val fprterm_env     : 'a assumptions -> constr -> std_ppcmds
+val fprterm         : constr -> std_ppcmds
+val fprtype_env     : 'a assumptions -> typed_type -> std_ppcmds
+val fprtype         : typed_type -> std_ppcmds
+
+(* For compatibility *)
+val fterm0          : 'a assumptions -> constr -> std_ppcmds
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 516856bcd9..064dc8c25b 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -6,13 +6,20 @@ open Names
 open Term
 open Sign
 open Rawterm
+open Pattern
 (*i*)
 
-(* Translation of pattern, rawterm and term into syntax trees for printing *)
+(* Translation of pattern, cases pattern, rawterm and term into syntax
+   trees for printing *)
 
-val ast_of_pattern : cases_pattern -> Coqast.t
+val ast_of_cases_pattern : cases_pattern -> Coqast.t
 val ast_of_rawconstr : rawconstr -> Coqast.t
-val bdize : bool -> unit assumptions -> constr -> Coqast.t
+val ast_of_pattern : unit assumptions -> constr_pattern -> Coqast.t
+
+(* If [b=true] in [ast_of_constr b env c] then the variables in the first 
+   level of quantification clashing with the variables in [env] are renamed *)
+
+val ast_of_constr : bool -> unit assumptions -> constr -> Coqast.t
 
 (*i C'est bdize qui sait maintenant s'il faut afficher les casts ou pas
 val bdize_no_casts : bool -> unit assumptions -> constr -> Coqast.t
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
-
diff --git a/tactics/auto.mli b/tactics/auto.mli
index fce449c027..d97e82df63 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -9,6 +9,7 @@ open Sign
 open Proof_trees
 open Tacmach
 open Clenv
+open Pattern
 (*i*)
   
 type auto_tactic = 
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 2d0b2f1065..d673b9316f 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Generic
 open Term
-open Rawterm
+open Pattern
 (*i*)
 
 (* Discrimination nets with bounded depth. *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index ec18aa9fe4..8dc9450d1a 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -9,6 +9,7 @@ open Evd
 open Environ
 open Proof_trees
 open Tacmach
+open Hipattern
 open Pattern
 open Wcclausenv
 open Tacticals
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 5275805236..5100d6c668 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Generic
 open Term
-open Rawterm
+open Pattern
 (*i*)
 
 (* Named, bounded-depth, term-discrimination nets. *)
@@ -27,5 +27,5 @@ val dnet_depth : int ref
 val freeze : ('na,'a) t -> ('na,'a) frozen_t
 val unfreeze : ('na,'a) frozen_t -> ('na,'a) t -> unit
 val empty : ('na,'a) t -> unit
-val to2lists : ('na,'a) t -> ('na * (Rawterm.constr_pattern * 'a)) list * 
-                             (Rawterm.constr_label option * 'a Btermdn.t) list
+val to2lists : ('na,'a) t -> ('na * (constr_pattern * 'a)) list * 
+                             (constr_label option * 'a Btermdn.t) list
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index f863bad68a..ac118b6d1b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -52,9 +52,8 @@ val clause_type : clause -> goal sigma -> constr
 val matches      : goal sigma -> constr -> marked_term -> bool
 val dest_match   : goal sigma -> constr -> marked_term -> constr list
 *)
-(* The second argument is the pattern *)
-val matches      : goal sigma -> constr -> marked_pattern -> bool
-val dest_match   : goal sigma -> constr -> constr -> constr list
+val gl_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list
+val gl_is_matching : goal sigma -> constr_pattern -> constr -> bool
 
 val allHyps    : goal sigma -> clause list
 val afterHyp   : identifier -> goal sigma -> clause list
@@ -83,7 +82,7 @@ val ifOnClause     :
    [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
    right values to build a tactic *)
 
-val conclPattern : constr -> Rawterm.constr_pattern -> Coqast.t -> tactic
+val conclPattern : constr -> constr_pattern -> Coqast.t -> tactic
 
 (*s Elimination tacticals. *)
 
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 1b8a132abf..10726df139 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Generic
 open Term
-open Rawterm
+open Pattern
 (*i*)
   
 (* Discrimination nets of terms. *)