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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135

//
// Fungi module: linked lists with names, holding natural numbers
//
fgi_mod!{
    // /// Lists of natural numbers
    // type List  = (
    //     rec list. foralli (X,Y):NmSet.
    //         (+ Unit +
    //          (exists (X1,X2):NmSet | ((X1%X2)=X:NmSet).
    //           x Nm[X1] x Nat x Ref[Y](list[X2][Y])
    //          )
    //         )
    // );

    type Lev = (Nat);
    
    /// Level trees of natural numbers
    type Seq  = (
        rec seq. foralli (X,Y):NmSet.
            (+ Unit
             + (x Nm[X] x Nat)
             (exists (X1,X2,X3):NmSet | ((X1%X2%X3)=X:NmSet).
              x Nm[X1] x Lev
              x Ref[Y](seq[X2][Y])
              x Ref[Y](seq[X3][Y])
             )
            )
    );
    /// References to sequences of natural numbers
    type RefSeq = (
        foralli (X,Y):NmSet. 
            Ref[Y](Seq[X][Y])
    );
}

pub mod static_tests {
    #[test]
    pub fn typing() { fgi_listing_test!{
        open crate::examples::seq_nat;
        ret 0
    }}
}

// TODO implement this stuff somewhere else:
// ============================================

// fn seq_of_list_untyped:(
//     Thk[0] foralli (X1,X2,Y):NmSet.
//         0 Lev ->
//         0 Ref[Y](x List[X1][Y] x Tree[X2][Y]) ->
//         exists (X1a,X1b):NmSet|(X1=(X1a%X1b)):NmSet.
//     { {@!}X1a ; ({@!}X1a)%Y }
//     F (Ref[Y] (x List[X1b][Y]
//                x Tree[X2%X1a][Y%({@!}X1a)]))
// ) = {
//     #plev. #list_ltree.
//     let list = {{force get_prj1} list_ltree }
//     unroll match list {
//         _u => { ret list_ltree }ll inj2 (inj1 (n, x))
//                 }
//                 let listref_xleaf = {{force ref_pair} listref xleaf}
//                 let (list_rtree, _list_rtree) = {
//                     memor{n,@1}{
//                         {force seq_of_list}[X1b][X1a][Y]
//                             xlev listref_xleaf
//                     }
//                 }
//                 let list  = {{force ref_prj1} list_ltree }
//                 let ltree = {{force ref_prj2} list_ltree }
//                 let nbin  = { n,(@@bin) }
//                 let tree = {
//                     ref nbin roll inj2 inj2 pack
//                         (?,?,?) (nbin, xlev, ltree, rtree)
//                 }
//                 let list_tree = {{force ref_pair} list tree}                  
//                 let (_list_rtree, list_rtree) = memo{n,@2}{
//                     {force seq_of_list}[?][?][?]
//                         plev list_tree
//                 }
//                 ret list_rtree
//             } else {
//                 ret list_ltree
//             }
//         }
//     }
// }

// fn seq_of_list:(
//     Thk[0] foralli (X1,X2,Y):NmSet.
//         0 Lev ->
//         0 Ref[Y](x List[X1][Y] x Tree[X2][Y]) ->
//         exists (X1a,X1b):NmSet|(X1=(X1a%X1b)):NmSet.
//     { {@!}X1a ; ({@!}X1a)%Y }
//     F (Ref[Y] (x List[X1b][Y]
//                x Tree[X2%X1a][Y%({@!}X1a)]))
// ) = {
//     #plev. #list_ltree.
//     let list = {{force get_prj1} list_ltree }
//     unroll match list {
//         _u => { ret list_ltree }
//         c => {
//             unpack (X1a,X1b) c = c
//             let (n, x, listref) = { ret c }
//             let xlev = {lev_of_name n}
//             if {xlev <= plev} {
//                 let xleaf : Tree[X1a][{@!}X1a] = {
//                     ref n roll inj2 (inj1 (n, x))
//                 }
//                 let listref_xleaf = {{force ref_pair} listref xleaf}
//                 let- (X1b1,X1b2) list_rtree = {
//                     memor{n,@1}{
//                         {force seq_of_list}[X1b][X1a][Y]
//                             xlev listref_xleaf
//                     }
//                 }
//                 let list  = {{force ref_prj1} list_ltree }
//                 let ltree = {{force ref_prj2} list_ltree }
//                 let nbin  = { n,(@@bin) }
//                 let tree : Tree[?][?] = {
//                     ref nbin roll inj2 inj2 pack
//                         (X1a,X2,X1b1) (nbin, xlev, ltree, rtree)
//                 }
//                 let list_tree = {{force ref_pair} list tree}
//                 pack- (?,?) {
//                     memo{n,@2}
//                     {{force seq_of_list}[?][?][?]
//                      plev list_tree
//                     }
//                 }
//             } else {
//                 ret list_ltree
//             }
//         }
//     }
// }