voile 0.2.6

Voile, a dependently-typed row-polymorphic programming language
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

use super::{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 simple_declaration_parsing() {
    success!("val a : b;");
    parse_str_err_printed("val a : b").unwrap_err();
    parse_str_err_printed("a : b").unwrap_err();
    success!("let a = b;");
    parse_str_err_printed("a = b").unwrap_err();
}

#[test]
fn primary_expr_parsing() {
    success!("let a = Type;");
    success!("let a = Type233;");
    success!("let van = (Type233);");
    parse_str_err_printed("let darkholm = (Type233;").unwrap_err();
    // Keyword are not allowed
    parse_str_err_printed("let darkholm = or;").unwrap_err();
}

#[test]
fn pi_type_parsing() {
    success!("val mayori : monika -> (a: A) -> (c d e : CDE) -> F;");
    success!("val star : platinum * (a: A) * F;");
}

#[test]
fn standalone_expr_parsing() {
    success_expr!("Agda");
    success_expr!("Rec { n : Idris; }");
    success_expr!("Sum { n : Idris; }");
    success_expr!("Rec { n : Coq; ... = Epigram }");
    success_expr!("Sum { n : Coq; ... = Epigram }");
    success_expr!("Sum { n : HOL; m : Isabelle; ... = Epigram }");
}

#[test]
fn simple_expr_parsing() {
    success!("let reimu = marisa|>alice;");
    success!("let madoka = homura sayaka kyoko;");
    success!("let touma = \\kazusa Setsuna. Ogiso;");
    success!("let komeji = satori$koishi orin$okku;");
    success!("let scarlet = devil, mansion;");
    success!("val deep : @Dark Fantasy;");
    success!("val uw : ^^^pl se;");
}

#[test]
fn row_polymorphic_type_def_expr_parsing() {
    success!("val king : Rec {n: A;};");
    success!("val crimson : Sum {};");
    success!("val experience : Rec {};");
}