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
//
// Fungi module: linked lists with names, holding natural numbers
//
fgi_mod!{
/// Convert a natural number into a name
//
// XXX -- This type is wrong. TODO -- figure out how to
// ecode this type correctly, with existentials.
fn name_of_nat:(
Thk[0]
foralli X:NmSet.
0 Nat -> 0 F Nm[X]
) = {
unsafe (1) trapdoor::name_of_nat
}
/// Test if two names are equal
fn name_eq:(
Thk[0]
foralli (X,Y):NmSet.
0 Nm[X] -> 0 Nm[Y] -> 0 F Bool
) = {
unsafe (2) trapdoor::name_eq
}
}
pub mod trapdoor {
// This code essentially extends the Fungi evaluator
use ast::{Name};
use dynamics::{RtVal,ExpTerm};
pub fn name_of_nat(args:Vec<RtVal>) -> ExpTerm {
match &args[0] {
RtVal::Nat(n) => {
ExpTerm::Ret(RtVal::Name(Name::Num(*n)))
}
v => panic!("expected a natural number, not: {:?}", v)
}
}
pub fn name_eq(args:Vec<RtVal>) -> ExpTerm {
match (&args[0],&args[1]) {
(RtVal::Name(n1), RtVal::Name(n2)) => {
ExpTerm::Ret(RtVal::Bool(n1 == n2))
}
(v1, v2) => panic!("expected two names, not: {:?} and {:?}", v1, v2)
}
}
}