Source file state.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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184

(* This file is free software, part of dolmen. See file "LICENSE" for more information *)

(* Type definition & Exceptions *)
(* ************************************************************************* *)

type perm =
  | Allow
  | Warn
  | Error

exception File_not_found of Dolmen.Std.Loc.full * string * string

exception Input_lang_changed of Logic.language * Logic.language

(* Type definition *)
(* ************************************************************************* *)

type lang = Logic.language
type ty_state = Typer.ty_state
type solve_state = unit

type 'solve state = {

  (* Debug option *)
  debug             : bool;

  (* Warning/Error options *)
  context           : bool;
  max_warn          : int;
  cur_warn          : int;

  (* Limits for time and size *)
  time_limit        : float;
  size_limit        : float;

  (* Input settings *)
  input_dir         : string;
  input_lang        : lang option;
  input_mode        : [ `Full
                      | `Incremental ] option;
  input_source      : [ `Stdin
                      | `File of string
                      | `Raw of string * string ];

  input_file_loc    : Dolmen.Std.Loc.file;

  (* Header check *)
  header_check      : bool;
  header_state      : Headers.t;
  header_licenses   : string list;
  header_lang_version : string option;

  (* Typechecking state *)
  type_state        : ty_state;
  type_check        : bool;
  type_strict       : bool;

  (* Solving state *)
  solve_state       : 'solve;

  (* Output settings *)
  export_lang       : (lang * Format.formatter) list;

}

type t = solve_state state

(* State and locations *)
(* ************************************************************************* *)

let pp_loc fmt o =
  match o with
  | None -> ()
  | Some loc ->
    if Dolmen.Std.Loc.is_dummy loc then ()
    else Format.fprintf fmt "%a:@ " Dolmen.Std.Loc.fmt loc

let error ?(code=Code.bug) ?loc _ format =
  let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in
  Format.kfprintf (fun _ -> Code.exit code) Format.err_formatter
    ("@[<v>%a%a @[<hov>" ^^ format ^^ "@]@]@.")
    Fmt.(styled `Bold @@ styled (`Fg (`Hi `White)) pp_loc) loc
    Fmt.(styled `Bold @@ styled (`Fg (`Hi `Red)) string) "Error"

let warn ?loc st format =
  let loc = Dolmen.Std.Misc.opt_map loc Dolmen.Std.Loc.full_loc in
  let aux _ = { st with cur_warn = st.cur_warn + 1; } in
  if st.cur_warn >= st.max_warn then
    Format.ikfprintf aux Format.err_formatter format
  else
    Format.kfprintf aux Format.err_formatter
      ("@[<v>%a%a @[<hov>" ^^ format ^^ "@]@]@.")
      Fmt.(styled `Bold @@ styled (`Fg (`Hi `White)) pp_loc) loc
      Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning"

let flush st () =
  let aux _ = { st with cur_warn = 0; } in
  if st.cur_warn <= st.max_warn then
    aux ()
  else
    Format.kfprintf aux Format.err_formatter
      ("@[<v>%a @[<hov>%s@ %d@ %swarnings@]@]@.")
      Fmt.(styled `Bold @@ styled (`Fg (`Hi `Magenta)) string) "Warning"
      (if st.max_warn = 0 then "Counted" else "Plus")
      (st.cur_warn - st.max_warn)
      (if st.max_warn = 0 then "" else "additional ")

(* Getting/Setting options *)
(* ************************************************************************* *)

let time_limit t = t.time_limit
let size_limit t = t.size_limit

let input_dir t = t.input_dir
let input_mode t = t.input_mode
let input_lang t = t.input_lang
let input_source t = t.input_source

let input_file_loc st = st.input_file_loc
let set_input_file_loc st f = { st with input_file_loc = f; }

let set_mode t m = { t with input_mode = Some m; }

let header_state { header_state; _ } = header_state
let set_header_state st header_state = { st with header_state; }

let check_headers { header_check; _ } = header_check
let allowed_licenses { header_licenses; _ } = header_licenses
let allowed_lang_version { header_lang_version; _ } = header_lang_version

let ty_state { type_state; _ } = type_state
let set_ty_state st type_state = { st with type_state; }

let typecheck st = st.type_check
let strict_typing { type_strict; _ } = type_strict

let is_interactive = function
  | { input_source = `Stdin; _ } -> true
  | _ -> false

let prelude st =
  match st.input_lang with
  | None -> "prompt> @?"
  | Some l ->
    Format.asprintf "(%s)# @?" (Logic.string_of_language l)

(* Setting language *)
(* ************************************************************************* *)

let switch_to_full_mode lang t =
  let old_mode = input_mode t in
  let t = set_mode t `Full in
  match old_mode with
  | Some `Incremental ->
    warn t
      "The@ %s@ format@ does@ not@ support@ \
       incremental@ mode,@ switching@ to@ full@ mode"
      lang
  | _ -> t

let set_lang_aux t l =
  let t = { t with input_lang = Some l; } in
  match l with
  | Logic.Alt_ergo -> switch_to_full_mode "Alt-Ergo" t
  | _ -> t

let set_lang t l =
  match t.input_lang with
  | None -> set_lang_aux t l
  | Some l' ->
    if l = l'
    then set_lang_aux t l
    else raise (Input_lang_changed (l', l))

(* Full state *)
(* ************************************************************************* *)

let start _ = ()
let stop _ = ()

let file_not_found ~loc ~dir ~file =
  raise (File_not_found (loc, dir, file))