Cleaning up and extending the expressivity of Pcoq.

10 files changed, 108 insertions, 145 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index aef9b10b26..141eab3f3f 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -520,7 +520,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")))]
+        (Loc.ghost,rawwit wit_constr,Extend.Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
 
 let _ =
   try
@@ -536,7 +536,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.ghost,rawwit wit_constr,Aentry (Entry.unsafe_of_name ("constr","constr")))]
+        (Loc.ghost,rawwit wit_constr,Extend.Aentry (Pcoq.name_of_entry Pcoq.Constr.constr))]
 
 (* Setting printer of unbound global reference *)
 open Names
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 5bf7b65d77..bebde706e4 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -43,7 +43,7 @@ let make_act loc act pil =
   make (List.rev pil)
 
 let make_prod_item = function
-  | ExtTerminal s -> <:expr< Pcoq.Atoken (Lexer.terminal $mlexpr_of_string s$) >>
+  | ExtTerminal s -> <:expr< Extend.Atoken (Lexer.terminal $mlexpr_of_string s$) >>
   | ExtNonTerminal (_, g, _) ->
     let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in
     mlexpr_of_prod_entry_key base g
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 4160d03c5c..d91bfd7b8d 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -48,18 +48,18 @@ let mlexpr_of_ident id =
   <:expr< Names.Id.of_string $str:id$ >>
 
 let rec mlexpr_of_prod_entry_key f = function
-  | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key f s$ >>
-  | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
-  | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key f s$ >>
-  | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
-  | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key f s$ >>
-  | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key f s$ >>
-  | Extend.Uentry e -> <:expr< Pcoq.Aentry $f e$ >>
+  | Extend.Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >>
+  | Extend.Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+  | Extend.Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >>
+  | Extend.Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+  | Extend.Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >>
+  | Extend.Umodifiers s -> <:expr< Extend.Amodifiers $mlexpr_of_prod_entry_key f s$ >>
+  | Extend.Uentry e -> <:expr< Extend.Aentry $f e$ >>
   | Extend.Uentryl (e, l) ->
     (** Keep in sync with Pcoq! *)
     assert (CString.equal e "tactic");
-    if l = 5 then <:expr< Pcoq.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >>
-    else <:expr< Pcoq.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
+    if l = 5 then <:expr< Extend.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >>
+    else <:expr< Extend.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
 
 let rec type_of_user_symbol = function
 | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s ->
diff --git a/intf/extend.mli b/intf/extend.mli
index 57abdc38fb..e1520dec54 100644
--- a/intf/extend.mli
+++ b/intf/extend.mli
@@ -65,6 +65,17 @@ type user_symbol =
 
 (** {5 Type-safe grammar extension} *)
 
