diff --git a/compiler/src/check.rs b/compiler/src/check.rs index 7a26a9a..8dcec25 100644 --- a/compiler/src/check.rs +++ b/compiler/src/check.rs @@ -221,6 +221,8 @@ struct Sym<'a> { /// O-3: not a name but a prop's argument, stored — its captures are the caller's ("*": all of props) prop_of: Option<(RId, String)>, maps_records: bool, + /// a declared equation, and whether it is deferred: a guess may sit over one that is not (AC-3, ST-5c) + eq_decl: Option, rows: Option>, comp: Option<&'a Decl>, expr: Option<(&'a Expr, EId)>, @@ -253,6 +255,7 @@ impl<'a> Sym<'a> { ret_captures: None, prop_of: None, maps_records: false, + eq_decl: None, rows: None, comp: None, expr: None, @@ -1166,7 +1169,8 @@ impl<'a> Checker<'a> { let r = self.region(Some(region), "component", true, Some(name.clone())); sym.comp_region = Some(r); } - Decl::Eq { e, key, .. } => { + Decl::Eq { e, key, deferred, .. } => { + sym.eq_decl = Some(*deferred); sym.maps_records = key.is_none() && maps_into_records(e); if let ExprKind::Id(n) = &e.k { if let Some(t) = self.lookup(env, n) { @@ -2332,7 +2336,16 @@ impl<'a> Checker<'a> { self.model.write(tsym, op, !target.path.is_empty()); if let Some(t) = tsym { let k = self.syms[t].kind; - if k != SymKind::Source { + // AC-3: a guess may sit over an equation (Solid's createOptimistic(fn)); it is not a write of the truth + let guessable = op == "optimistic" && k == SymKind::Eq && self.syms[t].eq_decl.is_some() && !self.syms[t].param && self.syms[t].imported.is_none(); + if guessable && self.syms[t].eq_decl == Some(true) { + self.err( + "GUESS_ON_DEFERRED", + "AC-3", + format!("{} is deferred: its value is a lagging copy (V-16), so nothing would confirm a guess on it — guess the equation it lags", target.name), + ); + } else if guessable { + } else if k != SymKind::Source { let what = match k { SymKind::Eq => "an equation".to_string(), SymKind::Props => "props".to_string(), diff --git a/compiler/src/emit.rs b/compiler/src/emit.rs index dfc058d..342a660 100644 --- a/compiler/src/emit.rs +++ b/compiler/src/emit.rs @@ -626,8 +626,11 @@ impl<'p> Gen<'p> { } // SF-1d: a server fn, not an accessor Decl::Eq { name, e, .. } if unwrap_server(e).is_some() => self.set(env, name, val(mg(name))), - Decl::Eq { name, .. } => { + Decl::Eq { name, e, deferred, .. } => { let mut b = bind(Kind::Acc, mg(name)); + if self.guessed_eq(name, e, *deferred) { + b.w = Some(format!("w${name}")); + } b.prev = self.u.prev_of.contains(name).then(|| format!("p${name}")); self.set(env, name, b); } @@ -952,6 +955,19 @@ impl<'p> Gen<'p> { prev(&mut out); Ok(out) } + Decl::Eq { name, e, key, deferred, .. } if self.guessed_eq(name, e, *deferred) => { + // AC-3 over an equation: createOptimistic(fn) / createOptimisticStore(fn, seed) — derived, its setter only guesses + let lv = self.loading_value(e, env)?; + let mode = obj(vec![("optimistic", E::Bool(true)), ("structured", E::Bool(self.u.paths.contains(name) || key.is_some())), ("derived", E::Bool(true))]); + let x = self.expr(e, env, &Ctx { tail: true, self_: Some(name.clone()), ..Ctx::default() })?; + let mut args = vec![str(name.clone()), arrow(&["__prev"], x), lv, mode]; + if let Some(k) = key { + args.push(str(k.clone())); + } + let mut out = vec![S::Const(pair(), rtc("question", args)), self.reg(name, b, true)]; + prev(&mut out); + Ok(out) + } Decl::Eq { name, e, key, deferred, .. } => { let fin = |mut out: Vec, g: &Self| { out.push(g.reg(name, b, false)); @@ -1516,6 +1532,10 @@ impl<'p> Gen<'p> { Ok(out) } /// A region's body as a child: its declarations, then its view (a function body, so it is owned where it is called). + /// An equation a guess sits over (AC-3): not deferred, not a draft, not a wrapped server fn. + fn guessed_eq(&self, name: &str, e: &Expr, deferred: bool) -> bool { + self.u.optimistic.contains(name) && !deferred && !matches!(&e.k, ExprKind::Draft { .. }) && unwrap_server(e).is_none() + } fn region_fn(&mut self, decls: &[Decl], view: &[Markup], env: Env, param: Option, narrow: Option<(String, Bind)>, bind_name: Option) -> R { let inner = self.new_env(Some(env)); let mut pre = vec![]; diff --git a/guide/async.md b/guide/async.md index 635abcd..c5525cc 100644 --- a/guide/async.md +++ b/guide/async.md @@ -85,7 +85,7 @@ by what the screen should do: | You want | Write | | --- | --- | -| Show a value now, and take it back if the action fails | `guess x := v` (x is a source with a question: `source x = …`) | +| Show a value now, and take it back if the action fails | `guess x := v` (x is an equation, `x = …`, or a source with a question, `source x = …`) | | `pending? x` true while the action runs | `affects x` | | Land a UI write now and keep it (close a menu, clear a message) | `onFlush(() => { x := v })` (EF-8) | | Record the server's answer | `x := answer` after the `await` | diff --git a/guide/diagnostics.md b/guide/diagnostics.md index b634c89..2b4e901 100644 --- a/guide/diagnostics.md +++ b/guide/diagnostics.md @@ -462,8 +462,9 @@ export default component App() { ### GUESS_NO_QUESTION -A guess is confirmed or replaced by the answer to a question, so `guess` writes a source declared with `=` (a -source with a question, ST-5c). A source seeded with `:=` has no question; write it plainly. +A guess is confirmed or replaced by the answer to a question, so `guess` writes an equation or a source declared +with `=` (a source with a question, ST-5c). A source seeded with `:=` has no question; write it plainly, or with +`onFlush` if it is a reset that should land now (EF-8). ```rx before export default component App() { @@ -481,6 +482,31 @@ export default component App() { } ``` +### GUESS_ON_DEFERRED + +A `deferred` equation is a lagging copy of another value (V-16), so nothing would confirm a guess on it. Guess the +value it lags. + +```rx before +export default component App() { + source name := "Ann" + shown = name + deferred later = shown + action fix() { guess later := "Zed"; await fetch("x") catch (e) => null } + +} +``` + +```rx after +export default component App() { + source name := "Ann" + shown = name + deferred later = shown + action fix() { guess shown := "Zed"; await fetch("x") catch (e) => null } + +} +``` + ### INVALID_REFRESH_TARGET `refresh x` re-asks `x`'s question (AC-4), so `x` is an equation that awaits or a source declared with `=`. A source diff --git a/guide/reference.md b/guide/reference.md index 5a0c36f..e691484 100644 --- a/guide/reference.md +++ b/guide/reference.md @@ -58,7 +58,7 @@ Expr ::= TypeScript's, without assignment, `this`, `function`, `new` on rea - A failure inside the body must be caught there: `try { … } catch (e) { … }` (R-f-6, AC-7). The catch runs inside the same change: its writes land with the body's end. A rejected body commits its plain writes and reverts its guesses (AC-1, DV-2). -- `guess x := e`: a guess on a source with a question (`source x = …`), shown now, kept until the action's change +- `guess x := e`: a guess on an equation (`x = …`) or a source with a question (`source x = …`), shown now, kept until the action's change commits or `x`'s own answer differs (AC-3, H-11). Guesses on one source hold together. - `refresh x`: asks `x` again, quietly (no `pending?`; the old value stays up until the new one lands). Inside an action, the answer lands with the action's commit (AC-4). diff --git a/ref/compile/emit.ts b/ref/compile/emit.ts index 8916109..3caf7c3 100644 --- a/ref/compile/emit.ts +++ b/ref/compile/emit.ts @@ -241,7 +241,7 @@ class Gen { if (d.k === "error" || d.k === "context") env.vars.set(d.name, { kind: "val", js: mg(d.name) }); if (d.k === "source") env.vars.set(d.name, { kind: "src", js: mg(d.name), w: `w$${d.name}`, prev: this.u.prevOf.has(d.name) ? `p$${d.name}` : undefined }); if (d.k === "eq" && unwrapServer(d.e)) { env.vars.set(d.name, { kind: "val", js: mg(d.name) }); continue; } // SF-1d: a server fn, not an accessor - if (d.k === "eq") env.vars.set(d.name, { kind: d.e.k === "call" && d.e.f.k === "id" && env.lookup(d.e.f.name)?.kind === "ifn" ? "acc" : "acc", js: mg(d.name), prev: this.u.prevOf.has(d.name) ? `p$${d.name}` : undefined }); + if (d.k === "eq") env.vars.set(d.name, { kind: d.e.k === "call" && d.e.f.k === "id" && env.lookup(d.e.f.name)?.kind === "ifn" ? "acc" : "acc", js: mg(d.name), w: this.guessedEq(d) ? `w$${d.name}` : undefined, prev: this.u.prevOf.has(d.name) ? `p$${d.name}` : undefined }); } for (const d of decls) if (d.k === "import" && !d.resolved) for (const { name, alias } of d.names) { const v = !d.from.startsWith(".") && !BUILTINS.has(name) && name !== "log" ? `w$${alias}` : name === "log" ? "__B.log" : d.declaredErrors?.includes(name) ? `__rt.jsError(${J(name)})` : BUILTINS.has(name) ? `__B.${name}` : d.from.endsWith("/api") ? `__rt.api(${J(name)})` : null; @@ -313,6 +313,8 @@ class Gen { }).join("\n"); } private hoistAll(es: Expr[], env: Env, pad: string): string[] { return es.map(x => this.hoist(null, x, env, pad, false)).filter(Boolean); } + /** An equation a guess sits over (AC-3): not deferred, not a draft, not a wrapped server fn. */ + private guessedEq(d: Extract): boolean { return this.u.optimistic.has(d.name) && !d.deferred && d.e.k !== "draft" && !unwrapServer(d.e); } private value1(d: Decl, env: Env, ind: number, b: Bind): string { const pad = " ".repeat(ind * 2); const prev = b.prev ? `\n${pad}const ${b.prev} = __rt.pre(${b.js});` : ""; @@ -323,6 +325,11 @@ class Gen { return `${pad}const [${b.js}, ${b.w}] = __rt.question(${J(d.name)}, (__prev) => ${this.expr(d.init, env, { imp: false, tail: true, self: d.name })}, ${lv}, ${mode}${d.key ? `, ${J(d.key)}` : ""});\n${pad}__rt.reg(${J(d.name)}, { get: ${b.js}, w: ${b.w} });${prev}`; } if (d.k !== "eq") throw new CompileError("unreachable"); + if (this.guessedEq(d)) { // AC-3 over an equation: createOptimistic(fn) / createOptimisticStore(fn, seed) — derived, its setter only guesses + const lv = this.loadingValue(d.e, env); + const mode = `{ optimistic: true, structured: ${this.u.paths.has(d.name) || !!d.key}, derived: true }`; + return `${pad}const [${b.js}, ${b.w}] = __rt.question(${J(d.name)}, (__prev) => ${this.expr(d.e, env, { imp: false, tail: true, self: d.name })}, ${lv}, ${mode}${d.key ? `, ${J(d.key)}` : ""});\n${pad}__rt.reg(${J(d.name)}, { get: ${b.js}, w: ${b.w} });${prev}`; + } const reg = `\n${pad}__rt.reg(${J(d.name)}, { get: ${b.js} });${prev}`; if (d.e.k === "draft") { // ST-3 const seed = d.e.seed; if (seed.k !== "pre" || seed.name !== d.name || !seed.init) throw new CompileError("a draft's seed must be `pre self -> seed`"); diff --git a/ref/compile/rt-server.ts b/ref/compile/rt-server.ts index 8d19c4d..48f629e 100644 --- a/ref/compile/rt-server.ts +++ b/ref/compile/rt-server.ts @@ -131,9 +131,10 @@ export function createApp(opts: { api?: Record unknown> if (typeof init === "object" && init !== null) { const [store] = createStore(init as any); const [get] = createSignal(store); return ro(get as Acc); } const [get] = createSignal(init); return ro(get as Acc); }, - question(name: string, compute: (prev: unknown) => unknown, o: { loadingValue?: unknown } | undefined, mode: { optimistic: boolean; structured: boolean }, key?: string): [Acc, Writer] { + question(name: string, compute: (prev: unknown) => unknown, o: { loadingValue?: unknown } | undefined, mode: { optimistic: boolean; structured: boolean; derived?: boolean }, key?: string): [Acc, Writer] { const fn = named(name, compute); if (mode.optimistic && mode.structured) { const [store] = (createOptimisticStore as any)((draft: any) => { const r = fn(draft); if (r instanceof Flight || r instanceof Promise) return (async () => assignDraft(draft, r instanceof Flight ? await r.first : await r))(); assignDraft(draft, r); }, key ? [] : {}, key ? { key } : undefined); return ro(() => store); } + if (mode.optimistic && mode.derived) { const [get] = createOptimistic(fn as any, o as any); return ro(get as Acc); } // AC-3 over an equation: the client's createOptimistic(fn), so the owner trees (and hydration keys) match if (mode.optimistic) { const [truth] = createSignal(fn as any, o as any); const [get] = createOptimistic(() => (truth as Acc)()); return ro(get as Acc); } if (mode.structured) { const [store] = (createStore as any)(async (draft: Record) => { const r = fn(draft); const v = r instanceof Flight ? await r.first : await r; if (v && typeof v === "object") { for (const k of Object.keys(draft)) if (!(k in (v as object))) delete draft[k]; Object.assign(draft, v); } }, {}); diff --git a/ref/compile/rt-web.ts b/ref/compile/rt-web.ts index 41e71dc..0b49df8 100644 --- a/ref/compile/rt-web.ts +++ b/ref/compile/rt-web.ts @@ -171,7 +171,7 @@ export function createApp(opts: { root: any; api?: Record unknown, opts: { loadingValue?: unknown } | undefined, mode: { optimistic: boolean; structured: boolean }, key?: string): [Acc, Writer] { + question(name: string, compute: (prev: unknown) => unknown, opts: { loadingValue?: unknown } | undefined, mode: { optimistic: boolean; structured: boolean; derived?: boolean }, key?: string): [Acc, Writer] { const fn = named(name, compute); if (mode.optimistic && mode.structured) { // AC-3 path targets: createOptimisticStore(fn, seed) — the derive writes its draft; the setter guesses per key const [store, setStore] = (createOptimisticStore as any)((draft: any) => { const r = fn(draft); if (r instanceof Flight || r instanceof Promise) return (async () => assignDraft(draft, r instanceof Flight ? await r.first : await r))(); assignDraft(draft, r); }, key ? [] : {}, key ? { key } : undefined); @@ -179,6 +179,11 @@ export function createApp(opts: { root: any; api?: Record { throw new Error("a plain write to an optimistic store is not lowered yet"); }; return [get, { set: plain, path: plain, guess: (v, keys = []) => setStore((d: any) => { if (keys.length === 0) return typeof v === "function" ? (v as (x: unknown) => unknown)(d) : v; /* a whole guess is the setter\'s return, which Solid diffs shallowly against the view as guesses */ let o = d; for (const k of keys.slice(0, -1)) o = o[k]; const last = keys[keys.length - 1]; o[last] = typeof v === "function" ? (v as (x: unknown) => unknown)(o[last]) : v; }) }]; } + if (mode.optimistic && mode.derived) { // AC-3 over an equation: createOptimistic(fn), whose setter only guesses + const plain = () => { throw new Error("a plain write to an equation"); }; + const [get, setGuess] = createOptimistic(fn as any, opts as any); + return [get as Acc, { set: plain, path: plain, guess: setGuess as any }]; + } if (mode.optimistic) { const [truth, setTruth] = createSignal(fn as any, opts as any); const [get, setGuess] = createOptimistic(() => truth()); diff --git a/ref/compile/rt.ts b/ref/compile/rt.ts index 92bc889..e97a113 100644 --- a/ref/compile/rt.ts +++ b/ref/compile/rt.ts @@ -181,7 +181,7 @@ export function createApp(opts: { api?: Record unknown> }, /** `source x = e` (ST-5): createSignal(fn); with a guess written to it, a createOptimistic layer over that truth (AC-3); * written or probed by path, createStore(fn, {}) whose derive writes its draft. */ - question(name: string, compute: (prev: unknown) => unknown, opts: { loadingValue?: unknown } | undefined, mode: { optimistic: boolean; structured: boolean }, key?: string): [Acc, Writer] { + question(name: string, compute: (prev: unknown) => unknown, opts: { loadingValue?: unknown } | undefined, mode: { optimistic: boolean; structured: boolean; derived?: boolean }, key?: string): [Acc, Writer] { const fn = named(name, compute); if (mode.optimistic && mode.structured) { // AC-3 path targets: createOptimisticStore(fn, seed) — the derive writes its draft; the setter guesses per key const [store, setStore] = (createOptimisticStore as any)((draft: any) => { const r = fn(draft); if (r instanceof Flight || r instanceof Promise) return (async () => assignDraft(draft, r instanceof Flight ? await r.first : await r))(); assignDraft(draft, r); }, key ? [] : {}, key ? { key } : undefined); @@ -189,6 +189,11 @@ export function createApp(opts: { api?: Record unknown> const plain = () => { throw new Error("a plain write to an optimistic store is not lowered yet"); }; return [get, { set: plain, path: plain, guess: (v, keys = []) => setStore((d: any) => { if (keys.length === 0) return typeof v === "function" ? (v as (x: unknown) => unknown)(d) : v; /* a whole guess is the setter\'s return, which Solid diffs shallowly against the view as guesses */ let o = d; for (const k of keys.slice(0, -1)) o = o[k]; const last = keys[keys.length - 1]; o[last] = typeof v === "function" ? (v as (x: unknown) => unknown)(o[last]) : v; }) }]; } + if (mode.optimistic && mode.derived) { // AC-3 over an equation: createOptimistic(fn), whose setter only guesses + const plain = () => { throw new Error("a plain write to an equation"); }; + const [get, setGuess] = createOptimistic(fn as any, opts as any); + return [get as Acc, { set: plain, path: plain, guess: setGuess as any }]; + } if (mode.optimistic) { const [truth, setTruth] = createSignal(fn as any, opts as any); const [get, setGuess] = createOptimistic(() => truth()); diff --git a/ref/oracle/lower.ts b/ref/oracle/lower.ts index 5cbff4d..b434412 100644 --- a/ref/oracle/lower.ts +++ b/ref/oracle/lower.ts @@ -282,6 +282,19 @@ export class Oracle { scope.vars.set(d.name, { k: "memo", get: () => proj }); break; } + if (this.optimisticTargets.has(d.name) && !d.deferred) { // AC-3 over an equation: Solid's createOptimistic(fn) / createOptimisticStore(fn, seed) — derived, its setter only guesses + const compute = this.computeOf(d.name, d.e, scope); + const plain = () => { throw new Unsupported("a plain write to an equation"); }; + if (this.pathTargets.has(d.name) || d.key) { + const derive = async (draft: any) => { const r = compute(draft); const v = r instanceof Flight ? await r.first : await r; assignDraft(draft, v); }; + const [store, setStore] = (createOptimisticStore as any)(derive, d.key ? [] : {}, d.key ? { key: d.key } : undefined); + scope.vars.set(d.name, { k: "store", get: () => store, set: plain, setPath: plain, question: true, setGuess: setStore }); + } else { + const [get, setGuess] = createOptimistic(compute as any, this.loadingValue(d.e, scope) as any); + scope.vars.set(d.name, { k: "sig", get, set: plain as any, setGuess: setGuess as any, question: true, optimistic: true }); + } + break; + } if (d.key) { // ST-4: a keyed projection const compute = this.computeOf(d.name, d.e, scope); const src = createMemo(() => compute(undefined) as any, this.loadingValue(d.e, scope) as any); // the answer (sync, or the tail await's) is a memo; the projection reconciles it by key (found by S-ai2-search) diff --git a/ref/src/check.ts b/ref/src/check.ts index 7b0113b..c0ff889 100644 --- a/ref/src/check.ts +++ b/ref/src/check.ts @@ -73,6 +73,7 @@ type SymKind = "source" | "eq" | "props" | "value" | "fn" | "action" | "comp" | type Sym = { kind: SymKind; name: string; region: Region; line: number; question?: boolean; // source x = e + eqDecl?: Extract; // a declared equation: a guess may sit over it (AC-3, ST-5c) io?: boolean; // calling it is io (R-io) param?: boolean; // a fn's parameter: never a write target (O-4) instantiating?: boolean; // fn with ref params or declarations (E-9) @@ -377,6 +378,7 @@ class Checker { if (d.k === "action") sym.io = true; // R-io-2: an action is io if (d.k === "fn") { sym.params = d.params; sym.instantiating = d.params.some(p => p.ref) || d.decls.length > 0; sym.fnDecl = d; sym.declEnv = env; } if (d.k === "component") { sym.comp = d; sym.compRegion = this.region(env.region, "component", { component: true, name: d.name }); this.compSyms.set(sym.compRegion, sym); } + if (d.k === "eq") sym.eqDecl = d; if (d.k === "eq") { sym.mapsRecords = !d.key && mapsIntoRecords(d.e); if (d.e.k === "id") { const t = env.lookup(d.e.name); if (t?.io) sym.io = true; } } if (d.k === "eq") { const sf = unwrapServer(d.e); if (sf) { sym.kind = "server"; sym.params = sf.params.map(name => ({ name, ref: false })); this.serverExprs.set(sf, sym); } } // SF-1d: a wrapped server fn is one, its rows the function's this.bind(env, d.name, sym); @@ -837,7 +839,10 @@ class Checker { } else { target = this.resolve(s.target.name, env, ctx); this.model.write(target, s.k, s.target.path.length > 0); - if (target && target.kind !== "source") this.err("WRITE_TO_NON_SOURCE", "W-1", `${s.target.name} is ${target.kind === "eq" ? "an equation" : target.kind === "props" ? "props" : `a ${target.kind}`}: only sources are written (W-1)${target.kind === "props" || target.kind === "value" || target.param ? " — a source is written only in the region that declares it: have its owner pass an action that writes it (O-4)" : ""}`); + const guessable = s.k === "optimistic" && target?.kind === "eq" && !!target.eqDecl && !target.param && !target.imported; // AC-3: a guess may sit over an equation (Solid's createOptimistic(fn)); it is not a write of the truth + if (guessable && target!.eqDecl!.deferred) this.err("GUESS_ON_DEFERRED", "AC-3", `${s.target.name} is deferred: its value is a lagging copy (V-16), so nothing would confirm a guess on it — guess the equation it lags`); + else if (guessable) {} + else if (target && target.kind !== "source") this.err("WRITE_TO_NON_SOURCE", "W-1", `${s.target.name} is ${target.kind === "eq" ? "an equation" : target.kind === "props" ? "props" : `a ${target.kind}`}: only sources are written (W-1)${target.kind === "props" || target.kind === "value" || target.param ? " — a source is written only in the region that declares it: have its owner pass an action that writes it (O-4)" : ""}`); else if (target?.imported) this.err("WRITE_TO_NON_SOURCE", "MO-2", `${s.target.name} is a source of ${target.imported}: a module boundary is a value boundary — write it through an action ${target.imported} exports`); } if (s.k === "optimistic") { diff --git a/ref/src/runtime.ts b/ref/src/runtime.ts index d60894d..42dc821 100644 --- a/ref/src/runtime.ts +++ b/ref/src/runtime.ts @@ -1102,7 +1102,7 @@ export class Runtime { else if (s.k === "optimistic") { if (!run.action) throw new RuleError("GUESS_OUTSIDE_HOLD", "a guess outside an action body"); const n = this.nodeNamed(s.target.name, region); - if (!n || !n.question) throw new RuleError("GUESS_NO_QUESTION", `${s.target.name} is not a source with a question (source x = e)`); + if (!n || !(n.question || (n.kind === "eq" && !n.deferred && n.compute))) throw new RuleError("GUESS_NO_QUESTION", `${s.target.name} is not a source with a question (source x = e)`); const path = s.target.path.map(p => typeof p === "string" ? p : String(this.ev(p, region, env))); this.pendingGuesses.push({ node: n, path, value: this.ev(s.e, region, env) }); } else if (s.k === "write") { diff --git a/scenarios/S-guess-equation-store.md b/scenarios/S-guess-equation-store.md new file mode 100644 index 0000000..0393611 --- /dev/null +++ b/scenarios/S-guess-equation-store.md @@ -0,0 +1,50 @@ +# S-guess-equation-store — a guess by path over a keyed equation (Solid `createOptimisticStore(fn, seed)`) + +Rules: AC-3, ST-5c, ST-4, H-11, D-34. + +## Program + +```rx +export default component App() { + source todos key id = await fetch("todos") + open key id = todos.filter(t => !t.done) + action finish(i) { + try { guess open[i].title := "…"; await fetch("save"); refresh todos } catch {} + } + + errored fallback(e) {

error: {e.message}

} { + {loading fallback {

loading

} { +
    {for t in open {
  • {t.title}
    • }}
+

{len(todos)}

+ }} + } +} +``` + +`open` is a keyed equation, never written. A guess by path sits over one +row of it (ST-5c), as Solid's `createOptimisticStore(fn, seed)` with the +filter as its derive: the rest of `open` is the truth beneath the guess. +`todos`, the source it is derived from, does not move. + +## Frames + +| instant | action | frame | +| ------- | ---------------------------------------------------------------------------------------- | ---------- | +| 0 | mount | `loading` | +| 1 | resolve todos [{ id: 1, title: "A", done: false }, { id: 2, title: "B", done: false }] | `AB2` | +| 2 | handler `finish(0)` | `…B2` | +| 3 | resolve "save" 0 | `…B2` | +| 4 | resolve todos [{ id: 1, title: "A2", done: false }, { id: 2, title: "B", done: false }] | `A2B2` | + +Instant 2: the guess shows on the one row. Instant 3: the re-ask of +`todos` is in flight, and `open` follows it, so the guess waits for that +answer (D-34). Instant 4: the answer differs at the guessed key, so it +corrects the row, and the action's change commits in one frame. + +## Variant: the save fails + +| instant | action | frame | +| ------- | ------------------------- | ---------- | +| 3 | reject "save" "boom" | `AB2` | + +Nothing is re-asked, so the guess gives way to the truth at hand (D-34). diff --git a/scenarios/S-guess-equation.md b/scenarios/S-guess-equation.md new file mode 100644 index 0000000..c997dd8 --- /dev/null +++ b/scenarios/S-guess-equation.md @@ -0,0 +1,101 @@ +# S-guess-equation — a guess over an equation, and over a prop through one (Solid `createOptimistic(fn)`) + +Rules: AC-3, ST-5c, H-11, D-34, W-1, O-4, RG-4b. + +## Program + +```rx +component Title(props) { + shown = props.title + action rename(t: string) { + guess shown := t + try { let r = await fetch("rename") catch (e) => props.title; props.done(r) } catch {} + } +

{shown}

+ +} + +export default component App() { + source name := "Ann" + upper = name.toUpperCase() + action shout() { try { guess upper := "ANN!"; await fetch("shout") } catch {} } + action setName(v: string) { name := v } + + + <p>{name} {upper}</p> + <button onClick={() => { shout() }}>shout</button> +} +``` + +`shown` and `upper` are equations, never written: a guess is not a write of +the truth, so it may sit over one (AC-3, ST-5c). Each lowers to Solid's +`createOptimistic(fn)`, whose setter only guesses. A guess over a prop is a +guess over the child's own equation of it: it shows where the child reads +`shown`, and the parent's `name` does not move until the answer is written. + +## Frames + +| instant | action | frame | +| ------- | ------------------------------ | ---------------------------------- | +| 0 | mount | `AnnrenameAnn ANNshout` | +| 1 | handler `rename("Bob")` | `BobrenameAnn ANNshout` | +| 2 | resolve "rename" "Bob" | `BobrenameBob BOBshout` | +| 3 | handler `shout()` | `BobrenameBob ANN!shout` | +| 4 | resolve "shout" 0 | `BobrenameBob BOBshout` | + +Instant 1: the guess shows in the child only; the parent's `name` and +`upper` are unchanged (H-11). Instant 2: the answer is written as the +truth through the action the parent passed (O-4), `shown` re-derives to the +same value, the guess confirms silently. Instant 3: a guess over an +equation of a source. Instant 4: the body ends with nothing answering +`upper`, so the guess gives way to the truth at hand (D-34). + +## Variant: the rename fails + +| instant | action | frame | +| ------- | ------------------------------ | ---------------------------------- | +| 2 | reject "rename" "boom" | `AnnrenameAnn ANNshout` | + +The catch writes the prop's own value back; the guess reverts with the +body's end (AC-1, D-34). + +## Rejected variants + +```rx +-- reject: WRITE_TO_NON_SOURCE +export default component App() { + source name := "Ann" + upper = name.toUpperCase() + <button onClick={() => { upper := "X" }}>{upper}</button> +} +``` + +A plain write to an equation stays an error (W-1): only the guess may sit +over one. + +```rx +-- reject: WRITE_TO_NON_SOURCE +component Title(props) { + action rename(t: string) { guess props.title := t; await fetch("x") catch (e) => null } + <button onClick={() => { rename("Bob") }}>{props.title}</button> +} +export default component App() { + <Title title="Ann" /> +} +``` + +A guess on `props` itself stays an error (O-4): it would read as the +owner's value changing. Guess over the child's own equation of it. + +```rx +-- reject: GUESS_ON_DEFERRED +export default component App() { + source name := "Ann" + deferred later = name + action fix() { guess later := "Zed"; await fetch("x") catch (e) => null } + <button onClick={() => { fix() }}>{later}</button> +} +``` + +A deferred equation's value is a lagging copy (V-16); a guess has nothing +to confirm it there. diff --git a/spec/06-stores.md b/spec/06-stores.md index 32a83a9..661a145 100644 --- a/spec/06-stores.md +++ b/spec/06-stores.md @@ -84,8 +84,18 @@ selected = draft(pre selected -> {}) { d[id] := true; d[prevId] := false } a `createOptimistic(() => truth())` layer. - **ST-5b.** Its question (V-9) is `e`'s inputs. `refresh x` re-asks it quietly; `affects x` declares that in-flight work will change it (H-9). -- **ST-5c.** It is the only legal target of `guess` (AC-3): a guess - needs a truth that will confirm or correct it. +- **ST-5c.** It and an equation (V-2) are the legal targets of `guess` + (AC-3): a guess needs a truth that will confirm or correct it, and an + equation's truth is its expression. A guess is not a write of the truth, + so an equation still takes no `:=` (W-1). A guessed equation lowers to + Solid's `createOptimistic(fn)` / `createOptimisticStore(fn, seed)`, whose + setter only guesses; a guessed source with a question to a + `createSignal(fn)` truth under a `createOptimistic` layer, because it is + also written plainly. Not a deferred equation (`GUESS_ON_DEFERRED`): its + value lags the one a guess would be confirmed by (V-16). Not `props` or a + parameter (O-4): guess over the child's own equation of a prop + (`shown = props.title`), which shows the guess where the child reads it + (S-guess-equation). ## ST-6 — Streams @@ -220,7 +230,7 @@ selected = draft(pre selected -> {}) { d[id] := true; d[prevId] := false } - **AC-3 (guess).** `guess x := e`, legal only inside an action body, declared or inferred (AC-1b); in an `effect`'s apply block, which is never an action, it is `GUESS_OUTSIDE_HOLD`, and only on a source with a - question (ST-5; `GUESS_NO_QUESTION`): writes a guess that is the + question (ST-5) or on an equation (ST-5c; else `GUESS_NO_QUESTION`): writes a guess that is the graph's and the screen's value for `x` from the instant's settle, display-ahead and verdict-inert, until the hold it was made over commits or `x`'s own answer differs — the full rule is H-11. `x`'s truth is @@ -304,6 +314,7 @@ selected = draft(pre selected -> {}) { d[id] := true; d[prevId] := false } | `STALE_OWN_READ` (new) | S | AC-1d: a read of the change's own write | | `STALE_WRITE_BACK` (new) | S | AC-1e: a pre-`await` read written back after it | | `GUESS_NO_QUESTION` (new) | S | AC-3 / ST-5c | +| `GUESS_ON_DEFERRED` (new) | S | AC-3 / ST-5c: a deferred equation lags its truth | ## Scenarios diff --git a/spec/07-surface.md b/spec/07-surface.md index 28d150b..ded3340 100644 --- a/spec/07-surface.md +++ b/spec/07-surface.md @@ -535,3 +535,10 @@ Expr ::= TSExpr with §3's removals and additions keyword need not. `source` was weighed against `state` and `signal` the same day and kept (decision 2): `signal` reads as atomic beside stores, and an equation is state too. +19. **A guess may sit over an equation** (ruled 2026-11-11): `x = e` then + `guess x := v` in an action, as Solid's `createOptimistic(fn)`, whose + setter only guesses (06 ST-5c). Requiring `source x = e` to guess was + stricter than Solid and guarded nothing: a guess is not a write of the + truth, and a plain `x := v` on an equation stays `WRITE_TO_NON_SOURCE`. + `source x = e` is for state that is also written as truth. A prop is + guessed through the child's own equation of it, never `props.x` (O-4). diff --git a/spec/99-diagnostics.md b/spec/99-diagnostics.md index 54543cf..22c1887 100644 --- a/spec/99-diagnostics.md +++ b/spec/99-diagnostics.md @@ -104,6 +104,7 @@ named. | `STALE_OWN_READ` | S | AC-1d | S-infer-5 | | `STALE_WRITE_BACK` | S | AC-1e | S-infer-6 | | `GUESS_NO_QUESTION` | S | AC-3 / ST-5c | S-check-1, S-solid-32 | +| `GUESS_ON_DEFERRED` | S | AC-3 / ST-5c (a deferred equation lags its truth, V-16) | S-guess-equation | | `INVALID_REFRESH_TARGET`, `INVALID_AFFECTS_TARGET` | S | AC-4, AC-5 | S-check-1 | | `REGION_ESCAPE` | S | O-3, O-3a, O-3b | S-check-1 (seven shapes), S-module-1 | | `UNSTABLE_LIST_IDENTITY` | S | ST-4b (narrow form: `map` into fresh records, unkeyed) | S-store-3 | @@ -171,7 +172,7 @@ section with a fix in `guide/diagnostics.md`, and the compiler's tests check its | bin | codes | | --- | ----- | | U | 21 | -| S | 12 | +| S | 13 | | S/R | 5 | | R | 17 (+ the SSR family) |