From b090942f20ac8854bf227698d31ca1efec492c47 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 15 Apr 2016 18:26:28 +0200
Subject: Higher-level API for tactic notations.

---
 grammar/tacextend.ml4    | 23 ++++++++++++++++++-----
 grammar/vernacextend.ml4 |  8 ++++++++
 2 files changed, 26 insertions(+), 5 deletions(-)

(limited to 'grammar')

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index e52770aa2..19b6e1b5f 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -45,13 +45,26 @@ let make_fun_clauses loc s l =
   let map c = Compat.make_fun loc [make_clause c] in
   mlexpr_of_list map l
 
+let get_argt e = <:expr< match $e$ with [ Genarg.ExtraArg tag -> tag | _ -> assert False ] >>
+
+let rec mlexpr_of_symbol = function
+| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >>
+| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >>
+| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >>
+| Uentry e ->
+  let arg = get_argt <:expr< $lid:"wit_"^e$ >> in
+  <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >>
+| Uentryl (e, l) ->
+  assert (e = "tactic");
+  let arg = get_argt <:expr< Constrarg.wit_tactic >> in
+  <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>>
+
 let make_prod_item = function
-  | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
+  | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >>
   | ExtNonTerminal (g, id) ->
-    let nt = type_of_user_symbol g in
-    let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in
-      <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
-      $mlexpr_of_prod_entry_key base g$ >>
+    <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >>
 
 let mlexpr_of_clause cl =
   mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index aedaead71..0d4bec69d 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -102,6 +102,14 @@ let make_fun_classifiers loc s c l =
   let cl = List.map (fun x -> Compat.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, id) ->
+    let nt = type_of_user_symbol g in
+    let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in
+      <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
+      $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
-- 
cgit v1.2.3