Implementing TACTIC EXTEND in coqpp.

4 files changed, 167 insertions, 20 deletions

diff --git a/grammar/coqpp_ast.mli b/grammar/coqpp_ast.mli
index 245e530ae..39b4d2ab3 100644
--- a/grammar/coqpp_ast.mli
+++ b/grammar/coqpp_ast.mli
@@ -13,14 +13,22 @@ type loc = {
 
 type code = { code : string }
 
+type user_symbol =
+| Ulist1 of user_symbol
+| Ulist1sep of user_symbol * string
+| Ulist0 of user_symbol
+| Ulist0sep of user_symbol * string
+| Uopt of user_symbol
+| Uentry of string
+| Uentryl of string * int
+
 type token_data =
 | TokNone
 | TokName of string
-| TokNameSep of string * string
 
 type ext_token =
 | ExtTerminal of string
-| ExtNonTerminal of string * token_data
+| ExtNonTerminal of user_symbol * token_data
 
 type tactic_rule = {
   tac_toks : ext_token list;
@@ -70,11 +78,18 @@ type grammar_ext = {
   gramext_entries : grammar_entry list;
 }
 
+type tactic_ext = {
+  tacext_name : string;
+  tacext_level : int option;
+  tacext_rules : tactic_rule list;
+}
+
 type node =
 | Code of code
 | Comment of string
+| DeclarePlugin of string
 | GramExt of grammar_ext
 | VernacExt
-| TacticExt of string * tactic_rule list
+| TacticExt of tactic_ext
 
 type t = node list
diff --git a/grammar/coqpp_lex.mll b/grammar/coqpp_lex.mll
index f35766b16..6c6562c20 100644
--- a/grammar/coqpp_lex.mll
+++ b/grammar/coqpp_lex.mll
@@ -83,6 +83,7 @@ let alphanum = ['_' 'a'-'z' 'A'-'Z' '0'-'9' '\'']
 let ident = letterlike alphanum*
 let qualid = ident ('.' ident)*
 let space = [' ' '\t' '\r']
+let number = [ '0'-'9' ]
 
 rule extend = parse
 | "(*" { start_comment (); comment lexbuf }
@@ -92,6 +93,8 @@ rule extend = parse
 | "TACTIC" { TACTIC }
 | "EXTEND" { EXTEND }
 | "END" { END }
+| "DECLARE" { DECLARE }
+| "PLUGIN" { PLUGIN }
 (** Camlp5 specific keywords *)
 | "GLOBAL" { GLOBAL }
 | "FIRST" { FIRST }
@@ -105,6 +108,7 @@ rule extend = parse
 (** Standard *)
 | ident { IDENT (Lexing.lexeme lexbuf) }
 | qualid { QUALID (Lexing.lexeme lexbuf) }
+| number { INT (int_of_string (Lexing.lexeme lexbuf)) }
 | space { extend lexbuf }
 | '\"' { string lexbuf }
 | '\n' { newline lexbuf; extend lexbuf }
diff --git a/grammar/coqpp_main.ml b/grammar/coqpp_main.ml
index 23a5104e2..a4a6b510a 100644
--- a/grammar/coqpp_main.ml
+++ b/grammar/coqpp_main.ml
@@ -55,6 +55,8 @@ let string_split s =
   in
   if len == 0 then [] else split 0
 
+let plugin_name = "__coq_plugin_name"
+
 module GramExt :
 sig
 
@@ -255,7 +257,75 @@ let print_ast chan ext =
   let () = fprintf chan "let _ = @[" in
   let () = fprintf chan "@[<v>%a@]" print_local ext in
   let () = List.iter (fun e -> print_entry chan ext.gramext_name e) ext.gramext_entries in
-  let () = fprintf chan "()@]\n" in
+  let () = fprintf chan "()@]@\n" in
+  ()
+
+end
+
+module TacticExt :
+sig
+
+val print_ast : Format.formatter -> tactic_ext -> unit
+
+end =
+struct
+
+let print_ident chan id =
+  (** Workaround for badly-designed generic arguments lacking a closure *)
+  fprintf chan "Names.Id.of_string_soft \"$%s\"" id
+
+let rec print_symbol chan = function
+| Ulist1 s ->
+  fprintf chan "@[Extend.TUlist1 (%a)@]" print_symbol s
+| Ulist1sep (s, sep) ->
+  fprintf chan "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep
+| Ulist0 s ->
+  fprintf chan "@[Extend.TUlist0 (%a)@]" print_symbol s
+| Ulist0sep (s, sep) ->
+  fprintf chan "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep
+| Uopt s ->
+  fprintf chan "@[Extend.TUopt (%a)@]" print_symbol s
+| Uentry e ->
+  fprintf chan "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e
+| Uentryl (e, l) ->
+  assert (e = "tactic");
+  fprintf chan "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l
+
+let rec print_clause chan = function
+| [] -> fprintf chan "@[TyNil@]"
+| ExtTerminal s :: cl -> fprintf chan "@[TyIdent (\"%s\", %a)@]" s print_clause cl
+| ExtNonTerminal (g, TokNone) :: cl ->
+  fprintf chan "@[TyAnonArg (Loc.tag (%a), %a)@]"
+    print_symbol g print_clause cl
+| ExtNonTerminal (g, TokName id) :: cl ->
+  fprintf chan "@[TyArg (Loc.tag (%a, %a), %a)@]"
+    print_symbol g print_ident id print_clause cl
+
+let rec print_binders chan = function
+| [] -> fprintf chan "ist@ "
+| (ExtTerminal _ | ExtNonTerminal (_, TokNone)) :: rem -> print_binders chan rem
+| (ExtNonTerminal (_, TokName id)) :: rem ->
+  fprintf chan "%s@ %a" id print_binders rem
+
+let print_rule chan r =
+  fprintf chan "@[TyML (%a, @[fun %a -> %s@])@]"
+    print_clause r.tac_toks print_binders r.tac_toks r.tac_body.code
+
+let rec print_rules chan = function
+| [] -> ()
+| [r] -> fprintf chan "(%a)@\n" print_rule r
+| r :: rem -> fprintf chan "(%a);@\n%a" print_rule r print_rules rem
+
+let print_rules chan rules =
+  fprintf chan "Tacentries.([@[<v>%a@]])" print_rules rules
+
+let print_ast chan ext =
+  let pr chan () =
+    let level = match ext.tacext_level with None -> 0 | Some i -> i in
+    fprintf chan "Tacentries.tactic_extend %s \"%s\" ~level:%i %a"
+      plugin_name ext.tacext_name level print_rules ext.tacext_rules
+  in
+  let () = fprintf chan "let () = @[%a@]\n" pr () in
   ()
 
 end
@@ -263,19 +333,10 @@ end
 let pr_ast chan = function
 | Code s -> fprintf chan "%s@\n" s.code
 | Comment s -> fprintf chan "%s@\n" s
+| DeclarePlugin name -> fprintf chan "let %s = \"%s\"@\n" plugin_name name
 | GramExt gram -> fprintf chan "%a@\n" GramExt.print_ast gram
 | VernacExt -> fprintf chan "VERNACEXT@\n"
-| TacticExt (id, rules) ->
-  let pr_tok = function
-  | ExtTerminal s -> Printf.sprintf "%s" s
-  | ExtNonTerminal (s, _) -> Printf.sprintf "%s" s
-  in
-  let pr_tacrule r =
-    let toks = String.concat " " (List.map pr_tok r.tac_toks) in
-    Printf.sprintf "[%s] -> {%s}" toks r.tac_body.code
-  in
-  let rules = String.concat ", " (List.map pr_tacrule rules) in
-  fprintf chan "TACTICEXT (%s, [%s])@\n" id rules
+| TacticExt tac -> fprintf chan "%a@\n" TacticExt.print_ast tac
 
 let () =
   let () =
diff --git a/grammar/coqpp_parse.mly b/grammar/coqpp_parse.mly
index aa22d2717..d7fcc122c 100644
--- a/grammar/coqpp_parse.mly
+++ b/grammar/coqpp_parse.mly
@@ -10,13 +10,60 @@
 
 open Coqpp_ast
 
+let starts s pat =
+  let len = String.length s in
+  let patlen = String.length pat in
+  if patlen <= len && String.sub s 0 patlen = pat then
+    Some (String.sub s patlen (len - patlen))
+  else None
+
+let ends s pat =
+  let len = String.length s in
+  let patlen = String.length pat in
+  if patlen <= len && String.sub s (len - patlen) patlen = pat then
+    Some (String.sub s 0 (len - patlen))
+  else None
+
+let between s pat1 pat2 = match starts s pat1 with
+| None -> None
+| Some s -> ends s pat2  
+
+let without_sep k sep r =
+  if sep <> "" then raise Parsing.Parse_error else k r
+
+let parse_user_entry s sep =
+  let table = [
+    "ne_", "_list", without_sep (fun r -> Ulist1 r);
+    "ne_", "_list_sep", (fun sep r -> Ulist1sep (r, sep));
+    "", "_list", without_sep (fun r -> Ulist0 r);
+    "", "_list_sep", (fun sep r -> Ulist0sep (r, sep));
+    "", "_opt", without_sep (fun r -> Uopt r);
+  ] in
+  let rec parse s sep = function
+  | [] ->
+    let () = without_sep ignore sep () in
+    let s = match s with "hyp" -> "var" | _ -> s in
+    begin match starts s "tactic" with
+    | Some ("0"|"1"|"2"|"3"|"4"|"5") -> Uentryl ("tactic", int_of_string s)
+    | Some _ | None -> Uentry s
+    end
+  | (pat1, pat2, k) :: rem ->
+    match between s pat1 pat2 with
+    | None -> parse s sep rem
+    | Some s ->
+      let r = parse s "" table in
+      k sep r      
+  in
+  parse s sep table
+
 %}
 
 %token <Coqpp_ast.code> CODE
 %token <string> COMMENT
 %token <string> IDENT QUALID
 %token <string> STRING
-%token VERNAC TACTIC GRAMMAR EXTEND END
+%token <int> INT
+%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN
 %token LBRACKET RBRACKET PIPE ARROW COMMA EQUAL
 %token LPAREN RPAREN COLON SEMICOLON
 %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA
@@ -42,11 +89,16 @@ nodes:
 node:
 | CODE { Code $1 }
 | COMMENT { Comment $1 }
+| declare_plugin { $1 }
 | grammar_extend { $1 }
 | vernac_extend { $1 }
 | tactic_extend { $1 }
 ;
 
+declare_plugin:
+| DECLARE PLUGIN STRING { DeclarePlugin $3 }
+;
+
 grammar_extend:
 | GRAMMAR EXTEND qualid_or_ident globals gram_entries END
   { GramExt { gramext_name = $3; gramext_globals = $4; gramext_entries = $5 } }
@@ -57,7 +109,13 @@ vernac_extend:
 ;
 
 tactic_extend:
-| TACTIC EXTEND IDENT tactic_rules END { TacticExt ($3, $4)  }
+| TACTIC EXTEND IDENT tactic_level tactic_rules END
+  { TacticExt { tacext_name = $3; tacext_level = $4; tacext_rules = $5 } }
+;
+
+tactic_level:
+| { None }
+| LEVEL INT { Some $2 }
 ;
 
 tactic_rules:
@@ -77,9 +135,18 @@ ext_tokens:
 
 ext_token:
 | STRING { ExtTerminal $1 }
-| IDENT { ExtNonTerminal ($1, TokNone) }
-| IDENT LPAREN IDENT RPAREN { ExtNonTerminal ($1, TokName $3) }
-| IDENT LPAREN IDENT COMMA STRING RPAREN { ExtNonTerminal ($1, TokNameSep ($3, $5)) }
+| IDENT {
+  let e = parse_user_entry $1 "" in
+  ExtNonTerminal (e, TokNone) 
+  }
+| IDENT LPAREN IDENT RPAREN {
+  let e = parse_user_entry $1 "" in
+  ExtNonTerminal (e, TokName $3)
+  }
+| IDENT LPAREN IDENT COMMA STRING RPAREN {
+  let e = parse_user_entry $1 $5 in
+  ExtNonTerminal (e, TokName $3)
+}
 ;
 
 qualid_or_ident: