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
use examples::{name,ref_edit,list_nat};
//
// Fungi module: Edit linked lists with names, holding natural numbers
//
fgi_mod!{
use name::*;
use ref_edit::*;
use 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}
}
}
}