(************************************************************************)
(*         *   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)         *)
(************************************************************************)

open Q_util

let loc = Ploc.dummy

IFDEF STRICT THEN
  let ploc_vala x = Ploc.VaVal x
ELSE
  let ploc_vala x = x
END

let declare_str_items loc l =
  MLast.StDcl (loc, ploc_vala l) (* correspond to <:str_item< declare $list:l'$ end >> *)

let declare_arg loc s e =
  declare_str_items loc [
    <:str_item< value ($lid:"wit_"^s$, $lid:s$) = $e$ >>;
    (** Prevent the unused variable warning *)
    <:str_item< value _ = ($lid:"wit_"^s$, $lid:s$) >>;
  ]

let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >>

let rec make_wit loc = function
  | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
  | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
  | PairArgType (t1,t2) ->
      <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >>
  | ExtraArgType s -> mk_extraarg loc s

let is_self s = function
| ExtraArgType s' -> s = s'
| _ -> false

let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >>
let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >>
let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>

let make_act loc act pil =
  let rec make = function
    | [] -> <:expr< (fun loc -> $act$) >>
    | ExtNonTerminal (_, None) :: tl -> <:expr< (fun $lid:"_"$ -> $make tl$) >>
    | ExtNonTerminal (_, Some p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
    | ExtTerminal _ :: tl ->
	<:expr< (fun _ -> $make tl$) >> in
  make (List.rev pil)

let make_prod_item self = function
  | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >>
  | ExtNonTerminal (Uentry e, _) when e = self -> <:expr< Extend.Aself >>
  | ExtNonTerminal (g, _) ->
    let base s = <:expr< $lid:s$ >> in
    mlexpr_of_prod_entry_key base g

let rec make_prod self = function
| [] -> <:expr< Extend.Stop >>
| item :: prods -> <:expr< Extend.Next $make_prod self prods$ $make_prod_item self item$ >>

let make_rule loc self (prods,act) =
  <:expr< Extend.Rule $make_prod self (List.rev prods)$ $make_act loc act prods$ >>

let is_ident x = function
| <:expr< $lid:s$ >> -> (s : string) = x
| _ -> false

let make_extend loc self cl = match cl with
| [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act ->
  (** Special handling of identity arguments by not redeclaring an entry *)
  <:expr< Vernacentries.Arg_alias $lid:e$ >>
| _ ->
  <:expr< Vernacentries.Arg_rules $mlexpr_of_list (make_rule loc self) (List.rev cl)$ >>

let warning_deprecated prefix s = function
| None -> ()
| Some _ ->
  Printf.eprintf "Deprecated [%sTYPED AS] clause in [ARGUMENT EXTEND %s]. \
                  Use [TYPED AS] instead.\n%!" prefix s

let get_type s = function
| None -> None
| Some typ ->
  if is_self s typ then
    let () = Printf.eprintf "Redundant [TYPED AS] clause in [ARGUMENT EXTEND %s].\n%!" s in
    None
  else Some typ

let declare_tactic_argument loc s (typ, f, g, h) cl =
  let se = mlexpr_of_string s in
  let typ, pr = match typ with
    | `Uniform (typ, pr) ->
      let typ = get_type s typ in
      typ, <:expr< ($lid:pr$, $lid:pr$, $lid:pr$) >>
    | `Specialized (a, rpr, c, gpr, e, tpr) ->
      let () = warning_deprecated "RAW_" s a in
      let () = warning_deprecated "GLOB_" s c in
      let typ = get_type s e in
      typ, <:expr< ($lid:rpr$, $lid:gpr$, $lid:tpr$) >>
  in
  let glob = match g, typ with
  | Some f, (None | Some _) ->
    <:expr< Tacentries.ArgInternFun (fun ist v -> (ist, $lid:f$ ist v)) >>
  | None, Some typ ->
    <:expr< Tacentries.ArgInternWit $make_wit loc typ$ >>
  | None, None ->
    <:expr< Tacentries.ArgInternFun (fun ist v -> (ist, v)) >>
  in
  let interp = match f, typ with
  | Some f, (None | Some _) ->
    <:expr< Tacentries.ArgInterpLegacy $lid:f$ >>
  | None, Some typ ->
    <:expr< Tacentries.ArgInterpWit $make_wit loc typ$ >>
  | None, None ->
    <:expr< Tacentries.ArgInterpRet >>
  in
  let subst = match h, typ with
  | Some f, (None | Some _) ->
    <:expr< Tacentries.ArgSubstFun $lid:f$ >>
  | None, Some typ ->
    <:expr< Tacentries.ArgSubstWit $make_wit loc typ$ >>
  | None, None ->
    <:expr< Tacentries.ArgSubstFun (fun s v -> v) >>
  in
  let dyn = mlexpr_of_option (fun typ -> <:expr< Geninterp.val_tag $make_topwit loc typ$ >>) typ in
  declare_arg loc s <:expr< Tacentries.argument_extend ~{ name = $se$ } {
    Tacentries.arg_parsing = $make_extend loc s cl$;
    Tacentries.arg_tag = $dyn$;
    Tacentries.arg_intern = $glob$;
    Tacentries.arg_subst = $subst$;
    Tacentries.arg_interp = $interp$;
    Tacentries.arg_printer = $pr$
  } >>

let declare_vernac_argument loc s pr cl =
  let se = mlexpr_of_string s in
  let pr_rules = match pr with
    | None -> <:expr< fun _ -> Pp.str $str:"[No printer for "^s^"]"$ >>
    | Some pr -> <:expr< $lid:pr$ >> in
  declare_arg loc s <:expr< Vernacentries.vernac_argument_extend ~{ name = $se$ } {
    Vernacentries.arg_printer = $pr_rules$;
    Vernacentries.arg_parsing = $make_extend loc s cl$
  } >>

open Pcaml

EXTEND
  GLOBAL: str_item;
  str_item:
    [ [ "ARGUMENT"; "EXTEND"; s = entry_name;
        header = argextend_header;
        OPT "|"; l = LIST1 argrule SEP "|";
        "END" ->
         declare_tactic_argument loc s header l
      | "VERNAC"; "ARGUMENT"; "EXTEND"; s = entry_name;
        pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr];
        OPT "|"; l = LIST1 argrule SEP "|";
        "END" ->
         declare_vernac_argument loc s pr l ] ]
  ;
  argextend_specialized:
  [ [ rawtyp = OPT [ "RAW_TYPED"; "AS"; rawtyp = argtype -> rawtyp ];
      "RAW_PRINTED"; "BY"; rawpr = LIDENT;
      globtyp = OPT [ "GLOB_TYPED"; "AS"; globtyp = argtype -> globtyp ];
      "GLOB_PRINTED"; "BY"; globpr = LIDENT ->
      (rawtyp, rawpr, globtyp, globpr) ] ]
  ;
  argextend_header:
    [ [ typ = OPT [ "TYPED"; "AS"; typ = argtype -> typ ];
        "PRINTED"; "BY"; pr = LIDENT;
        f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ];
        g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ];
        h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ];
        special = OPT argextend_specialized ->
        let repr = match special with
        | None -> `Uniform (typ, pr)
        | Some (rtyp, rpr, gtyp, gpr) -> `Specialized (rtyp, rpr, gtyp, gpr, typ, pr)
        in
        (repr, f, g, h) ] ]
  ;
  argtype:
    [ "2"
      [ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ]
    | "1"
      [ e = argtype; LIDENT "list" -> ListArgType e
      | e = argtype; LIDENT "option" -> OptArgType e ]
    | "0"
      [ e = LIDENT ->
        let e = parse_user_entry e "" in
        type_of_user_symbol e
      | "("; e = argtype; ")" -> e ] ]
  ;
  argrule:
    [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ]
  ;
  genarg:
    [ [ 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
    ] ]
  ;
  entry_name:
    [ [ s = LIDENT -> s
      | UIDENT -> failwith "Argument entry names must be lowercase"
      ] ]
  ;
  END