coq_elpi_vernacular_syntax.mlg

(* coq-elpi: Coq terms as the object language of elpi                        *)
(* license: GNU Lesser General Public License Version 2.1 or later           *)
(* ------------------------------------------------------------------------- *)

DECLARE PLUGIN "coq-elpi.elpi"

{

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 -> (Libnames.string_of_qualid q ^ "/" ^ x) :: inlogpath q xs

let warning_legacy_accumulate_gen =
  CWarnings.create ~default:CWarnings.AsError ~name:"elpi.accumulate-syntax" ~category:Coq_elpi_utils.elpi_depr_cat (fun has_from ->
      if has_from then
        Pp.strbrk "The syntax 'Elpi Accumulate File \"path\"' is deprecated, use 'Elpi Accumulate File \"path\" From logpath'"
      else Pp.strbrk "The syntax 'Elpi Accumulate File \"path\" From logpath' is deprecated, use 'From logpath Extra Dependency \"path\" as name. Elpi Accumulate File name.'")

let warning_legacy_accumulate ?loc () = warning_legacy_accumulate_gen ?loc true
let warning_legacy_accumulate2 ?loc () = warning_legacy_accumulate_gen ?loc false

let lib_ref id =
  let id = String.concat "." (snd id) in
  try Coqlib.lib_ref id
  with Coqlib.NotFoundRef _ ->
    CErrors.user_err
      Pp.(str "Global reference not found: lib:" ++ str id
          ++ str " (you may need to require some .v file with \
                  `Register ... as " ++ str id ++ str ".`).")

}
GRAMMAR EXTEND Gram
  GLOBAL: term;

  term: LEVEL "0"
    [ [ s = QUOTATION "lp:" -> 
        { 
          let loc = { loc with Loc.bp = loc.Loc.bp + 3 } in
          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.CGenarg arg) } ]
    ]
  ;
END

GRAMMAR EXTEND Gram
  GLOBAL: term;

  term: LEVEL "0"
    [ [ "lib"; ":"; id = qualified_name -> {
          let ref = lib_ref 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 = lib_ref 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 **************************************************************** *)

{
let classify_named_vernac (_,p) = Vernacextend.VtSideff([Names.Id.of_string_soft @@ String.concat "." p],VtNow)
}

VERNAC COMMAND EXTEND ElpiNamed
| #[ atts = any_attribute ] [ "Elpi" "Program" qualified_name(p) elpi_string(s) ] => { classify_named_vernac p } SYNTERP AS atts 
   { 
     let atts = validate_attributes raw_args_attributes atts in
     EV.Synterp.create_program ~atts ~init:s p;
     atts
   } -> {
     EV.Interp.create_program ~atts ~init:s p
   }
| #[ atts = any_attribute ] [ "Elpi" "Command" qualified_name(p) ] => { classify_named_vernac p }  SYNTERP AS atts
   { 
     let atts = validate_attributes raw_args_attributes atts in
     EV.Synterp.create_command ~atts p;
     atts
   } -> {
     EV.Interp.create_command ~atts p }
| #[ atts = any_attribute ] [ "Elpi" "Tactic" qualified_name(p) ] => { classify_named_vernac p }  SYNTERP AS _ 
   { 
     let () = ignore_unknown_attributes atts in
     EV.Synterp.create_tactic p
   } -> {
     EV.Interp.create_tactic p }
| #[ atts = any_attribute ] [ "Elpi" "Db" qualified_name(d) elpi_string(s) ] => { classify_named_vernac d }  SYNTERP AS atts
   { 
     let atts = validate_attributes synterp_attribute atts in
     EV.Synterp.create_db ~atts d ~init:s;
     atts
   } -> {
     EV.Interp.create_db ~atts d ~init:s }
END

VERNAC COMMAND EXTEND ElpiUnnamed CLASSIFIED AS SIDEFF
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" "File" ne_ident_list(ids) ] SYNTERP AS atts {
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_extra_deps ~atts  ids;
     atts
   } -> {
     EV.Interp.accumulate_extra_deps ~atts  ids }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" "Files" ne_ident_list(ids) ] SYNTERP AS atts {
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_extra_deps ~atts  ids;
     atts
   } -> {
     EV.Interp.accumulate_extra_deps ~atts  ids }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" qualified_name(p) "File" ne_ident_list(ids) ] SYNTERP AS atts {
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_extra_deps ~atts  ~program:(snd p) ids;
     atts
   } -> {
     EV.Interp.accumulate_extra_deps ~atts  ~program:(snd p) ids }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" qualified_name(p) "Files" ne_ident_list(ids) ] SYNTERP AS atts {
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_extra_deps ~atts  ~program:(snd p) ids;
     atts
   } -> {
     EV.Interp.accumulate_extra_deps ~atts  ~program:(snd p) ids }

