From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 pretyping/pattern.mli | 71 ++++++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 56 insertions(+), 15 deletions(-)

(limited to 'pretyping/pattern.mli')

diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 195fecfe..cde6d4dc 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -1,14 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
 (************************************************************************)
 
-(*i $Id: pattern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** This module defines the type of pattern used for pattern-matching
+    terms in tatics *)
 
-(*i*)
 open Pp
 open Names
 open Sign
@@ -16,17 +16,55 @@ open Term
 open Environ
 open Libnames
 open Nametab
-open Rawterm
+open Glob_term
 open Mod_subst
-(*i*)
 
-(* Types of substitutions with or w/o bound variables *)
+(** {5 Maps of pattern variables} *)
+
+(** Type [constr_under_binders] is for representing the term resulting
+    of a matching. Matching can return terms defined in a some context
+    of named binders; in the context, variable names are ordered by
+    (<) and referred to by index in the term Thanks to the canonical
+    ordering, a matching problem like
+
+    [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]]
+
+    will be accepted. Thanks to the reference by index, a matching
+    problem like
+
+    [match ... with [(fun x => ?p)] => [forall x => p]]
+
+    will work even if [x] is also the name of an existing goal
+    variable.
+
+    Note: we do not keep types in the signature. Besides simplicity,
+    the main reason is that it would force to close the signature over
+    binders that occur only in the types of effective binders but not
+    in the term itself (e.g. for a term [f x] with [f:A -> True] and
+    [x:A]).
+
+    On the opposite side, by not keeping the types, we loose
+    opportunity to propagate type informations which otherwise would
+    not be inferable, as e.g. when matching [forall x, x = 0] with
+    pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in
+    expression [forall x, h = x] where nothing tells how the type of x
+    could be inferred. We also loose the ability of typing ltac
+    variables before calling the right-hand-side of ltac matching clauses. *)
 
 type constr_under_binders = identifier list * constr
+
+(** Types of substitutions with or w/o bound variables *)
+
 type patvar_map = (patvar * constr) list
 type extended_patvar_map = (patvar * constr_under_binders) list
 
-(* Patterns *)
+(** {5 Patterns} *)
+
+type case_info_pattern =
+    { cip_style : case_style;
+      cip_ind : inductive option;
+      cip_ind_args : (int * int) option; (** number of params and args *)
+      cip_extensible : bool (** does this match end with _ => _ ? *) }
 
 type constr_pattern =
   | PRef of global_reference
@@ -38,14 +76,17 @@ type constr_pattern =
   | PLambda of name * constr_pattern * constr_pattern
   | PProd of name * constr_pattern * constr_pattern
   | PLetIn of name * constr_pattern * constr_pattern
-  | PSort of rawsort
+  | PSort of glob_sort
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
-  | PCase of (case_style * int array * inductive option * (int * int) option)
-      * constr_pattern * constr_pattern * constr_pattern array
+  | PCase of case_info_pattern * constr_pattern * constr_pattern *
+      (int * int * constr_pattern) list (** index of constructor, nb of args *)
   | PFix of fixpoint
   | PCoFix of cofixpoint
 
+(** 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
@@ -54,28 +95,28 @@ val subst_pattern : substitution -> constr_pattern -> constr_pattern
 
 exception BoundPattern
 
-(* [head_pattern_bound t] extracts the head variable/constant of the
+(** [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
+(** [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
+(** [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_rawconstr l c] translates a term [c] with metavariables into
+(** [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_rawconstr : rawconstr ->
+val pattern_of_glob_constr : glob_constr ->
       patvar list * constr_pattern
 
 val instantiate_pattern :
-- 
cgit v1.2.3