0.1HEADmaster

1 files changed, 129 insertions, 0 deletions

diff --git a/examples/primes.sysf b/examples/primes.sysf
new file mode 100644
index 0000000..3111890
--- /dev/null
+++ b/examples/primes.sysf
@@ -0,0 +1,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)