diff options
| author | Emilio Jesus Gallego Arias | 2018-10-07 07:50:16 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-29 01:25:34 +0100 |
| commit | 46ac5393bf8d3dfef069c4190e3bfe6a3b4dcd90 (patch) | |
| tree | 4a7e7e27a48b542fb28992002acd807117df043c /gramlib/gramext.ml | |
| parent | 641042302f05f6ec42f61a4bdb73fad70bb90c41 (diff) | |
[gramlib] Cleanup, remove unused parsing infrastructure.
We remove the functional and backtracking parsers as they are not used
in Coq.
Diffstat (limited to 'gramlib/gramext.ml')
| -rw-r--r-- | gramlib/gramext.ml | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml index 39da1de56d..8960d4f257 100644 --- a/gramlib/gramext.ml +++ b/gramlib/gramext.ml @@ -5,16 +5,10 @@ open Printf type 'a parser_t = 'a Stream.t -> Obj.t -type 'a fparser_t = 'a Fstream.t -> (Obj.t * 'a Fstream.t) option -type 'a bparser_t = ('a, Obj.t) Fstream.bp - -type parse_algorithm = - Predictive | Functional | Backtracking | DefaultAlgorithm type 'te grammar = { gtokens : (Plexing.pattern, int ref) Hashtbl.t; - mutable glexer : 'te Plexing.lexer; - mutable galgo : parse_algorithm } + mutable glexer : 'te Plexing.lexer } type 'te g_entry = { egram : 'te grammar; @@ -22,10 +16,6 @@ type 'te g_entry = elocal : bool; mutable estart : int -> 'te parser_t; mutable econtinue : int -> int -> Obj.t -> 'te parser_t; - mutable fstart : int -> err_fun -> 'te fparser_t; - mutable fcontinue : int -> int -> Obj.t -> err_fun -> 'te fparser_t; - mutable bstart : int -> err_fun -> 'te bparser_t; - mutable bcontinue : int -> int -> Obj.t -> err_fun -> 'te bparser_t; mutable edesc : 'te g_desc } and 'te g_desc = Dlevels of 'te g_level list |