mirror of
https://github.com/roc-lang/roc.git
synced 2025-08-04 12:18:19 +00:00
Support viewing multiple epochs
This commit is contained in:
Ayaz Hafiz
parent
f3c0b54fe9
commit
66b6b8b53d
12 changed files with 672 additions and 369 deletions
41
crates/compiler/checkmate/www/package-lock.json
generated
41
crates/compiler/checkmate/www/package-lock.json
generated
|
|
@ -14,6 +14,7 @@
|
|||
"react-dom": "^18.2.0",
|
||||
"react-router-dom": "^6.14.2",
|
||||
"react-router-hash-link": "^2.4.3",
|
||||
"react-tooltip": "^5.19.0",
|
||||
"reactflow": "^11.7.4"
|
||||
},
|
||||
"devDependencies": {
|
||||
|
|
@ -2621,6 +2622,28 @@
|
|||
"node": "^12.22.0 || ^14.17.0 || >=16.0.0"
|
||||
}
|
||||
},
|
||||
"node_modules/@floating-ui/core": {
|
||||
"version": "1.4.1",
|
||||
"resolved": "https://registry.npmjs.org/@floating-ui/core/-/core-1.4.1.tgz",
|
||||
"integrity": "sha512-jk3WqquEJRlcyu7997NtR5PibI+y5bi+LS3hPmguVClypenMsCY3CBa3LAQnozRCtCrYWSEtAdiskpamuJRFOQ==",
|
||||
"dependencies": {
|
||||
"@floating-ui/utils": "^0.1.1"
|
||||
}
|
||||
},
|
||||
"node_modules/@floating-ui/dom": {
|
||||
"version": "1.5.1",
|
||||
"resolved": "https://registry.npmjs.org/@floating-ui/dom/-/dom-1.5.1.tgz",
|
||||
"integrity": "sha512-KwvVcPSXg6mQygvA1TjbN/gh///36kKtllIF8SUm0qpFj8+rvYrpvlYdL1JoA71SHpDqgSSdGOSoQ0Mp3uY5aw==",
|
||||
"dependencies": {
|
||||
"@floating-ui/core": "^1.4.1",
|
||||
"@floating-ui/utils": "^0.1.1"
|
||||
}
|
||||
},
|
||||
"node_modules/@floating-ui/utils": {
|
||||
"version": "0.1.1",
|
||||
"resolved": "https://registry.npmjs.org/@floating-ui/utils/-/utils-0.1.1.tgz",
|
||||
"integrity": "sha512-m0G6wlnhm/AX0H12IOWtK8gASEMffnX08RtKkCgTdHb9JpHKGloI7icFfLg9ZmQeavcvR0PKmzxClyuFPSjKWw=="
|
||||
},
|
||||
"node_modules/@humanwhocodes/config-array": {
|
||||
"version": "0.11.10",
|
||||
"resolved": "https://registry.npmjs.org/@humanwhocodes/config-array/-/config-array-0.11.10.tgz",
|
||||
|
|
@ -6303,6 +6326,11 @@
|
|||
"resolved": "https://registry.npmjs.org/classcat/-/classcat-5.0.4.tgz",
|
||||
"integrity": "sha512-sbpkOw6z413p+HDGcBENe498WM9woqWHiJxCq7nvmxe9WmrUmqfAcxpIwAiMtM5Q3AhYkzXcNQHqsWq0mND51g=="
|
||||
},
|
||||
"node_modules/classnames": {
|
||||
"version": "2.3.2",
|
||||
"resolved": "https://registry.npmjs.org/classnames/-/classnames-2.3.2.tgz",
|
||||
"integrity": "sha512-CSbhY4cFEJRe6/GQzIk5qXZ4Jeg5pcsP7b5peFSDpffpe1cqjASH/n9UTjBwOp6XpMSTwQ8Za2K5V02ueA7Tmw=="
|
||||
},
|
||||
"node_modules/clean-css": {
|
||||
"version": "5.3.2",
|
||||
"resolved": "https://registry.npmjs.org/clean-css/-/clean-css-5.3.2.tgz",
|
||||
|
|
@ -15911,6 +15939,19 @@
|
|||
}
|
||||
}
|
||||
},
|
||||
"node_modules/react-tooltip": {
|
||||
"version": "5.19.0",
|
||||
"resolved": "https://registry.npmjs.org/react-tooltip/-/react-tooltip-5.19.0.tgz",
|
||||
"integrity": "sha512-NSUk77GMpxYKHFKJVNHL++QQXRuH2QW1qDrXPtJnp2s/MJvUnU73N5TTADwDyrO2+xGlr0xHhjvQphkF60cMEA==",
|
||||
"dependencies": {
|
||||
"@floating-ui/dom": "^1.0.0",
|
||||
"classnames": "^2.3.0"
|
||||
},
|
||||
"peerDependencies": {
|
||||
"react": ">=16.14.0",
|
||||
"react-dom": ">=16.14.0"
|
||||
}
|
||||
},
|
||||
"node_modules/reactflow": {
|
||||
"version": "11.7.4",
|
||||
"resolved": "https://registry.npmjs.org/reactflow/-/reactflow-11.7.4.tgz",
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@
|
|||
"react-dom": "^18.2.0",
|
||||
"react-router-dom": "^6.14.2",
|
||||
"react-router-hash-link": "^2.4.3",
|
||||
"react-tooltip": "^5.19.0",
|
||||
"reactflow": "^11.7.4"
|
||||
},
|
||||
"scripts": {
|
||||
|
|
|
|||
|
|
@ -0,0 +1,18 @@
|
|||
import clsx from "clsx";
|
||||
import { Variable } from "../../schema";
|
||||
import { VariableName } from "./VariableName";
|
||||
|
||||
export interface UnknownVariableProps {
|
||||
variable: Variable;
|
||||
}
|
||||
|
||||
export function UnknownVariable({
|
||||
variable,
|
||||
}: UnknownVariableProps): JSX.Element {
|
||||
return (
|
||||
<div className={clsx("rounded-md whitespace-nowrap space-x-1 pr-1")}>
|
||||
<VariableName className="inline-block" variable={variable} />
|
||||
<span>???</span>
|
||||
</div>
|
||||
);
|
||||
}
|
||||
|
|
@ -3,7 +3,7 @@ import type { Engine, EventEpoch } from "../../engine/engine";
|
|||
import { GraphMessage } from "../../utils/events";
|
||||
|
||||
export interface CommonProps {
|
||||
currentEpoch: EventEpoch;
|
||||
selectedEpochs: EventEpoch[];
|
||||
engine: Engine;
|
||||
graphEe: TypedEmitter<GraphMessage>;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,340 +0,0 @@
|
|||
import clsx from "clsx";
|
||||
import React, { useCallback, useMemo, useState } from "react";
|
||||
import { TypedEmitter } from "tiny-typed-emitter";
|
||||
import { EventEpoch } from "../engine/engine";
|
||||
import { lastSubEvent } from "../engine/event_util";
|
||||
import { useFocusOutlineEvent } from "../hooks/useFocusOutlineEvent";
|
||||
import { UnificationMode, Event } from "../schema";
|
||||
import { EventListMessage, GraphMessage } from "../utils/events";
|
||||
import { Refine } from "../utils/refine";
|
||||
import EpochCell from "./Common/EpochCell";
|
||||
import { CommonProps } from "./EventItem/types";
|
||||
import { VariableEl } from "./EventItem/Variable";
|
||||
|
||||
interface EventListProps extends CommonProps {
|
||||
events: Event[];
|
||||
eventListEe: TypedEmitter<EventListMessage>;
|
||||
root?: boolean;
|
||||
}
|
||||
|
||||
const MT = "my-2.5";
|
||||
const LOWER_OPACITY = "opacity-40";
|
||||
|
||||
export default function EventList(props: EventListProps): JSX.Element {
|
||||
const { events, root } = props;
|
||||
return (
|
||||
<ul className={clsx(MT, "space-y-2.5", root ? "" : "ml-[1em]")}>
|
||||
{events.map((event, i) => (
|
||||
<li key={i}>
|
||||
<OneEvent {...props} event={event} />
|
||||
</li>
|
||||
))}
|
||||
</ul>
|
||||
);
|
||||
}
|
||||
|
||||
interface OneEventProps extends CommonProps {
|
||||
event: Event;
|
||||
eventListEe: TypedEmitter<EventListMessage>;
|
||||
}
|
||||
|
||||
function OneEvent(props: OneEventProps): JSX.Element {
|
||||
const { event } = props;
|
||||
switch (event.type) {
|
||||
case "Unification":
|
||||
return <Unification {...props} event={event} />;
|
||||
case "VariableUnified":
|
||||
return <></>;
|
||||
case "VariableSetDescriptor":
|
||||
return <></>;
|
||||
}
|
||||
}
|
||||
|
||||
const DROPDOWN_CLOSED = "▶";
|
||||
const DROPDOWN_OPEN = "▼";
|
||||
|
||||
const UN_UNKNOWN = "💭";
|
||||
const UN_SUCCESS = "✅";
|
||||
const UN_FAILURE = "❌";
|
||||
|
||||
function epochInRange(
|
||||
epoch: EventEpoch,
|
||||
[start, end]: [EventEpoch, EventEpoch]
|
||||
): boolean {
|
||||
return epoch >= start && epoch <= end;
|
||||
}
|
||||
|
||||
interface UnificationProps extends CommonProps {
|
||||
event: Refine<Event, "Unification">;
|
||||
eventListEe: TypedEmitter<EventListMessage>;
|
||||
}
|
||||
|
||||
const COL_1_P = "pl-1.5";
|
||||
|
||||
const COL_1_OUTLINE_STYLES = clsx(COL_1_P, "outline-event-col-1");
|
||||
const COL_3_OUTLINE_STYLES = clsx("outline-event-col-3");
|
||||
|
||||
const COL_1_ROUNDED = "rounded-l-md";
|
||||
const COL_3_ROUNDED = "rounded-r-md";
|
||||
|
||||
const UN_EXPANDED_OUTLINE_STYLES = clsx(
|
||||
COL_1_P,
|
||||
"ring-inset ring-2 ring-blue-500"
|
||||
);
|
||||
|
||||
const TRANSITION_SHADOW = "transition-shadow ease-in-out duration-500";
|
||||
const TRANSITION_OPACITY = "transition-opacity ease-in-out duration-150";
|
||||
|
||||
function Unification(props: UnificationProps): JSX.Element {
|
||||
const { engine, event, currentEpoch, graphEe, eventListEe } = props;
|
||||
const { mode, subevents, success } = event;
|
||||
|
||||
const beforeUnificationEpoch = engine.getEventIndex(event);
|
||||
const afterUnificationEpoch = engine.getEventIndex(lastSubEvent(event));
|
||||
|
||||
const containsCurrentEpoch = epochInRange(currentEpoch, [
|
||||
beforeUnificationEpoch,
|
||||
afterUnificationEpoch,
|
||||
]);
|
||||
|
||||
const leftVar = useMemo(
|
||||
() => (epoch: EventEpoch) =>
|
||||
<VariableEl {...props} epoch={epoch} variable={event.left} />,
|
||||
[event.left, props]
|
||||
);
|
||||
const rightVar = useMemo(
|
||||
() => (epoch: EventEpoch) =>
|
||||
<VariableEl {...props} epoch={epoch} variable={event.right} />,
|
||||
[event.right, props]
|
||||
);
|
||||
|
||||
const [isOpen, setIsOpen] = useState(false);
|
||||
const isOutlined = useFocusOutlineEvent({
|
||||
ee: eventListEe,
|
||||
value: currentEpoch,
|
||||
event: "focusEpoch",
|
||||
});
|
||||
|
||||
const modeIcon = useMemo(() => <UnificationModeIcon mode={mode} />, [mode]);
|
||||
|
||||
const resultIcon = success ? UN_SUCCESS : UN_FAILURE;
|
||||
const resultHeadline = <Headline icon={resultIcon}></Headline>;
|
||||
|
||||
const epochCell = useMemo(() => {
|
||||
if (!containsCurrentEpoch) return null;
|
||||
return <EventListEpochCell epoch={currentEpoch} graphEe={graphEe} />;
|
||||
}, [containsCurrentEpoch, currentEpoch, graphEe]);
|
||||
|
||||
const getHeadline = useCallback(
|
||||
({
|
||||
epoch,
|
||||
includeEpochIfInRange,
|
||||
}: {
|
||||
epoch: EventEpoch;
|
||||
includeEpochIfInRange: boolean;
|
||||
}) => {
|
||||
const topHeadline = (
|
||||
<Headline icon={isOpen ? UN_UNKNOWN : resultIcon}></Headline>
|
||||
);
|
||||
|
||||
const optEpochCell =
|
||||
includeEpochIfInRange && containsCurrentEpoch && epochCell;
|
||||
|
||||
return (
|
||||
<button
|
||||
onClick={() => setIsOpen(!isOpen)}
|
||||
className="w-full text-left whitespace-nowrap h-full"
|
||||
>
|
||||
{optEpochCell}
|
||||
<span
|
||||
className={clsx(
|
||||
"mr-2",
|
||||
isOpen ? "text-slate-500" : "text-slate-400"
|
||||
)}
|
||||
>
|
||||
{isOpen ? DROPDOWN_OPEN : DROPDOWN_CLOSED}
|
||||
</span>
|
||||
{topHeadline} {leftVar(epoch)} {modeIcon} {rightVar(epoch)}
|
||||
</button>
|
||||
);
|
||||
},
|
||||
[
|
||||
isOpen,
|
||||
resultIcon,
|
||||
containsCurrentEpoch,
|
||||
epochCell,
|
||||
leftVar,
|
||||
modeIcon,
|
||||
rightVar,
|
||||
]
|
||||
);
|
||||
|
||||
if (!isOpen) {
|
||||
const headLine = getHeadline({
|
||||
epoch: afterUnificationEpoch,
|
||||
includeEpochIfInRange: true,
|
||||
});
|
||||
return (
|
||||
<div
|
||||
className={clsx(
|
||||
TRANSITION_OPACITY,
|
||||
!containsCurrentEpoch && LOWER_OPACITY
|
||||
)}
|
||||
>
|
||||
<div
|
||||
className={clsx(
|
||||
"rounded-md",
|
||||
TRANSITION_SHADOW,
|
||||
containsCurrentEpoch && isOutlined
|
||||
? UN_EXPANDED_OUTLINE_STYLES
|
||||
: COL_1_P
|
||||
)}
|
||||
>
|
||||
{headLine}
|
||||
</div>
|
||||
</div>
|
||||
);
|
||||
} else {
|
||||
const beforeIsCurrentEpoch = beforeUnificationEpoch === currentEpoch;
|
||||
const afterIsCurrentEpoch = afterUnificationEpoch === currentEpoch;
|
||||
|
||||
const epochCellBefore = beforeIsCurrentEpoch && epochCell;
|
||||
const epochCellAfter = afterIsCurrentEpoch && epochCell;
|
||||
|
||||
const outlineEpochCellAfter = afterIsCurrentEpoch && isOutlined;
|
||||
const outlineEpochCellBefore = beforeIsCurrentEpoch && isOutlined;
|
||||
|
||||
const headlineBefore = getHeadline({
|
||||
epoch: beforeUnificationEpoch,
|
||||
includeEpochIfInRange: false,
|
||||
});
|
||||
|
||||
const dropdownTransparent = (
|
||||
<span className="text-transparent mr-2">{DROPDOWN_OPEN}</span>
|
||||
);
|
||||
|
||||
const headlineAfter = (
|
||||
<div className={clsx("whitespace-nowrap")}>
|
||||
{dropdownTransparent}
|
||||
{resultHeadline} {leftVar(afterUnificationEpoch)} {modeIcon}{" "}
|
||||
{rightVar(afterUnificationEpoch)}
|
||||
</div>
|
||||
);
|
||||
|
||||
return (
|
||||
<div
|
||||
className={clsx(
|
||||
"grid gap-0 grid-cols-[min-content_min-content_auto] opacity-100",
|
||||
TRANSITION_OPACITY
|
||||
)}
|
||||
>
|
||||
{/* Row 1: unification start */}
|
||||
<div
|
||||
className={clsx(
|
||||
"row-start-1 col-start-1",
|
||||
TRANSITION_SHADOW,
|
||||
COL_1_ROUNDED,
|
||||
outlineEpochCellBefore ? COL_1_OUTLINE_STYLES : COL_1_P
|
||||
)}
|
||||
>
|
||||
{epochCellBefore}
|
||||
</div>
|
||||
<div
|
||||
className={clsx(
|
||||
"row-start-1 col-start-3",
|
||||
TRANSITION_SHADOW,
|
||||
COL_3_ROUNDED,
|
||||
outlineEpochCellBefore && COL_3_OUTLINE_STYLES
|
||||
)}
|
||||
>
|
||||
{headlineBefore}
|
||||
</div>
|
||||
|
||||
{/* Row 2: inner traces */}
|
||||
<div className={clsx("row-start-2 col-start-1")}></div>
|
||||
<div className={clsx("row-start-2 col-start-3")}>
|
||||
<EventList
|
||||
{...props}
|
||||
root={false}
|
||||
engine={engine}
|
||||
events={subevents}
|
||||
/>
|
||||
</div>
|
||||
|
||||
{/* Row 3: inner traces */}
|
||||
<div
|
||||
className={clsx(
|
||||
"row-start-3 col-start-1",
|
||||
TRANSITION_SHADOW,
|
||||
COL_1_ROUNDED,
|
||||
outlineEpochCellAfter ? COL_1_OUTLINE_STYLES : COL_1_P
|
||||
)}
|
||||
>
|
||||
{epochCellAfter}
|
||||
</div>
|
||||
<div
|
||||
className={clsx(
|
||||
"row-start-3 col-start-3",
|
||||
TRANSITION_SHADOW,
|
||||
COL_3_ROUNDED,
|
||||
outlineEpochCellAfter && COL_3_OUTLINE_STYLES
|
||||
)}
|
||||
>
|
||||
{headlineAfter}
|
||||
</div>
|
||||
|
||||
{/* Col 2: dropdown line */}
|
||||
<div
|
||||
className={clsx(
|
||||
"row-start-1 row-end-4 col-start-2 h-full",
|
||||
"relative z-[1] h-full",
|
||||
"before:content-[''] before:border-l before:border-slate-500 before:z-[-1]",
|
||||
"before:absolute before:w-0 before:h-[calc(100%-1.5rem)] before:top-[1rem] before:left-[0.3rem]"
|
||||
)}
|
||||
></div>
|
||||
</div>
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
function Headline({ icon }: { icon: string }): JSX.Element {
|
||||
return (
|
||||
<div className="inline-block align-middle">
|
||||
<div className="">{icon}</div>
|
||||
</div>
|
||||
);
|
||||
}
|
||||
|
||||
function UnificationModeIcon({ mode }: { mode: UnificationMode }): JSX.Element {
|
||||
switch (mode.type) {
|
||||
case "Eq":
|
||||
return <>~</>;
|
||||
case "Present":
|
||||
return <>+=</>;
|
||||
case "LambdaSetSpecialization":
|
||||
return <>|~|</>;
|
||||
}
|
||||
}
|
||||
|
||||
interface EventListEpochCellProps {
|
||||
epoch: EventEpoch;
|
||||
graphEe: TypedEmitter<GraphMessage>;
|
||||
}
|
||||
|
||||
function EventListEpochCell({
|
||||
epoch,
|
||||
graphEe,
|
||||
}: EventListEpochCellProps): JSX.Element {
|
||||
return (
|
||||
<span
|
||||
id={`events-${epoch}`}
|
||||
className={clsx("cursor-pointer rounded-md")}
|
||||
onClick={(e) => {
|
||||
e.stopPropagation();
|
||||
graphEe.emit("focusEpoch", epoch);
|
||||
}}
|
||||
>
|
||||
<EpochCell>{epoch}</EpochCell>
|
||||
</span>
|
||||
);
|
||||
}
|
||||
|
|
@ -0,0 +1,76 @@
|
|||
export interface GroupInfo {
|
||||
group: string;
|
||||
groupHover: string;
|
||||
}
|
||||
|
||||
export function depthToGroupInfo(depth: number): GroupInfo {
|
||||
switch (depth) {
|
||||
case 0:
|
||||
return {
|
||||
group: `group/event-0`,
|
||||
groupHover: `group-hover/event-0:opacity-100`,
|
||||
};
|
||||
case 1:
|
||||
return {
|
||||
group: `group/event-1`,
|
||||
groupHover: `group-hover/event-1:opacity-100`,
|
||||
};
|
||||
case 2:
|
||||
return {
|
||||
group: `group/event-2`,
|
||||
groupHover: `group-hover/event-2:opacity-100`,
|
||||
};
|
||||
case 3:
|
||||
return {
|
||||
group: `group/event-3`,
|
||||
groupHover: `group-hover/event-3:opacity-100`,
|
||||
};
|
||||
case 4:
|
||||
return {
|
||||
group: `group/event-4`,
|
||||
groupHover: `group-hover/event-4:opacity-100`,
|
||||
};
|
||||
case 5:
|
||||
return {
|
||||
group: `group/event-5`,
|
||||
groupHover: `group-hover/event-5:opacity-100`,
|
||||
};
|
||||
case 6:
|
||||
return {
|
||||
group: `group/event-6`,
|
||||
groupHover: `group-hover/event-6:opacity-100`,
|
||||
};
|
||||
case 7:
|
||||
return {
|
||||
group: `group/event-7`,
|
||||
groupHover: `group-hover/event-7:opacity-100`,
|
||||
};
|
||||
case 8:
|
||||
return {
|
||||
group: `group/event-8`,
|
||||
groupHover: `group-hover/event-8:opacity-100`,
|
||||
};
|
||||
case 9:
|
||||
return {
|
||||
group: `group/event-9`,
|
||||
groupHover: `group-hover/event-9:opacity-100`,
|
||||
};
|
||||
case 10:
|
||||
return {
|
||||
group: `group/event-10`,
|
||||
groupHover: `group-hover/event-10:opacity-100`,
|
||||
};
|
||||
case 11:
|
||||
return {
|
||||
group: `group/event-11`,
|
||||
groupHover: `group-hover/event-11:opacity-100`,
|
||||
};
|
||||
case 12:
|
||||
return {
|
||||
group: `group/event-12`,
|
||||
groupHover: `group-hover/event-12:opacity-100`,
|
||||
};
|
||||
default:
|
||||
throw new Error(`Too deep: ${depth}`);
|
||||
}
|
||||
}
|
||||
423
crates/compiler/checkmate/www/src/components/EventList/index.tsx
Normal file
423
crates/compiler/checkmate/www/src/components/EventList/index.tsx
Normal file
|
|
@ -0,0 +1,423 @@
|
|||
import clsx from "clsx";
|
||||
import React, { useCallback, useMemo, useState } from "react";
|
||||
import { TypedEmitter } from "tiny-typed-emitter";
|
||||
import { EventEpoch } from "../../engine/engine";
|
||||
import { lastSubEvent } from "../../engine/event_util";
|
||||
import { useFocusOutlineEvent } from "../../hooks/useFocusOutlineEvent";
|
||||
import { UnificationMode, Event } from "../../schema";
|
||||
import {
|
||||
EventListMessage,
|
||||
GlobalMessage,
|
||||
GraphMessage,
|
||||
LoadEpochView,
|
||||
} from "../../utils/events";
|
||||
import { Refine } from "../../utils/refine";
|
||||
import EpochCell from "../Common/EpochCell";
|
||||
import { CommonProps } from "../EventItem/types";
|
||||
import { VariableEl } from "../EventItem/Variable";
|
||||
import { depthToGroupInfo } from "./depthGroup";
|
||||
|
||||
interface EventListProps extends CommonProps {
|
||||
events: Event[];
|
||||
eventListEe: TypedEmitter<EventListMessage>;
|
||||
globalEe: TypedEmitter<GlobalMessage>;
|
||||
depth: number;
|
||||
}
|
||||
|
||||
const MT = "my-2.5";
|
||||
const LOWER_OPACITY = "opacity-40";
|
||||
|
||||
export default function EventList(props: EventListProps): JSX.Element {
|
||||
const { events, depth } = props;
|
||||
return (
|
||||
<ul className={clsx(MT, "space-y-2.5", depth === 0 ? "" : "ml-[1em]")}>
|
||||
{events.map((event, i) => (
|
||||
<li key={i}>
|
||||
<OneEvent {...props} event={event} />
|
||||
</li>
|
||||
))}
|
||||
</ul>
|
||||
);
|
||||
}
|
||||
|
||||
interface OneEventProps extends CommonProps {
|
||||
event: Event;
|
||||
eventListEe: TypedEmitter<EventListMessage>;
|
||||
globalEe: TypedEmitter<GlobalMessage>;
|
||||
depth: number;
|
||||
}
|
||||
|
||||
function OneEvent(props: OneEventProps): JSX.Element {
|
||||
const { event } = props;
|
||||
switch (event.type) {
|
||||
case "Unification":
|
||||
return <UnificationEvent {...props} event={event} />;
|
||||
case "VariableUnified":
|
||||
return <></>;
|
||||
case "VariableSetDescriptor":
|
||||
return <></>;
|
||||
}
|
||||
}
|
||||
|
||||
const DROPDOWN_CLOSED = "▶";
|
||||
const DROPDOWN_OPEN = "▼";
|
||||
|
||||
const UN_UNKNOWN = "💭";
|
||||
const UN_SUCCESS = "✅";
|
||||
const UN_FAILURE = "❌";
|
||||
|
||||
function epochInRange(
|
||||
epoch: EventEpoch,
|
||||
[start, end]: [EventEpoch, EventEpoch]
|
||||
): boolean {
|
||||
return epoch >= start && epoch <= end;
|
||||
}
|
||||
|
||||
interface UnificationProps extends CommonProps {
|
||||
event: Refine<Event, "Unification">;
|
||||
eventListEe: TypedEmitter<EventListMessage>;
|
||||
globalEe: TypedEmitter<GlobalMessage>;
|
||||
depth: number;
|
||||
}
|
||||
|
||||
const COL_1_P = "pl-1.5";
|
||||
|
||||
const COL_1_OUTLINE_STYLES = clsx(COL_1_P, "outline-event-col-1");
|
||||
const COL_3_OUTLINE_STYLES = clsx("outline-event-col-3");
|
||||
|
||||
const COL_1_ROUNDED = "rounded-l-md";
|
||||
const COL_3_ROUNDED = "rounded-r-md";
|
||||
|
||||
const UN_EXPANDED_OUTLINE_STYLES = clsx("ring-inset ring-2 ring-blue-500");
|
||||
|
||||
const TRANSITION_SHADOW = "transition-shadow ease-in-out duration-500";
|
||||
const TRANSITION_OPACITY = "transition-opacity ease-in-out duration-150";
|
||||
|
||||
const GROUP_STLYES = "relative overflow-hidden";
|
||||
|
||||
// Space for the hover cells at the end of line.
|
||||
const EOL_SPACE = "pr-12";
|
||||
|
||||
function UnificationEvent(props: UnificationProps): JSX.Element {
|
||||
const {
|
||||
engine,
|
||||
event,
|
||||
selectedEpochs,
|
||||
graphEe,
|
||||
eventListEe,
|
||||
depth,
|
||||
globalEe,
|
||||
} = props;
|
||||
const { mode, subevents, success } = event;
|
||||
|
||||
const beforeUnificationEpoch = engine.getEventIndex(event);
|
||||
const afterUnificationEpoch = engine.getEventIndex(lastSubEvent(event));
|
||||
|
||||
const containedEpoch = selectedEpochs.find((epoch) =>
|
||||
epochInRange(epoch, [beforeUnificationEpoch, afterUnificationEpoch])
|
||||
);
|
||||
|
||||
const leftVar = useMemo(
|
||||
() => (epoch: EventEpoch) =>
|
||||
<VariableEl {...props} epoch={epoch} variable={event.left} />,
|
||||
[event.left, props]
|
||||
);
|
||||
const rightVar = useMemo(
|
||||
() => (epoch: EventEpoch) =>
|
||||
<VariableEl {...props} epoch={epoch} variable={event.right} />,
|
||||
[event.right, props]
|
||||
);
|
||||
|
||||
const [isOpen, setIsOpen] = useState(false);
|
||||
const isOutlined = useFocusOutlineEvent<"focusEpoch", EventEpoch | undefined>(
|
||||
{
|
||||
ee: eventListEe,
|
||||
value: containedEpoch,
|
||||
event: "focusEpoch",
|
||||
}
|
||||
);
|
||||
|
||||
const modeIcon = useMemo(() => <UnificationModeIcon mode={mode} />, [mode]);
|
||||
|
||||
const resultIcon = success ? UN_SUCCESS : UN_FAILURE;
|
||||
const resultHeadline = <Headline icon={resultIcon}></Headline>;
|
||||
|
||||
const epochCell = useMemo(() => {
|
||||
if (containedEpoch === undefined) return null;
|
||||
return <EventListEpochCell epoch={containedEpoch} graphEe={graphEe} />;
|
||||
}, [containedEpoch, graphEe]);
|
||||
|
||||
const getBeforeUnificationHeadline = useCallback(
|
||||
({
|
||||
epoch,
|
||||
collapsedMode,
|
||||
}: {
|
||||
epoch: EventEpoch;
|
||||
collapsedMode?: boolean;
|
||||
}) => {
|
||||
const topHeadline = (
|
||||
<Headline icon={isOpen ? UN_UNKNOWN : resultIcon}></Headline>
|
||||
);
|
||||
|
||||
const optEpochCell =
|
||||
collapsedMode && containedEpoch !== undefined && epochCell;
|
||||
|
||||
return (
|
||||
<button
|
||||
onClick={() => setIsOpen(!isOpen)}
|
||||
className={clsx(
|
||||
"w-full text-left whitespace-nowrap h-full overflow-scroll",
|
||||
collapsedMode && COL_1_P
|
||||
)}
|
||||
>
|
||||
<span className={EOL_SPACE}>
|
||||
{optEpochCell}
|
||||
<span
|
||||
className={clsx(
|
||||
"mr-2",
|
||||
isOpen ? "text-slate-500" : "text-slate-400"
|
||||
)}
|
||||
>
|
||||
{isOpen ? DROPDOWN_OPEN : DROPDOWN_CLOSED}
|
||||
</span>
|
||||
{topHeadline} {leftVar(epoch)} {modeIcon} {rightVar(epoch)}
|
||||
</span>
|
||||
</button>
|
||||
);
|
||||
},
|
||||
[isOpen, resultIcon, containedEpoch, epochCell, leftVar, modeIcon, rightVar]
|
||||
);
|
||||
|
||||
const { group, groupHover } = depthToGroupInfo(depth);
|
||||
|
||||
if (!isOpen) {
|
||||
const headLine = getBeforeUnificationHeadline({
|
||||
epoch: afterUnificationEpoch,
|
||||
collapsedMode: true,
|
||||
});
|
||||
return (
|
||||
<div
|
||||
className={clsx(
|
||||
"rounded-md",
|
||||
TRANSITION_SHADOW,
|
||||
group,
|
||||
GROUP_STLYES,
|
||||
containedEpoch !== undefined &&
|
||||
isOutlined &&
|
||||
UN_EXPANDED_OUTLINE_STYLES
|
||||
)}
|
||||
>
|
||||
<div
|
||||
className={clsx(
|
||||
TRANSITION_OPACITY,
|
||||
containedEpoch === undefined && LOWER_OPACITY
|
||||
)}
|
||||
>
|
||||
{headLine}
|
||||
</div>
|
||||
<LoadEpochGraphLauncher
|
||||
groupHover={groupHover}
|
||||
epoch={afterUnificationEpoch}
|
||||
globalEe={globalEe}
|
||||
className="bottom-0 right-2"
|
||||
/>
|
||||
</div>
|
||||
);
|
||||
} else {
|
||||
const beforeIsCurrentEpoch = beforeUnificationEpoch === containedEpoch;
|
||||
const afterIsCurrentEpoch = afterUnificationEpoch === containedEpoch;
|
||||
|
||||
const epochCellBefore = beforeIsCurrentEpoch && epochCell;
|
||||
const epochCellAfter = afterIsCurrentEpoch && epochCell;
|
||||
|
||||
const outlineEpochCellAfter = afterIsCurrentEpoch && isOutlined;
|
||||
const outlineEpochCellBefore = beforeIsCurrentEpoch && isOutlined;
|
||||
|
||||
const headlineBefore = getBeforeUnificationHeadline({
|
||||
epoch: beforeUnificationEpoch,
|
||||
});
|
||||
|
||||
const dropdownTransparent = (
|
||||
<span className="text-transparent mr-2">{DROPDOWN_OPEN}</span>
|
||||
);
|
||||
|
||||
const headlineAfter = (
|
||||
<div className={clsx("whitespace-nowrap")}>
|
||||
{dropdownTransparent}
|
||||
{resultHeadline} {leftVar(afterUnificationEpoch)} {modeIcon}{" "}
|
||||
{rightVar(afterUnificationEpoch)}
|
||||
</div>
|
||||
);
|
||||
|
||||
return (
|
||||
<div className={clsx(group, GROUP_STLYES)}>
|
||||
<div
|
||||
className={clsx(
|
||||
"grid gap-0 grid-cols-[min-content_min-content_1fr_auto] opacity-100",
|
||||
"overflow-scroll",
|
||||
TRANSITION_OPACITY
|
||||
)}
|
||||
>
|
||||
{/* Row 1: unification start */}
|
||||
<div
|
||||
className={clsx(
|
||||
"row-start-1 col-start-1",
|
||||
TRANSITION_SHADOW,
|
||||
COL_1_ROUNDED,
|
||||
outlineEpochCellBefore ? COL_1_OUTLINE_STYLES : COL_1_P
|
||||
)}
|
||||
>
|
||||
{epochCellBefore}
|
||||
</div>
|
||||
<div
|
||||
className={clsx(
|
||||
"row-start-1 col-start-3 col-end-5",
|
||||
TRANSITION_SHADOW,
|
||||
COL_3_ROUNDED,
|
||||
outlineEpochCellBefore && COL_3_OUTLINE_STYLES,
|
||||
EOL_SPACE
|
||||
)}
|
||||
>
|
||||
{headlineBefore}
|
||||
</div>
|
||||
|
||||
{/* Row 2: inner traces */}
|
||||
<div className={clsx("row-start-2 col-start-1")}></div>
|
||||
<div className={clsx("row-start-2col-start-3 col-end-4", "w-full")}>
|
||||
<EventList
|
||||
{...props}
|
||||
depth={depth + 1}
|
||||
engine={engine}
|
||||
events={subevents}
|
||||
/>
|
||||
</div>
|
||||
|
||||
{/* Row 3: unification end */}
|
||||
<div
|
||||
className={clsx(
|
||||
"row-start-3 col-start-1",
|
||||
TRANSITION_SHADOW,
|
||||
COL_1_ROUNDED,
|
||||
outlineEpochCellAfter ? COL_1_OUTLINE_STYLES : COL_1_P
|
||||
)}
|
||||
>
|
||||
{epochCellAfter}
|
||||
</div>
|
||||
<div
|
||||
className={clsx(
|
||||
"row-start-3 col-start-3 col-end-5",
|
||||
TRANSITION_SHADOW,
|
||||
COL_3_ROUNDED,
|
||||
outlineEpochCellAfter && COL_3_OUTLINE_STYLES,
|
||||
EOL_SPACE
|
||||
)}
|
||||
>
|
||||
{headlineAfter}
|
||||
</div>
|
||||
|
||||
{/* Col 2: dropdown line */}
|
||||
<div
|
||||
className={clsx(
|
||||
"row-start-1 row-end-4 col-start-2 h-full",
|
||||
"relative z-[1] h-full",
|
||||
"before:content-[''] before:border-l before:border-slate-500 before:z-[-1]",
|
||||
"before:absolute before:w-0 before:h-[calc(100%-1.5rem)] before:top-[1rem] before:left-[0.3rem]"
|
||||
)}
|
||||
></div>
|
||||
</div>
|
||||
|
||||
<LoadEpochGraphLauncher
|
||||
groupHover={groupHover}
|
||||
epoch={beforeUnificationEpoch}
|
||||
globalEe={globalEe}
|
||||
className="top-0 right-2"
|
||||
/>
|
||||
<LoadEpochGraphLauncher
|
||||
groupHover={groupHover}
|
||||
epoch={afterUnificationEpoch}
|
||||
globalEe={globalEe}
|
||||
className="bottom-0 right-2"
|
||||
/>
|
||||
</div>
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
function Headline({ icon }: { icon: string }): JSX.Element {
|
||||
return (
|
||||
<div className="inline-block align-middle">
|
||||
<div className="">{icon}</div>
|
||||
</div>
|
||||
);
|
||||
}
|
||||
|
||||
function UnificationModeIcon({ mode }: { mode: UnificationMode }): JSX.Element {
|
||||
switch (mode.type) {
|
||||
case "Eq":
|
||||
return <>~</>;
|
||||
case "Present":
|
||||
return <>+=</>;
|
||||
case "LambdaSetSpecialization":
|
||||
return <>|~|</>;
|
||||
}
|
||||
}
|
||||
|
||||
interface EventListEpochCellProps {
|
||||
epoch: EventEpoch;
|
||||
graphEe: TypedEmitter<GraphMessage>;
|
||||
}
|
||||
|
||||
function EventListEpochCell({
|
||||
epoch,
|
||||
graphEe,
|
||||
}: EventListEpochCellProps): JSX.Element {
|
||||
return (
|
||||
<span
|
||||
id={`events-${epoch}`}
|
||||
className={clsx("cursor-pointer rounded-md")}
|
||||
onClick={(e) => {
|
||||
e.stopPropagation();
|
||||
graphEe.emit("focusEpoch", epoch);
|
||||
}}
|
||||
>
|
||||
<EpochCell>{epoch}</EpochCell>
|
||||
</span>
|
||||
);
|
||||
}
|
||||
|
||||
interface LoadEpochGraphLauncherProps {
|
||||
groupHover: string;
|
||||
epoch: EventEpoch;
|
||||
globalEe: TypedEmitter<GlobalMessage>;
|
||||
className?: string;
|
||||
}
|
||||
|
||||
function LoadEpochGraphLauncher({
|
||||
groupHover,
|
||||
epoch,
|
||||
className,
|
||||
globalEe,
|
||||
}: LoadEpochGraphLauncherProps): JSX.Element {
|
||||
return (
|
||||
<div className={clsx("absolute opacity-0", groupHover, className)}>
|
||||
<span className="space-x-0.5 bg-gray-200 ring-1 ring-slate-300 rounded-sm px-1 opacity-80 hover:opacity-100">
|
||||
<span
|
||||
className="text-blue-400 hover:text-blue-500 cursor-pointer"
|
||||
onClick={() => {
|
||||
globalEe.emit("loadEpoch", epoch, LoadEpochView.Top);
|
||||
}}
|
||||
>
|
||||
↑
|
||||
</span>
|
||||
<span
|
||||
className="text-blue-400 hover:text-blue-500 cursor-pointer"
|
||||
onClick={() => {
|
||||
globalEe.emit("loadEpoch", epoch, LoadEpochView.Bot);
|
||||
}}
|
||||
>
|
||||
↓
|
||||
</span>
|
||||
</span>
|
||||
</div>
|
||||
);
|
||||
}
|
||||
|
|
@ -9,6 +9,7 @@ import { TypedEmitter } from "tiny-typed-emitter";
|
|||
import { VariableLink } from "../Common/VariableLink";
|
||||
import { VariableMessage } from "../../utils/events";
|
||||
import { useFocusOutlineEvent } from "../../hooks/useFocusOutlineEvent";
|
||||
import { UnknownVariable } from "../Common/UnknownVariable";
|
||||
|
||||
type AddSubVariableLink = ({
|
||||
from,
|
||||
|
|
@ -51,12 +52,17 @@ export default function VariableNode({
|
|||
});
|
||||
|
||||
const varType = subs.get(rawVariable);
|
||||
if (!varType) throw new Error("VariableNode: no entry for variable");
|
||||
|
||||
let renderContent: JSX.Element;
|
||||
let bgStyles: string;
|
||||
const isContent = varType.type === "descriptor";
|
||||
switch (varType.type) {
|
||||
const isContent = varType?.type === "descriptor";
|
||||
switch (varType?.type) {
|
||||
case undefined: {
|
||||
bgStyles = "bg-red-500";
|
||||
renderContent = <UnknownVariable variable={rawVariable} />;
|
||||
|
||||
break;
|
||||
}
|
||||
case "link": {
|
||||
bgStyles = LinkStyles.bg;
|
||||
|
||||
|
|
|
|||
|
|
@ -325,8 +325,14 @@ function Graph({
|
|||
graphEe,
|
||||
eventListEe,
|
||||
}: VariablesGraphProps): JSX.Element {
|
||||
const initialNodes: Node[] = [];
|
||||
const initialEdges: Edge[] = [];
|
||||
const instance = useReactFlow();
|
||||
|
||||
// We need to reset the graph when the subs snapshot changes. I'm not sure
|
||||
// why this isn't done by the existing state manager.
|
||||
useEffect(() => {
|
||||
instance.setNodes([]);
|
||||
instance.setEdges([]);
|
||||
}, [instance, subs.epoch]);
|
||||
|
||||
const varEe = useRef(new TypedEmitter<VariableMessage>());
|
||||
// Allow an unbounded number of listeners since we attach a listener for each
|
||||
|
|
@ -343,8 +349,8 @@ function Graph({
|
|||
useState<LayoutConfiguration>(LAYOUT_CONFIG_DOWN);
|
||||
|
||||
const [elements, setElements] = useState<LayoutedElements>({
|
||||
nodes: initialNodes,
|
||||
edges: initialEdges,
|
||||
nodes: [],
|
||||
edges: [],
|
||||
});
|
||||
|
||||
const [variablesNeedingFocus, setVariablesNeedingFocus] = useState<
|
||||
|
|
@ -548,10 +554,14 @@ function LayoutPanel({
|
|||
);
|
||||
}
|
||||
|
||||
export default function VariablesGraph(props: VariablesGraphProps) {
|
||||
export default function VariablesGraph({
|
||||
subs,
|
||||
graphEe,
|
||||
eventListEe,
|
||||
}: VariablesGraphProps) {
|
||||
return (
|
||||
<ReactFlowProvider>
|
||||
<Graph {...props} />
|
||||
<Graph subs={subs} graphEe={graphEe} eventListEe={eventListEe} />
|
||||
</ReactFlowProvider>
|
||||
);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,26 +1,52 @@
|
|||
import React, { useState } from "react";
|
||||
import React, { useEffect, useState } from "react";
|
||||
import { AllEvents } from "../schema";
|
||||
import { Engine } from "../engine/engine";
|
||||
import EventList from "./EventList";
|
||||
import { Engine, EventEpoch } from "../engine/engine";
|
||||
import EventList from "./EventList/index";
|
||||
import VariablesGraph from "./Graph/VariablesGraph";
|
||||
import { TypedEmitter } from "tiny-typed-emitter";
|
||||
import { EventListMessage, GraphMessage } from "../utils/events";
|
||||
import {
|
||||
EventListMessage,
|
||||
GlobalMessage,
|
||||
GraphMessage,
|
||||
LoadEpochView,
|
||||
} from "../utils/events";
|
||||
import { assertExhaustive } from "../utils/exhaustive";
|
||||
import { SubsSnapshot } from "../engine/subs";
|
||||
|
||||
interface UiProps {
|
||||
events: AllEvents;
|
||||
}
|
||||
|
||||
export default function Ui({ events }: UiProps): JSX.Element {
|
||||
const engine = new Engine(events);
|
||||
const engine = React.useRef(new Engine(events));
|
||||
|
||||
const graphEe = React.useRef(new TypedEmitter<GraphMessage>());
|
||||
const eventListEe = React.useRef(new TypedEmitter<EventListMessage>());
|
||||
const globalEe = React.useRef(new TypedEmitter<GlobalMessage>());
|
||||
|
||||
engine.stepTo(engine.lastEventIndex());
|
||||
const subs = engine.subsSnapshot();
|
||||
const [subsTop, setSubsTop] = useState<SubsSnapshot | undefined>(undefined);
|
||||
const [subsBot, setSubsBot] = useState<SubsSnapshot | undefined>(undefined);
|
||||
|
||||
// _setEpoch to be used in the future!
|
||||
const [epoch, _setEpoch] = useState(subs.epoch);
|
||||
useEffect(() => {
|
||||
globalEe.current.on("loadEpoch", (epoch, view) => {
|
||||
switch (view) {
|
||||
case LoadEpochView.Top: {
|
||||
setSubsTop(engine.current.stepToSnapshot(epoch));
|
||||
break;
|
||||
}
|
||||
case LoadEpochView.Bot: {
|
||||
setSubsBot(engine.current.stepToSnapshot(epoch));
|
||||
break;
|
||||
}
|
||||
default:
|
||||
assertExhaustive(view);
|
||||
}
|
||||
});
|
||||
}, []);
|
||||
|
||||
const selectedEpochs = [subsTop?.epoch, subsBot?.epoch]
|
||||
.filter((x): x is EventEpoch => x !== undefined)
|
||||
.sort();
|
||||
|
||||
return (
|
||||
<div
|
||||
|
|
@ -29,23 +55,51 @@ export default function Ui({ events }: UiProps): JSX.Element {
|
|||
graphEe.current.emit("keydown", e.key);
|
||||
}}
|
||||
>
|
||||
<div className="font-mono mt-2 text-lg md:flex-1 overflow-scroll">
|
||||
<div className="font-mono mt-2 text-lg md:flex-1 overflow-x-hidden overflow-y-scroll">
|
||||
<EventList
|
||||
engine={engine}
|
||||
root
|
||||
engine={engine.current}
|
||||
depth={0}
|
||||
events={events}
|
||||
graphEe={graphEe.current}
|
||||
eventListEe={eventListEe.current}
|
||||
currentEpoch={epoch}
|
||||
globalEe={globalEe.current}
|
||||
selectedEpochs={selectedEpochs}
|
||||
/>
|
||||
</div>
|
||||
<div className="flex-1 min-h-[50%] h-full">
|
||||
<VariablesGraph
|
||||
subs={subs}
|
||||
graphEe={graphEe.current}
|
||||
eventListEe={eventListEe.current}
|
||||
/>
|
||||
<div className="flex-1 min-h-[50%] h-full flex flex-col">
|
||||
{subsTop !== undefined && (
|
||||
<VariablesGraphView
|
||||
subs={subsTop}
|
||||
graphEe={graphEe.current}
|
||||
eventListEe={eventListEe.current}
|
||||
/>
|
||||
)}
|
||||
{/* */}
|
||||
{subsBot !== undefined && (
|
||||
<VariablesGraphView
|
||||
subs={subsBot}
|
||||
graphEe={graphEe.current}
|
||||
eventListEe={eventListEe.current}
|
||||
/>
|
||||
)}
|
||||
</div>
|
||||
</div>
|
||||
);
|
||||
}
|
||||
|
||||
interface VariablesGraphViewProps {
|
||||
subs: SubsSnapshot;
|
||||
graphEe: TypedEmitter<GraphMessage>;
|
||||
eventListEe: TypedEmitter<EventListMessage>;
|
||||
}
|
||||
|
||||
function VariablesGraphView({
|
||||
subs,
|
||||
graphEe,
|
||||
eventListEe,
|
||||
}: VariablesGraphViewProps): JSX.Element {
|
||||
console.log("re-rendering...");
|
||||
return (
|
||||
<VariablesGraph subs={subs} graphEe={graphEe} eventListEe={eventListEe} />
|
||||
);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -83,6 +83,11 @@ export class Engine {
|
|||
}
|
||||
}
|
||||
|
||||
stepToSnapshot(eventIndex: EventEpoch): SubsSnapshot {
|
||||
this.stepTo(eventIndex);
|
||||
return this.subsSnapshot();
|
||||
}
|
||||
|
||||
get subs(): Readonly<Subs> {
|
||||
return this.#subs;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -14,3 +14,12 @@ export interface GraphMessage {
|
|||
export interface EventListMessage {
|
||||
focusEpoch: (epoch: EventEpoch) => void;
|
||||
}
|
||||
|
||||
export enum LoadEpochView {
|
||||
Top,
|
||||
Bot,
|
||||
}
|
||||
|
||||
export interface GlobalMessage {
|
||||
loadEpoch: (epoch: EventEpoch, view: LoadEpochView) => void;
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue