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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
// Converts Term to Nets, and back.
use super::*;
// Converts a term to an Interaction Combinator net. Both systems are directly isomorphic, so,
// each node of the Interaction Calculus correspond to a single Interaction Combinator node.
pub fn to_net(term : &Term) -> INet {
fn encode_term
( net : &mut INet
, term : &Term
, up : Port
, scope : &mut HashMap<Vec<u8>,u32>
, vars : &mut Vec<(Vec<u8>,u32)>
) -> Port {
match term {
// A lambda becomes to a con node. Ports:
// - 0: points to where the lambda occurs.
// - 1: points to the lambda variable.
// - 2: points to the lambda body.
//&Lam{ref nam, ref typ, ref bod} => {
//// TODO: handle typ
//let fun = new_node(net, CON);
//scope.insert(nam.to_vec(), port(fun, 1));
//// Also, if the variable is unused, crease an erase node.
//if nam == b"*" {
//let era = new_node(net, ERA);
//link(net, port(era, 1), port(era, 2));
//link(net, port(fun, 1), port(era, 0));
//}
//let bod = encode_term(net, bod, port(fun, 2), scope, vars);
//link(net, port(fun, 2), bod);
//port(fun, 0)
//},
&Lam { ref nam, ref typ, ref bod } => {
let fun = new_node(net, CON);
if let Some(ref typ) = typ {
let ann = new_node(net, ANN);
let typ = encode_term(net, typ, port(ann, 0), scope, vars);
link(net, port(ann, 0), typ);
link(net, port(fun, 1), port(ann, 1));
scope.insert(nam.to_vec(), port(ann, 2));
} else {
scope.insert(nam.to_vec(), port(fun, 1));
}
if nam == b"*" {
let era = new_node(net, ERA);
link(net, port(era, 1), port(era, 2));
link(net, port(fun, 1), port(era, 0));
}
let bod = encode_term(net, bod, port(fun, 2), scope, vars);
link(net, port(fun, 2), bod);
port(fun, 0)
},
// An application becomes to a con node too. Ports:
// - 0: points to the function being applied.
// - 1: points to the function's argument.
// - 2: points to where the application occurs.
&App{ref fun, ref arg} => {
let app = new_node(net, CON);
let fun = encode_term(net, fun, port(app, 0), scope, vars);
link(net, port(app, 0), fun);
let arg = encode_term(net, arg, port(app, 1), scope, vars);
link(net, port(app, 1), arg);
port(app, 2)
},
// An annotation becomes an ANN node. Ports:
// - 0: points to the type of the annotation.
// - 1: points to where the annotation occurs.
// - 2: points to the value being annotated.
&Ann{ref val, ref typ} => {
let ann = new_node(net, ANN);
let val = encode_term(net, val, port(ann, 2), scope, vars);
link(net, port(ann, 2), val);
let typ = encode_term(net, typ, port(ann, 0), scope, vars);
link(net, port(ann, 0), typ);
port(ann, 1)
},
// A pair becomes a dup node. Ports:
// - 0: points to where the pair occurs.
// - 1: points to the first value.
// - 2: points to the second value.
&Sup{tag, ref fst, ref snd} => {
let dup = new_node(net, DUP + tag);
let fst = encode_term(net, fst, port(dup, 1), scope, vars);
link(net, port(dup, 1), fst);
let snd = encode_term(net, snd, port(dup, 2), scope, vars);
link(net, port(dup, 2), snd);
port(dup, 0)
},
// A dup becomes a dup node too. Ports:
// - 0: points to the value projected.
// - 1: points to the occurrence of the first variable.
// - 2: points to the occurrence of the second variable.
&Dup{tag, ref fst, ref snd, ref val, ref nxt} => {
let dup = new_node(net, DUP + tag);
scope.insert(fst.to_vec(), port(dup, 1));
scope.insert(snd.to_vec(), port(dup, 2));
// If the first variable is unused, create an erase node.
if fst == b"*" {
let era = new_node(net, ERA);
link(net, port(era, 1), port(era, 2));
link(net, port(dup, 1), port(era, 0));
}
// If the second variable is unused, create an erase node.
if snd == b"*" {
let era = new_node(net, ERA);
link(net, port(era, 1), port(era, 2));
link(net, port(dup, 2), port(era, 0));
}
let val = encode_term(net, &val, port(dup, 0), scope, vars);
link(net, val, port(dup, 0));
encode_term(net, &nxt, up, scope, vars)
},
// A set is just an erase node stored in a place.
&Set => {
let set = new_node(net, ERA);
link(net, port(set, 1), port(set, 2));
port(set, 0)
},
Var{ref nam} => {
vars.push((nam.to_vec(), up));
up
}
}
}
let mut net = new_inet();
let mut vars = Vec::new();
let mut scope = HashMap::new();
// Encodes the main term.
let main = encode_term(&mut net, &term, ROOT, &mut scope, &mut vars);
// Links bound variables.
for i in 0..vars.len() {
let (ref nam, var) = vars[i];
match scope.get(nam) {
Some(next) => {
let next = *next;
if enter(&net, next) == next {
link(&mut net, var, next);
} else {
panic!("Variable used more than once: {}.", std::str::from_utf8(nam).unwrap());
}
},
None => panic!("Unbound variable: {}.", std::str::from_utf8(nam).unwrap())
}
}
// Connects unbound variables to erase nodes
for (_, addr) in scope {
if enter(&net, addr) == addr {
let era = new_node(&mut net, ERA);
link(&mut net, port(era, 1), port(era, 2));
link(&mut net, addr, port(era, 0));
}
}
// Links the term to the net's root.
link(&mut net, 1, main);
net
}
// Converts an Interaction-INet node to an Interaction Calculus term.
pub fn from_net(net : &INet) -> Term {
// Given a port, returns its name, or assigns one if it wasn't named yet.
fn name_of(net : &INet, var_port : Port, var_name : &mut HashMap<u32, Vec<u8>>) -> Vec<u8> {
// If port is linked to an erase node, return an unused variable
if kind(net, addr(enter(net, var_port))) == ERA {
return b"*".to_vec();
}
if !var_name.contains_key(&var_port) {
let nam = index_to_name(var_name.len() as u32 + 1);
var_name.insert(var_port, nam.clone());
}
var_name.get(&var_port).unwrap().to_vec()
}
// Reads a term recursively by starting at root node.
fn read_term
( net : &INet
, next : Port
, var_name : &mut HashMap<u32, Vec<u8>>
, dups_vec : &mut Vec<u32>
, dups_set : &mut HashSet<(u32)>
) -> Term {
match kind(net, addr(next)) {
// If we're visiting a set...
ERA => Set,
// If we're visiting a con node...
CON => match slot(next) {
// If we're visiting a port 0, then it is a lambda.
0 => {
let nam = name_of(net, port(addr(next), 1), var_name);
let prt = enter(net, port(addr(next), 2));
let bod = read_term(net, prt, var_name, dups_vec, dups_set);
let ann = enter(net, port(addr(next), 1));
let typ = if kind(net, addr(ann)) == ANN && slot(ann) == 1 {
let ann_addr = addr(ann);
let typ_port = enter(net, port(ann_addr, 0));
Some(Box::new(read_term(net, typ_port, var_name, dups_vec, dups_set)))
} else {
None
};
let mut lam = Lam {
nam: nam,
typ: typ,
bod: Box::new(bod),
};
lam
},
// If we're visiting a port 1, then it is a variable.
1 => {
Var{nam: name_of(net, next, var_name)}
},
// If we're visiting a port 2, then it is an application.
_ => {
let prt = enter(net, port(addr(next), 0));
let fun = read_term(net, prt, var_name, dups_vec, dups_set);
let prt = enter(net, port(addr(next), 1));
let arg = read_term(net, prt, var_name, dups_vec, dups_set);
App{fun: Box::new(fun), arg: Box::new(arg)}
}
},
// If we're visiting an ANN node...
ANN => match slot(next) {
// If we're visiting a port 0, then it is an annotation...
0 => {
todo!();
},
// If we're visiting a port 1, then it is where the annotation occurs.
1 => {
let prt = enter(net, port(addr(next), 2));
let val = read_term(net, prt, var_name, dups_vec, dups_set);
let prt = enter(net, port(addr(next), 0));
let typ = read_term(net, prt, var_name, dups_vec, dups_set);
Ann{val: Box::new(val), typ: Box::new(typ)}
},
// If we're visiting a port 2, then it is the value being annotated.
_ => {
let prt = enter(net, port(addr(next), 1));
let val = read_term(net, prt, var_name, dups_vec, dups_set);
val
//let prt = enter(net, port(addr(next), 0));
//let typ = read_term(net, prt, var_name, dups_vec, dups_set);
//Ann{val: Box::new(val), typ: Box::new(typ)}
}
},
// If we're visiting a fan node...
tag => match slot(next) {
// If we're visiting a port 0, then it is a pair.
0 => {
let tag = tag - DUP;
let prt = enter(net, port(addr(next), 1));
let fst = read_term(net, prt, var_name, dups_vec, dups_set);
let prt = enter(net, port(addr(next), 2));
let snd = read_term(net, prt, var_name, dups_vec, dups_set);
Sup{tag, fst: Box::new(fst), snd: Box::new(snd)}
},
// If we're visiting a port 1 or 2, then it is a variable.
// Also, that means we found a dup, so we store it to read later.
_ => {
if !dups_set.contains(&addr(next)) {
dups_set.insert(addr(next));
dups_vec.push(addr(next));
}
let nam = name_of(net, next, var_name);
Var{nam}
}
}
}
}
// A hashmap linking ports to binder names. Those ports have names:
// Port 1 of a con node (λ), ports 1 and 2 of a fan node (let).
let mut binder_name = HashMap::new();
// Dup aren't scoped. We find them when we read one of the variables
// introduced by them. Thus, we must store the dups we find to read later.
// We have a vec for .pop(). and a set to avoid storing duplicates.
let mut dups_vec = Vec::new();
let mut dups_set = HashSet::new();
// Reads the main term from the net
let mut main = read_term(net, enter(net, ROOT), &mut binder_name, &mut dups_vec, &mut dups_set);
// Reads let founds by starting the read_term function from their 0 ports.
while dups_vec.len() > 0 {
let dup = dups_vec.pop().unwrap();
let val = read_term(net, enter(net,port(dup,0)), &mut binder_name, &mut dups_vec, &mut dups_set);
let tag = kind(net, dup) - DUP;
let fst = name_of(net, port(dup,1), &mut binder_name);
let snd = name_of(net, port(dup,2), &mut binder_name);
let val = Box::new(val);
let nxt = Box::new(main);
main = Dup{tag, fst, snd, val, nxt};
}
main
}