WP Interactive Prover

plugins.wp.tip.proofStatus (SIGNAL)

Proof Status has changed

plugins.wp.tip.printStatus (SIGNAL)

Updated TIP printer

plugins.wp.tip.node (DATA)

Proof Node index

node ::= #node

plugins.wp.tip.tactic (DATA)

Tactic identifier

tactic ::= $tactic

plugins.wp.tip.getNodeInfos (GET)

Proof node information

input ::= node

output ::= { output… }

Output Format Description
"title" string Proof node title
"proved" boolean Proof node complete
"pending" number Pending children
"size" number Proof size
"stats" string Node statistics
"results" [ prover , result ] [] Prover results for current node
"tactic" (opt.) tactic Applied tactic (if any)
"header" (opt.) string Proof node tactic label (if any)
"childLabel" (opt.) string Proof node child label (from parent, if any)
"path" node [] Proof node path from goal
"children" node [] Proof node tactic children (id any)

signals

plugins.wp.tip.getResult (GET)

Result for specified node and prover

input ::= { input… }

output ::= result

Input Format Description
"node" node Proof node
"prover" prover Prover

signals

plugins.wp.tip.getProofStatus (GET)

Current Proof Status of a Goal

input ::= { input… }

output ::= { output… }

Input Format Description
"main" goal Proof Obligation
"unproved" (opt.) boolean Report unproved children only
"subtree" (opt.) boolean Report subtree children only
Output Format Description
"size" number Proof size
"index" number Current node index among pending nodes (else -1)
"pending" number Pending proof nodes
"current" node Current proof node
"parents" node [] parents nodes
"tactic" (opt.) tactic Applied tactic (if any)
"children" node [] Children nodes

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.clearNode (SET)

Cancel all node results and sub-tree (if any)

input ::= node

output ::= null

plugins.wp.tip.clearNodeTactic (SET)

Cancel node current tactic

input ::= node

output ::= null

plugins.wp.tip.clearParentTactic (SET)

Cancel parent node tactic

input ::= node

output ::= null

plugins.wp.tip.clearGoal (SET)

Remove the complete goal proof tree

input ::= goal

output ::= null

plugins.wp.tip.part (DATA)

Proof part marker

part ::= $part

plugins.wp.tip.term (DATA)

Term marker

term ::= $term

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 (GET)

Pretty-print the associated node

input ::= { input… }

output ::= text

Input Format Description
"node" (opt.) 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

plugins.wp.tip.getSelection (GET)

Get current selection in proof node

input ::= node

output ::= { output… }

Output Format Description
"part" (opt.) part Selected part
"term" (opt.) term Selected term

signals

plugins.wp.tip.runProvers (SET)

Schedule provers on proof node

input ::= { input… }

output ::= null

Input Format Description
"node" node Proof node
"timeout" (opt.) number Prover timeout (in seconds, default: current)
"provers" (opt.) prover [] Prover selection (default: current

plugins.wp.tip.killProvers (SET)

Interrupt running provers on proof node

input ::= { input… }

output ::= null

Input Format Description
"node" node Proof node
"provers" (opt.) prover [] Prover selection (default: all running provers

plugins.wp.tip.clearProvers (SET)

Remove prover results from proof node

input ::= { input… }

output ::= null

Input Format Description
"node" node Proof node
"provers" (opt.) prover [] Prover selection (default: all results

plugins.wp.tip.getScriptStatus (GET)

Script Status for a given Goal

input ::= goal

output ::= { output… }

Output Format Description
"proof" boolean Some Proof Tree can be Saved
"script" (opt.) string Script File (if any)
"saved" boolean Current Proof Script has been Saved

signals

plugins.wp.tip.saveScript (SET)

Save Script for the Goal

input ::= goal

output ::= null

plugins.wp.tip.runScript (SET)

Replay Saved Script for the Goal (if any)

input ::= goal

output ::= null

plugins.wp.tip.clearProofScript (SET)

Clear Proof and Remove any Saved Script for the Goal

input ::= goal

output ::= null