lojban-rs implementation plan

The plan is split into focused documents under plan/. Code is the source of truth for implemented features; the plan tracks gaps and documents architecture.

The document references @cll-md/ reference grammar book.

Quick start for agents

1. Read plan/RULES.md before implementing any feature.
2. Consult the CLL section(s) cited in the open ticket row.
3. Add or update #[jbo_ref(...)] in code; keep plan/OPEN.md rows for non-ready work.
4. Run bash scripts/regenerate_plan.sh (or at minimum sync_plan_ready.py + ref_audit.py --strict).

Regenerate

bash scripts/regenerate_plan.sh

Plan rules & agent workflow

This document must be kept up to date. Update the plan after implementing or fixing any features/tasks from it.

The plan is split under plan/ — see PLAN.md for the index. The document references @cll-md/ reference grammar book.

Rule: Read Before Implement

Before implementing any feature, you MUST read the corresponding CLL section(s) listed in the reference column. CLL sections contain the authoritative grammar definitions, examples, and edge cases needed for correct implementation. Do not implement from the feature description alone — always consult the source material first.

When implementing or fixing a feature: (1) add or update #[jbo_ref(...)] (Rust) or an @ref: comment block (.egg, Cargo.toml) with full metadata in code, (2) if still AD HOC / PARTIAL / MISSING, keep or update the row in OPEN.md, (3) run python3 scripts/sync_plan_ready.py and python3 scripts/ref_audit.py.

Reference Conventions

Code is the source of truth for implemented features. Each @ref: block in source holds: Feature, Status, CLL, PlanSection, and optional Deviation, Notes.

Code-first workflow

When you implement or fix a feature:

1. Read the CLL section(s) cited in the open ticket row (if any).
2. Add or update #[jbo_ref(...)] on the Rust item (or a const marker for module-level gaps). Use comment blocks only in .egg / Cargo.toml.
3. If the feature is still AD HOC, PARTIAL, or MISSING, keep or update the matching OPEN.md row.
4. Run python3 scripts/sync_plan_ready.py to regenerate READY.md from code.
5. Run python3 scripts/ref_audit.py --strict and JBO_REF_STRICT=1 cargo build.

Migrating remaining gaps: use python3 scripts/migrate_plan_refs.py for templates. Completed features live in #[jbo_ref] (Rust), comment blocks (.egg/Cargo.toml), or src/plan_implemented.rs for bulk registry entries — then run sync_plan_ready.py.

See SCRIPTS.md for the full maintenance script reference.

Slug naming

Slugs follow layer.name and are stable across refactors:

Grammar rule alts use semantic names {cll_nonterminal}_{variant}. Tree extraction uses CLL-aligned disambiguation: longest-match for left-grouped ... repetition (CLL §21 rule 7), empty-alt preference for zero-width optional matches, shortest-base-alt for equal-span optional suffixes, and ParseTree::Ambig parse-forest nodes for remaining structural ambiguity.

Anchor formats

Rust (required — use #[jbo_ref], not hand-written /// @ref: comments):

#[jbo_ref(
    slug = "semantic.parse_sumti_atom",
    feature = "All sumti atom types",
    status = "IMPLEMENTED",
    cll = "§6.2, §6.6",
    plan_section = "2.4",
)]
fn parse_sumti_atom(...) { ... }

Egg / TOML comment block:

; @ref:grammar.sumti_6_zo
; Feature: ZO single-word quotation
; Status: IMPLEMENTED
; CLL: §19.10
; Notes: sumti_6_zo = ZO_clause any_word frees; word-1100 skips indicator merge after ZO
; PlanSection: 2.4

Validate with python3 scripts/sync_plan_ready.py, python3 scripts/ref_audit.py --strict, and JBO_REF_STRICT=1 cargo build after any change.

Status Legend

• ✅ IMPLEMENTED — fully working in lojban-rs
• ⚠️ PARTIAL — partially implemented or behind feature flag
• ⚠️ AD HOC — works, but implemented via hardcoded cmavo/special-case rather than generic rule
• ❌ MISSING — not implemented yet
• ✅ N/A — Not needed for lojban-rs (reference/design feature)
• ⏳ NEEDS EVAL — feature needs a math evaluator for full semantics
• 📝 DOC-ONLY — documentation/reference section with no parser gap

