lsts 0.6.34

Large Scale Type Systems
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

use lsts::tlc::TLC;

#[test]
fn l1_literals() {
   let mut tlc = TLC::new();
   let l1 = tlc.import_file(None, "preludes/l1.tlc").unwrap();

   tlc.check(Some(l1), "0: I64;").unwrap();
   tlc.check(Some(l1), "0: I64;").unwrap();
   tlc.check(Some(l1), "1: I64;").unwrap();
   tlc.check(Some(l1), "1: I64;").unwrap();
   tlc.check(Some(l1), "-1: I64;").unwrap();
   tlc.check(Some(l1), "-1: U64;").unwrap_err();
}

#[test]
fn l1_functions() {
   let mut tlc = TLC::new();
   let l1 = tlc.import_file(None, "preludes/l1.tlc").unwrap();

   tlc.check(Some(l1), "let f(x:I64): I64 = x; f(1:I64);").unwrap();
   tlc.check(Some(l1), "let f(x:I64): I64 = x; f(1:I64);").unwrap();
   tlc.check(Some(l1), "let f(x:I64): I64 = x; f(-1);").unwrap();
   tlc.check(Some(l1), "let f(x:I64): I64 = x; f(-1);").unwrap();
   tlc.check(Some(l1), "let f(x:I64): I64 = x; f(-1);").unwrap();
}

#[test]
fn l1_dot_functions() {
   let mut tlc = TLC::new();
   let l1 = tlc.import_file(None, "preludes/l1.tlc").unwrap();

   tlc.check(Some(l1), "let .f(x:I64): I64 = x; (1:I64).f: I64;").unwrap();
   tlc.check(Some(l1), "let .f(x:I64, y:I64): I64 = x; (1:I64).f(2:I64): I64;").unwrap();
   tlc.check(Some(l1), "let .f(x:I64, y:I64, z:I64): I64 = x; (1:I64).f(2:I64,3:I64): I64;").unwrap();
}

#[test]
fn l1_reduce() {
   let mut tlc = TLC::new();
   let l1 = tlc.import_file(None, "preludes/l1.tlc").unwrap();

   tlc.check(Some(l1), "- 0 @reduce;").unwrap();
   tlc.check(Some(l1), "- 1 @reduce;").unwrap();
   tlc.check(Some(l1), "-1 @reduce;").unwrap();
   tlc.check(Some(l1), "- -1 @reduce;").unwrap();
}

#[test]
fn l1_homogenous_tuples() {
   let mut tlc = TLC::new();
   let l1 = tlc.import_file(None, "preludes/l1.tlc").unwrap();

   tlc.check(Some(l1), "(): I64[0];").unwrap();
   tlc.check(Some(l1), "(1): I64[0];").unwrap_err();
   tlc.check(Some(l1), "(1): I64;").unwrap();
   tlc.check(Some(l1), "(1,): I64[0];").unwrap_err();
   tlc.check(Some(l1), "(1,): I64[1];").unwrap();
   tlc.check(Some(l1), "(1,2): I64[1];").unwrap_err();
   tlc.check(Some(l1), "(1,2): I64[];").unwrap();
   tlc.check(Some(l1), "(1,2): I64[2];").unwrap();
   tlc.check(Some(l1), "(1,2,3): I64[2];").unwrap_err();
   tlc.check(Some(l1), "(1,2,3): I64[3];").unwrap();
   tlc.check(Some(l1), "((1,2,3): I64[3]).0 @reduce :[1];").unwrap();
   tlc.check(Some(l1), "((1,2,3): I64[3]).1 @reduce :[2];").unwrap();
   tlc.check(Some(l1), "((1,2,3): I64[3]).2 @reduce :[3];").unwrap();
   tlc.check(Some(l1), "((1,2,3): I64[3])[0] @reduce :[1];").unwrap();
   tlc.check(Some(l1), "((1,2,3): I64[3])[1] @reduce :[2];").unwrap();
   tlc.check(Some(l1), "((1,2,3): I64[3])[2] @reduce :[3];").unwrap();
   tlc.check(Some(l1), "((1,2,3): I64[])[2] @reduce :[3];").unwrap();
   tlc.check(Some(l1), "().length @reduce :[0];").unwrap();
   tlc.check(Some(l1), "(3,).length @reduce :[1];").unwrap();
   tlc.check(Some(l1), "(3,4).length @reduce :[2];").unwrap();
   tlc.check(Some(l1), "(3,4,7).length @reduce :[3];").unwrap();
   tlc.check(Some(l1), "((3,4,7): I64[]).length @reduce :[3];").unwrap();
   //tlc.check(Some(l1), "((1,),(),(2,3,)).flatten() @reduce :[(1,2,3)];").unwrap();
   //tlc.check(Some(l1), "((1,),(),(2,3,)).flatten().length @reduce :[3];").unwrap();
}

/* TODO FIXME destructure tuples
#[test]
fn l1_destructure_tuples() {
   let mut tlc = TLC::new();
   let l1 = tlc.import_file(None, "preludes/l1.tlc").unwrap();

   tlc.check(Some(l1), "match () { () => 1 }  @reduce :[1];").unwrap();
   tlc.check(Some(l1), "match () { (x,) => 1 }  @reduce :[1];").unwrap_err();
   tlc.check(Some(l1), "match () { (x,y) => 1 }  @reduce :[1];").unwrap_err();
   tlc.check(Some(l1), "match (3,) { () => 1 }  @reduce :[1];").unwrap_err();
   tlc.check(Some(l1), "match (3,) { (x) => 1 }  @reduce :[1];").unwrap();
   tlc.check(Some(l1), "match (3,) { (x,y) => 1 }  @reduce :[1];").unwrap_err();
   tlc.check(Some(l1), "match (3,4) { () => 1 }  @reduce :[1];").unwrap_err();
   tlc.check(Some(l1), "match (3,4) { (x,) => 1 }  @reduce :[1];").unwrap_err();
   tlc.check(Some(l1), "match (3,4) { (x,y) => 1 }  @reduce :[1];").unwrap();
   tlc.check(Some(l1), "match (3,4) { (x,y) => x }  @reduce :[3];").unwrap();
}
*/

/* TODO FIXME update tuple LHS syntax
#[test]
fn l1_partial_tuples() {
   let mut tlc = TLC::new();
   let l1 = tlc.import_file(None, "preludes/l1.tlc").unwrap();

   tlc.check(Some(l1), "match (3,4) { +((x,),y) => x }  @reduce :[3];").unwrap();
   tlc.check(Some(l1), "match (3,4) { +(x,(y,)) => y }  @reduce :[4];").unwrap();
   tlc.check(Some(l1), "match (3,4) { +((3,),(y,)) => 5 }  @reduce :[5];").unwrap();
   tlc.check(Some(l1), "match (3,4) { +((3,),x,(y,)) => 5 }  @reduce :[5];").unwrap();
   tlc.check(Some(l1), "match (3,4) { +((3,),(y,)) => 5 }  @reduce :[5];").unwrap();
}
*/