From 010775eba60ea89645792b48a0686ff15c4ebcb5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 25 Oct 2015 18:43:32 +0100
Subject: Pcoq entries are given a proper module.

Entries defined in the Pcoq AST of symbols must be marshallable, because they
are present in the libstack. Yet, CAMLP4/5 entries are not marshallable as
they contain functional values. This is why the Pcoq module used a pair
[string * string] to describe entries. It is obviously type-unsafe, so
we define a new abstract type in its own module. There is a little issue
though, which is that our entries and CAMLP4/5 entries must be kept
synchronized through an association table. The Pcoq module tries to
maintain this invariant.
---
 grammar/grammar.mllib |  1 +
 grammar/q_util.ml4    | 13 ++++++++++---
 grammar/tacextend.ml4 |  6 +++++-
 3 files changed, 16 insertions(+), 4 deletions(-)

(limited to 'grammar')

diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 60ea0df026..7e4eea641b 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -51,6 +51,7 @@ Constrexpr_ops
 Compat
 Tok
 Lexer
+Entry
 Pcoq
 G_prim
 G_tactic
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 20c83dfafa..5ec7510f79 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -58,6 +58,13 @@ let rec mlexpr_of_prod_entry_key : type s a. (s, a) Pcoq.entry_key -> _ = functi
   | Pcoq.Amodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >>
   | Pcoq.Aself -> <:expr< Pcoq.Aself >>
   | Pcoq.Anext -> <:expr< Pcoq.Anext >>
-  | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:s$) >>
-  | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry ($str:u$, $str:s$) >>
-  | Pcoq.Aentryl ((u,s), l) -> <:expr< Pcoq.Aentryl ($str:u$, $str:s$) $mlexpr_of_int l$ >>
+  | Pcoq.Aentry e ->
+    begin match Entry.repr e with
+    | Entry.Dynamic s -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:s$) >>
+    | Entry.Static (u, s) -> <:expr< Pcoq.Aentry (Entry.unsafe_of_name ($str:u$, $str:s$)) >>
+    end
+  | Pcoq.Aentryl (e, l) ->
+    begin match Entry.repr e with
+    | Entry.Dynamic s -> <:expr< Pcoq.Aentryl (Pcoq.name_of_entry $lid:s$) >>
+    | Entry.Static (u, s) -> <:expr< Pcoq.Aentryl (Entry.unsafe_of_name ($str:u$, $str:s$)) $mlexpr_of_int l$ >>
+    end
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 70151cef1b..4709a79989 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -162,7 +162,11 @@ let is_constr_gram = function
 | GramTerminal _ -> false
 | GramNonTerminal (_, _, e, _) ->
   match e with
-  | Aentry ("constr", "constr") -> true
+  | Aentry e ->
+    begin match Entry.repr e with
+    | Entry.Static ("constr", "constr") -> true
+    | _ -> false
+    end
   | _ -> false
 
 let make_var = function
-- 
cgit v1.2.3