module Phases_impl:sig
..end
See Phases
for the list of steps to execute
val parse_cli : (Phases.filename list * Params.t, [ `Init ], [ `Parse_cli ]) Phases.t
val load_extensions : (Extensions.t list, [ `Parse_cli ], [ `LoadExtensions ]) Phases.t
val setup_gc : (unit, [ `Init ], [ `Init ]) Phases.t
val setup_signal : (unit, [ `Init ], [ `Init ]) Phases.t
val process_file : Phases.prelude ->
Phases.filename ->
(Phases.env_with_result, [ `Parse_prelude ], [ `Saturate ]) Phases.t
process_file f
parses f
, does the preprocessing phases, including
type inference, choice of precedence, ordering, etc. , saturates
the set of clauses, and return the resultval print : Phases.filename ->
'c Env.packed ->
Saturate.szs_status -> (unit, [ `Saturate ], [ `Print_dot ]) Phases.t
val check : Saturate.szs_status ->
(Phases.errcode, [ `Print_dot ], [ `Check_proof ]) Phases.t
val process_files_and_print : Params.t ->
Phases.filename list ->
(Phases.errcode, [ `LoadExtensions ], [ `Check_proof ]) Phases.t