Plan maintenance scripts

Companion to RULES.md. Run bash scripts/regenerate_plan.sh to refresh the auto-generated sections and audit reports.

Detecting gaps and discrepancies

Regenerate everything

bash scripts/regenerate_plan.sh

This runs, in order:

1. python3 scripts/sync_plan_ready.py — regenerate READY.md from code #[jbo_ref] / @ref: blocks
2. python3 scripts/ref_audit.py — consistency report at scripts/ref_audit_report.md
3. python3 scripts/cll_coverage.py — CLL section coverage at scripts/cll_coverage_report.md
4. python3 scripts/grammar_audit.py — CLL Ch 21 non-terminal coverage at scripts/grammar_audit_report.md

CI on main runs the same pipeline and commits updated plan/READY.md plus audit reports when they drift.

After any feature change

python3 scripts/sync_plan_ready.py
python3 scripts/ref_audit.py --strict
JBO_REF_STRICT=1 cargo build

Architecture & tooling

Human-readable description of the parser pipeline, semantic layers, and subsystems. Open gaps are tracked in OPEN.md; completed features are auto-listed in READY.md.

Pure CFG Earley

The word-level Earley recognizer is a pure CFG: earley_word_schema.egg saturates all chart items with no ordered-choice pruning.

Behaviour

Tree extraction policy (src/earley_extract.rs)

1. Longest match — maximize child_end at each dot (CLL §21 rule 7, left-grouped ...; not PEG).
2. Zero-width tie — prefer alt ending in _empty (CLL optional []).
3. Equal non-zero span — prefer shortest alt name (base rule over optional suffix, e.g. sumti_6_koha over sumti_6_koha_frees).
4. Remaining equal-span ties — emit ParseTree::Ambig { alternatives } (parse forest).

AST resolution (src/earley_to_syntax.rs): resolve_ambig_first_ok tries each alternative at root and hot spots (sumti, paragraph, lerfu_word) until conversion succeeds.

Verification

• cargo test --test earley_integration — 85/85 pass (including indefinite-description, FA scrambling, semantics pipeline).
• cargo test --test earley_ambiguity_probe — corpus accepted; report at scripts/grammar_ambiguity_report.json.
• python3 scripts/grammar_audit.py — 374 egg rules vs 90 CLL non-terminals.
• No peg_alt_priority / grammar_alt_priority references remain in the codebase.

Comprehensive Feature Gap Analysis: CLL vs lojban-rs

Our parser must follow the grammar of @cll-md/chapter-grammars.md so no rule or part of it can be omitted. If there is or planned a deviation from that it must be done through a feature flag and reported by editing this document. Thus no simplficatons to the formal grammar are allowed. Fix related issues if any.

The codebase must be clean, stramlined, avoid duplication, avoid hardcoding where needed. the codebase must try to be generic where needed.

Ad hoc / architecture principles (avoid when implementing fixes):

1. No string comparisons on cmavo names — use selma'o checks, generated tables, or AST tags instead.
2. No hand-enumerating optional-position variants — prefer optional ([]) and repetition (...) in grammar; expand at generation time.
3. No layer crossing — morphology should not hide grammar structure (e.g., ZO/ZOI must consume quoted content) unless CLL explicitly says so.
4. No manual semantic tables in parser code — move tables like indicator_bridi_tail or ZAhO pairings into typed_dictionary.rs or external data files.

Gaps, deviations, and missing features are tracked once each in the section tables below (grouped by CLL topic). Do not maintain a separate duplicate index.

14. SEMANTIC RULES (egglog_rules.egg)

14.0 Rewrite rule taxonomy (3a–3d)

Tersmu/camxes-rs groups rewrite rules into four categories. lojban-rs implements the same rules under the §1–§23 section names below.

14.1 Implemented Rules (Internal egglog rules — no direct CLL mapping)

14.2 Testing Strategy (CLL Ch 2 — examples throughout)

