Source file ssrvernac.ml

# 13 "plugins/ssr/ssrvernac.mlg"
 

open Names
module CoqConstr = Constr
open CoqConstr
open Constrexpr
open Constrexpr_ops
open Procq.Prim
open Procq.Constr
open Pvernac.Vernac_
open Ltac_plugin
open Glob_term
open Stdarg
open Pp
open Ppconstr
open Printer
open Util
open Ssrprinters
open Ssrcommon


# 25 "plugins/ssr/ssrvernac.ml"


# 42 "plugins/ssr/ssrvernac.mlg"
 

(* global syntactic changes and vernacular commands *)

(** Alternative notations for anonymous arguments. *)(* ************)

(* Syntax:                                                        *)
(*  let: <pattern> := <term> in ...                               *)
(*  let: <pattern> [in ...] := <term> return ... in ...           *)
(* The scope of a top-level 'as' in the pattern extends over the  *)
(* 'return' type (dependent let).                              *)
(* Note that the optional "in ..." appears next to the <pattern>  *)
(* rather than the <term> in the "let:" syntax. The alternative   *)
(* would lead to ambiguities in, e.g.,                            *)
(* let: p1 := (*v---INNER LET:---v *)                             *)
(*   let: p2 := let: p3 := e3 in k return t in k2 in k1 return t' *)
(* 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.                                    *)

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_let ?loc rt ct mp c1 =
  CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [CAst.make ?loc (mp, c1)])
let mk_pat c (na, t) = (c, na, t)


# 65 "plugins/ssr/ssrvernac.ml"

let _ =
  let ssr_rtype = Procq.Entry.make "ssr_rtype"
  and ssr_mpat = Procq.Entry.make "ssr_mpat"
  in
  let () = assert (Procq.Entry.is_empty ssr_rtype) in
  let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ssreflect", "ssrvernac.mlg:0") ~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 -> 
# 81 "plugins/ssr/ssrvernac.mlg"
                                                    mk_rtype t 
# 85 "plugins/ssr/ssrvernac.ml"
)])]))
  in let () = assert (Procq.Entry.is_empty ssr_mpat) in
  let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ssreflect", "ssrvernac.mlg:1") ~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 -> 
# 82 "plugins/ssr/ssrvernac.mlg"
                                [[p]] 
# 99 "plugins/ssr/ssrvernac.ml"
)])]))
  in let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ssreflect", "ssrvernac.mlg:2") ~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.next
                 (Procq.Rule.next
                  (Procq.Rule.next
                   (Procq.Rule.next
                    (Procq.Rule.next (Procq.Rule.stop)
                     ((Procq.Symbol.token (Tok.PKEYWORD ("let")))))
                    ((Procq.Symbol.token (Tok.PKEYWORD (":")))))
                   ((Procq.Symbol.nterm ssr_mpat)))
                  ((Procq.Symbol.token (Tok.PKEYWORD ("in")))))
                 ((Procq.Symbol.nterm pattern)))
                ((Procq.Symbol.token (Tok.PKEYWORD (":=")))))
               ((Procq.Symbol.nterm lconstr)))
              ((Procq.Symbol.nterm ssr_rtype)))
             ((Procq.Symbol.token (Tok.PKEYWORD ("in")))))
            ((Procq.Symbol.nterm lconstr)))
           (fun c1 _ rt c _ t _ mp _ _ loc -> 
# 91 "plugins/ssr/ssrvernac.mlg"
        mk_let ~loc rt [mk_pat c (mk_ctype mp t)] mp c1 
# 129 "plugins/ssr/ssrvernac.ml"
);
          Procq.Production.make
          (Procq.Rule.next
           (Procq.Rule.next
            (Procq.Rule.next
             (Procq.Rule.next
              (Procq.Rule.next
               (Procq.Rule.next
                (Procq.Rule.next
                 (Procq.Rule.next (Procq.Rule.stop)
                  ((Procq.Symbol.token (Tok.PKEYWORD ("let")))))
                 ((Procq.Symbol.token (Tok.PKEYWORD (":")))))
                ((Procq.Symbol.nterm ssr_mpat)))
               ((Procq.Symbol.token (Tok.PKEYWORD (":=")))))
              ((Procq.Symbol.nterm lconstr)))
             ((Procq.Symbol.nterm ssr_rtype)))
            ((Procq.Symbol.token (Tok.PKEYWORD ("in")))))
           ((Procq.Symbol.nterm lconstr)))
          (fun c1 _ rt c _ mp _ _ loc -> 
# 88 "plugins/ssr/ssrvernac.mlg"
        mk_let ~loc rt [mk_pat c (mk_cnotype mp)] mp c1 
# 151 "plugins/ssr/ssrvernac.ml"
);
          Procq.Production.make
          (Procq.Rule.next
           (Procq.Rule.next
            (Procq.Rule.next
             (Procq.Rule.next
              (Procq.Rule.next
               (Procq.Rule.next
                (Procq.Rule.next (Procq.Rule.stop)
                 ((Procq.Symbol.token (Tok.PKEYWORD ("let")))))
                ((Procq.Symbol.token (Tok.PKEYWORD (":")))))
               ((Procq.Symbol.nterm ssr_mpat)))
              ((Procq.Symbol.token (Tok.PKEYWORD (":=")))))
             ((Procq.Symbol.nterm lconstr)))
            ((Procq.Symbol.token (Tok.PKEYWORD ("in")))))
           ((Procq.Symbol.nterm lconstr)))
          (fun c1 _ c _ mp _ _ loc -> 
# 85 "plugins/ssr/ssrvernac.mlg"
        mk_let ~loc no_rt [mk_pat c no_ct] mp c1 
# 171 "plugins/ssr/ssrvernac.ml"
)]))
  in ()


