Type-safe grammar extensions.

5 files changed, 104 insertions, 26 deletions

diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 5ec7510f79..19f436f926 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -49,7 +49,20 @@ let mlexpr_of_option f = function
   | None -> <:expr< None >>
   | Some e -> <:expr< Some $f e$ >>
 
+let mlexpr_of_token = function
+| Tok.KEYWORD s -> <:expr< Tok.KEYWORD $mlexpr_of_string s$ >>
+| Tok.METAIDENT s -> <:expr< Tok.METAIDENT $mlexpr_of_string s$ >>
+| Tok.PATTERNIDENT s -> <:expr< Tok.PATTERNIDENT $mlexpr_of_string s$ >>
+| Tok.IDENT s -> <:expr< Tok.IDENT $mlexpr_of_string s$ >>
+| Tok.FIELD s -> <:expr< Tok.FIELD $mlexpr_of_string s$ >>
+| Tok.INT s -> <:expr< Tok.INT $mlexpr_of_string s$ >>
+| Tok.STRING s -> <:expr< Tok.STRING $mlexpr_of_string s$ >>
+| Tok.LEFTQMARK -> <:expr< Tok.LEFTQMARK >>
+| Tok.BULLET s -> <:expr< Tok.BULLET $mlexpr_of_string s$ >>
+| Tok.EOI -> <:expr< Tok.EOI >>
+
 let rec mlexpr_of_prod_entry_key : type s a. (s, a) Pcoq.entry_key -> _ = function
+  | Pcoq.Atoken t -> <:expr< Pcoq.Atoken $mlexpr_of_token t$ >>
   | Pcoq.Alist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >>
   | Pcoq.Alist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
   | Pcoq.Alist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >>
diff --git a/intf/extend.mli b/intf/extend.mli
index ad9706f3a5..aa0db52d7f 100644
--- a/intf/extend.mli
+++ b/intf/extend.mli
@@ -50,3 +50,37 @@ type constr_prod_entry_key =
 
 type simple_constr_prod_entry_key =
     (production_level,unit) constr_entry_key_gen
+
+(** {5 Type-safe grammar extension} *)
+
+type ('self, 'a) symbol =
+| Atoken : Tok.t -> ('self, Tok.t) symbol
+| Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol
+| Alist1sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol
+| Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol
+| Alist0sep : ('self, 'a) symbol * string -> ('self, 'a list) symbol
+| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol
+| Amodifiers : ('self, 'a) symbol -> ('self, 'a list) symbol
+| Aself : ('self, 'self) symbol
+| Anext : ('self, 'self) symbol
+| Aentry : 'a Entry.t -> ('self, 'a) symbol
+| Aentryl : 'a Entry.t * int -> ('self, 'a) symbol
+
+type ('self, _, 'r) rule =
+| Stop : ('self, 'r, 'r) rule
+| Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule
+
+type 'a production_rule =
+| Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
+
+type 'a single_extend_statment =
+  string option *
+  (** Level *)
+  gram_assoc option *
+  (** Associativity *)
+  'a production_rule list
+  (** Symbol list with the interpretation function *)
+
+type 'a extend_statment =
+  gram_position option *
+  'a single_extend_statment list
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index fba754eaaf..7bfcf65e3e 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -170,7 +170,7 @@ let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
   let entry =
     if forpat then weaken_entry Constr.pattern
     else weaken_entry Constr.operconstr in
-  grammar_extend entry reinit (pos,[(name, p4assoc, [])])
+  unsafe_grammar_extend entry reinit (pos,[(name, p4assoc, [])])
 
 let pure_sublevels level symbs =
   let filter s =
@@ -195,7 +195,7 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules =
   let pos,p4assoc,name,reinit = find_position forpat assoc level in
   let nb_decls = List.length needed_levels + 1 in
   List.iter (prepare_empty_levels forpat) needed_levels;
-  grammar_extend entry reinit (Option.map of_coq_position pos,
+  unsafe_grammar_extend entry reinit (Option.map of_coq_position pos,
     [(name, Option.map of_coq_assoc p4assoc, [symbs, mkact pt])]);
   nb_decls) 0 rules
 
@@ -265,7 +265,7 @@ let add_ml_tactic_entry name prods =
   in
   let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in
   synchronize_level_positions ();
-  grammar_extend entry None (None ,[(None, None, List.rev rules)]);
+  unsafe_grammar_extend entry None (None ,[(None, None, List.rev rules)]);
   1
 
 (* Declaration of the tactic grammar rule *)
@@ -285,7 +285,7 @@ let add_tactic_entry kn tg =
   in
   let rules = make_rule mkact tg.tacgram_prods in
   synchronize_level_positions ();
-  grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]);
+  unsafe_grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]);
   1
 
 let (grammar_state : (int * all_grammar_command) list ref) = ref []
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 5b980b3489..1dea3497e4 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -67,7 +67,8 @@ let weaken_entry x = Gramobj.weaken_entry x
    dynamically interpreted as entries for the Coq level extensions
 *)
 
