Relying on the abstract notion of streams with location for parsing.

We also get rid of ploc.ml, now useless, relying a priori on more
robust code in lStream.ml for location reporting (see
e.g. parse_parsable in grammar.ml).

1 files changed, 13 insertions, 30 deletions

diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index d8d2f2a2ef..bb1797ee02 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -11,7 +11,6 @@
 open Pp
 open Util
 open Tok
-open Gramlib
 
 (* Dictionaries: trees annotated with string options, each node being a map
    from chars to dictionaries (the subtrees). A trie, in other words. *)
@@ -115,7 +114,7 @@ let bad_token str = raise (Error.E (Bad_token str))
 
 (* Update a loc without allocating an intermediate pair *)
 let set_loc_pos loc bp ep =
-  Ploc.sub loc (bp - loc.Loc.bp) (ep - bp)
+  Loc.sub loc (bp - loc.Loc.bp) (ep - bp)
 
 (* Increase line number by 1 and update position of beginning of line *)
 let bump_loc_line loc bol_pos =
@@ -216,7 +215,9 @@ let lookup_utf8 loc cs =
     | Some ('\x80'..'\xFF' as c) -> lookup_utf8_tail loc c cs
     | None -> EmptyStream
 
-let unlocated f x = f x
+let unlocated f x =
+  let dummy_loc = Loc.(initial ToplevelInput) in
+  f dummy_loc x
   (** FIXME: should we still unloc the exception? *)
 (*   try f x with Loc.Exc_located (_, exc) -> raise exc *)
 
@@ -226,7 +227,7 @@ let check_keyword str =
         Stream.junk s;
         bad_token str
     | _ ->
-        match unlocated lookup_utf8 Ploc.dummy s with
+        match unlocated lookup_utf8 s with
         | Utf8Token (_,n) -> njunk n s; loop_symb s
         | AsciiChar -> Stream.junk s; loop_symb s
         | EmptyStream -> ()
@@ -242,7 +243,7 @@ let check_ident str =
         Stream.junk s;
         loop_id true s
     | _ ->
-        match unlocated lookup_utf8 Ploc.dummy s with
+        match unlocated lookup_utf8 s with
         | Utf8Token (st, n) when not intail && Unicode.is_valid_ident_initial st -> njunk n s; loop_id true s
         | Utf8Token (st, n) when intail && Unicode.is_valid_ident_trailing st ->
           njunk n s;
@@ -793,20 +794,6 @@ let next_token ~diff_mode loc s =
   Printf.eprintf "(line %i, %i-%i)[%s]\n%!" (Ploc.line_nb loc) (Ploc.first_pos loc) (Ploc.last_pos loc) (Tok.to_string t);
   r *)
 
-(* Location table system for creating tables associating a token count
-   to its location in a char stream (the source) *)
-
-let locerr i =
-  let m = "Lexer: location function called on token "^string_of_int i in
-  invalid_arg m
-
-let loct_create () = Hashtbl.create 207
-
-let loct_func loct i =
-  try Hashtbl.find loct i with Not_found -> locerr i
-
-let loct_add loct i loc = Hashtbl.add loct i loc
-
 (** {6 The lexer of Coq} *)
 
 (** Note: removing a token.
@@ -837,17 +824,13 @@ let token_text : type c. c Tok.p -> string = function
   | PBULLET (Some s) -> "BULLET \"" ^ s ^ "\""
   | PQUOTATION lbl -> "QUOTATION \"" ^ lbl ^ "\""
 
-let func next_token ?loc cs =
-  let loct = loct_create () in
-  let cur_loc = ref (Option.default Loc.(initial ToplevelInput) loc) in
-  let ts =
-    Stream.from
-      (fun i ->
-         let (tok, loc) = next_token !cur_loc cs in
-         cur_loc := after loc;
-         loct_add loct i loc; Some tok)
-  in
-  (ts, loct_func loct)
+let func next_token ?(source=Loc.ToplevelInput) cs =
+  let cur_loc = ref (Loc.initial source) in
+  LStream.from ~source
+    (fun i ->
+      let (tok, loc) = next_token !cur_loc cs in
+      cur_loc := after loc;
+      Some (tok,loc))
 
 module MakeLexer (Diff : sig val mode : bool end) = struct
   type te = Tok.t