# 109 "plugins/ssr/ssrvernac.mlg"
 

let declare_one_prenex_implicit locality f =
  let fref =
    try Smartlocate.global_with_alias f
    with e when CErrors.noncritical e -> errorstrm (pr_qualid f ++ str " is not declared") in
  let rec loop = function
  | a :: args' when Impargs.is_status_implicit a ->
    MaxImplicit :: loop args'
  | args' when List.exists Impargs.is_status_implicit args' ->
      errorstrm (str "Expected prenex implicits for " ++ pr_qualid f)
  | _ -> [] in
  let impls =
    match Impargs.implicits_of_global fref  with
    | [cond,impls] -> impls
    | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f)
    | _ -> errorstrm (str "Multiple implicits not supported") in
  match loop impls  with
  | [] ->
    errorstrm (str "Expected some implicits for " ++ pr_qualid f)
  | impls ->
    Impargs.set_implicits locality fref [List.map (fun imp -> (Anonymous,imp)) impls]


# 201 "plugins/ssr/ssrvernac.ml"

let () = Vernacextend.static_vernac_extend ~plugin:(Some "rocq-runtime.plugins.ssreflect") ~command:"Ssrpreneximplicits" ~classifier:(fun ~atts:_ _ -> Vernacextend.classify_as_sideeff) ~ignore_kw:true ?entry:None 
         [(Vernacextend.TyML
         (false,
          Vernacextend.TyTerminal
          ("Prenex",
           Vernacextend.TyTerminal
           ("Implicits",
            Vernacextend.TyNonTerminal (Extend.TUlist1 (Extend.TUentry (Genarg.get_arg_tag wit_global)),
            Vernacextend.TyNil))),
          (let coqpp_body fl locality = Vernactypes.vtdefault (fun () -> 
# 136 "plugins/ssr/ssrvernac.mlg"
      
         let locality = Locality.make_section_locality locality in
         List.iter (declare_one_prenex_implicit locality) fl;
     
# 218 "plugins/ssr/ssrvernac.ml"
) in
            fun fl ?loc ~atts () -> coqpp_body fl (Attributes.parse 
# 135 "plugins/ssr/ssrvernac.mlg"
                   Attributes.locality
# 223 "plugins/ssr/ssrvernac.ml"
 atts)),
          None))]

let _ = let () =
  Egramml.grammar_extend ~plugin_uid:("rocq-runtime.plugins.ssreflect", "ssrvernac.mlg:3") ~ignore_kw:true
  gallina_ext
  (Procq.Reuse (None, [Procq.Production.make
                       (Procq.Rule.next
                        (Procq.Rule.next
                         (Procq.Rule.next (Procq.Rule.stop)
                          ((Procq.Symbol.token (Tok.PIDENT (Some
                          ("Import"))))))
                         ((Procq.Symbol.token (Tok.PIDENT (Some
                         ("Prenex"))))))
                        ((Procq.Symbol.token (Tok.PIDENT (Some
                        ("Implicits"))))))
                       (fun _ _ _ loc -> 
# 148 "plugins/ssr/ssrvernac.mlg"
        Vernacexpr.VernacSynterp (Vernacexpr.VernacSetOption (false, ["Printing"; "Implicit"; "Defensive"], Vernacexpr.OptionUnset)) 
# 243 "plugins/ssr/ssrvernac.ml"
)]))
  in ()


