package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file ssrrewrite.ml

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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296

# 11 "plugins/ssrrewrite/ssrrewrite.mlg"
 

open Constrexpr
open Procq.Constr
open Ltac_plugin
open Ssreflect_plugin.Ssrtacticals
open Ssreflect_plugin.Ssrequality
open Ssreflect_plugin.Ssrparser
open Ssreflect_plugin.Ssrtacs

let warn_deprecated_rewrite =
  CWarnings.create ~name:"rewrite-rw" ~category:Deprecation.Version.v9_3
    ~quickfix:(fun ~loc () -> [Quickfix.make ~loc (Pp.str "rw")])
    (fun () -> Pp.str "The ssreflect 'rewrite' tactic has been renamed 'rw' (available from Rocq 9.3).")

let warn_deprecated_rewrite ?loc () =
  (* 7 = length "rewrite" *)
  let loc = Option.map (fun l -> Loc.sub l 0 7) loc in
  warn_deprecated_rewrite ?loc ()


# 25 "plugins/ssrrewrite/ssrrewrite.ml"

let (wit_ssrrewriteargs, ssrrewriteargs) =
  Tacentries.argument_extend ~plugin:"rocq-runtime.plugins.ssreflect_rewrite" ~name:"ssrrewriteargs" ~ignore_kw:true
  {
  Tacentries.arg_parsing =
  Vernacextend.Arg_rules [];
  Tacentries.arg_tag = Some
                       (Geninterp.Val.List (Geninterp.val_tag (Genarg.topwit wit_ssrrwarg)));
  Tacentries.arg_intern = Tacentries.ArgInternWit (Genarg.ListArg (wit_ssrrwarg));
  Tacentries.arg_subst = Tacentries.ArgSubstWit (Genarg.ListArg (wit_ssrrwarg));
  Tacentries.arg_interp = Tacentries.ArgInterpWit (Genarg.ListArg (wit_ssrrwarg));
  Tacentries.arg_printer = ((fun env sigma -> 
# 42 "plugins/ssrrewrite/ssrrewrite.mlg"
                                                                   pr_ssrrwargs 
# 40 "plugins/ssrrewrite/ssrrewrite.ml"
), (fun env sigma -> 
# 42 "plugins/ssrrewrite/ssrrewrite.mlg"
                                                                   pr_ssrrwargs 
# 44 "plugins/ssrrewrite/ssrrewrite.ml"
), (fun env sigma -> 
                           
# 42 "plugins/ssrrewrite/ssrrewrite.mlg"
                                                                   pr_ssrrwargs 
# 49 "plugins/ssrrewrite/ssrrewrite.ml"
));
  }
let _ = (wit_ssrrewriteargs, ssrrewriteargs)


# 45 "plugins/ssrrewrite/ssrrewrite.mlg"
 

let ssr_rewrite_syntax = Summary.ref ~name:"SSR:rewrite" true

let () =
  Goptions.(declare_bool_option
    { optstage = Summary.Stage.Synterp;
      optkey   = ["SsrRewrite"];
      optread  = (fun _ -> !ssr_rewrite_syntax);
      optdepr  = None;
      optwrite = (fun b -> ssr_rewrite_syntax := b) })

let lbrace = Char.chr 123
(** Workaround to a limitation of coqpp *)

let test_ssr_rewrite_syntax =
  let test kwstate strm =
    if not !ssr_rewrite_syntax then Error () else
    if Pptactic.ssr_rewrite_loaded () then Ok () else
    match LStream.peek_nth kwstate 0 strm with
    | Some (Tok.KEYWORD key) when List.mem key.[0] [lbrace; '['; '/'] -> Ok ()
    | _ -> Error () in
  Procq.Entry.(of_parser "test_ssr_rewrite_syntax" { parser_fun = test })


# 81 "plugins/ssrrewrite/ssrrewrite.ml"

let _ = let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ssreflect_rewrite", "ssrrewrite.mlg:0") ~ignore_kw:true
  ssrrewriteargs
  (Procq.Reuse (None, [Procq.Production.make
                       (Procq.Rule.next
                        (Procq.Rule.next (Procq.Rule.stop)
                         ((Procq.Symbol.nterm test_ssr_rewrite_syntax)))
                        ((Procq.Symbol.nterm ssrrwargs)))
                       (fun a _ loc -> 
# 73 "plugins/ssrrewrite/ssrrewrite.mlg"
                                                                     a 
# 94 "plugins/ssrrewrite/ssrrewrite.ml"
)]))
  in ()

