Module ProofEngine

module ProofEngine: sig .. end

Interactive Proof Engine


type tree 

A proof tree

type node 

A proof node

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

Leaves are numbered from 0 to n-1

type status = [ `Main | `Pending of int | `Proved ] 
type state = [ `Opened | `Pending of int | `Proved | `Script of int ] 
type current = [ `Internal of node | `Leaf of int * node | `Main ] 
type position = [ `Leaf of int | `Main | `Node of node ] 
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_model : tree -> Model.t
val node_model : node -> Model.t
val opened : node -> bool

not proved

val proved : node -> bool

not opened

val title : node -> string
val state : node -> state
val parent : node -> node option
val pending : node -> int
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 : resolve:bool ->
fork -> node * (string * node) list
val pretty : Format.formatter -> fork -> unit
val script : tree -> ProofScript.jscript
val bind : node -> ProofScript.jscript -> unit
val bound : node -> ProofScript.jscript