2e:null 2f:["$","title",null,{"children":"Agda input method fuzzy algo. comparison | qbane | Observable"}] 34:T409,renderResults = (results, decimalScore) => { const ul = DOM.element('ul') const els = results.map(({item, score, matches}) => { const itemSpan = html`` let prev = 0 for (const [a, b] of matches) { if (prev != a) itemSpan.appendChild(html`${item.slice(prev, a)}`) itemSpan.appendChild(html`${item.slice(a, b)}`) prev = b } if (prev != item.length) { itemSpan.appendChild(html`${item.slice(prev, item.length)}`) } const scoreDisp = decimalScore ? formatDecimals(score) : score const cands = dict[item].slice(0, 8).map(renderGlyph).join('') let candsEx = '' if (dict[item].length > 8) { candsEx = html` +${dict[item].length - 8}` } return html`

${itemSpan} (${cands}${candsEx}) ${scoreDisp}

` }) els.forEach(s => ul.appendChild(s)) return ul }35:[] 32:{"id":"1e47ef7a036042b8","slug":"agda-input-method-fuzzy","title":"Agda input method fuzzy algo. comparison","thumbnail":"564e445eaa946564feb8a41c8a804ea7bac38761ef6de982ed6f73d0a58b6da4","access_level":"public","create_time":"$D2025-12-30T14:44:25.590Z","update_time":"$D2026-09-14T13:51:21.783Z","view_time":null,"first_public_time":"$D2025-12-30T16:23:09.344Z","has_unpublished_edits":null,"fork":false,"stars":0,"starred":false,"owner":{"type":"team","id":"ec0e60aaa9ae681d","login":"qbane","name":"qbane","avatar_url":"https://avatars-next.observableusercontent.com/cc5506cefb6901edcab91e234d80c6d5bbd53092b8f9cb23a68b5cd0e30d0395","tier":"starter_2024"},"version":334,"publish_version":null,"role":null,"authored":false,"authors":[{"type":"individual","id":"cb0ad463bcac9eaa","login":"qbane","name":"qbane","avatar_url":"https://avatars-next.observableusercontent.com/cc5506cefb6901edcab91e234d80c6d5bbd53092b8f9cb23a68b5cd0e30d0395","tier":null}],"members":[{"type":"individual","id":"cb0ad463bcac9eaa","login":"qbane","name":"qbane","avatar_url":"https://avatars-next.observableusercontent.com/cc5506cefb6901edcab91e234d80c6d5bbd53092b8f9cb23a68b5cd0e30d0395","tier":null,"role":"editor"},{"type":"team","id":"ec0e60aaa9ae681d","login":"qbane","name":"qbane","avatar_url":"https://avatars-next.observableusercontent.com/cc5506cefb6901edcab91e234d80c6d5bbd53092b8f9cb23a68b5cd0e30d0395","tier":"starter_2024","role":"editor"}],"comments":[],"custom_thumbnail":false,"trashed":false,"lapsed":null,"subscribed":null,"forks":0,"collection":{"id":"de49574875f11e8b","slug":"playground","title":"Playground","owner":{"id":"ec0e60aaa9ae681d","login":"qbane","name":"qbane"}},"type":"notebook","body":{"title":"Agda input method fuzzy algo. comparison","cells":[{"id":0,"value":"# Agda input method fuzzy algo. comparison","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","output":"","database":"$undefined"},{"id":7,"value":"viewof query = Inputs.text({ label: 'Query' })","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":62,"value":"{\n if (query === '') {\n return html`(Query is empty)`\n }\n\n const entries = [\n { name: 'CM', fn: CMFuzzyMatcherEngine(keys) },\n { name: 'FZF', fn: FzfEngine(keys) },\n { name: 'QuickScore', fn: QuickScoreEngine(keys), decimalScore: true },\n ]\n \n return html`

\n ${entries.map(({name, fn, decimalScore}) => {\n const rs = fn(query)\n return html`

${name} (${rs.length}):

\n ${renderResults(rs, decimalScore)}\n

`\n })}\n

`\n}","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":230,"value":"## Issues\n\n* CM includes lowercase result when the query is lowercase only (e.g. `alpha`/`Alpha`)\n* QuickScore favors longer results while Fzf does not (is possible to do so via a built-in tiebreaker); e.g. `zdig`.\n* Some candidates beginning `^\\` have peculiarly long names (and contains spaces in them). Not sure how much I can do...","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","output":"","database":"$undefined"},{"id":228,"value":"---","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","output":"","database":"$undefined"},{"id":60,"value":"$34","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":242,"value":"---","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","output":"","database":"$undefined"},{"id":225,"value":"# Engines","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","output":"","database":"$undefined"},{"id":158,"value":"CMFuzzyMatcherEngine = keys => s => {\n const fm = new FuzzyMatcher(s)\n return keys.map(item => {\n const ok = fm.match(item)\n if (!ok) return null\n const { score, matched } = fm\n const matches = []\n for (let i = 0; i < matched.length; i += 2) {\n matches.push([matched[i], matched[i + 1]])\n }\n return { item, score, matches }\n })\n .filter(result => result && result.matches.length)\n // assuming the sort is stable: \n // https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/Array/sort#sort_stability\n .sort((a, b) => b.score - a.score)\n}","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":26,"value":"FzfEngine = {\n const fzf = await import('https://esm.sh/fzf')\n\n function positionsToIntervals(xs) {\n if (!xs.length) return []\n let start = xs[0], prev = xs[0]\n const ret = []\n for (let idx = 1; idx < xs.length; idx++) {\n const cur = xs[idx]\n if (cur == prev + 1) {\n prev++\n continue\n }\n ret.push([start, prev + 1])\n start = prev = cur\n }\n ret.push([start, prev + 1])\n return ret\n }\n \n return keys => {\n const coll = new fzf.Fzf(keys, {\n casing: 'case-sensitive',\n tiebreakers: [fzf.byStartAsc],\n })\n \n return s => coll.find(s).map(({ item, score, positions }) => ({\n item, score, matches: positionsToIntervals(Array.from(positions).sort((a, b) => a - b)),\n }))\n }\n}","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":23,"value":"QuickScoreEngine = {\n const QS = await import('quick-score@0.0.14')\n return keys => {\n const qs = new QS.QuickScore(keys, {\n transformString: s => s,\n config: QS.createConfig({\n wordSeparators: ' \\t\\n\\r',\n })\n })\n \n return s => qs.search(s).map(({ item, score, matches }) => ({\n item, score, matches,\n }))\n }\n}","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":198,"value":"---","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","output":"","database":"$undefined"},{"id":160,"value":"import { FuzzyMatcher } from '@qbane/cm6-fuzzy-matcher'","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":200,"value":"formatDecimals = {\n const fmt = Intl.NumberFormat(undefined, {\n minimumFractionDigits: 2,\n maximumFractionDigits: 4,\n })\n return n => fmt.format(n)\n}","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":143,"value":"renderGlyph = s => {\n // TODO: space\n if (s.match(/\\p{Mn}/u)) {\n return '\\u25cc' + s\n }\n return s\n}","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":287,"value":"---","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","output":"","database":"$undefined"},{"id":5,"value":"dict = fetch('https://raw.githubusercontent.com/agda-web/agda-input/refs/heads/master/out/dict.json').then(x => x.json())","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":123,"value":"keys = Object.keys(dict)","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":247,"value":"values = Array.from(new Set(Object.values(dict).flat())).sort()","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":293,"value":"trie = {\n const trie = {}\n function insert(key, value) {\n let node = trie\n for (let idx = 0; idx < key.length; idx++) {\n const chr = key[idx]\n node[chr] ??= {}\n node = node[chr]\n }\n node['>>'] = value\n }\n\n for (const [k, v] of Object.entries(dict)) {\n insert(k, v)\n }\n\n return trie\n}","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":294,"value":"nonPrefixFreeKeys = {\n const result = []\n function scan(node, prefix) {\n const kvs = Object.entries(node)\n let hasLeaf = false\n for (const [k, v] of kvs) {\n if (k == '>>') {\n hasLeaf = true\n continue\n }\n scan(v, prefix + k)\n }\n if (hasLeaf && kvs.length > 1) {\n result.push([prefix, node])\n }\n }\n\n scan(trie, '')\n return result\n}","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":295,"value":"reverseMap = {\n const result = new Map()\n for (const [k, vs] of Object.entries(dict)) {\n for (let i = 0; i < vs.length; i++) {\n const arr = result.getOrInsertComputed(vs[i], () => [])\n arr.push(\n vs.length == 1 ? { key: k, index: -1 } : { key: k, index: i, len: vs.length })\n }\n }\n return result\n}","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":296,"value":"trickyToType = {\n return Array.from(reverseMap.entries().filter(([k, xs]) => {\n return !(xs.some(x => x.index === -1) || xs.length == 1)\n }))\n}","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":289,"value":"# \"Tricky\" characters","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","output":"","database":"$undefined"},{"id":245,"value":"values.filter(x => x.match(/\\p{Mn}/u)).map(renderGlyph)","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":251,"value":"html`Z category:

⟧${'\\u200b'}${c}${'\\u200b'}⟦: ${cp}

`","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":267,"value":"html`C category:

⟧\\u200b${c}\\u200b⟦: ${cp}

`","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":292,"value":"keys.filter(x => x.includes(' ') && !x.startsWith('^\\\\'))","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","output":"$undefined","database":"$undefined"},{"id":10,"value":"","pinned":false,"hidden":false,"mode":"html","author":"$undefined","summary":"$undefined","output":"","database":"$undefined"}],"files":"$W35","stdlib":"2","titling":"auto"}} 33:"$32:body"