WP Interactive Prover

plugins.wp.tip.proofStatus (SIGNAL)

Proof Status has changed

plugins.wp.tip.getNodeInfos (GET)

Proof node information

input ::= #node

output ::= { output… }

Output Format Description
"result" string Proof node title
"proved" boolean Proof node complete
"pending" number Pending children
"size" number Proof size
"stats" string Node statistics

signals

plugins.wp.tip.getProofState (GET)

Current Proof Status of a Goal

input ::= goal

output ::= { output… }

Output Format Description
"current" #node Current proof node
"parents" #node [] Proof node parents
"pending" number Pending proof nodes
"index" number Current node index among pending nodes (else -1)
"results" [ prover , result ] [] Prover results for current node
"tactic" string Proof node tactic header (if any)
"children" [ string , #node ] [] Proof node tactic children (id any)

signals

plugins.wp.tip.goForward (SET)

Go to to first pending node, or root if none

input ::= goal

output ::= null

plugins.wp.tip.goToRoot (SET)

Go to root of proof tree

input ::= goal

output ::= null

plugins.wp.tip.goToIndex (SET)

Go to k-th pending node of proof tree

input ::= [ goal , number ]

output ::= null

plugins.wp.tip.goToNode (SET)

Set current node of associated proof tree

input ::= #node

output ::= null

plugins.wp.tip.removeNode (SET)

Remove node from tree and go to parent

input ::= #node

output ::= null

plugins.wp.tip.printStatus (SIGNAL)

Updated TIP printer

plugins.wp.tip.iformat (DATA)

Integer constants format

iformat ::= "dec" | "hex" | "bin"

plugins.wp.tip.rformat (DATA)

Real constants format

rformat ::= "ratio" | "float" | "double"

plugins.wp.tip.printSequent (EXEC)

Pretty-print the associated node

input ::= { input… }

output ::= text

Input Format Description
"node" #node Proof Node
"indent" (opt.) number Number of identation spaces
"margin" (opt.) number Maximial text width
"iformat" (opt.) iformat Integer constants format
"rformat" (opt.) rformat Real constants format
"autofocus" (opt.) boolean Auto-focus mode
"unmangled" (opt.) boolean Unmangled memory model

signals

plugins.wp.tip.clearSelection (SET)

Reset node selection

input ::= #node

output ::= null

plugins.wp.tip.setSelection (SET)

Set node selection

input ::= { input… }

output ::= null

Input Format Description
"node" #node Proof Node
"part" (opt.) $part Selected part
"term" (opt.) $term Selected term
"extend" (opt.) boolean Extending selection mode