Crate logicaffeine_language

Expand description

§logicaffeine-language

The English → first-order logic pipeline: lexer, parser, semantics, and transpiler that turn natural-language sentences into formal logic with neo-Davidsonian event semantics and ontology expansion.

Part of the Logicaffeine workspace. Tier 3 — depends on logicaffeine_base, logicaffeine_lexicon, logicaffeine_proof.

§Role in the workspace

This is the language front-end. It sits between the structural atoms (logicaffeine-base — arena, interner, spans), the vocabulary (logicaffeine-lexicon), and the proof engine (logicaffeine-proof), and is consumed by the compiler, CLI, LSP, and web app. See logic-mode.md.

Input → Lexer → Parser (AST + DRS) → Semantics → Transpiler → FOL

Lexer (lexer, token, lexicon) — two-stage: structural LineLexer then token Lexer, with morphology, multi-word-expression collapsing (mwe), and lexicon lookup.
Parser (parser/{clause,noun,verb,quantifier,modal,question,pragmatics}) — hand-written recursive descent over arena-allocated AST, with discourse tracking via Discourse Representation Structures (drs). Declarative (NL) and imperative (LOGOS) modes selected by ParserMode.
AST (ast/{logic,stmt,theorem}) — the arena-lifetime LogicExpr<'a> / Term<'a> logical form plus statement and theorem nodes.
Semantics (semantics/{axioms,kripke,knowledge_graph}, lambda, scope) — axiom expansion, Kripke lowering for modals, intensional/event readings, and Montague-style lambda transforms.
Transpiler (transpile, formatter) — renders the logical form to the target notation.

The parser handles both declarative natural language and the imperative LOGOS surface (selected by ParserMode), so recent imperative constructs — ## Define definitional blocks and the followed by sequence-concatenation operator among them — flow through this same front-end; the full LOGOS surface is in the imperative-mode guide.

§Module map

Grouped by pipeline stage. intern and arena re-export the logicaffeine-base primitives so downstream crates need only depend on this one.

Module	Role
`token`, `lexer`, `lexicon`, `mwe`	tokenization: structural `LineLexer` → token `Lexer`, morphology, lexicon lookup, multi-word-expression collapsing
`parser`, `ast`, `arena_ctx`	recursive-descent parse into arena-allocated AST (`arena_ctx` owns the allocation context)
`drs`, `session`, `pragmatics`	discourse: Discourse Representation Structures, the incremental-evaluation `Session`, and post-parse pragmatic inference
`semantics`, `lambda`, `scope`, `ontology`	axiom expansion, Montague lambda transforms, quantifier-scope permutation, and sort/anaphora ontology checks
`transpile`, `formatter`, `view`, `style`	render the logical form; `view` is the owned serialization form, `style` adds ANSI coloring
`source_format`	the canonical LOGOS source formatter (`format_source`/`format_line`) — structural reindent (4 spaces per lexed nesting level), string/prose interiors untouched; one rule set shared by the LSP’s formatting providers and `largo fmt`
`token_class`	the single token-classification truth (verbs=function, nouns=type, …) every highlighting surface derives from — LSP semantic tokens and the REPL’s ANSI painting can never disagree
`teach`	the single teaching truth: a `ConstructDoc` lesson (one plain sentence + runnable example + socratic question/tip, all required by the type) for every taught keyword, every `##` block type, and the built-in types — LSP hover/completion docs and the REPL’s `:explain` all derive from this table, ratcheted by `tests/teach_lock.rs`; also the literate-doc extractors (`module_doc`/`doc_for_header_at`/`extract_literate_docs`) that turn a `## Note` above a definition into its hover documentation
`analysis`, `registry`, `symbol_dict`	static discovery passes (`## Definition` scan), the symbol/type registries, and symbol-dictionary extraction
`optimization`, `proof_convert`	the shared `Opt` optimization bitset and the bridge from arena `LogicExpr` to the proof engine’s owned `ProofExpr`
`ast_depth`	the nesting-depth gate: rejects programs whose AST nests deeper than every downstream walker (optimizer, codegen, interpreter, VM) can safely recurse — `AstTooDeep` at parse time instead of a stack overflow later
`error`, `suggest`, `visitor`, `debug`, `analysis`	parse-error types + Socratic explanations, spelling suggestions, the AST visitor, and interner-aware debug display