# 161 "plugins/ssr/ssrvernac.mlg"
 

let pr_raw_ssrhintref env sigma prc _ _ = let open CAst in function
  | { v = CAppExpl ((r,x), args) } when isCHoles args ->
    prc env sigma (CAst.make @@ CRef (r,x)) ++ str "|" ++ int (List.length args)
  | { v = CApp ({ v = CRef _ }, _) } as c -> prc env sigma c
  | { v = CApp (c, args) } when isCxHoles args ->
    prc env sigma c ++ str "|" ++ int (List.length args)
  | c -> prc env sigma c

let pr_rawhintref env sigma c =
  match DAst.get c with
  | GApp (f, args) when isRHoles args ->
    pr_glob_constr_env env sigma f ++ str "|" ++ int (List.length args)
  | _ -> pr_glob_constr_env env sigma c

let pr_glob_ssrhintref env sigma _ _ _ (c, _) = pr_rawhintref env sigma c

let pr_ssrhintref env sigma prc _ _ = prc env sigma

let mkhintref ?loc c n = match c.CAst.v with
  | CRef (r,x) -> CAst.make ?loc @@ CAppExpl ((r, x), mkCHoles ?loc n)
  | _ -> mkAppC (c, mkCHoles ?loc n)


# 274 "plugins/ssr/ssrvernac.ml"

let (wit_ssrhintref, ssrhintref) =
  Tacentries.argument_extend ~plugin:"rocq-runtime.plugins.ssreflect" ~name:"ssrhintref" ~ignore_kw:true
  {
  Tacentries.arg_parsing =
  Vernacextend.Arg_rules
  [(Procq.Production.make
    (Procq.Rule.next
     (Procq.Rule.next
      (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.nterm constr)))
      ((Procq.Symbol.token (CLexer.terminal "|"))))
     ((Procq.Symbol.nterm natural)))
    (fun n _ c loc -> 
# 193 "plugins/ssr/ssrvernac.mlg"
                                       mkhintref ~loc c n  
# 290 "plugins/ssr/ssrvernac.ml"
));
  (Procq.Production.make
   (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.nterm constr)))
   (fun c loc -> 
# 192 "plugins/ssr/ssrvernac.mlg"
                        c  
# 297 "plugins/ssr/ssrvernac.ml"
))];
  Tacentries.arg_tag = Some (Geninterp.val_tag (Genarg.topwit wit_constr));
  Tacentries.arg_intern = Tacentries.ArgInternWit (wit_constr);
  Tacentries.arg_subst = Tacentries.ArgSubstWit (wit_constr);
  Tacentries.arg_interp = Tacentries.ArgInterpWit (wit_constr);
  Tacentries.arg_printer = ((fun env sigma -> 
# 190 "plugins/ssr/ssrvernac.mlg"
                   pr_raw_ssrhintref env sigma 
# 306 "plugins/ssr/ssrvernac.ml"
), (fun env sigma -> 
# 191 "plugins/ssr/ssrvernac.mlg"
                    pr_glob_ssrhintref env sigma 
# 310 "plugins/ssr/ssrvernac.ml"
), (fun env sigma -> 
                           
# 189 "plugins/ssr/ssrvernac.mlg"
               pr_ssrhintref env sigma 
# 315 "plugins/ssr/ssrvernac.ml"
));
  }
let _ = (wit_ssrhintref, ssrhintref)


# 196 "plugins/ssr/ssrvernac.mlg"
 

(* View purpose *)

let pr_viewpos = function
  | Some Ssrview.AdaptorDb.Forward -> str " for move/"
  | Some Ssrview.AdaptorDb.Backward -> str " for apply/"
  | Some Ssrview.AdaptorDb.Equivalence -> str " for apply//"
  | None -> mt ()

let pr_ssrviewpos _ _ _ = pr_viewpos


# 335 "plugins/ssr/ssrvernac.ml"

