blob: 7022949ab6af317eb24460ccc210117ad33c09a7 (
plain)
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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
{
open Ltac_plugin
open Pcoq.Constr
open Ssrmatching
open Ssrmatching.Internal
(* Defining grammar rules with "xx" in it automatically declares keywords too,
* we thus save the lexer to restore it at the end of the file *)
let frozen_lexer = CLexer.get_keyword_state () ;;
}
DECLARE PLUGIN "ssrmatching_plugin"
{
let pr_rpattern _ _ _ = pr_rpattern
}
ARGUMENT EXTEND rpattern
TYPED AS rpatternty
PRINTED BY { pr_rpattern }
INTERPRETED BY { interp_rpattern }
GLOBALIZED BY { glob_rpattern }
SUBSTITUTED BY { subst_rpattern }
| [ lconstr(c) ] -> { mk_rpattern (T (mk_lterm c None)) }
| [ "in" lconstr(c) ] -> { mk_rpattern (In_T (mk_lterm c None)) }
| [ lconstr(x) "in" lconstr(c) ] ->
{ mk_rpattern (X_In_T (mk_lterm x None, mk_lterm c None)) }
| [ "in" lconstr(x) "in" lconstr(c) ] ->
{ mk_rpattern (In_X_In_T (mk_lterm x None, mk_lterm c None)) }
| [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] ->
{ mk_rpattern (E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) }
| [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] ->
{ mk_rpattern (E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) }
END
{
let pr_ssrterm _ _ _ = pr_ssrterm
}
ARGUMENT EXTEND cpattern
PRINTED BY { pr_ssrterm }
INTERPRETED BY { interp_ssrterm }
GLOBALIZED BY { glob_cpattern } SUBSTITUTED BY { subst_ssrterm }
RAW_PRINTED BY { pr_ssrterm }
GLOB_PRINTED BY { pr_ssrterm }
| [ "Qed" constr(c) ] -> { mk_lterm c None }
END
{
let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
| Tok.KEYWORD "(" -> InParens
| Tok.KEYWORD "@" -> WithAt
| _ -> NoFlag
let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
}
GRAMMAR EXTEND Gram
GLOBAL: cpattern;
cpattern: [[ k = ssrtermkind; c = constr -> {
let pattern = mk_term k c None in
if loc_of_cpattern pattern <> Some loc && k = InParens
then mk_term Cpattern c None
else pattern } ]];
END
ARGUMENT EXTEND lcpattern
TYPED AS cpattern
PRINTED BY { pr_ssrterm }
INTERPRETED BY { interp_ssrterm }
GLOBALIZED BY { glob_cpattern } SUBSTITUTED BY { subst_ssrterm }
RAW_PRINTED BY { pr_ssrterm }
GLOB_PRINTED BY { pr_ssrterm }
| [ "Qed" lconstr(c) ] -> { mk_lterm c None }
END
GRAMMAR EXTEND Gram
GLOBAL: lcpattern;
lcpattern: [[ k = ssrtermkind; c = lconstr -> {
let pattern = mk_term k c None in
if loc_of_cpattern pattern <> Some loc && k = InParens
then mk_term Cpattern c None
else pattern } ]];
END
ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY { pr_rpattern }
| [ rpattern(pat) ] -> { pat }
END
TACTIC EXTEND ssrinstoftpat
| [ "ssrinstancesoftpat" cpattern(arg) ] -> { ssrinstancesof arg }
END
{
(* We wipe out all the keywords generated by the grammar rules we defined. *)
(* The user is supposed to Require Import ssreflect or Require ssreflect *)
(* and Import ssreflect.SsrSyntax to obtain these keywords and as a *)
(* consequence the extended ssreflect grammar. *)
let () = CLexer.set_keyword_state frozen_lexer ;;
}
|
