Simpler data structure for Arules token.

2 files changed, 13 insertions, 33 deletions

diff --git a/intf/extend.mli b/intf/extend.mli
index 3deb8233f0..bf5a18c47d 100644
--- a/intf/extend.mli
+++ b/intf/extend.mli
@@ -66,17 +66,6 @@ type 'a 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
@@ -88,18 +77,16 @@ type ('self, 'a) symbol =
 | Anext : ('self, 'self) symbol
 | Aentry : 'a entry -> ('self, 'a) symbol
 | Aentryl : 'a entry * int -> ('self, 'a) symbol
-| Arules : 'a rules -> ('self, 'a index) symbol
+| Arules : 'a rules list -> ('self, 'a) symbol
 
 and ('self, _, 'r) rule =
 | Stop : ('self, 'r, 'r) rule
 | Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule
 
+and ('a, 'r) norec_rule = { norec_rule : 's. ('s, '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
+| Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules
 
 type 'a production_rule =
 | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 42eb8724af..b06362dc38 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -675,12 +675,9 @@ 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 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 rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
   | Atoken t -> Symbols.stoken t
@@ -697,25 +694,21 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
     Symbols.snterm (Gram.Entry.obj (weaken_entry e))
   | Aentryl (e, n) ->
     Symbols.snterml (Gram.Entry.obj (weaken_entry e), string_of_int n)
-  | Arules rs -> Gram.srules' (symbol_of_rules rs [] (fun x -> I0 x))
+  | Arules rs ->
+    Gram.srules' (List.map symbol_of_rules rs)
 
 and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function
 | Stop -> fun accu -> 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))
+| Rules (r, act) ->
+  let symb = symbol_of_rule r.norec_rule [] in
+  let act = of_coq_action r.norec_rule act in
+  (symb, act)
 
 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) -> (symbol_of_rule toks [], of_coq_action toks act)