| #[ atts = any_attribute ] [ "Elpi" "Accumulate" "File" string_list(s) ] SYNTERP AS atts { warning_legacy_accumulate ();
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_files ~atts  s;
     atts
   } -> {
     EV.Interp.accumulate_files ~atts  s }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" "File" string_list(s) "From" global(g) ] SYNTERP AS atts { warning_legacy_accumulate2 ();
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_files ~atts  (inlogpath g s);
     atts
   } -> {
     EV.Interp.accumulate_files ~atts  (inlogpath g s) }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" "Files" string_list(s) ] SYNTERP AS atts { warning_legacy_accumulate ();
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_files ~atts  s;
     atts
   } -> {
     EV.Interp.accumulate_files ~atts  s }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" "Files" string_list(s) "From" global(g) ] SYNTERP AS atts { warning_legacy_accumulate2 ();
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_files ~atts  (inlogpath g s);
     atts
   } -> {
     EV.Interp.accumulate_files ~atts  (inlogpath g s) }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" elpi_string(s) ] SYNTERP AS atts {
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_string ~atts  s;
     atts
   } -> {
     EV.Interp.accumulate_string ~atts  s }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" qualified_name(p) "File" string_list(s) ] SYNTERP AS atts { warning_legacy_accumulate ();
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_files ~atts  ~program:(snd p) s;
     atts
   } -> {
     EV.Interp.accumulate_files ~atts  ~program:(snd p) s }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" qualified_name(p) "File" string_list(s) "From" global(g) ] SYNTERP AS atts { warning_legacy_accumulate2 ();
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_files ~atts  ~program:(snd p) (inlogpath g s);
     atts
   } -> {
     EV.Interp.accumulate_files ~atts  ~program:(snd p) (inlogpath g s) }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" qualified_name(p) "Files" string_list(s) ] SYNTERP AS atts { warning_legacy_accumulate ();
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_files ~atts  ~program:(snd p) s;
     atts
   } -> {
     EV.Interp.accumulate_files ~atts  ~program:(snd p) s }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" qualified_name(p) "Files" string_list(s) "From" global(g) ] SYNTERP AS atts { warning_legacy_accumulate2 ();
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_files ~atts  ~program:(snd p) (inlogpath g s);
     atts
   } -> {
     EV.Interp.accumulate_files ~atts  ~program:(snd p) (inlogpath g s) }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" qualified_name(p) elpi_string(s) ] SYNTERP AS atts {
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_string ~atts  ~program:(snd p) s;
     atts
   } -> {
     EV.Interp.accumulate_string ~atts  ~program:(snd p) s }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" "Db" qualified_name(d) ] SYNTERP AS atts {
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_db ~atts  (snd d);
     atts
   } -> {
     EV.Interp.accumulate_db ~atts  (snd d) }
| #[ atts = any_attribute ] [ "Elpi" "Accumulate" qualified_name(p) "Db" qualified_name(d) ] SYNTERP AS atts { 
     let atts = validate_attributes skip_and_synterp_attributes atts in
     EV.Synterp.accumulate_db ~atts  ~program:(snd p) (snd d);
     atts
   } -> {
     EV.Interp.accumulate_db ~atts  ~program:(snd p) (snd d) }

| #[ atts = any_attribute ] [ "Elpi" "Debug" string_list(s) ] SYNTERP AS atts {
     let atts = validate_attributes synterp_attribute atts in
     EV.Synterp.debug  ~atts s;
     atts
   } -> {
     EV.Interp.debug  ~atts s }
| #[ atts = any_attribute ] [ "Elpi" "Trace" "Browser" string_list(s) ] SYNTERP AS atts {
     let atts = validate_attributes synterp_attribute atts in
     EV.Synterp.trace_browser  ~atts s;
     atts
   } -> {
     EV.Interp.trace_browser  ~atts s }
| #[ atts = any_attribute ] [ "Elpi" "Trace" string_list(s) ] SYNTERP AS atts {
     let atts = validate_attributes synterp_attribute atts in
     EV.Synterp.trace  ~atts 1 max_int s [];
     atts
   } -> {
     EV.Interp.trace  ~atts 1 max_int s [] }
| #[ atts = any_attribute ] [ "Elpi" "Trace" string_list(s) "/" string_list(o) ] SYNTERP AS atts {
     let atts = validate_attributes synterp_attribute atts in
     EV.Synterp.trace  ~atts 1 max_int s o;
     atts
   } -> {
     EV.Interp.trace ~atts 1 max_int s o }
| #[ atts = any_attribute ] [ "Elpi" "Trace" int(start) int(stop) string_list(s) ] SYNTERP AS atts {  
     let atts = validate_attributes synterp_attribute atts in
     EV.Synterp.trace  ~atts start stop s [];
     atts
   } -> {
     EV.Interp.trace ~atts start stop s [] }
| #[ atts = any_attribute ] [ "Elpi" "Trace" int(start) int(stop) string_list(s) "/" string_list(o) ] SYNTERP AS atts {
     let atts = validate_attributes synterp_attribute atts in
     EV.Synterp.trace  ~atts start stop s o;
     atts
   } -> {
     EV.Interp.trace  ~atts start stop s o }

| #[ atts = any_attribute ] [ "Elpi" "Trace" "Off" ] SYNTERP AS atts {
     let atts = validate_attributes synterp_attribute atts in
     EV.Synterp.trace  ~atts 0 0 [] [];
     atts
   } -> {
     EV.Interp.trace  ~atts 0 0 [] [] }