§Public API

All fallible entry points return Result<_, ParseError>; compile_forest is infallible (it returns whatever readings parse).

Function	Signature	Purpose
`compile`	`(&str) -> Result<String, ParseError>`	Unicode FOL (default)
`compile_simple`	`(&str) -> Result<String, ParseError>`	ASCII SimpleFOL
`compile_kripke`	`(&str) -> Result<String, ParseError>`	modals as explicit world quantification
`compile_pragmatic`	`(&str) -> Result<String, ParseError>`	adds scalar-implicature enrichment (`some` ⇝ `∃ +> ¬∀`)
`compile_with_options`	`(&str, CompileOptions) -> Result<String, ParseError>`	choose `format` + `pragmatic`
`compile_all_scopes`	`(&str) -> Result<Vec<String>, ParseError>`	every quantifier-scope permutation
`compile_forest`	`(&str) -> Vec<String>`	every parse reading (noun/verb, PP attachment)
`compile_ambiguous`	`(&str) -> Result<Vec<String>, ParseError>`	readings × scopes
`compile_discourse`	`(&[&str]) -> Result<String, ParseError>`	batch with shared discourse context
`compile_with_discourse`	`(&str, &mut WorldState, &mut Interner) -> Result<String, ParseError>`	thread your own discourse state
`compile_theorem`	`(&str) -> Result<String, ParseError>`	parse + prove a `Given:`/`Prove:` block

Each entry point has a *_with_options companion taking CompileOptions. MAX_FOREST_READINGS (= 12) caps forest size to bound combinatorial blowup. Lower-level variants (compile_kripke_with, compile_with_world_state{,_options}, compile_with_world_state_interner_options) expose the WorldState / Interner directly.

Key types and re-exports:

OutputFormat — Unicode (default), LaTeX, SimpleFOL, Kripke.
CompileOptions { format: OutputFormat, pragmatic: bool } — defaults to { Unicode, false }.
Session — multi-sentence discourse: new / with_format, eval, history, turn_count, world_state{,_mut}, reset. Carries anaphora state across eval calls.
Pipeline types: Lexer, LineLexer, LineToken, Token/TokenType, Parser, ParserMode, NegativeScopeMode, QuantifierParsing, Drs/WorldState, ParseError/ParseErrorKind/socratic_explanation, TypeRegistry, SymbolRegistry, AstContext, TranspileContext.
proof_convert (logic_expr_to_proof_expr, term_to_proof_term) bridges the arena LogicExpr<'a> to the proof engine’s owned ProofExpr/ProofTerm; compile_theorem proves via logicaffeine_proof.
optimization is the single source of truth for compiler optimization toggles (an OptimizationConfig u64 bitset over the 40-pass Opt enum), shared across the AOT/run/VM/JIT/codegen paths. It lives here because the parser maps ## No <X> source decorators onto Opts.

§Quick example

use logicaffeine_language::compile;

let fol = compile("Every man is mortal.").unwrap();
assert_eq!(fol, "∀x((Man(x) → Mortal(x)))");

Discourse across sentences:

use logicaffeine_language::Session;

let mut s = Session::new();
s.eval("A man walked in.").unwrap();
s.eval("He sat down.").unwrap();   // "He" resolves to "a man"
let transcript = s.history();

§Feature flags

Feature	Default	Description
`dynamic-lexicon`	off	Enables runtime lexicon loading (`logicaffeine-lexicon/dynamic-lexicon`), re-exported as the `runtime_lexicon` module.

A build.rs step compiles assets/lexicon.json into generated Rust tables (lexicon, multi-word expressions, ontology, axioms) under OUT_DIR; changing the lexicon requires a rebuild.

§Dependencies

Internal: logicaffeine-base (arena, interner, symbols, spans — re-exported as Arena/Interner/Symbol), logicaffeine-lexicon (vocabulary), logicaffeine-proof (theorem proving).

External: bumpalo (arena allocation), serde + serde_json (hardware/ontology types and build-time lexicon compilation).

§License

Business Source License 1.1 — see LICENSE.md.

Docs index · Root README · Changelog

Re-exports§

