minitt 0.4.3

Mini-TT, a dependently-typed lambda calculus, extended and (re)implemented in Rust
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

#[macro_use]
extern crate minitt;

use minitt_util::repl::ReplEnvType;

/// CLI arguments. Based on structopt (clap)
mod args;

/// File IO. Build AST.
mod util;

/// REPL
mod repl;

pub fn main() {
    use minitt::check::check_main;
    let args = args::pre();

    // Parse
    let checked = args
        .file
        .clone()
        .and_then(|s| util::parse_file(s.as_str(), args.lexical_json))
        .map(|ast| {
            if !args.quiet {
                println!("Parse successful.");
                if args.generated {
                    println!("{}", ast);
                }
            }
            if !args.parse_only {
                // Type Check
                let checked = check_main(ast)
                    .map_err(|err| eprintln!("{}", err))
                    .unwrap_or_else(|()| {
                        eprintln!("Type-Check failed.");
                        std::process::exit(1);
                    });
                if !args.quiet {
                    println!("Type-Check successful.");
                }
                checked
            } else {
                Default::default()
            }
        })
        .unwrap_or_else(|| Default::default());

    // REPL
    repl::repl(
        checked,
        if args.interactive_plain {
            Some(ReplEnvType::Plain)
        } else if args.interactive {
            Some(ReplEnvType::Rich)
        } else {
            None
        },
    );
}