let (wit_ssrviewpos, ssrviewpos) =
  Tacentries.argument_extend ~plugin:"rocq-runtime.plugins.ssreflect" ~name:"ssrviewpos" ~ignore_kw:true
  {
  Tacentries.arg_parsing =
  Vernacextend.Arg_rules
  [(Procq.Production.make (Procq.Rule.stop) (fun loc -> 
# 215 "plugins/ssr/ssrvernac.mlg"
              None  
# 345 "plugins/ssr/ssrvernac.ml"
));
  (Procq.Production.make
   (Procq.Rule.next
    (Procq.Rule.next
     (Procq.Rule.next (Procq.Rule.stop)
      ((Procq.Symbol.token (CLexer.terminal "for"))))
     ((Procq.Symbol.token (CLexer.terminal "apply"))))
    ((Procq.Symbol.token (CLexer.terminal "//"))))
   (fun _ _ _ loc -> 
# 214 "plugins/ssr/ssrvernac.mlg"
                                 Some Ssrview.AdaptorDb.Equivalence  
# 357 "plugins/ssr/ssrvernac.ml"
));
  (Procq.Production.make
   (Procq.Rule.next
    (Procq.Rule.next
     (Procq.Rule.next
      (Procq.Rule.next (Procq.Rule.stop)
       ((Procq.Symbol.token (CLexer.terminal "for"))))
      ((Procq.Symbol.token (CLexer.terminal "apply"))))
     ((Procq.Symbol.token (CLexer.terminal "/"))))
    ((Procq.Symbol.token (CLexer.terminal "/"))))
   (fun _ _ _ _ loc -> 
# 213 "plugins/ssr/ssrvernac.mlg"
                                    Some Ssrview.AdaptorDb.Equivalence  
# 371 "plugins/ssr/ssrvernac.ml"
));
  (Procq.Production.make
   (Procq.Rule.next
    (Procq.Rule.next
     (Procq.Rule.next (Procq.Rule.stop)
      ((Procq.Symbol.token (CLexer.terminal "for"))))
     ((Procq.Symbol.token (CLexer.terminal "apply"))))
    ((Procq.Symbol.token (CLexer.terminal "/"))))
   (fun _ _ _ loc -> 
# 212 "plugins/ssr/ssrvernac.mlg"
                                Some Ssrview.AdaptorDb.Backward  
# 383 "plugins/ssr/ssrvernac.ml"
));
  (Procq.Production.make
   (Procq.Rule.next
    (Procq.Rule.next
     (Procq.Rule.next (Procq.Rule.stop)
      ((Procq.Symbol.token (CLexer.terminal "for"))))
     ((Procq.Symbol.token (CLexer.terminal "move"))))
    ((Procq.Symbol.token (CLexer.terminal "/"))))
   (fun _ _ _ loc -> 
# 211 "plugins/ssr/ssrvernac.mlg"
                               Some Ssrview.AdaptorDb.Forward  
# 395 "plugins/ssr/ssrvernac.ml"
))];
  Tacentries.arg_tag = None;
  Tacentries.arg_intern = Tacentries.ArgInternFun (fun ist v -> (ist, v));
  Tacentries.arg_subst = Tacentries.ArgSubstFun (fun s v -> v);
  Tacentries.arg_interp = Tacentries.ArgInterpRet;
  Tacentries.arg_printer = ((fun env sigma -> 
# 210 "plugins/ssr/ssrvernac.mlg"
                                        pr_ssrviewpos 
# 404 "plugins/ssr/ssrvernac.ml"
), (fun env sigma -> 
# 210 "plugins/ssr/ssrvernac.mlg"
                                        pr_ssrviewpos 
# 408 "plugins/ssr/ssrvernac.ml"
), (fun env sigma -> 
                           
# 210 "plugins/ssr/ssrvernac.mlg"
                                        pr_ssrviewpos 
# 413 "plugins/ssr/ssrvernac.ml"
));
  }
let _ = (wit_ssrviewpos, ssrviewpos)


# 218 "plugins/ssr/ssrvernac.mlg"
 

let pr_ssrviewposspc _ _ _ i = pr_viewpos i ++ spc ()


# 425 "plugins/ssr/ssrvernac.ml"

