Module Wp.ProofEngine

Interactive Proof Engine

type tree

A proof tree

type node

A proof node

val get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]
val proof : main:Wpo.t -> tree
val reset : tree -> unit
val remove : Wpo.t -> unit
val validate : tree -> unit

Re-compute stats & set status of the entire script

val consolidated : Wpo.t -> Stats.stats

Consolidate statistics wrt current script or prover results

Leaves are numbered from 0 to n-1

type status = [
| `Unproved(*

proof obligation not proved

*)
| `Proved(*

proof obligation is proved

*)
| `Pending of int(*

proof is pending

*)
| `Passed(*

smoke test is passed (PO is not proved)

*)
| `Invalid(*

smoke test has failed (PO is proved)

*)
| `StillResist of int(*

proof is pending

*)
]
type current = [
| `Main
| `Internal of node
| `Leaf of int * node
]
type position = [
| `Main
| `Node of node
| `Leaf of int
]
val pool : tree -> Lang.F.pool
val saved : tree -> bool
val set_saved : tree -> bool -> unit
val status : tree -> status
val current : tree -> current
val goto : tree -> position -> unit
val main : tree -> Wpo.t
val head : tree -> Wpo.t
val goal : node -> Wpo.t
val tree_context : tree -> WpContext.t
val node_context : node -> WpContext.t
val title : node -> string
val proved : node -> bool
val pending : node -> int
val stats : node -> Stats.stats
val parent : node -> node option
val children : node -> (string * node) list
val tactical : node -> ProofScript.jtactic option
val get_strategies : node -> int * Strategy.t array
val set_strategies : node -> ?index:int -> Strategy.t array -> unit
val forward : tree -> unit
val cancel : tree -> unit
type fork
val anchor : tree -> ?node:node -> unit -> node
val fork : tree -> anchor:node -> ProofScript.jtactic -> Tactical.process -> fork
val iter : ( Wpo.t -> unit ) -> fork -> unit
val commit : fork -> node * (string * node) list
val pretty : Stdlib.Format.formatter -> fork -> unit
val script : tree -> ProofScript.jscript
val bind : node -> ProofScript.jscript -> unit
val bound : node -> ProofScript.jscript