Skip to content

Commit b23971f

Browse files
caldwellbcaldwellb
authored
Merge pull request #24 from inQWIRE/feature-scale
Improved visualization and interactivity
2 parents 1ddd6c8 + 4f3dc53 commit b23971f

File tree

14 files changed

+638
-165
lines changed

14 files changed

+638
-165
lines changed

‎README.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,3 +35,4 @@ This extension contributes the following commands:
3535
- `vizx.lspRender`: to communicate with coq-lsp for automatic rendering. should not be used manually.
3636
- `vizx.activateRendering`: activates automatic rendering of goal state.
3737
- `vizx.deactivateRendering`: deactivates automatic rendering of goal state.
38+
- `vizx.lex`: debug tool to lex term without rendering

‎package-lock.json‎

Lines changed: 1 addition & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎package.json‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
"name": "vizx",
33
"displayName": "ZXViz",
44
"description": "Visualizer for the ZX calculus",
5-
"version": "0.2.0",
5+
"version": "0.2.1",
66
"repository": "https://github.com/inQWIRE/ViZX/",
77
"publisher": "inQWIRE",
88
"engines": {
@@ -25,6 +25,10 @@
2525
"command": "vizx.render",
2626
"title": "ZXViz: Render expressions with ZXViz"
2727
},
28+
{
29+
"command": "vizx.lex",
30+
"title": "ZXViz: Lex expression with ZXViz"
31+
},
2832
{
2933
"command": "vizx.lspRender",
3034
"title": "ZXViz: Render expressions with ZXViz using CoqLSP information"
@@ -88,6 +92,8 @@
8892
"deep-object-diff": "^1.1.9",
8993
"esbuild": "0.16.00",
9094
"esbuild-plugin-copy": "^2.0.2",
95+
"n": "^10.2.0",
96+
"stable": "^0.1.8",
9197
"typescript-parsec": "^0.3.2"
9298
}
9399
}

‎src/constants/consts.ts‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,9 @@ export const COMPOSE_OP = "⟷"; //\longleftrightarrow
1010
export const STACK_OP = "↕"; // \updownarrow
1111
export const N_STACK_1_OP = "↑";
1212

13+
export const SCALE_OP = ".*";
14+
// export const ZX_PLUS_OP = ".+";
15+
1316
export const PROP_TO = "∝";
1417
export const EQ = "=";
1518
export const CAP = "⊂";

‎src/constants/variableconsts.ts‎

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,15 @@ export function changeScale(scale: number) {
33
LINE_WIDTH = scale / 200;
44
BASE_SIZE = 1 * scale;
55
PAD_SIZE = 0.1 * scale;
6-
PROPTO_SIZE = 0.2 * scale;
6+
PROPTO_SIZE = 0.1 * scale;
77
CAST_SIZE = 0.3 * scale;
88
TEXT_PAD_SIZE = 0.08 * scale;
99
DOTS_PAD_SIZE = 0.1 * scale;
1010
FUNC_ARG_SIZE = 0.7 * scale;
1111
REALLY_SMALL_TEXT = (scale / 15).toString().concat("px");
1212
SMALL_TEXT = (scale / 10).toString().concat("px");
1313
MEDIUM_TEXT = (scale / 7).toString().concat("px");
14+
MEDIUM_LARGE_TEXT = (scale / 4).toString().concat("px");
1415
LARGE_TEXT = (scale / 2).toString().concat("px");
1516
MONOSPACE_FONT = "Monospace";
1617
ARIAL_FONT = "Arial";
@@ -26,6 +27,11 @@ export function changeScale(scale: number) {
2627
export let CANVAS_WIDTH = 100;
2728
export let CANVAS_HEIGHT = 100;
2829

30+
export let LHS_CANVAS_WIDTH = 100;
31+
export let LHS_CANVAS_HEIGHT = 100;
32+
export let RHS_CANVAS_WIDTH = 100;
33+
export let RHS_CANVAS_HEIGHT = 100;
34+
2935
// SCALE = size of base square, ideally do not go below 100 or it'll be too small
3036
export let SCALE: number;
3137
export let LINE_WIDTH: number;
@@ -39,6 +45,7 @@ export let FUNC_ARG_SIZE: number;
3945
export let REALLY_SMALL_TEXT: string;
4046
export let SMALL_TEXT: string;
4147
export let MEDIUM_TEXT: string;
48+
export let MEDIUM_LARGE_TEXT: string;
4249
export let LARGE_TEXT: string;
4350
export let MONOSPACE_FONT: string;
4451
export let ARIAL_FONT: string;
@@ -93,6 +100,17 @@ export function setCanvasWidthHeight(wh: [number, number]) {
93100
};
94101
}
95102

103+
export function setLHSCanvasWidthHeight(wh: [number, number]) {
104+
LHS_CANVAS_WIDTH = wh[0] + 2 * HOR_PAD;
105+
LHS_CANVAS_HEIGHT = wh[1] + 2 * VER_PAD;
106+
}
107+
108+
export function setRHSCanvasWidthHeight(wh: [number, number]) {
109+
RHS_CANVAS_WIDTH = wh[0] + 2 * HOR_PAD;
110+
RHS_CANVAS_HEIGHT = wh[1] + 2 * VER_PAD;
111+
}
112+
113+
96114
export let COLOR_DICT: string[] = ["#FFFFFF"];
97115
// export let COLOR_DICT : string[] = [
98116
// "#d0d6e4",

‎src/extension.ts‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
import * as vscode from "vscode";
44
import { coqLspApi, only_with_lsp } from "./lspguards";
55
import { render, renderCallback } from "./rendering/callback";
6+
import { lexer, lexerPrettyPrinter, lexerPrettyPrinter_string } from "./parsing/lexer";
67

78
let history: string[] = [];
89
const HISTORY_LENGTH = vscode.workspace
@@ -26,6 +27,12 @@ export function activate(context: vscode.ExtensionContext) {
2627
renderCommand(context)
2728
),
2829
];
30+
31+
disposables.push(
32+
vscode.commands.registerCommand("vizx.lex", () =>
33+
lexCommand(context)
34+
)
35+
);
2936