let () = Tacentries.tactic_extend "rocq-runtime.plugins.ssreflect_rewrite" "ssrrewrite" ~level:0 ~warn:( warn_deprecated_rewrite ) 
         [(Tacentries.TyML (Tacentries.TyIdent ("rewrite", Tacentries.TyArg (
                                                           Extend.TUentry (Genarg.get_arg_tag wit_ssrrewriteargs), 
                                                           Tacentries.TyArg (
                                                           Extend.TUentry (Genarg.get_arg_tag wit_ssrclauses), 
                                                           Tacentries.TyNil))), 
           (fun args clauses ist -> 
# 80 "plugins/ssrrewrite/ssrrewrite.mlg"
      tclCLAUSES (ssrrewritetac ist args) clauses 
# 107 "plugins/ssrrewrite/ssrrewrite.ml"
)))]


# 83 "plugins/ssrrewrite/ssrrewrite.mlg"
 

(* global syntactic changes and vernacular commands *)

(** Alternative notations for "match" and anonymous arguments. *)(* ************)

(* Syntax:                                                        *)
(*  if <term> is <pattern> then ... else ...                      *)
(*  if <term> is <pattern> [in ..] return ... then ... else ...   *)
(* The scope of a top-level 'as' in the pattern extends over the  *)
(* 'return' type (dependent if/let).                              *)
(* in b       (*^--ALTERNATIVE INNER LET--------^ *)              *)

