Source file phases.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
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
(** {1 Phases of the Prover} *)
open Logtk
open Libzipperposition
module E = CCResult
type filename = string
type 'a or_error = ('a, string) CCResult.t
(** {2 Phases} *)
type env_with_clauses =
Env_clauses : 'c Env.packed * 'c Clause.sets -> env_with_clauses
type env_with_result =
Env_result : 'c Env.packed * Saturate.szs_status -> env_with_result
type errcode = int
type prelude = UntypedAST.statement Iter.t
type ('ret, 'before, 'after) phase =
| Init : (unit, _, [`Init]) phase
| Setup_gc : (unit, [`Init], [`Init]) phase
| Setup_signal : (unit, [`Init], [`Init]) phase
| Parse_CLI :
(filename list * Params.t, [`Init], [`Parse_cli]) phase
| LoadExtensions : (Extensions.t list, [`Parse_cli], [`LoadExtensions]) phase
| Parse_prelude : (prelude, [`LoadExtensions], [`Parse_prelude]) phase
| Start_file :
(filename, [`Parse_prelude], [`Start_file]) phase
| Parse_file :
(Input_format.t * UntypedAST.statement Iter.t,
[`Start_file], [`Parse_file]) phase
| Typing :
(TypeInference.typed_statement CCVector.ro_vector, [`Parse_file], [`Typing]) phase
| CNF :
(Statement.clause_t CCVector.ro_vector, [`Typing], [`CNF]) phase
| Compute_prec :
(Precedence.t, [`CNF], [`Precedence]) phase
| Compute_ord_select :
(Ordering.t * Selection.t * Bool_selection.t, [`Precedence], [`Compute_ord_select]) phase
| MakeCtx : ((module Ctx.S), [`Compute_ord_select], [`MakeCtx]) phase
| MakeEnv : (env_with_clauses, [`MakeCtx], [`MakeEnv]) phase
| Pre_saturate :
('c Env.packed * Saturate.szs_status * 'c Clause.sets,
[`MakeEnv], [`Pre_saturate]) phase
| Saturate :
(env_with_result, [`Pre_saturate], [`Saturate]) phase
| Print_result : (unit, [`Saturate], [`Print_result]) phase
| Print_dot : (unit, [`Print_result], [`Print_dot]) phase
| Check_proof : (errcode, [`Print_dot], [`Check_proof]) phase
| Print_stats : (unit, [`Check_proof], [`Print_stats]) phase
| Exit : (unit, _, [`Exit]) phase
type any_phase = Any_phase : (_, _, _) phase -> any_phase
(** A phase hidden in an existential type *)
module State = Flex_state
module Key = struct
let cur_phase = State.create_key()
end
let empty_state = State.empty |> State.add Key.cur_phase (Any_phase Init)
type (+'a, 'p1, 'p2) t = State.t -> (State.t * 'a) or_error
let string_of_phase : type a b c. (a,b,c) phase -> string
= function
| Init -> "init"
| Setup_gc -> "setup_gc"
| Setup_signal -> "setup_signal"
| Parse_CLI -> "parse_cli"
| LoadExtensions -> "load_extensions"
| Parse_prelude -> "parse_prelude"
| Start_file -> "start_file"
| Parse_file -> "parse_file"
| Typing -> "typing"
| CNF -> "cnf"
| Compute_prec -> "compute_prec"
| Compute_ord_select -> "compute_ord_select"
| MakeCtx -> "make_ctx"
| MakeEnv -> "make_env"
| Pre_saturate -> "pre_saturate"
| Saturate -> "saturate"
| Print_result -> "print_result"
| Print_stats -> "print_stats"
| Print_dot -> "print_dot"
| Check_proof -> "check_proof"
| Exit -> "exit"
let string_of_any_phase (Any_phase p) = string_of_phase p
let return x st = E.return (st, x)
let return_err x st = match x with
| E.Ok x -> E.Ok (st, x)
| E.Error msg -> E.Error msg
let fail msg _ = E.Error msg
let bind x ~f st =
match x st with
| E.Ok (st, x) -> f x st
| E.Error msg -> E.Error msg
let bind_err e ~f st =
match e with
| E.Ok x -> f x st
| E.Error msg -> fail msg st
let map x ~f st = match x st with
| E.Error msg -> E.Error msg
| E.Ok (st, x) -> E.Ok (st, f x)
module Infix = struct
let (>>=) x f = bind x ~f
let (>>?=) x f = bind_err x ~f
let (>|=) x f = map x ~f
end
include Infix
let rec fold_l ~f ~x = function
| [] -> return x
| y :: ys -> f x y >>= fun x' -> fold_l ~f ~x:x' ys
let current_phase st =
try E.Ok (st, State.get_exn Key.cur_phase st)
with Not_found ->
let msg = "could not find current phase" in
E.Error msg
let start_phase p st =
Util.debugf ~section:Const.section 2 "@{<yellow>start phase@} %s" (fun k->k (string_of_phase p));
let st = State.add Key.cur_phase (Any_phase p) st in
E.Ok (st, ())
let return_phase_err x =
current_phase >>= fun p ->
Util.debugf ~section:Const.section 2 "@{<yellow>terminate phase@} %s"
(fun k->k (string_of_any_phase p));
return_err x
let return_phase x = return_phase_err (E.Ok x)
let with_phase1 p ~f x =
start_phase p >>= fun () ->
let y = f x in
return_phase y
let with_phase p ~f = with_phase1 p ~f ()
let with_phase2 p ~f x y = with_phase1 p ~f:(f x) y
let exit =
start_phase Exit >>= fun () ->
return_phase ()
let get st = E.Ok (st, st)
let get_key k st =
match Flex_state.get k st with
| None -> E.Error "key not found"
| Some v -> E.Ok (st, v)
let set new_st _st = E.Ok (new_st, ())
let set_key k v st =
let st = Flex_state.add k v st in
E.Ok (st, ())
let run_parallel l =
let rec aux = function
| [] -> return 0
| [a] -> a
| a :: tail ->
get >>= fun old_st ->
a >>= fun n ->
if n<>0 then return n
else (
set old_st >>= fun () ->
aux tail
)
in
aux l
let update ~f st =
let st = f st in
E.Ok (st, ())
let run_with st m =
try
m st
with e ->
let stack = Printexc.get_backtrace () in
let msg = Printexc.to_string e in
E.Error (msg ^ "\n" ^ stack)
let run m = run_with State.empty m