Source file util_zf.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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79

(* This file is free software, part of Zipperposition. See file "license" for more details. *)

(** {1 Utils for ZF} *)

open Logtk

module A = UntypedAST

type parse_cache = (string,unit) Hashtbl.t

let create_parse_cache () = Hashtbl.create 8

type parser_res = (UntypedAST.statement Iter.t, string) CCResult.t
type 'a parser_ = 'a -> parser_res

let find_file name ~dir : string option =
  Util.debugf 2 "search `%s` in `%s`" (fun k->k name dir);
  let abs_path = Filename.concat dir name in
  if Sys.file_exists abs_path
  then Some abs_path
  else None

let rec parse_lexbuf_ ?cache ?(recursive=true) ~dir lex =
  let l =
    Parse_zf.parse_statement_list Lex_zf.token lex
  in
  if recursive
  then (
    let cache = CCOpt.get_lazy create_parse_cache cache in
    CCList.flat_map
      (fun st -> match st.A.stmt with
         | A.Include s ->
           begin match find_file s ~dir with
             | None ->
               Util.errorf ~where:"utils_zf"
                 "could not find included file `%s`" s
             | Some s' when Hashtbl.mem cache s' ->
               [] (* already included *)
             | Some s' ->
               (* put in cache *)
               Hashtbl.add cache s' ();
               parse_file_ ~cache ~recursive s'
           end
         | _ ->
           [st])
      l
  )
  else l

and parse_file_ ?cache ?recursive file =
  CCIO.with_in file
    (fun ic ->
       let lexbuf = Lexing.from_channel ic in
       ParseLocation.set_file lexbuf file;
       let dir = Filename.dirname file in
       parse_lexbuf_ ?cache ?recursive ~dir lexbuf)

let parse_lexbuf ?cache ?recursive file : parser_res =
  try parse_lexbuf_ ?cache ?recursive ~dir:"." file
      |> Iter.of_list |> CCResult.return
  with e -> CCResult.of_exn e

let parse_stdin () : parser_res =
  let lexbuf = Lexing.from_channel stdin in
  ParseLocation.set_file lexbuf "stdin";
  parse_lexbuf ~recursive:false lexbuf

let parse_file ?cache ?recursive file : parser_res =
  if file="stdin"
  then parse_stdin()
  else try
      parse_file_ ?cache ?recursive file
      |> Iter.of_list
      |> CCResult.return
    with
    | Sys_error e ->
      CCResult.fail (Util.err_spf "sys_error when parsing `%s`:@ %s" file e)
    | e -> CCResult.of_exn e