Module `Libzipperposition_phases.Phases`Source

Phases of the Prover

To process a file, the prover goes through a sequence of phases that are used to build values. This module reifies the phases.

Sourcetype filename = string

Sourcetype 'a or_error = ('a, string) CCResult.t

Phases

Sourcetype env_with_clauses =

| Env_clauses : 'c Libzipperposition.Env.packed * 'c Libzipperposition.Clause.sets -> env_with_clauses

Sourcetype env_with_result =

| Env_result : 'c Libzipperposition.Env.packed * Libzipperposition.Saturate.szs_status -> env_with_result

Sourcetype errcode = int

Sourcetype prelude = Logtk.UntypedAST.statement Iter.t

Sourcetype ('ret, 'before, 'after) phase =

| Init : (unit, _, [ `Init ]) phase
| Setup_gc : (unit, [ `Init ], [ `Init ]) phase
| Setup_signal : (unit, [ `Init ], [ `Init ]) phase
| Parse_CLI : (filename list * Libzipperposition.Params.t, [ `Init ], [ `Parse_cli ]) phase
| LoadExtensions : (Libzipperposition.Extensions.t list, [ `Parse_cli ], [ `LoadExtensions ]) phase
| Parse_prelude : (prelude, [ `LoadExtensions ], [ `Parse_prelude ]) phase
| Start_file : (filename, [ `Parse_prelude ], [ `Start_file ]) phase
| Parse_file : (Logtk.Input_format.t * Logtk.UntypedAST.statement Iter.t, [ `Start_file ], [ `Parse_file ]) phase
| Typing : (Logtk.TypeInference.typed_statement CCVector.ro_vector, [ `Parse_file ], [ `Typing ]) phase
| CNF : (Logtk.Statement.clause_t CCVector.ro_vector, [ `Typing ], [ `CNF ]) phase
| Compute_prec : (Logtk.Precedence.t, [ `CNF ], [ `Precedence ]) phase
| Compute_ord_select : (Logtk.Ordering.t * Libzipperposition.Selection.t, [ `Precedence ], [ `Compute_ord_select ]) phase
| MakeCtx : ((module Libzipperposition.Ctx.S), [ `Compute_ord_select ], [ `MakeCtx ]) phase
| MakeEnv : (env_with_clauses, [ `MakeCtx ], [ `MakeEnv ]) phase
| Pre_saturate : ('c Libzipperposition.Env.packed * Libzipperposition.Saturate.szs_status * 'c Libzipperposition.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

Sourcetype any_phase =

| Any_phase : (_, _, _) phase -> any_phase
(*
A phase hidden in an existential type
*)

Main Type

Sourcetype (+'a, 'p1, 'p2) t

Monad type, representing an action starting at phase 'p1 and stopping at phase 'p2

Sourceval string_of_phase : (_, _, _) phase -> string

Sourceval string_of_any_phase : any_phase -> string

Sourceval return : 'a -> ('a, 'p, 'p) t

Return a value into the monad

Sourceval fail : string -> (_, _, _) t

Fail with the given error message

Sourceval return_err : 'a or_error -> ('a, 'p, 'p) t

Sourceval exit : (unit, _, [ `Exit ]) t

Exit

Sourceval start_phase : (_, 'p1, 'p2) phase -> (unit, 'p1, [ `InPhase of 'p2 ]) t

Start the given phase

Sourceval return_phase : 'a -> ('a, [ `InPhase of 'p2 ], 'p2) t

Finish the given phase

Sourceval return_phase_err : 'a or_error -> ('a, [ `InPhase of 'p2 ], 'p2) t

Sourceval current_phase : (any_phase, _, 'p2) t

Get the current phase

Sourceval with_phase : ('a, 'p1, 'p2) phase -> f:(unit -> 'a) -> ('a, 'p1, 'p2) t

Start phase, call f () to get the result, return its result using return_phase

Source

val with_phase1 : 
  ('b, 'p1, 'p2) phase ->
  f:('a -> 'b) ->
  'a ->
  ('b, 'p1, 'p2) t

Source

val with_phase2 : 
  ('c, 'p1, 'p2) phase ->
  f:('a -> 'b -> 'c) ->
  'a ->
  'b ->
  ('c, 'p1, 'p2) t

Source

val bind : 
  ('a, 'p_before, 'p_middle) t ->
  f:('a -> ('b, 'p_middle, 'p_after) t) ->
  ('b, 'p_before, 'p_after) t

bind state f calls f to go one step further from state

Sourceval map : ('a, 'p1, 'p2) t -> f:('a -> 'b) -> ('b, 'p1, 'p2) t

Map the current value

Source

val fold_l : 
  f:('a -> 'b -> ('a, 'p, 'p) t) ->
  x:'a ->
  'b list ->
  ('a, 'p, 'p) t

Sourceval run_parallel : (errcode, 'p1, 'p2) t list -> (errcode, 'p1, 'p2) t

run_sequentiel l runs each action of the list in succession, restarting every time with the initial state (once an action has finished, its state is discarded). Only the very last state is kept. If any errcode is non-zero, then the evaluation stops with this errcode

Sourcemodule Infix : sig ... end

include module type of Infix

Sourceval (>>=) : ('a, 'p1, 'p2) t -> ('a -> ('b, 'p2, 'p3) t) -> ('b, 'p1, 'p3) t

Sourceval (>>?=) : 'a or_error -> ('a -> ('b, 'p1, 'p2) t) -> ('b, 'p1, 'p2) t

Sourceval (>|=) : ('a, 'p1, 'p2) t -> ('a -> 'b) -> ('b, 'p1, 'p2) t

Sourceval empty_state : Logtk.Flex_state.t

Sourceval get : (Logtk.Flex_state.t, 'a, 'a) t

Sourceval set : Logtk.Flex_state.t -> (unit, 'a, 'a) t

Sourceval get_key : 'a Logtk.Flex_state.key -> ('a, 'b, 'b) t

get_key k returns the value associated with k in the state

Sourceval set_key : 'a Logtk.Flex_state.key -> 'a -> (unit, 'b, 'b) t

Sourceval update : f:(Logtk.Flex_state.t -> Logtk.Flex_state.t) -> (unit, 'a, 'a) t

update ~f changes the state using f

Source

val run_with : 
  Logtk.Flex_state.t ->
  ('a, [ `Init ], [ `Exit ]) t ->
  (Logtk.Flex_state.t * 'a) or_error

run_with state m executes the actions in m starting with state, returning some value (or error) and the final state.

Sourceval run : ('a, [ `Init ], [ `Exit ]) t -> (Logtk.Flex_state.t * 'a) or_error

run m is run_with empty_state m

Sourcemodule Key : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

doc/libzipperposition.phases/Libzipperposition_phases/Phases/index.html

Module `Libzipperposition_phases.Phases`Source

Phases of the Prover

Phases

Main Type

package libzipperposition

Install

Dune Dependency

Authors

Maintainers

Sources

doc/libzipperposition.phases/Libzipperposition_phases/Phases/index.html

Module Libzipperposition_phases.PhasesSource

Phases of the Prover

Phases

Main Type

Module `Libzipperposition_phases.Phases`Source