fungi-lang 0.1.63

Fungi: A typed, functional language for programs that name their cached dependency graphs
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

#[test]
pub fn listing0_ok () { fgi_listing_expect![ [Expect::Success]

    let foo:(
        Thk[0] foralli (X,Y):NmSet.
            0 Bool ->
            0 Nm[X] ->
            0 Nm[Y] ->
        { {@!}(X%Y) ; 0 }
        F (exists (Z):NmSet | (Z=(X%Y):NmSet).
           (x Nm[Z] x Ref[{@!}(Z)] Nat))
    ) = {
        ret thunk #b. #nx. #ny.
            if (b) {
                let r = {ref nx 1}
                ret pack X (nx, r)
            } else {
                let r = {ref ny 2}
                ret pack Y (ny, r)
            }
    }
    ret 0
]}


#[test]
pub fn listing1_ok () { fgi_listing_expect![ [Expect::Success]
    let foo:(
        Thk[0] foralli (X,Y,Z):NmSet.
            0 Bool ->
            0 Nm[X] ->
            0 Nm[Y] ->
            0 Nm[Z] ->
        { {@!}(X%Y) ; 0 }
        F (exists (ZZ):NmSet | (ZZ=(X%Y):NmSet).
           (x Nm[ZZ%Z] x Ref[{@!}(ZZ)] Nat))
    ) = {
        ret thunk #b. #nx. #ny. #nz.
            if (b) {
                let r = {ref nx 1}
                ret pack X (nx, r)
            } else {
                let r = {ref ny 2}
                ret pack Y (nz, r) // <------- Note that 'nz : Nm[Z]'
            }
    }
    ret 0
]}

#[test]
pub fn listing1_err1 () { fgi_listing_expect![[Expect::Failure]

    let foo:(
        Thk[0] foralli (X,Y,Z):NmSet.
            0 Bool ->
            0 Nm[X] ->
            0 Nm[Y] ->
            0 Nm[Z] ->
        { {@!}(X%Y) ; 0 }
        F (exists (ZZ):NmSet | (ZZ=(X%Y):NmSet).
           (x Nm[ZZ] x Ref[{@!}(ZZ)] Nat))
    ) = {
        ret thunk #b. #nx. #ny. #nz.
            if (b) {
                let r = {ref nz 1} // <------ Should be 'nx'
                ret pack X (nx, r)
            } else {
                let r = {ref ny 2}
                ret pack Y (ny, r)
            }
    }
    ret 0
]}

#[test]
pub fn listing1_err2 () { fgi_listing_expect![[Expect::Failure]

    let foo:(
        Thk[0] foralli (X,Y,Z):NmSet.
            0 Bool ->
            0 Nm[X] ->
            0 Nm[Y] ->
            0 Nm[Z] ->
        { {@!}(X%Y) ; 0 }
        F (exists (ZZ):NmSet | (ZZ=(X%Y):NmSet).
           (x Nm[ZZ] x Ref[{@!}(ZZ)] Nat))
    ) = {
        ret thunk #b. #nx. #ny. #nz.
            if (b) {
                let r = {ref nx 1}
                ret pack X (nx, r)
            } else {
                let r = {ref ny 2}
                ret pack X (ny, r) // <--- Should be 'pack Y ...'
            }
    }
    ret 0
]}