aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/cLexer.ml2
-rw-r--r--parsing/extend.ml18
-rw-r--r--parsing/pcoq.ml97
-rw-r--r--parsing/pcoq.mli15
4 files changed, 64 insertions, 68 deletions
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index de23f05a9e..7f0d768d3f 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -436,7 +436,7 @@ let comment_stop ep =
let bp = match !comment_begin with
Some bp -> bp
| None ->
- Feedback.msg_notice
+ Feedback.msg_debug
(str "No begin location for comment '"
++ str current_s ++str"' ending at "
++ int ep);
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 63e121c0d1..ed6ebe5aed 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -79,8 +79,10 @@ type ('a,'b,'c) ty_user_symbol =
(** {5 Type-safe grammar extension} *)
-type norec = NoRec (* just two *)
-type mayrec = MayRec (* incompatible types *)
+(* Should be merged with gramlib's implementation *)
+
+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
@@ -107,15 +109,3 @@ and 'a rules =
type 'a production_rule =
| Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
-
-type 'a single_extend_statement =
- string option *
- (* Level *)
- Gramlib.Gramext.g_assoc option *
- (* Associativity *)
- 'a production_rule list
- (* Symbol list with the interpretation function *)
-
-type 'a extend_statement =
- Gramlib.Gramext.position option *
- 'a single_extend_statement list
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 3aaba27579..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)
@@ -215,6 +199,18 @@ let fix_extend_statement (pos, st) =
(** Type of reinitialization data *)
type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
+type 'a single_extend_statement =
+ string option *
+ (* Level *)
+ Gramlib.Gramext.g_assoc option *
+ (* Associativity *)
+ 'a production_rule list
+ (* Symbol list with the interpretation function *)
+
+type 'a extend_statement =
+ Gramlib.Gramext.position option *
+ 'a single_extend_statement list
+
type extend_rule =
| ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule
@@ -462,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
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7efeab6ba0..10f78a5a72 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -212,8 +212,19 @@ val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Extend.symbol -> 'self optio
type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
(** Type of reinitialization data *)
-val grammar_extend : 'a Entry.t -> gram_reinit option ->
- 'a Extend.extend_statement -> unit
+type 'a single_extend_statement =
+ string option *
+ (* Level *)
+ Gramlib.Gramext.g_assoc option *
+ (* Associativity *)
+ 'a production_rule list
+ (* Symbol list with the interpretation function *)
+
+type 'a extend_statement =
+ Gramlib.Gramext.position option *
+ 'a single_extend_statement list
+
+val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a extend_statement -> unit
(** Extend the grammar of Coq, without synchronizing it with the backtracking
mechanism. This means that grammar extensions defined this way will survive
an undo. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 10:32:28 +0000