logicaffeine_language/
lib.rs

1#![cfg_attr(docsrs, feature(doc_cfg))]
2#![doc = include_str!("../README.md")]
3
4// Re-export base types for internal use and consumers
5pub use logicaffeine_base::{Arena, Interner, Symbol, SymbolEq, Span as BaseSpan};
6
7// Provide an `intern` module alias for internal code that uses `crate::intern::*`
8pub mod intern {
9    pub use logicaffeine_base::{Interner, Symbol, SymbolEq};
10}
11
12// Provide an `arena` module alias for internal code that uses `crate::arena::*`
13pub mod arena {
14    pub use logicaffeine_base::Arena;
15}
16
17// Core modules
18pub mod token;
19pub mod token_class;
20pub mod teach;
21pub mod lexer;
22pub mod lexicon;
23pub mod drs;
24pub mod error;
25
26// Parser and AST
27pub mod parser;
28pub mod ast;
29
30// Semantic analysis
31pub mod semantics;
32pub mod lambda;
33pub mod transpile;
34
35// Compile API
36pub mod compile;
37
38// Support modules
39pub mod analysis;
40pub mod arena_ctx;
41pub mod ast_depth;
42pub mod formatter;
43pub mod mwe;
44pub mod ontology;
45pub mod pragmatics;
46pub mod registry;
47pub mod scope;
48pub mod session;
49pub mod source_format;
50pub mod suggest;
51pub mod symbol_dict;
52pub mod view;
53pub mod visitor;
54pub mod debug;
55pub mod style;
56
57// The single source of truth for compiler optimization toggles.
58pub mod optimization;
59
60// Proof conversion: bridges language AST to proof engine
61pub mod proof_convert;
62pub use proof_convert::{logic_expr_to_proof_expr, term_to_proof_term};
63
64// Re-export key types at crate root
65pub use token::{BlockType, FocusKind, MeasureKind, PresupKind, Span, Token, TokenType};
66pub use lexer::{Lexer, LineLexer, LineToken};
67pub use parser::{Parser, ParserMode, NegativeScopeMode, QuantifierParsing};
68pub use error::{ParseError, ParseErrorKind, socratic_explanation};
69pub use drs::{Drs, BoxType, WorldState, Gender, Number, Case};
70pub use analysis::TypeRegistry;
71pub use registry::SymbolRegistry;
72pub use arena_ctx::AstContext;
73pub use session::Session;
74
75// Compile API re-exports
76pub use compile::{
77    compile, compile_pragmatic, compile_simple, compile_kripke, compile_kripke_with, compile_with_options,
78    compile_with_world_state, compile_with_world_state_options,
79    compile_with_discourse, compile_with_world_state_interner_options,
80    compile_all_scopes, compile_all_scopes_with_options,
81    compile_forest, compile_forest_with_options, MAX_FOREST_READINGS,
82    compile_discourse, compile_discourse_with_options,
83    compile_ambiguous, compile_ambiguous_with_options,
84    compile_theorem,
85};
86
87// Runtime lexicon re-export (when dynamic-lexicon feature is enabled)
88#[cfg(feature = "dynamic-lexicon")]
89pub use logicaffeine_lexicon::runtime as runtime_lexicon;
90
91// Output format configuration
92#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
93pub enum OutputFormat {
94    #[default]
95    Unicode,
96    LaTeX,
97    SimpleFOL,
98    /// Kripke semantics output: modals lowered to explicit world quantification.
99    Kripke,
100}
101
102// Transpile context
103pub struct TranspileContext<'a> {
104    pub registry: &'a mut SymbolRegistry,
105    pub interner: &'a Interner,
106}
107
108impl<'a> TranspileContext<'a> {
109    pub fn new(registry: &'a mut SymbolRegistry, interner: &'a Interner) -> Self {
110        TranspileContext { registry, interner }
111    }
112}
113
114#[derive(Debug, Clone, Copy)]
115pub struct CompileOptions {
116    pub format: OutputFormat,
117    /// Enrich the parse with conversational (scalar) implicature (§8.7): a weak
118    /// scalar "some" is strengthened to `∃… +> ¬∀…`. Off by default so the literal
119    /// truth-conditional output is unchanged.
120    pub pragmatic: bool,
121}
122
123impl Default for CompileOptions {
124    fn default() -> Self {
125        CompileOptions {
126            format: OutputFormat::Unicode,
127            pragmatic: false,
128        }
129    }
130}
logicaffeine_language/lib.rs

logicaffeine_language/
lib.rs
