Add full mode stdin parsing (#201)

* Clean up logic interface and add way to parse stdin in full mode

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

* Better fix for parsing doc

* Remove dead code

doc/parsing.md

@@ -49,7 +49,8 @@ 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 _, lazy_l = P.parse_all (`File "example.smt2")
+let statements = Lazy.force lazy_l
 ```
 
 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,15 +21,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
@@ -147,32 +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_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 ->
@@ -193,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,46 +40,48 @@ 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.
-      @param language specify a language; overrides auto-detection. *)
-
-  val parse_file_lazy :
+  val parse_all :
     ?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 ->
     [< `File of string
     | `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 triplet [(lan, gen, cl)], containing
-      the language detexted [lan], a genratro function [gen] for parsing the input,
-      and a cleanup function [cl] to call in order to cleanup the file descriptors.
+      Returns a quadruplet [(lan, file, gen, cl)], containing:
+      - the language [lan] detected
+      - a [file] value that stores the metadata about file locations
+      - a genrator function [gen] for parsing the input,
+      - a cleanup function [cl] to call in order to cleanup the file descriptors
+
       @param language specify a language for parsing, overrides auto-detection
       and stdin specification. *)
 

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

@@ -192,11 +192,20 @@ module Make(State : State.S) = struct
       st, None
 
   let parse_stdin st (file : Logic.language file) =
-    let lang, file_loc, gen, _ = Logic.parse_input
-        ?language:file.lang (`Stdin (Logic.Smtlib2 `Latest))
-    in
-    let file = { file with loc = file_loc; lang = Some lang; } in
-    st, file, gen
+    match file.mode with
+    | None
+    | Some `Incremental ->
+      let lang, file_loc, gen, _ = Logic.parse_input
+          ?language:file.lang (`Stdin (Logic.Smtlib2 `Latest))
+      in
+      let file = { file with loc = file_loc; lang = Some lang; } in
+      st, file, gen
+    | Some `Full ->
+      let lang, file_loc, l = Logic.parse_all
+          ?language:file.lang (`Stdin (Logic.Smtlib2 `Latest))
+      in
+      let file = { file with loc = file_loc; lang = Some lang; } in
+      st, file, gen_of_llist l
 
   let parse_file st source (file : Logic.language file) lang =
     (* Parse the input *)
@@ -210,8 +219,8 @@ 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 = Logic.parse_raw_lazy ~language:lang
-          ~filename contents
+        let lang, file_loc, l = Logic.parse_all
+            ~language:lang (`Raw (filename, lang, contents))
         in
         let file = { file with loc = file_loc; lang = Some lang; } in
         st, file, gen_of_llist l
@@ -332,8 +341,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
@@ -354,7 +364,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
@@ -401,7 +411,7 @@ module Make(State : State.S) = struct
                 let st = set_logic_file st new_logic_file in
                 st, `Gen (merge, wrap_parser ~file:new_logic_file (gen_finally gen cl))
               | Some `Full ->
-                let lang, file_loc, l = Logic.parse_file_lazy ?language file in
+                let lang, file_loc, l = Logic.parse_all ?language (`File file) in
                 let new_logic_file = { logic_file with loc = file_loc; lang = Some lang; } in
                 let st = set_logic_file st new_logic_file in
                 st, `Gen (merge, wrap_parser ~file:new_logic_file (gen_of_llist l))