Real stdin parsing instead of reading it into a string to parse

Author: Gbury

doc/parsing.md

@@ -49,7 +49,7 @@ module P =
     (Dolmen.Std.Loc)(Dolmen.Std.Id)(Dolmen.Std.Term)(Dolmen.Std.Statement)
     (Dolmen.Std.Extensions.Smtlib2)
 
-let _ = P.parse_file "example.smt2"
+let _ = P.parse_all (`File "example.smt2")
 ```
 
 For more examples, see the [tutorial](https://github.com/Gbury/dolmen/tree/master/doc/tuto.md).

doc/tuto.md

@@ -31,8 +31,12 @@ let test file =
   (* Parse the file, and we get a tuple:
     - format: the guessed format (according to the file extension)
     - loc: some meta-data used for source file locations
-    - statements: the list of top-level directives found in the file *)
-  let format, loc, parsed_statements = Logic.parse_file file in
+    - statements: a lazy list of top-level directives found in the file *)
+  let format, loc, parsed_statements_lazy = Logic.parse_all (`File file) in
+
+  (* Any lexing/parsing error will be raised when forcing the lazy list
+     of statements *)
+  let parsed_statements = Lazy.force parsed_statements_lazy in
 
   (* You can match on the detected format of the input *)
   let () =

src/classes/logic.ml

@@ -21,9 +21,6 @@ module type S = sig
   val find :
     ?language:language ->
     ?dir:string -> string -> string option
-  val parse_file :
-    ?language:language ->
-    string -> language * file * statement list
   val parse_all :
     ?language:language ->
     [< `File of string | `Stdin of language
@@ -146,45 +143,31 @@ module Make
       let _, _, (module P : S) = of_language l in
       P.find ~dir file
 
-  let parse_file ?language file =
-    let l, _, (module P : S) =
-      match language with
-      | None -> of_filename file
-      | Some l -> of_language l
-    in
-    let locfile, res = P.parse_file file in
-    l, locfile, res
-
-  let parse_raw_lazy ?language ~filename contents =
-    let l, _, (module P : S) =
-      match language with
-      | None -> of_filename filename
-      | Some l -> of_language l
-    in
-    let locfile, res = P.parse_raw_lazy ~filename contents in
-    l, locfile, res
-
   let parse_all ?language = function
     | `File file ->
       let l, _, (module P : S) =
         match language with
         | None -> of_filename file
         | Some l -> of_language l
       in
-      let locfile, res = P.parse_file_lazy file in
+      let locfile, res = P.parse_all (`File file) in
       l, locfile, res
     | `Raw (filename, l, s) ->
-      let language =
-        match language with Some _ -> language | None -> Some l
+      let l, _, (module P : S) =
+        match language with
+        | None -> of_language l
+        | Some lang -> of_language lang
       in
-      parse_raw_lazy ?language ~filename s
+      let locfile, res = P.parse_all (`Contents (filename, s)) in
+      l, locfile, res
     | `Stdin l ->
-      let filename = "<stdin>" in
-      let s = Dolmen_std.Misc.read_all ~size:1024 stdin in
-      let language =
-        match language with Some _ -> language | None -> Some l
+      let l, _, (module P : S) =
+        match language with
+        | None -> of_language l
+        | Some lang -> of_language lang
       in
-      parse_raw_lazy ?language ~filename s
+      let locfile, res = P.parse_all `Stdin in
+      l, locfile, res
 
   let parse_input ?language = function
     | `File file ->
@@ -205,4 +188,5 @@ module Make
           (match language with | Some l' -> l' | None -> l) in
       let locfile, gen, cl = P.parse_input (`Contents (filename, s)) in
       l, locfile, gen, cl
+
 end

src/classes/logic.mli

@@ -14,6 +14,7 @@ module type S = sig
   exception Extension_not_found of string
   (** Raised when trying to find a language given a file extension. *)
 
+
   (** {2 Supported languages} *)
 
   type language =
@@ -39,28 +40,14 @@ module type S = sig
   val string_of_language : language -> string
   (** String representation of the variant *)
 
+
   (** {2 High-level parsing} *)
 
   val find :
     ?language:language ->
     ?dir:string -> string -> string option
   (** Tries and find the given file, using the language specification. *)
 
-  val parse_file :
-    ?language:language ->
-    string -> language * file * statement list
-  (** Given a filename, parse the file, and return the detected language
-      together with the list of statements parsed.
-
-      WARNING: please note that this function makes it difficult to report
-               error locations, since exceptions might be raised during parsing
-               and any caller of this function will not have access to the [file]
-               return value of the function, which is necessary to correctly
-               interpret the locations in error exceptions. Instead, please use
-               either {parse_all} or {parse_input}.
-
-      @param language specify a language; overrides auto-detection. *)
-
   val parse_all :
     ?language:language ->
     [< `File of string
@@ -86,7 +73,7 @@ module type S = sig
     | `Stdin of language
     | `Raw of string * language * string ] ->
     language * file * (unit -> statement option) * (unit -> unit)
-  (** Incremental parsing of either a file (see {!parse_file}), stdin
+  (** Incremental parsing of either a file, stdin
       (with given language), or some arbitrary contents, of the form
       [`Raw (filename, language, contents)].
       Returns a quadruplet [(lan, file, gen, cl)], containing:

src/classes/response.ml

@@ -16,15 +16,11 @@ module type S = sig
   val find :
     ?language:language ->
     ?dir:string -> string -> string option
-  val parse_file :
+  val parse_all :
     ?language:language ->
-    string -> language * file * statement list
-  val parse_file_lazy :
-    ?language:language ->
-    string -> language * file * statement list Lazy.t
-  val parse_raw_lazy :
-    ?language:language ->
-    filename:string -> string -> language * file * statement list Lazy.t
+    [< `File of string | `Stdin of language
+    | `Raw of string * language * string ] ->
+    language * file * statement list Lazy.t
   val parse_input :
     ?language:language ->
     [< `File of string | `Stdin of language
@@ -104,32 +100,31 @@ module Make
       let _, _, (module P : S) = of_language l in
       P.find ~dir file
 
-  let parse_file ?language file =
-    let l, _, (module P : S) =
-      match language with
-      | None -> of_filename file
-      | Some l -> of_language l
-    in
-    let locfile, res = P.parse_file file in
-    l, locfile, res
-
-  let parse_file_lazy ?language file =
-    let l, _, (module P : S) =
-      match language with
-      | None -> of_filename file
-      | Some l -> of_language l
-    in
-    let locfile, res = P.parse_file_lazy file in
-    l, locfile, res
-
-  let parse_raw_lazy ?language ~filename contents =
-    let l, _, (module P : S) =
-      match language with
-      | None -> of_filename filename
-      | Some l -> of_language l
-    in
-    let locfile, res = P.parse_raw_lazy ~filename contents in
-    l, locfile, res
+  let parse_all ?language = function
+    | `File file ->
+      let l, _, (module P : S) =
+        match language with
+        | None -> of_filename file
+        | Some l -> of_language l
+      in
+      let locfile, res = P.parse_all (`File file) in
+      l, locfile, res
+    | `Raw (filename, l, s) ->
+      let l, _, (module P : S) =
+        match language with
+        | None -> of_language l
+        | Some lang -> of_language lang
+      in
+      let locfile, res = P.parse_all (`Contents (filename, s)) in
+      l, locfile, res
+    | `Stdin l ->
+      let l, _, (module P : S) =
+        match language with
+        | None -> of_language l
+        | Some lang -> of_language lang
+      in
+      let locfile, res = P.parse_all `Stdin in
+      l, locfile, res
 
   let parse_input ?language = function
     | `File file ->

src/classes/response.mli

@@ -36,26 +36,23 @@ module type S = sig
     ?dir:string -> string -> string option
   (** Tries and find the given file, using the language specification. *)
 
-  val parse_file :
+  val parse_all :
     ?language:language ->
-    string -> language * file * statement list
-  (** Given a filename, parse the file, and return the detected language
-      together with the list of statements parsed.
-      @param language specify a language; overrides auto-detection. *)
-
-  val parse_file_lazy :
-    ?language:language ->
-    string -> language * file * statement list Lazy.t
-  (** Given a filename, parse the file, and return the detected language
-      together with the list of statements parsed.
-      @param language specify a language; overrides auto-detection. *)
+    [< `File of string | `Stdin of language
+    | `Raw of string * language * string ] ->
+    language * file * statement list Lazy.t
+  (** Full (but lazy) parsing of either a file (see {!parse_file}), stdin
+      (with given language), or some arbitrary contents, of the form
+      [`Raw (filename, language, contents)].
+      Returns a triplet [(lan, file, stmts)], containing:
+      - the language [lan] detected
+      - a [file] value that stores the metadata about file locations
+      - a lazy list of statements [stmts]; forcing this list will run the actual
+        parsing of the whole input given as argument, and may raise errors, if
+        any arises during the parsing (such as lexical errors, etc..)
 
-  val parse_raw_lazy :
-    ?language:language ->
-    filename:string -> string -> language * file * statement list Lazy.t
-  (** Given a filename and a string, parse the string, and return the detected
-      language together with the list of statements parsed.
-      @param language specify a language; overrides auto-detection. *)
+      @param language specify a language for parsing, overrides auto-detection
+      and stdin specification. *)
 
   val parse_input :
     ?language:language ->

src/interface/language.ml

@@ -28,14 +28,13 @@ module type S = sig
       Separates directory and file because most include directives in languages
       are relative to the directory of the original file being processed. *)
 
-  val parse_file : string -> file * statement list
-  (** Parse the whole given file into a list. *)
-
-  val parse_file_lazy : string -> file * statement list Lazy.t
-  (** Parse the whole given file into a list. *)
-
-  val parse_raw_lazy : filename:string -> string -> file * statement list Lazy.t
-  (** Parse the whole given string into a list. *)
+  val parse_all :
+    [ `Stdin | `File of string | `Contents of string * string ] ->
+    file * statement list Lazy.t
+  (** Whole input parsing. Given an input to read (either a file, stdin,
+      or some contents of the form [(filename, s)] where [s] is the contents to parse),
+      returns a lazy list of the parsed statements. Forcing the lazy list may raise
+      an exception if some error occurs during parsing (e.g. lexing or parsing error). *)
 
   val parse_input :
     [ `Stdin | `File of string | `Contents of string * string ] ->

src/loop/parser.ml

@@ -342,8 +342,9 @@ module Make(State : State.S) = struct
             let file = { file with loc = file_loc; lang = Some lang; } in
             st, file, gen_finally gen cl
           | Some `Full ->
-            let lang, file_loc, l = Response.parse_raw_lazy ?language:file.lang
-              ~filename contents
+            let lang, file_loc, l =
+              Response.parse_all ?language:file.lang
+              (`Raw (filename, Response.Smtlib2 `Latest, contents))
             in
             let file = { file with loc = file_loc; lang = Some lang; } in
             st, file, gen_of_llist l
@@ -364,7 +365,7 @@ module Make(State : State.S) = struct
                   st, file, gen_finally gen cl
                 | Some `Full ->
                   let lang, file_loc, l =
-                    Response.parse_file_lazy ?language:file.lang filename
+                    Response.parse_all ?language:file.lang (`File filename)
                   in
                   let file = { file with loc = file_loc; lang = Some lang; } in
                   st, file, gen_of_llist l

src/standard/transformer.ml

@@ -130,36 +130,9 @@ module Make
   (* Instantiations of the parsing loop
      ---------------------------------- *)
 
-  let parse_file file =
-    let lexbuf, cleanup = Misc.mk_lexbuf (`File file) in
-    let locfile = Loc.mk_file file in
-    let newline = Loc.newline locfile in
-    let sync = Loc.update_size locfile in
-    let k_exn () = cleanup () in
-    let res = parse_aux ~k_exn newline sync lexbuf Parser.file () in
-    let () = cleanup () in
-    locfile, res
-
-  let parse_file_lazy file =
-    let lexbuf, cleanup = Misc.mk_lexbuf (`File file) in
-    let locfile = Loc.mk_file file in
-    let newline = Loc.newline locfile in
-    let sync = Loc.update_size locfile in
-    let k_exn () = cleanup () in
-    let res =
-      lazy (
-        let res =
-          parse_aux ~k_exn newline sync lexbuf Parser.file ()
-        in
-        let () = cleanup () in
-        res
-      )
-    in
-    locfile, res
-
-  let parse_raw_lazy ~filename contents =
-    let lexbuf, cleanup = Misc.mk_lexbuf (`Contents (filename, contents)) in
-    let locfile = Loc.mk_file filename in
+  let parse_all i =
+    let lexbuf, cleanup = Misc.mk_lexbuf i in
+    let locfile = Loc.mk_file (Misc.filename_of_input i) in
     let newline = Loc.newline locfile in
     let sync = Loc.update_size locfile in
     let k_exn () = cleanup () in