; 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)