Implement ARGUMENT EXTEND in coqpp.

4 files changed, 313 insertions, 28 deletions

diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
index 6f697f5d49..93a07cff9d 100644
--- a/coqpp/coqpp_ast.mli
+++ b/coqpp/coqpp_ast.mli
@@ -60,6 +60,17 @@ and gram_prod = {
   gprod_body : code;
 }
 
+type symb =
+| SymbToken of string * string option
+| SymbEntry of string * string option
+| SymbSelf
+| SymbNext
+| SymbList0 of symb * symb option
+| SymbList1 of symb * symb option
+| SymbOpt of symb
+| SymbRules of ((string option * symb) list * code) list
+| SymbQuote of string (** Not used by GRAMMAR EXTEND *)
+
 type gram_rule = {
   grule_label : string option;
   grule_assoc : assoc option;
@@ -104,12 +115,38 @@ type vernac_ext = {
   vernacext_rules : vernac_rule list;
 }
 
+type vernac_argument_ext = {
+  vernacargext_name : string;
+  vernacargext_printer : code option;
+  vernacargext_rules : tactic_rule list;
+}
+
+type argument_type =
+| ListArgType of argument_type
+| OptArgType of argument_type
+| PairArgType of argument_type * argument_type
+| ExtraArgType of string
+
+type argument_ext = {
+  argext_name : string;
+  argext_rules : tactic_rule list;
+  argext_type : argument_type option;
+  argext_interp : code option;
+  argext_glob : code option;
+  argext_subst : code option;
+  argext_rprinter : code option;
+  argext_gprinter : code option;
+  argext_tprinter : code option;
+}
+
 type node =
 | Code of code
 | Comment of string
 | DeclarePlugin of string
 | GramExt of grammar_ext
 | VernacExt of vernac_ext
+| VernacArgumentExt of vernac_argument_ext
 | TacticExt of tactic_ext
+| ArgumentExt of argument_ext
 
 type t = node list
diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll
index d809b824df..cdea4b99ef 100644
--- a/coqpp/coqpp_lex.mll
+++ b/coqpp/coqpp_lex.mll
@@ -103,6 +103,14 @@ rule extend = parse
 | "PLUGIN" { PLUGIN }
 | "DEPRECATED" { DEPRECATED }
 | "CLASSIFIED" { CLASSIFIED }
+| "PRINTED" { PRINTED }
+| "TYPED" { TYPED }
+| "INTERPRETED" { INTERPRETED }
+| "GLOBALIZED" { GLOBALIZED }
+| "SUBSTITUTED" { SUBSTITUTED }
+| "ARGUMENT" { ARGUMENT }
+| "RAW_PRINTED" { RAW_PRINTED }
+| "GLOB_PRINTED" { GLOB_PRINTED }
 | "BY" { BY }
 | "AS" { AS }
 (** Camlp5 specific keywords *)
@@ -133,6 +141,7 @@ rule extend = parse
 | '(' { LPAREN }
 | ')' { RPAREN }
 | '=' { EQUAL }
+| '*' { STAR }
 | _ { lex_error lexbuf "syntax error" }
 | eof { EOF }
 
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 89b4d340b2..5314806c24 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -14,6 +14,9 @@ let fatal msg =
   let () = Format.eprintf "Error: %s@\n%!" msg in
   exit 1
 
+let dummy_loc = { loc_start = Lexing.dummy_pos; loc_end = Lexing.dummy_pos }
+let mk_code s = { code = s; loc = dummy_loc }
+
 let pr_loc loc =
   let file = loc.loc_start.pos_fname in
   let line = loc.loc_start.pos_lnum in
@@ -97,9 +100,16 @@ let rec print_symbol fmt = function
   assert (e = "tactic");
   fprintf fmt "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l
 
+let print_string fmt s = fprintf fmt "\"%s\"" s
+
+let print_opt fmt pr = function
+| None -> fprintf fmt "None"
+| Some x -> fprintf fmt "Some@ @[(%a)@]" pr x
+
 module GramExt :
 sig
 
+val print_extrule : Format.formatter -> (symb list * string option list * code) -> unit
 val print_ast : Format.formatter -> grammar_ext -> unit
 
 end =
@@ -135,12 +145,6 @@ let print_local fmt ext =
     let () = List.iter iter locals in
     fprintf fmt "in@ "
 
-let print_string fmt s = fprintf fmt "\"%s\"" s
-
-let print_opt fmt pr = function
-| None -> fprintf fmt "None"
-| Some x -> fprintf fmt "Some@ (%a)" pr x
-
 let print_position fmt pos = match pos with
 | First -> fprintf fmt "Extend.First"
 | Last -> fprintf fmt "Extend.Last"
@@ -153,16 +157,6 @@ let print_assoc fmt = function
 | RightA -> fprintf fmt "Extend.RightA"
 | NonA -> fprintf fmt "Extend.NonA"
 
-type symb =
-| SymbToken of string * string option
-| SymbEntry of string * string option
-| SymbSelf
-| SymbNext
-| SymbList0 of symb * symb option
-| SymbList1 of symb * symb option
-| SymbOpt of symb
-| SymbRules of ((string option * symb) list * code) list
-
 let is_token s = match string_split s with
 | [s] -> is_uident s
 | _ -> false
@@ -232,9 +226,12 @@ let print_tok fmt = function
 
 let rec print_prod fmt p =
   let (vars, tkns) = List.split p.gprod_symbs in
-  let f = (vars, p.gprod_body) in
-  let tkn = List.rev_map parse_tokens tkns in
-  fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun f
+  let tkn = List.map parse_tokens tkns in
+  print_extrule fmt (tkn, vars, p.gprod_body)
+
+and print_extrule fmt (tkn, vars, body) =
+  let tkn = List.rev tkn in
+  fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun (vars, body)
 
 and print_symbols fmt = function
 | [] -> fprintf fmt "Extend.Stop"
@@ -271,6 +268,8 @@ and print_symbol fmt tkn = match tkn with
   in
   let pr fmt rules = print_list fmt pr rules in
   fprintf fmt "(Extend.Arules %a)" pr (List.rev rules)
+| SymbQuote c ->
+  fprintf fmt "(%s)" c
 
 let print_rule fmt r =
   let pr_lvl fmt lvl = print_opt fmt print_string lvl in
@@ -303,11 +302,16 @@ struct
 
 let print_rule_classifier fmt r = match r.vernac_class with
 | None -> fprintf fmt "None"
-| Some f -> fprintf fmt "Some @[(fun %a-> %s)@]" print_binders r.vernac_toks f.code
+| Some f ->
+  let no_binder = function ExtTerminal _ -> true | ExtNonTerminal _ -> false in
+  if List.for_all no_binder r.vernac_toks then
+    fprintf fmt "Some @[%a@]" print_code f
+  else
+    fprintf fmt "Some @[(fun %a-> %a)@]" print_binders r.vernac_toks print_code f
 
 let print_body fmt r =
-  fprintf fmt "@[(fun %a~atts@ ~st@ -> let () = %s in st)@]"
-    print_binders r.vernac_toks r.vernac_body.code
+  fprintf fmt "@[(fun %a~atts@ ~st@ -> let () = %a in st)@]"
+    print_binders r.vernac_toks print_code r.vernac_body
 
 let rec print_sig fmt = function
 | [] -> fprintf fmt "@[Vernacentries.TyNil@]"
@@ -335,7 +339,7 @@ let print_classifier fmt = function
 
 let print_entry fmt = function
 | None -> fprintf fmt "None"
-| Some e -> fprintf fmt "Some (%s)" e.code
+| Some e -> fprintf fmt "(Some (%s))" e.code
 
 let print_ast fmt ext =
   let pr fmt () =
@@ -364,7 +368,7 @@ let rec print_clause fmt = function
     print_symbol g print_clause cl
 
 let print_rule fmt r =
-  fprintf fmt "@[Tacentries.TyML (%a, @[fun %aist@ -> %a@])@]"
+  fprintf fmt "@[Tacentries.TyML (%a, @[(fun %aist@ -> %a)@])@]"
     print_clause r.tac_toks print_binders r.tac_toks print_code r.tac_body
 
 let print_rules fmt rules =
@@ -388,6 +392,161 @@ let print_ast fmt ext =
 
 end
 
+module VernacArgumentExt :
+sig
+
+val print_ast : Format.formatter -> vernac_argument_ext -> unit
+val print_rules : Format.formatter -> string * tactic_rule list -> unit
+
+end =
+struct
+
+let terminal s =
+  let c = Printf.sprintf "Extend.Atoken (CLexer.terminal \"%s\")" s in
+  SymbQuote c
+
+let rec parse_symb self = function
+| Ulist1 s -> SymbList1 (parse_symb self s, None)
+| Ulist1sep (s, sep) -> SymbList1 (parse_symb self s, Some (terminal sep))
+| Ulist0 s -> SymbList0 (parse_symb self s, None)
+| Ulist0sep (s, sep) -> SymbList0 (parse_symb self s, Some (terminal sep))
+| Uopt s -> SymbOpt (parse_symb self s)
+| Uentry e -> if e = self then SymbSelf else SymbEntry (e, None)
+| Uentryl (e, l) ->
+  assert (e = "tactic");
+  if l = 5 then SymbEntry ("Pltac.binder_tactic", None)
+  else SymbEntry ("Pltac.tactic_expr", Some (string_of_int l))
+
+let parse_token self = function
+| ExtTerminal s -> (terminal s, None)
+| ExtNonTerminal (e, TokNone) -> (parse_symb self e, None)
+| ExtNonTerminal (e, TokName s) -> (parse_symb self e, Some s)
+
+let parse_rule self r =
+  let symbs = List.map (fun t -> parse_token self t) r.tac_toks in
+  let symbs, vars = List.split symbs in
+  (symbs, vars, r.tac_body)
+
+let print_rules fmt (name, rules) =
+  (** Rules are reversed. *)
+  let rules = List.rev rules in
+  let rules = List.map (fun r -> parse_rule name r) rules in
+  let pr fmt l = print_list fmt (fun fmt r -> fprintf fmt "(%a)" GramExt.print_extrule r) l in
+  match rules with
+  | [([SymbEntry (e, None)], [Some s], { code = c } )] when String.trim c = s ->
+    (** This is a horrible hack to work aroud limitations of camlp5 regarding
+        factorization of parsing rules. It allows to recognize rules of the
+        form [ entry(x) ] -> [ x ] so as not to generate a proxy entry and
+        reuse the same entry directly. *)
+    fprintf fmt "@[Vernacentries.Arg_alias (%s)@]" e
+  | _ -> fprintf fmt "@[Vernacentries.Arg_rules (%a)@]" pr rules
+
+let print_printer fmt = function
+| None -> fprintf fmt "@[fun _ -> Pp.str \"missing printer\"@]"
+| Some f -> print_code fmt f
+
+let print_ast fmt arg =
+  let name = arg.vernacargext_name in
+  let pr fmt () =
+    fprintf fmt "Vernacentries.vernac_argument_extend ~name:%a @[{@\n\
+      Vernacentries.arg_parsing = %a;@\n\
+      Vernacentries.arg_printer = %a;@\n}@]"
+      print_string name print_rules (name, arg.vernacargext_rules)
+      print_printer arg.vernacargext_printer
+  in
+  fprintf fmt "let (wit_%s, %s) = @[%a@]@\nlet _ = (wit_%s, %s)@\n"
+    name name pr () name name
+
+end
+
+module ArgumentExt :
+sig
+
+val print_ast : Format.formatter -> argument_ext -> unit
+
+end =
+struct
+
+let rec print_argtype fmt = function
+| ExtraArgType s ->
+  fprintf fmt "Geninterp.val_tag (Genarg.topwit wit_%s)" s
+| PairArgType (arg1, arg2) ->
+  fprintf fmt "Geninterp.Val.Pair (@[(%a)@], @[(%a)@])" print_argtype arg1 print_argtype arg2
+| ListArgType arg ->
+  fprintf fmt "Geninterp.Val.List @[(%a)@]" print_argtype arg
+| OptArgType arg ->
+  fprintf fmt "Geninterp.Val.Opt @[(%a)@]" print_argtype arg
+
+let rec print_wit fmt = function
+| ExtraArgType s ->
+  fprintf fmt "wit_%s" s
+| PairArgType (arg1, arg2) ->
+  fprintf fmt "Genarg.PairArg (@[(%a)@], @[(%a)@])" print_wit arg1 print_wit arg2
+| ListArgType arg ->
+  fprintf fmt "Genarg.ListArg @[(%a)@]" print_wit arg
+| OptArgType arg ->
+  fprintf fmt "Genarg.OptArg @[(%a)@]" print_wit arg
+
+let print_ast fmt arg =
+  let name = arg.argext_name in
+  let pr_tag fmt t = print_opt fmt print_argtype t in
+  let intern fmt () = match arg.argext_glob, arg.argext_type with
+  | Some f, (None | Some _) ->
+    fprintf fmt "@[Tacentries.ArgInternFun ((fun f ist v -> (ist, f ist v)) (%a))@]" print_code f
+  | None, Some t ->
+    fprintf fmt "@[Tacentries.ArgInternWit (%a)@]" print_wit t
+  | None, None ->
+    fprintf fmt "@[Tacentries.ArgInternFun (fun ist v -> (ist, v))@]"
+  in
+  let subst fmt () = match arg.argext_subst, arg.argext_type with
+  | Some f, (None | Some _) ->
+    fprintf fmt "@[Tacentries.ArgSubstFun (%a)@]" print_code f
+  | None, Some t ->
+    fprintf fmt "@[Tacentries.ArgSubstWit (%a)@]" print_wit t
+  | None, None ->
+    fprintf fmt "@[Tacentries.ArgSubstFun (fun s v -> v)@]"
+  in
+  let interp fmt () = match arg.argext_interp, arg.argext_type with
+  | Some f, (None | Some _) ->
+    fprintf fmt "@[Tacentries.ArgInterpLegacy (%a)@]" print_code f
+  | None, Some t ->
+    fprintf fmt "@[Tacentries.ArgInterpWit (%a)@]" print_wit t
+  | None, None ->
+    fprintf fmt "@[Tacentries.ArgInterpRet@]"
+  in
+  let default_printer = mk_code "fun _ _ _ _ -> Pp.str \"missing printer\"" in
+  let rpr = match arg.argext_rprinter, arg.argext_tprinter with
+  | Some f, (None | Some _) -> f
+  | None, Some f -> f
+  | None, None -> default_printer
+  in
+  let gpr = match arg.argext_gprinter, arg.argext_tprinter with
+  | Some f, (None | Some _) -> f
+  | None, Some f -> f
+  | None, None -> default_printer
+  in
+  let tpr = match arg.argext_tprinter with
+  | Some f -> f
+  | None -> default_printer
+  in
+  let pr fmt () =
+    fprintf fmt "Tacentries.argument_extend ~name:%a @[{@\n\
+      Tacentries.arg_parsing = %a;@\n\
+      Tacentries.arg_tag = @[%a@];@\n\
+      Tacentries.arg_intern = @[%a@];@\n\
+      Tacentries.arg_subst = @[%a@];@\n\
+      Tacentries.arg_interp = @[%a@];@\n\
+      Tacentries.arg_printer = @[((%a), (%a), (%a))@];@\n}@]"
+      print_string name
+      VernacArgumentExt.print_rules (name, arg.argext_rules)
+      pr_tag arg.argext_type
+      intern () subst () interp () print_code rpr print_code gpr print_code tpr
+  in
+  fprintf fmt "let (wit_%s, %s) = @[%a@]@\nlet _ = (wit_%s, %s)@\n"
+    name name pr () name name
+
+end
+
 let declare_plugin fmt name =
   fprintf fmt "let %s = \"%s\"@\n" plugin_name name;
   fprintf fmt "let _ = Mltop.add_known_module %s@\n" plugin_name
@@ -398,7 +557,9 @@ let pr_ast fmt = function
 | DeclarePlugin name -> declare_plugin fmt name
 | GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram
 | VernacExt vernac -> fprintf fmt "%a@\n" VernacExt.print_ast vernac
+| VernacArgumentExt arg -> fprintf fmt "%a@\n" VernacArgumentExt.print_ast arg
 | TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac
+| ArgumentExt arg -> fprintf fmt "%a@\n" ArgumentExt.print_ast arg
 
 let () =
   let () =
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly
index 31f234c37f..1fb5461b21 100644
--- a/coqpp/coqpp_parse.mly
+++ b/coqpp/coqpp_parse.mly
@@ -43,7 +43,7 @@ let parse_user_entry s sep =
   | [] ->
     let () = without_sep ignore sep () in
     begin match starts s "tactic" with
-    | Some ("0"|"1"|"2"|"3"|"4"|"5") -> Uentryl ("tactic", int_of_string s)
+    | Some ("0"|"1"|"2"|"3"|"4"|"5" as s) -> Uentryl ("tactic", int_of_string s)
     | Some _ | None -> Uentry s
     end
   | (pat1, pat2, k) :: rem ->
@@ -62,9 +62,10 @@ let parse_user_entry s sep =
 %token <string> IDENT QUALID
 %token <string> STRING
 %token <int> INT
-%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED
-%token COMMAND CLASSIFIED BY AS
-%token LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL
+%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT
+%token RAW_PRINTED GLOB_PRINTED
+%token COMMAND CLASSIFIED PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS
+%token LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR
 %token LPAREN RPAREN COLON SEMICOLON
 %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA
 %token EOF
@@ -93,6 +94,7 @@ node:
 | grammar_extend { $1 }
 | vernac_extend { $1 }
 | tactic_extend { $1 }
+| argument_extend { $1 }
 ;
 
 declare_plugin:
@@ -104,6 +106,82 @@ grammar_extend:
   { GramExt { gramext_name = $3; gramext_globals = $4; gramext_entries = $5 } }
 ;
 
+argument_extend:
+| ARGUMENT EXTEND IDENT
+    typed_opt
+    printed_opt
+    interpreted_opt
+    globalized_opt
+    substituted_opt
+    raw_printed_opt
+    glob_printed_opt
+    tactic_rules
+  END
+  { ArgumentExt {
+    argext_name = $3;
+    argext_rules = $11;
+    argext_rprinter = $9;
+    argext_gprinter = $10;
+    argext_tprinter = $5;
+    argext_interp = $6;
+    argext_glob = $7;
+    argext_subst = $8;
+    argext_type = $4;
+  } }
+| VERNAC ARGUMENT EXTEND IDENT printed_opt tactic_rules END
+  { VernacArgumentExt {
+    vernacargext_name = $4;
+    vernacargext_printer = $5;
+    vernacargext_rules = $6;
+  } }
+;
+
+printed_opt:
+| { None }
+| PRINTED BY CODE { Some $3 }
+;
+
+raw_printed_opt:
+| { None }
+| RAW_PRINTED BY CODE { Some $3 }
+;
+
+glob_printed_opt:
+| { None }
+| GLOB_PRINTED BY CODE { Some $3 }
+;
+
+interpreted_opt:
+| { None }
+| INTERPRETED BY CODE { Some $3 }
+;
+
+globalized_opt:
+| { None }
+| GLOBALIZED BY CODE { Some $3 }
+;
+
+substituted_opt:
+| { None }
+| SUBSTITUTED BY CODE { Some $3 }
+;
+
+typed_opt:
+| { None }
+| TYPED AS argtype { Some $3 }
+;
+
+argtype:
+| IDENT { ExtraArgType $1 }
+| argtype IDENT {
+    match $2 with
+    | "list" -> ListArgType $1
+    | "option" ->  OptArgType $1
+    | _ -> raise Parsing.Parse_error
+  }
+| LPAREN argtype STAR argtype RPAREN { PairArgType ($2, $4) }
+;
+
 vernac_extend:
 | VERNAC vernac_entry EXTEND IDENT vernac_classifier vernac_rules END
   { VernacExt {