').text(msg);
- this.notifications.append(div);
- setTimeout(() => div.remove(), 4000);
- }
-}
-
-type OpenOptions = {name?: string, silent?: boolean};
-const DEFAULT_URL = '/trace.out';
-
-
-class DragDropJson extends EventEmitter {
-
- constructor(container: JQuery) {
- super();
- container.on('dragover', (ev) => {
- ev.preventDefault();
- });
- container.on('drop', (ev) => {
- this.drop(ev.originalEvent.dataTransfer);
- ev.preventDefault();
- });
- }
-
- async drop(dt: DataTransfer) {
- if (dt.files.length == 1) {
- this.emit('open', {file: dt.files[0]});
- }
- else this.emit('error', "Can only process one file at a time");
- }
-}
-
-
-
-export { MainDocument, OpenOptions, DragDropJson }
diff --git a/src/viz/ts/proof-interaction.css b/src/viz/ts/proof-interaction.css
new file mode 100644
index 000000000..8107ec8fd
--- /dev/null
+++ b/src/viz/ts/proof-interaction.css
@@ -0,0 +1,18 @@
+.proof-interaction-choices div.goal {
+ display: inline-block;
+ max-width: 20em;
+ vertical-align: top;
+ margin-right: .5em;
+ border: 1px solid #888;
+ padding: 2px;
+}
+
+.proof-trace .proof-trace-highlight-interact-focus {
+ outline: 3px solid violet;
+}
+
+.proof-interaction-result div.procedure {
+ font-family: Courier, Consolas, 'Courier New', monospace;
+ font-size: 10pt;
+ white-space: pre;
+}
\ No newline at end of file
diff --git a/src/viz/ts/proof-interaction.ts b/src/viz/ts/proof-interaction.ts
new file mode 100644
index 000000000..ceca4763e
--- /dev/null
+++ b/src/viz/ts/proof-interaction.ts
@@ -0,0 +1,178 @@
+import { EventEmitter } from 'events';
+import Vue from 'vue';
+
+import { VueEventHook } from './infra/event-hooks';
+import type { ProofTrace } from './proof-trace';
+import type { BenchmarksDB } from './benchmarks';
+
+import './proof-interaction.css';
+
+
+
+class ProofInteraction extends EventEmitter {
+ wsURL: string
+ ws: WebSocket
+
+ pt: ProofTrace
+ view: View.State
+
+ _actionHook = new VueEventHook('interaction:action')
+
+ defaultMode = ProofInteraction.Data.ProofMode.INTERACTIVE
+
+ constructor(pt: ProofTrace, pane: Vue & View.PaneProps) {
+ super();
+ this.wsURL = this._wsURL();
+ this.pt = pt;
+ this.createView(pane);
+ }
+
+ get id() { return this.pt.id; }
+
+ createView(pane: Vue & View.PaneProps) {
+ this.view = {focused: [], choices: undefined, result: undefined};
+ Vue.set(pane.docs[this.id], 'interaction', this.view);
+ this._actionHook.attach(pane, action => this.handleAction(action));
+ }
+
+ destroy() {
+ this._actionHook.detach();
+ this.ws?.close();
+ }
+
+ async start(spec?: Data.Spec, mode?: Data.ProofMode) {
+ this.ws = new WebSocket(this.wsURL);
+ this.ws.addEventListener('message', m => this.handleMessage(m.data));
+ await new Promise((resolve, reject) => {
+ this.ws.addEventListener('open', resolve);
+ this.ws.addEventListener('error', reject)
+ });
+ this.ws.addEventListener('error', err => this.emit('error', err));
+ if (spec) this.sendSpec(spec, mode);
+ }
+
+ /**
+ * For auto mode, terminates ongoing computation.
+ */
+ stop() {
+ this.destroy(); // possibly can still allow expanding nodes after termination; not currently supported
+ }
+
+ sendSpec(spec: Data.Spec, mode: Data.ProofMode = this.defaultMode) {
+ this._send({mode, ...spec}, ProofInteraction.Data.Classes.SPEC);
+ }
+
+ sendChoose(choice: string) {
+ this._send({choice}, ProofInteraction.Data.Classes.CHOOSE);
+ }
+
+ sendExpandRequest(nodeId: ProofTrace.Data.NodeId) {
+ this._send({id: nodeId}, ProofInteraction.Data.Classes.EXPAND_REQUEST);
+ }
+
+ _send(json: any, $type?: string) {
+ if (this.ws.readyState !== WebSocket.OPEN) {
+ this.emit('error', {message: 'disconnected from server'});
+ return;
+ }
+ this.ws.send(JSON.stringify($type ? {$type, ...json} : json))
+ }
+
+ handleMessage(data: string) {
+ try {
+ var msg = JSON.parse(data);
+ }
+ catch { console.error(data); return; }
+
+ this.emit('message', msg);
+
+ if (Array.isArray(msg)) {
+ this.view.focused = this.getNodesForChoices(msg);
+ this.view.choices = msg;
+ this.emit('choose', msg);
+ }
+ else if (msg.procs) {
+ this.view.result = msg;
+ this.emit('done', msg);
+ }
+ else if (msg.tag === 'SynthesisStatsEntry') { console.log('stats', msg); /** @todo */ }
+ else if (msg.error) this.emit('error', {message: msg.error, sticky: msg.sticky});
+ else this.emit('trace', msg);
+ }
+
+ handleAction(action: View.Action) {
+ switch (action.type) {
+ case 'select':
+ this.view.choices = undefined; // clear choices
+ this.sendChoose(action.goal.id);
+ break;
+ }
+ }
+
+ getNodesForChoices(choices: {from: ProofTrace.Data.GoalId[]}[]): ProofTrace.Data.NodeId[] {
+ var ret: ProofTrace.Data.NodeId[] = [];
+ for (let choice of choices) {
+ for (let goalId of choice.from) {
+ let node = this.pt.nodeIndex.byGoalId.get(goalId);
+ if (node) ret.push(node.id);
+ }
+ }
+ return ret;
+ }
+
+ _wsURL() {
+ switch (window.location.protocol) {
+ case 'https:': return `wss://${location.host}${location.pathname}`;
+ case 'http:': return `ws://${location.host}${location.pathname}`;
+ default: return 'ws://localhost:8033'; // dev mode
+ }
+ }
+}
+
+
+import Data = ProofInteraction.Data;
+import View = ProofInteraction.View;
+
+
+namespace ProofInteraction {
+
+ export namespace Data {
+
+ export namespace Classes {
+ const NS = "org.tygus.suslik.interaction.AsyncSynthesisRunner";
+
+ export const SPEC = `${NS}.SpecMessage`,
+ CHOOSE = `${NS}.ChooseMessage`,
+ EXPAND_REQUEST = `${NS}.ExpandRequestMessage`;
+ }
+
+ export type Spec = BenchmarksDB.Data.Spec;
+
+ export enum ProofMode {
+ AUTOMATIC = "automatic",
+ INTERACTIVE = "interactive"
+ }
+ }
+
+ export namespace View {
+
+ export type PaneProps = {docs: {[id: string]: {interaction: State}}};
+
+ export type State = {
+ focused: ProofTrace.Data.NodeId[]
+ choices: ProofTrace.Data.GoalEntry[]
+ result: {procs: {pp: string}[]}
+ };
+
+ export type Action = {
+ type: 'select'
+ goal?: ProofTrace.Data.GoalEntry
+ };
+
+ }
+
+}
+
+
+
+export { ProofInteraction }
\ No newline at end of file
diff --git a/src/viz/ts/proof-trace.css b/src/viz/ts/proof-trace.css
index 8ab3a29ea..1ef73ec70 100644
--- a/src/viz/ts/proof-trace.css
+++ b/src/viz/ts/proof-trace.css
@@ -1,14 +1,15 @@
#proof-trace-pane {
padding-bottom: 25%;
+ padding-left: .5em;
}
-.proof-trace-pane-area {
+.proof-trace-pane-rendered {
transform: scale(var(--zoom));
transform-origin: 0 0;
}
.proof-trace .subtrees {
- white-space: nowrap;
+ display: flex;
}
.proof-trace-node {
@@ -26,11 +27,16 @@
cursor: default;
}
+.proof-trace-node > .title > span.pp {
+ margin-right: .75em;
+}
+
.proof-trace-node > .title > span.goal-id,
.proof-trace-node > .title > span.cost,
.proof-trace-node > .title > span.tag,
-.proof-trace-node > .title > span.num-descendants {
- float: right;
+.proof-trace-node > .title > span.num-descendants,
+.proof-trace-node > .title > span.call {
+ float: right;
margin-left: 1em;
font-family: 'Times New Roman', Times, serif;
font-size: 90%;
@@ -51,12 +57,28 @@
line-height: 1pt;
}
+.proof-trace-node > .title > span.call::before {
+ content: "📣";
+ line-height: 1pt;
+}
+
.proof-trace-goal {
+ clear: both; /* skip any floats from title */
white-space: normal;
border: 1px solid #999;
padding: 2px;
}
+.proof-trace-goal .synth-arrow {
+ color: #88f;
+}
+
+.proof-trace-goal .proof-trace-sketch {
+ color: #66e;
+ font-family: Courier, Consolas, 'Courier New', monospace;
+ font-size: 80%;
+}
+
.proof-trace-node:hover > .proof-trace-goal {
background: #fff;
}
@@ -67,6 +89,7 @@
margin-right: 0.2em;
margin-bottom: 0.5em;
vertical-align: top;
+ flex-shrink: 0;
}
.proof-trace-vars > span:not(:last-child)::after {
@@ -129,6 +152,10 @@
background: #eee;
}
+.proof-trace-formula span.null-cardinality {
+ display: none;
+}
+
.proof-trace:not(:last-child) {
border-top: 1px solid #aaa;
margin-right: 0;
@@ -141,6 +168,8 @@
.proof-trace-node.AndNode {
background: #999;
color: #ddd;
+ padding-left: .4em;
+ padding-right: .3em;
}
.proof-trace-node.AndNode:hover {
@@ -216,6 +245,26 @@
display: inline;
}
+.proof-trace-node-subordinate {
+ background: #fffe;
+ border: 1px solid #aaa;
+}
+.proof-trace-node-subordinate > .title {
+ text-align: right;
+ padding: 0 .25em;
+ font-size: 90%;
+ margin-bottom: -.25em;
+}
+.proof-trace-node-subordinate > .title span.goal-id {
+ border: 1px solid #aaf;
+ border-radius: 5px;
+ padding: 0 3px;
+ background: #bbf2;
+}
+.proof-trace-node-subordinate > .proof-trace-goal {
+ border: none;
+}
+
/* Filters */
.proof-trace-filter--only-success .proof-trace:not(.Succeeded):not(.Succeeded\*) {
@@ -229,11 +278,11 @@
/* Toobar */
.proof-trace-toolbar {
- position: fixed;
+ position: sticky;
top: 0;
- left: 20em;
+ left: 2em;
+ width: calc(100% - 2em);
background: #ffffffd0;
- padding: 1em 5em .75em 1em;
z-index: 1;
}
@@ -249,14 +298,3 @@
padding: .1em .5em;
background: #ddd;
}
-
-#notifications {
- position: fixed;
- top: 0;
- right: 0;
-}
-#notifications > div {
- background: #fbb;
- color: #333;
- padding: 9px;
-}
diff --git a/src/viz/ts/proof-trace.ts b/src/viz/ts/proof-trace.ts
index a8d286a3c..11729c9ec 100644
--- a/src/viz/ts/proof-trace.ts
+++ b/src/viz/ts/proof-trace.ts
@@ -1,65 +1,104 @@
+import { EventEmitter } from 'events';
import arreq from 'array-equal';
-import $ from 'jquery';
-import Vue from 'vue/dist/vue';
-import { VueContext } from 'vue-context'
+import Vue from 'vue';
import 'vue-context/dist/css/vue-context.css';
+import { VueEventHook } from './infra/event-hooks';
+
import './proof-trace.css';
import './menu.css';
-class ProofTrace {
+class ProofTrace extends EventEmitter {
+ id: string
data: Data
root: Data.NodeEntry
nodeIndex: {
byId: JSONMap
+ byGoalUid: JSONMap
childrenById: JSONMap
subtreeSizeById: JSONMap
statusById: JSONMap
+ derivationById: JSONMap
+ derivationByGoalUid: JSONMap
viewById: JSONMap
}
- view: Vue
+ view: View.Props
+
+ _actionHook = new VueEventHook('action')
+ _dirty: {nodes: Set} = {nodes: new Set}
- constructor(data: ProofTrace.Data) {
+ constructor(id: string, data: ProofTrace.Data, pane?: Vue & View.PaneProps) {
+ super();
+ this.id = id;
this.data = data;
this.root = this.data.nodes[0];
this.createIndex();
- this.createView();
+ this.createView(pane);
+ }
+
+ append(data: Data, opts: {expand?: boolean} = {}) {
+ Data.append(this.data, data);
+ this.updateIndex(data);
+ for (let node of data.nodes)
+ this.addNode(node, opts);
+ this.refreshView();
}
createIndex() {
this.nodeIndex = {
- byId: new JSONMap(),
- childrenById: new JSONMap(), subtreeSizeById: new JSONMap(),
- statusById: new JSONMap(),
- viewById: new JSONMap()
+ byId: new JSONMap, byGoalUid: new JSONMap,
+ childrenById: new JSONMap, subtreeSizeById: new JSONMap,
+ statusById: new JSONMap, derivationById: new JSONMap,
+ derivationByGoalUid: new JSONMap,
+ viewById: new JSONMap
};
- // Build byId
- for (let node of this.data.nodes) {
- if (!this.nodeIndex.byId.get(node.id))
- this.nodeIndex.byId.set(node.id, node);
+ this.updateIndex(this.data);
+ }
+
+ updateIndex(data: Data) {
+ // Build byId, byGoalId
+ for (let node of data.nodes) {
+ this.nodeIndex.byId.set(node.id, node);
+ if (node.goal)
+ this.nodeIndex.byGoalUid.set(node.goal.uid, node);
}
// Build childrenById
- for (let node of this.data.nodes) {
+ for (let node of data.nodes) {
if (node.id.length >= 1) {
var parent = node.id.slice(1);
- this.addChild(parent, node);
+ this.addChildToIndex(parent, node);
+ }
+ }
+
+ let update = (m: JSONMap,
+ node: Data.NodeEntry, value: T) => {
+ if (!node) return;
+ var key = node.id, old = m.get(key);
+ if (value !== old) { /** @todo better equality check */
+ m.set(key, value);
+ this._dirty.nodes.add(node);
}
}
// Build statusById
- for (let entry of this.data.statuses) {
+ for (let entry of data.statuses) {
var id = entry.at;
- this.nodeIndex.statusById.set(id, entry);
+ update(this.nodeIndex.statusById,
+ this.nodeIndex.byId.get(id), entry);
}
- for (let node of this.data.nodes.sort((a, b) => b.id.length - a.id.length)) {
+ // - compute transitive success
+ // This has to be computed over *all* data; can optimize by only
+ // considering ancestors of newly indexed nodes
+ var nodesBottomUp = this.data.nodes.slice().sort((a, b) => b.id.length - a.id.length)
+ for (let node of nodesBottomUp) {
if (!this.nodeIndex.statusById.get(node.id)) {
let children = (this.nodeIndex.childrenById.get(node.id) || [])
.map(c => this.nodeIndex.statusById.get(c.id));
@@ -67,12 +106,14 @@ class ProofTrace {
switch (node.tag) {
case Data.NodeType.OrNode:
if (children.some(x => x && x.status.tag === 'Succeeded'))
- this.nodeIndex.statusById.set(node.id, {at: node.id, status: {tag: 'Succeeded', from: '*'}});
+ update(this.nodeIndex.statusById, node,
+ {at: node.id, status: {tag: 'Succeeded', from: '*'}});
break;
case Data.NodeType.AndNode:
if (children.length == node.nChildren &&
children.every(x => x && x.status.tag === 'Succeeded'))
- this.nodeIndex.statusById.set(node.id, {at: node.id, status: {tag: 'Succeeded', from: '*'}});
+ update(this.nodeIndex.statusById,
+ node, {at: node.id, status: {tag: 'Succeeded', from: '*'}});
break;
}
}
@@ -80,15 +121,35 @@ class ProofTrace {
}
// Build subtreeSizeById
+ // (same here)
var sz = this.nodeIndex.subtreeSizeById;
- for (let node of this.data.nodes.sort((a, b) => b.id.length - a.id.length)) {
+ for (let node of nodesBottomUp) {
let children = (this.nodeIndex.childrenById.get(node.id) || []);
- sz.set(node.id, 1 + children.map(u => sz.get(u.id) || 1)
- .reduce((x,y) => x + y, 0));
+ update(sz, node, 1 + children.map(u => sz.get(u.id) || 1)
+ .reduce((x,y) => x + y, 0));
+ }
+
+ // Build derivationById, derivationByGoalId
+ for (let deriv of data.trail) {
+ for (let goalUid of deriv.to) {
+ this.nodeIndex.derivationByGoalUid.set(goalUid, deriv);
+ let node = this.nodeIndex.byGoalUid.get(goalUid),
+ parent = node && this.parent(node);
+ if (parent)
+ update(this.nodeIndex.derivationById, parent, deriv);
+ }
+ }
+
+ for (let node of data.nodes) {
+ if (node.goal) {
+ var deriv = this.nodeIndex.derivationByGoalUid.get(node.goal.uid);
+ if (deriv)
+ update(this.nodeIndex.derivationById, this.parent(node), deriv);
+ }
}
}
- addChild(parent: Data.NodeId, child: Data.NodeEntry) {
+ addChildToIndex(parent: Data.NodeId, child: Data.NodeEntry) {
var m = this.nodeIndex.childrenById;
// Note: nodes can re-occur if they were suspended during the search
var l = m.get(parent) || [];
@@ -96,6 +157,11 @@ class ProofTrace {
m.set(parent, l.concat([child]));
}
+ parent(node: Data.NodeEntry) {
+ var id = Data.parentId(node.id);
+ return this.nodeIndex.byId.get(id);
+ }
+
children(node: Data.NodeEntry) {
function lex2(a1: number[], a2: number[]) {
let n = Math.min(2, a1.length, a2.length);
@@ -112,14 +178,48 @@ class ProofTrace {
.sort(byId2); // modifies the list but that's ok
}
- createView() {
- this.view = new (Vue.component('proof-trace-pane'))();
- this.view.root = this.createNode(this.root);
- this.expandNode(this.view.root);
- this.expandNode(this.view.root.children[0]);
- this.view.$mount();
+ createView(pane: Vue & View.PaneProps) {
+ this.view = {root: undefined};
+ this._dirty.nodes.clear();
+ if (this.root) {
+ this.view.root = this.createNode(this.root);
+ this.expandNode(this.view.root);
+ if (this.view.root.children?.[0]) /* a bit arbitrary I know */
+ this.expandNode(this.view.root.children[0]);
+ }
+
+ Vue.set(pane.docs, this.id, {trace: this.view});
+ this._actionHook.attach(
+ pane, (ev: View.ActionEvent) => this.viewAction(ev));
+ }
+
+ refreshView() {
+ for (let node of this._dirty.nodes)
+ this.refreshNode(node);
+ this._dirty.nodes.clear();
+ }
- this.view.$on('action', (ev: View.ActionEvent) => this.viewAction(ev));
+ destroy() {
+ this._actionHook.detach();
+ }
+
+ addNode(node: Data.NodeEntry, opts: {expand?: boolean}) {
+ if (node.id.length == 0) { // this is the root
+ this.root = node;
+ this.view.root = this.createNode(node);
+ }
+ else {
+ var parentId = Data.parentId(node.id),
+ parentView = this.nodeIndex.viewById.get(parentId);
+ if (parentView) {
+ parentView.children ??= [];
+ parentView.children.push(this.createNode(node));
+ if (opts.expand) { /** @todo only if parent is visible */
+ parentView.focus = true;
+ parentView.expanded = true;
+ }
+ }
+ }
}
getStatus(node: Data.NodeEntry): Data.GoalStatusEntry {
@@ -131,26 +231,41 @@ class ProofTrace {
return this.nodeIndex.subtreeSizeById.get(node.id) || 1;
}
+ getDerivationTrail(node: Data.NodeEntry): Data.DerivationTrailEntry {
+ return this.nodeIndex.derivationById.get(node.id);
+ }
+
createNode(node: Data.NodeEntry): View.Node {
var v = {value: node, children: undefined, focus: false, expanded: false,
status: this.getStatus(node),
+ derivation: this.getDerivationTrail(node),
numDescendants: this.getSubtreeSize(node)};
this.nodeIndex.viewById.set(node.id, v);
return v;
}
- expandNode(nodeView: View.Node, focus: boolean = false) {
+ refreshNode(node: Data.NodeEntry) {
+ var view = this.nodeIndex.viewById.get(node.id);
+ if (view) {
+ view.status = this.getStatus(node);
+ view.derivation = this.getDerivationTrail(node);
+ view.numDescendants = this.getSubtreeSize(node);
+ }
+ }
+
+ expandNode(nodeView: View.Node, focus: boolean = false, emit: boolean = true) {
nodeView.focus = focus;
nodeView.expanded = true;
nodeView.children = this.children(nodeView.value)
.map(node => this.createNode(node));
+ if (emit) this.emit('expand', nodeView);
}
expandOrNode(nodeView: View.Node, focus: boolean = false) {
this.expandNode(nodeView, focus);
for (let c of nodeView.children) {
if (c.value.tag == Data.NodeType.AndNode) {
- this.expandOrNode(c, focus);
+ this.expandNode(c, focus);
}
}
}
@@ -173,12 +288,14 @@ class ProofTrace {
}
expandAll(nodeView: View.Node = this.view.root) {
- this.expandNode(nodeView);
+ this.expandNode(nodeView, false, false);
for (let c of nodeView.children)
this.expandAll(c);
}
viewAction(ev: View.ActionEvent) {
+ if (ev.id !== this.id) return;
+
switch (ev.type) {
case 'expand':
this.expandOrNode(ev.target, true); break;
@@ -200,7 +317,8 @@ namespace ProofTrace {
export type Data = {
nodes: Data.NodeEntry[],
- statuses: Data.StatusEntry[]
+ statuses: Data.StatusEntry[],
+ trail: Data.DerivationTrailEntry[]
};
export namespace Data {
@@ -216,15 +334,28 @@ namespace ProofTrace {
export type NodeId = number[];
export enum NodeType { AndNode = 'AndNode', OrNode = 'OrNode' };
+ const NODE_TAGS = Object.values(NodeType);
export type GoalEntry = {
- id: string
- pre: string, post: string, sketch: string,
+ id: GoalId
+ uid: GoalUid
+ pre: AssertionEntry, post: AssertionEntry, sketch: string,
programVars: [string, string][]
existentials: [string, string][]
ghosts: [string, string][]
};
+ export type GoalId = string /* this is actually the label */
+ export type GoalUid = string
+
+ export type AssertionEntry = {
+ pp: String,
+ phi: AST[],
+ sigma: AST[]
+ };
+
+ export type AST = any /** @todo */
+
export type Environment = Map;
export type StatusEntry = {
@@ -234,15 +365,46 @@ namespace ProofTrace {
export type GoalStatusEntry = {tag: "Succeeded" | "Failed", from?: string | string[]};
+ export type DerivationTrailEntry = {
+ tag: "DerivationTrail"
+ from: GoalId
+ to: GoalId[]
+ ruleName: string
+ subst: {[metavar: string]: OrVec}
+ };
+ const DERIVATION_TRAIL_TAG = "DerivationTrail"
+
+ export type OrVec = T | T[];
+
+ export function empty() {
+ return {nodes: [], statuses: [], trail: []};
+ }
+
+ export function append(to: Data, from: Data): Data {
+ to.nodes.push(...from.nodes);
+ to.statuses.push(...from.statuses);
+ to.trail.push(...from.trail);
+ return to;
+ }
+
export function parse(traceText: string): Data {
- var entries = traceText.split('\n\n').filter(x => x).map(ln =>
- JSON.parse(ln));
- var nodes = [], statuses = [];
+ var entries = traceText.split('\n\n').filter(x => x)
+ .map(ln => JSON.parse(ln));
+ return fromEntries(entries);
+ }
+
+ export function fromEntries(entries: any[]): Data {
+ var nodes = [], statuses = [], trail = [];
for (let e of entries) {
- if (e.tag) nodes.push(e);
+ if (NODE_TAGS.includes(e.tag)) nodes.push(e);
+ else if (e.tag === DERIVATION_TRAIL_TAG) trail.push(e);
else if (e.status) statuses.push(e);
}
- return {nodes, statuses};
+ return {nodes, statuses, trail};
+ }
+
+ export function parentId(id: NodeId) {
+ return id.slice(1);
}
export function envOfGoal(goal: GoalEntry) {
@@ -262,17 +424,23 @@ namespace ProofTrace {
// View Part
// =========
export namespace View {
+
+ export type PaneProps = {docs: {[id: string]: {trace: Props}}};
+
+ export type Props = {root: View.Node};
export type Node = {
value: Data.NodeEntry
children: Node[]
numDescendants: number
- status: Data.GoalStatusEntry
+ status?: Data.GoalStatusEntry
+ derivation?: Data.DerivationTrailEntry
focus: boolean
expanded: boolean
};
export type ActionEvent = {
+ id?: string /* document id */
type: "expand" | "collapse" | "expandAll" | "menu"
| "copyNodeId" | "copyGoalId" | "copyGoal",
target: Node
@@ -294,9 +462,10 @@ namespace ProofTrace {
return {kind: 'whitespace', text: s};
else if (s.match(/^[(){}[\]]$/))
return {kind: 'brace', text: s};
- else if (mo = s.match(/^<(\w+)>$/)) {
+ else if (s === '<0>')
+ return {kind: 'null-cardinality', text: ''}
+ else if (mo = s.match(/^<(\w+)>$/))
return {kind: 'cardinality', text: s, pp: pprintIdentifier(mo[1])};
- }
else if (s != '')
return {kind: 'unknown', text: s};
})
@@ -315,7 +484,6 @@ import Data = ProofTrace.Data;
import View = ProofTrace.View;
-
abstract class KeyedMap {
_map: Map = new Map();
abstract key(k: K): K0;
@@ -332,229 +500,5 @@ class JSONMap extends KeyedMap {
}
-Vue.component('proof-trace-pane', {
- props: ['root'],
- data: () => ({options: {}, zoom: 1}),
- template: `
- `,
- methods: {
- toplevelAction(ev) {
- switch (ev.type) {
- case 'menu': this.$refs.contextMenu.open(ev); break;
- }
- this.$emit('action', ev);
- }
- }
-});
-
-Vue.component('proof-trace', {
- props: ['root'],
- data: () => ({statusClass: undefined}),
- template: `
- `,
- mounted() {
- this.$watch('root.expanded', () => {
- requestAnimationFrame(() => {
- if (this.root.focus && this.$refs.subtrees)
- this.focusElement(this.$refs.subtrees);
- });
- });
- if (this.$refs.nroot)
- this.statusClass = this.$refs.nroot.statusClass;
- },
- methods: {
- action(ev) { this.$emit('action', ev); },
- nodeAction(ev) {
- if (ev.type == 'expand/collapse') {
- this.root.expanded = !this.root.expanded;
- ev.type = this.root.expanded ? 'expand' : 'collapse';
- }
- this.action({...ev, target: this.root});
- },
- expandAll() { this.action({type: 'expandAll', target: this.root})},
- focusElement(el: HTMLElement) {
- var box = el.getBoundingClientRect(), clrse = 50,
- viewport = (window).visualViewport,
- v = (box.bottom + clrse) - viewport.height,
- hl = box.left - clrse - viewport.width * 0.33,
- hr = (box.right + clrse) - viewport.width,
- h = Math.min(hl, hr);
- window.scrollBy({left: Math.max(h, 0), top: Math.max(v, 0), behavior: 'smooth'});
- }
- }
-});
-
-Vue.component('proof-trace-node', {
- props: ['value', 'status', 'numDescendants'],
- data: () => ({_anchor: false}),
- template: `
-
-
- {{value.pp}}
- {{value.cost}}
- {{numDescendants}}
- {{value.goal.id}}
- {{tag}}
-
-
-
-
-
-
-
{{value.sketch}}
-
-
-
-
- {{v[0]}}
- {{pp(v[1])}}
-
-
-
`,
- methods: {
- pp: View.pprintIdentifier
- }
-});
-
-Vue.component('proof-trace-formula', {
- props: ['pp', 'env', 'css-class'],
- template: `
-
-
- {{token.pp || token.text}}
-
-
`,
- methods: {
- tokenize: View.tokenize
- }
-});
-
-Vue.component('proof-trace-toolbar', {
- props: {options: {default: () => ({})}},
- template: `
-
-
-
`
-});
-
-Vue.component('proof-trace-context-menu', {
- template: `
-
- Expand all
- Copy Node Id
- Copy goal
- `,
- components: {VueContext},
- methods: {
- open(ev: View.ActionEvent) {
- this._target = ev.target;
- this.$refs.m.open(ev.$event);
- },
- action(ev) {
- this.$emit('action', {
- type: ev.currentTarget.name,
- target: this._target
- });
- }
- }
-});
-
-
export { ProofTrace }
diff --git a/src/viz/tsconfig.json b/src/viz/tsconfig.json
index 971a287ed..a15e5ca86 100644
--- a/src/viz/tsconfig.json
+++ b/src/viz/tsconfig.json
@@ -2,6 +2,9 @@
"compilerOptions": {
"target": "es2019",
"moduleResolution": "node",
- "allowSyntheticDefaultImports": true
+ "allowSyntheticDefaultImports": true,
+ "esModuleInterop": true,
+ "downlevelIteration": true,
+ "experimentalDecorators": true
}
}
\ No newline at end of file
diff --git a/src/viz/vue/app-context-menu.vue b/src/viz/vue/app-context-menu.vue
new file mode 100644
index 000000000..ff932dcf2
--- /dev/null
+++ b/src/viz/vue/app-context-menu.vue
@@ -0,0 +1,28 @@
+
+
+ Expand all
+ Copy Node Id
+ Copy goal
+
+
+
+
diff --git a/src/viz/vue/app-toolbar.vue b/src/viz/vue/app-toolbar.vue
new file mode 100644
index 000000000..e46c99bd0
--- /dev/null
+++ b/src/viz/vue/app-toolbar.vue
@@ -0,0 +1,73 @@
+
+
+
+
+
+
+
diff --git a/src/viz/vue/app.vue b/src/viz/vue/app.vue
new file mode 100644
index 000000000..f20b2bc96
--- /dev/null
+++ b/src/viz/vue/app.vue
@@ -0,0 +1,48 @@
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/src/viz/vue/benchmark-list-pane.vue b/src/viz/vue/benchmark-list-pane.vue
new file mode 100644
index 000000000..c73f16b38
--- /dev/null
+++ b/src/viz/vue/benchmark-list-pane.vue
@@ -0,0 +1,85 @@
+
+
+
+
+
+
+
diff --git a/src/viz/vue/editor-pane.vue b/src/viz/vue/editor-pane.vue
new file mode 100644
index 000000000..7eaeecf22
--- /dev/null
+++ b/src/viz/vue/editor-pane.vue
@@ -0,0 +1,55 @@
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/src/viz/vue/proof-interaction.vue b/src/viz/vue/proof-interaction.vue
new file mode 100644
index 000000000..6e4d91fb9
--- /dev/null
+++ b/src/viz/vue/proof-interaction.vue
@@ -0,0 +1,34 @@
+
+
+
+
+
diff --git a/src/viz/vue/proof-trace-formula.vue b/src/viz/vue/proof-trace-formula.vue
new file mode 100644
index 000000000..448665828
--- /dev/null
+++ b/src/viz/vue/proof-trace-formula.vue
@@ -0,0 +1,20 @@
+
+
+
+ {{token.pp || token.text}}
+
+
+
+
+
diff --git a/src/viz/vue/proof-trace-goal.vue b/src/viz/vue/proof-trace-goal.vue
new file mode 100644
index 000000000..2011c201c
--- /dev/null
+++ b/src/viz/vue/proof-trace-goal.vue
@@ -0,0 +1,29 @@
+
+
+
+
+
+
+ ⤳
+
+
+ {{value.sketch}}
+
+
+
+
+ {{label}}
+
+
+ {{numDescendants}}
+ {{value.goal.id}}
+ {{tag}}
+
+
+
+
↖️{{value.goal.callGoal[0].id}}
+
+
+
+
+
+ {{v[0]}}
+ {{pp(v[1])}}
+
+
+
+
+
+
diff --git a/src/viz/vue/proof-trace.vue b/src/viz/vue/proof-trace.vue
new file mode 100644
index 000000000..3d555bafc
--- /dev/null
+++ b/src/viz/vue/proof-trace.vue
@@ -0,0 +1,87 @@
+
+
+
+
+
diff --git a/src/viz/vue/widgets/slider-switch.vue b/src/viz/vue/widgets/slider-switch.vue
new file mode 100644
index 000000000..4127c4d34
--- /dev/null
+++ b/src/viz/vue/widgets/slider-switch.vue
@@ -0,0 +1,80 @@
+
+
+
+
+
+
+
\ No newline at end of file