Pattern as a mli-only file, operations in Patternops

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

18 files changed, 79 insertions, 93 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index c3b5742ac..a5e0d27be 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -86,7 +86,7 @@ Recordops
 Evarconv
 Arguments_renaming
 Typing
-Pattern
+Patternops
 Matching
 Tacred
 Classops
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 91e0cf6a1..5a1dea89e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -18,6 +18,7 @@ open Impargs
 open Glob_term
 open Glob_ops
 open Pattern
+open Patternops
 open Pretyping
 open Cases
 open Constrexpr
diff --git a/pretyping/pattern.mli b/intf/pattern.mli
index f9c2358b7..63d4ffa7a 100644
--- a/pretyping/pattern.mli
+++ b/intf/pattern.mli
@@ -6,18 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** This module defines the type of pattern used for pattern-matching
-    terms in tatics *)
-
-open Pp
 open Names
-open Sign
-open Term
-open Environ
 open Libnames
-open Nametab
-open Glob_term
-open Mod_subst
+open Term
 open Misctypes
 
 (** {5 Maps of pattern variables} *)
@@ -87,41 +78,3 @@ type constr_pattern =
 
 (** Nota : in a [PCase], the array of branches might be shorter than
     expected, denoting the use of a final "_ => _" branch *)
-
-(** {5 Functions on patterns} *)
-
-val occur_meta_pattern : constr_pattern -> bool
-
-val subst_pattern : substitution -> constr_pattern -> constr_pattern
-
-exception BoundPattern
-
-(** [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 *)
-
-val head_pattern_bound : constr_pattern -> global_reference
-
-(** [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 -> global_reference
-
-(** [pattern_of_constr c] translates a term [c] with metavariables into
-   a pattern; currently, no destructor (Cases, Fix, Cofix) and no
-   existential variable are allowed in [c] *)
-
-val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern
-
-(** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
-   a pattern; variables bound in [l] are replaced by the pattern to which they
-    are bound *)
-
-val pattern_of_glob_constr : glob_constr ->
-      patvar list * constr_pattern
-
-val instantiate_pattern :
-  Evd.evar_map -> (identifier * (identifier list * constr)) list ->
-  constr_pattern -> constr_pattern
-
-val lift_pattern : int -> constr_pattern -> constr_pattern
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index c2dce0231..7ab65b443 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -65,7 +65,6 @@ Inductiveops
 Miscops
 Glob_ops
 Detyping
-Pattern
 Topconstr
 Genarg
 Ppextend
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 543240a82..d78b6c8c0 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -31,7 +31,7 @@ EXTEND
   GLOBAL: expr;
   expr:
     [ [ "PATTERN"; "["; c = constr; "]" ->
-      <:expr< snd (Pattern.pattern_of_glob_constr $c$) >> ] ]
+      <:expr< snd (Patternops.pattern_of_glob_constr $c$) >> ] ]
   ;
   sort:
     [ [ "Set"  -> GSet
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index fe025e6da..e8ee433c6 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -107,6 +107,7 @@ open Util
 open Names
 open Term
 open Pattern
+open Patternops
 open Matching
 open Tacmach
 open Tactics
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 6be95cd82..554face37 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -20,6 +20,7 @@ open Glob_term
 open Sign
 open Environ
 open Pattern
+open Patternops
 open Misctypes
 (*i*)
 
diff --git a/pretyping/pattern.ml b/pretyping/patternops.ml
index 08e5ac75c..244d03021 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/patternops.ml
@@ -20,39 +20,8 @@ open Pp
 open Mod_subst
 open Misctypes
 open Decl_kinds
-
-(* Metavariables *)
-
-type constr_under_binders = identifier list * constr
-
-type patvar_map = (patvar * constr) list
-type extended_patvar_map = (patvar * constr_under_binders) list
-
-(* Patterns *)
-
-type case_info_pattern =
-    { cip_style : case_style;
-      cip_ind : inductive option;
-      cip_ind_args : int option; (** number of args *)
-      cip_extensible : bool (** does this match end with _ => _ ? *) }
-
-type constr_pattern =
-  | PRef of global_reference
-  | PVar of identifier
-  | PEvar of existential_key * constr_pattern array
-  | PRel of int
-  | PApp of constr_pattern * constr_pattern array
-  | PSoApp of patvar * constr_pattern list
-  | PLambda of name * constr_pattern * constr_pattern
-  | PProd of name * constr_pattern * constr_pattern
-  | PLetIn of name * constr_pattern * constr_pattern
-  | PSort of glob_sort
-  | PMeta of patvar option
-  | PIf of constr_pattern * constr_pattern * constr_pattern
-  | PCase of case_info_pattern * constr_pattern * constr_pattern *
-      (int * int * constr_pattern) list (** constructor index, nb of args *)
-  | PFix of fixpoint
-  | PCoFix of cofixpoint
+open Pattern
+open Evd
 
 let rec occur_meta_pattern = function
   | PApp (f,args) ->
@@ -94,8 +63,6 @@ let head_of_constr_reference c = match kind_of_term c with
   | Var id -> VarRef id
   | _ -> anomaly "Not a rigid reference"
 
-open Evd
-
 let pattern_of_constr sigma t =
   let ctx = ref [] in
   let rec pattern_of_constr t =
@@ -111,7 +78,7 @@ let pattern_of_constr sigma t =
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
     | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
     | App (f,a) ->
-        (match 
+        (match
           match kind_of_term f with
             Evar (evk,args as ev) ->
               (match snd (Evd.evar_source evk sigma) with
@@ -377,5 +344,5 @@ and pats_of_glob_branches loc metas vars ind brs =
 
 let pattern_of_glob_constr c =
   let metas = ref [] in
-  let p = pat_of_raw metas [] c in	
+  let p = pat_of_raw metas [] c in
   (!metas,p)
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
new file mode 100644
index 000000000..74e5a81ae
--- /dev/null
+++ b/pretyping/patternops.mli
@@ -0,0 +1,57 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Names
+open Sign
+open Term
+open Environ
+open Libnames
+open Nametab
+open Glob_term
+open Mod_subst
+open Misctypes
+open Pattern
+
+(** {5 Functions on patterns} *)
+
+val occur_meta_pattern : constr_pattern -> bool
+
+val subst_pattern : substitution -> constr_pattern -> constr_pattern
+
+exception BoundPattern
+
+(** [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 *)
+
+val head_pattern_bound : constr_pattern -> global_reference
+
+(** [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 -> global_reference
+
+(** [pattern_of_constr c] translates a term [c] with metavariables into
+   a pattern; currently, no destructor (Cases, Fix, Cofix) and no
+   existential variable are allowed in [c] *)
+
+val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern
+
+(** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
+   a pattern; variables bound in [l] are replaced by the pattern to which they
+    are bound *)
+
+val pattern_of_glob_constr : glob_constr ->
+      patvar list * constr_pattern
+
+val instantiate_pattern :
+  Evd.evar_map -> (identifier * (identifier list * constr)) list ->
+  constr_pattern -> constr_pattern
+
+val lift_pattern : int -> constr_pattern -> constr_pattern
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index fca2d714f..2d25b1413 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -17,7 +17,7 @@ Typing
 Miscops
 Glob_ops
 Redops
-Pattern
+Patternops
 Matching
 Tacred
 Typeclasses_errors
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 6ff469012..05136d25d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -24,6 +24,7 @@ open Reductionops
 open Cbv
 open Glob_term
 open Pattern
+open Patternops
 open Matching
 open Locus
 
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 12aec9142..d0782e970 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -223,7 +223,7 @@ let subst_red_expr subs e =
   subst_gen_red_expr
     (Mod_subst.subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
-    (Pattern.subst_pattern subs)
+    (Patternops.subst_pattern subs)
     e
 
 let inReduction : bool * string * red_expr -> obj =
diff --git a/tactics/auto.ml b/tactics/auto.ml
index f580f839c..158221d79 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -22,6 +22,7 @@ open Evd
 open Reduction
 open Typing
 open Pattern
+open Patternops
 open Matching
 open Tacmach
 open Proof_type
@@ -485,7 +486,7 @@ let make_exact_entry sigma pri ?(name=PathAny) (c,cty) =
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = snd (Pattern.pattern_of_constr sigma cty) in
+	let pat = snd (Patternops.pattern_of_constr sigma cty) in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -502,7 +503,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri ?(name=PathAny) (c,cty)
     | Prod _ ->
         let ce = mk_clenv_from dummy_goal (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = snd (Pattern.pattern_of_constr sigma c') in
+	let pat = snd (Patternops.pattern_of_constr sigma c') in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
@@ -576,7 +577,7 @@ let make_trivial env sigma ?(name=PathAny) c =
   let hd = head_of_constr_reference (fst (head_constr t)) in
   let ce = mk_clenv_from dummy_goal (c,t) in
   (Some hd, { pri=1;
-              pat = Some (snd (Pattern.pattern_of_constr sigma (clenv_type ce)));
+              pat = Some (snd (Patternops.pattern_of_constr sigma (clenv_type ce)));
 	      name = name;
               code=Res_pf_THEN_trivial_fail(c,t) })
   
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index cafe17ad9..bfebf7810 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -24,6 +24,7 @@ open Tacmach
 open Evar_refiner
 open Tactics
 open Pattern
+open Patternops
 open Clenv
 open Auto
 open Glob_term
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index e9602762d..fb692873e 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -24,6 +24,7 @@ open Tacmach
 open Evar_refiner
 open Tactics
 open Pattern
+open Patternops
 open Clenv
 open Auto
 open Genredexpr
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 4a0d143dc..75f6bdb7c 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -25,6 +25,7 @@ open Tacmach
 open Evar_refiner
 open Tactics
 open Pattern
+open Patternops
 open Clenv
 open Auto
 open Glob_term
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 88767a363..9b4df0ad5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -13,6 +13,7 @@ open Declarations
 open Entries
 open Libobject
 open Pattern
+open Patternops
 open Matching
 open Pp
 open Genredexpr
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 5f6e5580e..0e7009113 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -12,6 +12,7 @@ open Names
 open Nameops
 open Term
 open Pattern
+open Patternops
 open Glob_term
 open Libnames
 open Nametab