-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtimecube.sml
41 lines (35 loc) · 1.08 KB
/
timecube.sml
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
structure Timecube =
struct
open Kompiler
val f = Card Card.Put
val t = Card Card.K
val s = Card Card.S
val sc = Card Card.Succ
val i = Card Card.I
fun comp x y = Apply(Apply(s, Apply(t, x)), y)
(* \x -> x + {1,2} respectively *)
val a = Apply (s, Apply(t, sc))
val b = Apply (s, Apply(t, comp sc sc))
val basefour =
Lambda("x",
Apply((* x f i *)
Apply(Apply(Var "x",f),i),
(* x (t a) b i *)
Apply(Apply(Apply(Var "x",Apply(t,a)),b),i)
)
)
fun four v = Apply(basefour,Var v)
(* fun four v = Apply(Apply(Card Card.Get, Card Card.Zero), Var v) *)
fun quad x = Apply(Card Card.Dbl,(Apply(Card Card.Dbl,x)))
val timecube =
Lambda("x",Lambda("y",Lambda("z",Lambda("w",
(* \xyzw -> *)
Apply(four "x",
quad(Apply(four "y",
quad(Apply(four "z",
quad(Apply(four "w", Card Card.Zero))
))
))
)
))))
end