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

1 files changed, 80 insertions, 0 deletions

diff --git a/intf/pattern.mli b/intf/pattern.mli
new file mode 100644
index 0000000000..63d4ffa7a3
--- /dev/null
+++ b/intf/pattern.mli
@@ -0,0 +1,80 @@
+(************************************************************************)
+(*  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 Names
+open Libnames
+open Term
+open Misctypes
+
+(** {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
+
+(** {5 Patterns} *)
+
+type case_info_pattern =
+    { cip_style : case_style;
+      cip_ind : inductive option;
+      cip_ind_args : int option; (** number of params and 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 (** 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 *)