1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
open Globnames
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 = Id.t list * EConstr.constr
(** Types of substitutions with or w/o bound variables *)
type patvar_map = EConstr.constr Id.Map.t
type extended_patvar_map = constr_under_binders Id.Map.t
(** {5 Patterns} *)
type case_info_pattern =
{ cip_style : case_style;
cip_ind : inductive option;
cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *)
cip_extensible : bool (** does this match end with _ => _ ? *) }
type constr_pattern =
| PRef of global_reference
| PVar of Id.t
| PEvar of existential_key * constr_pattern array
| PRel of int
| PApp of constr_pattern * constr_pattern array
| PSoApp of patvar * constr_pattern list
| PProj of projection * constr_pattern
| PLambda of Name.t * constr_pattern * constr_pattern
| PProd of Name.t * constr_pattern * constr_pattern
| PLetIn of Name.t * constr_pattern * constr_pattern option * 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 * bool list * 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 *)
|
