diff options
Diffstat (limited to 'examples/primes2.sysf')
| -rw-r--r-- | examples/primes2.sysf | 195 |
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 |