-type ('self, _) entry_key =
+type ('self, 'a) entry_key = ('self, 'a) Extend.symbol =
+| Atoken : Tok.t -> ('self, Tok.t) entry_key
 | Alist1 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
 | Alist1sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
 | Alist0 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
@@ -168,7 +169,7 @@ module Gram =
 
 (** This extension command is used by the Grammar constr *)
 
-let grammar_extend e reinit ext =
+let unsafe_grammar_extend e reinit ext =
   camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state;
   camlp4_verbose (maybe_uncurry (G.extend e)) ext
 
@@ -707,6 +708,7 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
 (** Binding general entry keys to symbol *)
 
 let rec symbol_of_prod_entry_key : type s a. (s, a) entry_key -> _ = function
+  | Atoken t -> Symbols.stoken t
   | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s)
   | Alist1sep (s,sep) ->
       Symbols.slist1sep (symbol_of_prod_entry_key s, gram_token_of_string sep)
@@ -732,6 +734,29 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) entry_key -> _ = function
 
 let level_of_snterml e = int_of_string (Symbols.snterml_level e)
 
+let rec of_coq_rule : type self a r. (self, a, r) Extend.rule -> _ = function
+| Stop -> fun accu -> accu
+| Next (r, tok) -> fun accu ->
+  let symb = symbol_of_prod_entry_key tok in
+  of_coq_rule r (symb :: accu)
+
+let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> Gram.action = function
+| Stop -> fun f -> Gram.action (fun loc -> f (to_coqloc loc))
+| Next (r, _) -> fun f -> Gram.action (fun x -> of_coq_action r (f x))
+
+let of_coq_production_rule : type a. a Extend.production_rule -> _ = function
+| Rule (toks, act) -> (of_coq_rule toks [], of_coq_action toks act)
+
+let of_coq_single_extend_statement (lvl, assoc, rule) =
+  (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule)
+
+let of_coq_extend_statement (pos, st) =
+  (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st)
+
+let grammar_extend e reinit ext =
+  let ext = of_coq_extend_statement ext in
+  unsafe_grammar_extend e reinit ext
+
 (**********************************************************************)
 (* Interpret entry names of the form "ne_constr_list" as entry keys   *)
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 18eb3eed34..74b7bcc93f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -105,12 +105,37 @@ type grammar_object
 (** Type of reinitialization data *)
 type gram_reinit = gram_assoc * gram_position
 
+(** General entry keys *)
+
+(** This intermediate abstract representation of entries can
+   both be reified into mlexpr for the ML extensions and
+   dynamically interpreted as entries for the Coq level extensions
+*)
+
+type ('self, 'a) entry_key = ('self, 'a) Extend.symbol =
+| Atoken : Tok.t -> ('self, Tok.t) entry_key
+| Alist1 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Alist1sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
+| Alist0 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Alist0sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
+| Aopt : ('self, 'a) entry_key -> ('self, 'a option) entry_key
+| Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Aself : ('self, 'self) entry_key
+| Anext : ('self, 'self) entry_key
+| Aentry : 'a Entry.t -> ('self, 'a) entry_key
+| Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key
+
 (** Add one extension at some camlp4 position of some camlp4 entry *)
-val grammar_extend :
+val unsafe_grammar_extend :
   grammar_object Gram.entry ->
   gram_reinit option (** for reinitialization if ever needed *) ->
   Gram.extend_statment -> unit
 
+val grammar_extend :
+  'a Gram.entry ->
+  gram_reinit option (** for reinitialization if ever needed *) ->
+  'a Extend.extend_statment -> unit
+
 (** Remove the last n extensions *)
 val remove_grammars : int -> unit
 
@@ -253,25 +278,6 @@ val symbol_of_constr_prod_entry_key : gram_assoc option ->
   constr_entry_key -> bool -> constr_prod_entry_key ->
     Gram.symbol
 
-(** General entry keys *)
-
-(** This intermediate abstract representation of entries can
-   both be reified into mlexpr for the ML extensions and
-   dynamically interpreted as entries for the Coq level extensions
-*)
-
-type ('self, _) entry_key =
-| Alist1 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
-| Alist1sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
-| Alist0 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
-| Alist0sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
-| Aopt : ('self, 'a) entry_key -> ('self, 'a option) entry_key
-| Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key
-| Aself : ('self, 'self) entry_key
-| Anext : ('self, 'self) entry_key
-| Aentry : 'a Entry.t -> ('self, 'a) entry_key
-| Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key
-
 val name_of_entry : 'a Gram.entry -> 'a Entry.t
 
 (** Binding general entry keys to symbols *)