[gramlib] Cleanup, remove unused parsing infrastructure.

We remove the functional and backtracking parsers as they are not used in Coq.
ggonthier · Oct 29, 2018 · 46ac539 · 46ac539
1 parent 6410423
commit 46ac539
Show file tree

Hide file tree

Showing 8 changed files with 15 additions and 2,105 deletions.
diff --git a/gramlib/fstream.ml b/gramlib/fstream.ml
diff --git a/gramlib/fstream.mli b/gramlib/fstream.mli
diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml
@@ -5,27 +5,17 @@
 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;
     ename : string;
     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

diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli
@@ -3,27 +3,17 @@
 (* Copyright (c) INRIA 2007-2017 *)
 
 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;
     ename : string;
     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