const id = idHint || ('inst:' + qid(inst.iiClass) + ':' + (inst._idx ?? renderInstanceHead(inst, originClassQn)));
if (seenNodes.has(id)) return id;
seenNodes.add(id);
+ const head = renderInstanceHead(inst, originClassQn);
+ // Equality constraints from the instance's iiContext are rendered
+ // as "chip" lines beneath the head, indented and prefixed with
+ // `where`, instead of being drawn as fake-class edges. This keeps
+ // them visible at-a-glance without polluting the layout.
+ const eqs = (inst.iiContext || [])
+ .filter(p => p.piIsEq)
+ .map(p =>
+ renderArg(p.piArgs[0], inst.iiTyVars) + ' ' +
+ p.piClass.qnName + ' ' +
+ renderArg(p.piArgs[1], inst.iiTyVars)
+ );
+ const label = eqs.length === 0
+ ? head
+ : head + '\n' + eqs.map(s => 'where ' + s).join('\n');
els.push({ group: 'nodes', data: {
id,
- label: renderInstanceHead(inst, originClassQn),
+ label,
kind: 'instance',
orphan: !!inst.iiOrphan,
classId: qid(inst.iiClass),
instance: inst,
+ eqs, // exposed for the side panel / tests
}});
return id;
}
// origin node, and lift the family's known type-instance rows into
// the graph so the user can verify the family is actually defined
// for the relevant types.
- function addFamilyLinksFromArgs(args, originId, edgeTag) {
+ //
+ // If @predClassQn@ is non-null, we additionally try to /resolve/ the
+ // predicate using each fam-instance's RHS — substitute the family
+ // application out, find a matching instance of the predicate's class,
+ // and draw a `fam-resolves` chain edge from the fam-instance node to
+ // the matched class-instance node. This makes the chain
+ // focused-instance → family → concrete fam-instance → Eq instance
+ // visible as one path instead of two unrelated arrows.
+ function addFamilyLinksFromArgs(args, originId, edgeTag, predClassQn) {
const fams = collectFamilyRefs(args);
for (const fa of fams) {
const famNodeId = ensureFamilyNode(fa);
const linkId = originId + '#viafam#' + edgeTag + '#' + famNodeId;
- if (seenNodes.has(linkId)) continue;
- seenNodes.add(linkId);
- els.push({ group: 'edges', data: {
- id: linkId,
- source: originId,
- target: famNodeId,
- kind: 'via-family',
- label: 'via ' + fa.qnName,
- }});
- // Also surface the matching type-instance rows so we see where
- // the family is actually defined for which heads.
+ if (!seenNodes.has(linkId)) {
+ seenNodes.add(linkId);
+ els.push({ group: 'edges', data: {
+ id: linkId,
+ source: originId,
+ target: famNodeId,
+ kind: 'via-family',
+ label: 'via ' + fa.qnName,
+ }});
+ }
+ // Surface only the type-instance rows whose LHS *can* describe
+ // the focused instance's family-app — anything else is unrelated
+ // noise (e.g. `TxIn ByronBlock` while looking at a Shelley
+ // instance). Run the relevance check *before* creating the
+ // fam-instance node so irrelevant rows are skipped entirely.
for (const fi of (famInstsByFamily.get(famNodeId) || [])) {
+ let resolvedArgs = null;
+ if (predClassQn) {
+ resolvedArgs = args.map(a => replaceFamilyApp(a, fa, fi));
+ if (resolvedArgs.some(a => a === null)) continue;
+ }
+
const fiNodeId = ensureFamInstanceNode(fi);
const fdId = famNodeId + '=>' + fiNodeId;
- if (seenNodes.has(fdId)) continue;
- seenNodes.add(fdId);
- els.push({ group: 'edges', data: {
- id: fdId,
- source: famNodeId,
- target: fiNodeId,
- kind: 'fam-defines',
- }});
+ if (!seenNodes.has(fdId)) {
+ seenNodes.add(fdId);
+ els.push({ group: 'edges', data: {
+ id: fdId,
+ source: famNodeId,
+ target: fiNodeId,
+ kind: 'fam-defines',
+ }});
+ }
+
+ // Resolution chain: with the substituted RHS in hand, look for
+ // a matching class instance of @predClassQn@.
+ if (predClassQn && resolvedArgs) {
+ const reduced = resolvedArgs.map(reduceTypeArg);
+ const matched = findMatchingInstances(predClassQn, reduced);
+ for (const m of matched) {
+ const mId = ensureInstanceNode(
+ m, predClassQn,
+ 'inst:' + m._idx
+ );
+ // Make sure the matched instance hangs under its class node
+ // so the user has a stable place to find it.
+ const predClsId = ensureClassNode(predClassQn);
+ const defId = predClsId + '=>' + mId;
+ if (!seenNodes.has(defId)) {
+ seenNodes.add(defId);
+ els.push({ group: 'edges', data: {
+ id: defId, source: predClsId, target: mId, kind: 'defines',
+ }});
+ }
+ const resId = fiNodeId + '=>resolves=>' + mId;
+ if (!seenNodes.has(resId)) {
+ seenNodes.add(resId);
+ els.push({ group: 'edges', data: {
+ id: resId,
+ source: fiNodeId,
+ target: mId,
+ kind: 'fam-resolves',
+ label: 'satisfies ' + predClassQn.qnName,
+ }});
+ }
+ }
+ }
}
}
}
}});
// Surface any type-family applications hiding inside the predicate
// (e.g. `Eq (TxOut era)` — `Eq` itself is the class, but `TxOut`
- // is a type family that must be defined for that era).
- addFamilyLinksFromArgs(pred.piArgs, instId, 'ctx-fam');
+ // is a type family that must be defined for that era). For each
+ // fam-instance we surface, we also try to resolve `pred.piClass`
+ // for the fam-instance's RHS and chain to the matching instance.
+ addFamilyLinksFromArgs(pred.piArgs, instId, 'ctx-fam', pred.piClass);
});
// Associated type families: when the focused class declares assoc
// data for instances of S whose head shape matches.
cls.ciSuperclasses.forEach((sc, si) => {
if (mutedSet.has(qid(sc.seSuperclass))) return;
- const reqArgs = sc.seArgs.map(a => substTypeArg(a, inst.iiArgs));
- // Same family-linkage as for context preds: a superclass requirement
- // like `Eq (TxOut era)` should also flag the `TxOut` family.
- addFamilyLinksFromArgs(reqArgs, instId, 'sc-fam-' + si);
+ // The chain helper needs the *unreduced* (only substituted) form
+ // so collectFamilyRefs still finds the FamilyApp nodes — if we
+ // hand it the post-reduction `reqArgs` below, the FamilyApps have
+ // already been replaced by some fam-instance's RHS and the chain
+ // never gets a chance to enumerate alternative fam-instances.
+ const subbedArgs = sc.seArgs.map(a => substTypeArgRaw(a, inst.iiArgs));
+ addFamilyLinksFromArgs(subbedArgs, instId, 'sc-fam-' + si, sc.seSuperclass);
+ // Direct-match path uses the reduced args as before.
+ const reqArgs = subbedArgs.map(reduceTypeArg);
const matched = findMatchingInstances(sc.seSuperclass, reqArgs);
const scClsId = ensureClassNode(sc.seSuperclass);
const reqLabel = 'needs ' + sc.seSuperclass.qnName + ' ' +
for (const m of matched) {
const mId = ensureInstanceNode(
m, sc.seSuperclass,
- 'inst:matched:' + qid(m.iiClass) + ':' + m._idx
+ 'inst:' + m._idx
);
// Also draw the matched instance under its class.
ensureClassNode(sc.seSuperclass);
return t;
}
+ // For the resolution chain we want to ask: "if the family @fa@ resolves
+ // via this particular fam-instance @fi@, what would the predicate look
+ // like?" That requires *bi-directional* unification — we may need to
+ // bind a tyvar on the pred side to a concrete value from fi (e.g. for
+ // @Pretty (Bag a)@ vs @type instance Bag Int = [Int]@, we hypothetically
+ // bind @a := Int@), and we may also need to bind a tyvar on fi's side
+ // to a value from the pred (e.g. fi's @a@ to pred's @era@).
+ function biUnify(pat, t, substPat, substT) {
+ if (!pat || !t) return false;
+ if (pat.tag === 'TyVarRef') {
+ const ix = pat.contents;
+ if (substPat[ix] !== undefined) return deepEqArg(substPat[ix], t);
+ substPat[ix] = t;
+ return true;
+ }
+ if (t.tag === 'TyVarRef') {
+ const ix = t.contents;
+ if (substT[ix] !== undefined) return deepEqArg(substT[ix], pat);
+ substT[ix] = pat;
+ return true;
+ }
+ if (pat.tag !== t.tag) return false;
+ if (pat.tag === 'TyConApp' || pat.tag === 'FamilyApp') {
+ const [pq, pa] = pat.contents;
+ const [tq, ta] = t.contents;
+ if (qid(pq) !== qid(tq)) return false;
+ if (pa.length !== ta.length) return false;
+ for (let i = 0; i < pa.length; i++) {
+ if (!biUnify(pa[i], ta[i], substPat, substT)) return false;
+ }
+ return true;
+ }
+ return pat.contents === t.contents;
+ }
+
+ // Resolve a predicate-arg expression as if the family @fa@ were to be
+ // realised via the fam-instance @fi@. Walks @t@ for the first
+ // @FamilyApp(fa, _)@, computes a bi-substitution by unifying @fi.fiArgs@
+ // against that @FamilyApp@'s args, then rewrites the entire expression
+ // using that substitution: tyvars of the predicate get pinned to fi's
+ // concrete values and the @FamilyApp@ itself is replaced with @fi.fiRhs@
+ // (substituted with fi's bindings).
+ //
+ // Return value:
+ //
+ // * @t@ unchanged — when the arg contains no @FamilyApp(fa, _)@ at
+ // all. The fi is irrelevant to this particular arg, but other args
+ // of the same predicate may still yield a successful resolution.
+ // * the rewritten arg — on success.
+ // * @null@ — when @t@ DOES contain @FamilyApp(fa, _)@ but the
+ // unification with this fi's LHS fails. This is the signal the
+ // caller uses to skip irrelevant fam-instances entirely (e.g.
+ // @TxIn ByronBlock@ vs a Shelley-flavoured predicate).
+ function replaceFamilyApp(t, fa, fi) {
+ let pivot = null; // first FamilyApp(fa, _) seen
+ function find(x) {
+ if (pivot) return;
+ if (!x || !x.tag) return;
+ if (x.tag === 'FamilyApp' && qid(x.contents[0]) === qid(fa)) {
+ pivot = x; return;
+ }
+ if (x.tag === 'TyConApp' || x.tag === 'FamilyApp') {
+ for (const sub of x.contents[1]) find(sub);
+ }
+ }
+ find(t);
+ if (!pivot) return t;
+ const pivotArgs = pivot.contents[1];
+ if (!fi.fiArgs || fi.fiArgs.length !== pivotArgs.length) return null;
+ const substFi = {}; // fi-side tyvars → pred-side values
+ const substPred = {}; // pred-side tyvars → fi-side values
+ for (let i = 0; i < pivotArgs.length; i++) {
+ if (!biUnify(fi.fiArgs[i], pivotArgs[i], substFi, substPred)) return null;
+ }
+ function go(x) {
+ if (!x || !x.tag) return x;
+ if (x.tag === 'TyVarRef') {
+ const ix = x.contents;
+ return substPred[ix] !== undefined ? substPred[ix] : x;
+ }
+ if (x.tag === 'FamilyApp' && qid(x.contents[0]) === qid(fa)) {
+ return applySubst(fi.fiRhs, substFi);
+ }
+ if (x.tag === 'TyConApp' || x.tag === 'FamilyApp') {
+ const [q, args] = x.contents;
+ return { tag: x.tag, contents: [q, args.map(go)] };
+ }
+ return x;
+ }
+ return go(t);
+ }
+
function deepEqArg(a, b) {
if (a === b) return true;
if (!a || !b || a.tag !== b.tag) return false;
color: '#065f46',
'border-color': '#10b981',
shape: 'round-rectangle',
+ 'text-wrap': 'wrap',
+ 'text-max-width': 280,
+ 'text-justification': 'left',
+ 'line-height': 1.3,
+ 'font-family': 'ui-monospace, "SF Mono", Menlo, Consolas, monospace',
},
},
{
width: 1.4,
},
},
+ // Family-resolution chain: fam-instance -> matching class instance,
+ // i.e. "this concrete RHS of the family makes that instance
+ // available". Distinct teal so the chain reads as a separate path
+ // from the via-family / fam-defines edges.
+ {
+ selector: 'edge[kind = "fam-resolves"]',
+ style: {
+ 'line-color': '#0d9488',
+ 'target-arrow-color': '#0d9488',
+ 'line-style': 'dotted',
+ width: 1.4,
+ 'font-size': 9,
+ },
+ },
// Highlight / dim
{ selector: '.dim', style: { opacity: 0.12 } },
{ selector: 'node.highlight', style: { 'border-width': 3, 'border-color': '#f97316' } },
// ---------------------------------------------------------------------------
// Interactions
- cy.on('tap', 'node', evt => {
- const n = evt.target;
- const data = n.data();
+ // Single tap = highlight + show details in the side panel.
+ // Double tap (same node within DOUBLE_TAP_MS) = drill in / pin a ghost.
+ // We implement this by hand because cytoscape's `tap` events don't carry
+ // a click count and `dblclick` doesn't fire reliably across browsers
+ // when cytoscape captures the pointer.
+ const DOUBLE_TAP_MS = 350;
+ const lastTap = { id: null, t: 0 };
- // In the classes view, when focus filtering is on:
- // * clicking a *ghost* node (visible because it's a one-hop superclass
- // of something pinned) promotes it to pinned, expanding the view.
- // * clicking a pinned node still drills in to its instance view.
+ function highlightOnly(n) {
+ cy.elements().addClass('dim').removeClass('highlight');
+ const inc = n.connectedEdges();
+ n.removeClass('dim').addClass('highlight');
+ inc.removeClass('dim').addClass('highlight');
+ inc.connectedNodes().removeClass('dim');
+ showSelection(n);
+ }
+
+ function drillInto(n) {
+ const data = n.data();
+ // In the classes view, when focus filtering is on, double-tapping a
+ // *ghost* (one-hop) class promotes it to pinned and expands the view.
if (state.view === 'classes' && focusSet.size > 0
&& data.kind === 'class' && data.ghost && classById.has(n.id())) {
pinClass(n.id());
return;
}
-
- // Class node → drill into its instance view (skip the already-focused
- // class in the current instance view).
+ // Class node → drill into its instance view.
if (data.kind === 'class' && !data.focused && classById.has(n.id())) {
switchToInstance(n.id());
return;
}
- // Family node → drill into its family view (skip the focused family in
- // the current family view).
+ // Family node → drill into its family view.
if (data.kind === 'family' && !data.focused && familyById.has(n.id())) {
switchToFamily(n.id());
return;
}
- // Otherwise: highlight node + incident edges (xdot-style).
- cy.elements().addClass('dim').removeClass('highlight');
- const inc = n.connectedEdges();
- n.removeClass('dim').addClass('highlight');
- inc.removeClass('dim').addClass('highlight');
- inc.connectedNodes().removeClass('dim');
- showSelection(n);
+ // Anything else (instance, fam-instance, focused-self, external):
+ // there's nothing to drill into — fall back to highlighting so the
+ // double-click still has a visible effect.
+ highlightOnly(n);
+ }
+
+ cy.on('tap', 'node', evt => {
+ const n = evt.target;
+ const id = n.id();
+ const now = Date.now();
+ const isDouble = lastTap.id === id && (now - lastTap.t) < DOUBLE_TAP_MS;
+ lastTap.id = id;
+ lastTap.t = now;
+ if (isDouble) {
+ // Reset the tracker so a third quick tap doesn't chain into a
+ // second drill-in.
+ lastTap.id = null;
+ drillInto(n);
+ } else {
+ highlightOnly(n);
+ }
});
cy.on('tap', evt => {