-
Notifications
You must be signed in to change notification settings - Fork 632
/
Pattern.v
160 lines (140 loc) · 6.23 KB
/
Pattern.v
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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import Ltac2.Init.
Require Ltac2.Control.
Ltac2 Type t := pattern.
Ltac2 Type context.
Ltac2 Type match_kind := [
| MatchPattern
| MatchContext
].
Ltac2 @ external empty_context : context :=
"coq-core.plugins.ltac2" "pattern_empty_context".
(** A trivial context only made of the hole. *)
Ltac2 @ external matches : t -> constr -> (ident * constr) list :=
"coq-core.plugins.ltac2" "pattern_matches".
(** If the term matches the pattern, returns the bound variables. If it doesn't,
fail with [Match_failure]. Panics if not focused. *)
Ltac2 @ external matches_subterm : t -> constr -> context * ((ident * constr) list) :=
"coq-core.plugins.ltac2" "pattern_matches_subterm".
(** Returns a stream of results corresponding to all of the subterms of the term
that matches the pattern as in [matches]. The stream is encoded as a
backtracking value whose last exception is [Match_failure]. The additional
value compared to [matches] is the context of the match, to be filled with
the instantiate function. *)
Ltac2 @ external matches_vect : t -> constr -> constr array :=
"coq-core.plugins.ltac2" "pattern_matches_vect".
(** Internal version of [matches] that does not return the identifiers. *)
Ltac2 @ external matches_subterm_vect : t -> constr -> context * constr array :=
"coq-core.plugins.ltac2" "pattern_matches_subterm_vect".
(** Internal version of [matches_subterms] that does not return the identifiers. *)
Ltac2 @ external matches_goal :
bool ->
((match_kind * t) option * (match_kind * t)) list ->
(match_kind * t) ->
ident array * context array * context array * constr array * context :=
"coq-core.plugins.ltac2" "pattern_matches_goal".
(** Given a list of patterns [hpats] for hypotheses and one pattern [cpat] for the
conclusion, [matches_goal rev hpats cpat] produces (a stream of) tuples of:
- An array of idents, whose size is the length of [hpats], corresponding to the
name of matched hypotheses.
- An array of contexts, whose size is the number of [hpats] which have non empty body pattern,
corresponding to the contexts matched for every body pattern.
In case the match kind of a body pattern was [MatchPattern],
the corresponding context is ensured to be empty.
- An array of contexts, whose size is the length of [hpats], corresponding to
the contexts matched for every hypothesis pattern. In case the match kind of
a hypothesis was [MatchPattern], the corresponding context is ensured to be empty.
- An array of terms, whose size is the total number of pattern variables without
duplicates. Terms are ordered by identifier order, e.g. ?a comes before ?b.
- A context corresponding to the conclusion, which is ensured to be empty if
the kind of [cpat] was [MatchPattern].
This produces a backtracking stream of results containing all the possible
result combinations. The order of considered hypotheses is reversed if [rev]
is true.
*)
Ltac2 @ external instantiate : context -> constr -> constr :=
"coq-core.plugins.ltac2" "pattern_instantiate".
(** Fill the hole of a context with the given term. *)
(** Implementation of Ltac matching over terms and goals *)
Ltac2 Type 'a constr_matching := (match_kind * t * (context -> constr array -> 'a)) list.
Ltac2 lazy_match0 t (pats:'a constr_matching) :=
let rec interp m := match m with
| [] => Control.zero Match_failure
| p :: m =>
let next _ := interp m in
let (knd, pat, f) := p in
let p := match knd with
| MatchPattern =>
(fun _ =>
let context := empty_context in
let bind := matches_vect pat t in
fun _ => f context bind)
| MatchContext =>
(fun _ =>
let (context, bind) := matches_subterm_vect pat t in
fun _ => f context bind)
end in
Control.plus p next
end in
Control.once (fun () => interp pats) ().
Ltac2 multi_match0 t (pats:'a constr_matching) :=
let rec interp e m := match m with
| [] => Control.zero e
| p :: m =>
let next e := interp e m in
let (knd, pat, f) := p in
let p := match knd with
| MatchPattern =>
(fun _ =>
let context := empty_context in
let bind := matches_vect pat t in
f context bind)
| MatchContext =>
(fun _ =>
let (context, bind) := matches_subterm_vect pat t in
f context bind)
end in
Control.plus p next
end in
interp Match_failure pats.
Ltac2 one_match0 t m := Control.once (fun _ => multi_match0 t m).
Ltac2 Type 'a goal_matching :=
((((match_kind * t) option * (match_kind * t)) list * (match_kind * t)) *
(ident array -> context array -> context array -> constr array -> context -> 'a)) list.
Ltac2 lazy_goal_match0 rev (pats:'a goal_matching) :=
let rec interp m := match m with
| [] => Control.zero Match_failure
| p :: m =>
let next _ := interp m in
let (pat, f) := p in
let (phyps, pconcl) := pat in
let cur _ :=
let (hids, hbctx, hctx, subst, cctx) := matches_goal rev phyps pconcl in
fun _ => f hids hbctx hctx subst cctx
in
Control.plus cur next
end in
Control.once (fun () => interp pats) ().
Ltac2 multi_goal_match0 rev (pats:'a goal_matching) :=
let rec interp e m := match m with
| [] => Control.zero e
| p :: m =>
let next e := interp e m in
let (pat, f) := p in
let (phyps, pconcl) := pat in
let cur _ :=
let (hids, hbctx, hctx, subst, cctx) := matches_goal rev phyps pconcl in
f hids hbctx hctx subst cctx
in
Control.plus cur next
end in
interp Match_failure pats.
Ltac2 one_goal_match0 rev pats := Control.once (fun _ => multi_goal_match0 rev pats).