let (wit_ssrviewposspc, ssrviewposspc) =
  Tacentries.argument_extend ~plugin:"rocq-runtime.plugins.ssreflect" ~name:"ssrviewposspc" ~ignore_kw:true
  {
  Tacentries.arg_parsing =
  Vernacextend.Arg_alias (ssrviewpos);
  Tacentries.arg_tag = Some
                       (Geninterp.val_tag (Genarg.topwit wit_ssrviewpos));
  Tacentries.arg_intern = Tacentries.ArgInternWit (wit_ssrviewpos);
  Tacentries.arg_subst = Tacentries.ArgSubstWit (wit_ssrviewpos);
  Tacentries.arg_interp = Tacentries.ArgInterpWit (wit_ssrviewpos);
  Tacentries.arg_printer = ((fun env sigma -> 
# 224 "plugins/ssr/ssrvernac.mlg"
                                                               pr_ssrviewposspc 
# 440 "plugins/ssr/ssrvernac.ml"
), (fun env sigma -> 
# 224 "plugins/ssr/ssrvernac.mlg"
                                                               pr_ssrviewposspc 
# 444 "plugins/ssr/ssrvernac.ml"
), (fun env sigma -> 
                           
# 224 "plugins/ssr/ssrvernac.mlg"
                                                               pr_ssrviewposspc 
# 449 "plugins/ssr/ssrvernac.ml"
));
  }
let _ = (wit_ssrviewposspc, ssrviewposspc)


# 228 "plugins/ssr/ssrvernac.mlg"
 

let print_view_hints env sigma kind l =
  let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in
  let pp_hints = pr_list spc (pr_rawhintref env sigma) l in
  Feedback.msg_notice  (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())


# 464 "plugins/ssr/ssrvernac.ml"

let () = Vernacextend.static_vernac_extend ~plugin:(Some "rocq-runtime.plugins.ssreflect") ~command:"PrintView" ~classifier:(fun ~atts:_ _ -> Vernacextend.classify_as_query) ~ignore_kw:true ?entry:None 
         [(Vernacextend.TyML
         (false,
          Vernacextend.TyTerminal
          ("Print",
           Vernacextend.TyTerminal
           ("Hint",
            Vernacextend.TyTerminal
            ("View",
             Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_ssrviewpos),
             Vernacextend.TyNil)))),
          (let coqpp_body i () = Vernactypes.vtdefault (fun () -> 
# 239 "plugins/ssr/ssrvernac.mlg"
   
    let env = Global.env () in
    let sigma = Evd.from_env env in
    (match i with
    | Some k ->
      print_view_hints env sigma k (Ssrview.AdaptorDb.get k)
    | None ->
        List.iter (fun k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k))
          [ Ssrview.AdaptorDb.Forward;
            Ssrview.AdaptorDb.Backward;
            Ssrview.AdaptorDb.Equivalence ])
  
# 491 "plugins/ssr/ssrvernac.ml"
) in
            fun i ?loc ~atts () ->
            coqpp_body i (Attributes.unsupported_attributes atts)),
          None))]


# 253 "plugins/ssr/ssrvernac.mlg"
 

let glob_view_hints lvh =
  List.map (Constrintern.intern_constr (Global.env ()) (Evd.from_env (Global.env ()))) lvh


# 505 "plugins/ssr/ssrvernac.ml"

let () = Vernacextend.static_vernac_extend ~plugin:(Some "rocq-runtime.plugins.ssreflect") ~command:"HintView" ~classifier:(fun ~atts:_ _ -> Vernacextend.classify_as_sideeff) ~ignore_kw:true ?entry:None 
         [(Vernacextend.TyML
         (false,
          Vernacextend.TyTerminal
          ("Hint",
           Vernacextend.TyTerminal
           ("View",
            Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_ssrviewposspc),
            Vernacextend.TyNonTerminal (Extend.TUlist1 (Extend.TUentry (Genarg.get_arg_tag wit_ssrhintref)),
            Vernacextend.TyNil)))),
          (let coqpp_body n lvh () = Vernactypes.vtdefault (fun () -> 
# 262 "plugins/ssr/ssrvernac.mlg"
       let hints = glob_view_hints lvh in
       match n with
       | None ->
          Ssrview.AdaptorDb.declare Ssrview.AdaptorDb.Forward hints;
          Ssrview.AdaptorDb.declare Ssrview.AdaptorDb.Backward hints
       | Some k ->
          Ssrview.AdaptorDb.declare k hints 
# 526 "plugins/ssr/ssrvernac.ml"
) in
            fun n lvh ?loc ~atts () ->
            coqpp_body n lvh (Attributes.unsupported_attributes atts)),
          None))]