• Add test cases for each new feature in the relevant test file
• Add CLL-referenced test sentences for each missing feature
• Ensure all 20 example tests pass before and after changes
• Add dedicated test files for complex features (mekso, abstractions, intervals)
• Add mekso-specific test suite with CLL examples 18.2–18.148

15. QUANTIFIER SCOPE & naku BOUNDARIES — IMPLEMENTATION

15.1 Problem Statement

egglog rewrite rules are unconditional pattern matches. They can match structural patterns like (PAnd p q) but cannot express predicate conditions like "x is not free in q". This blocks:

• Partial distribution: ∃x.(P∧Q) → (∃x.P)∧Q when x∉FV(Q)
• Vacuous quantification: ∀x.P → P when x∉FV(P)
• Quantifier over implication: ∀x.(P→Q) → (∃x.P→Q) when x∉FV(Q)
• naku partial distribution: naku (∃x.P ∧ Q) ↔ (∀x.(naku P) ∨ naku Q) when x∉FV(Q)

The negation push-through rule (¬∃x.P ↔ ∀x.¬P) already handles the core naku boundary case, but partial distribution under quantifiers was the gap.

15.2 Solution: Two-Phase Architecture

The solution uses two complementary phases that together cover all cases:

Phase 1 (Rust pre-lowering)          Phase 2 (egglog saturation)
─────────────────────────            ──────────────────────────
simplify_prop() on JboProp           FreeIn facts + conditional rules
    │                                     │
    ├─ Partial distribution               ├─ Partial distribution
    ├─ Vacuous quantifier removal         ├─ Vacuous quantification
    │                                     ├─ Quantifier over implication
    │                                     │
    ▼                                     ▼
  Lowered to egglog ◄──────────── FreeIn(BoundVar(v), subprop) = 0/1

Phase 1 handles the initial parse form before saturation. It's fast, deterministic, and handles the common case.

Phase 2 handles forms discovered during equality saturation. When egglog rewrites produce new quantified forms, the conditional rules can simplify them.

15.3 Phase 1: Rust Pre-Lowering Simplification

File: jbo_prop.rs — pub fn simplify_prop(prop: &JboProp) -> JboProp

Core mechanism: A recursive contains_bound_var(v, prop) function traverses JboProp (including HOAS closures) to check if BoundVar(v) appears in a subformula. When it doesn't, the quantifier is vacuous or partial distribution applies.

Rules implemented (6 distribution + 1 vacuous):

Hook point: egglog_lower.rs:lower_texticule() calls simplify_prop() before lowering each TexticuleProp.

Helper functions (all in jbo_prop.rs):

• contains_bound_var(v, prop) — main checker
• contains_bound_var_in_rel(v, rel) — relation traversal
• contains_bound_var_in_term(v, term) — term traversal
• contains_bound_var_in_mex(v, mex) — mex expression traversal
• contains_bound_var_in_operator(v, op) — operator traversal
• contains_bound_var_in_tag(v, tag) — tag traversal
• contains_bound_var_in_tag_unit(v, tu) — tag unit traversal

Tests: 6 unit tests in jbo_prop::simplify_tests covering vacuous removal, partial distribution, and negative cases.

15.4 Phase 2: egglog FreeIn Facts + Conditional Rules

Schema (egglog_schema.egg):

(function FreeIn (JboTerm JboProp) i64 :merge (max old new))

• FreeIn(BoundVar(v), prop) = 1 means v is free in prop
• FreeIn(BoundVar(v), prop) = 0 (default) means v is not free (or not checked)
• Merge: max(old, new) — once set to 1, stays 1

Lowering (egglog_lower.rs):

• generate_free_in_facts(prop, lines) — entry point, called from lower_texticule()
• collect_free_in_facts(bound_var_idx, prop, lines) — recursive traversal
• For each PQuant(v, body), evaluates body(1) and asserts (set (FreeIn (BoundVar 1) subprop) 1) for every subprop containing BoundVar(1)
• Helper functions: term_contains_bound_var, prop_contains_bound_var, rel_contains_bound_var, mex_contains_bound_var, op_contains_bound_var, tag_contains_bound_var, tag_unit_contains_bound_var

