Basis support for inspecting types

This commit is contained in:
Ayaz Hafiz 2023-07-16 20:39:27 -05:00
parent 8b7823a237
commit 9e055dcf53
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
8 changed files with 753 additions and 7 deletions

View file

@ -17,6 +17,7 @@
"@types/node": "^16.18.38",
"@types/react": "^18.2.15",
"@types/react-dom": "^18.2.7",
"clsx": "^2.0.0",
"json-schema-to-typescript": "^13.0.2",
"react-scripts": "5.0.1",
"tailwindcss": "^3.3.3",
@ -5953,6 +5954,15 @@
"wrap-ansi": "^7.0.0"
}
},
"node_modules/clsx": {
"version": "2.0.0",
"resolved": "https://registry.npmjs.org/clsx/-/clsx-2.0.0.tgz",
"integrity": "sha512-rQ1+kcj+ttHG0MKVGBUXwayCCF1oh39BF5COIpRzuCEv8Mwjv0XucrI2ExNTOn9IlLifGClWQcU9BrZORvtw6Q==",
"dev": true,
"engines": {
"node": ">=6"
}
},
"node_modules/co": {
"version": "4.6.0",
"resolved": "https://registry.npmjs.org/co/-/co-4.6.0.tgz",

View file

@ -37,6 +37,7 @@
"@types/node": "^16.18.38",
"@types/react": "^18.2.15",
"@types/react-dom": "^18.2.7",
"clsx": "^2.0.0",
"json-schema-to-typescript": "^13.0.2",
"react-scripts": "5.0.1",
"tailwindcss": "^3.3.3",

View file

@ -1,13 +1,35 @@
import React from "react";
import FileInput, { LoadedEvents } from "./components/FileInput";
import Ui from "./components/Ui";
import data from "./checkmate.json";
import { AllEvents } from "./schema";
export default function App() {
const [events, setEvents] = React.useState<LoadedEvents | null>({
kind: "ok",
events: data as AllEvents,
});
return (
<div className="App">
<header className="App-header">
<p>
Edit <code>src/App.tsx</code> and save to reload.
</p>
</header>
<div className="container w-screen h-screen p-2">
<FileInput setResult={setEvents} />
<EventsWrapper events={events} />
</div>
);
}
interface EventsWrapperProps {
events: LoadedEvents | null;
}
function EventsWrapper({ events }: EventsWrapperProps): JSX.Element {
if (events === null) {
return <div></div>;
}
switch (events.kind) {
case "ok":
return <Ui events={events.events} />;
case "err":
return <div className="text-red-400 text-lg">{events.error}</div>;
}
}

View file

@ -0,0 +1,545 @@
[
{
"type": "Unification",
"left": 1540,
"right": 71,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 71,
"rank": 1,
"content": {
"type": "Function",
"arguments": [1543, 1544],
"lambda_type": 1542,
"ret": 1541
}
},
{ "type": "VariableUnified", "from": 1540, "to": 71 },
{ "type": "VariableUnified", "from": 71, "to": 71 }
]
},
{
"type": "Unification",
"left": 71,
"right": 1546,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "Unification",
"left": 1543,
"right": 67,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 67,
"rank": 1,
"content": {
"type": "Alias",
"name": "`Num.Num`",
"variables": {
"type_variables": [1545],
"lambda_set_variables": [],
"infer_ext_in_output_position_variables": []
},
"real_variable": 1545,
"kind": { "type": "Opaque" }
}
},
{ "type": "VariableUnified", "from": 1543, "to": 67 },
{ "type": "VariableUnified", "from": 67, "to": 67 }
]
},
{
"type": "Unification",
"left": 1544,
"right": 69,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 69,
"rank": 1,
"content": {
"type": "Alias",
"name": "`Num.Num`",
"variables": {
"type_variables": [1545],
"lambda_set_variables": [],
"infer_ext_in_output_position_variables": []
},
"real_variable": 1545,
"kind": { "type": "Opaque" }
}
},
{ "type": "VariableUnified", "from": 1544, "to": 69 },
{ "type": "VariableUnified", "from": 69, "to": 69 }
]
},
{
"type": "Unification",
"left": 1541,
"right": 73,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 73,
"rank": 1,
"content": {
"type": "Alias",
"name": "`Num.Num`",
"variables": {
"type_variables": [1545],
"lambda_set_variables": [],
"infer_ext_in_output_position_variables": []
},
"real_variable": 1545,
"kind": { "type": "Opaque" }
}
},
{ "type": "VariableUnified", "from": 1541, "to": 73 },
{ "type": "VariableUnified", "from": 73, "to": 73 }
]
},
{
"type": "Unification",
"left": 1542,
"right": 72,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 72,
"rank": 1,
"content": {
"type": "LambdaSet",
"solved": [{ "function": "`Num.add`", "environment": [] }],
"unspecialized": [],
"recursion_var": null,
"ambient_function": 1540
}
},
{ "type": "VariableUnified", "from": 1542, "to": 72 },
{ "type": "VariableUnified", "from": 72, "to": 72 }
]
},
{
"type": "VariableSetDescriptor",
"variable": 1546,
"rank": 1,
"content": {
"type": "Function",
"arguments": [67, 69],
"lambda_type": 1542,
"ret": 73
}
},
{ "type": "VariableUnified", "from": 71, "to": 1546 },
{ "type": "VariableUnified", "from": 1546, "to": 1546 }
]
},
{
"type": "Unification",
"left": 66,
"right": 1547,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 1547,
"rank": 1,
"content": {
"type": "RangedNumber",
"range": {
"kind": { "type": "AnyNum" },
"signed": true,
"min_width": 8
}
}
},
{ "type": "VariableUnified", "from": 66, "to": 1547 },
{ "type": "VariableUnified", "from": 1547, "to": 1547 }
]
},
{
"type": "Unification",
"left": 1548,
"right": 67,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "Unification",
"left": 66,
"right": 1545,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 1545,
"rank": 1,
"content": {
"type": "RangedNumber",
"range": {
"kind": { "type": "AnyNum" },
"signed": true,
"min_width": 8
}
}
},
{ "type": "VariableUnified", "from": 1547, "to": 1545 },
{ "type": "VariableUnified", "from": 1545, "to": 1545 }
]
},
{
"type": "VariableSetDescriptor",
"variable": 67,
"rank": 1,
"content": {
"type": "Alias",
"name": "`Num.Num`",
"variables": {
"type_variables": [66],
"lambda_set_variables": [],
"infer_ext_in_output_position_variables": []
},
"real_variable": 66,
"kind": { "type": "Opaque" }
}
},
{ "type": "VariableUnified", "from": 1548, "to": 67 },
{ "type": "VariableUnified", "from": 67, "to": 67 }
]
},
{
"type": "Unification",
"left": 68,
"right": 1549,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 1549,
"rank": 1,
"content": {
"type": "RangedNumber",
"range": {
"kind": { "type": "AnyNum" },
"signed": true,
"min_width": 8
}
}
},
{ "type": "VariableUnified", "from": 68, "to": 1549 },
{ "type": "VariableUnified", "from": 1549, "to": 1549 }
]
},
{
"type": "Unification",
"left": 1550,
"right": 69,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "Unification",
"left": 68,
"right": 1545,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 1545,
"rank": 1,
"content": {
"type": "RangedNumber",
"range": {
"kind": { "type": "AnyNum" },
"signed": true,
"min_width": 8
}
}
},
{ "type": "VariableUnified", "from": 1549, "to": 1545 },
{ "type": "VariableUnified", "from": 1545, "to": 1545 }
]
},
{
"type": "VariableSetDescriptor",
"variable": 69,
"rank": 1,
"content": {
"type": "Alias",
"name": "`Num.Num`",
"variables": {
"type_variables": [68],
"lambda_set_variables": [],
"infer_ext_in_output_position_variables": []
},
"real_variable": 68,
"kind": { "type": "Opaque" }
}
},
{ "type": "VariableUnified", "from": 1550, "to": 69 },
{ "type": "VariableUnified", "from": 69, "to": 69 }
]
},
{
"type": "Unification",
"left": 73,
"right": 1551,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "Unification",
"left": 73,
"right": 1552,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "Unification",
"left": 1545,
"right": 1553,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "Unification",
"left": 1556,
"right": 1554,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 1554,
"rank": 1,
"content": {
"type": "Alias",
"name": "`Num.Unsigned8`",
"variables": {
"type_variables": [],
"lambda_set_variables": [],
"infer_ext_in_output_position_variables": []
},
"real_variable": 1555,
"kind": { "type": "Opaque" }
}
},
{ "type": "VariableUnified", "from": 1556, "to": 1554 },
{ "type": "VariableUnified", "from": 1554, "to": 1554 }
]
}
]
},
{
"type": "Unification",
"left": 1545,
"right": 1553,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 1553,
"rank": 1,
"content": {
"type": "Alias",
"name": "`Num.Integer`",
"variables": {
"type_variables": [1556],
"lambda_set_variables": [],
"infer_ext_in_output_position_variables": []
},
"real_variable": 1556,
"kind": { "type": "Opaque" }
}
},
{ "type": "VariableUnified", "from": 1545, "to": 1553 },
{ "type": "VariableUnified", "from": 1553, "to": 1553 }
]
},
{
"type": "VariableSetDescriptor",
"variable": 1552,
"rank": 1,
"content": {
"type": "Alias",
"name": "`Num.Num`",
"variables": {
"type_variables": [1545],
"lambda_set_variables": [],
"infer_ext_in_output_position_variables": []
},
"real_variable": 1545,
"kind": { "type": "Opaque" }
}
},
{ "type": "VariableUnified", "from": 73, "to": 1552 },
{ "type": "VariableUnified", "from": 1552, "to": 1552 }
]
}
]
},
{
"type": "Unification",
"left": 1551,
"right": 75,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 75,
"rank": 1,
"content": {
"type": "Alias",
"name": "`Num.U8`",
"variables": {
"type_variables": [],
"lambda_set_variables": [],
"infer_ext_in_output_position_variables": []
},
"real_variable": 1552,
"kind": { "type": "Structural" }
}
},
{ "type": "VariableUnified", "from": 1551, "to": 75 },
{ "type": "VariableUnified", "from": 75, "to": 75 }
]
},
{
"type": "Unification",
"left": 80,
"right": 75,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 75,
"rank": 1,
"content": {
"type": "Alias",
"name": "`Num.U8`",
"variables": {
"type_variables": [],
"lambda_set_variables": [],
"infer_ext_in_output_position_variables": []
},
"real_variable": 1552,
"kind": { "type": "Structural" }
}
},
{ "type": "VariableUnified", "from": 80, "to": 75 },
{ "type": "VariableUnified", "from": 75, "to": 75 }
]
},
{
"type": "Unification",
"left": 1557,
"right": 79,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 79,
"rank": 1,
"content": {
"type": "Alias",
"name": "`Bool.Bool`",
"variables": {
"type_variables": [],
"lambda_set_variables": [],
"infer_ext_in_output_position_variables": []
},
"real_variable": 1558,
"kind": { "type": "Opaque" }
}
},
{ "type": "VariableUnified", "from": 1557, "to": 79 },
{ "type": "VariableUnified", "from": 79, "to": 79 }
]
},
{
"type": "Unification",
"left": 79,
"right": 5,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "Unification",
"left": 1558,
"right": 4,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "Unification",
"left": 84,
"right": 3,
"mode": { "type": "Eq" },
"success": true,
"subevents": [
{
"type": "VariableSetDescriptor",
"variable": 3,
"rank": 0,
"content": { "type": "EmptyTagUnion" }
},
{ "type": "VariableUnified", "from": 84, "to": 3 },
{ "type": "VariableUnified", "from": 3, "to": 3 }
]
},
{
"type": "VariableSetDescriptor",
"variable": 4,
"rank": 0,
"content": {
"type": "TagUnion",
"tags": { "False": [], "True": [] },
"extension": { "type": "Any", "variable": 84 }
}
},
{ "type": "VariableUnified", "from": 1558, "to": 4 },
{ "type": "VariableUnified", "from": 4, "to": 4 }
]
},
{
"type": "VariableSetDescriptor",
"variable": 5,
"rank": 0,
"content": {
"type": "Alias",
"name": "`Bool.Bool`",
"variables": {
"type_variables": [],
"lambda_set_variables": [],
"infer_ext_in_output_position_variables": []
},
"real_variable": 1558,
"kind": { "type": "Opaque" }
}
},
{ "type": "VariableUnified", "from": 79, "to": 5 },
{ "type": "VariableUnified", "from": 5, "to": 5 }
]
}
]

