oxilean-kernel 0.1.5

OxiLean kernel - The trusted computing base for type checking
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

//! `print_expr`, `print_expr_ascii`, `print_expr_with_config` and
//! `print_level` against verbatim copies of their earlier bodies.

use super::{print_expr, print_expr_ascii, print_expr_with_config, print_level};
use crate::prettyprint::types::{ExprPrinter, PrintConfig};
use crate::{BinderInfo, Expr, FVarId, Level, Literal, Name, Node};

fn old_print_expr(expr: &Expr) -> String {
    let mut printer = ExprPrinter::new();
    printer
        .print(expr)
        .expect("pretty-printer must succeed on valid expression");
    printer.output()
}
fn old_print_expr_ascii(expr: &Expr) -> String {
    let mut printer = ExprPrinter::new().with_unicode(false);
    printer
        .print(expr)
        .expect("pretty-printer must succeed on valid expression");
    printer.output()
}
fn old_print_expr_with_config(expr: &Expr, config: PrintConfig) -> String {
    let mut printer = ExprPrinter::with_config(config);
    printer
        .print(expr)
        .expect("pretty-printer must succeed on valid expression");
    printer.output()
}
fn old_print_level(level: &Level) -> String {
    let mut printer = ExprPrinter::new();
    printer
        .print_level(level)
        .expect("pretty-printer must succeed on valid level");
    printer.output()
}

fn levels() -> Vec<Level> {
    let u = Level::param(Name::str("u"));
    let v = Level::param(Name::str("v"));
    vec![
        Level::zero(),
        Level::succ(Level::zero()),
        Level::succ(Level::succ(u.clone())),
        Level::max(u.clone(), v.clone()),
        Level::imax(u.clone(), Level::succ(v.clone())),
        Level::max(Level::succ(Level::zero()), Level::imax(v, u)),
    ]
}

fn exprs() -> Vec<Expr> {
    let nat = Expr::Const(Name::str("Nat"), vec![]);
    let f = Expr::Const(Name::str("f"), vec![]);
    let mut out: Vec<Expr> = levels().into_iter().map(Expr::Sort).collect();
    out.extend([
        Expr::BVar(0),
        Expr::BVar(7),
        Expr::FVar(FVarId(3)),
        nat.clone(),
        Expr::Const(Name::str("List"), vec![Level::succ(Level::zero())]),
        Expr::Lit(Literal::nat(42)),
        Expr::Lit(Literal::string("a \"quoted\" text")),
        Expr::App(Node::new(f.clone()), Node::new(Expr::Lit(Literal::nat(1)))),
        Expr::App(
            Node::new(Expr::App(Node::new(f), Node::new(Expr::BVar(0)))),
            Node::new(nat.clone()),
        ),
    ]);
    for bi in [
        BinderInfo::Default,
        BinderInfo::Implicit,
        BinderInfo::StrictImplicit,
        BinderInfo::InstImplicit,
    ] {
        out.push(Expr::Lam(
            bi,
            Name::str("x"),
            Node::new(nat.clone()),
            Node::new(Expr::BVar(0)),
        ));
        out.push(Expr::Pi(
            bi,
            Name::str("α"),
            Node::new(Expr::Sort(Level::succ(Level::zero()))),
            Node::new(Expr::Pi(
                BinderInfo::Default,
                Name::str("_"),
                Node::new(Expr::BVar(0)),
                Node::new(Expr::BVar(1)),
            )),
        ));
    }
    out.push(Expr::Let(
        Name::str("y"),
        Node::new(nat.clone()),
        Node::new(Expr::Lit(Literal::nat(5))),
        Node::new(Expr::BVar(0)),
    ));
    out.push(Expr::Proj(Name::str("Prod"), 1, Node::new(Expr::BVar(2))));
    out
}

#[test]
fn the_wrappers_print_what_the_earlier_bodies_printed() {
    for expr in exprs() {
        assert_eq!(print_expr(&expr), old_print_expr(&expr));
        assert_eq!(print_expr_ascii(&expr), old_print_expr_ascii(&expr));
        for config in [
            PrintConfig::default(),
            PrintConfig::verbose(),
            PrintConfig::ascii(),
        ] {
            assert_eq!(
                print_expr_with_config(&expr, config.clone()),
                old_print_expr_with_config(&expr, config)
            );
        }
    }
    for level in levels() {
        assert_eq!(print_level(&level), old_print_level(&level));
    }
}