blob: 746c368aa9489ef2782ef480b1f6749d378fbe6b (
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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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) *)
(************************************************************************)
open Ltac_plugin
open Genarg
open Pcoq
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 "(" -> '('
| Tok.KEYWORD "@" -> '@'
| _ -> ' '
let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
GEXTEND Gram
GLOBAL: cpattern;
cpattern: [[ k = ssrtermkind; c = constr ->
let pattern = mk_term k c None in
if loc_of_cpattern pattern <> Some !@loc && k = '('
then mk_term 'x' 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
GEXTEND Gram
GLOBAL: lcpattern;
lcpattern: [[ k = ssrtermkind; c = lconstr ->
let pattern = mk_term k c None in
if loc_of_cpattern pattern <> Some !@loc && k = '('
then mk_term 'x' 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) ] -> [ Proofview.V82.tactic (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 ;;
|
