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
//
// Fungi module: Edit linked lists with names, holding natural numbers
//
fgi_mod!{
open crate::examples::name;
open crate::examples::ref_edit;
open crate::examples::list_nat;
/// Insert a Cons cell into a list, at the given Ref cell.
//
// XXX: Technically, this operation is only permitted by the editor:
fn insert:(
Thk[0]
foralli (X1,X2,Y1,Y2):NmSet.
0 Nm[X1] ->
0 Nat ->
0 Ref[Y1](List[X1%X2][Y2]) ->
{Y1; Y1} // <-- XXX/TODO: An editor-level operation only
F Unit
) = {
#n.#h.#r.
let l1 = {get r}
let l2 = {{force cons_ref} [?][?][?][?] n h l1}
{force ref_update} r l2
}
/// Remove the Cons cell within a Ref cell. Return true if this
/// Cons cell was removed, and false otherwise, if the Ref cell
/// holds an empty list.
//
// XXX: Technically, this operation is only permitted by the editor:
fn remove:(
Thk[0]
foralli (X1,X2,Y1,Y2):NmSet.
0 Ref[Y1](List[X1%X2][Y2]) ->
{Y1; Y1} // <-- XXX/TODO: An editor-level operation only
F Bool
) = {
#r.
let l1 = {get r}
unroll match l1 {
_u => { ret false }
c => {
unpack (X1,X2,Y1,Y2) c = c
let (n, h, t) = { ret c }
let l2 = {get t}
let _u = {{force ref_update} r l2}
ret true
}
}
}
/// Insert a Cons cell after a given name in a given list.
/// Return true if successful, and false otherwise.
fn insert_after:(
Thk[0]
foralli (X):NmSet.
0 Nm[X1] ->
0 Nm[X2] ->
0 Nat ->
0 List[X2%X3][Y] ->
{Y;Y} // <-- XXX/TODO: An editor-level operation only
F Bool
) = {
#n1.#n2.#h.#l.
unroll match l {
_u => { ret false }
c => {
unpack (X1,X2,Y1,Y2) c = c
let (n, _ch, t) = { ret c }
if {{force name_eq} n n1 } {
let _u = {{force insert}[?][?][?][?] n2 h t}
ret true
} else {
{force insert_after}[?] n1 n2 h {!t}
}
}
}
}
/// Remove the Cons cell after a given name in a given list.
/// Return true if successful, and false otherwise.
fn remove_after:(
Thk[0]
foralli (X):NmSet.
0 Nm[X1] ->
0 List[X2%X3][Y] ->
{Y;Y} // <-- XXX/TODO: An editor-level operation only
F Bool
) = {
#n1.#l.
unroll match l {
_u => { ret false }
c => {
unpack (X1,X2,Y1,Y2) c = c
let (n, h, t) = { ret c }
if {{force name_eq} n n1 } {
{force remove}[?][?][?][?] t
} else {
{force remove_after}[?] n1 {!t}
}
}
}
}
/// Generate a list of naturals [n - 1, n - 2, ..., 0]
//
// XXX -- This type is wrong. TODO -- figure out how to
// ecode this type correctly, with existentials.
fn gen:(
Thk[0]
foralli (Y1,X1,Y2):NmSet.
0 Nat -> 0 F Ref[Y1](List[X1][Y2])
) = {
#n. if {{force nat_is_zero} n} {
ref (@0) roll inj1 ()
} else {
let nm = {{force name_of_nat} n}
let p = {{force nat_sub} n 1}
let l = {{force gen} p}
{{force ref_cons}
[X1][X1][X1][(Y1%Y2)][Y1][Y2]
nm p l}
}
}
}