(* Caveat : There is no pretty-printing support, since this would *)
(* require a modification to the Rocq kernel (adding a new match  *)
(* display style -- why aren't these strings?); also, the v8.1    *)
(* pretty-printer only allows extension hooks for printing        *)
(* integer or string literals.                                    *)
(*   Also note that in the v8 grammar "is" needs to be a keyword; *)
(* as this can't be done from an ML extension file, the new       *)
(* syntax will only work when ssreflect.v is imported.            *)

let no_ct = None, None and no_rt = None
let aliasvar = function
  | [[{ CAst.v = CPatAlias (_, na); loc }]] -> Some na
  | _ -> None
let mk_cnotype mp = aliasvar mp, None
let mk_ctype mp t = aliasvar mp, Some t
let mk_rtype t = Some t
let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt
let mk_pat c (na, t) = (c, na, t)


# 145 "plugins/ssrrewrite/ssrrewrite.ml"

let _ =
  let ssr_rtype = Procq.Entry.make "ssr_rtype"
  and ssr_mpat = Procq.Entry.make "ssr_mpat"
  and ssr_dpat = Procq.Entry.make "ssr_dpat"
  and ssr_dthen = Procq.Entry.make "ssr_dthen"
  and ssr_elsepat = Procq.Entry.make "ssr_elsepat"
  and ssr_else = Procq.Entry.make "ssr_else"
  in
  let () = assert (Procq.Entry.is_empty ssr_rtype) in
  let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ssreflect_rewrite", "ssrrewrite.mlg:1") ~ignore_kw:true
  ssr_rtype
  (Procq.Fresh
  (Gramlib.Gramext.First, [(None, None,
                           [Procq.Production.make
                            (Procq.Rule.next
                             (Procq.Rule.next (Procq.Rule.stop)
                              ((Procq.Symbol.token (Tok.PKEYWORD ("return")))))
                             ((Procq.Symbol.nterml term ("100"))))
                            (fun t _ loc -> 
# 119 "plugins/ssrrewrite/ssrrewrite.mlg"
                                                    mk_rtype t 
# 169 "plugins/ssrrewrite/ssrrewrite.ml"
)])]))
  in let () = assert (Procq.Entry.is_empty ssr_mpat) in
  let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ssreflect_rewrite", "ssrrewrite.mlg:2") ~ignore_kw:true
  ssr_mpat
  (Procq.Fresh
  (Gramlib.Gramext.First, [(None, None,
                           [Procq.Production.make
                            (Procq.Rule.next (Procq.Rule.stop)
                             ((Procq.Symbol.nterm pattern)))
                            (fun p loc -> 
# 120 "plugins/ssrrewrite/ssrrewrite.mlg"
                                [[p]] 
# 183 "plugins/ssrrewrite/ssrrewrite.ml"
)])]))
  in let () = assert (Procq.Entry.is_empty ssr_dpat) in
  let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ssreflect_rewrite", "ssrrewrite.mlg:3") ~ignore_kw:true
  ssr_dpat
  (Procq.Fresh
  (Gramlib.Gramext.First, [(None, None,
                           [Procq.Production.make
                            (Procq.Rule.next (Procq.Rule.stop)
                             ((Procq.Symbol.nterm ssr_mpat)))
                            (fun mp loc -> 
# 124 "plugins/ssrrewrite/ssrrewrite.mlg"
                         mp, no_ct, no_rt 
# 197 "plugins/ssrrewrite/ssrrewrite.ml"
);
                           Procq.Production.make
                           (Procq.Rule.next
                            (Procq.Rule.next (Procq.Rule.stop)
                             ((Procq.Symbol.nterm ssr_mpat)))
                            ((Procq.Symbol.nterm ssr_rtype)))
                           (fun rt mp loc -> 
# 123 "plugins/ssrrewrite/ssrrewrite.mlg"
                                         mp, mk_cnotype mp, rt 
# 207 "plugins/ssrrewrite/ssrrewrite.ml"
);
                           Procq.Production.make
                           (Procq.Rule.next
                            (Procq.Rule.next
                             (Procq.Rule.next
                              (Procq.Rule.next (Procq.Rule.stop)
                               ((Procq.Symbol.nterm ssr_mpat)))
                              ((Procq.Symbol.token (Tok.PKEYWORD ("in")))))
                             ((Procq.Symbol.nterm pattern)))
                            ((Procq.Symbol.nterm ssr_rtype)))
                           (fun rt t _ mp loc -> 
# 122 "plugins/ssrrewrite/ssrrewrite.mlg"
                                                            mp, mk_ctype mp t, rt 
# 221 "plugins/ssrrewrite/ssrrewrite.ml"
)])]))
  in let () = assert (Procq.Entry.is_empty ssr_dthen) in
  let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ssreflect_rewrite", "ssrrewrite.mlg:4") ~ignore_kw:true
  ssr_dthen
  (Procq.Fresh
  (Gramlib.Gramext.First, [(None, None,
                           [Procq.Production.make
                            (Procq.Rule.next
                             (Procq.Rule.next
                              (Procq.Rule.next (Procq.Rule.stop)
                               ((Procq.Symbol.nterm ssr_dpat)))
                              ((Procq.Symbol.token (Tok.PKEYWORD ("then")))))
                             ((Procq.Symbol.nterm lconstr)))
                            (fun c _ dp loc -> 
# 126 "plugins/ssrrewrite/ssrrewrite.mlg"
                                                        mk_dthen ~loc dp c 
# 239 "plugins/ssrrewrite/ssrrewrite.ml"
)])]))
  in let () = assert (Procq.Entry.is_empty ssr_elsepat) in
  let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ssreflect_rewrite", "ssrrewrite.mlg:5") ~ignore_kw:true
  ssr_elsepat
  (Procq.Fresh
  (Gramlib.Gramext.First, [(None, None,
                           [Procq.Production.make
                            (Procq.Rule.next (Procq.Rule.stop)
                             ((Procq.Symbol.token (Tok.PKEYWORD ("else")))))
                            (fun _ loc -> 
# 127 "plugins/ssrrewrite/ssrrewrite.mlg"
                              [[CAst.make ~loc @@ CPatAtom None]] 
# 253 "plugins/ssrrewrite/ssrrewrite.ml"
)])]))
  in let () = assert (Procq.Entry.is_empty ssr_else) in
  let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ssreflect_rewrite", "ssrrewrite.mlg:6") ~ignore_kw:true
  ssr_else
  (Procq.Fresh
  (Gramlib.Gramext.First, [(None, None,
                           [Procq.Production.make
                            (Procq.Rule.next
                             (Procq.Rule.next (Procq.Rule.stop)
                              ((Procq.Symbol.nterm ssr_elsepat)))
                             ((Procq.Symbol.nterm lconstr)))
                            (fun c mp loc -> 
# 128 "plugins/ssrrewrite/ssrrewrite.mlg"
                                                  CAst.make ~loc (mp, c) 
# 269 "plugins/ssrrewrite/ssrrewrite.ml"
)])]))
  in let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ssreflect_rewrite", "ssrrewrite.mlg:7") ~ignore_kw:true
  term
  (Procq.Reuse (Some
  ("10"), [Procq.Production.make
           (Procq.Rule.next
            (Procq.Rule.next
             (Procq.Rule.next
              (Procq.Rule.next
               (Procq.Rule.next (Procq.Rule.stop)
                ((Procq.Symbol.token (Tok.PKEYWORD ("if")))))
               ((Procq.Symbol.nterml term ("200"))))
              ((Procq.Symbol.token (Tok.PKEYWORD ("isn't")))))
             ((Procq.Symbol.nterm ssr_dthen)))
            ((Procq.Symbol.nterm ssr_else)))
           (fun b2 db1 _ c _ loc -> 
# 131 "plugins/ssrrewrite/ssrrewrite.mlg"
        let b1, ct, rt = db1 in
      let b1, b2 = let open CAst in
        let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in
        (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1))
      in
      CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) 
# 294 "plugins/ssrrewrite/ssrrewrite.ml"
)]))
  in ()