Conditional rules (egglog_rules.egg §7c) — 12 rules:

; ∃x.(P∧Q) → (∃x.P)∧Q when x∉FV(Q)
(rule ((PQuant (Exists) restr (PAnd p q) v)
       (= (FreeIn (BoundVar v) q) 0))
      ((union (PQuant (Exists) restr (PAnd p q) v)
              (PAnd (PQuant (Exists) restr p v) q))))

Full list:

1. ∃-conjunction: (P∧Q) with x∉FV(Q) and x∉FV(P)
2. ∀-disjunction: (P∨Q) with x∉FV(Q) and x∉FV(P)
3. ∀-conjunction: (P∧Q) with x∉FV(Q) and x∉FV(P)
4. ∃-disjunction: (P∨Q) with x∉FV(Q) and x∉FV(P)
5. ∀-implication: (P→Q) with x∉FV(Q)
6. ∃-implication: (P→Q) with x∉FV(Q)
7. Vacuous ∀: any body with x∉FV(body)
8. Vacuous ∃: any body with x∉FV(body)

Key design decision: Using (= (FreeIn ...) 0) instead of (not (FreeIn ...)) because egglog's not requires built-in Bool type, but FreeIn returns i64. The = 0 check achieves the same semantics.

15.5 How the Two Phases Interact

Input: ∃x.(P(x) ∧ Q)
         │
         ▼
Phase 1: simplify_prop()
  - contains_bound_var(1, Q) = false
  - Apply ∃-conjunction-left: (∃x.P(x)) ∧ Q
         │
         ▼
Lowering: egglog_lower.rs
  - Lower (∃x.P(x)) ∧ Q to egglog
  - Generate FreeIn facts:
    - FreeIn(BoundVar(1), P(BoundVar(1))) = 1  [P contains x]
    - FreeIn(BoundVar(1), Q) = 0  [Q does not contain x]
         │
         ▼
Phase 2: egglog saturation
  - If equality saturation produces ∃x.(P∧Q) again
  - §7c rule fires: (= (FreeIn (BoundVar v) q) 0) → union with (∃x.P)∧Q

15.6 Status Updates

§14.1: Added §7c Quantifier Scope Conditional Rules to implemented rules list.

§15.7 naku Negation Boundaries — How They're Solved

The CLL §16.9 rule "naku ro da P ↔ su'o da naku P" is semantically identical to ¬∀x.P ↔ ∃x.¬P, which was already implemented in §7 (negation push-through). The partial distribution rules in §7c complete the picture:

• naku (∃x.P ∧ Q) = ¬∃x.(P ∧ Q)
• By §7: ¬∃x.(P ∧ Q) = ∀x.¬(P ∧ Q) = ∀x.(¬P ∨ ¬Q)
• If x∉FV(Q): by §7c: ∀x.(¬P ∨ ¬Q) → (∀x.¬P) ∨ ¬Q = (∀x.naku P) ∨ naku Q

This is the composition of existing §7 rules + new §7c rules — no separate naku-specific rules needed.

16. OLOG INTEGRATION (dzaske)

Ologs (Ontology Logs) are a category-theoretic knowledge-representation format. lojban-rs embeds the dzaske olog system with bidirectional integration: extract schemas from parsed Lojban, validate instance data, run relational queries, and compose with the egglog e-graph.

Theory & sources: docs/ologs.md, docs/olog/sources/ (Spivak & Kent 2012, Patterson 2017, Lambert & Patterson 2024).

Note: Olog integration uses Cargo features olog and olog-proofs (both default-on). See @ref:feature.olog.

16.1 Core extraction

Extraction mapping:

16.2 Validation & querying

16.3 Bundled corpus

16.4 Egglog composition (Layers A/B/C)

Tests: cargo test --test camxes_olog_egglog.

17. PROLOG EXPORT

Prolog source generation from Lojban semantics via a target-neutral Prolog IR (src/prolog/: AST + tokenizer + precedence-climbing parser + dialect-aware pretty-printer). Two emission dialects behind PrologDialect:

• Swi — executable SWI-Prolog source (:-, ?-, \+, is/2, =.., lists, member/2).
• Tersmu — tersmu/lojysamban parity mode matching examples/*.loj (Skolem constants c0/c1, --> implication, non-veridical: side-facts, ju'a nai rewrites).

The legacy SWI-dialect string API (prop_to_prolog, semantic_results_to_prolog, eval_text_to_prolog) is preserved for backward compatibility; new code uses the _dialect variants. References: docs/prolog/references.md.

18. SEMANTIC EQUIVALENCE & OUTPUT FORMATS

18.1 Semantic equivalence

18.2 Output formats

18.3 Future CLI (tersmu parity)

lojban-rs has no main.rs today. tersmu/camxes-rs CLI flags for reference when a binary is added: --json, -E/--egglog, --equiv=S, -O/--olog, --olog-schema=F, -P/--prolog, -l/--loj, -j/--jbo.

Open Tickets

Manual tracking for MISSING, PARTIAL, AD HOC, NEEDS EVAL, and @ref:plan.* rows without a code anchor. Completed work moves to code #[jbo_ref] entries and appears in READY.md after sync_plan_ready.py.

3. TENSES & MODALS (CLL Ch 10)

Simple tense cmavo from CLL §10.2–10.11 (PU/ZI/FAhA/VA/ZAhO/ZEhA/VEhA/VIhA/MOhI/TAhE/ROI/re'u/FEhE/KI/CUhE/CAhA and compounds) are implemented — see auto-generated §3.1 Spatial Tenses, §3.2 Temporal Tenses, and §8.1–8.2. Remaining Ch 10 gaps are tracked in §3.6 below (§10.23 tense vs modals). §10.26–10.28 are reference/summary (N/A for parser).

3.6 Complex Tense Constructs (remaining)

5. NEGATION (CLL Ch 15)

5.2 Scalar Negation (CLL Ch 15)

5.6 Metalinguistic Negation (CLL Ch 15)

6. QUANTIFIERS (CLL Ch 16)

6.3 bu'a-series (selbri variables)

bu'a/bu'e/bu'i (selma'o GOhA) are second-order predicate-logic relation variables (CLL §16.13). Core quantification, xi subscripts (bu'a xi re == bu'e), and prenex su'o/ro forms are implemented — see @ref:semantic.tu_is_buha in READY.md. The remaining AD HOC special cases are tracked here as a single consolidated ticket.

7. ABSTRACTIONS (CLL Ch 11)

7.3 Event Contour Relationship (CLL Ch 11)

9. MEKSO / MATHEMATICS (CLL Ch 18)

9.7 Mekso Selbri & Conversions (CLL §18.7, §18.11, §18.18–18.19, §18.21)

10. LETTERALS (CLL Ch 17)

CLL §17.14 auxiliary lerfu-word cmavo (this chapter):

Not letterals (were incorrectly listed under the old §9.8 “Acronyms” ticket): la'u (BAI modal “with quantity”, §9.6/§10.25), te'u (TEhU mekso/vector terminator, §18.15/§18.18), ce'u (KOhA abstraction focus, §7.11) — implemented elsewhere; see auto-generated §7.11, §9.6, §18.15.

Core BY/LAU/tei…foi/bu parsing is implemented — see auto-generated §9.8 lerfu entries and @ref:grammar.lerfu_word_lau_chain. Open gaps below.

10.1 Shift & Alphabet Cmavo (CLL §17.3, §17.5, §17.7)

10.2 Acronyms & Lerfu Names (CLL §17.12)

10.3 Mathematical Lerfu Strings (CLL §17.11)

11. ATTITUDINALS & INDICATORS (CLL Ch 13, 21)

11.1 Vocatives (CLL Ch 6, 13)

11.2 Miscellaneous (CLL Ch 13, 19)

11.3 Formal Grammar (CLL Ch 21)

17. PROLOG EXPORT — tersmu parity gaps

The Prolog IR (src/prolog/), dialect flag (PrologDialect::Swi / Tersmu), AST lowerer, tersmu display-format path (eval_text_to_tersmu_lines, behind tersmu-parity), and the rendering/AST fixes (connective normalization, is/2 arithmetic goals, AbsPred/AbsProp/Moi lowering, tanru seltau in convert_selbri_3) are implemented — see auto-generated §17 in READY.md. Remaining examples/*.loj byte-parity gaps are upstream PARSER/semantic issues (forethought ganai…gi / afterthought .e/.ijanai logical connection not producing Connected props), tracked under §3/§5.

Implemented Features (auto-generated)

1.1 Phonology (CLL Ch 3)

1.2 Word Classes (CLL Ch 4)

1.3 Lujvo Formation & Decomposition (CLL Ch 4, 12)

1.4 Fu'ivla (CLL Ch 4)

1.5 Cmevla (CLL Ch 4)

2.1 Text Structure (CLL Ch 19)

2.2 Sentence Structure (CLL Ch 9, 19)

2.3 Terms (CLL Ch 9, 14, 16)

2.4 Sumti (CLL Ch 6, 8, 14)

2.5 Relative Clauses (CLL Ch 8)

2.6 Selbri (CLL Ch 5, 11)

2.7 Selbri Place Structure (CLL Ch 9)

2.8a SE conversion AST + type inference (CLL §9.4, §6.8)

2.8 Pro-sumti and Pro-bridi (CLL Ch 7)

3.1 Spatial Tenses (CLL Ch 10)

3.2 Temporal Tenses (CLL Ch 10)

3.3 Aspect & Modality (CLL Ch 10)

3.4 BAI Modal Tags (CLL Ch 9)

3.5 Modal Connections (CLL Ch 9)

3.6 Complex Tense Constructs (remaining)

4.1 Logical Connectives (CLL Ch 14)

4.2 Gihek (Bridi-tail connection) (CLL Ch 14)

4.3 Non-Logical Connectives (CLL Ch 14)

4.4 Termset Connection (CLL Ch 14)

4.5 Tensed Connectives (CLL Ch 10, 14)

4.6 Connective Questions (CLL Ch 14)

5.1 Bridi Negation (CLL Ch 15)

5.2 Scalar Negation (CLL Ch 15)

5.3 Sumti Negation (CLL Ch 15, 16)

5.4 nai Suffix Negation (CLL Ch 15)

5.5 Affirmation (CLL Ch 15)

6.1 Variables (CLL Ch 16)

6.2 Prenex (CLL Ch 16)

6.3 Quantifiers (CLL Ch 16)

6.4 Scope & DeMorgan (CLL Ch 16)

7.1 Abstractor Types (CLL Ch 11)

7.2 Abstractor Features (CLL Ch 7, 11)

7.3 Event Contour Relationship (CLL Ch 11)

8.1 Tense Conversion (CLL Ch 10)

8.2 Complex Tense Constructs (CLL Ch 10)

9.1 Numbers & Punctuation (CLL §18.2–18.4)

9.2 Operators & Infix (CLL §18.5, §18.14, §18.24)

9.3 Forethought & Reverse Polish (CLL §18.6, §18.16)

9.4 Non-decimal & Compound Bases (CLL §18.10)

9.5 Vectors & Matrices (CLL §18.15)

9.6 Indefinite & Approximate Numbers (CLL §18.8–18.9)

9.7 Mekso Selbri & Conversions (CLL §18.7, §18.11, §18.18–18.19)

9.8 Mekso Evaluator (NEEDED for full semantics)

11.1 Emotion Indicators (CLL Ch 13)

11.2 Scale System (CLL Ch 13)

11.3 Emotional Categories (CLL Ch 13)

11.5 Vocatives (CLL Ch 6, 13)

11.6 Miscellaneous (CLL Ch 13, 19)

12. TEXT STRUCTURE (CLL Ch 19)

12b.4 Status

13.1 Selma'o Catalogue (CLL Ch 20)

13.2 Formal Grammar (CLL Ch 21)

14.1 Implemented Rules (Internal egglog rules — no direct CLL mapping)

17. PROLOG EXPORT — tersmu parity

16

16.2

16.3

16.4

16.6

16.7

16.8

18