Doxa extended#1
Draft
hakimjonas wants to merge 58 commits into
Draft
Conversation
Phase 0 — Tokenizer & Highlighting: - lib/src/tokenize.dart: Doxa LangGrammar for rumil_tokens (doxaGrammar), pre-built doxaTokenizer, tokenizeDoxa() / tokenizeDoxaSpans() convenience functions - lib/src/highlight.dart: cssClassFor() mapping to unified tok-* classes, highlightDoxaBlock()/highlightDoxaInline() HTML generators, tokenizeToSegments() for template engines - lib/doxa.dart: barrel exports tokenize + highlight + syntax - pubspec.yaml: +rumil_tokens: ^0.10.0 Phase 1 — GreenNode Parse Tree: - lib/src/syntax.dart: DoxaToken (19 values) + DoxaSyntax (38 values) alphabets, tokenKind()/tokenToGreen()/ tokenizeAsGreens() canonical mappings, reparsableKinds, isSimpleToken, DoxaGreen/DoxaRed type aliases - lib/src/parse_tree.dart: parseProgramTree()/parseExprTree() produce both SProgram AST and lossless GreenNode tree via tokenizer + AST span alignment - lib/src/cst.dart: parseProgramCst()/parseExprCst() return RedTree, nodeAt()/enclosingDecl()/childrenOf()/toSource() position queries, reparse() via buildDoxaReparser() - test/parse_tree_test.dart: parse tree + position query tests docs/TOOLING_PLAN.md: full 4-phase architecture, dev discipline hard gate (analyze/formatter/tests must be green before done)
Phase 2 - Structured Check Output: - lib/src/output.dart: CheckOutput sealed class, CheckSuccess (declarations, count, semInfo), CheckFailure (kind, line, column, expected, actual, message, span), DeclInfo (name, kind, type, normalForm, span). Serialised to JSON via dart:convert. - lib/src/web_check.dart: checkSourceOutput() → CheckOutput, checkSourceJson() → JSON string, checkSourceString() kept for backward compat. Per-declaration normal forms computed in full accumulated TopEnv. - bin/doxa.dart: --json flag for structured CLI output. - web/doxa_check.dart: switched from checkSourceString to checkSourceJson (still String-to-String, no interop change). Phase 3a - Semantic Metadata (InfoTree): - lib/src/sem_info.dart: SemInfo (span, name, kind, type, defSpan) and SemInfoKind enum (localVar, topBinding, constructor, dataType, implicitParam). - lib/src/meta.dart: List<SemInfo>? semInfos field on MetaContext for opt-in metadata collection. - lib/src/elab.dart: _recordSemInfo called at 6 resolution sites (SIdentKind/SDotKind local var, data type, constructor, top binding). MetaContext created per-decl with semInfos enabled. - SemInfo collected per-declaration, sorted by span.start, exposed in CheckSuccess.semInfo JSON field. docs/TOOLING_PLAN.md: expanded Phase 3 into 3a/3b/3c with full REPL and LSP server specifications. LSP transport to be built from scratch (no third-party package). Principles added: build infrastructure, not demos.
- lib/src/repl.dart: ReplSession (immutable, final fields), ReplStep tuple (ReplResult, ReplSession), processInput returns new session on declaration success. Expression-first parsing: parseExpr then parseDecl fallback. Seeded with prelude (Eq, refl) via bindings/dataDecls constructor params. Error formatting uses actual REPL input text for correct caret display. - lib/src/parse.dart: parseDecl(String) entry point for single- declaration parsing, wiring existing _decl parser. - bin/doxa.dart: doxa repl subcommand. Interactive mode (banner, > prompt, :quit) and piped mode. Tuple destructuring for session state updates. Expression output: : type / = normal form. Declaration output: name : type.
…WASM) Two sibling packages in monorepo, following the Dart SDK pattern (analyzer ↔ analysis_server) and rumil-dart pattern. doxa/ (kernel): - 15 src files (term, value, env, ctx, meta, registry, eval, check, elab, parse, surface, pretty, diff, report, source) + sem_info.dart - 16 kernel unit tests - 342 tests pass, 0 analyze issues - Depends on: rumil doxa_tooling/ (tooling + CLI + WASM): - 10 src files (tokenize, highlight, syntax, parse_tree, cst, output, web_check, repl) + lsp/ (transport, protocol, handler) - bin/doxa.dart (check, check --json, repl, lsp) - web/doxa_check.dart (WASM entry) - 23 tooling tests + test/programs/ fixtures - 424 tests pass (6 skipped), 31 info-only (implementation_imports) - Depends on: doxa (path ../doxa), rumil, rumil_tokens Root pubspec.yaml resolves path deps for tool/ scripts. sem_info.dart kept in kernel (imported by both elab.dart and meta.dart). docs/PACKAGE_SPLIT_PLAN.md: SOTA research + step-by-step migration plan.
…2, deferred decisions Adds three kernel-hardening phases before the language features: - 14.5: Quotient types (~200 lines) - 14.6: Definitional constructor injectivity (~30 lines) - 14.7: Reducibility hints (~10 lines) Adds a benchmarking interlude to measure actual kernel performance before deciding on native numerics and other optimizations. Preserves the original develop-branch phases 15-22 (universe polymorphism through release) in compressed form. Documents four deferred decisions with explicit triggers: well-founded recursion, native numerics/Int, stdlib expansion, coinductive types. Supersedes the develop-branch PLAN.md for future-facing work. TOOLING_PLAN.md (phases 0-3c) is complete and unchanged.
…iants Changes: - Benchmarking now runs BEFORE 14.5 (measures pre-change kernel, results inform implementation). Re-benchmark after 14.7 measures impact. - Dependency graph updated accordingly. - Added timeline estimate table (sessions per phase, ~95-140 total, ~2-3 months full-time, ~8-12 months part-time). - Added cross-cutting invariants (backward compat, test count, performance band, analyze+format) that every phase must preserve. - Added educational content as continuous cross-cutting concern: each phase contributes example .doxa files that accumulate into the Phase 22 tutorial. - Clarified relationship with develop PLAN.md: this is the overview roadmap; develop PLAN.md remains authoritative for implementation detail on Phases 15-22.
The CONSOLIDATED_PLAN.md is the overview roadmap. This file is the per-step detailed plan for Phases 15-22 with prior-work study requirements, risk assessments, and sub-step exit criteria. Referenced by CONSOLIDATED_PLAN.md as the authoritative source for implementation-level detail.
DETAILED_PLAN.md: - Phase 14.5 (quotients): Step -1 (prior work), Steps 0-6 (design, kernel shapes, eval/conv, infer/check, elaboration, tests, exit). Risk assessment (Lean 3 soundness bug, VRec interaction). - Phase 14.6 (constructor injectivity): Steps 0-2 (~30 lines, conv arm in _Conv step, 6 tests). - Phase 14.7 (reducibility hints): Steps 0-3 (~10 lines, opaque flag on TopBindingEntry, surface syntax, tests, plus_zero bug). - Phase 14.8 (re-benchmark): short, references CONSOLIDATED_PLAN. - Updated dependency graph to show 14.5-14.7 in parallel. PHASE_14.5_IMPLEMENTATION_PROMPT.md: - Self-contained implementation guide (~300 lines). - Exact class signatures, defunctionalized driver frame shapes, conversion rules, ι-reduction, infer/check logic. - File modification checklist, design constraints. - 8 required test cases, verification commands. - References to Lean 4 quot.cpp and Lean 3 soundness bug.
Existing kernel code paths are unchanged by the new features. Post-14.5 measurements of non-quotient paths are identical to pre-14.5 measurements. The re-benchmark after 14.7 measures the delta from the three kernel-hardening phases.
Kernel: TQuot/TQuotMk/TQuotLift term/value forms, driver dispatch (eval/conv/quote/infer/check), ι-reduction, identity-only VQuotMk conv. Parser: Quot(A,R), mk a, lift(fn,proof) surface syntax. Elaboration: full walker coverage. Lean 3 bug prevented architecturally (quotients always Type-sorted). 373+424=797 tests, 0 analyze errors.
tool/benchmark.dart:
- Reusable harness measuring parse + elaborate + check timing on
real and synthetic workloads
- --only=<regex> / --repeat=N / --warmup=N / --output=json|table
/ --depth=N,N,N CLI flags
- Default workloads: stdlib files (7), example/proofs.doxa,
Church-encoded depth ladder (100, 500)
- Warmup runs + best-of-N timing for stable warm measurements
- Markdown table output suitable for docs/BENCHMARKS.md
- Graceful handling of stack overflow in elaborator (depth 1000+)
Initial findings (post-Phase 14.5, Dart JIT warm):
stdlib/proofs (11.5 KB, 42 decls): 32ms
example/proofs (4.8 KB): 8ms
Church depth 100: 6ms
Church depth 500: 108ms (elab dominates)
Church depth 1000+: STACK OVERFLOW (elaborator
_inferExpr/_checkExpr mutual recursion was never defunctionalized)
doxa/lib/src/elab.dart (_inferExprInner SAppKind): - Replaced recursive _inferExpr(fn) call with iterative spine collection: walk left for left-deep f(a)(b)(c), right for right-deep f(g(...(x)...)). Process innermost-to-outermost in a single O(1)-stack loop. - Insert implicits per-layer, check args against domains, advance codomains — semantics identical to recursive version. doxa/lib/src/meta.dart (inlineSolvedMetas TApp case): - Flat-right inlining: collect right spine iteratively to avoid overflow on deeply right-nested TApp chains. Verification: - 373+424=797 tests pass (no regressions) - Church depth 5000: 9.2s (was StackOverflowError at ~1000) - Church depth 1000: 384ms (was StackOverflowError) - dart analyze: 0 errors, 0 warnings docs/ELAB_STACK_FIX_PLAN.md: root cause, fix approach, implementation steps, design constraints.
tool/alloc_profile.dart: parse vs elab vs check breakdown, eval/conv stress micro-benchmarks tool/parse_ast_profile.dart: per-declaration parse cost by kind, parser throughput tool/parse_deep_profile.dart: lexer overhead, scaling analysis tool/parse_profile.dart: parser-only benchmarking .gitignore: exclude compiled AOT binaries
Covers: completed tooling (Phases 0-3c), kernel hardening (Phase 14.5), elaborator stack fix, benchmarking suite, AOT performance numbers, next steps, project memory, and repository layout.
…olymorphism Phase 14.6 — Constructor Injectivity Tests - 5 new injectivity tests in conv_test.dart (ConvOk for same ctor, ConvMismatch for different ctors/different args, Type-sorted guard, succ_injective propositional proof) - No kernel code needed — VConstr pointwise comparison already existed Phase 14.7 — Reducibility Hints (opaque/transparent) - isOpaque field on TopBindingEntry, TopBinding, SValKind, SFunKind - _opaqueMod parser (optional 'opaque' keyword before val/fun) - _Eval(TTop): opaque bindings yield VNeutral(NTop(name)) instead of body - 5 opacity tests in opaque_test.dart Phase 14.8 — Benchmarking Interlude - docs/BENCHMARKS.md with AOT numbers and phase history table Phase 15 — Universe Polymorphism - Level sealed class: LLevel, LVar, LSucc, LMax, LImax - VType.level/TType.level: int → Level (30+ site updates) - _normalizeLevel, _normalizeMax, _levelGte, _levelEq in eval.dart - _Conv VType uses _levelEq, _Subtype VType uses _levelGte - _piSort/_computePiSort use LMax - _inferValueType uses LSucc(level) - Non-cumulative levels preserved (strict == in conv, <= in subtype) - Recursor bridge (.ind/.rect) kept for backward compat - All 807 tests pass (383 doxa + 424 doxa_tooling) - dart analyze: info-only, no errors
- TSProp/VSProp kernel term/value forms alongside TProp/VProp - _Conv early short-circuit: VSProp × VSProp → ConvOk (strict irrelevance) - _Subtype: SProp ≤ SProp, SProp ≤ Prop - _Sort._SProp, _asSort/_sortToValue SProp support - _piSort: SProp codomain → Pi:SProp (impredicative) - _isSPropSorted / _isSPropSortedTerm for mismatch-site admission - _mismatchOrIrrelevance gains SProp check (after Prop) - _Infer/_Quote/_Eval/_Apply/_inferValueType TSProp/VSProp cases - SSPropKind surface node, 'SProp' keyword parser - SProp data validation: fields must be SProp-sorted - SProp rec restriction: only .rec emitted (no .ind/.rect) - meta.dart: TSProp added to inlineSolvedMeta patterns - web_check.dart: SPropFieldNotProofIrrelevant error kind - 23 new tests in sprop_test.dart (parsing, conv, Pi rules, data, fields) - All 830 tests pass (406 doxa + 424 doxa_tooling) - dart analyze: info-only, no errors
- TProj term form and NProj neutral form for record field projection - _EvalProj frame: extracts field from VConstr or wraps as stuck NProj - _projectField helper: looks up field index in constructor args - Record η rule in _Conv: VConstr × non-VConstr where type is record → projects all fields and compares pointwise - _InferProjFieldType: infers projection type from record telescope - NProj × NProj conv: same field name + convertible inner exprs - NProj quote: quotes to TProj(quote(expr), fieldName) - _isRecordData predicate: single-ctor, non-recursive, no indices - SDotKind disambiguation: elaborates qualifier first; if type is record → field projection, otherwise → name qualification - TProj in meta-inlining, pretty-printing, sem_info - Fix: _InferProjFieldType env construction narrowed to params + preceding fields only (was pushing all args including later fields) - 7 kernel-level tests in record_test.dart - Re-benchmark: stdlib/proofs 9.678ms (flat vs Phase 16 baseline) - All 837 tests pass (413 doxa + 424 doxa_tooling) - dart analyze: info-only, no errors - No tooling updates needed (TProj/NProj are kernel-only)
- SImportKind surface node with path field - _importDecl parser: import "path/to/file.doxa" - _strLit parser for quoted string literals - _processImport in elab.dart: load file, parse, elaborate, check, merge TopEnv, detect duplicates, detect cycles - CyclicImport / ImportFileNotFound error types - Idempotent import: already-imported files silently skipped - currentImportPath / importedPaths / _importStack state tracking - Tooling: kwImport token, importDecl syntax kind, web_check SImportKind case, parse_tree CST mapping, reparsableKinds - Stdlib reorganised: bool.doxa standalone, nat/list/vec import dependencies, proofs.doxa imports 5 modules with 0 duplicates - example/proofs.doxa imports from ../lib/stdlib/ - 11 new import tests (resolution, idempotent, cycles, transitive) - All 848 tests pass (413 doxa + 435 doxa_tooling) - dart analyze: 0 errors across both packages
Item 1 — Local let rec:
- isRec bool on SLetKind, TLet (surface + kernel)
- rec keyword parsing in _valBinding block-expr bindings
- _EvalLetBody: wraps bound value in VFun when isRec is true
- Elaborator builds TLet with recDecreasingArg/recArity for VFun guard
- Usage: { val rec f(x: Nat): Nat = body; f(zero) }
Item 2 — Per-member {struct <name>} annotation:
- structAnn field on SFunKind
- _structAnn parser: {struct ident} after fun params
- _findParamIndex / _designatedArgIndex in elab.dart
- _elabFunBlock uses structAnn for recDecreasingArg stamping
- Structural recursion walker updated with designatedIdx parameter
- StructAnnotationNotFound error type + web_check + report
Item 3 — plus_zero bug investigation:
- Confirmed VFun guard (Phase 14.7) prevents infinite normalization
- Match-based dependent return type fails with type mismatch
(index refinement limitation), not infinite looping
- Existing Nat.ind/recursor approach is correct — no fix needed
All 856 tests pass (418 doxa + 438 doxa_tooling)
dart analyze: 0 errors, 4 pre-existing warnings
Item 1 — VMatch Quote Scope-Faithfulness:
- Fixed resolveViaEnv in _substArmBody to use envIdxAdj instead
of depth for TBound index computation
- Main-walk and meta-spine index regimes now shift independently
when level > env.depth
- Un-skipped all 5 previously-skipped tests in
vmatch_roundtrip_test.dart
- Fixes map_compose-style VMatch quoting through cong/trans
Item 2 — Zero-Parameter fun Parser Fix:
- Made _valueParams content optional (.optional.map()) so ()
parses as empty parameter list
- Un-skipped zero-param fun test in
structural_recursion_walker_test.dart
All 862 tests pass (418 doxa + 444 doxa_tooling)
0 skipped tests remaining
Item 1 — fun body braces:
- _mkFunBody accepts = expr | { expr } via _blockExpr
Item 2 — data product form:
- _isProductForm detects when no ctor references the data name
- _desugarProduct builds mk ctor with Pi chain from fields
- Applied in _dataBody: product form desugars to single-ctor sum
Item 3 — | variant separator:
- _ctorSep = _sym('|') | _sym(';')
Item 4 — selective import:
- importedNames field on SImportKind (default [])
- _processImport filters by importedNames when non-empty
Item 5 — optional type param kind:
- Already supported via .optional in _typeParams
All 863 tests pass (418 doxa + 445 doxa_tooling)
dart analyze: 0 errors across both packages
- Tactic engine: tactic.dart (~340 lines) — TacticState, TacticResult
(TacticOk/TacticFail), TacticFn typedef, seq/alt combinators
- 7 primitives: intro, exact, apply, refl, rewrite, induction, trivial
- Surface: 7 sealed STacticStep types + SByKind for by { ... } blocks
- Parser: theorem/by keywords, 7 tactic step parsers, | as alternative
- Elaborator: _elabTacticBlock creates goal meta, runs tactic steps,
returns solved term; TacticFailed/TacticIncomplete errors
- theorem desugars to SValKind, by works in both val and theorem
- Fungal-compatible: | for alternative (not <|>), by { ... } block
- 9 tactic tests: parsing, alternatives, intro+exact elaboration
- All 872 tests pass (427 doxa + 445 doxa_tooling)
- dart analyze: 0 errors across both packages
- STypeclassKind, SImplKind, SClassMethod, SIntersectionKind
surface nodes
- typeclass/impl keywords, constraint syntax in _funTypeParamGroup
with & for multi-constraint intersection
- _elabTypeclass: desugars to single-ctor data + classRegistry
- _elabImpl: desugars to val binding + instance registration
- Constraint binder insertion in _elabFun/_elabFunBlock
- Instance resolution in _insertImplicits via pattern unification
- NoInstanceFound / OverlappingInstances error types
- classRegistry on TopEnv + DeclResult for per-class instance table
- Fungal-compatible: typeclass Eq[A], impl Eq[Int],
[A: Eq & Ord] constraints
- Fix: constraint parser only activates on explicit [...] groups,
not implicit {...} — prevents false constraints on type vars
- 13 typeclass tests: parsing, structural checks, elaboration
- All 885 tests pass (440 doxa + 445 doxa_tooling)
- dart analyze: 0 errors across both packages
- SPEC_COVERAGE.md: 85-entry audit mapping every SPEC clause to tests - tutorial.md: 16 sections, 14/14 code blocks verified - RELEASE_NOTES.md: full feature list, limitations, install guide - WASM browser demo (index.html, 329KB .wasm artifact) - SPEC.md §1.1a/§1.1b: split built extensions from future directions - README.md, SYNTAX.md, CHANGELOG.md: stale claims fixed - Code comments (7 src files): 20 AI-language violations fixed per domain-writing skill - Plan docs (3 files): 10 AI-language violations fixed
The previous edit claimed bare Type resolves to a fresh level variable and Eq is universe-polymorphic. In the current implementation, bare Type always resolves to LLevel(0). Eq requires Type-sorted arguments; UIP is not statable, matching the concrete sort-signature discipline.
…aceBindings, currentImportPath)
…tic tokens/references/rename, IDE plugins, CI, fuzz
…ton, case study foundations) + kernel fixes + formatter impl bug fix
- MetaContext snapshot/restore API (MetaSnapshot class) - Optional name parameter on intro tactic - Public elabExprInScope for expression elaboration with local binders - _ProofSession + proof-mode meta-commands in REPL (:goal, :step, :undo, :print, :qed, :abort) - Context display in :step output, :goal without args shows current state - MetaSnapshot round-trip tests (7) and REPL proof-mode tests (14)
Stdlib: - Add mult_succ_right, mult_comm, mult_2 to proofs.doxa (3 new lemmas, 59 declarations total) Tutorial: - Add REPL invocation to section 1 - Add section 9b (Interactive proof mode) with full command reference - Add proof guide and interactive mode links to Next steps Docs: - Write docs/proof-guide.md covering the sqrt2 proof strategy and the arithmetic and parity lemmas needed
… nat_wf/sqrt2 support elab.dart — enriched teleEnv (27e): - Parallel enrichedTeleEnv in _elabMatch provides actual scrutinee index values for wildcard ctor-arg binders (_ in acc_intro _ _ f), enabling closure β-reduction: R a m → Lt a m in f a p1 calls. - Named binders keep their neutral NVar to preserve de-Bruijn identity. - Refined expected type for non-indexed match arms: _substNVar substitutes the scrutinee NVar with the ctor result value (e.g. Acc[Nat] ... n → Acc[Nat] ... zero in nat_wf case zero arm). - memberDeclIdxs fallback in structural recursion walker: try callee designated arg index first; fall back to caller. Lets both directions of a mutual block pass termination (nat_wf ↔ nat_wf_help). eval.dart — reversed-spine _tryUnify (27f): - Extended canonical spine check to accept both [0,1,...,n-1] and [n-1,...,1,0] orders from _insertImplicits. - Added NMeta forcing in spine entries before pattern restriction check, solving acc_intro implicit A unification when Lt.rec appears in the third argument. test: structural_recursion_walker_test updated for memberDeclIdxs API. All 972 tests pass (452 doxa + 520 doxa_tooling).
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.
No description provided.