3037
disposables.push(
3138
vscode.commands.registerCommand("vizx.lspRender", (expr) =>
@@ -43,6 +50,7 @@ export function activate(context: vscode.ExtensionContext) {
4350
deactivateRenderingCommand()
4451
)
4552
);
53+
4654
context.subscriptions.push(...disposables);
4755

4856
const config = vscode.workspace.getConfiguration("vizx");
@@ -108,6 +116,21 @@ function renderCommand(context: vscode.ExtensionContext): void {
108116
});
109117
}
110118

119+
function lexCommand(context: vscode.ExtensionContext): void {
120+
vscode.window
121+
.showInputBox({ prompt: "Enter diagram syntax with notations" })
122+
.then((value) => {
123+
if (value) {
124+
vscode.window
125+
.showInformationMessage(
126+
"Parsed expression: " + lexerPrettyPrinter_string(value),
127+
"Ok"
128+
)
129+
}
130+
}).then((selection) => {})
131+
return;
132+
}
133+
111134
function activateRenderingCommand(context: vscode.ExtensionContext): void {
112135
const config = vscode.workspace.getConfiguration("vizx");
113136
const enabled = config.get<boolean>("enableAutomaticRendering", false);

‎src/parsing/ast.ts‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -87,6 +87,21 @@ export interface ASTCompose extends ASTNode {
8787
index: number;
8888
}
8989

90+
// export interface ASTPlus extends ASTNode {
91+
// kind: "plus";
92+
// left: ASTNode;
93+
// right: ASTNode;
94+
// index: number;
95+
// }
96+
97+
export interface ASTScale extends ASTNode {
98+
kind: "scale";
99+
coefficient: Num;
100+
// width: number;
101+
node: ASTNode;
102+
index: number;
103+
}
104+
90105
export interface ASTNStack extends ASTNode {
91106
kind: "nstack";
92107
n: Num;

‎src/parsing/coords.ts‎

Lines changed: 65 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,14 @@
11
import * as ast from "./ast";
2-
import { NUMBER_KINDS } from "../constants/consts";
2+
import { NUMBER_KINDS, SCALE_OP } from "../constants/consts";
33
import {
44
FUNC_ARG_SIZE,
55
CAST_SIZE,
66
PAD_SIZE,
7+
PROPTO_SIZE
78
} from "../constants/variableconsts";
89
import { quad, coord } from "../constants/types";
10+
import { mainModule } from "process";
11+
import { createContext } from "vm";
912

1013
export function findCenter(q: quad): coord {
1114
return {
@@ -67,7 +70,7 @@ export function makeAtCenter(
6770
};
6871
}
6972

70-
export function addCoords(node: ast.ASTNode, boundary: quad): ast.ASTNode {
73+
export function addCoords(node: ast.ASTNode, boundary: quad, preboxed:Boolean = false): ast.ASTNode {
7174
switch (node.kind) {
7275
case "transform": {
7376
let node_ = <ast.ASTTransform>node;
@@ -85,7 +88,29 @@ export function addCoords(node: ast.ASTNode, boundary: quad): ast.ASTNode {
8588
bound.bl.y -= PAD_SIZE;
8689
bound.br.x -= PAD_SIZE;
8790
bound.br.y -= PAD_SIZE;
88-
node_.node = addCoords(node_.node, bound);
91+
node_.node = addCoords(node_.node, bound, true);
92+
return node_;
93+
}
94+
case "scale": {
95+
let node_ = <ast.ASTScale>node;
96+
node_.boundary = makeAtCenter(
97+
findCenter(boundary),
98+
node.hor_len!,
99+
node.ver_len!
100+
);
101+
let size = Math.max(0.2 * CAST_SIZE * (node_.coefficient.expr.length + 3) + PAD_SIZE,
102+
FUNC_ARG_SIZE);
103+
104+
let bound: quad = JSON.parse(JSON.stringify(boundary));
105+
bound.tl.x += PAD_SIZE + size;
106+
bound.tl.y += PAD_SIZE;
107+
bound.tr.x -= PAD_SIZE;
108+
bound.tr.y += PAD_SIZE;
109+
bound.bl.x += PAD_SIZE + size;
110+
bound.bl.y -= PAD_SIZE;
111+
bound.br.x -= PAD_SIZE;
112+
bound.br.y -= PAD_SIZE;
113+
node_.node = addCoords(node_.node, bound, true);
89114
return node_;
90115
}
91116
case "const": {
@@ -130,41 +155,42 @@ export function addCoords(node: ast.ASTNode, boundary: quad): ast.ASTNode {
130155
node.ver_len!
131156
);
132157
// console.log("stack node bound: ", node_.boundary);
158+
let ADJ_SIZE = preboxed ? 0 : PAD_SIZE;
133159
let l_bound = {
134160
tl: {
135-
x: node_.boundary.tl.x + PAD_SIZE,
136-
y: node_.boundary.tl.y + PAD_SIZE,
161+
x: node_.boundary.tl.x + ADJ_SIZE,
162+
y: node_.boundary.tl.y + ADJ_SIZE,
137163
},
138164
tr: {
139-
x: node_.boundary.tr.x - PAD_SIZE,
140-
y: node_.boundary.tr.y + PAD_SIZE,
165+
x: node_.boundary.tr.x - ADJ_SIZE,
166+
y: node_.boundary.tr.y + ADJ_SIZE,
141167
},
142168
bl: {
143-
x: node_.boundary.tl.x + PAD_SIZE,
144-
y: node_.boundary.tl.y + l_ver + PAD_SIZE,
169+
x: node_.boundary.tl.x + ADJ_SIZE,
170+
y: node_.boundary.tl.y + l_ver + ADJ_SIZE,
145171
},
146172
br: {
147-
x: node_.boundary.tr.x - PAD_SIZE,
148-
y: node_.boundary.tr.y + l_ver + PAD_SIZE,
173+
x: node_.boundary.tr.x - ADJ_SIZE,
174+
y: node_.boundary.tr.y + l_ver + ADJ_SIZE,
149175
},
150176
} as quad;
151177
// console.log("l_bound: ", l_bound);
152178
let r_bound = {
153179
bl: {
154-
x: node_.boundary.bl.x + PAD_SIZE,
155-
y: node_.boundary.bl.y - PAD_SIZE,
180+
x: node_.boundary.bl.x + ADJ_SIZE,
181+
y: node_.boundary.bl.y - ADJ_SIZE,
156182
},
157183
br: {
158-
x: node_.boundary.br.x - PAD_SIZE,
159-
y: node_.boundary.br.y - PAD_SIZE,
184+
x: node_.boundary.br.x - ADJ_SIZE,
185+
y: node_.boundary.br.y - ADJ_SIZE,
160186
},
161187
tl: {
162-
x: node_.boundary.tl.x + PAD_SIZE,
163-
y: node_.boundary.bl.y - r_ver - PAD_SIZE,
188+
x: node_.boundary.tl.x + ADJ_SIZE,
189+
y: node_.boundary.bl.y - r_ver - ADJ_SIZE,
164190
},
165191
tr: {
166-
x: node_.boundary.tr.x - PAD_SIZE,
167-
y: node_.boundary.br.y - r_ver - PAD_SIZE,
192+
x: node_.boundary.tr.x - ADJ_SIZE,
193+
y: node_.boundary.br.y - r_ver - ADJ_SIZE,
168194
},
169195
} as quad;
170196
// console.log("r_bound: ", r_bound);
@@ -181,41 +207,42 @@ export function addCoords(node: ast.ASTNode, boundary: quad): ast.ASTNode {
181207
node.hor_len!,
182208
node.ver_len!
183209
);
210+
let ADJ_SIZE = preboxed ? 0 : PAD_SIZE;
184211
let l_bound = {
185212
tl: {
186-
x: node_.boundary.tl.x + PAD_SIZE,
187-
y: node_.boundary.tl.y + PAD_SIZE,
213+
x: node_.boundary.tl.x + ADJ_SIZE,
214+
y: node_.boundary.tl.y + ADJ_SIZE,
188215
},
189216
tr: {
190-
x: node_.boundary.tl.x + l_hor + PAD_SIZE,
191-
y: node_.boundary.tl.y + PAD_SIZE,
217+
x: node_.boundary.tl.x + l_hor + ADJ_SIZE,
218+
y: node_.boundary.tl.y + ADJ_SIZE,
192219
},
193220
bl: {
194-
x: node_.boundary.bl.x + PAD_SIZE,
195-
y: node_.boundary.bl.y - PAD_SIZE,
221+
x: node_.boundary.bl.x + ADJ_SIZE,
222+
y: node_.boundary.bl.y - ADJ_SIZE,
196223
},
197224
br: {
198-
x: node_.boundary.tl.x + l_hor + PAD_SIZE,
199-
y: node_.boundary.bl.y - PAD_SIZE,
225+
x: node_.boundary.tl.x + l_hor + ADJ_SIZE,
226+
y: node_.boundary.bl.y - ADJ_SIZE,
200227
},
201228
} as quad;
202229
// console.log("l_bound: ", l_bound);
203230
let r_bound = {
204231
tl: {
205-
x: node_.boundary.tr.x - r_hor - PAD_SIZE,
206-
y: node_.boundary.tr.y + PAD_SIZE,
232+
x: node_.boundary.tr.x - r_hor - ADJ_SIZE,
233+
y: node_.boundary.tr.y + ADJ_SIZE,
207234
},
208235
tr: {
209-
x: node_.boundary.tr.x - PAD_SIZE,
210-
y: node_.boundary.tr.y + PAD_SIZE,
236+
x: node_.boundary.tr.x - ADJ_SIZE,
237+
y: node_.boundary.tr.y + ADJ_SIZE,
211238
},
212239
bl: {
213-
x: node_.boundary.br.x - r_hor - PAD_SIZE,
214-
y: node_.boundary.bl.y - PAD_SIZE,
240+
x: node_.boundary.br.x - r_hor - ADJ_SIZE,
241+
y: node_.boundary.bl.y - ADJ_SIZE,
215242
},
216243
br: {
217-
x: node_.boundary.br.x - PAD_SIZE,
218-
y: node_.boundary.br.y - PAD_SIZE,
244+
x: node_.boundary.br.x - ADJ_SIZE,
245+
y: node_.boundary.br.y - ADJ_SIZE,
219246
},
220247
} as quad;
221248
// console.log("r_bound: ", r_bound);
@@ -309,7 +336,7 @@ export function addCoords(node: ast.ASTNode, boundary: quad): ast.ASTNode {
309336
bound.bl.y -= PAD_SIZE;
310337
bound.br.x -= CAST_SIZE;
311338
bound.br.y -= PAD_SIZE;
312-
node_.node = addCoords(node_.node, bound);
339+
node_.node = addCoords(node_.node, bound, true);
313340
return node_;
314341
}
315342
case "function": {
@@ -392,8 +419,8 @@ export function addCoords(node: ast.ASTNode, boundary: quad): ast.ASTNode {
392419
y: node_.boundary.br.y - PAD_SIZE,
393420
},
394421
} as quad;
395-
node_.l = addCoords(node_.l, l_bound);
396-
node_.r = addCoords(node_.r, r_bound);
422+
node_.l = addCoords(node_.l, l_bound, true);
423+
node_.r = addCoords(node_.r, r_bound, true);
397424
return node_;
398425
}
399426
default: {

0 commit comments

Comments
 (0)