0.1HEADmaster

1 files changed, 195 insertions, 0 deletions

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