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

use crate::syntax::surf::{parse_expr_err_printed, parse_str_err_printed};

macro_rules! success {
    ($str:literal) => {
        parse_str_err_printed($str)
            .map(|ast| println!("{:?}", ast))
            .unwrap();
    };
}

macro_rules! success_expr {
    ($str:literal) => {
        parse_expr_err_printed($str)
            .map(|ast| println!("{:?}", ast))
            .unwrap();
    };
}

#[test]
fn definition_parse() {
    success!("");
    success!("definition test : Type;");
    success!("definition test : a b;");
    success!("definition test : a $ b c;");
}

#[test]
fn data_parse() {
    success!("data empty {};");
    success!("data unit { constructor tt; };");
    success!("data test tele {};");
    success!("data test tele { constructor tt tele; };");
    success!("data test (x : tele) { constructor tt (y : x); };");
}

#[test]
fn codata_parse() {
    success!("codata unit {};");
    success!("codata unit2 { projection tt : unit; };");
    success!("codata test tele {};");
    success!("codata test tele { projection tt : tele; };");
    success!("codata test (x : tele) { projection tt : (y : x) -> y; };");
}

#[test]
fn expr_parse() {
    success_expr!("Type");
    success_expr!("a b");
    success_expr!("a $ b c");
}

#[test]
fn clause_parse() {
    success!("");
    success!("clause test = Type;");
    success!("clause test .a = a;");
    success!("clause test a = a;");
    success!("clause test (a b) = b;");
    success!("clause test |_a b_| = b;");
    success!("clause test |_a b_| c = b;");
    success!("clause test |_a b_| (c d) = b;");
    success!("clause test |_a b_| .c = b;");
    success!("clause test |_a b_| .c (c d) = b;");
    success!("clause test .e |_a b_| .c (c d) = b;");
}