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

Author: Gbury

src/classes/logic.ml

@@ -24,12 +24,11 @@ module type S = sig
   val parse_file :
     ?language:language ->
     string -> language * file * statement list
-  val parse_file_lazy :
+  val parse_all :
     ?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
@@ -156,15 +155,6 @@ module Make
     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
@@ -174,6 +164,28 @@ module Make
     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
+      l, locfile, res
+    | `Raw (filename, l, s) ->
+      let language =
+        match language with Some _ -> language | None -> Some l
+      in
+      parse_raw_lazy ?language ~filename s
+    | `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
+      in
+      parse_raw_lazy ?language ~filename s
+
   let parse_input ?language = function
     | `File file ->
       let l, _, (module P : S) =

src/classes/logic.mli

@@ -51,21 +51,34 @@ module type S = sig
     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.
+      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_raw_lazy :
+  val parse_all :
     ?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. *)
+    [< `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..)
+
+      @param language specify a language for parsing, overrides auto-detection
+      and stdin specification. *)
 
   val parse_input :
     ?language:language ->
@@ -76,9 +89,12 @@ module type S = sig
   (** Incremental 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, 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/loop/parser.ml

@@ -193,11 +193,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 *)
@@ -211,8 +220,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
@@ -402,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))

src/standard/misc.ml

@@ -234,3 +234,25 @@ let mk_lexbuf i =
     set_file buf filename;
     buf, cl
 
+(* Read everything from stdin *)
+(* ************************************************************************* *)
+(* Implementations mostly taken from containers, see
+   https://github.com/c-cube/ocaml-containers/blob/master/src/core/CCIO.ml *)
+
+let read_all ~size ic =
+  let buf = ref (Bytes.create size) in
+  let len = ref 0 in
+  try
+    while true do
+      (* resize *)
+      if !len = Bytes.length !buf then buf := Bytes.extend !buf 0 !len;
+      assert (Bytes.length !buf > !len);
+      let n = input ic !buf !len (Bytes.length !buf - !len) in
+      len := !len + n;
+      if n = 0 then raise Exit
+      (* exhausted *)
+    done;
+    assert false (* never reached*)
+  with Exit ->
+    Bytes.sub_string !buf 0 !len
+

src/standard/misc.mli

@@ -97,3 +97,8 @@ val mk_lexbuf :
     contents to be parsed. *)
 
 
+(** {2 In_channel helpers} *)
+
+val read_all : size:int -> in_channel -> string
+(** Read all the contents of an in_channel into a string. *)
+

tests/qcheck/maps.ml

@@ -5,7 +5,7 @@ module M = Map.Make(String)
 module T = Dolmen_std.Maps.String
 
 let add_find =
-  QCheck2.Test.make ~count:1_000 ~long_factor:100
+  QCheck2.Test.make ~count:500 ~long_factor:100
     ~name:"Maps.add_find"
     QCheck2.Gen.(list (pair string int))
     (fun l ->

tests/qcheck/print.ml

@@ -17,7 +17,7 @@ module L = Dolmen.Class.Logic.Make
 let identifier
     ~print ~template ~name ~is_print_exn ~language ~gen =
   QCheck2.Test.make
-    ~count:1_000 ~long_factor:1_000
+    ~count:50 ~max_gen:500 ~long_factor:100
     ~print:(fun name -> Format.asprintf template print name)
     ~name gen
     (fun name ->
@@ -26,7 +26,7 @@ let identifier
          with exn when is_print_exn exn ->
            QCheck2.assume_fail ()
        in
-       let _, _, l = L.parse_raw_lazy ~language ~filename:"test" test in
+       let _, _, l = L.parse_all ~language (`Raw ("test", language, test)) in
        try
          let _ = Lazy.force l in
          true