Allowing generalized rules in typed symbols.

1 files changed, 20 insertions, 7 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index dac5b3bfd8..91f933987b 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -671,6 +671,13 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
 
 (** Binding general entry keys to symbol *)
 
+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)
@@ -695,21 +702,27 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
   | Aentryl (e, n) ->
     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 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
+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)