From b16633a5dc044e5d95c73b4c912ec7232f9caf12 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Mon, 23 Oct 2017 14:27:04 +0200
Subject: Make most of TACTIC EXTEND macros runtime calls.

Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic
and its parsing rule. Instead, we make it generate a typed AST that is
passed to the parser and a generic tactic execution routine.

PMP has written a small parser that can generate the same typed ASTs
without relying on camlp5, which is overkill for such simple macros.
---
 lib/genarg.ml  | 13 +++++++------
 lib/genarg.mli |  3 +++
 2 files changed, 10 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/genarg.ml b/lib/genarg.ml
index cf3a2bee7..209d1b271 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -174,19 +174,22 @@ sig
   val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option
 end
 
+let get_arg_tag = function
+| ExtraArg s -> s
+| _ -> assert false
+
 module Register (M : GenObj) =
 struct
   module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end)
   let arg0_map = ref GenMap.empty
 
-  let register0 arg f = match arg with
-  | ExtraArg s ->
+  let register0 arg f =
+    let s = get_arg_tag arg in
     if GenMap.mem s !arg0_map then
       let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in
       CErrors.anomaly msg
     else
       arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map
-  | _ -> assert false
 
   let get_obj0 name =
     try
@@ -199,8 +202,6 @@ struct
 
   (** For now, the following function is quite dummy and should only be applied
       to an extra argument type, otherwise, it will badly fail. *)
-  let obj t = match t with
-  | ExtraArg s -> get_obj0 s
-  | _ -> assert false
+  let obj t = get_obj0 @@ get_arg_tag t
 
 end
diff --git a/lib/genarg.mli b/lib/genarg.mli
index d49cb334a..bb85f99e3 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -159,6 +159,9 @@ val unquote : ('a, 'co) abstract_argument_type -> argument_type
 
   This is boilerplate code used here and there in the code of Coq. *)
 
+val get_arg_tag : ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c) ArgT.tag
+(** Works only on base objects (ExtraArg), otherwise fails badly. *)
+
 module type GenObj =
 sig
   type ('raw, 'glb, 'top) obj
-- 
cgit v1.2.3