(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(** Implementation of the VERNAC EXTEND macro. *)

open Q_util
open Argextend

type rule = {
  r_patt : extend_token list;
  (** The remaining tokens of the parsing rule *)
  r_class : MLast.expr option;
  (** An optional classifier for the STM *)
  r_branch : MLast.expr;
  (** The action performed by this rule. *)
  r_depr : bool;
  (** Whether this entry is deprecated *)
}

let rec make_patt r = function
| [] -> r
| ExtNonTerminal (_, Some p) :: l -> <:expr< fun $lid:p$ -> $make_patt r l$ >>
| ExtNonTerminal (_, None) :: l -> <:expr< fun _ -> $make_patt r l$ >>
| ExtTerminal _ :: l -> make_patt r l

let rec mlexpr_of_clause = function
| [] -> <:expr< Vernacentries.TyNil >>
| ExtTerminal s :: cl -> <:expr< Vernacentries.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >>
| ExtNonTerminal (g, id) :: cl ->
  let id = mlexpr_of_option mlexpr_of_string id in
  <:expr< Vernacentries.TyNonTerminal ($id$, $mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>

let make_rule r =
  let ty = mlexpr_of_clause r.r_patt in
  let cmd = make_patt r.r_branch r.r_patt in
  let make_classifier c = make_patt c r.r_patt in
  let classif = mlexpr_of_option make_classifier r.r_class in
  <:expr< Vernacentries.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >>

let declare_command loc s c nt cl =
  let se = mlexpr_of_string s in
  let c = mlexpr_of_option (fun x -> x) c in
  let rules = mlexpr_of_list make_rule cl in
  declare_str_items loc
  [ <:str_item< Vernacentries.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ]

open Pcaml

EXTEND
  GLOBAL: str_item;
  str_item:
    [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; c = OPT classification;
        OPT "|"; l = LIST1 rule SEP "|";
        "END" ->
         declare_command loc s c <:expr<None>> l
      | "VERNAC"; "COMMAND"; "FUNCTIONAL"; "EXTEND"; s = UIDENT; c = OPT classification;
        OPT "|"; l = LIST1 fun_rule SEP "|";
        "END" ->
         declare_command loc s c <:expr<None>> l
      | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification;
        OPT "|"; l = LIST1 rule SEP "|";
        "END" ->
          declare_command loc s c <:expr<Some $lid:nt$>> l
      | "DECLARE"; "PLUGIN"; name = STRING ->
        declare_str_items loc [
          <:str_item< value __coq_plugin_name = $str:name$ >>;
          <:str_item< value _ = Mltop.add_known_module __coq_plugin_name >>;
        ]
      ] ]
  ;
  classification:
    [ [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >>
      | "CLASSIFIED"; "AS"; "SIDEFF" ->
          <:expr< fun _ -> Vernac_classifier.classify_as_sideeff >>
      | "CLASSIFIED"; "AS"; "QUERY" ->
          <:expr< fun _ -> Vernac_classifier.classify_as_query >>
    ] ]
  ;
  deprecation:
    [ [ -> false | "DEPRECATED" -> true ] ]
  ;
  rule:
    [ [ "["; OPT "-"; l = LIST1 args; "]";
        d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
      let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
      { r_patt = l; r_class = c; r_branch = b; r_depr = d; }
    ] ]
  ;
  (** The [OPT "-"] argument serves no purpose nowadays, it is left here for
      backward compatibility. *)
  fun_rule:
    [ [ "["; OPT "-"; l = LIST1 args; "]";
        d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
      { r_patt = l; r_class = c; r_branch = e; r_depr = d; }
    ] ]
  ;
  classifier:
    [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< $c$>> ] ]
  ;
  args:
    [ [ e = LIDENT; "("; s = LIDENT; ")" ->
        let e = parse_user_entry e "" in
        ExtNonTerminal (e, Some s)
      | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
        let e = parse_user_entry e sep in
        ExtNonTerminal (e, Some s)
      | e = LIDENT ->
        let e = parse_user_entry e "" in
        ExtNonTerminal (e, None)
      | s = STRING ->
        ExtTerminal s
    ] ]
  ;
  END
;;