Source file ssrrewrite.ml

# 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 ()