aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--gramlib/grammar.ml8
-rw-r--r--gramlib/grammar.mli5
-rw-r--r--parsing/extend.ml4
-rw-r--r--parsing/pcoq.ml85
4 files changed, 42 insertions, 60 deletions
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index f86cb0f6f2..ff0b90dcff 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -10,6 +10,9 @@ open Util
module type GLexerType = Plexing.Lexer
+type ty_norec = TyNoRec
+type ty_mayrec = TyMayRec
+
module type S =
sig
type te
@@ -27,8 +30,6 @@ module type S =
val parse_token_stream : 'a e -> te Stream.t -> 'a
val print : Format.formatter -> 'a e -> unit
end
- type ty_norec = TyNoRec
- type ty_mayrec = TyMayRec
type ('self, 'trec, 'a) ty_symbol
type ('self, 'trec, 'f, 'r) ty_rule
type 'a ty_rules
@@ -92,9 +93,6 @@ let tokens con =
egram.gtokens;
!list
-type ty_norec = TyNoRec
-type ty_mayrec = TyMayRec
-
type ('a, 'b, 'c) ty_and_rec =
| NoRec2 : (ty_norec, ty_norec, ty_norec) ty_and_rec
| MayRec2 : ('a, 'b, ty_mayrec) ty_and_rec
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 658baf1de9..9e48460206 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -19,6 +19,9 @@ module type GLexerType = Plexing.Lexer
(** The input signature for the functor [Grammar.GMake]: [te] is the
type of the tokens. *)
+type ty_norec = TyNoRec
+type ty_mayrec = TyMayRec
+
module type S =
sig
type te
@@ -36,8 +39,6 @@ module type S =
val parse_token_stream : 'a e -> te Stream.t -> 'a
val print : Format.formatter -> 'a e -> unit
end
- type ty_norec = TyNoRec
- type ty_mayrec = TyMayRec
type ('self, 'trec, 'a) ty_symbol
type ('self, 'trec, 'f, 'r) ty_rule
type 'a ty_rules
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 8dc77e1216..ed6ebe5aed 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -81,8 +81,8 @@ type ('a,'b,'c) ty_user_symbol =
(* Should be merged with gramlib's implementation *)
-type norec = NoRec (* just two *)
-type mayrec = MayRec (* incompatible types *)
+type norec = Gramlib.Grammar.ty_norec
+type mayrec = Gramlib.Grammar.ty_mayrec
type ('self, 'trec, 'a) symbol =
| Atoken : 'c Tok.p -> ('self, norec, 'c) symbol
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index fa837c484c..e0d63a723e 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -131,73 +131,57 @@ end
(** Binding general entry keys to symbol *)
-type ('s, 'trec, 'a, 'r) casted_rule =
-| CastedRNo : ('s, G.ty_norec, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, norec, 'a, 'r) casted_rule
-| CastedRMay : ('s, G.ty_mayrec, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, mayrec, 'a, 'r) casted_rule
-
-type ('s, 'trec, 'a) casted_symbol =
-| CastedSNo : ('s, G.ty_norec, 'a) G.ty_symbol -> ('s, norec, 'a) casted_symbol
-| CastedSMay : ('s, G.ty_mayrec, 'a) G.ty_symbol -> ('s, mayrec, 'a) casted_symbol
-
-let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) casted_symbol =
+let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) G.ty_symbol =
function
-| Atoken t -> CastedSNo (G.s_token t)
+| Atoken t -> G.s_token t
| Alist1 s ->
- begin match symbol_of_prod_entry_key s with
- | CastedSNo s -> CastedSNo (G.s_list1 s)
- | CastedSMay s -> CastedSMay (G.s_list1 s) end
+ let s = symbol_of_prod_entry_key s in
+ G.s_list1 s
| Alist1sep (s,sep) ->
- let CastedSNo sep = symbol_of_prod_entry_key sep in
- begin match symbol_of_prod_entry_key s with
- | CastedSNo s -> CastedSNo (G.s_list1sep s sep false)
- | CastedSMay s -> CastedSMay (G.s_list1sep s sep false) end
+ let s = symbol_of_prod_entry_key s in
+ let sep = symbol_of_prod_entry_key sep in
+ G.s_list1sep s sep false
| Alist0 s ->
- begin match symbol_of_prod_entry_key s with
- | CastedSNo s -> CastedSNo (G.s_list0 s)
- | CastedSMay s -> CastedSMay (G.s_list0 s) end
+ let s = symbol_of_prod_entry_key s in
+ G.s_list0 s
| Alist0sep (s,sep) ->
- let CastedSNo sep = symbol_of_prod_entry_key sep in
- begin match symbol_of_prod_entry_key s with
- | CastedSNo s -> CastedSNo (G.s_list0sep s sep false)
- | CastedSMay s -> CastedSMay (G.s_list0sep s sep false) end
+ let s = symbol_of_prod_entry_key s in
+ let sep = symbol_of_prod_entry_key sep in
+ G.s_list0sep s sep false
| Aopt s ->
- begin match symbol_of_prod_entry_key s with
- | CastedSNo s -> CastedSNo (G.s_opt s)
- | CastedSMay s -> CastedSMay (G.s_opt s) end
-| Aself -> CastedSMay G.s_self
-| Anext -> CastedSMay G.s_next
-| Aentry e -> CastedSNo (G.s_nterm e)
-| Aentryl (e, n) -> CastedSNo (G.s_nterml e n)
+ let s = symbol_of_prod_entry_key s in
+ G.s_opt s
+| Aself -> G.s_self
+| Anext -> G.s_next
+| Aentry e -> G.s_nterm e
+| Aentryl (e, n) -> G.s_nterml e n
| Arules rs ->
let warning msg = Feedback.msg_warning Pp.(str msg) in
- CastedSNo (G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs))
+ G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs)
-and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) casted_rule = function
-| Stop -> CastedRNo (G.r_stop, fun act loc -> act loc)
+and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) G.ty_rule = function
+| Stop ->
+ G.r_stop
| Next (r, s) ->
- begin match symbol_of_rule r, symbol_of_prod_entry_key s with
- | CastedRNo (r, cast), CastedSNo s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x)))
- | CastedRNo (r, cast), CastedSMay s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x)))
- | CastedRMay (r, cast), CastedSNo s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x)))
- | CastedRMay (r, cast), CastedSMay s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) end
+ let r = symbol_of_rule r in
+ let s = symbol_of_prod_entry_key s in
+ G.r_next r s
| NextNoRec (r, s) ->
- let CastedRNo (r, cast) = symbol_of_rule r in
- let CastedSNo s = symbol_of_prod_entry_key s in
- CastedRNo (G.r_next_norec r s, (fun act x -> cast (act x)))
+ let r = symbol_of_rule r in
+ let s = symbol_of_prod_entry_key s in
+ G.r_next_norec r s
and symbol_of_rules : type a. a Extend.rules -> a G.ty_rules = function
| Rules (r, act) ->
- let CastedRNo (symb, cast) = symbol_of_rule r in
- G.rules (symb, cast act)
+ let symb = symbol_of_rule r in
+ G.rules (symb,act)
(** FIXME: This is a hack around a deficient camlp5 API *)
type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production
let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function
| Rule (toks, act) ->
- match symbol_of_rule toks with
- | CastedRNo (symb, cast) -> AnyProduction (symb, cast act)
- | CastedRMay (symb, cast) -> AnyProduction (symb, cast act)
+ AnyProduction (symbol_of_rule toks, act)
let of_coq_single_extend_statement (lvl, assoc, rule) =
(lvl, assoc, List.map of_coq_production_rule rule)
@@ -474,11 +458,10 @@ module Module =
let module_expr = Entry.create "module_expr"
let module_type = Entry.create "module_type"
end
+
let epsilon_value (type s tr a) f (e : (s, tr, a) symbol) =
- let r =
- match symbol_of_prod_entry_key e with
- | CastedSNo s -> G.production (G.r_next G.r_stop s, (fun x _ -> f x))
- | CastedSMay s -> G.production (G.r_next G.r_stop s, (fun x _ -> f x)) in
+ let s = symbol_of_prod_entry_key e in
+ let r = G.production (G.r_next G.r_stop s, (fun x _ -> f x)) in
let ext = [None, None, [r]] in
let entry = Gram.entry_create "epsilon" in
let warning msg = Feedback.msg_warning Pp.(str msg) in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:16:27 +0000