(************************************************************************)
(*         *   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 TACTIC EXTEND macro. *)

open Q_util
open Argextend

let plugin_name = <:expr< __coq_plugin_name >>

let rec mlexpr_of_symbol = function
| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >>
| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >>
| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >>
| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >>
| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >>
| Uentry e ->
  let wit = <:expr< $lid:"wit_"^e$ >> in
  <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
| Uentryl (e, l) ->
  assert (e = "tactic");
  let wit = <:expr< $lid:"wit_"^e$ >> in
  <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>

let rec mlexpr_of_clause = function
| [] -> <:expr< TyNil >>
| ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >>
| ExtNonTerminal(g,None) :: cl ->
  <:expr< TyAnonArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
| ExtNonTerminal(g,Some id) :: cl ->
  <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_string id$, $mlexpr_of_clause cl$) >>

let rec binders_of_clause e = function
| [] -> <:expr< fun ist -> $e$ >>
| ExtNonTerminal(_,None) :: cl -> binders_of_clause e cl
| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_clause e cl$ >>
| _ :: cl -> binders_of_clause e cl

open Pcaml

EXTEND
  GLOBAL: str_item;
  str_item:
    [ [ "TACTIC"; "EXTEND"; s = tac_name;
        depr = OPT [ "DEPRECATED"; depr = LIDENT -> depr ];
        level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ];
        OPT "|"; l = LIST1 tacrule SEP "|";
        "END" ->
        let level = match level with Some i -> int_of_string i | None -> 0 in
        let level = mlexpr_of_int level in
        let depr = mlexpr_of_option (fun l -> <:expr< $lid:l$ >>) depr in
        let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in
        declare_str_items loc [ <:str_item< Tacentries.tactic_extend
          $plugin_name$ $str:s$ ~{ level = $level$ } ?{ deprecation =
          $depr$ } $l$ >> ] ] ]
  ;
  tacrule:
    [ [ "["; l = LIST1 tacargs; "]";
        "->"; "["; e = Pcaml.expr; "]" ->
         <:expr< TyML($mlexpr_of_clause l$, $binders_of_clause e l$) >>
    ] ]
  ;

  tacargs:
    [ [ 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 ->
	let () = if s = "" then failwith "Empty terminal." in
        ExtTerminal s
    ] ]
  ;
  tac_name:
    [ [ s = LIDENT -> s
      | s = UIDENT -> s
    ] ]
  ;
  END