Module Wp.ProofEngineSource

Interactive Proof Engine

Sourcetype tree

A proof tree

Sourcetype node

A proof node

Sourcemodule Node : sig ... end
Sourceval get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]
Sourceval proof : main:Wpo.t -> tree
Sourceval validate : tree -> unit

Consolidate and update status of the entire script (memoized).

Sourceval consolidate : Wpo.t -> unit

Consolidate proof tree (memoized).

Sourceval consolidated : Wpo.t -> Stats.stats

Consolidated statistics (memoized).

Sourceval results : Wpo.t -> (VCS.prover * VCS.result) list

Consolidated results (memoized).

Leaves are numbered from 0 to n-1

Sourcetype status = [
  1. | `Unproved
    (*

    proof obligation not proved

    *)
  2. | `Proved
    (*

    proof obligation is proved

    *)
  3. | `Pending of int
    (*

    proof is pending

    *)
  4. | `Passed
    (*

    smoke test is passed (PO is not proved)

    *)
  5. | `Invalid
    (*

    smoke test has failed (PO is proved)

    *)
  6. | `StillResist of int
    (*

    proof is pending

    *)
]
Sourcetype current = [
  1. | `Main
  2. | `Internal of node
  3. | `Leaf of int * node
]
Sourcetype position = [
  1. | `Main
  2. | `Node of node
  3. | `Leaf of int
]
Sourceval pool : tree -> Lang.F.pool
Sourceval saved : tree -> bool
Sourceval set_saved : tree -> bool -> unit
Sourceval status : tree -> status
Sourceval current : tree -> current
Sourceval goto : tree -> position -> unit
Sourceval root : tree -> node
Sourceval main : tree -> Wpo.t
Sourceval goal : node -> Wpo.t
Sourceval tree : node -> tree
Sourceval head : tree -> node option
Sourceval head_goal : tree -> Wpo.t
Sourceval tree_context : tree -> WpContext.t
Sourceval node_context : node -> WpContext.t
Sourceval title : node -> string
Sourceval fully_proved : node -> bool
Sourceval locally_proved : node -> bool
Sourceval pending : node -> int
Sourceval stats : node -> Stats.stats
Sourceval depth : node -> int
Sourceval path : node -> node list
Sourceval parent : node -> node option
Sourceval tactic : node -> Tactical.t option
Sourceval child_label : node -> string option
Sourceval tactic_label : node -> string option
Sourceval subgoals : node -> node list
Sourceval children : node -> (string * node) list
Sourceval tactical : node -> ProofScript.jtactic option
Sourceval get_strategies : node -> int * Strategy.t array
Sourceval set_strategies : node -> ?index:int -> Strategy.t array -> unit
Sourceval get_hint : node -> string option
Sourceval set_hint : node -> string -> unit
Sourceval forward : tree -> unit
Sourceval clear_goal : Wpo.t -> unit
Sourceval clear_tree : tree -> unit
Sourceval clear_node : tree -> node -> unit
Sourceval clear_node_tactic : tree -> node -> unit
Sourceval clear_parent_tactic : tree -> node -> unit
Sourceval add_goal_hook : (Wpo.t -> unit) -> unit
Sourceval add_clear_hook : (Wpo.t -> unit) -> unit
Sourceval add_remove_hook : (node -> unit) -> unit
Sourceval add_update_hook : (node -> unit) -> unit
Sourceval cancel_parent_tactic : tree -> unit
Sourceval cancel_current_node : tree -> unit
Sourcetype fork
Sourceval anchor : tree -> ?node:node -> unit -> node
Sourceval iter : (Wpo.t -> unit) -> fork -> unit
Sourceval commit : fork -> node * (string * node) list
Sourceval pretty : Format.formatter -> fork -> unit
Sourceval has_proof : Wpo.t -> bool
Sourceval has_script : tree -> bool
Sourceval bind : node -> ProofScript.jscript -> unit