; 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