Sync to PurePy 0.9#1538
Conversation
Mirrors the existing FV/BV machinery on core Expr/Stmt/Elim. Surface side now exports: - BV Pattern and BV ListRestPattern (variables bound by destructuring). - FV (Expr a), FV (Stmt a), FV (VarDef a), FV (LambdaClause a), FV (Clause a), FV (DictEntry a), FV (ListRest a), FV (ParagraphElem a). - Helpers fvRecDefs (mutual recursion: bodies' frees minus all branch names) and qualsFv (list-comp qualifiers bind for subsequent ones). Reuses the FV / BV classes from Expr, so client code can call fv/bv uniformly on surface or core values. Foundation for static-analysis checks that need free-variable information (mutual-region forward references, captured-variable shadowing, etc.).
WellFormed gains checkScope -- the general 'var' rule from the PurePy spec. Walks the AST threading a scope set; each expression must have fv ⊆ scope. Initial scope comes from primitives + imported modules' top-level definitions (computed by envNames + moduleExports). scope is extended as we walk: - Seq s1 s2: s2 sees scope ∪ bvBlock(s1). - DefRec rs: bodies see scope ∪ region names (mutual rec) ∪ parameters. - Match branches: body sees scope ∪ bv(pattern). - If/else: branches see outer scope; bindings don't propagate (no definite assignment yet). Catches the spec's mutual_split case (odd unbound when even's body is checked, because the intervening x = even(0) splits the regions). The earlier targeted forward-reference check is subsumed. Also fixes a Matrix FV typo (was subtracting bound (x, y) from the source instead of the body).
Adds the type-level infrastructure for definite-assignment analysis, per PurePy spec §2.1: - Ctx = Map Var Boolean (tt=True, ff=False, ⊥=absent). - Result = Returns | Assigns Ctx. - overrideCtx (Γ · Δ): right-biased sequential composition. - mergeCtx (Γ ⊕ Δ): parallel composition; vars defined in only one operand become ff (lost in merge). - overrideRes / mergeRes: lifted to Result. Returns is zero for · and unit for ⊕. Not yet consumed -- existing unreachable check now uses a simpler isReturns Boolean predicate (was: TyReturns vs TyAssigns) until the checkDA refactor that will replace check + checkScope with a single spec-faithful well-formedness judgement.
Per PurePy spec §2.2:
- assigns(s): syntactic over-approximation of vars assigned in s,
not descending into nested function definitions. Each def's name is
included; its body's assigns are not.
- captures(s): vars from enclosing scope referenced by closures
(lambdas or nested function definitions) within s. Other forms
recurse to find closures.
Both unused so far -- the consumer is the upcoming checkDA refactor.
The DefRec case of captures faithfully implements the spec's formula:
⋃ᵢ (fv(bᵢ) \ ({x⃗ᵢ} ∪ assigns(bᵢ))) \ {f₁..fₙ₊₁}
ListComp captures uses a simplified body-only fv -- full qualifier
binding handling is a small follow-up.
The single well-formedness judgement per PurePy spec §2.3: checkDA :: Ctx -> Stmt -> m Result Each stmt is checked under a context Γ and yields a Result (Returns | Assigns Δ). Variable references are validated against Γ: unbound names error; ff-bound names also error (definite-assignment violation, once any rule produces ff -- currently nothing does, but future rules will). Subsumes the previous two passes: - unreachable: caught in the Seq case (s1 Returns ⇒ throw). - var rule: every variable reference must be tt in Γ. Pattern-bound vars in match branches are stripped from each branch's result before merging (branch-local, don't propagate). Function bodies (in DefRec) are checked under Γ + region names + parameters, all tt. 124 tests + 3 website suites green. Next iterations will populate the Δ side of the checks meaningfully (e.g. partial-def detection via merge producing ff), which catches cond_partial_def, no_else, etc.
Both are caught for free by the new checkDA: branch merge produces ff for variables defined in only some branches; reading a ff-bound var triggers "Not definitely assigned: x". - cond_partial_def: x = 6 then if-branch reassigns x = 3, else doesn't, so the merged context has x:ff overriding the earlier x:tt. - no_else: x = 0 then if-branch sets x = 1, else is pass (no assign), so merged x is ff post-if. shadow_captured needs a separate "no reassign of captured var" rule (captures-based); deferred.
Adds the spec's captures-based well-formedness checks: assign rule (x ∉ captures(e) for x = e), seq side-condition (captures(s) disjoint from assigns of later stmts), and mutual rule's ff-locals (body locals shadow outer-scope bindings as not-definitely-assigned). Ports six ill-formed tests from the spec corpus. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Mirrors zero-arg def: empty parameter list desugars to a single __NoArgs param. Removes the dummy-param workaround from two ill-formed tests now that the spec syntax parses directly. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds duplicate_def_in_region from the spec corpus, registered with the existing 'Shape mismatch' error produced by elim construction. Note: this verifies overlap detection, not the spec's full distinct- names rule (which forbids same-name defs in a region even when patterns are disjoint). Also adds a FluidImplementor skill with conventions for running a focused subset of tests via the scratchpad, plus a note on when to run the website Puppeteer tests. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Restores a check that was lost: clauses for a given name within a mutual region must be contiguous. Previously non-contiguous same-name clauses silently merged via Map.fromFoldable, dropping the earlier definition. With this in place, Fluid's overlap-rejection plus contiguity check is a strict generalisation of PurePy's distinct-names rule: piecewise definitions are accepted when contiguous and pattern- disjoint, rejected otherwise. Adds positive (piecewise_def.fld) and negative (non_contiguous_def.fld) tests; notes the generalisation in the ill-formed test comments. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Parser: 'else' is now optional on 'if'; defaults to Pass. Eval: a match statement whose scrutinee's top-level constructor isn't covered by any case falls through (Pass semantics) instead of throwing 'Incomplete patterns'. Pattern-matching in lambda application and var definitions remains strict. Adds two positive tests covering both relaxations. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Splits Specs/IllFormed.purs into purepy_cases (corresponds to entries
in pure-py-spec/test/ill-formed/semantic) and illFormed_cases
(Fluid-specific). Adds two new spec-derived tests:
- mutual_split_by_assign: same failure mode as mutual_split but
region split by assignment rather than call.
- mutual_def_block_local: defs only in if-branch render g not
definitely assigned after the merge.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
A match's branches are merged with Assigns ∅ to represent the implicit no-matching-case fall-through, mirroring how if-no-else merges with an implicit Pass else. DA does not reason about pattern exhaustiveness — by the same principle that 'if true:' doesn't definitely assign anything. Moves match_partial.fld to ill_formed/ (Fluid-specific; no PurePy correspondent). Simplifies purepy/no_else.fld to use the bare-if form now that the parser supports it. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Keeps the conservative DA treatment of match (always merge with Assigns ∅), without an exhaustiveness check. A totality analysis belongs in PurePy once match is in scope of the spec; until then match-as-assignment is necessarily restricted to the variable- already-assigned-before-match pattern. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Reshapes match_partial_def to the function-wrapping form (return inside a function, idiomatic). Adds match_exhaustive_assign — same shape but with both List constructors covered — to document that even an apparently-exhaustive match doesn't save the assigned variable, because DA does not reason about exhaustiveness. Becomes a positive test once we land a static exhaustiveness check (#1537 pending; track separately). Also extends FluidImplementor skill with a Style note (minimal), the See also issue convention, and GH project field population. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Refactoring-only. Two structural changes that prepare the ground
for attribute-grammar-style well-formedness analysis (carrying
TyResult per function body through the AST):
- TyResult, Ctx, and the lattice ops (override/merge) move from
WellFormed.purs to a new DefiniteAssignment.purs. SExpr.purs
can now import them without creating a cycle.
- Clause gains an a annotation slot:
data Clause a = Clause a (NonEmptyList Pattern × Stmt a)
Parser fills unit; downstream code can populate with TyResult.
No behaviour change. 151 tests pass.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
checkDA now validates AND reconstructs the surface AST with TyResult attached at every node. The annotation is meaningful at Clause sites (carries the body's TyResult); elsewhere it's the multiplicative identity assignsEmpty (Assigns Map.empty — the unit of overrideRes, viewing TyResult as a near-semiring with Returns as additive unit). Module.prepConfig captures the annotated AST but doesn't consume it yet; desug still works on the raw input. Next step: feed the annotated AST to desug for implicit-None injection. 151 tests pass; no behaviour change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Function bodies whose checkDA TyResult is Assigns get an implicit `return None` appended during post-validation normalisation in WellFormed. Trivial Lattice instances for TyResult so it can sit in the AST annotation slot through desug. Test infrastructure uses prepConfig's desugared output directly instead of re-desugaring the raw input, so the augmented body reaches eval. Adds implicit_return.fld covering def with no return. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Skill-unique content (scratchpad protocol, no-ad-hoc-CLI rule, website test timing, See also footer, Status/Aspect field guidance, "Fluid" redundancy, issue-body formatting) moves into docs/workflow/process.md. CLAUDE.md opens with an explicit directive to read process.md and issue-lifecycle.md before starting work, so the conventions are reliably loaded. Also corrects project board URL from explorable-viz to fluid-org. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
| overrideCtx :: Ctx -> Ctx -> Ctx | ||
| overrideCtx = flip Map.union | ||
|
|
||
| -- Parallel composition Γ ⊕ Δ on contexts. |
There was a problem hiding this comment.
Wrap comment at ~110, not these mini-paragraphs. Add that to the workflow docs.
| assignsEmpty :: TyResult | ||
| assignsEmpty = Assigns Map.empty | ||
|
|
||
| -- Trivial Lattice instances so TyResult can sit in the AST's annotation slot |
There was a problem hiding this comment.
Does "trivial" here mean "broken", or what?
| case κ of | ||
| ContStmt s' -> evalStmt doc_opt (γ <+> γ') s' (αs ∪ αs') | ||
| _ -> error "Stmt continuation expected as match branch" | ||
| -- At statement level, a value whose top-level constructor isn't covered |
There was a problem hiding this comment.
Comment looks obsolete (which is why we shouldn't insert comments).
|
|
||
| stripVars :: Set Var -> TyResult -> TyResult | ||
| stripVars _ Returns = Returns | ||
| stripVars vars (Assigns δ) = Assigns (foldl (flip Map.delete) δ vars) |
| @@ -0,0 +1,17 @@ | |||
| # Mutual region of {f, g} is split by an intervening assignment. | |||
There was a problem hiding this comment.
Remove comments from test cases unless there to document something very specific
| @@ -0,0 +1,12 @@ | |||
| # Even an apparently-exhaustive match doesn't save the assigned variable, | |||
| # because DA does not reason about exhaustiveness. Becomes well-formed once | |||
| # we land a static exhaustiveness check. | |||
There was a problem hiding this comment.
Avoid the jargon land. Add this to the workflow notes too, along with other terms to reject ("honestly", "honest").
| @@ -0,0 +1,11 @@ | |||
| # Fluid generalises PurePy's distinct-names rule by permitting piecewise | |||
| # definitions, but clauses for a given name must be contiguous within their | |||
There was a problem hiding this comment.
Rational here isn't quite right; a good reason not to embed commentary (it quickly goes stale).
…se tests - WellFormed: strip section/explanatory comments; rename ad-hoc names (body, cond, bad, pBindings, elseR, regionNames, locals_ff) to conventional metavars (s, e, x, xs, ys, fs); use foldl1 for the NonEmpty merges; for_ over Maybe for the captures clash report. - DefiniteAssignment: strip explanatory commentary; absorb the set-to-Map helper as fromSet (replaces mapFromSet). - SExpr: drop historical comment on recDefsFwd; replace Maybe-case-throw with for_ idiom (renamed findDuplicate to firstDuplicate for accuracy); drop fvRecDefs comment. - Eval: drop obsolete comment on the Match fall-through case. - Test fixtures: drop commentary from .fld files. - Test layout: move 15 spec-derived positive tests into test/fluid/purepy/ to mirror test/fluid/ill_formed/purepy/. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
If now carries Maybe (Stmt a) for the else branch. Parser produces Nothing when else is absent; ifElseFwd substitutes Pass during desugaring. assigns, captures, implicitNone, checkDA, and Pretty updated to handle the Maybe. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Desugarable specialises to TyResult — desug operates on the post- WellFormed annotated AST. The implicit-None injection moves from a separate walker (implicitNone) into recDefFwd, the one site that needs the annotation in hand: a Clause whose TyResult is Assigns gets `return None` appended to its body before desugaring. Prelude bypasses checkProgram, so its Clause annotations are lifted to Returns (always-returns) rather than the sentinel assignsEmpty, which would have caused spurious Return None to be appended and broken doc propagation through Seq. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
prepConfig now builds the top-level env via buildTopLevelEnv (the extracted prefix of the old initialConfig) and derives the static scope for checkProgram from envNames of that env. Single source of truth for what's in scope at top level; gconfig.γ is the same env restricted to fv e. Also tighten the weasel-words list in process.md. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
| _, _ -> do | ||
| γ' × κ × αs' <- match v σ | ||
| case κ of | ||
| ContStmt s' -> evalStmt doc_opt (γ <+> γ') s' (αs ∪ αs') |
There was a problem hiding this comment.
I thought we were using asStmt?
| , γ :: Env Vertex | ||
| } | ||
|
|
||
| buildTopLevelEnv |
There was a problem hiding this comment.
I thought we said we'd call it topLevelEnv?
| defNames (Left d) = bv d | ||
| defNames (Right (E.RecDefs _ ρ)) = keys ρ | ||
|
|
||
| envNames :: forall a. Env a -> Set Var |
| capturesE (S.ListComp _ e _) = capturesE e | ||
| capturesE (S.DocExpr e e') = capturesE e ∪ capturesE e' | ||
|
|
||
| checkDA :: forall m a. MonadError Error m => Ctx -> S.Stmt a -> m (TyResult × S.Stmt TyResult) |
There was a problem hiding this comment.
Is this the right name? Looks like it's implementing the well-formedness rules.
| Just false -> throw $ "Not definitely assigned: " <> x | ||
| Nothing -> throw $ "Unbound name: " <> x | ||
|
|
||
| stripVars :: Set Var -> TyResult -> TyResult |
There was a problem hiding this comment.
Perhaps TyResult should implement Functor?
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Drops the TopLevelEnv type and the buildTopLevelEnv helper; the runAllocT body sits directly in prepConfig with the env named topLevelEnv at the binding site. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Use keys directly in Module; the rename helpers added nothing. moduleExports is unused since scope is now derived from the top-level env. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Parameterise TyResult as Returns | Assigns a; derive Functor. Concrete TyResult Ctx replaces TyResult throughout. stripVars becomes a one-liner via map. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The function implements the well-formedness rules; the module name is WellFormed. The DA prefix understated what it does. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Desug operates on the concrete TyResult Ctx, so bot/top calls filling synthetic annotation slots in SExpr are replaced with the concrete assignsEmpty/Returns values. The trivial JoinSemilattice, MeetSemilattice, BoundedJoinSemilattice, BoundedMeetSemilattice instances on TyResult Ctx are no longer needed. Also drops the unused imports flagged by strict CI. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Use Assigns Map.empty directly at the call sites; drop the named binding from DefiniteAssignment. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Closes #1530.
Brings Fluid in line with PurePy 0.9 across syntax, statement structure, and definite-assignment semantics.
Summary
deffor both var and rec definitions,return,pass,assert, expression statements,print.def(piecewise pattern-matching) preserved as a strict generalisation of PurePy's distinct-names rule.ifwithoutelseparses (defaults toPass); match without all-cases falls through toPassat runtime.Returns | Assigns Δ, parallel and sequential composition. Captured-variable reassignment, self-capture, unbound-local, unreachable-code rejection. Spec ill-formed corpus ported undertest/fluid/ill_formed/purepy/; Fluid-specific cases sit at top ofill_formed/.return Nonefor function bodies whose body doesn't always Return — implemented attribute-grammar-style:Clausecarries aTyResultannotation,checkProgramreturns an annotated AST, post-validationimplicitNoneinjects the return where needed.DefiniteAssignmentmodule hosts the lattice data (Ctx, TyResult, override/merge,assignsEmpty).Test plan
yarn test— 152 unit tests pass../script/test-website-all.sh— all three websites (article, fluid-org, literate-execution) pass.See also