aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-04-01 12:51:16 +0200
committerPierre-Marie Pédrot2019-04-01 12:51:16 +0200
commitd16633368ba33d05bcae3e98b1e05efc5f530206 (patch)
tree4cd4f1c348a7e0a5d90a91c2b9a61ab91672cb73
parent4c3f4d105a32cc7661ae714fe4e25619e32bc84c (diff)
parentd8d3b7a8251b874c436ac11b881cf4fb5f991784 (diff)
Merge PR #9815: Multiple payload types in tokens
Reviewed-by: ppedrot Ack-by: proux01
Diffstat
-rw-r--r--coqpp/coqpp_main.ml52
-rw-r--r--dev/ci/user-overlays/09815-token-type.sh4
-rw-r--r--gramlib/grammar.ml749
-rw-r--r--gramlib/grammar.mli54
-rw-r--r--gramlib/plexing.ml20
-rw-r--r--gramlib/plexing.mli32
-rw-r--r--parsing/cLexer.ml63
-rw-r--r--parsing/cLexer.mli25
-rw-r--r--parsing/extend.ml50
-rw-r--r--parsing/notation_gram.ml2
-rw-r--r--parsing/pcoq.ml104
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--parsing/tok.ml117
-rw-r--r--parsing/tok.mli30
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--printing/proof_diffs.ml3
-rw-r--r--vernac/egramcoq.ml85
-rw-r--r--vernac/egramml.ml16
-rw-r--r--vernac/egramml.mli2
-rw-r--r--vernac/metasyntax.ml8
-rw-r--r--vernac/pvernac.ml2
-rw-r--r--vernac/vernacextend.ml2
22 files changed, 826 insertions, 598 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index f4c819eeb6..baa6c2d64e 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -161,29 +161,33 @@ let is_token s = match string_split s with
| [s] -> is_uident s
| _ -> false
-let rec parse_tokens = function
+let rec parse_tokens ?(in_anon=false) =
+let err_anon () =
+ if in_anon then
+ fatal (Printf.sprintf "'SELF' or 'NEXT' illegal in anonymous entry level") in
+function
| [GSymbString s] -> SymbToken ("", Some s)
| [GSymbQualid ("QUOTATION", None); GSymbString s] ->
SymbToken ("QUOTATION", Some s)
-| [GSymbQualid ("SELF", None)] -> SymbSelf
-| [GSymbQualid ("NEXT", None)] -> SymbNext
+| [GSymbQualid ("SELF", None)] -> err_anon (); SymbSelf
+| [GSymbQualid ("NEXT", None)] -> err_anon (); SymbNext
| [GSymbQualid ("LIST0", None); tkn] ->
- SymbList0 (parse_token tkn, None)
+ SymbList0 (parse_token ~in_anon tkn, None)
| [GSymbQualid ("LIST1", None); tkn] ->
- SymbList1 (parse_token tkn, None)
+ SymbList1 (parse_token ~in_anon tkn, None)
| [GSymbQualid ("LIST0", None); tkn; GSymbQualid ("SEP", None); tkn'] ->
- SymbList0 (parse_token tkn, Some (parse_token tkn'))
+ SymbList0 (parse_token ~in_anon tkn, Some (parse_token ~in_anon tkn'))
| [GSymbQualid ("LIST1", None); tkn; GSymbQualid ("SEP", None); tkn'] ->
- SymbList1 (parse_token tkn, Some (parse_token tkn'))
+ SymbList1 (parse_token ~in_anon tkn, Some (parse_token ~in_anon tkn'))
| [GSymbQualid ("OPT", None); tkn] ->
- SymbOpt (parse_token tkn)
+ SymbOpt (parse_token ~in_anon tkn)
| [GSymbQualid (e, None)] when is_token e -> SymbToken (e, None)
| [GSymbQualid (e, None); GSymbString s] when is_token e -> SymbToken (e, Some s)
| [GSymbQualid (e, lvl)] when not (is_token e) -> SymbEntry (e, lvl)
-| [GSymbParen tkns] -> parse_tokens tkns
+| [GSymbParen tkns] -> parse_tokens ~in_anon tkns
| [GSymbProd prds] ->
let map p =
- let map (pat, tkns) = (pat, parse_tokens tkns) in
+ let map (pat, tkns) = (pat, parse_tokens ~in_anon:true tkns) in
(List.map map p.gprod_symbs, p.gprod_body)
in
SymbRules (List.map map prds)
@@ -199,7 +203,7 @@ let rec parse_tokens = function
in
fatal (Printf.sprintf "Invalid token: %s" (db_tokens t))
-and parse_token tkn = parse_tokens [tkn]
+and parse_token ~in_anon tkn = parse_tokens ~in_anon [tkn]
let print_fun fmt (vars, body) =
let vars = List.rev vars in
@@ -214,9 +218,20 @@ let print_fun fmt (vars, body) =
(** Meta-program instead of calling Tok.of_pattern here because otherwise
violates value restriction *)
-let print_tok fmt (k,o) =
- let print_pat fmt = print_opt fmt print_string in
- fprintf fmt "(%a,%a)" print_string k print_pat o
+let print_tok fmt =
+let print_pat fmt = print_opt fmt print_string in
+function
+| "", Some s -> fprintf fmt "Tok.PKEYWORD (%a)" print_string s
+| "IDENT", s -> fprintf fmt "Tok.PIDENT (%a)" print_pat s
+| "PATTERNIDENT", s -> fprintf fmt "Tok.PPATTERNIDENT (%a)" print_pat s
+| "FIELD", s -> fprintf fmt "Tok.PFIELD (%a)" print_pat s
+| "INT", s -> fprintf fmt "Tok.PINT (%a)" print_pat s
+| "STRING", s -> fprintf fmt "Tok.PSTRING (%a)" print_pat s
+| "LEFTQMARK", None -> fprintf fmt "Tok.PLEFTQMARK"
+| "BULLET", s -> fprintf fmt "Tok.PBULLET (%a)" print_pat s
+| "QUOTATION", Some s -> fprintf fmt "Tok.PQUOTATION %a" print_string s
+| "EOI", None -> fprintf fmt "Tok.PEOI"
+| _ -> failwith "Tok.of_pattern: not a constructor"
let rec print_prod fmt p =
let (vars, tkns) = List.split p.gprod_symbs in
@@ -225,12 +240,13 @@ let rec print_prod fmt p =
and print_extrule fmt (tkn, vars, body) =
let tkn = List.rev tkn in
- fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun (vars, body)
+ fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" (print_symbols ~norec:false) tkn print_fun (vars, body)
-and print_symbols fmt = function
+and print_symbols ~norec fmt = function
| [] -> fprintf fmt "Extend.Stop"
| tkn :: tkns ->
- fprintf fmt "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn
+ let c = if norec then "Extend.NextNoRec" else "Extend.Next" in
+ fprintf fmt "%s @[(%a,@ %a)@]" c (print_symbols ~norec) tkns print_symbol tkn
and print_symbol fmt tkn = match tkn with
| SymbToken (t, s) ->
@@ -257,7 +273,7 @@ and print_symbol fmt tkn = match tkn with
let pr fmt (r, body) =
let (vars, tkn) = List.split r in
let tkn = List.rev tkn in
- fprintf fmt "Extend.Rules @[({ Extend.norec_rule = %a },@ (%a))@]" print_symbols tkn print_fun (vars, body)
+ fprintf fmt "Extend.Rules @[(%a,@ (%a))@]" (print_symbols ~norec:true) tkn print_fun (vars, body)
in
let pr fmt rules = print_list fmt pr rules in
fprintf fmt "(Extend.Arules %a)" pr (List.rev rules)
diff --git a/dev/ci/user-overlays/09815-token-type.sh b/dev/ci/user-overlays/09815-token-type.sh
new file mode 100644
index 0000000000..4b49011de3
--- /dev/null
+++ b/dev/ci/user-overlays/09815-token-type.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "9815" ] || [ "$CI_BRANCH" = "token-type" ]; then
+ ltac2_CI_REF=token-type
+ ltac2_CI_GITURL=https://github.com/proux01/ltac2
+fi
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 9eebe7a1e2..c452c7b307 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -4,16 +4,16 @@
open Gramext
open Format
-
-type ('a, 'b) eq = Refl : ('a, 'a) eq
+open Util
(* Functorial interface *)
-module type GLexerType = sig type te val lexer : te Plexing.lexer end
+module type GLexerType = Plexing.Lexer
module type S =
sig
type te
+ type 'c pattern
type parsable
val parsable : ?loc:Loc.t -> char Stream.t -> parsable
val tokens : string -> (string option * int) list
@@ -27,29 +27,36 @@ module type S =
val parse_token_stream : 'a e -> te Stream.t -> 'a
val print : Format.formatter -> 'a e -> unit
end
- type ('self, 'a) ty_symbol
- type ('self, 'f, 'r) ty_rule
+ 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
type 'a ty_production
- val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol
- val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol
- val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
+ val s_nterm : 'a Entry.e -> ('self, ty_norec, 'a) ty_symbol
+ val s_nterml : 'a Entry.e -> string -> ('self, ty_norec, 'a) ty_symbol
+ val s_list0 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol
val s_list0sep :
- ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool ->
- ('self, 'a list) ty_symbol
- val s_list1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
+ ('self, 'trec, 'a) ty_symbol -> ('self, ty_norec, 'b) ty_symbol -> bool ->
+ ('self, 'trec, 'a list) ty_symbol
+ val s_list1 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol
val s_list1sep :
- ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool ->
- ('self, 'a list) ty_symbol
- val s_opt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol
- val s_self : ('self, 'self) ty_symbol
- val s_next : ('self, 'self) ty_symbol
- val s_token : Plexing.pattern -> ('self, string) ty_symbol
- val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol
- val r_stop : ('self, 'r, 'r) ty_rule
+ ('self, 'trec, 'a) ty_symbol -> ('self, ty_norec, 'b) ty_symbol -> bool ->
+ ('self, 'trec, 'a list) ty_symbol
+ val s_opt : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a option) ty_symbol
+ val s_self : ('self, ty_mayrec, 'self) ty_symbol
+ val s_next : ('self, ty_mayrec, 'self) ty_symbol
+ val s_token : 'c pattern -> ('self, ty_norec, 'c) ty_symbol
+ val s_rules : warning:(string -> unit) option -> 'a ty_rules list -> ('self, ty_norec, 'a) ty_symbol
+ val r_stop : ('self, ty_norec, 'r, 'r) ty_rule
val r_next :
- ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
- ('self, 'b -> 'a, 'r) ty_rule
- val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
+ ('self, _, 'a, 'r) ty_rule -> ('self, _, 'b) ty_symbol ->
+ ('self, ty_mayrec, 'b -> 'a, 'r) ty_rule
+ val r_next_norec :
+ ('self, ty_norec, 'a, 'r) ty_rule -> ('self, ty_norec, 'b) ty_symbol ->
+ ('self, ty_norec, 'b -> 'a, 'r) ty_rule
+ val rules : (_, ty_norec, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_rules
+ val production : ('a, _, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
module Unsafe :
sig
val clear_entry : 'a Entry.e -> unit
@@ -59,7 +66,7 @@ module type S =
(string option * Gramext.g_assoc option * 'a ty_production list)
list ->
unit
- val safe_delete_rule : 'a Entry.e -> ('a, 'r, 'f) ty_rule -> unit
+ val safe_delete_rule : 'a Entry.e -> ('a, _, 'r, 'f) ty_rule -> unit
end
(* Implementation *)
@@ -68,15 +75,15 @@ module GMake (L : GLexerType) =
struct
type te = L.te
+type 'c pattern = 'c L.pattern
type 'a parser_t = L.te Stream.t -> 'a
type grammar =
- { gtokens : (Plexing.pattern, int ref) Hashtbl.t;
- glexer : L.te Plexing.lexer }
+ { gtokens : (string * string option, int ref) Hashtbl.t }
let egram =
- {gtokens = Hashtbl.create 301; glexer = L.lexer }
+ {gtokens = Hashtbl.create 301 }
let tokens con =
let list = ref [] in
@@ -85,6 +92,17 @@ 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
+
+type ('a, 'b, 'c, 'd) ty_and_rec3 =
+| NoRec3 : (ty_norec, ty_norec, ty_norec, ty_norec) ty_and_rec3
+| MayRec3 : ('a, 'b, 'c, ty_mayrec) ty_and_rec3
+
type 'a ty_entry = {
ename : string;
mutable estart : int -> 'a parser_t;
@@ -96,45 +114,50 @@ and 'a ty_desc =
| Dlevels of 'a ty_level list
| Dparser of 'a parser_t
-and 'a ty_level = {
+and 'a ty_level = Level : (_, _, 'a) ty_rec_level -> 'a ty_level
+
+and ('trecs, 'trecp, 'a) ty_rec_level = {
assoc : g_assoc;
lname : string option;
- lsuffix : ('a, 'a -> Loc.t -> 'a) ty_tree;
- lprefix : ('a, Loc.t -> 'a) ty_tree;
+ lsuffix : ('a, 'trecs, 'a -> Loc.t -> 'a) ty_tree;
+ lprefix : ('a, 'trecp, Loc.t -> 'a) ty_tree;
}
-and ('self, 'a) ty_symbol =
-| Stoken : Plexing.pattern -> ('self, string) ty_symbol
-| Slist1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
-| Slist1sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol
-| Slist0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
-| Slist0sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol
-| Sopt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol
-| Sself : ('self, 'self) ty_symbol
-| Snext : ('self, 'self) ty_symbol
-| Snterm : 'a ty_entry -> ('self, 'a) ty_symbol
-| Snterml : 'a ty_entry * string -> ('self, 'a) ty_symbol
-| Stree : ('self, Loc.t -> 'a) ty_tree -> ('self, 'a) ty_symbol
-
-and ('self, _, 'r) ty_rule =
-| TStop : ('self, 'r, 'r) ty_rule
-| TNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule
-
-and ('self, 'a) ty_tree =
-| Node : ('self, 'b, 'a) ty_node -> ('self, 'a) ty_tree
-| LocAct : 'k * 'k list -> ('self, 'k) ty_tree
-| DeadEnd : ('self, 'k) ty_tree
-
-and ('self, 'a, 'r) ty_node = {
- node : ('self, 'a) ty_symbol;
- son : ('self, 'a -> 'r) ty_tree;
- brother : ('self, 'r) ty_tree;
+and ('self, 'trec, 'a) ty_symbol =
+| Stoken : 'c pattern -> ('self, ty_norec, 'c) ty_symbol
+| Slist1 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol
+| Slist1sep : ('self, 'trec, 'a) ty_symbol * ('self, ty_norec, _) ty_symbol * bool -> ('self, 'trec, 'a list) ty_symbol
+| Slist0 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol
+| Slist0sep : ('self, 'trec, 'a) ty_symbol * ('self, ty_norec, _) ty_symbol * bool -> ('self, 'trec, 'a list) ty_symbol
+| Sopt : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a option) ty_symbol
+| Sself : ('self, ty_mayrec, 'self) ty_symbol
+| Snext : ('self, ty_mayrec, 'self) ty_symbol
+| Snterm : 'a ty_entry -> ('self, ty_norec, 'a) ty_symbol
+| Snterml : 'a ty_entry * string -> ('self, ty_norec, 'a) ty_symbol
+| Stree : ('self, 'trec, Loc.t -> 'a) ty_tree -> ('self, 'trec, 'a) ty_symbol
+
+and ('self, _, _, 'r) ty_rule =
+| TStop : ('self, ty_norec, 'r, 'r) ty_rule
+| TNext : ('trr, 'trs, 'tr) ty_and_rec * ('self, 'trr, 'a, 'r) ty_rule * ('self, 'trs, 'b) ty_symbol -> ('self, 'tr, 'b -> 'a, 'r) ty_rule
+
+and ('self, 'trec, 'a) ty_tree =
+| Node : ('trn, 'trs, 'trb, 'tr) ty_and_rec3 * ('self, 'trn, 'trs, 'trb, 'b, 'a) ty_node -> ('self, 'tr, 'a) ty_tree
+| LocAct : 'k * 'k list -> ('self, ty_norec, 'k) ty_tree
+| DeadEnd : ('self, ty_norec, 'k) ty_tree
+
+and ('self, 'trec, 'trecs, 'trecb, 'a, 'r) ty_node = {
+ node : ('self, 'trec, 'a) ty_symbol;
+ son : ('self, 'trecs, 'a -> 'r) ty_tree;
+ brother : ('self, 'trecb, 'r) ty_tree;
}
+type 'a ty_rules =
+| TRules : (_, ty_norec, 'act, Loc.t -> 'a) ty_rule * 'act -> 'a ty_rules
+
type 'a ty_production =
-| TProd : ('a, 'act, Loc.t -> 'a) ty_rule * 'act -> 'a ty_production
+| TProd : ('a, _, 'act, Loc.t -> 'a) ty_rule * 'act -> 'a ty_production
-let rec derive_eps : type s a. (s, a) ty_symbol -> bool =
+let rec derive_eps : type s r a. (s, r, a) ty_symbol -> bool =
function
Slist0 _ -> true
| Slist0sep (_, _, _) -> true
@@ -142,14 +165,14 @@ let rec derive_eps : type s a. (s, a) ty_symbol -> bool =
| Stree t -> tree_derive_eps t
| Slist1 _ -> false
| Slist1sep (_, _, _) -> false
- | Snterm _ | Snterml (_, _) -> false
+ | Snterm _ -> false | Snterml (_, _) -> false
| Snext -> false
| Sself -> false
| Stoken _ -> false
-and tree_derive_eps : type s a. (s, a) ty_tree -> bool =
+and tree_derive_eps : type s tr a. (s, tr, a) ty_tree -> bool =
function
LocAct (_, _) -> true
- | Node {node = s; brother = bro; son = son} ->
+ | Node (_, {node = s; brother = bro; son = son}) ->
derive_eps s && tree_derive_eps son || tree_derive_eps bro
| DeadEnd -> false
@@ -158,7 +181,7 @@ let eq_entry : type a1 a2. a1 ty_entry -> a2 ty_entry -> (a1, a2) eq option = fu
if (Obj.magic e1) == (Obj.magic e2) then Some (Obj.magic Refl)
else None
-let rec eq_symbol : type s a1 a2. (s, a1) ty_symbol -> (s, a2) ty_symbol -> (a1, a2) eq option = fun s1 s2 ->
+let rec eq_symbol : type s r1 r2 a1 a2. (s, r1, a1) ty_symbol -> (s, r2, a2) ty_symbol -> (a1, a2) eq option = fun s1 s2 ->
match s1, s2 with
Snterm e1, Snterm e2 -> eq_entry e1 e2
| Snterml (e1, l1), Snterml (e2, l2) ->
@@ -188,23 +211,42 @@ let rec eq_symbol : type s a1 a2. (s, a1) ty_symbol -> (s, a2) ty_symbol -> (a1,
| Stree _, Stree _ -> None
| Sself, Sself -> Some Refl
| Snext, Snext -> Some Refl
- | Stoken p1, Stoken p2 -> if p1 = p2 then Some Refl else None
+ | Stoken p1, Stoken p2 -> L.tok_pattern_eq p1 p2
| _ -> None
-let is_before : type s1 s2 a1 a2. (s1, a1) ty_symbol -> (s2, a2) ty_symbol -> bool = fun s1 s2 ->
+let is_before : type s1 s2 r1 r2 a1 a2. (s1, r1, a1) ty_symbol -> (s2, r2, a2) ty_symbol -> bool = fun s1 s2 ->
match s1, s2 with
- Stoken ("ANY", _), _ -> false
- | _, Stoken ("ANY", _) -> true
- | Stoken (_, Some _), Stoken (_, None) -> true
- | Stoken _, Stoken _ -> false
+ | Stoken p1, Stoken p2 ->
+ snd (L.tok_pattern_strings p1) <> None
+ && snd (L.tok_pattern_strings p2) = None
| Stoken _, _ -> true
| _ -> false
(** Ancilliary datatypes *)
-type ('self, _) ty_symbols =
-| TNil : ('self, unit) ty_symbols
-| TCns : ('self, 'a) ty_symbol * ('self, 'b) ty_symbols -> ('self, 'a * 'b) ty_symbols
+type 'a ty_rec = MayRec : ty_mayrec ty_rec | NoRec : ty_norec ty_rec
+
+type ('a, 'b, 'c) ty_and_ex =
+| NR00 : (ty_mayrec, ty_mayrec, ty_mayrec) ty_and_ex
+| NR01 : (ty_mayrec, ty_norec, ty_mayrec) ty_and_ex
+| NR10 : (ty_norec, ty_mayrec, ty_mayrec) ty_and_ex
+| NR11 : (ty_norec, ty_norec, ty_norec) ty_and_ex
+
+type ('a, 'b) ty_mayrec_and_ex =
+| MayRecNR : ('a, 'b, _) ty_and_ex -> ('a, 'b) ty_mayrec_and_ex
+
+type ('s, 'a) ty_mayrec_symbol =
+| MayRecSymbol : ('s, _, 'a) ty_symbol -> ('s, 'a) ty_mayrec_symbol
+
+type ('s, 'a) ty_mayrec_tree =
+| MayRecTree : ('s, 'tr, 'a) ty_tree -> ('s, 'a) ty_mayrec_tree
+
+type ('s, 'a, 'r) ty_mayrec_rule =
+| MayRecRule : ('s, _, 'a, 'r) ty_rule -> ('s, 'a, 'r) ty_mayrec_rule
+
+type ('self, 'trec, _) ty_symbols =
+| TNil : ('self, ty_norec, unit) ty_symbols
+| TCns : ('trh, 'trt, 'tr) ty_and_rec * ('self, 'trh, 'a) ty_symbol * ('self, 'trt, 'b) ty_symbols -> ('self, 'tr, 'a * 'b) ty_symbols
(** ('i, 'p, 'f, 'r) rel_prod0 ~
∃ α₁ ... αₙ.
@@ -217,99 +259,196 @@ type ('i, _, 'f, _) rel_prod0 =
type ('p, 'k, 'r) rel_prod = (unit, 'p, 'k, 'r) rel_prod0
-type ('s, 'i, 'k, 'r) any_symbols =
-| AnyS : ('s, 'p) ty_symbols * ('i, 'p, 'k, 'r) rel_prod0 -> ('s, 'i, 'k, 'r) any_symbols
-
-(** FIXME *)
-let rec symbols : type s p k r. (s, p) ty_symbols -> (s, k, r) ty_rule -> (s, unit, k, r) any_symbols =
- fun accu r -> match r with
- | TStop -> AnyS (Obj.magic accu, Rel0)
- | TNext (r, s) ->
- let AnyS (r, pf) = symbols (TCns (s, accu)) r in
- AnyS (Obj.magic r, RelS (Obj.magic pf))
-
-let get_symbols : type s k r. (s, k, r) ty_rule -> (s, unit, k, r) any_symbols =
- fun r -> symbols TNil r
-
-let insert_tree (type s p k a) ~warning entry_name (gsymbols : (s, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, a) ty_tree) =
- let rec insert : type p f k. (s, p) ty_symbols -> (p, k, f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree =
- fun symbols pf tree action ->
+type ('s, 'tr, 'i, 'k, 'r) any_symbols =
+| AnyS : ('s, 'tr, 'p) ty_symbols * ('i, 'p, 'k, 'r) rel_prod0 -> ('s, 'tr, 'i, 'k, 'r) any_symbols
+
+type ('s, 'tr, 'k, 'r) ty_belast_rule =
+| Belast : ('trr, 'trs, 'tr) ty_and_rec * ('s, 'trr, 'k, 'a -> 'r) ty_rule * ('s, 'trs, 'a) ty_symbol -> ('s, 'tr, 'k, 'r) ty_belast_rule
+
+(* unfortunately, this is quadratic, but ty_rules aren't too long
+ * (99% of the time of length less or equal 10 and maximum is 22
+ * when compiling Coq and its standard library) *)
+let rec get_symbols : type s trec k r. (s, trec, k, r) ty_rule -> (s, trec, unit, k, r) any_symbols =
+ let rec belast_rule : type s trr trs tr a k r. (trr, trs, tr) ty_and_rec -> (s, trr, k, r) ty_rule -> (s, trs, a) ty_symbol -> (s, tr, a -> k, r) ty_belast_rule =
+ fun ar r s -> match ar, r with
+ | NoRec2, TStop -> Belast (NoRec2, TStop, s)
+ | MayRec2, TStop -> Belast (MayRec2, TStop, s)
+ | NoRec2, TNext (NoRec2, r, s') ->
+ let Belast (NoRec2, r, s') = belast_rule NoRec2 r s' in
+ Belast (NoRec2, TNext (NoRec2, r, s), s')
+ | MayRec2, TNext (_, r, s') ->
+ let Belast (_, r, s') = belast_rule MayRec2 r s' in
+ Belast (MayRec2, TNext (MayRec2, r, s), s') in
+ function
+ | TStop -> AnyS (TNil, Rel0)
+ | TNext (MayRec2, r, s) ->
+ let Belast (MayRec2, r, s) = belast_rule MayRec2 r s in
+ let AnyS (r, pf) = get_symbols r in
+ AnyS (TCns (MayRec2, s, r), RelS pf)
+ | TNext (NoRec2, r, s) ->
+ let Belast (NoRec2, r, s) = belast_rule NoRec2 r s in
+ let AnyS (r, pf) = get_symbols r in
+ AnyS (TCns (NoRec2, s, r), RelS pf)
+
+let get_rec_symbols (type s tr p) (s : (s, tr, p) ty_symbols) : tr ty_rec =
+ match s with TCns (MayRec2, _, _) -> MayRec
+ | TCns (NoRec2, _, _) -> NoRec | TNil -> NoRec
+
+let get_rec_tree (type s tr f) (s : (s, tr, f) ty_tree) : tr ty_rec =
+ match s with Node (MayRec3, _) -> MayRec
+ | Node (NoRec3, _) -> NoRec | LocAct _ -> NoRec | DeadEnd -> NoRec
+
+let and_symbols_tree (type s trs trt p f) (s : (s, trs, p) ty_symbols) (t : (s, trt, f) ty_tree) : (trs, trt) ty_mayrec_and_ex =
+ match get_rec_symbols s, get_rec_tree t with
+ | MayRec, MayRec -> MayRecNR NR00 | MayRec, NoRec -> MayRecNR NR01
+ | NoRec, MayRec -> MayRecNR NR10 | NoRec, NoRec -> MayRecNR NR11
+
+let and_and_tree (type s tr' trt tr trn trs trb f) (ar : (tr', trt, tr) ty_and_rec) (arn : (trn, trs, trb, trt) ty_and_rec3) (t : (s, trb, f) ty_tree) : (tr', trb, tr) ty_and_rec =
+ match ar, arn, get_rec_tree t with
+ | MayRec2, _, MayRec -> MayRec2 | MayRec2, _, NoRec -> MayRec2
+ | NoRec2, NoRec3, NoRec -> NoRec2
+
+let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, tr) ty_and_ex) (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, tr, a) ty_tree =
+ let rec insert : type trs trt tr p f k. (trs, trt, tr) ty_and_ex -> (s, trs, p) ty_symbols -> (p, k, f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree =
+ fun ar symbols pf tree action ->
match symbols, pf with
- TCns (s, sl), RelS pf -> insert_in_tree s sl pf tree action
+ TCns (ars, s, sl), RelS pf -> insert_in_tree ar ars s sl pf tree action
| TNil, Rel0 ->
- match tree with
- Node {node = s; son = son; brother = bro} ->
- Node {node = s; son = son; brother = insert TNil Rel0 bro action}
- | LocAct (old_action, action_list) ->
+ let node (type tb) ({node = s; son = son; brother = bro} : (_, _, _, tb, _, _) ty_node) =
+ let ar : (ty_norec, tb, tb) ty_and_ex =
+ match get_rec_tree bro with MayRec -> NR10 | NoRec -> NR11 in
+ {node = s; son = son; brother = insert ar TNil Rel0 bro action} in
+ match ar, tree with
+ | NR10, Node (_, n) -> Node (MayRec3, node n)
+ | NR11, Node (NoRec3, n) -> Node (NoRec3, node n)
+ | NR11, LocAct (old_action, action_list) ->
begin match warning with
| None -> ()
| Some warn_fn ->
let msg =
"<W> Grammar extension: " ^
- (if entry_name <> "" then "" else "in ["^entry_name^"%s], ") ^
+ (if entry_name = "" then "" else "in ["^entry_name^"%s], ") ^
"some rule has been masked" in
warn_fn msg
end;
LocAct (action, old_action :: action_list)
- | DeadEnd -> LocAct (action, [])
- and insert_in_tree : type a p f k. (s, a) ty_symbol -> (s, p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree =
- fun s sl pf tree action ->
- match try_insert s sl pf tree action with
+ | NR11, DeadEnd -> LocAct (action, [])
+ and insert_in_tree : type trs trs' trs'' trt tr a p f k. (trs'', trt, tr) ty_and_ex -> (trs, trs', trs'') ty_and_rec -> (s, trs, a) ty_symbol -> (s, trs', p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree =
+ fun ar ars s sl pf tree action ->
+ let ar : (trs'', trt, tr) ty_and_rec = match ar with NR11 -> NoRec2
+ | NR00 -> MayRec2 | NR01 -> MayRec2 | NR10 -> MayRec2 in
+ match try_insert ar ars s sl pf tree action with
Some t -> t
- | None -> Node {node = s; son = insert sl pf DeadEnd action; brother = tree}
- and try_insert : type a p f k. (s, a) ty_symbol -> (s, p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree option =
- fun s sl pf tree action ->
+ | None ->
+ let node ar =
+ {node = s; son = insert ar sl pf DeadEnd action; brother = tree} in
+ match ar, ars, get_rec_symbols sl with
+ | MayRec2, MayRec2, MayRec -> Node (MayRec3, node NR01)
+ | MayRec2, _, NoRec -> Node (MayRec3, node NR11)
+ | NoRec2, NoRec2, NoRec -> Node (NoRec3, node NR11)
+ and try_insert : type trs trs' trs'' trt tr a p f k. (trs'', trt, tr) ty_and_rec -> (trs, trs', trs'') ty_and_rec -> (s, trs, a) ty_symbol -> (s, trs', p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree option =
+ fun ar ars s sl pf tree action ->
match tree with
- Node {node = s1; son = son; brother = bro} ->
+ Node (arn, {node = s1; son = son; brother = bro}) ->
begin match eq_symbol s s1 with
| Some Refl ->
- let t = Node {node = s1; son = insert sl pf son action; brother = bro} in
- Some t
+ let MayRecNR arss = and_symbols_tree sl son in
+ let son = insert arss sl pf son action in
+ let node = {node = s1; son = son; brother = bro} in
+ begin match ar, ars, arn, arss with
+ | MayRec2, _, _, _ -> Some (Node (MayRec3, node))
+ | NoRec2, NoRec2, NoRec3, NR11 -> Some (Node (NoRec3, node)) end
| None ->
+ let ar' = and_and_tree ar arn bro in
if is_before s1 s || derive_eps s && not (derive_eps s1) then
let bro =
- match try_insert s sl pf bro action with
+ match try_insert ar' ars s sl pf bro action with
Some bro -> bro
- | None -> Node {node = s; son = insert sl pf DeadEnd action; brother = bro}
+ | None ->
+ let MayRecNR arss = and_symbols_tree sl DeadEnd in
+ let son = insert arss sl pf DeadEnd action in
+ let node = {node = s; son = son; brother = bro} in
+ match ar, ars, arn, arss with
+ | MayRec2, _, _, _ -> Node (MayRec3, node)
+ | NoRec2, NoRec2, NoRec3, NR11 -> Node (NoRec3, node)
in
- let t = Node {node = s1; son = son; brother = bro} in Some t
+ let node = {node = s1; son = son; brother = bro} in
+ match ar, arn with
+ | MayRec2, _ -> Some (Node (MayRec3, node))
+ | NoRec2, NoRec3 -> Some (Node (NoRec3, node))
else
- begin match try_insert s sl pf bro action with
+ match try_insert ar' ars s sl pf bro action with
Some bro ->
- let t = Node {node = s1; son = son; brother = bro} in Some t
+ let node = {node = s1; son = son; brother = bro} in
+ begin match ar, arn with
+ | MayRec2, _ -> Some (Node (MayRec3, node))
+ | NoRec2, NoRec3 -> Some (Node (NoRec3, node)) end
| None -> None
- end
end
- | LocAct (_, _) | DeadEnd -> None
+ | LocAct (_, _) -> None | DeadEnd -> None
in
- insert gsymbols pf tree action
+ insert ar gsymbols pf tree action
-let srules (type self a) ~warning (rl : a ty_production list) =
+let insert_tree_norec (type s p k a) ~warning entry_name (gsymbols : (s, ty_norec, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, ty_norec, a) ty_tree) : (s, ty_norec, a) ty_tree =
+ insert_tree ~warning entry_name NR11 gsymbols pf action tree
+
+let insert_tree (type s trs trt p k a) ~warning entry_name (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, a) ty_mayrec_tree =
+ let MayRecNR ar = and_symbols_tree gsymbols tree in
+ MayRecTree (insert_tree ~warning entry_name ar gsymbols pf action tree)
+
+let srules (type self a) ~warning (rl : a ty_rules list) : (self, ty_norec, a) ty_symbol =
+ let rec retype_tree : type s a. (s, ty_norec, a) ty_tree -> (self, ty_norec, a) ty_tree =
+ function
+ | Node (NoRec3, {node = s; son = son; brother = bro}) ->
+ Node (NoRec3, {node = retype_symbol s; son = retype_tree son; brother = retype_tree bro})
+ | LocAct (k, kl) -> LocAct (k, kl)
+ | DeadEnd -> DeadEnd
+ and retype_symbol : type s a. (s, ty_norec, a) ty_symbol -> (self, ty_norec, a) ty_symbol =
+ function
+ | Stoken p -> Stoken p
+ | Slist1 s -> Slist1 (retype_symbol s)
+ | Slist1sep (s, sep, b) -> Slist1sep (retype_symbol s, retype_symbol sep, b)
+ | Slist0 s -> Slist0 (retype_symbol s)
+ | Slist0sep (s, sep, b) -> Slist0sep (retype_symbol s, retype_symbol sep, b)
+ | Sopt s -> Sopt (retype_symbol s)
+ | Snterm e -> Snterm e
+ | Snterml (e, l) -> Snterml (e, l)
+ | Stree t -> Stree (retype_tree t) in
+ let rec retype_rule : type s k r. (s, ty_norec, k, r) ty_rule -> (self, ty_norec, k, r) ty_rule =
+ function
+ | TStop -> TStop
+ | TNext (NoRec2, r, s) -> TNext (NoRec2, retype_rule r, retype_symbol s) in
let t =
List.fold_left
- (fun tree (TProd (symbols, action)) ->
+ (fun tree (TRules (symbols, action)) ->
+ let symbols = retype_rule symbols in
let AnyS (symbols, pf) = get_symbols symbols in
- insert_tree ~warning "" symbols pf action tree)
+ insert_tree_norec ~warning "" symbols pf action tree)
DeadEnd rl
in
- (* FIXME: use an universal self type to ensure well-typedness *)
- (Obj.magic (Stree t) : (self, a) ty_symbol)
+ Stree t
-let is_level_labelled n lev =
+let is_level_labelled n (Level lev) =
match lev.lname with
Some n1 -> n = n1
| None -> false
-let insert_level (type s p k) ~warning entry_name (symbols : (s, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level =
+let insert_level (type s tr p k) ~warning entry_name (symbols : (s, tr, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level =
match symbols with
- | TCns (Sself, symbols) ->
+ | TCns (_, Sself, symbols) ->
+ let Level slev = slev in
let RelS pf = pf in
+ let MayRecTree lsuffix = insert_tree ~warning entry_name symbols pf action slev.lsuffix in
+ Level
{assoc = slev.assoc; lname = slev.lname;
- lsuffix = insert_tree ~warning entry_name symbols pf action slev.lsuffix;
+ lsuffix = lsuffix;
lprefix = slev.lprefix}
| _ ->
+ let Level slev = slev in
+ let MayRecTree lprefix = insert_tree ~warning entry_name symbols pf action slev.lprefix in
+ Level
{assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix;
- lprefix = insert_tree ~warning entry_name symbols pf action slev.lprefix}
+ lprefix = lprefix}
let empty_lev lname assoc =
let assoc =
@@ -317,9 +456,10 @@ let empty_lev lname assoc =
Some a -> a
| None -> LeftA
in
+ Level
{assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd}
-let change_lev ~warning lev n lname assoc =
+let change_lev ~warning (Level lev) n lname assoc =
let a =
match assoc with
None -> lev.assoc
@@ -343,6 +483,7 @@ let change_lev ~warning lev n lname assoc =
end;
| None -> ()
end;
+ Level
{assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix}
let get_level ~warning entry position levs =
@@ -396,21 +537,24 @@ let get_level ~warning entry position levs =
lev :: levs -> [], change_lev ~warning lev "<top>", levs
| [] -> [], empty_lev, []
-let change_to_self0 (type s) (type a) (entry : s ty_entry) : (s, a) ty_symbol -> (s, a) ty_symbol =
+let change_to_self0 (type s) (type trec) (type a) (entry : s ty_entry) : (s, trec, a) ty_symbol -> (s, a) ty_mayrec_symbol =
function
| Snterm e ->
begin match eq_entry e entry with
- | None -> Snterm e
- | Some Refl -> Sself
+ | None -> MayRecSymbol (Snterm e)
+ | Some Refl -> MayRecSymbol (Sself)
end
- | x -> x
+ | x -> MayRecSymbol x
-let rec change_to_self : type s a r. s ty_entry -> (s, a, r) ty_rule -> (s, a, r) ty_rule = fun e r -> match r with
-| TStop -> TStop
-| TNext (r, t) -> TNext (change_to_self e r, change_to_self0 e t)
+let rec change_to_self : type s trec a r. s ty_entry -> (s, trec, a, r) ty_rule -> (s, a, r) ty_mayrec_rule = fun e r -> match r with
+| TStop -> MayRecRule TStop
+| TNext (_, r, t) ->
+ let MayRecRule r = change_to_self e r in
+ let MayRecSymbol t = change_to_self0 e t in
+ MayRecRule (TNext (MayRec2, r, t))
let insert_tokens gram symbols =
- let rec insert : type s a. (s, a) ty_symbol -> unit =
+ let rec insert : type s trec a. (s, trec, a) ty_symbol -> unit =
function
| Slist0 s -> insert s
| Slist1 s -> insert s
@@ -418,25 +562,25 @@ let insert_tokens gram symbols =
| Slist1sep (s, t, _) -> insert s; insert t
| Sopt s -> insert s
| Stree t -> tinsert t
- | Stoken ("ANY", _) -> ()
| Stoken tok ->
- gram.glexer.Plexing.tok_using tok;
+ L.tok_using tok;
let r =
+ let tok = L.tok_pattern_strings tok in
try Hashtbl.find gram.gtokens tok with
Not_found -> let r = ref 0 in Hashtbl.add gram.gtokens tok r; r
in
incr r
- | Snterm _ | Snterml (_, _) -> ()
+ | Snterm _ -> () | Snterml (_, _) -> ()
| Snext -> ()
| Sself -> ()
- and tinsert : type s a. (s, a) ty_tree -> unit =
+ and tinsert : type s tr a. (s, tr, a) ty_tree -> unit =
function
- Node {node = s; brother = bro; son = son} ->
+ Node (_, {node = s; brother = bro; son = son}) ->
insert s; tinsert bro; tinsert son
- | LocAct (_, _) | DeadEnd -> ()
- and linsert : type s p. (s, p) ty_symbols -> unit = function
+ | LocAct (_, _) -> () | DeadEnd -> ()
+ and linsert : type s tr p. (s, tr, p) ty_symbols -> unit = function
| TNil -> ()
- | TCns (s, r) -> insert s; linsert r
+ | TCns (_, s, r) -> insert s; linsert r
in
linsert symbols
@@ -460,7 +604,7 @@ let levels_of_rules ~warning entry position rules =
let lev =
List.fold_left
(fun lev (TProd (symbols, action)) ->
- let symbols = change_to_self entry symbols in
+ let MayRecRule symbols = change_to_self entry symbols in
let AnyS (symbols, pf) = get_symbols symbols in
insert_tokens egram symbols;
insert_level ~warning entry.ename symbols pf action lev)
@@ -472,7 +616,7 @@ let levels_of_rules ~warning entry position rules =
levs1 @ List.rev levs @ levs2
let logically_eq_symbols entry =
- let rec eq_symbols : type s1 s2 a1 a2. (s1, a1) ty_symbol -> (s2, a2) ty_symbol -> bool = fun s1 s2 ->
+ let rec eq_symbols : type s1 s2 trec1 trec2 a1 a2. (s1, trec1, a1) ty_symbol -> (s2, trec2, a2) ty_symbol -> bool = fun s1 s2 ->
match s1, s2 with
Snterm e1, Snterm e2 -> e1.ename = e2.ename
| Snterm e1, Sself -> e1.ename = entry.ename
@@ -486,16 +630,19 @@ let logically_eq_symbols entry =
eq_symbols s1 s2 && eq_symbols sep1 sep2 && b1 = b2
| Sopt s1, Sopt s2 -> eq_symbols s1 s2
| Stree t1, Stree t2 -> eq_trees t1 t2
- | Stoken p1, Stoken p2 -> p1 = p2
+ | Stoken p1, Stoken p2 -> L.tok_pattern_eq p1 p2 <> None
| Sself, Sself -> true
| Snext, Snext -> true
| _ -> false
- and eq_trees : type s1 s2 a1 a2. (s1, a1) ty_tree -> (s2, a2) ty_tree -> bool = fun t1 t2 ->
+ and eq_trees : type s1 s2 tr1 tr2 a1 a2. (s1, tr1, a1) ty_tree -> (s2, tr2, a2) ty_tree -> bool = fun t1 t2 ->
match t1, t2 with
- Node n1, Node n2 ->
+ Node (_, n1), Node (_, n2) ->
eq_symbols n1.node n2.node && eq_trees n1.son n2.son &&
eq_trees n1.brother n2.brother
- | (LocAct (_, _) | DeadEnd), (LocAct (_, _) | DeadEnd) -> true
+ | LocAct _, LocAct _ -> true
+ | LocAct _, DeadEnd -> true
+ | DeadEnd, LocAct _ -> true
+ | DeadEnd, DeadEnd -> true
| _ -> false
in
eq_symbols
@@ -509,55 +656,56 @@ let logically_eq_symbols entry =
[None] if failure *)
type 's ex_symbols =
-| ExS : ('s, 'p) ty_symbols -> 's ex_symbols
+| ExS : ('s, 'tr, 'p) ty_symbols -> 's ex_symbols
let delete_rule_in_tree entry =
let rec delete_in_tree :
- type s p r. (s, p) ty_symbols -> (s, r) ty_tree -> (s ex_symbols option * (s, r) ty_tree) option =
+ type s tr tr' p r. (s, tr, p) ty_symbols -> (s, tr', r) ty_tree -> (s ex_symbols option * (s, r) ty_mayrec_tree) option =
fun symbols tree ->
match symbols, tree with
- | TCns (s, sl), Node n ->
+ | TCns (_, s, sl), Node (_, n) ->
if logically_eq_symbols entry s n.node then delete_son sl n
else
begin match delete_in_tree symbols n.brother with
- Some (dsl, t) ->
- Some (dsl, Node {node = n.node; son = n.son; brother = t})
+ Some (dsl, MayRecTree t) ->
+ Some (dsl, MayRecTree (Node (MayRec3, {node = n.node; son = n.son; brother = t})))
| None -> None
end
- | TCns (s, sl), _ -> None
- | TNil, Node n ->
+ | TCns (_, s, sl), _ -> None
+ | TNil, Node (_, n) ->
begin match delete_in_tree TNil n.brother with
- Some (dsl, t) ->
- Some (dsl, Node {node = n.node; son = n.son; brother = t})
+ Some (dsl, MayRecTree t) ->
+ Some (dsl, MayRecTree (Node (MayRec3, {node = n.node; son = n.son; brother = t})))
| None -> None
end
| TNil, DeadEnd -> None
- | TNil, LocAct (_, []) -> Some (Some (ExS TNil), DeadEnd)
- | TNil, LocAct (_, action :: list) -> Some (None, LocAct (action, list))
+ | TNil, LocAct (_, []) -> Some (Some (ExS TNil), MayRecTree DeadEnd)
+ | TNil, LocAct (_, action :: list) -> Some (None, MayRecTree (LocAct (action, list)))
and delete_son :
- type s p a r. (s, p) ty_symbols -> (s, a, r) ty_node -> (s ex_symbols option * (s, r) ty_tree) option =
+ type s p tr trn trs trb a r. (s, tr, p) ty_symbols -> (s, trn, trs, trb, a, r) ty_node -> (s ex_symbols option * (s, r) ty_mayrec_tree) option =
fun sl n ->
match delete_in_tree sl n.son with
- Some (Some (ExS dsl), DeadEnd) -> Some (Some (ExS (TCns (n.node, dsl))), n.brother)
- | Some (Some (ExS dsl), t) ->
- let t = Node {node = n.node; son = t; brother = n.brother} in
- Some (Some (ExS (TCns (n.node, dsl))), t)
- | Some (None, t) ->
- let t = Node {node = n.node; son = t; brother = n.brother} in
- Some (None, t)
+ Some (Some (ExS dsl), MayRecTree DeadEnd) -> Some (Some (ExS (TCns (MayRec2, n.node, dsl))), MayRecTree n.brother)
+ | Some (Some (ExS dsl), MayRecTree t) ->
+ let t = Node (MayRec3, {node = n.node; son = t; brother = n.brother}) in
+ Some (Some (ExS (TCns (MayRec2, n.node, dsl))), MayRecTree t)
+ | Some (None, MayRecTree t) ->
+ let t = Node (MayRec3, {node = n.node; son = t; brother = n.brother}) in
+ Some (None, MayRecTree t)
| None -> None
in
delete_in_tree
-let rec decr_keyw_use : type s a. _ -> (s, a) ty_symbol -> unit = fun gram ->
+let rec decr_keyw_use : type s tr a. _ -> (s, tr, a) ty_symbol -> unit = fun gram ->
function
Stoken tok ->
- let r = Hashtbl.find gram.gtokens tok in
+ let tok' = L.tok_pattern_strings tok in
+ let r = Hashtbl.find gram.gtokens tok' in
decr r;
if !r == 0 then
begin
- Hashtbl.remove gram.gtokens tok;
- gram.glexer.Plexing.tok_removing tok
+ Hashtbl.remove gram.gtokens tok';
+ L.tok_removing tok
end
| Slist0 s -> decr_keyw_use gram s
| Slist1 s -> decr_keyw_use gram s
@@ -567,69 +715,71 @@ let rec decr_keyw_use : type s a. _ -> (s, a) ty_symbol -> unit = fun gram ->
| Stree t -> decr_keyw_use_in_tree gram t
| Sself -> ()
| Snext -> ()
- | Snterm _ | Snterml (_, _) -> ()
-and decr_keyw_use_in_tree : type s a. _ -> (s, a) ty_tree -> unit = fun gram ->
+ | Snterm _ -> () | Snterml (_, _) -> ()
+and decr_keyw_use_in_tree : type s tr a. _ -> (s, tr, a) ty_tree -> unit = fun gram ->
function
- DeadEnd | LocAct (_, _) -> ()
- | Node n ->
+ DeadEnd -> () | LocAct (_, _) -> ()
+ | Node (_, n) ->
decr_keyw_use gram n.node;
decr_keyw_use_in_tree gram n.son;
decr_keyw_use_in_tree gram n.brother
-and decr_keyw_use_in_list : type s p. _ -> (s, p) ty_symbols -> unit = fun gram ->
+and decr_keyw_use_in_list : type s tr p. _ -> (s, tr, p) ty_symbols -> unit = fun gram ->
function
| TNil -> ()
- | TCns (s, l) -> decr_keyw_use gram s; decr_keyw_use_in_list gram l
+ | TCns (_, s, l) -> decr_keyw_use gram s; decr_keyw_use_in_list gram l
let rec delete_rule_in_suffix entry symbols =
function
- lev :: levs ->
+ Level lev :: levs ->
begin match delete_rule_in_tree entry symbols lev.lsuffix with
- Some (dsl, t) ->
+ Some (dsl, MayRecTree t) ->
begin match dsl with
Some (ExS dsl) -> decr_keyw_use_in_list egram dsl
| None -> ()
end;
- begin match t with
- DeadEnd when lev.lprefix == DeadEnd -> levs
+ begin match t, lev.lprefix with
+ DeadEnd, DeadEnd -> levs
| _ ->
let lev =
{assoc = lev.assoc; lname = lev.lname; lsuffix = t;
lprefix = lev.lprefix}
in
- lev :: levs
+ Level lev :: levs
end
| None ->
- let levs = delete_rule_in_suffix entry symbols levs in lev :: levs
+ let levs = delete_rule_in_suffix entry symbols levs in
+ Level lev :: levs
end
| [] -> raise Not_found
let rec delete_rule_in_prefix entry symbols =
function
- lev :: levs ->
+ Level lev :: levs ->
begin match delete_rule_in_tree entry symbols lev.lprefix with
- Some (dsl, t) ->
+ Some (dsl, MayRecTree t) ->
begin match dsl with
Some (ExS dsl) -> decr_keyw_use_in_list egram dsl
| None -> ()
end;
- begin match t with
- DeadEnd when lev.lsuffix == DeadEnd -> levs
+ begin match t, lev.lsuffix with
+ DeadEnd, DeadEnd -> levs
| _ ->
let lev =
{assoc = lev.assoc; lname = lev.lname; lsuffix = lev.lsuffix;
lprefix = t}
in
- lev :: levs
+ Level lev :: levs
end
| None ->
- let levs = delete_rule_in_prefix entry symbols levs in lev :: levs
+ let levs = delete_rule_in_prefix entry symbols levs in
+ Level lev :: levs
end
| [] -> raise Not_found
-let delete_rule_in_level_list (type s p) (entry : s ty_entry) (symbols : (s, p) ty_symbols) levs =
+let delete_rule_in_level_list (type s tr p) (entry : s ty_entry) (symbols : (s, tr, p) ty_symbols) levs =
match symbols with
- TCns (Sself, symbols) -> delete_rule_in_suffix entry symbols levs
- | TCns (Snterm e, symbols') ->
+ TCns (_, Sself, symbols) -> delete_rule_in_suffix entry symbols levs
+ | TCns (_, Snterm e, symbols') ->
begin match eq_entry e entry with
| None -> delete_rule_in_prefix entry symbols levs
| Some Refl ->
@@ -637,12 +787,12 @@ let delete_rule_in_level_list (type s p) (entry : s ty_entry) (symbols : (s, p)
end
| _ -> delete_rule_in_prefix entry symbols levs
-let rec flatten_tree : type s a. (s, a) ty_tree -> s ex_symbols list =
+let rec flatten_tree : type s tr a. (s, tr, a) ty_tree -> s ex_symbols list =
function
DeadEnd -> []
| LocAct (_, _) -> [ExS TNil]
- | Node {node = n; brother = b; son = s} ->
- List.map (fun (ExS l) -> ExS (TCns (n, l))) (flatten_tree s) @ flatten_tree b
+ | Node (_, {node = n; brother = b; son = s}) ->
+ List.map (fun (ExS l) -> ExS (TCns (MayRec2, n, l))) (flatten_tree s) @ flatten_tree b
let utf8_print = ref true
@@ -671,7 +821,7 @@ let string_escaped s =
let print_str ppf s = fprintf ppf "\"%s\"" (string_escaped s)
-let rec print_symbol : type s r. formatter -> (s, r) ty_symbol -> unit =
+let rec print_symbol : type s tr r. formatter -> (s, tr, r) ty_symbol -> unit =
fun ppf ->
function
| Slist0 s -> fprintf ppf "LIST0 %a" print_symbol1 s
@@ -683,30 +833,36 @@ let rec print_symbol : type s r. formatter -> (s, r) ty_symbol -> unit =
fprintf ppf "LIST1 %a SEP %a%s" print_symbol1 s print_symbol1 t
(if osep then " OPT_SEP" else "")
| Sopt s -> fprintf ppf "OPT %a" print_symbol1 s
- | Stoken (con, Some prm) when con <> "" ->
- fprintf ppf "%s@ %a" con print_str prm
+ | Stoken p when L.tok_pattern_strings p <> ("", None) ->
+ begin match L.tok_pattern_strings p with
+ | con, Some prm -> fprintf ppf "%s@ %a" con print_str prm
+ | con, None -> fprintf ppf "%s" con end
| Snterml (e, l) ->
fprintf ppf "%s%s@ LEVEL@ %a" e.ename ""
print_str l
| s -> print_symbol1 ppf s
-and print_symbol1 : type s r. formatter -> (s, r) ty_symbol -> unit =
+and print_symbol1 : type s tr r. formatter -> (s, tr, r) ty_symbol -> unit =
fun ppf ->
function
| Snterm e -> fprintf ppf "%s%s" e.ename ""
| Sself -> pp_print_string ppf "SELF"
| Snext -> pp_print_string ppf "NEXT"
- | Stoken ("", Some s) -> print_str ppf s
- | Stoken (con, None) -> pp_print_string ppf con
+ | Stoken p ->
+ begin match L.tok_pattern_strings p with
+ | "", Some s -> print_str ppf s
+ | con, None -> pp_print_string ppf con
+ | con, Some prm -> fprintf ppf "(%s@ %a)" con print_str prm end
| Stree t -> print_level ppf pp_print_space (flatten_tree t)
| s ->
fprintf ppf "(%a)" print_symbol s
-and print_rule : type s p. formatter -> (s, p) ty_symbols -> unit =
+and print_rule : type s tr p. formatter -> (s, tr, p) ty_symbols -> unit =
fun ppf symbols ->
fprintf ppf "@[<hov 0>";
- let rec fold : type s p. _ -> (s, p) ty_symbols -> unit =
- fun sep symbols -> match symbols with
+ let rec fold : type s tr p. _ -> (s, tr, p) ty_symbols -> unit =
+ fun sep symbols ->
+ match symbols with
| TNil -> ()
- | TCns (symbol, symbols) ->
+ | TCns (_, symbol, symbols) ->
fprintf ppf "%t%a" sep print_symbol symbol;
fold (fun ppf -> fprintf ppf ";@ ") symbols
in
@@ -727,9 +883,9 @@ and print_level : type s. _ -> _ -> s ex_symbols list -> _ =
let print_levels ppf elev =
let _ =
List.fold_left
- (fun sep lev ->
+ (fun sep (Level lev) ->
let rules =
- List.map (fun (ExS t) -> ExS (TCns (Sself, t))) (flatten_tree lev.lsuffix) @
+ List.map (fun (ExS t) -> ExS (TCns (MayRec2, Sself, t))) (flatten_tree lev.lsuffix) @
flatten_tree lev.lprefix
in
fprintf ppf "%t@[<hov 2>" sep;
@@ -765,31 +921,39 @@ let loc_of_token_interval bp ep =
else
let loc1 = !floc bp in let loc2 = !floc (pred ep) in Loc.merge loc1 loc2
-let name_of_symbol : type s a. s ty_entry -> (s, a) ty_symbol -> string =
+let name_of_symbol : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> string =
fun entry ->
function
Snterm e -> "[" ^ e.ename ^ "]"
| Snterml (e, l) -> "[" ^ e.ename ^ " level " ^ l ^ "]"
| Sself -> "[" ^ entry.ename ^ "]"
| Snext -> "[" ^ entry.ename ^ "]"
- | Stoken tok -> egram.glexer.Plexing.tok_text tok
+ | Stoken tok -> L.tok_text tok
| _ -> "???"
type ('r, 'f) tok_list =
| TokNil : ('f, 'f) tok_list
-| TokCns : ('r, 'f) tok_list -> (string -> 'r, 'f) tok_list
+| TokCns : 'a pattern * ('r, 'f) tok_list -> ('a -> 'r, 'f) tok_list
+
+type ('s, 'f) tok_tree = TokTree : 'a pattern * ('s, _, 'a -> 'r) ty_tree * ('r, 'f) tok_list -> ('s, 'f) tok_tree
-type ('s, 'f) tok_tree = TokTree : ('s, string -> 'r) ty_tree * ('r, 'f) tok_list -> ('s, 'f) tok_tree
+let rec tok_list_length : type a b. (a, b) tok_list -> int =
+ function
+ | TokNil -> 0
+ | TokCns (_, t) -> 1 + tok_list_length t
-let rec get_token_list : type s r f.
- s ty_entry -> _ -> _ -> _ -> (r, f) tok_list -> (s, string -> r) ty_tree -> (_ * _ * _ * (s, f) tok_tree) option =
- fun entry first_tok rev_tokl last_tok pf tree ->
+let rec get_token_list : type s tr a r f.
+ s ty_entry -> a pattern -> (r, f) tok_list -> (s, tr, a -> r) ty_tree -> (s, f) tok_tree option =
+ fun entry last_tok rev_tokl tree ->
match tree with
- Node {node = Stoken tok; son = son; brother = DeadEnd} ->
- get_token_list entry first_tok (last_tok :: rev_tokl) tok (TokCns pf) son
- | _ -> if rev_tokl = [] then None else Some (first_tok, rev_tokl, last_tok, TokTree (tree, pf))
+ Node (_, {node = Stoken tok; son = son; brother = DeadEnd}) ->
+ get_token_list entry tok (TokCns (last_tok, rev_tokl)) son
+ | _ ->
+ match rev_tokl with
+ | TokNil -> None
+ | _ -> Some (TokTree (last_tok, tree, rev_tokl))
-let rec name_of_symbol_failed : type s a. s ty_entry -> (s, a) ty_symbol -> _ =
+let rec name_of_symbol_failed : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> _ =
fun entry ->
function
| Slist0 s -> name_of_symbol_failed entry s
@@ -799,13 +963,13 @@ let rec name_of_symbol_failed : type s a. s ty_entry -> (s, a) ty_symbol -> _ =
| Sopt s -> name_of_symbol_failed entry s
| Stree t -> name_of_tree_failed entry t
| s -> name_of_symbol entry s
-and name_of_tree_failed : type s a. s ty_entry -> (s, a) ty_tree -> _ =
+and name_of_tree_failed : type s tr a. s ty_entry -> (s, tr, a) ty_tree -> _ =
fun entry ->
function
- Node {node = s; brother = bro; son = son} ->
+ Node (_, {node = s; brother = bro; son = son}) ->
let tokl =
match s with
- Stoken tok -> get_token_list entry tok [] tok TokNil son
+ Stoken tok -> get_token_list entry tok TokNil son
| _ -> None
in
begin match tokl with
@@ -818,20 +982,20 @@ and name_of_tree_failed : type s a. s ty_entry -> (s, a) ty_tree -> _ =
in
let txt =
match bro with
- DeadEnd | LocAct (_, _) -> txt
+ DeadEnd -> txt | LocAct (_, _) -> txt
| Node _ -> txt ^ " or " ^ name_of_tree_failed entry bro
in
txt
- | Some (_, rev_tokl, last_tok, _) ->
- List.fold_left
- (fun s tok ->
- (if s = "" then "" else s ^ " ") ^
- egram.glexer.Plexing.tok_text tok)
- "" (List.rev (last_tok :: rev_tokl))
+ | Some (TokTree (last_tok, _, rev_tokl)) ->
+ let rec build_str : type a b. string -> (a, b) tok_list -> string =
+ fun s -> function
+ | TokNil -> s
+ | TokCns (tok, t) -> build_str (L.tok_text tok ^ " " ^ s) t in
+ build_str (L.tok_text last_tok) rev_tokl
end
- | DeadEnd | LocAct (_, _) -> "???"
+ | DeadEnd -> "???" | LocAct (_, _) -> "???"
-let tree_failed (type s a) (entry : s ty_entry) (prev_symb_result : a) (prev_symb : (s, a) ty_symbol) tree =
+let tree_failed (type s tr a) (entry : s ty_entry) (prev_symb_result : a) (prev_symb : (s, tr, a) ty_symbol) tree =
let txt = name_of_tree_failed entry tree in
let txt =
match prev_symb with
@@ -866,14 +1030,9 @@ let tree_failed (type s a) (entry : s ty_entry) (prev_symb_result : a) (prev_sym
txt ^ " (in [" ^ entry.ename ^ "])"
let symb_failed entry prev_symb_result prev_symb symb =
- let tree = Node {node = symb; brother = DeadEnd; son = DeadEnd} in
+ let tree = Node (MayRec3, {node = symb; brother = DeadEnd; son = DeadEnd}) in
tree_failed entry prev_symb_result prev_symb tree
-let is_level_labelled n lev =
- match lev.lname with
- Some n1 -> n = n1
- | None -> false
-
let level_number entry lab =
let rec lookup levn =
function
@@ -885,7 +1044,7 @@ let level_number entry lab =
Dlevels elev -> lookup 0 elev
| Dparser _ -> raise Not_found
-let rec top_symb : type s a. s ty_entry -> (s, a) ty_symbol -> (s, a) ty_symbol =
+let rec top_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> (s, ty_norec, a) ty_symbol =
fun entry ->
function
Sself -> Snterm entry
@@ -894,7 +1053,7 @@ let rec top_symb : type s a. s ty_entry -> (s, a) ty_symbol -> (s, a) ty_symbol
| Slist1sep (s, sep, b) -> Slist1sep (top_symb entry s, sep, b)
| _ -> raise Stream.Failure
-let entry_of_symb : type s a. s ty_entry -> (s, a) ty_symbol -> a ty_entry =
+let entry_of_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> a ty_entry =
fun entry ->
function
Sself -> entry
@@ -903,12 +1062,14 @@ let entry_of_symb : type s a. s ty_entry -> (s, a) ty_symbol -> a ty_entry =
| Snterml (e, _) -> e
| _ -> raise Stream.Failure
-let top_tree : type s a. s ty_entry -> (s, a) ty_tree -> (s, a) ty_tree =
+let top_tree : type s tr a. s ty_entry -> (s, tr, a) ty_tree -> (s, tr, a) ty_tree =
fun entry ->
function
- Node {node = s; brother = bro; son = son} ->
- Node {node = top_symb entry s; brother = bro; son = son}
- | LocAct (_, _) | DeadEnd -> raise Stream.Failure
+ Node (MayRec3, {node = s; brother = bro; son = son}) ->
+ Node (MayRec3, {node = top_symb entry s; brother = bro; son = son})
+ | Node (NoRec3, {node = s; brother = bro; son = son}) ->
+ Node (NoRec3, {node = top_symb entry s; brother = bro; son = son})
+ | LocAct (_, _) -> raise Stream.Failure | DeadEnd -> raise Stream.Failure
let skip_if_empty bp p strm =
if Stream.count strm == bp then fun a -> p strm
@@ -957,18 +1118,18 @@ let call_and_push ps al strm =
let al = if !item_skipped then al else a :: al in item_skipped := false; al
let token_ematch gram tok =
- let tematch = gram.glexer.Plexing.tok_match tok in
+ let tematch = L.tok_match tok in
fun tok -> tematch tok
-let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree -> r parser_t =
+let rec parser_of_tree : type s tr r. s ty_entry -> int -> int -> (s, tr, r) ty_tree -> r parser_t =
fun entry nlevn alevn ->
function
DeadEnd -> (fun (strm__ : _ Stream.t) -> raise Stream.Failure)
| LocAct (act, _) -> (fun (strm__ : _ Stream.t) -> act)
- | Node {node = Sself; son = LocAct (act, _); brother = DeadEnd} ->
+ | Node (_, {node = Sself; son = LocAct (act, _); brother = DeadEnd}) ->
(fun (strm__ : _ Stream.t) ->
let a = entry.estart alevn strm__ in act a)
- | Node {node = Sself; son = LocAct (act, _); brother = bro} ->
+ | Node (_, {node = Sself; son = LocAct (act, _); brother = bro}) ->
let p2 = parser_of_tree entry nlevn alevn bro in
(fun (strm__ : _ Stream.t) ->
match
@@ -976,10 +1137,10 @@ let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree ->
with
Some a -> act a
| _ -> p2 strm__)
- | Node {node = s; son = son; brother = DeadEnd} ->
+ | Node (_, {node = s; son = son; brother = DeadEnd}) ->
let tokl =
match s with
- Stoken tok -> get_token_list entry tok [] tok TokNil son
+ Stoken tok -> get_token_list entry tok TokNil son
| _ -> None
in
begin match tokl with
@@ -996,19 +1157,16 @@ let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree ->
raise (Stream.Error (tree_failed entry a s son))
in
act a)
- | Some (first_tok, rev_tokl, last_tok, TokTree (son, pf)) ->
- let s = Stoken first_tok in
+ | Some (TokTree (last_tok, son, rev_tokl)) ->
let lt = Stoken last_tok in
let p1 = parser_of_tree entry nlevn alevn son in
let p1 = parser_cont p1 entry nlevn alevn lt son in
- parser_of_token_list entry s son pf p1
- (fun (strm__ : _ Stream.t) -> raise Stream.Failure) rev_tokl
- last_tok
+ parser_of_token_list entry son p1 rev_tokl last_tok
end
- | Node {node = s; son = son; brother = bro} ->
+ | Node (_, {node = s; son = son; brother = bro}) ->
let tokl =
match s with
- Stoken tok -> get_token_list entry tok [] tok TokNil son
+ Stoken tok -> get_token_list entry tok TokNil son
| _ -> None
in
match tokl with
@@ -1028,28 +1186,28 @@ let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree ->
| None -> raise (Stream.Error (tree_failed entry a s son))
end
| None -> p2 strm)
- | Some (first_tok, rev_tokl, last_tok, TokTree (son, pf)) ->
+ | Some (TokTree (last_tok, son, rev_tokl)) ->
let lt = Stoken last_tok in
let p2 = parser_of_tree entry nlevn alevn bro in
let p1 = parser_of_tree entry nlevn alevn son in
let p1 = parser_cont p1 entry nlevn alevn lt son in
let p1 =
- parser_of_token_list entry lt son pf p1 p2 rev_tokl last_tok
+ parser_of_token_list entry son p1 rev_tokl last_tok
in
fun (strm__ : _ Stream.t) ->
try p1 strm__ with Stream.Failure -> p2 strm__
-and parser_cont : type s a r.
- (a -> r) parser_t -> s ty_entry -> int -> int -> (s, a) ty_symbol -> (s, a -> r) ty_tree -> int -> a -> (a -> r) parser_t =
+and parser_cont : type s tr tr' a r.
+ (a -> r) parser_t -> s ty_entry -> int -> int -> (s, tr, a) ty_symbol -> (s, tr', a -> r) ty_tree -> int -> a -> (a -> r) parser_t =
fun p1 entry nlevn alevn s son bp a (strm__ : _ Stream.t) ->
try p1 strm__ with
Stream.Failure ->
recover parser_of_tree entry nlevn alevn bp a s son strm__
-and parser_of_token_list : type s r f.
- s ty_entry -> (s, string) ty_symbol -> (s, string -> r) ty_tree ->
- (r, f) tok_list -> (int -> string -> (string -> r) parser_t) -> f parser_t -> _ -> _ -> f parser_t =
- fun entry s son pf p1 p2 rev_tokl last_tok ->
+and parser_of_token_list : type s tr lt r f.
+ s ty_entry -> (s, tr, lt -> r) ty_tree ->
+ (int -> lt -> (lt -> r) parser_t) -> (r, f) tok_list -> lt pattern -> f parser_t =
+ fun entry son p1 rev_tokl last_tok ->
+ let n = tok_list_length rev_tokl + 1 in
let plast : r parser_t =
- let n = List.length rev_tokl + 1 in
let tematch = token_ematch egram last_tok in
let ps strm =
match peek_nth n strm with
@@ -1063,41 +1221,24 @@ and parser_of_token_list : type s r f.
let a = ps strm in
match try Some (p1 bp a strm) with Stream.Failure -> None with
Some act -> act a
- | None -> raise (Stream.Error (tree_failed entry a s son))
+ | None -> raise (Stream.Error (tree_failed entry a (Stoken last_tok) son))
in
- match List.rev rev_tokl, pf with
- [], TokNil -> (fun (strm__ : _ Stream.t) -> plast strm__)
- | tok :: tokl, TokCns pf ->
- let tematch = token_ematch egram tok in
- let ps strm =
- match peek_nth 1 strm with
- Some tok -> tematch tok
- | None -> raise Stream.Failure
- in
- let p1 =
- let rec loop : type s f. _ -> _ -> (s, f) tok_list -> (string -> s) parser_t -> (string -> f) parser_t =
- fun n tokl pf plast ->
- match tokl, pf with
- [], TokNil -> plast
- | tok :: tokl, TokCns pf ->
- let tematch = token_ematch egram tok in
- let ps strm =
- match peek_nth n strm with
- Some tok -> tematch tok
- | None -> raise Stream.Failure
- in
- let p1 = loop (n + 1) tokl pf (Obj.magic plast) in (* FIXME *)
- fun (strm__ : _ Stream.t) ->
- let a = ps strm__ in let act = p1 strm__ in (Obj.magic act a) (* FIXME *)
- | _ -> assert false
- in
- loop 2 tokl pf plast
- in
- fun (strm__ : _ Stream.t) ->
- let a = ps strm__ in let act = p1 strm__ in act a
- | _ -> assert false
-and parser_of_symbol : type s a.
- s ty_entry -> int -> (s, a) ty_symbol -> a parser_t =
+ let rec loop : type s f. _ -> (s, f) tok_list -> s parser_t -> f parser_t =
+ fun n tokl plast -> match tokl with
+ | TokNil -> plast
+ | TokCns (tok, tokl) ->
+ let tematch = token_ematch egram tok in
+ let ps strm =
+ match peek_nth n strm with
+ Some tok -> tematch tok
+ | None -> raise Stream.Failure
+ in
+ let plast = fun (strm : _ Stream.t) ->
+ let a = ps strm in let act = plast strm in act a in
+ loop (n - 1) tokl plast in
+ loop (n - 1) rev_tokl plast
+and parser_of_symbol : type s tr a.
+ s ty_entry -> int -> (s, tr, a) ty_symbol -> a parser_t =
fun entry nlevn ->
function
| Slist0 s ->
@@ -1219,22 +1360,22 @@ and parser_of_symbol : type s a.
| Sself -> (fun (strm__ : _ Stream.t) -> entry.estart 0 strm__)
| Snext -> (fun (strm__ : _ Stream.t) -> entry.estart nlevn strm__)
| Stoken tok -> parser_of_token entry tok
-and parser_of_token : type s.
- s ty_entry -> Plexing.pattern -> string parser_t =
+and parser_of_token : type s a.
+ s ty_entry -> a pattern -> a parser_t =
fun entry tok ->
- let f = egram.glexer.Plexing.tok_match tok in
+ let f = L.tok_match tok in
fun strm ->
match Stream.peek strm with
Some tok -> let r = f tok in Stream.junk strm; r
| None -> raise Stream.Failure
-and parse_top_symb : type s a. s ty_entry -> (s, a) ty_symbol -> a parser_t =
+and parse_top_symb : type s tr a. s ty_entry -> (s, tr, a) ty_symbol -> a parser_t =
fun entry symb ->
parser_of_symbol entry 0 (top_symb entry symb)
let rec start_parser_of_levels entry clevn =
function
[] -> (fun levn (strm__ : _ Stream.t) -> raise Stream.Failure)
- | lev :: levs ->
+ | Level lev :: levs ->
let p1 = start_parser_of_levels entry (succ clevn) levs in
match lev.lprefix with
DeadEnd -> p1
@@ -1277,7 +1418,7 @@ let rec start_parser_of_levels entry clevn =
let rec continue_parser_of_levels entry clevn =
function
[] -> (fun levn bp a (strm__ : _ Stream.t) -> raise Stream.Failure)
- | lev :: levs ->
+ | Level lev :: levs ->
let p1 = continue_parser_of_levels entry (succ clevn) levs in
match lev.lsuffix with
DeadEnd -> p1
@@ -1399,7 +1540,7 @@ let clear_entry e =
| Dparser _ -> ()
let parsable ?loc cs =
- let (ts, lf) = L.lexer.Plexing.tok_func ?loc cs in
+ let (ts, lf) = L.tok_func ?loc cs in
{pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf}
module Entry =
struct
@@ -1432,9 +1573,11 @@ let clear_entry e =
let s_self = Sself
let s_next = Snext
let s_token tok = Stoken tok
- let s_rules ~warning (t : 'a ty_production list) = srules ~warning t
+ let s_rules ~warning (t : 'a ty_rules list) = srules ~warning t
let r_stop = TStop
- let r_next r s = TNext (r, s)
+ let r_next r s = TNext (MayRec2, r, s)
+ let r_next_norec r s = TNext (NoRec2, r, s)
+ let rules (p, act) = TRules (p, act)
let production (p, act) = TProd (p, act)
module Unsafe =
struct
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 453ec85187..ec4ec62409 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -15,13 +15,14 @@
rule "an entry cannot call an entry of another grammar" by
normal OCaml typing. *)
-module type GLexerType = sig type te val lexer : te Plexing.lexer end
+module type GLexerType = Plexing.Lexer
(** The input signature for the functor [Grammar.GMake]: [te] is the
type of the tokens. *)
module type S =
sig
type te
+ type 'c pattern
type parsable
val parsable : ?loc:Loc.t -> char Stream.t -> parsable
val tokens : string -> (string option * int) list
@@ -35,29 +36,37 @@ module type S =
val parse_token_stream : 'a e -> te Stream.t -> 'a
val print : Format.formatter -> 'a e -> unit
end
- type ('self, 'a) ty_symbol
- type ('self, 'f, 'r) ty_rule
+ 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
type 'a ty_production
- val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol
- val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol
- val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
+ val s_nterm : 'a Entry.e -> ('self, ty_norec, 'a) ty_symbol
+ val s_nterml : 'a Entry.e -> string -> ('self, ty_norec, 'a) ty_symbol
+ val s_list0 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol
val s_list0sep :
- ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool ->
- ('self, 'a list) ty_symbol
- val s_list1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
+ ('self, 'trec, 'a) ty_symbol -> ('self, ty_norec, 'b) ty_symbol -> bool ->
+ ('self, 'trec, 'a list) ty_symbol
+ val s_list1 : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a list) ty_symbol
val s_list1sep :
- ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool ->
- ('self, 'a list) ty_symbol
- val s_opt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol
- val s_self : ('self, 'self) ty_symbol
- val s_next : ('self, 'self) ty_symbol
- val s_token : Plexing.pattern -> ('self, string) ty_symbol
- val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol
- val r_stop : ('self, 'r, 'r) ty_rule
+ ('self, 'trec, 'a) ty_symbol -> ('self, ty_norec, 'b) ty_symbol -> bool ->
+ ('self, 'trec, 'a list) ty_symbol
+ val s_opt : ('self, 'trec, 'a) ty_symbol -> ('self, 'trec, 'a option) ty_symbol
+ val s_self : ('self, ty_mayrec, 'self) ty_symbol
+ val s_next : ('self, ty_mayrec, 'self) ty_symbol
+ val s_token : 'c pattern -> ('self, ty_norec, 'c) ty_symbol
+ val s_rules : warning:(string -> unit) option -> 'a ty_rules list -> ('self, ty_norec, 'a) ty_symbol
+
+ val r_stop : ('self, ty_norec, 'r, 'r) ty_rule
val r_next :
- ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol ->
- ('self, 'b -> 'a, 'r) ty_rule
- val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
+ ('self, _, 'a, 'r) ty_rule -> ('self, _, 'b) ty_symbol ->
+ ('self, ty_mayrec, 'b -> 'a, 'r) ty_rule
+ val r_next_norec :
+ ('self, ty_norec, 'a, 'r) ty_rule -> ('self, ty_norec, 'b) ty_symbol ->
+ ('self, ty_norec, 'b -> 'a, 'r) ty_rule
+ val rules : (_, ty_norec, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_rules
+ val production : ('a, _, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production
module Unsafe :
sig
@@ -68,7 +77,7 @@ module type S =
(string option * Gramext.g_assoc option * 'a ty_production list)
list ->
unit
- val safe_delete_rule : 'a Entry.e -> ('a, 'f, 'r) ty_rule -> unit
+ val safe_delete_rule : 'a Entry.e -> ('a, _, 'f, 'r) ty_rule -> unit
end
(** Signature type of the functor [Grammar.GMake]. The types and
functions are almost the same than in generic interface, but:
@@ -80,4 +89,5 @@ module type S =
type (instead of (string * string)); the module parameter
must specify a way to show them as (string * string) *)
-module GMake (L : GLexerType) : S with type te = L.te
+module GMake (L : GLexerType) :
+ S with type te = L.te and type 'c pattern = 'c L.pattern
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index 6da06f147f..e881ab3350 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -2,15 +2,17 @@
(* plexing.ml,v *)
(* Copyright (c) INRIA 2007-2017 *)
-type pattern = string * string option
-
type location_function = int -> Loc.t
type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function
-type 'te lexer =
- { tok_func : 'te lexer_func;
- tok_using : pattern -> unit;
- tok_removing : pattern -> unit;
- tok_match : pattern -> 'te -> string;
- tok_text : pattern -> string;
- }
+module type Lexer = sig
+ type te
+ type 'c pattern
+ val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option
+ val tok_pattern_strings : 'c pattern -> string * string option
+ val tok_func : te lexer_func
+ val tok_using : 'c pattern -> unit
+ val tok_removing : 'c pattern -> unit
+ val tok_match : 'c pattern -> te -> 'c
+ val tok_text : 'c pattern -> string
+end
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli
index 26443df026..521eba7446 100644
--- a/gramlib/plexing.mli
+++ b/gramlib/plexing.mli
@@ -8,27 +8,21 @@
grammars (see module [Grammar]). It also provides some useful functions
to create lexers. *)
-type pattern = string * string option
- (* Type for values used by the generated code of the EXTEND
- statement to represent terminals in entry rules.
-- The first string is the constructor name (must start with
- an uppercase character). When it is empty, the second string
- is supposed to be a keyword.
-- The second component is the constructor parameter. None if it
- has no parameter (corresponding to the 'wildcard' pattern).
-- The way tokens patterns are interpreted to parse tokens is done
- by the lexer, function [tok_match] below. *)
-
(** Lexer type *)
-type 'te lexer =
- { tok_func : 'te lexer_func;
- tok_using : pattern -> unit;
- tok_removing : pattern -> unit;
- tok_match : pattern -> 'te -> string;
- tok_text : pattern -> string;
- }
-and 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function
+type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function
and location_function = int -> Loc.t
(** The type of a function giving the location of a token in the
source from the token number in the stream (starting from zero). *)
+
+module type Lexer = sig
+ type te
+ type 'c pattern
+ val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option
+ val tok_pattern_strings : 'c pattern -> string * string option
+ val tok_func : te lexer_func
+ val tok_using : 'c pattern -> unit
+ val tok_removing : 'c pattern -> unit
+ val tok_match : 'c pattern -> te -> 'c
+ val tok_text : 'c pattern -> string
+end
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index 33890545da..b81d89edf9 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -790,20 +790,25 @@ let loct_add loct i loc = Hashtbl.add loct i loc
we unfreeze the state of the lexer. This restores the behaviour of the
lexer. B.B. *)
-type te = Tok.t
-
(** Names of tokens, for this lexer, used in Grammar error messages *)
-let token_text = function
- | ("", Some t) -> "'" ^ t ^ "'"
- | ("IDENT", None) -> "identifier"
- | ("IDENT", Some t) -> "'" ^ t ^ "'"
- | ("INT", None) -> "integer"
- | ("INT", Some s) -> "'" ^ s ^ "'"
- | ("STRING", None) -> "string"
- | ("EOI", None) -> "end of input"
- | (con, None) -> con
- | (con, Some prm) -> con ^ " \"" ^ prm ^ "\""
+let token_text : type c. c Tok.p -> string = function
+ | PKEYWORD t -> "'" ^ t ^ "'"
+ | PIDENT None -> "identifier"
+ | PIDENT (Some t) -> "'" ^ t ^ "'"
+ | PINT None -> "integer"
+ | PINT (Some s) -> "'" ^ s ^ "'"
+ | PSTRING None -> "string"
+ | PSTRING (Some s) -> "STRING \"" ^ s ^ "\""
+ | PLEFTQMARK -> "LEFTQMARK"
+ | PEOI -> "end of input"
+ | PPATTERNIDENT None -> "PATTERNIDENT"
+ | PPATTERNIDENT (Some s) -> "PATTERNIDENT \"" ^ s ^ "\""
+ | PFIELD None -> "FIELD"
+ | PFIELD (Some s) -> "FIELD \"" ^ s ^ "\""
+ | PBULLET None -> "BULLET"
+ | PBULLET (Some s) -> "BULLET \"" ^ s ^ "\""
+ | PQUOTATION lbl -> "QUOTATION \"" ^ lbl ^ "\""
let func next_token ?loc cs =
let loct = loct_create () in
@@ -817,18 +822,24 @@ let func next_token ?loc cs =
in
(ts, loct_func loct)
-let make_lexer ~diff_mode = {
- Plexing.tok_func = func (next_token ~diff_mode);
- Plexing.tok_using =
- (fun pat -> match Tok.is_keyword pat with
- | Some (false,s) -> add_keyword ~quotation:NoQuotation s
- | Some (true,s) -> add_keyword ~quotation:Quotation s
- | None -> ());
- Plexing.tok_removing = (fun _ -> ());
- Plexing.tok_match = Tok.match_pattern;
- Plexing.tok_text = token_text }
+module MakeLexer (Diff : sig val mode : bool end) = struct
+ type te = Tok.t
+ type 'c pattern = 'c Tok.p
+ let tok_pattern_eq = Tok.equal_p
+ let tok_pattern_strings = Tok.pattern_strings
+ let tok_func = func (next_token ~diff_mode:Diff.mode)
+ let tok_using : type c. c pattern -> unit = function
+ | PKEYWORD s -> add_keyword ~quotation:NoQuotation s
+ | PQUOTATION s -> add_keyword ~quotation:Quotation s
+ | _ -> ()
+ let tok_removing = (fun _ -> ())
+ let tok_match = Tok.match_pattern
+ let tok_text = token_text
+end
+
+module Lexer = MakeLexer (struct let mode = false end)
-let lexer = make_lexer ~diff_mode:false
+module LexerDiff = MakeLexer (struct let mode = true end)
(** Terminal symbols interpretation *)
@@ -863,6 +874,6 @@ let strip s =
let terminal s =
let s = strip s in
let () = match s with "" -> failwith "empty token." | _ -> () in
- if is_ident_not_keyword s then "IDENT", Some s
- else if is_number s then "INT", Some s
- else "", Some s
+ if is_ident_not_keyword s then PIDENT (Some s)
+ else if is_number s then PINT (Some s)
+ else PKEYWORD s
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 6d5a621877..9df3e45f49 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -45,26 +45,14 @@ val get_keyword_state : unit -> keyword_state
val check_ident : string -> unit
val is_ident : string -> bool
val check_keyword : string -> unit
-val terminal : string -> Tok.pattern
-(** The lexer of Coq: *)
-
-(* modtype Grammar.GLexerType: sig
- type te val
- lexer : te Plexing.lexer
- end
+(** When string is neither an ident nor an int, returns a keyword. *)
+val terminal : string -> string Tok.p
-where
+(** The lexer of Coq: *)
- type lexer 'te =
- { tok_func : lexer_func 'te;
- tok_using : pattern -> unit;
- tok_removing : pattern -> unit;
- tok_match : pattern -> 'te -> string;
- tok_text : pattern -> string;
- tok_comm : mutable option (list location) }
- *)
-include Gramlib.Grammar.GLexerType with type te = Tok.t
+module Lexer :
+ Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p
module Error : sig
type t
@@ -90,4 +78,5 @@ as if it was unquoted, possibly becoming multiple tokens
it was not in a comment, possibly becoming multiple tokens
- return any unrecognized Ascii or UTF-8 character as a string
*)
-val make_lexer : diff_mode:bool -> Tok.t Gramlib.Plexing.lexer
+module LexerDiff :
+ Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p
diff --git a/parsing/extend.ml b/parsing/extend.ml
index ff879dd1c2..dd7c301dfb 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -10,7 +10,7 @@
(** Entry keys for constr notations *)
-type 'a entry = 'a Gramlib.Grammar.GMake(CLexer).Entry.e
+type 'a entry = 'a Gramlib.Grammar.GMake(CLexer.Lexer).Entry.e
type side = Left | Right
@@ -44,7 +44,7 @@ type simple_constr_prod_entry_key =
(** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *)
-type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.pattern list
+type binder_entry_kind = ETBinderOpen | ETBinderClosed of string Tok.p list
type binder_target = ForBinder | ForTerm
@@ -54,7 +54,7 @@ type constr_prod_entry_key =
| ETProdBigint (* Parsed as an (unbounded) integer *)
| ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
| ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *)
- | ETProdConstrList of (production_level * production_position) * Tok.pattern list (* Parsed as non-empty list of constr *)
+ | ETProdConstrList of (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr *)
| ETProdBinderList of binder_entry_kind (* Parsed as non-empty list of local binders *)
(** {5 AST for user-provided entries} *)
@@ -79,30 +79,34 @@ type ('a,'b,'c) ty_user_symbol =
(** {5 Type-safe grammar extension} *)
-type ('self, 'a) symbol =
-| Atoken : Tok.pattern -> ('self, string) symbol
-| Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol
-| Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol
-| Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol
-| Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol
-| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol
-| Aself : ('self, 'self) symbol
-| Anext : ('self, 'self) symbol
-| Aentry : 'a entry -> ('self, 'a) symbol
-| Aentryl : 'a entry * string -> ('self, 'a) 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 }
+type norec = NoRec (* just two *)
+type mayrec = MayRec (* incompatible types *)
+
+type ('self, 'trec, 'a) symbol =
+| Atoken : 'c Tok.p -> ('self, norec, 'c) symbol
+| Alist1 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol
+| Alist1sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol
+ -> ('self, 'trec, 'a list) symbol
+| Alist0 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol
+| Alist0sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol
+ -> ('self, 'trec, 'a list) symbol
+| Aopt : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a option) symbol
+| Aself : ('self, mayrec, 'self) symbol
+| Anext : ('self, mayrec, 'self) symbol
+| Aentry : 'a entry -> ('self, norec, 'a) symbol
+| Aentryl : 'a entry * string -> ('self, norec, 'a) symbol
+| Arules : 'a rules list -> ('self, norec, 'a) symbol
+
+and ('self, 'trec, _, 'r) rule =
+| Stop : ('self, norec, 'r, 'r) rule
+| Next : ('self, _, 'a, 'r) rule * ('self, _, 'b) symbol -> ('self, mayrec, 'b -> 'a, 'r) rule
+| NextNoRec : ('self, norec, 'a, 'r) rule * ('self, norec, 'b) symbol -> ('self, norec, 'b -> 'a, 'r) rule
and 'a rules =
-| Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules
+| Rules : (_, norec, 'act, Loc.t -> 'a) rule * 'act -> 'a rules
type 'a production_rule =
-| Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
+| Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
type 'a single_extend_statement =
string option *
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index a50f8d69e3..6df0d6f21a 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -21,7 +21,7 @@ type level = Constrexpr.notation_entry * precedence * tolerability list * constr
(* first argument is InCustomEntry s for custom entries *)
type grammar_constr_prod_item =
- | GramConstrTerminal of Tok.pattern
+ | GramConstrTerminal of string Tok.p
| GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option
| GramConstrListMark of int * bool * int
(* tells action rule to make a list of the n previous parsed items;
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index f2f5d17da3..8f38e437b4 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -17,7 +17,7 @@ open Gramlib
(** The parser of Coq *)
module G : sig
- include Grammar.S with type te = Tok.t
+ include Grammar.S with type te = Tok.t and type 'c pattern = 'c Tok.p
(* where Grammar.S
@@ -67,7 +67,7 @@ module type S =
end with type 'a Entry.e = 'a Extend.entry = struct
- include Grammar.GMake(CLexer)
+ include Grammar.GMake(CLexer.Lexer)
type coq_parsable = parsable * CLexer.lexer_state ref
@@ -107,7 +107,7 @@ end
module Entry =
struct
- type 'a t = 'a Grammar.GMake(CLexer).Entry.e
+ type 'a t = 'a Grammar.GMake(CLexer.Lexer).Entry.e
let create = G.Entry.create
let parse = G.entry_parse
@@ -118,15 +118,6 @@ struct
end
-module Symbols : sig
- val slist0sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol
- val slist1sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol
-end = struct
-
- let slist0sep x y = G.s_list0sep x y false
- let slist1sep x y = G.s_list1sep x y false
-end
-
(** Grammar extensions *)
(** NB: [extend_statement =
@@ -140,43 +131,73 @@ end
(** Binding general entry keys to symbol *)
-type ('s, 'a, 'r) casted_rule = Casted : ('s, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, 'a, 'r) casted_rule
-
-let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol = function
-| Atoken t -> G.s_token t
-| Alist1 s -> G.s_list1 (symbol_of_prod_entry_key s)
+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 =
+function
+| Atoken t -> CastedSNo (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
| Alist1sep (s,sep) ->
- Symbols.slist1sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep)
-| Alist0 s -> G.s_list0 (symbol_of_prod_entry_key s)
+ 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
+| 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
| Alist0sep (s,sep) ->
- Symbols.slist0sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep)
-| Aopt s -> G.s_opt (symbol_of_prod_entry_key s)
-| Aself -> G.s_self
-| Anext -> G.s_next
-| Aentry e -> G.s_nterm e
-| Aentryl (e, n) -> G.s_nterml e n
+ 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
+| 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)
| Arules rs ->
let warning msg = Feedback.msg_warning Pp.(str msg) in
- G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs)
+ CastedSNo (G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs))
-and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Loc.t -> r) casted_rule = function
-| Stop -> Casted (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) casted_rule = function
+| Stop -> CastedRNo (G.r_stop, fun act loc -> act loc)
| Next (r, s) ->
- let Casted (r, cast) = symbol_of_rule r in
- Casted (G.r_next r (symbol_of_prod_entry_key s), (fun act x -> cast (act x)))
-
-and symbol_of_rules : type a. a Extend.rules -> a G.ty_production = function
+ 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
+| 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)))
+
+and symbol_of_rules : type a. a Extend.rules -> a G.ty_rules = function
| Rules (r, act) ->
- let Casted (symb, cast) = symbol_of_rule r.norec_rule in
- G.production (symb, cast act)
+ let CastedRNo (symb, cast) = symbol_of_rule r in
+ G.rules (symb, cast act)
(** FIXME: This is a hack around a deficient camlp5 API *)
-type 'a any_production = AnyProduction : ('a, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production
+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) ->
- let Casted (symb, cast) = symbol_of_rule toks in
- AnyProduction (symb, cast act)
+ match symbol_of_rule toks with
+ | CastedRNo (symb, cast) -> AnyProduction (symb, cast act)
+ | CastedRMay (symb, cast) -> AnyProduction (symb, cast act)
let of_coq_single_extend_statement (lvl, assoc, rule) =
(lvl, assoc, List.map of_coq_production_rule rule)
@@ -288,7 +309,7 @@ let make_rule r = [None, None, r]
let eoi_entry en =
let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in
- let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (G.s_token Tok.pattern_for_EOI) in
+ let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (G.s_token Tok.PEOI) in
let act = fun _ x loc -> x in
let warning msg = Feedback.msg_warning Pp.(str msg) in
Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]);
@@ -425,8 +446,11 @@ module Module =
let module_expr = Entry.create "module_expr"
let module_type = Entry.create "module_type"
end
-let epsilon_value f e =
- let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in
+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 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 0418249e42..e361f0d00f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -203,7 +203,7 @@ module Module :
val module_type : module_ast Entry.t
end
-val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
+val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Extend.symbol -> 'self option
(** {5 Extending the parser without synchronization} *)
diff --git a/parsing/tok.ml b/parsing/tok.ml
index f0846dcf90..186d0502fc 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -12,6 +12,31 @@
let string_equal (s1 : string) s2 = s1 = s2
+type 'c p =
+ | PKEYWORD : string -> string p
+ | PPATTERNIDENT : string option -> string p
+ | PIDENT : string option -> string p
+ | PFIELD : string option -> string p
+ | PINT : string option -> string p
+ | PSTRING : string option -> string p
+ | PLEFTQMARK : unit p
+ | PBULLET : string option -> string p
+ | PQUOTATION : string -> string p
+ | PEOI : unit p
+
+let pattern_strings : type c. c p -> string * string option =
+ function
+ | PKEYWORD s -> "", Some s
+ | PPATTERNIDENT s -> "PATTERNIDENT", s
+ | PIDENT s -> "IDENT", s
+ | PFIELD s -> "FIELD", s
+ | PINT s -> "INT", s
+ | PSTRING s -> "STRING", s
+ | PLEFTQMARK -> "LEFTQMARK", None
+ | PBULLET s -> "BULLET", s
+ | PQUOTATION lbl -> "QUOTATION", Some lbl
+ | PEOI -> "EOI", None
+
type t =
| KEYWORD of string
| PATTERNIDENT of string
@@ -24,6 +49,22 @@ type t =
| QUOTATION of string * string
| EOI
+let equal_p (type a b) (t1 : a p) (t2 : b p) : (a, b) Util.eq option =
+ let streq s1 s2 = match s1, s2 with None, None -> true
+ | Some s1, Some s2 -> string_equal s1 s2 | _ -> false in
+ match t1, t2 with
+ | PKEYWORD s1, PKEYWORD s2 when string_equal s1 s2 -> Some Util.Refl
+ | PPATTERNIDENT s1, PPATTERNIDENT s2 when streq s1 s2 -> Some Util.Refl
+ | PIDENT s1, PIDENT s2 when streq s1 s2 -> Some Util.Refl
+ | PFIELD s1, PFIELD s2 when streq s1 s2 -> Some Util.Refl
+ | PINT s1, PINT s2 when streq s1 s2 -> Some Util.Refl
+ | PSTRING s1, PSTRING s2 when streq s1 s2 -> Some Util.Refl
+ | PLEFTQMARK, PLEFTQMARK -> Some Util.Refl
+ | PBULLET s1, PBULLET s2 when streq s1 s2 -> Some Util.Refl
+ | PQUOTATION s1, PQUOTATION s2 when string_equal s1 s2 -> Some Util.Refl
+ | PEOI, PEOI -> Some Util.Refl
+ | _ -> None
+
let equal t1 t2 = match t1, t2 with
| IDENT s1, KEYWORD s2 -> string_equal s1 s2
| KEYWORD s1, KEYWORD s2 -> string_equal s1 s2
@@ -63,22 +104,6 @@ let extract_string diff_mode = function
| QUOTATION(_,s) -> s
| EOI -> ""
-let to_string = function
- | KEYWORD s -> Format.sprintf "%S" s
- | IDENT s -> Format.sprintf "IDENT %S" s
- | PATTERNIDENT s -> Format.sprintf "PATTERNIDENT %S" s
- | FIELD s -> Format.sprintf "FIELD %S" s
- | INT s -> Format.sprintf "INT %s" s
- | STRING s -> Format.sprintf "STRING %S" s
- | LEFTQMARK -> "LEFTQMARK"
- | BULLET s -> Format.sprintf "BULLET %S" s
- | QUOTATION(lbl,s) -> lbl ^ s
- | EOI -> "EOI"
-
-let match_keyword kwd = function
- | KEYWORD kwd' when kwd = kwd' -> true
- | _ -> false
-
(* Invariant, txt is "ident" or a well parenthesized "{{....}}" *)
let trim_quotation txt =
let len = String.length txt in
@@ -93,45 +118,23 @@ let trim_quotation txt =
aux 0
else None, txt
-(* Needed to fix Camlp5 signature.
- Cannot use Pp because of silly Tox -> Compat -> Pp dependency *)
-let print ppf tok = Format.pp_print_string ppf (to_string tok)
-
-(** For camlp5, conversion from/to [Plexing.pattern],
- and a match function analoguous to [Plexing.default_match] *)
-
-type pattern = string * string option
-
-let is_keyword = function
- | "", Some s -> Some (false,s)
- | "QUOTATION", Some s -> Some (true,s)
- | _ -> None
-
-let pattern_for_EOI = ("EOI",None)
-let pattern_for_KEYWORD s = ("",Some s)
-let pattern_for_IDENT s = ("IDENT",Some s)
-
-let match_pattern (key, value) =
+let match_pattern (type c) (p : c p) : t -> c =
let err () = raise Stream.Failure in
- let cond x =
- match value with
- | None -> x
- | Some value -> if string_equal value x then x else err () in
- match key with
- | "" -> (function KEYWORD s -> cond s | _ -> err ())
- | "IDENT" when value <> None -> (function (IDENT s | KEYWORD s) -> cond s | _ -> err ())
- | "IDENT" -> (function IDENT s -> cond s | _ -> err ())
- | "PATTERNIDENT" -> (function PATTERNIDENT s -> cond s | _ -> err ())
- | "FIELD" -> (function FIELD s -> cond s | _ -> err ())
- | "INT" -> (function INT s -> cond s | _ -> err ())
- | "STRING" -> (function STRING s -> cond s | _ -> err ())
- | "LEFTQMARK" -> (function LEFTQMARK -> cond "" | _ -> err ())
- | "BULLET" -> (function BULLET s -> cond s | _ -> err ())
- | "QUOTATION" -> (function
- | QUOTATION(lbl,s) ->
- begin match value with
- | None -> assert false
- | Some lbl1 -> if string_equal lbl1 lbl then s else err () end
- | _ -> err ())
- | "EOI" -> (function EOI -> cond "" | _ -> err ())
- | p -> CErrors.anomaly Pp.(str "Tok: unknown pattern " ++ str p)
+ let seq = string_equal in
+ match p with
+ | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | _ -> err ())
+ | PIDENT None -> (function IDENT s' -> s' | _ -> err ())
+ | PIDENT (Some s) -> (function (IDENT s' | KEYWORD s') when seq s s' -> s' | _ -> err ())
+ | PPATTERNIDENT None -> (function PATTERNIDENT s -> s | _ -> err ())
+ | PPATTERNIDENT (Some s) -> (function PATTERNIDENT s' when seq s s' -> s' | _ -> err ())
+ | PFIELD None -> (function FIELD s -> s | _ -> err ())
+ | PFIELD (Some s) -> (function FIELD s' when seq s s' -> s' | _ -> err ())
+ | PINT None -> (function INT s -> s | _ -> err ())
+ | PINT (Some s) -> (function INT s' when seq s s' -> s' | _ -> err ())
+ | PSTRING None -> (function STRING s -> s | _ -> err ())
+ | PSTRING (Some s) -> (function STRING s' when seq s s' -> s' | _ -> err ())
+ | PLEFTQMARK -> (function LEFTQMARK -> () | _ -> err ())
+ | PBULLET None -> (function BULLET s -> s | _ -> err ())
+ | PBULLET (Some s) -> (function BULLET s' when seq s s' -> s' | _ -> err ())
+ | PQUOTATION lbl -> (function QUOTATION(lbl',s') when string_equal lbl lbl' -> s' | _ -> err ())
+ | PEOI -> (function EOI -> () | _ -> err ())
diff --git a/parsing/tok.mli b/parsing/tok.mli
index 8a255be06f..678877720d 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -10,6 +10,20 @@
(** The type of token for the Coq lexer and parser *)
+type 'c p =
+ | PKEYWORD : string -> string p
+ | PPATTERNIDENT : string option -> string p
+ | PIDENT : string option -> string p
+ | PFIELD : string option -> string p
+ | PINT : string option -> string p
+ | PSTRING : string option -> string p
+ | PLEFTQMARK : unit p
+ | PBULLET : string option -> string p
+ | PQUOTATION : string -> string p
+ | PEOI : unit p
+
+val pattern_strings : 'c p -> string * string option
+
type t =
| KEYWORD of string
| PATTERNIDENT of string
@@ -22,13 +36,11 @@ type t =
| QUOTATION of string * string
| EOI
+val equal_p : 'a p -> 'b p -> ('a, 'b) Util.eq option
+
val equal : t -> t -> bool
(* pass true for diff_mode *)
val extract_string : bool -> t -> string
-val to_string : t -> string
-(* Needed to fit Camlp5 signature *)
-val print : Format.formatter -> t -> unit
-val match_keyword : string -> t -> bool
(** Utility function for the test returned by a QUOTATION token:
It returns the delimiter parenthesis, if any, and the text
@@ -37,12 +49,6 @@ val trim_quotation : string -> char option * string
(** for camlp5,
eg GRAMMAR EXTEND ..... [ IDENT "x" -> .... END
- is a pattern ("IDENT", Some "x")
+ is a pattern (PIDENT (Some "x"))
*)
-type pattern = string * string option (* = Plexing.pattern *)
-
-val is_keyword : pattern -> (bool * string) option
-val pattern_for_EOI : pattern
-val pattern_for_KEYWORD : string -> pattern
-val pattern_for_IDENT : string -> pattern
-val match_pattern : pattern -> t -> string
+val match_pattern : 'c p -> t -> 'c
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index b770b97384..814be64f81 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -48,7 +48,7 @@ let atactic n =
else Aentryl (Pltac.tactic_expr, string_of_int n)
type entry_name = EntryName :
- 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
+ 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Extend.symbol -> entry_name
(** Quite ad-hoc *)
let get_tacentry n m =
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index ab4501fe75..d042a1d650 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -102,8 +102,7 @@ let tokenize_string s =
let st = CLexer.get_lexer_state () in
try
let istr = Stream.of_string s in
- let lexer = CLexer.make_lexer ~diff_mode:true in
- let lex = lexer.Gramlib.Plexing.tok_func istr in
+ let lex = CLexer.LexerDiff.tok_func istr in
let toks = stream_tok [] (fst lex) in
CLexer.set_lexer_state st;
toks
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index f96b567f1b..f1a08cc9b3 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -247,10 +247,10 @@ type (_, _) entry =
| TTReference : ('self, qualid) entry
| TTBigint : ('self, Constrexpr.raw_natural_number) entry
| TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
-| TTConstrList : prod_info * Tok.pattern list * 'r target -> ('r, 'r list) entry
+| TTConstrList : prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
| TTPattern : int -> ('self, cases_pattern_expr) entry
| TTOpenBinderList : ('self, local_binder_expr list) entry
-| TTClosedBinderList : Tok.pattern list -> ('self, local_binder_expr list list) entry
+| TTClosedBinderList : string Tok.p list -> ('self, local_binder_expr list list) entry
type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
@@ -319,41 +319,49 @@ let is_binder_level from e = match e with
let make_sep_rules = function
| [tk] -> Atoken tk
| tkl ->
- let rec mkrule : Tok.pattern list -> string rules = function
- | [] -> Rules ({ norec_rule = Stop }, fun _ -> (* dropped anyway: *) "")
+ let rec mkrule : 'a Tok.p list -> 'a rules = function
+ | [] -> Rules (Stop, fun _ -> (* dropped anyway: *) "")
| tkn :: rem ->
- let Rules ({ norec_rule = r }, f) = mkrule rem in
- let r = { norec_rule = Next (r, Atoken tkn) } in
+ let Rules (r, f) = mkrule rem in
+ let r = NextNoRec (r, Atoken tkn) in
Rules (r, fun _ -> f)
in
let r = mkrule (List.rev tkl) in
Arules [r]
-let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) symbol = fun custom p assoc from forpat ->
- if custom = InConstrEntry && is_binder_level from p then Aentryl (target_entry InConstrEntry forpat, "200")
- else if is_self from p then Aself
+type ('s, 'a) mayrec_symbol =
+| MayRecNo : ('s, norec, 'a) symbol -> ('s, 'a) mayrec_symbol
+| MayRecMay : ('s, mayrec, 'a) symbol -> ('s, 'a) mayrec_symbol
+
+let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat ->
+ if custom = InConstrEntry && is_binder_level from p then MayRecNo (Aentryl (target_entry InConstrEntry forpat, "200"))
+ else if is_self from p then MayRecMay Aself
else
let g = target_entry custom forpat in
let lev = adjust_level assoc from p in
begin match lev with
- | None -> Aentry g
- | Some None -> Anext
- | Some (Some (lev, cur)) -> Aentryl (g, string_of_int lev)
+ | None -> MayRecNo (Aentry g)
+ | Some None -> MayRecMay Anext
+ | Some (Some (lev, cur)) -> MayRecNo (Aentryl (g, string_of_int lev))
end
-let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with
+let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with
| TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat
| TTConstrList (typ', [], forpat) ->
- Alist1 (symbol_of_target InConstrEntry typ' assoc from forpat)
+ begin match symbol_of_target InConstrEntry typ' assoc from forpat with
+ | MayRecNo s -> MayRecNo (Alist1 s)
+ | MayRecMay s -> MayRecMay (Alist1 s) end
| TTConstrList (typ', tkl, forpat) ->
- Alist1sep (symbol_of_target InConstrEntry typ' assoc from forpat, make_sep_rules tkl)
-| TTPattern p -> Aentryl (Constr.pattern, string_of_int p)
-| TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
-| TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
-| TTName -> Aentry Prim.name
-| TTOpenBinderList -> Aentry Constr.open_binders
-| TTBigint -> Aentry Prim.bigint
-| TTReference -> Aentry Constr.global
+ begin match symbol_of_target InConstrEntry typ' assoc from forpat with
+ | MayRecNo s -> MayRecNo (Alist1sep (s, make_sep_rules tkl))
+ | MayRecMay s -> MayRecMay (Alist1sep (s, make_sep_rules tkl)) end
+| TTPattern p -> MayRecNo (Aentryl (Constr.pattern, string_of_int p))
+| TTClosedBinderList [] -> MayRecNo (Alist1 (Aentry Constr.binder))
+| TTClosedBinderList tkl -> MayRecNo (Alist1sep (Aentry Constr.binder, make_sep_rules tkl))
+| TTName -> MayRecNo (Aentry Prim.name)
+| TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders)
+| TTBigint -> MayRecNo (Aentry Prim.bigint)
+| TTReference -> MayRecNo (Aentry Constr.global)
let interp_entry forpat e = match e with
| ETProdName -> TTAny TTName
@@ -406,8 +414,8 @@ match e with
| TTConstrList _ -> { subst with constrlists = v :: subst.constrlists }
type (_, _) ty_symbol =
-| TyTerm : Tok.pattern -> ('s, string) ty_symbol
-| TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) symbol * bool -> ('s, 'a) ty_symbol
+| TyTerm : string Tok.p -> ('s, string) ty_symbol
+| TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) mayrec_symbol * bool -> ('s, 'a) ty_symbol
type ('self, _, 'r) ty_rule =
| TyStop : ('self, 'r, 'r) ty_rule
@@ -444,11 +452,23 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env ->
in
ty_eval rem f { env with constrs; constrlists; }
-let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function
-| TyStop -> Stop
+type ('s, 'a, 'r) mayrec_rule =
+| MayRecRNo : ('s, Extend.norec, 'a, 'r) Extend.rule -> ('s, 'a, 'r) mayrec_rule
+| MayRecRMay : ('s, Extend.mayrec, 'a, 'r) Extend.rule -> ('s, 'a, 'r) mayrec_rule
+
+let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function
+| TyStop -> MayRecRNo Stop
| TyMark (_, _, _, r) -> ty_erase r
-| TyNext (rem, TyTerm tok) -> Next (ty_erase rem, Atoken tok)
-| TyNext (rem, TyNonTerm (_, _, s, _)) -> Next (ty_erase rem, s)
+| TyNext (rem, TyTerm tok) ->
+ begin match ty_erase rem with
+ | MayRecRNo rem -> MayRecRMay (Next (rem, Atoken tok))
+ | MayRecRMay rem -> MayRecRMay (Next (rem, Atoken tok)) end
+| TyNext (rem, TyNonTerm (_, _, s, _)) ->
+ begin match ty_erase rem, s with
+ | MayRecRNo rem, MayRecNo s -> MayRecRMay (Next (rem, s))
+ | MayRecRNo rem, MayRecMay s -> MayRecRMay (Next (rem, s))
+ | MayRecRMay rem, MayRecNo s -> MayRecRMay (Next (rem, s))
+ | MayRecRMay rem, MayRecMay s -> MayRecRMay (Next (rem, s)) end
type ('self, 'r) any_ty_rule =
| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
@@ -485,7 +505,7 @@ let rec pure_sublevels' custom assoc from forpat level = function
let rem = pure_sublevels' custom assoc from forpat level rem in
let push where p rem =
match symbol_of_target custom p assoc from forpat with
- | Aentryl (_,i) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem
+ | MayRecNo (Aentryl (_,i)) when level <> Some (int_of_string i) -> (where,int_of_string i) :: rem
| _ -> rem in
(match e with
| ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem
@@ -507,7 +527,6 @@ let extend_constr state forpat ng =
let (entry, level) = interp_constr_entry_key custom forpat n in
let fold (accu, state) pt =
let AnyTyRule r = make_ty_rule assoc n forpat pt in
- let symbs = ty_erase r in
let pure_sublevels = pure_sublevels' custom assoc n forpat level pt in
let isforpat = target_to_bool forpat in
let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
@@ -515,7 +534,11 @@ let extend_constr state forpat ng =
let empty_rules = List.map (prepare_empty_levels forpat) needed_levels in
let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in
let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
- let rule = (name, p4assoc, [Rule (symbs, act)]) in
+ let rule =
+ let r = match ty_erase r with
+ | MayRecRNo symbs -> Rule (symbs, act)
+ | MayRecRMay symbs -> Rule (symbs, act) in
+ name, p4assoc, [r] in
let r = ExtendRule (entry, reinit, (pos, [rule])) in
(accu @ empty_rules @ [r], state)
in
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 89caff847f..bc58993a2e 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -19,17 +19,17 @@ open Vernacexpr
type 's grammar_prod_item =
| GramTerminal of string
| GramNonTerminal :
- ('a raw_abstract_argument_type * ('s, 'a) symbol) Loc.located -> 's grammar_prod_item
+ ('a raw_abstract_argument_type * ('s, _, 'a) symbol) Loc.located -> 's grammar_prod_item
type 'a ty_arg = ('a -> raw_generic_argument)
-type ('self, _, 'r) ty_rule =
-| TyStop : ('self, 'r, 'r) ty_rule
-| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) Extend.symbol * 'b ty_arg option ->
- ('self, 'b -> 'a, 'r) ty_rule
+type ('self, 'tr, _, 'r) ty_rule =
+| TyStop : ('self, Extend.norec, 'r, 'r) ty_rule
+| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Extend.symbol * 'b ty_arg option ->
+ ('self, Extend.mayrec, 'b -> 'a, 'r) ty_rule
type ('self, 'r) any_ty_rule =
-| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
+| AnyTyRule : ('self, _, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
let rec ty_rule_of_gram = function
| [] -> AnyTyRule TyStop
@@ -44,13 +44,13 @@ let rec ty_rule_of_gram = function
let r = TyNext (rem, tok, inj) in
AnyTyRule r
-let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function
+let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Extend.rule = function
| TyStop -> Extend.Stop
| TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok)
type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r
-let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function
+let rec ty_eval : type s tr a. (s, tr, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function
| TyStop -> fun f loc -> f loc []
| TyNext (rem, tok, None) -> fun f _ -> ty_eval rem f
| TyNext (rem, tok, Some inj) -> fun f x ->
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index 3689f60383..1cf75a55b1 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -18,7 +18,7 @@ open Vernacexpr
type 's grammar_prod_item =
| GramTerminal of string
| GramNonTerminal : ('a Genarg.raw_abstract_argument_type *
- ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
+ ('s, _, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
val extend_vernac_command_grammar :
extend_name -> vernac_expr Pcoq.Entry.t option ->
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 781fd404f8..b5e9e1b0d5 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -574,20 +574,20 @@ let is_not_small_constr = function
| _ -> false
let rec define_keywords_aux = function
- | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal("IDENT",Some k) :: l
+ | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(Tok.PIDENT (Some k)) :: l
when is_not_small_constr e ->
Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
CLexer.add_keyword k;
- n1 :: GramConstrTerminal(Tok.pattern_for_KEYWORD k) :: define_keywords_aux l
+ n1 :: GramConstrTerminal(Tok.PKEYWORD k) :: define_keywords_aux l
| n :: l -> n :: define_keywords_aux l
| [] -> []
(* Ensure that IDENT articulation terminal symbols are keywords *)
let define_keywords = function
- | GramConstrTerminal("IDENT", Some k)::l ->
+ | GramConstrTerminal(Tok.PIDENT (Some k))::l ->
Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
CLexer.add_keyword k;
- GramConstrTerminal(Tok.pattern_for_KEYWORD k) :: define_keywords_aux l
+ GramConstrTerminal(Tok.PKEYWORD k) :: define_keywords_aux l
| l -> define_keywords_aux l
let distribute a ll = List.map (fun l -> a @ l) ll
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 9438b9749f..d474ef8637 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -55,7 +55,7 @@ module Vernac_ =
let act_vernac v loc = Some CAst.(make ~loc v) in
let act_eoi _ loc = None in
let rule = [
- Rule (Next (Stop, Atoken Tok.pattern_for_EOI), act_eoi);
+ Rule (Next (Stop, Atoken Tok.PEOI), act_eoi);
Rule (Next (Stop, Aentry vernac_control), act_vernac);
] in
Pcoq.grammar_extend main_entry None (None, [None, None, rule])
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 4bfe5c66b5..ef06e59316 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -169,7 +169,7 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_comm
| Some Refl -> untype_command ty (f v) args
end
-let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol =
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Extend.norec, a) Extend.symbol =
let open Extend in function
| TUlist1 l -> Alist1 (untype_user_symbol l)
| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s))
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:55:48 +0000