View file

@ -0,0 +1,53 @@
import { AllEvents } from "../schema";
export type EventsOk = {
kind: "ok";
events: AllEvents;
};
export type EventsErr = {
kind: "err";
error: string;
};
export type LoadedEvents = EventsOk | EventsErr;
interface FileInputProps {
setResult(result: LoadedEvents): void;
}
export default function FileInput({ setResult }: FileInputProps) {
async function setFile(e: React.ChangeEvent<HTMLInputElement>) {
e.preventDefault();
const files = e.target.files;
if (!files) {
setResult({ kind: "err", error: "Please choose a checkmate file." });
return;
}
const file = files[0];
const buf = await file.arrayBuffer();
try {
const events: AllEvents = JSON.parse(new TextDecoder().decode(buf));
setResult({ kind: "ok", events });
} catch (e) {
setResult({ kind: "err", error: "Invalid checkmate file." });
return;
}
}
return (
<div>
<label htmlFor="small-file-input" className="sr-only">
Choose file
</label>
<input
type="file"
name="small-file-input"
id="small-file-input"
onChange={(e) => setFile(e)}
className="block w-full border border-gray-200 shadow-sm rounded-md text-sm
file:bg-roc-purple-bg file:border-0 file:mr-4 file:py-2 file:px-4"
></input>
</div>
);
}