+(** (a, b, r) adj => [a = x₁ -> ... xₙ -> r] & [b = x₁ * (... (xₙ * unit))]. *)
+type (_, _, _) adj =
+| Adj0 : ('r, unit, 'r) adj
+| AdjS : ('s, 'b, 'r) adj -> ('a -> 's, 'a * 'b, 'r) adj
+
+type _ index =
+| I0 : 'a -> ('a * 'r) index
+| IS : 'a index -> ('b * 'a) index
+
+(** This type should be marshallable, this is why we use a convoluted
+    representation in the [Arules] constructor instead of putting a function. *)
 type ('self, 'a) symbol =
 | Atoken : Tok.t -> ('self, string) symbol
 | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol
@@ -77,11 +88,19 @@ type ('self, 'a) symbol =
 | Anext : ('self, 'self) symbol
 | Aentry : 'a Entry.t -> ('self, 'a) symbol
 | Aentryl : 'a Entry.t * int -> ('self, 'a) symbol
+| Arules : 'a rules -> ('self, 'a index) symbol
 
-type ('self, _, 'r) rule =
+and ('self, _, 'r) rule =
 | Stop : ('self, 'r, 'r) rule
 | Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule
 
+and 'a rules =
+| Rule0 : unit rules
+| RuleS :
+  ('any, 'act, Loc.t -> Loc.t * 'a) rule *
+  ('act, 'a, Loc.t -> Loc.t * 'a) adj *
+  'b rules -> ((Loc.t * 'a) * 'b) rules
+
 type 'a production_rule =
 | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
 
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 77252e7425..37fccdb3c2 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -9,6 +9,7 @@
 open Util
 open Compat
 open Names
+open Extend
 open Pcoq
 open Genarg
 open Vernacexpr
@@ -18,7 +19,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal :
-      Loc.t * 'a raw_abstract_argument_type * ('s, 'a) entry_key -> 's grammar_prod_item
+      Loc.t * 'a raw_abstract_argument_type * ('s, 'a) symbol -> 's grammar_prod_item
 
 type 'a ty_arg = ('a -> raw_generic_argument)
 
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index edf971574d..1ad9472007 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -16,7 +16,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type *
-      ('s, 'a) Pcoq.entry_key -> 's grammar_prod_item
+      ('s, 'a) Extend.symbol -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
   Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option ->
diff --git a/parsing/entry.ml b/parsing/entry.ml
index 0519903d3d..b7c6c23fa6 100644
--- a/parsing/entry.ml
+++ b/parsing/entry.ml
@@ -9,51 +9,22 @@
 open Errors
 open Util
 
-type 'a t = string * string
-
-type repr = string * string
-
-type universe = string
-
-(* The univ_tab is not part of the state. It contains all the grammars that
-   exist or have existed before in the session. *)
-
-let univ_tab = (Hashtbl.create 7 : (string, unit) Hashtbl.t)
-
-let create_univ s =
-  Hashtbl.add univ_tab s (); s
-
-let univ_name s = s
-
-let uprim   = create_univ "prim"
-let uconstr = create_univ "constr"
-let utactic = create_univ "tactic"
-let uvernac = create_univ "vernac"
-
-let get_univ s =
-  try
-    Hashtbl.find univ_tab s; s
-  with Not_found ->
-    anomaly (Pp.str ("Unknown grammar universe: "^s))
+type 'a t = string
 
 (** Entries are registered with a unique name *)
 
 let entries = ref String.Set.empty
 
-let create u name =
-  let uname = u ^ ":" ^ name in
+let create name =
   let () =
-    if String.Set.mem uname !entries then
-    anomaly (Pp.str ("Entry " ^ uname ^ " already defined"))
+    if String.Set.mem name !entries then
+    anomaly (Pp.str ("Entry " ^ name ^ " already defined"))
   in
-  let () = entries := String.Set.add uname !entries in
-  (u, name)
-
-let dynamic name = ("", name)
+  let () = entries := String.Set.add name !entries in
+  name
 
-let unsafe_of_name (u, s) =
-  let uname = u ^ ":" ^ s in
-  assert (String.Set.mem uname !entries);
-  (u, s)
+let unsafe_of_name name =
+  assert (String.Set.mem name !entries);
+  name
 
-let repr (u, s) = (u, s)
+let repr s = s
diff --git a/parsing/entry.mli b/parsing/entry.mli
index 97cd5b1105..4c73fe2049 100644
--- a/parsing/entry.mli
+++ b/parsing/entry.mli
@@ -11,34 +11,13 @@
 type 'a t
 (** Typed grammar entries. We need to defined them here so that they are
     marshallable and defined before the Pcoq.Gram module. They are basically
-    unique names made of a universe and an entry name. They should be kept
-    synchronized with the {!Pcoq} entries though. *)
+    unique names. They should be kept synchronized with the {!Pcoq} entries. *)
 
-type repr = string * string
-(** Representation of entries. *)
-
-(** Table of Coq statically defined grammar entries *)
-
-type universe
-
-(** There are four predefined universes: "prim", "constr", "tactic", "vernac" *)
-
-val get_univ : string -> universe
-val univ_name : universe -> string
-
-val uprim : universe
-val uconstr : universe
-val utactic : universe
-val uvernac : universe
-
-(** {5 Uniquely defined entries} *)
-
-val create : universe -> string -> 'a t
+val create : string -> 'a t
 (** Create an entry. They should be synchronized with the entries defined in
     {!Pcoq}. *)
 
 (** {5 Meta-programming} *)
 
-val repr : 'a t -> repr
-
-val unsafe_of_name : (string * string) -> 'a t
+val repr : 'a t -> string
+val unsafe_of_name : string -> 'a t
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index bf46fffffe..91f933987b 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -64,21 +64,8 @@ let weaken_entry x = Gramobj.weaken_entry x
    dynamically interpreted as entries for the Coq level extensions
 *)
 
