aufbau 0.1.2

Generalized prefix parsing for a class of context-dependent languages
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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135

use super::{Grammar, Symbol};
use crate::logic::typing::Conclusion;
use std::path::Path;

impl Grammar {
    /// Produce the textual specification string.
    pub fn to_spec_string(&self) -> String {
        let mut out = String::new();
        // Preserve original declaration order; fall back to sorted for any missing
        let nt_list: Vec<&String> = self.productions.keys().collect();

        // ---------- Productions ----------
        out.push_str("// --- Production Rules ---\n");
        for nt in nt_list {
            if let Some(alts) = self.productions.get(nt) {
                let mut first = true;
                for prod in alts {
                    let lhs = if let Some(rule_name) = self.nonterminal_rule(nt) {
                        format!("{}({})", nt, rule_name)
                    } else {
                        nt.clone()
                    };

                    let rhs = self.format_rhs(&prod.rhs);

                    if first {
                        out.push_str(&format!("{} ::= {}", lhs, rhs));
                        first = false;
                    } else {
                        out.push_str(&format!(" | {}", rhs));
                    }
                }
                out.push('\n');
            }
        }
        out.push('\n');

        // ---------- Typing rules ----------
        if !self.rules.is_empty() {
            out.push_str("// --- Typing Rules ---\n");
            let mut rule_list: Vec<_> = self.rules.values().collect();
            rule_list.sort_by_key(|r| &r.name);

            for rule in rule_list {
                out.push_str(&format_premises(&rule.premises));
                out.push('\n');
                let concl_str = format_conclusion(&rule.conclusion);
                let line = "-".repeat(std::cmp::max(20, concl_str.len() + 5));
                out.push_str(&format!("{} ({})\n", line, rule.name));
                out.push_str(&concl_str);
                out.push_str("\n\n");
            }
        }

        out
    }

    /// Helper to format the right-hand side of a production
    fn format_rhs(&self, rhs_symbols: &[Symbol]) -> String {
        rhs_symbols
            .iter()
            .map(|s| self.format_symbol(s))
            .collect::<Vec<_>>()
            .join(" ")
    }

    fn format_symbol(&self, symbol: &Symbol) -> String {
        match symbol {
            Symbol::Nonterminal { name, binding, .. } => {
                if let Some(b) = binding {
                    format!("{}[{}]", name, b)
                } else {
                    name.to_string()
                }
            }
            Symbol::Terminal { regex, binding } => {
                let base = format!("/{}/", regex.to_pattern());
                if let Some(b) = binding {
                    format!("{}[{}]", base, b)
                } else {
                    base
                }
            }
        }
    }

    /// Write the textual specification to a file on disk.
    pub fn save<P: AsRef<Path>>(&self, path: P) -> std::io::Result<()> {
        std::fs::write(path, self.to_spec_string())
    }
}

/// Helper to format a list of premises as a string
fn format_premises(premises: &[crate::logic::typing::Premise]) -> String {
    use crate::logic::typing::TypingJudgment;

    premises
        .iter()
        .map(|p| match (&p.setting, &p.judgment) {
            (Some(setting), Some(TypingJudgment::Ascription((term, ty)))) => {
                if setting.extensions.is_empty() {
                    format!("{} ⊢ {} : {}", setting.name, term, ty)
                } else {
                    let exts = setting
                        .extensions
                        .iter()
                        .map(|(v, t)| format!("[{}:{}]", v, t))
                        .collect::<Vec<_>>()
                        .join("");
                    format!("{}{} ⊢ {} : {}", setting.name, exts, term, ty)
                }
            }
            (None, Some(TypingJudgment::Ascription((term, ty)))) => {
                format!("{} : {}", term, ty)
            }
            (None, Some(TypingJudgment::Membership(var, ctx))) => {
                format!("{} ∈ {}", var, ctx)
            }
            (Some(_), Some(TypingJudgment::Membership(var, ctx))) => {
                // Membership with setting doesn't make sense in current design, but handle it
                format!("{} ∈ {}", var, ctx)
            }
            (_, Some(TypingJudgment::Operation { left, op, right })) => {
                format!("{} {} {}", left, op, right)
            }
            (Some(setting), None) => setting.name.to_string(),
            (None, None) => String::new(),
        })
        .collect::<Vec<_>>()
        .join(", ")
}

fn format_conclusion(conclusion: &Conclusion) -> String {
    format!("{}", conclusion)
}