| #[ atts = any_attribute ] [ "Elpi" "Bound" "Steps" int(steps) ] SYNTERP AS atts {
     let atts = validate_attributes synterp_attribute atts in
     EV.Synterp.bound_steps  ~atts steps;
     atts
   } -> {
     EV.Interp.bound_steps  ~atts steps }

| #[ atts = any_attribute ] [ "Elpi" "Print" qualified_name(p) string(output) string_list(args) ] SYNTERP AS atts {
     let atts = validate_attributes synterp_attribute atts in
     EV.Synterp.print ~atts ~name:(snd p) ~args output;
     atts
   } -> {
     EV.Interp.print  ~atts ~name:(snd p) ~args output; }

| #[ atts = any_attribute ] [ "Elpi" "Typecheck" ] SYNTERP AS _ 
   { 
     let () = ignore_unknown_attributes atts in
     EV.Synterp.typecheck_program ()
   } -> {
     EV.Interp.typecheck_program () }
| #[ atts = any_attribute ] [ "Elpi" "Typecheck" qualified_name(p) ] SYNTERP AS _ 
   { 
     let () = ignore_unknown_attributes atts in
     EV.Synterp.typecheck_program ~program:(snd p) ()
   } -> {
     let () = ignore_unknown_attributes atts in
     EV.Interp.typecheck_program ~program:(snd p) () }

| #[ atts = any_attribute ] [ "Elpi" "Document" "Builtins" ] -> {
     let () = ignore_unknown_attributes atts in
     EV.document_builtins () }
| #[ atts = any_attribute ] [ "Elpi" "Checker" string(syn) string(int) ] SYNTERP AS _ {
     let () = ignore_unknown_attributes atts in
     EV.Synterp.load_checker syn
   } -> {
     EV.Interp.load_checker int }
| #[ atts = any_attribute ] [ "Elpi" "Printer" string(syn) string(int) ] SYNTERP AS _ {
     let () = ignore_unknown_attributes atts in
     EV.Synterp.load_printer syn
   } -> {
     EV.Interp.load_printer int }
| #[ atts = any_attribute ] [ "Elpi" "Template" "Command" string(syn) string(int) ] SYNTERP AS _ {
     let () = ignore_unknown_attributes atts in
     EV.Synterp.load_command syn
   } -> {
     EV.Interp.load_command int }
| #[ atts = any_attribute ] [ "Elpi" "Template" "Tactic" string(s) ] SYNTERP AS _ {
     let () = ignore_unknown_attributes atts in
     () (* no synterp tactics  EV.Synterp.load_tactic syn *)
   } -> {
     EV.Interp.load_tactic s }
END

VERNAC COMMAND EXTEND ElpiRun CLASSIFIED BY { fun _ -> Vernacextend.(VtSideff ([], VtNow)) }
| #[ atts = any_attribute ] [ "Elpi" "Query" elpi_string(synterp) elpi_string_opt(interp) ] SYNTERP AS syndata
   { 
     let () = ignore_unknown_attributes atts in
     let synterp, interp = match interp with None -> None, synterp | Some interp -> Some synterp, interp in
     match synterp with
     | Some synterp -> EV.Synterp.run_in_program synterp
     | None -> None
   } -> {
     let synterp, interp = match interp with None -> None, synterp | Some interp -> Some synterp, interp in
     EV.Interp.run_in_program ~syndata interp }
| #[ atts = any_attribute ] [ "Elpi" "Query"  qualified_name(p) elpi_string(synterp) elpi_string_opt(interp) ] SYNTERP AS syndata
   { 
     let () = ignore_unknown_attributes atts in
     let synterp, interp = match interp with None -> None, synterp | Some interp -> Some synterp, interp in
     match synterp with
     | Some synterp -> EV.Synterp.run_in_program synterp
     | None -> None
   } -> {
     let synterp, interp = match interp with None -> None, synterp | Some interp -> Some synterp, interp in
     EV.Interp.run_in_program ~program:(snd p) ~syndata interp }
| #[ atts = any_attribute ] [ "Elpi" "Export" qualified_name(p) ] => { Vernacextend.(VtSideff ([],VtNow)) } SYNTERP AS _ {
     EV.export_command (snd p)
  } -> {
     let () = ignore_unknown_attributes atts in  
     ()
  }
| #[ atts = any_attribute ] [ "Elpi" "Export" qualified_name(p) "As" qualified_name(q) ] => { Vernacextend.(VtSideff ([],VtNow)) } SYNTERP AS _ {
     EV.export_command ~as_:(snd q) (snd p)
  } -> {
     let () = ignore_unknown_attributes atts in  
     ()
  }
| #[ atts = any_attribute ] [ "Elpi" qualified_name(p) elpi_cmd_arg_list(args) ] SYNTERP AS syndata
   { 
     let () = ignore_unknown_attributes atts in
     EV.Synterp.run_program (fst p) (snd p) ~atts args
   } -> {
     EV.Interp.run_program (fst p) (snd p) ~atts ~syndata 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: *)