Source file `Smtlib_utils.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
(* This file is free software, copyright Simon Cruanes. See file "LICENSE" for more details. *)

(** {1 SMTLIB parser} *)

module V_2_6 = struct
  module Ast = Ast
  module Loc = Loc
  module Parser = Parser
  module Lexer = Lexer

  let with_in_ file f =
    let ic = open_in file in
    try
      let x = f ic in
      close_in ic;
      x
    with e ->
      close_in_noerr ic;
      raise e

  let parse_list_exn lexbuf =
    try
      Parser.parse_list Lexer.token lexbuf
    with
    | Parsing.Parse_error ->
      raise (Ast.Parse_error (Some (Loc.of_lexbuf lexbuf), "syntax error"))

  let parse_list lexbuf =
    try Ok (parse_list_exn lexbuf)
    with e -> Result.Error (Printexc.to_string e)

  let parse_chan_exn ?(filename="<no name>") ic =
    let lexbuf = Lexing.from_channel ic in
    Loc.set_file lexbuf filename;
    parse_list_exn lexbuf

  let parse_chan ?filename ic =
    try Result.Ok (parse_chan_exn ?filename ic)
    with e -> Result.Error (Printexc.to_string e)

  let parse_file_exn file : Ast.statement list =
    with_in_ file (parse_chan_exn ~filename:file)

  let parse_file file =
    try Result.Ok (parse_file_exn file)
    with e -> Result.Error (Printexc.to_string e)

  let parse_string_exn s =
    let lexbuf = Lexing.from_string s in
    Loc.set_file lexbuf "<memory>";
    parse_list_exn lexbuf

  let parse_string s =
    try Result.Ok (parse_string_exn s)
    with e -> Result.Error (Printexc.to_string e)
end