-type ('self, 'a) entry_key = ('self, 'a) Extend.symbol =
-| Atoken : Tok.t -> ('self, string) 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
-
 type entry_name = EntryName :
-  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) entry_key -> entry_name
+  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) symbol -> entry_name
 
 (** Grammar extensions *)
 
@@ -198,40 +185,49 @@ let map_entry f en =
 let parse_string f x =
   let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm)
 
-type gram_universe = Entry.universe
-
-let uprim   = Entry.uprim
-let uconstr = Entry.uconstr
-let utactic = Entry.utactic
-let uvernac = Entry.uvernac
-let get_univ = Entry.get_univ
+type gram_universe = string
 
 let utables : (string, (string, typed_entry) Hashtbl.t) Hashtbl.t =
   Hashtbl.create 97
 
+let create_universe u =
+  let table = Hashtbl.create 97 in
+  let () = Hashtbl.add utables u table in
+  u
+
+let uprim   = create_universe "prim"
+let uconstr = create_universe "constr"
+let utactic = create_universe "tactic"
+let uvernac = create_universe "vernac"
+
+let get_univ u =
+  if Hashtbl.mem utables u then u
+  else raise Not_found
+
 let get_utable u =
-  let u = Entry.univ_name u in
   try Hashtbl.find utables u
-  with Not_found ->
-    let table = Hashtbl.create 97 in
-    Hashtbl.add utables u table;
-    table
+  with Not_found -> assert false
 
 let get_entry u s =
   let utab = get_utable u in
   Hashtbl.find utab s
 
-let get_typed_entry e =
-  let (u, s) = Entry.repr e in
-  let u = Entry.get_univ u in
-  get_entry u s
+(** A table associating grammar to entries *)
+let gtable : Obj.t Gram.entry String.Map.t ref = ref String.Map.empty
+
+let get_grammar (e : 'a Entry.t) : 'a Gram.entry =
+  Obj.magic (String.Map.find (Entry.repr e) !gtable)
+
+let set_grammar (e : 'a Entry.t) (g : 'a Gram.entry) =
+  assert (not (String.Map.mem (Entry.repr e) !gtable));
+  gtable := String.Map.add (Entry.repr e) (Obj.magic g) !gtable
 
 let new_entry etyp u s =
   let utab = get_utable u in
-  let uname = Entry.univ_name u in
-  let _ = Entry.create u s in
-  let ename = uname ^ ":" ^ s in
+  let ename = u ^ ":" ^ s in
+  let entry = Entry.create ename in
   let e = Gram.entry_create ename in
+  let () = set_grammar entry e in
   Hashtbl.add utab s (TypedEntry (etyp, e)); e
 
 let make_gen_entry u rawwit s = new_entry rawwit u s
@@ -251,8 +247,7 @@ let genarg_grammar = Grammar.obj
 let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry =
   let utab = get_utable u in
   if Hashtbl.mem utab s then
-    let u = Entry.univ_name u in
-    failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists");
+    failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists")
   else
     let e = new_entry etyp u s in
     let Rawwit t = etyp in
@@ -603,7 +598,6 @@ let compute_entry adjust forpat = function
   | ETPattern -> weaken_entry Constr.pattern, None, false
   | ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.")
   | ETOther (u,n) ->
-      let u = get_univ u in
       let e = get_entry u n in
       object_of_typed_entry e, None, true
 
@@ -677,7 +671,14 @@ 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
+let tuplify l =
+  List.fold_left (fun accu x -> Obj.repr (x, accu)) (Obj.repr ()) l
+
+let rec adj : type a b c. (a, b, Loc.t -> Loc.t * c) adj -> _ = function
+| Adj0 -> Obj.magic (fun accu f loc -> f (Obj.repr (to_coqloc loc, tuplify accu)))
+| AdjS e -> Obj.magic (fun accu f x -> adj e (x :: accu) f)
+
+let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
   | Atoken t -> Symbols.stoken t
   | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s)
   | Alist1sep (s,sep) ->