pub use proof_convert::logic_expr_to_proof_expr;
pub use proof_convert::term_to_proof_term;
pub use token::BlockType;
pub use token::FocusKind;
pub use token::MeasureKind;
pub use token::PresupKind;
pub use token::Span;
pub use token::Token;
pub use token::TokenType;
pub use lexer::Lexer;
pub use lexer::LineLexer;
pub use lexer::LineToken;
pub use parser::Parser;
pub use parser::ParserMode;
pub use parser::NegativeScopeMode;
pub use parser::QuantifierParsing;
pub use error::ParseError;
pub use error::ParseErrorKind;
pub use error::socratic_explanation;
pub use drs::Drs;
pub use drs::BoxType;
pub use drs::WorldState;
pub use analysis::TypeRegistry;
pub use registry::SymbolRegistry;
pub use arena_ctx::AstContext;
pub use session::Session;
pub use compile::compile;
pub use compile::compile_pragmatic;
pub use compile::compile_simple;
pub use compile::compile_kripke;
pub use compile::compile_kripke_with;
pub use compile::compile_with_options;
pub use compile::compile_with_world_state;
pub use compile::compile_with_world_state_options;
pub use compile::compile_with_discourse;
pub use compile::compile_with_world_state_interner_options;
pub use compile::compile_all_scopes;
pub use compile::compile_all_scopes_with_options;
pub use compile::compile_forest;
pub use compile::compile_forest_with_options;
pub use compile::MAX_FOREST_READINGS;
pub use compile::compile_discourse;
pub use compile::compile_discourse_with_options;
pub use compile::compile_ambiguous;
pub use compile::compile_ambiguous_with_options;
pub use compile::compile_theorem;

Modules§

analysis: Static analysis passes for type and policy discovery.
arena
arena_ctx: Arena context for AST allocation.
ast: Abstract Syntax Tree types for both logical expressions and imperative statements.
ast_depth: The AST depth gate — “parsed ⇒ bounded”.
compile: Compilation API
debug: Debug display utilities for AST types with interner access.
drs: Discourse Representation Structure (DRS) for anaphora resolution and scope tracking.
error: Error types and display formatting for parse errors.
formatter: Output formatters for logical expressions.
intern
lambda: Lambda calculus transformations for Montague-style compositional semantics.
lexer: Two-stage lexer for LOGOS natural language input.
lexicon: Lexicon: Vocabulary lookup functions
mwe: Multi-Word Expression (MWE) processing.
ontology: Ontology module for bridging anaphora and sort compatibility checking.
optimization: The single source of truth for compiler optimization toggles.
parser: Recursive descent parser for natural language to first-order logic.
pragmatics: Post-parse pragmatic inference transformations.
proof_convert: Conversion from parser AST to proof engine representation.
registry: Symbol registry for consistent variable naming in FOL output.
scope: Scope stack for variable binding during code generation.
semantics: Semantic transformations for logical expressions.
session: Session Manager for Incremental Evaluation
source_format: The canonical LOGOS source formatter.
style: ANSI terminal color styling for error messages.
suggest: Spelling suggestions for unknown words.
symbol_dict: Symbol Dictionary Extraction
teach: The one teaching truth for LOGOS constructs: every lesson a surface shows — LSP hover, completion documentation, the REPL’s :explain — comes from THIS table, so the editor and the terminal always teach the same thing.
token: Token types for the LOGOS lexer and parser.
token_class: The one classification truth for LOGOS tokens: parts of speech ARE the syntax — verbs paint as functions, nouns as types, adjectives as modifiers. Every highlighting surface (LSP semantic tokens, the terminal REPL, any future renderer) derives its colors from THIS mapping, so they can never disagree.
transpile: Transpilation from AST to first-order logic notation.
view: Owned view types for AST serialization and display.
visitor: AST visitor pattern for traversing logical expressions.

Structs§

Arena: A bump allocator for stable, arena-allocated references.
BaseSpan: A byte-offset range in source text.
CompileOptions
Interner: A string interner providing O(1) equality comparison via Symbol handles.
Symbol: A lightweight handle to an interned string.
TranspileContext

Enums§

Case: Grammatical case (for pronouns).
Gender: Grammatical gender (for pronouns and agreement).
Number: Grammatical number for nouns and agreement.
OutputFormat

Traits§

SymbolEq: Convenience trait for comparing a Symbol to a string literal.