View file

@ -0,0 +1,107 @@
import React from "react";
import { AllEvents, Event, UnificationMode } from "../schema";
import { Refine } from "../utils/refine";
import clsx from "clsx";
interface UiProps {
events: AllEvents;
}
export default function Ui({ events }: UiProps): JSX.Element {
return (
<div className="font-mono">
<EventList root events={events}></EventList>
</div>
);
}
interface EventListProps {
events: Event[];
root?: boolean;
}
function EventList({ events, root }: EventListProps): JSX.Element {
return (
<ul className={clsx(root ? "ml-2 mt-4" : "ml-[1.5em]", "relative")}>
{events.map((event, i) => (
<li key={i} className="mt-2">
<OneEvent event={event} />
</li>
))}
</ul>
);
}
interface OneEventProps {
event: Event;
}
function OneEvent({ event }: OneEventProps): JSX.Element {
switch (event.type) {
case "Unification":
return <Unification event={event} />;
case "VariableUnified":
return <></>;
case "VariableSetDescriptor":
return <></>;
}
}
const DROPDOWN_CLOSED = "▶";
const DROPDOWN_OPEN = "▼";
const UN_UNKNOWN = "❔";
const UN_SUCCESS = "✅";
const UN_FAILURE = "❌";
function Unification({
event,
}: {
event: Refine<Event, "Unification">;
}): JSX.Element {
const { left, right, mode, subevents, success } = event;
const [isOpen, setIsOpen] = React.useState(false);
const result = success ? UN_SUCCESS : UN_FAILURE;
const modeIcon = <UnificationModeIcon mode={mode} />;
const dropdownIcon = isOpen ? DROPDOWN_OPEN : DROPDOWN_CLOSED;
const headLineIcon = isOpen ? UN_UNKNOWN : result;
const headLine = (
<button onClick={() => setIsOpen(!isOpen)} className="w-full text-left">
<span className="text-slate-400 mr-2">{dropdownIcon}</span>
{headLineIcon} {left} {modeIcon} {right}
</button>
);
if (!isOpen) {
return <div className="opacity-60">{headLine}</div>;
} else {
const dropdownTransparent = (
<span className="text-transparent mr-2">{dropdownIcon}</span>
);
return (
<div>
<div>{headLine}</div>
<EventList events={subevents} />
<div className="mt-2">
{dropdownTransparent}
{result} {left} {modeIcon} {right}
</div>
</div>
);
}
}
function UnificationModeIcon({ mode }: { mode: UnificationMode }): JSX.Element {
switch (mode.type) {
case "Eq":
return <>~</>;
case "Present":
return <>+=</>;
case "LambdaSetSpecialization":
return <>|~|</>;
}
}

View file

@ -0,0 +1,3 @@
export type Refine<T extends { type: string }, Type extends string> = T & {
type: Type;
};

View file

@ -5,7 +5,12 @@ module.exports = {
"./src/**/*.{js,jsx,ts,tsx}",
],
theme: {
extend: {},
extend: {
colors: {
'roc-purple': '#7c38f5',
'roc-purple-bg': '#ece2fd',
},
},
},
plugins: [],
}