isabelle-dump/src/main.rs


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

use std::io::{self, BufRead, Write};

use lrlex::lrlex_mod;
use lrpar::lrpar_mod;

#[derive(Debug)]
pub enum Isabelle {
    Symbol(String),
    Text(String),
}


lrlex_mod!("calc.l");
lrpar_mod!("calc.y");


symbolmacro::make_symbols!();


fn main() {
    // Get the `LexerDef` for the `calc` language.
    let lexerdef = calc_l::lexerdef();
    let stdin = io::stdin();
    loop {
        io::stdout().flush().ok();
        match stdin.lock().lines().next() {
            Some(Ok(ref l)) => {
                if l.trim().is_empty() {
                    println!("");
                    continue;
                }
                let lexer = lexerdef.lexer(l);
                let (res, errs) = calc_y::parse(&lexer);
                for e in errs {
                    eprintln!(
                        "{}",
                        e.pp(&lexer, &calc_y::token_epp)
                    );
                }
                match res {
                    Some(r) => {
                        //eprintln!("Result: {:?}", r);
                        let rendered = r
                            .unwrap()
                            .iter()
                            .map(|token| match token {
                                Isabelle::Text(ref t) =>
                                    t,
                                Isabelle::Symbol(name) =>
                                    symbol(name)
                                    .unwrap_or_else(|| {
                                        Box::leak(
                                            format!("\\<{}>", name)
                                                .into()
                                        )
                                    })
                            })
                            .collect::<Vec<&str>>()
                            .join("");
                        println!("{}", rendered);
                    }
                    _ => {
                        eprintln!("could not parse file (probably spurious \\, <, or >)");
                        std::process::exit(1);
                    }
                }
            }
            _ => break,
        }
    }
}