Rewrite of Python FE to separate out Python-specific resolution, threading of effects, and coercion insertion with Laurel resolver#1415
Draft
ssomayyajula wants to merge 10 commits into
Conversation
…lusive / 14 internal Verified-green snapshot BEFORE the proof-relevant-coercion change. - Build: lake build pyAnalyzeV2 strata = 515 jobs, exit 0 - Unit suite (--solver z3): 159 success / 4 fail / 43 inconclusive / 14 internal / 0 crash - src/Strata (v2 spec) untouched Recovery point in case the resolver/elaborator coercion refactor regresses.
…t Coercion verdict LaurelAST.lean: add Coercion (refl|inject|project|upcast) + coerce judgment that returns the abstract verdict, reusing the existing unfold/gradualTypes/ancestors. isConsistentSubtype := (coerce …).isSome — ONE judgment, boolean derived from it, so the yes/no answer and any inserted coercion can never disagree. TypeLattice gains realizeCoercion + toBool caller hooks (default none = identity, native Laurel). GENERIC: the verdict names the KIND of coercion, never a runtime function; the caller (Python frontend) realizes it. No realizer wired yet -> behaviorally neutral. Build green. Unit suite (--solver z3): 159/4/43/14 = EXACTLY the baseline (no change), confirming the boolean is provably identical to the old isConsistent ∨ isSubtype.
…r effects-only Wire the Python realizer (pythonRealizeCoercion/pythonToBool) onto TypeLattice via LaurelTranslateOptions; flip elaborator applySubtype to identity (the two coercers are mutually exclusive). coerceTo realizes the coerce verdict at the subsumption chokepoint, assignment RHS (both gaps), datatype-ctor args (getCallInfo), and preconditions (vs TBool). KEY FIX: isDynamicBoxable must recognize Any as BOTH .TCore "Any" (the erased/runtime form, the common case) AND gradual .UserDefined "Any". Unknown/other-TCore stay gradual wildcards (refl, no coercion) so prelude/heap-plumbing code isn't spuriously wrapped. Composite↔Any typed via re_Match (flattens to Composite); from_Composite is bare. Unit suite (--solver z3): 151 success / 4 fail / 41 inconclusive / 24 internal / 0 crash. Up from the 212-internal mid-refactor low; 24 remaining are coverage gaps still being triaged (some pre-existing). One judgment: isConsistentSubtype := (coerce …).isSome.
…al; remove toBool hack coerce: distinguish the boxable dynamic type (Any, as BOTH .TCore "Any" and gradual .UserDefined) from pure wildcards (Unknown). Concrete .TCore containers (ListAny/ DictStrAny) box/unbox against Any via the realizer (from_ListAny/Any..as_ListAny!/...) instead of being mis-classified as no-op gradual. Translation: Python float -> TReal (one domain with the LiteralDecimal literal + from_float:real). Removed the applyToBool/toBool side-mechanism (a second coercer beside coerce — the banned two-judgments pattern). Bool-context sites (if/while/assert/assume) route the condition through the single coerce path (Check.resolveStmtExpr cond TBool) as before. Unit suite (--solver z3): 160 success / 4 fail / 47 inconclusive / 9 internal / 0 crash. Above the 159 baseline, with the clean generic-resolver-coerces / caller-realizes design.
…e toBool side-hook T -> bool truthiness is a real coercion in a gradual language, so it is now a verdict of the ONE coerce judgment (.truthify source), realized by the ONE realizer (int_to_bool/str_to_bool/Any_to_bool/...). Removed the applyToBool/toBool side-mechanism; bool-context sites route through the single coerce path. coerce: when sup=TBool and sub is concrete, return .truthify sub (this extends the decision: concrete T is now consistent-subtype of bool, correct for Python boolean context). Unit suite (--solver z3): 164 success / 4 fail / 47 inconclusive / 5 internal / 0 crash. Architecture clean: one judgment (isConsistentSubtype := (coerce).isSome), generic resolver decides, Python realizer maps verdict->runtime call. The 5 internal are all pre-existing baseline items (field_write, 2 __main__, reassign(ill-typed), type_alias).
Drop the now-unused toBool field/param from TypeLattice, LaurelTranslateOptions, resolve, and the pipeline call sites — truthiness is a coerce verdict (.truthify) realized by the one realizer, so the side-channel is gone. No behavior change: 164/4/47/5 unchanged.
Collect module-level 'Name = <type-name>' aliases in translateModule, thread via TransState.typeAliases into pythonTypeToHighType (now takes an alias map) at every type-resolution site (proc inputs/outputs/locals/param-copies, module locals). An annotation referring to an alias resolves to the aliased type instead of a phantom UserDefined composite. test_type_alias: Internal error -> Analysis success. Unit suite: 165 success / 4 fail / 47 inconclusive / 4 internal / 0 crash. No regression.
…s prelude stubs The resolver remaps these builtins to Any_*_to_* names (Resolution.lean builtinContext) but the prelude never declared 6 of them, so a call like type(e) failed elaboration (lookupFuncSig miss) instead of producing a sound opaque Any. Declared the 6 missing stubs in PythonRuntimeLaurelPart (arities per mkBuiltinSig, Any params per convention). test_invalid_client_type + test_missing_required_param (both use type(e) in an f-string): Internal error -> Analysis success. Unit suite: 167 success / 4 fail / 47 inconclusive / 2 internal / 0 crash. The 2 remaining internal errors are NOT-OUR-BUG ill-formed input: test_field_write (unannotated c = Cell(1)) and test_reassign_different_type (x:int=42; x="hello", mypy-rejected).
Full pipeline writeup (Read -> Resolution -> Translation -> Elaboration -> Laurel resolve+coerce -> Core), the one-judgment coerce mechanism + caller realizer, files touched, and honest verification numbers (unit 167/47/4/2; 192/220 match v1 with the 28 differences itemized incl. the 14 precision regressions; benchmark standalone).
github-actions
Bot
added
Laurel
dependencies
… Python-only The proof-relevant coercion change must not alter the generic Laurel resolver's behavior for non-Python callers. Three deviations had leaked into the generic path and broke native diagnostic tests (T22_ArityMismatch, T23_ArithTyping, T9_IfBranchJoin, ResolutionTypeCheckTests): 1. truthify: `coerce` had a `sup = TBool => some (.truthify sub)` arm that made `isConsistentSubtype int bool = true`, breaking native type-checking. Removed the `truthify` constructor entirely. Python truthiness needs no special verdict: a Python condition is `Any`-typed, so `coerce Any bool = project bool`, which the realizer turns into `Any_to_bool`. 2. resolveHighType: the `(expected := …)` kind constraint on `resolveRef` had been dropped, suppressing the "resolves to X but expected composite" diagnostic. Restored to baseline verbatim. 3. Synth.assign / Check.assign: had been rewritten from baseline CHECK mode (`Check.resolveStmtExpr value expectedTy`) to SYNTH mode + a resolver-side (T, Error) error-sink expansion. That switched the assignment RHS off the check path, changing native diagnostics (whole-expr "cannot apply" instead of per-operand "expected/got", wrong spans, swallowed arity errors). The expansion was redundant: the elaborator's projProcedureCall already lowers an exception-throwing call into a multi-target `(result, maybe_except) := f(args)` BEFORE resolution. Reverted both arms to baseline; Python RHS coercion still flows through the one `coerceTo` chokepoint in the subsumption fallback of Check.resolveStmtExpr. Also: import the two new FineGrainLaurel modules from Strata.lean (the FE package lives outside Strata, so nothing else makes them transitively imported), and drop an unused `iden` binding. Verified: brazil-build Strata green end-to-end (all 256 modules imported, all diagnostic + SMT tests pass). Synth.assign/Check.assign/resolveHighType are byte-identical to baseline HEAD.
ssomayyajula
force-pushed
the
ssomayyajula/incremental-hybrid-experiment-v4
branch
from
June 29, 2026 01:40
7a4d54f to
cfb36b6
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
TODO