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
|
; primes -- list the primes, slowly
;
; This program outputs the prime numbers, one per line. It uses a unary
; representation and is not particular optimised, making it very slow.
; Copyright (C) 2026 Sebastian G. Kirmayer <gloria@gloria-mundi.eu>
;
; Permission to use, copy, modify, and/or distribute this software for any
; purpose with or without fee is hereby granted.
;
; THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH
; REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY
; AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT,
; INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM
; LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR
; OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR
; PERFORMANCE OF THIS SOFTWARE.
/\IO\fix:\/X((X->IO)->X->IO)->X->IO\read:IO->IO->IO->IO\write0:IO->IO\write1:IO->IO\exit:IO
#Pair[a b] \/X (a->b->X)->X
(\m:(\/a\/b a->b->Pair[a b])->IO m
/\A/\B\a:A\b:B/\X\x:A->B->X x a b
)\pair:\/a\/b a->b->Pair[a b]
#Triple[a b c] \/X (a->b->c->X)->X
(\m:(\/a\/b\/c a->b->c->Triple[a b c])->IO m
/\A/\B/\C\a:A\b:B\c:C/\X\x:A->B->C->X x a b c
)\triple:\/a\/b\/c a->b->c->Triple[a b c]
#Nat \/X (X->X)->X->X
(\m:Nat->IO m
/\X\s:X->X\z:X z
)\zero:Nat
(\m:(Nat->Nat)->IO m
\n:Nat /\X\s:X->X\z:X n X s (s z)
)\succ:Nat->Nat
(\m:(Nat->Nat)->IO m
\n:Nat n Pair[Nat Nat]
(\p:Pair[Nat Nat] p Pair[Nat Nat] \a:Nat\b:Nat pair Nat Nat (succ a) a)
(pair Nat Nat zero zero)
Nat
\a:Nat\b:Nat b
)\pred:Nat->Nat
(\m:(Nat->Nat->Pair[Nat Nat])->IO m
\n:Nat\m:Nat
n Triple[Nat Nat Nat]
(\t:Triple[Nat Nat Nat]
t Triple[Nat Nat Nat] \div:Nat \rem:Nat \irem:Nat
irem Triple[Nat Nat Nat]
(\_:Triple[Nat Nat Nat]
triple Nat Nat Nat div (succ rem) (pred irem))
(triple Nat Nat Nat (succ div) zero (pred m)))
(triple Nat Nat Nat zero zero (pred m))
Pair[Nat Nat]
\div:Nat \rem:Nat \irem:Nat pair Nat Nat div rem
)\divmod:Nat->Nat->Pair[Nat Nat]
(\m:Nat->IO m
(succ (succ zero))
)\2:Nat
(\m:Nat->IO m
(succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))))
)\10:Nat
(\m:(Nat->IO->IO)->IO m
\n:Nat n IO->IO (\_:IO->IO write1) write0
)\print_bit:Nat->IO->IO
(\m:(Nat->IO->IO)->IO m
\n:Nat n Nat->IO->IO
(\rest:Nat->IO->IO\cur:Nat\then:IO cur IO
(\_:IO divmod cur 10 IO \div:Nat\mod:Nat
divmod mod 2 IO \mod2:Nat\b1:Nat
divmod mod2 2 IO \mod4:Nat\b2:Nat
divmod mod4 2 IO \b8:Nat\b4:Nat
rest div
(print_bit b1
(print_bit b2
(print_bit b4
(print_bit b8
(write1 (write1 (write0 (write0 then)))))))))
then)
(\_:Nat\then:IO then)
n
)\print:Nat->IO->IO
(\m:(IO->IO)->IO m
\_:IO write0 (write1 (write0 (write1 (write0 (write0 (write0 (write0 _)))))))
)\newline:IO->IO
#Bool \/X X->X->X
(\m:Bool->IO m /\X \f:X \t:X f)\false:Bool
(\m:Bool->IO m /\X \f:X \t:X t)\true:Bool
(\m:(Bool->Bool->Bool)->IO m
\a:Bool\b:Bool a Bool a b
)\and:Bool->Bool->Bool
(\m:(Bool->Bool->Bool)->IO m
\a:Bool\b:Bool a Bool b a
)\or:Bool->Bool->Bool
#Maybe[a] \/X (a->X)->X->X
(\m:(\/a a->Maybe[a])->IO m
/\A\a:A /\X \j:A->X\n:X j a
)\just:\/a a->Maybe[a]
(\m:(\/a Maybe[a])->IO m
/\A /\X\j:A->X\n:X n
)\nothing:\/a Maybe[a]
(\m:(Nat->Bool)->IO m
\n:Nat
pred (pred n) Maybe[Nat]
(\r:Maybe[Nat] r Maybe[Nat]
(\d:Nat divmod n d Maybe[Nat]
\div:Nat\mod:Nat mod Maybe[Nat]
(\_:Maybe[Nat] just Nat (succ d))
(nothing Nat))
r)
(just Nat 2)
Bool (\_:Nat true) false
)\is_prime:Nat->Bool
fix Nat (\f:Nat->IO\n:Nat
(\_:IO is_prime n IO _ (print n (newline _))) (f (succ n))) 2
; print (pred 10) (newline exit)
|
