aufbau 0.1.0

Type-aware constrained decoding for LLMs using context-dependent grammars with typing rules
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

// Type system core definitions and re-exports

pub mod binding;
pub mod core;
pub mod eval;
pub mod ops;
pub mod rule;
pub mod symbols;
pub mod syntax;
pub mod tree;

pub use tree::*;

pub use core::{Context, TreeRef};
pub use eval::evaluate_typing;
pub use ops::{equal, subtype, Unifier, UnifyResult};
pub use symbols::{gather_raw_types, gather_terminal_nodes, gather_terminals, gather_terminals_typed, gather_type_symbols};
///---------------
/// Type Representation
///---------------

#[derive(Debug, Clone)]
pub enum Type {
    // Base types as bindable vars
    Atom(String),
    // Meta type variables for inference (e.g. ?A, ?B in typing rules)
    Meta(String),
    // Raw/concrete types (e.g., 'int', 'string') - literal types that don't need variable resolution
    Raw(String),
    // Function types (τ₁ → τ₂)
    Arrow(Box<Type>, Box<Type>),
    // Union types (τ₁ | τ₂ | ...)
    Union(Vec<Type>),
    // Negation type (¬τ) - "anything that is not τ"
    Not(Box<Type>),
    // Context call (Γ(x)) - lookup the type of variable x in context Γ
    ContextCall(String, String), // (context_name, variable_name)
    // Any type - accepts all inputs (⊤, the universal type)
    Any,
    // None type - rejects all inputs (∅, the empty type)
    None,

    // partial expression: parsed type-so-far plus original input string for continuation analysis
    Partial(Box<Type>, String),

    // "Fake" type for binding resolution
    Path(TreePath), // Absolute path to a binding location
    // path of the node at this location
    // type is a pattern
    PathOf(Box<Type>, TreePath),
}

// Re-export frequently used items for external users of the module.
pub use rule::{
    Conclusion, Premise, Term, TypeAscription, TypeSetting, TypingJudgment, TypingRule,
};

use crate::logic::typing::core::TreePath;

#[cfg(test)]
mod tests;