forked from LPCIC/coq-elpi
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcoq_elpi_vernacular_syntax.mlg
176 lines (146 loc) · 7.34 KB
/
coq_elpi_vernacular_syntax.mlg
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
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
(* coq-elpi: Coq terms as the object language of elpi *)
(* license: GNU Lesser General Public License Version 2.1 or later *)
(* ------------------------------------------------------------------------- *)
DECLARE PLUGIN "elpi_plugin"
{
open Stdarg
open Ltac_plugin
open Pcoq.Constr
open Coq_elpi_arg_syntax
module EV = Coq_elpi_vernacular
module EA = Coq_elpi_arg_HOAS
module U = Coq_elpi_utils
}
(* Anti-quotation ******************************************************** *)
{
let pr_elpi_code _ _ _ (s : Elpi.API.Ast.Loc.t * string) = Pp.str (snd s)
}
ARGUMENT EXTEND elpi_code
PRINTED BY { pr_elpi_code }
END
{
let () = Coq_elpi_glob_quotation.is_elpi_code :=
(fun x -> Genarg.(has_type x (glbwit wit_elpi_code)))
let () = Coq_elpi_glob_quotation.get_elpi_code :=
(fun x -> Genarg.(out_gen (glbwit wit_elpi_code) x))
let pr_elpi_code_appArg _ _ _ (s : Elpi.API.Ast.Loc.t * string list) = Pp.prlist Pp.str (snd s)
}
ARGUMENT EXTEND elpi_code_appArg
PRINTED BY { pr_elpi_code_appArg }
END
{
let () = Coq_elpi_glob_quotation.is_elpi_code_appArg :=
(fun x -> Genarg.(has_type x (glbwit wit_elpi_code_appArg )))
let () = Coq_elpi_glob_quotation.get_elpi_code_appArg :=
(fun x -> Genarg.(out_gen (glbwit wit_elpi_code_appArg ) x))
let rec inlogpath q = function
| [] -> []
| x :: xs -> ("coq://" ^ Libnames.string_of_qualid q ^ "/" ^ x) :: inlogpath q xs
let warning_legacy_accumulate =
CWarnings.create ~name:"elpi.accumulate-syntax" ~category:"elpi.deprecated" (fun () ->
Pp.strbrk "The syntax 'Elpi Accumulate File \"path\"' is deprecated, use 'Elpi Accumulate File \"path\" From logpath'")
}
GRAMMAR EXTEND Gram
GLOBAL: term;
term: LEVEL "0"
[ [ s = QUOTATION "lp:" ->
{
let arg =
if s.[0] = '('
then Genarg.in_gen (Genarg.rawwit wit_elpi_code_appArg) (idents_of loc s)
else if s.[0] = '\123'
then Genarg.in_gen (Genarg.rawwit wit_elpi_code) (strip_curly loc s)
else Genarg.in_gen (Genarg.rawwit wit_elpi_code) (Coq_elpi_utils.of_coq_loc loc,s) in
CAst.make ~loc
(Constrexpr.CHole (None, Namegen.IntroAnonymous, Some arg)) } ]
]
;
END
GRAMMAR EXTEND Gram
GLOBAL: term;
term: LEVEL "0"
[ [ "lib"; ":"; id = qualified_name -> {
let ref = Coqlib.lib_ref (String.concat "." (snd id)) in
let path = Nametab.path_of_global ref in
CAst.make ~loc Constrexpr.(CRef (Libnames.qualid_of_path ~loc:(fst id) path,None)) }
| "lib"; ":"; "@"; id = qualified_name -> {
let ref = Coqlib.lib_ref (String.concat "." (snd id)) in
let path = Nametab.path_of_global ref in
let f = Libnames.qualid_of_path ~loc:(fst id) path in
CAst.make ~loc Constrexpr.(CAppExpl((f,None),[])) } ] ]
;
END
(* Syntax **************************************************************** *)
VERNAC COMMAND EXTEND Elpi CLASSIFIED AS SIDEFF
| #[ atts = skip_attribute ] [ "Elpi" "Accumulate" "File" string_list(s) ] -> { warning_legacy_accumulate ();
EV.skip ~atts EV.accumulate_files s }
| #[ atts = skip_attribute ] [ "Elpi" "Accumulate" "File" string_list(s) "From" global(g) ] -> {
EV.skip ~atts EV.accumulate_files (inlogpath g s) }
| #[ atts = skip_attribute ] [ "Elpi" "Accumulate" "Files" string_list(s) ] -> { warning_legacy_accumulate ();
EV.skip ~atts EV.accumulate_files s }
| #[ atts = skip_attribute ] [ "Elpi" "Accumulate" "Files" string_list(s) "From" global(g) ] -> {
EV.skip ~atts EV.accumulate_files (inlogpath g s) }
| #[ atts = skip_attribute ] [ "Elpi" "Accumulate" elpi_string(s) ] -> {
EV.skip ~atts EV.accumulate_string s }
| #[ atts = skip_attribute ] [ "Elpi" "Accumulate" qualified_name(p) "File" string_list(s) ] -> { warning_legacy_accumulate ();
EV.skip ~atts (EV.accumulate_files ~program:(snd p)) s }
| #[ atts = skip_attribute ] [ "Elpi" "Accumulate" qualified_name(p) "File" string_list(s) "From" global(g) ] -> {
EV.skip ~atts (EV.accumulate_files ~program:(snd p)) (inlogpath g s) }
| #[ atts = skip_attribute ] [ "Elpi" "Accumulate" qualified_name(p) "Files" string_list(s) ] -> { warning_legacy_accumulate ();
EV.skip ~atts (EV.accumulate_files ~program:(snd p)) s }
| #[ atts = skip_attribute ] [ "Elpi" "Accumulate" qualified_name(p) "Files" string_list(s) "From" global(g) ] -> {
EV.skip ~atts (EV.accumulate_files ~program:(snd p)) (inlogpath g s) }
| #[ atts = skip_attribute ] [ "Elpi" "Accumulate" qualified_name(p) elpi_string(s) ] -> {
EV.skip ~atts (EV.accumulate_string ~program:(snd p)) s }
| #[ atts = skip_attribute ] [ "Elpi" "Accumulate" "Db" qualified_name(d) ] -> {
EV.skip ~atts EV.accumulate_db (snd d) }
| #[ atts = skip_attribute ] [ "Elpi" "Accumulate" qualified_name(p) "Db" qualified_name(d) ] -> {
EV.skip ~atts (EV.accumulate_db ~program:(snd p)) (snd d) }
| [ "Elpi" "Debug" string_list(s) ] -> { EV.debug s }
| [ "Elpi" "Trace" string_list(s) ] -> { EV.trace 1 max_int s [] }
| [ "Elpi" "Trace" string_list(s) "/" string_list(o) ] -> { EV.trace 1 max_int s o }
| [ "Elpi" "Trace" int(start) int(stop) string_list(s) ] -> { EV.trace start stop s [] }
| [ "Elpi" "Trace" int(start) int(stop) string_list(s) "/" string_list(o) ] -> { EV.trace start stop s o }
| [ "Elpi" "Trace" "Off" ] -> { EV.trace 0 0 [] [] }
| [ "Elpi" "Bound" "Steps" int(steps) ] -> { EV.bound_steps steps }
| [ "Elpi" "Print" qualified_name(p) string_list(s) ] -> { EV.print (snd p) s }
| [ "Elpi" "Program" qualified_name(p) elpi_string(s) ] ->
{ EV.create_program p ~init:s }
| [ "Elpi" "Command" qualified_name(p) ] ->
{ EV.create_command p }
| [ "Elpi" "Tactic" qualified_name(p) ] ->
{ EV.create_tactic p }
| [ "Elpi" "Db" qualified_name(d) elpi_string(s) ] ->
{ EV.create_db d ~init:s }
| [ "Elpi" "Typecheck" ] -> { EV.typecheck_program () }
| [ "Elpi" "Typecheck" qualified_name(p) ] -> { EV.typecheck_program ~program:(snd p) () }
| [ "Elpi" "Document" "Builtins" ] -> { EV.document_builtins () }
| [ "Elpi" "Checker" string(s) ] -> { EV.load_checker s }
| [ "Elpi" "Printer" string(s) ] -> { EV.load_printer s }
| [ "Elpi" "Template" "Command" string(s) ] -> { EV.load_command s }
| [ "Elpi" "Template" "Tactic" string(s) ] -> { EV.load_tactic s }
END
VERNAC COMMAND EXTEND ElpiRun CLASSIFIED BY { fun _ -> Vernacextend.(VtSideff ([], VtNow)) }
| [ "Elpi" "Query" elpi_string(s) ] ->
{ EV.run_in_program s }
| [ "Elpi" "Query" qualified_name(p) elpi_string(s) ] ->
{ EV.run_in_program ~program:(snd p) s }
| [ "Elpi" "Export" qualified_name(p) ] => { Vernacextend.(VtSideff ([],VtNow)) } ->
{ EV.export_command (snd p) }
| #[ atts = any_attribute ]
[ "Elpi" qualified_name(p) elpi_arg_list(args) ] ->
{ EV.run_program (fst p) (snd p) ~atts args }
END
TACTIC EXTEND elpi_tac
| [ "elpi" qualified_name(p) elpi_tactic_arg_list(args) ] ->
{ EV.run_tactic (fst p) (snd p) ~atts:[] ist args }
| [ "ltac_attributes" ":" "(" ltac_attributes(atts) ")" "elpi" qualified_name(p) elpi_tactic_arg_list(args) ] ->
{ EV.run_tactic (fst p) (snd p) ~atts ist args }
| [ "#[" attributes(atts) "]" "elpi" qualified_name(p) elpi_tactic_arg_list(args) ] ->
{ EV.run_tactic (fst p) (snd p) ~atts ist args }
| [ "elpi" "query" elpi_string(s) ] ->
{ EV.run_in_tactic s ist }
| [ "elpi" "query" qualified_name(p) elpi_string(s) ] ->
{ EV.run_in_tactic s ~program:(snd p) ist }
END
(* vim:set ft=ocaml: *)