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
|
; primes2 -- list the primes, slightly faster
;
; This program outputs the prime numbers, one per line. It uses a binary
; representation, so it is a bit faster than primes.
; 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]
#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:(\/a\/b (a->b)->Maybe[a]->Maybe[b])->IO m
/\A/\B \f:A->B \x:Maybe[A] x Maybe[B] (\a:A just B (f a)) (nothing B)
)\map_maybe:\/a\/b (a->b)->Maybe[a]->Maybe[b]
#List[a] \/X (a->X->X)->X->X
(\m:(\/a List[a])->IO m
/\A /\X \c:A->X->X \n:X n
)\nil:\/a List[a]
(\m:(\/a a->List[a]->List[a])->IO m
/\A \hd:A \tl:List[A] /\X \c:A->X->X \n:X c hd (tl X c n)
)\cons:\/a a->List[a]->List[a]
(\m:(\/a List[a]->Maybe[Pair[a List[a]]])->IO m
/\A \l:List[A] l Maybe[Pair[A List[A]]]
(\hd:A\r:Maybe[Pair[A List[A]]] just Pair[A List[A]] (pair A List[A] hd
(r List[A]
(\p:Pair[A List[A]] p List[A] (\h:A\t:List[A] cons A h t))
(nil A))))
(nothing Pair[A List[A]])
)\uncons:\/a List[a]->Maybe[Pair[a List[a]]]
#Nat List[Bool]
(\m:Nat->IO m
(nil Bool)
)\zero:Nat
(\m:(Nat->Nat)->IO m
\n:Nat
n Pair[Nat Nat]
(\bit:Bool\r:Pair[Nat Nat] r Pair[Nat Nat] \x:Nat\y:Nat
pair Nat Nat
(cons Bool bit x)
(bit Nat (cons Bool true x) (cons Bool false y)))
(pair Nat Nat zero (cons Bool true zero))
Nat \x:Nat\y:Nat y
)\succ:Nat->Nat
(\m:(Nat->Maybe[Nat])->IO m
\n:Nat
n Pair[Nat Maybe[Nat]]
(\bit:Bool\r:Pair[Nat Maybe[Nat]] r Pair[Nat Maybe[Nat]]
\x:Nat\y:Maybe[Nat]
pair Nat Maybe[Nat]
(cons Bool bit x)
(bit Maybe[Nat]
(map_maybe Nat Nat (cons Bool true) y)
(just Nat (cons Bool false x))))
(pair Nat Maybe[Nat] zero (nothing Nat))
Maybe[Nat] \x:Nat\y:Maybe[Nat] y
)\pred:Nat->Maybe[Nat]
(\m:(Nat->Nat)->IO m
\n:Nat pred n Nat (\x:Nat x) zero
)\pred_:Nat->Nat
(\m:(Nat->Pair[Bool Nat])->IO m
\n:Nat
uncons Bool n Pair[Bool Nat]
(\p:Pair[Bool Nat] p)
(pair Bool Nat false zero)
)\divmod2:Nat->Pair[Bool Nat]
(\m:(Nat->Bool)->IO m
\n:Nat n Bool (\b:Bool\r:Bool b Bool r false) true
)\is_zero:Nat->Bool
(\m:(Nat->Nat->Nat)->IO m
\n:Nat
n Nat->Nat
(\bit:Bool\r:Nat->Nat\m:Nat
divmod2 (bit Nat m (succ m)) Nat
\x:Bool\y:Nat cons Bool x (r y))
(\m:Nat m)
)\add:Nat->Nat->Nat
(\m:(Nat->Nat->Maybe[Nat])->IO m
\n:Nat\m:Nat
m Nat->Maybe[Nat]
(\bit:Bool\r:Nat->Maybe[Nat]\n:Nat
bit Maybe[Nat] (just Nat n) (pred n) Maybe[Nat]
(\n:Nat divmod2 n Maybe[Nat]
\x:Bool\y:Nat map_maybe Nat Nat (cons Bool x) (r y))
(nothing Nat))
(\n:Nat just Nat n)
n
)\sub:Nat->Nat->Maybe[Nat]
(\m:(Nat->Nat->Pair[Bool Nat])->IO m
\n:Nat\m:Nat
sub n m Pair[Bool Nat]
(\x:Nat pair Bool Nat true x)
(pair Bool Nat false n)
)\try_sub:Nat->Nat->Pair[Bool Nat]
; NOTE: Division by m+1
(\m:(Nat->Nat->Pair[Nat Nat])->IO m
\n:Nat\m:Nat
n Pair[Nat Nat]
(\bit:Bool\p:Pair[Nat Nat] p Pair[Nat Nat] \div:Nat\mod:Nat
try_sub (cons Bool bit mod) (succ m) Pair[Nat Nat]
\bit2:Bool\mod2:Nat pair Nat Nat (cons Bool bit2 div) mod2)
(pair Nat Nat zero zero)
)\divmod:Nat->Nat->Pair[Nat Nat]
(\m:Nat->IO m
(cons Bool true (cons Bool false (cons Bool false (cons Bool true zero))))
)\9:Nat
(\m:Nat->IO m
(cons Bool false (cons Bool true zero))
)\2:Nat
(\m:(Bool->IO->IO)->IO m
\b:Bool b IO->IO write0 write1
)\write_bit:Bool->IO->IO
(\m:(Nat->IO->IO)->IO m
\n:Nat n Nat->IO->IO
(\_:Bool\rest:Nat->IO->IO\cur:Nat\then:IO
is_zero cur IO (
divmod cur 9 IO \div:Nat\mod1:Nat
divmod2 mod1 IO \b1:Bool\mod2:Nat
divmod2 mod2 IO \b2:Bool\mod4:Nat
divmod2 mod4 IO \b4:Bool\mod8:Nat
divmod2 mod8 IO \b8:Bool\_:Nat
rest div
(write_bit b1
(write_bit b2
(write_bit b4
(write_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
(\m:(\/X Nat->(X->X)->X->X)->IO m
/\X \n:Nat n (X->X)->X->X
(\bit:Bool\rest:(X->X)->X->X\f:X->X\x:X
rest (\x:X f (f x)) (bit X x (f x)))
(\f:X->X\x:X x)
)\loop:\/X Nat->(X->X)->X->X
(\m:(Nat->Bool)->IO m
\n:Nat
loop Maybe[Nat] (pred_ (pred_ n))
(\v:Maybe[Nat] v Maybe[Nat]
(\m:Nat divmod n m Maybe[Nat] \div:Nat\mod:Nat
is_zero mod Maybe[Nat] (just Nat (succ m)) (nothing Nat))
v)
(just Nat (succ zero))
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
|
