sig
  type filename = string
  type 'a or_error = ('a, string) CCResult.t
  type env_with_clauses =
      Env_clauses : 'c Env.packed * 'c Clause.sets -> Phases.env_with_clauses
  type env_with_result =
      Env_result : 'c Env.packed *
        Saturate.szs_status -> Phases.env_with_result
  type errcode = int
  type prelude = Logtk.UntypedAST.statement Sequence.t
  type ('ret, 'before, 'after) phase =
      Init : (unit, 'a, [ `Init ]) Phases.phase
    | Setup_gc : (unit, [ `Init ], [ `Init ]) Phases.phase
    | Setup_signal : (unit, [ `Init ], [ `Init ]) Phases.phase
    | Parse_CLI :
        (Phases.filename list * Params.t, [ `Init ], [ `Parse_cli ])
        Phases.phase
    | LoadExtensions :
        (Extensions.t list, [ `Parse_cli ], [ `LoadExtensions ]) Phases.phase
    | Parse_prelude :
        (Phases.prelude, [ `LoadExtensions ], [ `Parse_prelude ])
        Phases.phase
    | Start_file :
        (Phases.filename, [ `Parse_prelude ], [ `Start_file ]) Phases.phase
    | Parse_file :
        (Logtk.Input_format.t * Logtk.UntypedAST.statement Sequence.t,
         [ `Start_file ], [ `Parse_file ])
        Phases.phase
    | Typing :
        (Logtk.TypeInference.typed_statement CCVector.ro_vector,
         [ `Parse_file ], [ `Typing ])
        Phases.phase
    | CNF :
        (Logtk.Statement.clause_t CCVector.ro_vector, [ `Typing ], [ `CNF ])
        Phases.phase
    | Compute_prec :
        (Logtk.Precedence.t, [ `CNF ], [ `Precedence ]) Phases.phase
    | Compute_ord_select :
        (Logtk.Ordering.t * Selection.t, [ `Precedence ],
         [ `Compute_ord_select ])
        Phases.phase
    | MakeCtx :
        ((module Ctx.S), [ `Compute_ord_select ], [ `MakeCtx ]) Phases.phase
    | MakeEnv :
        (Phases.env_with_clauses, [ `MakeCtx ], [ `MakeEnv ]) Phases.phase
    | Pre_saturate :
        ('c Env.packed * Saturate.szs_status * 'c Clause.sets, [ `MakeEnv ],
         [ `Pre_saturate ])
        Phases.phase
    | Saturate :
        (Phases.env_with_result, [ `Pre_saturate ], [ `Saturate ])
        Phases.phase
    | Print_result : (unit, [ `Saturate ], [ `Print_result ]) Phases.phase
    | Print_dot : (unit, [ `Print_result ], [ `Print_dot ]) Phases.phase
    | Check_proof :
        (Phases.errcode, [ `Print_dot ], [ `Check_proof ]) Phases.phase
    | Print_stats : (unit, [ `Check_proof ], [ `Print_stats ]) Phases.phase
    | Exit : (unit, 'b, [ `Exit ]) Phases.phase
  type any_phase = Any_phase : ('a, 'b, 'c) Phases.phase -> Phases.any_phase
  type (+'a, 'p1, 'p2) t
  val string_of_phase : ('a, 'b, 'c) Phases.phase -> string
  val string_of_any_phase : Phases.any_phase -> string
  val return : 'a -> ('a, 'p, 'p) Phases.t
  val fail : string -> ('a, 'b, 'c) Phases.t
  val return_err : 'a Phases.or_error -> ('a, 'p, 'p) Phases.t
  val exit : (unit, 'a, [ `Exit ]) Phases.t
  val start_phase :
    ('a, 'p1, 'p2) Phases.phase -> (unit, 'p1, [ `InPhase of 'p2 ]) Phases.t
  val return_phase : 'a -> ('a, [ `InPhase of 'p2 ], 'p2) Phases.t
  val return_phase_err :
    'a Phases.or_error -> ('a, [ `InPhase of 'p2 ], 'p2) Phases.t
  val current_phase : (Phases.any_phase, 'a, 'p2) Phases.t
  val with_phase :
    ('a, 'p1, 'p2) Phases.phase -> f:(unit -> 'a) -> ('a, 'p1, 'p2) Phases.t
  val with_phase1 :
    ('b, 'p1, 'p2) Phases.phase ->
    f:('a -> 'b) -> 'a -> ('b, 'p1, 'p2) Phases.t
  val with_phase2 :
    ('c, 'p1, 'p2) Phases.phase ->
    f:('a -> 'b -> 'c) -> 'a -> 'b -> ('c, 'p1, 'p2) Phases.t
  val bind :
    ('a, 'p_before, 'p_middle) Phases.t ->
    f:('a -> ('b, 'p_middle, 'p_after) Phases.t) ->
    ('b, 'p_before, 'p_after) Phases.t
  val map :
    ('a, 'p1, 'p2) Phases.t -> f:('a -> 'b) -> ('b, 'p1, 'p2) Phases.t
  val fold_l :
    f:('a -> 'b -> ('a, 'p, 'p) Phases.t) ->
    x:'a -> 'b list -> ('a, 'p, 'p) Phases.t
  val run_parallel :
    (Phases.errcode, 'p1, 'p2) Phases.t list ->
    (Phases.errcode, 'p1, 'p2) Phases.t
  module Infix :
    sig
      val ( >>= ) :
        ('a, 'p1, 'p2) Phases.t ->
        ('a -> ('b, 'p2, 'p3) Phases.t) -> ('b, 'p1, 'p3) Phases.t
      val ( >>?= ) :
        'a Phases.or_error ->
        ('a -> ('b, 'p1, 'p2) Phases.t) -> ('b, 'p1, 'p2) Phases.t
      val ( >|= ) :
        ('a, 'p1, 'p2) Phases.t -> ('a -> 'b) -> ('b, 'p1, 'p2) Phases.t
    end
  val ( >>= ) :
    ('a, 'p1, 'p2) t -> ('a -> ('b, 'p2, 'p3) t) -> ('b, 'p1, 'p3) t
  val ( >>?= ) : 'a or_error -> ('a -> ('b, 'p1, 'p2) t) -> ('b, 'p1, 'p2) t
  val ( >|= ) : ('a, 'p1, 'p2) t -> ('a -> 'b) -> ('b, 'p1, 'p2) t
  val empty_state : Logtk.Flex_state.t
  val get : (Logtk.Flex_state.t, 'a, 'a) Phases.t
  val set : Logtk.Flex_state.t -> (unit, 'a, 'a) Phases.t
  val get_key : 'a Logtk.Flex_state.key -> ('a, 'b, 'b) Phases.t
  val set_key : 'a Logtk.Flex_state.key -> 'a -> (unit, 'b, 'b) Phases.t
  val update :
    f:(Logtk.Flex_state.t -> Logtk.Flex_state.t) -> (unit, 'a, 'a) Phases.t
  val run_with :
    Logtk.Flex_state.t ->
    ('a, [ `Init ], [ `Exit ]) Phases.t ->
    (Logtk.Flex_state.t * 'a) Phases.or_error
  val run :
    ('a, [ `Init ], [ `Exit ]) Phases.t ->
    (Logtk.Flex_state.t * 'a) Phases.or_error
  module Key : sig val cur_phase : Phases.any_phase Logtk.Flex_state.key end
end