(************************************************************************)
(*         *   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_head : string option;
  (** The first terminal grammar token *)
  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 : unit option;
  (** Whether this entry is deprecated *)
}

(** Quotation difference for match clauses *)

let default_patt loc =
  (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>)

let make_fun loc cl =
  let l = cl @ [default_patt loc] in
  MLast.ExFun (loc, ploc_vala l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)

let rec make_patt = function
  | [] -> <:patt< [] >>
  | ExtNonTerminal (_, Some p) :: l ->
      <:patt< [ $lid:p$ :: $make_patt l$ ] >>
  | _::l -> make_patt l

let rec make_let e = function
  | [] -> e
  | ExtNonTerminal (g, Some p) :: l ->
      let t = type_of_user_symbol g in
      let loc = MLast.loc_of_expr e in
      let e = make_let e l in
      <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
  | _::l -> make_let e l

let make_clause { r_patt = pt; r_branch = e; } =
  (make_patt pt,
   ploc_vala None,
   make_let e pt)

(* To avoid warnings *)
let mk_ignore c pt =
  let fold accu = function
  | ExtNonTerminal (_, Some p) -> p :: accu
  | _ -> accu
  in
  let names = List.fold_left fold [] pt in
  let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in
  let names = List.fold_left fold <:expr< () >> names in
  <:expr< do { let _ = $names$ in $c$ } >>

let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
  match c ,cg with
  | Some c, _ ->
     (make_patt pt,
      ploc_vala None,
      make_let (mk_ignore c pt) pt)
  | None, Some cg ->
     (make_patt pt,
      ploc_vala None,
      <:expr< fun loc -> $cg$ $str:s$ >>)
  | None, None -> prerr_endline
      (("Vernac entry \""^s^"\" misses a classifier. "^
         "A classifier is a function that returns an expression "^
         "of type vernac_classification (see Vernacexpr). You can: ") ^
       "- " ^ (
        ("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^
          "new vernacular command does not alter the system state;"))^ "\n" ^
       "- " ^ (
        ("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^
          "new vernacular command alters the system state but not the "^
          "parser nor it starts a proof or ends one;"))^ "\n" ^
       "- " ^ (
        ("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^
          "a global function f.  The function f will be called passing "^
          "\""^s^"\" as the only argument;")) ^ "\n" ^
       "- " ^ (
        "Add a specific classifier in each clause using the syntax:"
        ^ "\n" ^("'[...] => [ f ] -> [...]'. "))^ "\n" ^
       ("Specific classifiers have precedence over global "^
         "classifiers. Only one classifier is called.") ^ "\n");
    (make_patt pt,
      ploc_vala None,
      <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>)

let make_fun_clauses loc s l =
  let map c =
    let depr = match c.r_depr with
    | None -> false
    | Some () -> true
    in
    let cl = make_fun loc [make_clause c] in
    <:expr< ($mlexpr_of_bool depr$, $cl$)>>
  in
  mlexpr_of_list map l

let make_fun_classifiers loc s c l =
  let cl = List.map (fun x -> make_fun loc [make_clause_classifier c s x]) l in
  mlexpr_of_list (fun x -> x) cl

let make_prod_item = function
  | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
  | ExtNonTerminal (g, ido) ->
    let nt = type_of_user_symbol g in
    let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
    let typ = match ido with None -> None | Some _ -> Some nt in
      <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ ,
      $mlexpr_of_prod_entry_key base g$ ) ) >>

let mlexpr_of_clause cl =
  let mkexpr { r_head = a; r_patt = b; } = match a with
  | None -> mlexpr_of_list make_prod_item b
  | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b)
  in
  mlexpr_of_list mkexpr cl

let declare_command loc s c nt cl =
  let se = mlexpr_of_string s in
  let gl = mlexpr_of_clause cl in
  let funcl = make_fun_clauses loc s cl in
  let classl = make_fun_classifiers loc s c cl in
  declare_str_items loc
    [ <:str_item< do {
        CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$;
        CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$;
	CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$;
      } >> ]

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:
    [ [ "DEPRECATED" -> () ] ]
  ;
  (* spiwack: comment-by-guessing: it seems that the isolated string
      (which otherwise could have been another argument) is not passed
      to the VernacExtend interpreter function to discriminate between
      the clauses. *)
  rule:
    [ [ "["; s = STRING; l = LIST0 args; "]";
        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
      let () = if s = "" then failwith "Command name is empty." in
      let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
      { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
      | "[" ; "-" ; l = LIST1 args ; "]" ;
        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
      let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
      { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
    ] ]
  ;
  fun_rule:
    [ [ "["; s = STRING; l = LIST0 args; "]";
        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
      let () = if s = "" then failwith "Command name is empty." in
      let b = <:expr< $e$ >> in
      { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
      | "[" ; "-" ; l = LIST1 args ; "]" ;
        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
      let b = <:expr< $e$ >> in
      { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
    ] ]
  ;
  classifier:
    [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun loc -> $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
;;