nar 0.0.8

Narc, a dependently-typed programming language with dependent pattern matching
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

use voile_util::{
    meta::MI,
    uid::{GI, UID},
};

use crate::syntax::{
    abs::{desugar::desugar_main, *},
    pat::{Copat, Pat},
    surf::parse_str,
};

macro_rules! make_expect_decl {
    ($name:ident, $pat:ident, $ret:ty) => {
        fn $name(def: AbsDecl) -> $ret {
            if let AbsDecl::$pat(c) = def {
                c
            } else {
                panic!("Test failed")
            }
        }
    };
}

make_expect_decl!(expect_clause, Clause, AbsClause);
make_expect_decl!(expect_data, Data, AbsDataInfo);
make_expect_decl!(expect_constructor, Cons, AbsConsInfo);

fn expect_var_expr(p: Abs) -> UID {
    if let Abs::Var(_, uid) = p {
        uid
    } else {
        panic!("Test failed")
    }
}

fn expect_app_var_pat(p: AbsCopat) -> UID {
    if let Copat::App(Pat::Var(uid)) = p {
        uid
    } else {
        panic!("Test failed")
    }
}

#[test]
fn simple_data_and_constructor_desugar() {
    let code = "\
    data test {
      constructor test-cons;
    };
    ";
    let mut state = desugar_main(parse_str(code).unwrap()).unwrap();
    println!("{:#?}", state);
    assert_eq!(state.decls.len(), 2);
    assert!(state.local.is_empty());
    let cons: AbsConsInfo = expect_constructor(state.decls.remove(1));
    let data: AbsDataInfo = expect_data(state.decls.remove(0));
    assert!(data.tele.is_empty());
    assert!(cons.tele.is_empty());
    assert_eq!(cons.name.text, "test-cons");
    assert_eq!(data.name.text, "test");
    assert_eq!(data.conses, vec![GI(1)]);
    assert_eq!(cons.data_ix, GI(0));
}

#[test]
fn multiple_patterns_increases_ix() {
    let code = "\
    definition test : (a : Type) -> Type a;
    clause test a = a;
    clause test a = a;

    definition test2 : (a : Type) -> Type a;
    clause test2 a = a;
    ";
    let mut state = desugar_main(parse_str(code).unwrap()).unwrap();
    println!("{:#?}", state);
    assert!(state.local.is_empty());
    assert_eq!(state.decls.len(), 5);
    let mut c: AbsClause = expect_clause(state.decls.remove(4));
    assert_eq!(c.patterns.len(), 1);
    assert_eq!(c.definition, GI(3));
    assert_eq!(
        expect_app_var_pat(c.patterns.remove(0)),
        expect_var_expr(c.body)
    );
}

#[test]
fn simple_pattern_definition_desugar() {
    let code = "\
    definition test : (a : Type) -> Type a;
    clause test a = a;
    ";
    let mut state = desugar_main(parse_str(code).unwrap()).unwrap();
    println!("{:#?}", state);
    assert!(state.local.is_empty());
    assert_eq!(state.decls.len(), 2);
    let mut c = expect_clause(state.decls.remove(1));
    assert_eq!(c.patterns.len(), 1);
    assert_eq!(
        expect_app_var_pat(c.patterns.remove(0)),
        expect_var_expr(c.body)
    );
}

#[test]
fn simple_definition_desugar() {
    let code = "\
    definition test : Type;
    clause test = Type;
    ";
    let mut state = desugar_main(parse_str(code).unwrap()).unwrap();
    println!("{:#?}", state);
    assert!(state.local.is_empty());
    assert_eq!(state.decls.len(), 2);
    assert_eq!(state.meta_count, MI(0));
    let c = expect_clause(state.decls.remove(1));
    assert_eq!(c.definition, GI(0));
    assert!(c.patterns.is_empty());
}