@@ -696,26 +697,32 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) entry_key -> _ = function
   | Aself -> Symbols.sself
   | Anext -> Symbols.snext
   | Aentry e ->
-    let e = get_typed_entry e in
-    Symbols.snterm (Gram.Entry.obj (object_of_typed_entry e))
+    let e = get_grammar e in
+    Symbols.snterm (Gram.Entry.obj (weaken_entry e))
   | Aentryl (e, n) ->
-    let e = get_typed_entry e in
-    Symbols.snterml (Gram.Entry.obj (object_of_typed_entry e), string_of_int n)
-
-let level_of_snterml e = int_of_string (Symbols.snterml_level e)
+    let e = get_grammar e in
+    Symbols.snterml (Gram.Entry.obj (weaken_entry e), string_of_int n)
+  | Arules rs -> Gram.srules' (symbol_of_rules rs [] (fun x -> I0 x))
 
-let rec of_coq_rule : type self a r. (self, a, r) Extend.rule -> _ = function
+and symbol_of_rule : type s a r. (s, 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)
+| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu)
+
+and symbol_of_rules : type a. a Extend.rules -> _ = function
+| Rule0 -> fun accu _ -> accu
+| RuleS (r, e, rs) -> fun accu f ->
+  let symb = symbol_of_rule r [] in
+  let act = adj e [] f in
+  symbol_of_rules rs ((symb, act) :: accu) (fun x -> IS (f x))
+
+let level_of_snterml e = int_of_string (Symbols.snterml_level e)
 
 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)
+| Rule (toks, act) -> (symbol_of_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)
@@ -742,9 +749,7 @@ let coincide s pat off =
   done;
   !break
 
-let name_of_entry e = match String.split ':' (Gram.Entry.name e) with
-| u :: s :: [] -> Entry.unsafe_of_name (u, s)
-| _ -> assert false
+let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e)
 
 let atactic n =
   if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e57da42cb3..d6bfe3eb39 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -112,19 +112,6 @@ type gram_reinit = gram_assoc * gram_position
    dynamically interpreted as entries for the Coq level extensions
 *)
 
-type ('self, 'a) entry_key = ('self, 'a) Extend.symbol =
-| Atoken : Tok.t -> ('self, string) 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 unsafe_grammar_extend :
   grammar_object Gram.entry ->
@@ -149,7 +136,7 @@ val parse_string : 'a Gram.entry -> string -> 'a
 val eoi_entry : 'a Gram.entry -> 'a Gram.entry
 val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry
 
-type gram_universe = Entry.universe
+type gram_universe
 
 val get_univ : string -> gram_universe
 
@@ -158,6 +145,7 @@ val uconstr : gram_universe
 val utactic : gram_universe
 val uvernac : gram_universe
 
+val set_grammar : 'a Entry.t -> 'a Gram.entry -> unit
 val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
 val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
 
@@ -276,7 +264,7 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 (** Binding general entry keys to symbols *)
 
 type entry_name = EntryName :
-  'a raw_abstract_argument_type * (raw_tactic_expr, 'a) entry_key -> entry_name
+  'a raw_abstract_argument_type * (raw_tactic_expr, 'a) Extend.symbol -> entry_name
 
 (** [interp_entry_name lev n sep] returns the entry corresponding to the name
     [n] of the form "ne_constr_list" in a tactic entry of level [lev] with