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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94

// Type contradiction tests

use crate::logic::grammar::Grammar;
use crate::logic::partial::parse::Parser;
use crate::logic::typing::core::TreeStatus;
use crate::logic::typing::eval::check_tree;
use crate::set_debug_level;

fn load_grammar() -> Grammar {
    let spec = include_str!("../../../../examples/stlc.auf");
    Grammar::load(spec).expect("Failed to load STLC grammar")
}

#[test]
fn test_valid_app() {
    // (λx:X.x) should be valid (identity function)
    let grammar = load_grammar();
    let mut parser = Parser::new(grammar.clone());

    let input = "(λx:X.x)";
    println!("\n=== Valid Application Test ===");
    println!("Input: {}", input);

    let ast = parser.partial(input).expect("Failed to parse");
    let complete_trees: Vec<_> = ast
        .roots()
        .into_iter()
        .filter(|r| r.is_complete())
        .collect();

    let valid = complete_trees.iter().any(|tree| {
        let status = check_tree(tree, &grammar);
        !matches!(status, TreeStatus::Malformed)
    });

    assert!(valid, "Identity function should type-check");
}

#[test]
fn test_simple_lambda() {
    let grammar = load_grammar();
    let mut parser = Parser::new(grammar.clone());

    let input = "λx:A.x";
    println!("\n=== Simple Lambda Test ===");
    println!("Input: {}", input);

    let ast = parser.partial(input).expect("Failed to parse");
    let complete_trees: Vec<_> = ast
        .roots()
        .into_iter()
        .filter(|r| r.is_complete())
        .collect();

    for tree in &complete_trees {
        let status = check_tree(tree, &grammar);
        println!("Status: {:?}", status);
    }

    let valid = complete_trees
        .iter()
        .any(|tree| !matches!(check_tree(tree, &grammar), TreeStatus::Malformed));

    assert!(valid, "Simple lambda should type-check");
}

#[test]
fn test_unbound_variable() {
    // (λx:X.i) should fail - 'i' is unbound
    let grammar = load_grammar();
    let mut parser = Parser::new(grammar.clone());

    let input = "(λx:X.i)";
    println!("\n=== Unbound variable test ===");
    println!("Input: {}", input);

    set_debug_level(crate::DebugLevel::Trace);
    let ast = parser.partial(input).expect("Failed to parse");
    let complete_trees: Vec<_> = ast
        .roots()
        .into_iter()
        .filter(|r| r.is_complete())
        .collect();

    // All complete trees should be malformed (unbound variable)
    let all_malformed = complete_trees
        .iter()
        .all(|tree| matches!(check_tree(tree, &grammar), TreeStatus::Malformed));

    assert!(
        all_malformed,
        "Unbound variable 'i' should cause type error"
    );
}