diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/cat.sysf | 19 | ||||
| -rw-r--r-- | examples/hello.sysf | 54 | ||||
| -rw-r--r-- | examples/primes.sysf | 129 | ||||
| -rw-r--r-- | examples/primes2.sysf | 195 |
4 files changed, 397 insertions, 0 deletions
diff --git a/examples/cat.sysf b/examples/cat.sysf new file mode 100644 index 0000000..84ab121 --- /dev/null +++ b/examples/cat.sysf @@ -0,0 +1,19 @@ +; cat -- echo back input +; +; This program echoes its input back to stdout until end of file is reached. + +; 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 +fix IO (\f:IO->IO \_:IO read exit (write0 (f _)) (write1 (f _))) exit diff --git a/examples/hello.sysf b/examples/hello.sysf new file mode 100644 index 0000000..7b300fb --- /dev/null +++ b/examples/hello.sysf @@ -0,0 +1,54 @@ +; hello -- friendly greeting program +; +; Print a friendly, non-customizable greeting. + +; 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 + +(\m:(IO->IO)->IO m + \r:IO write0 (write0 (write0 (write1 (write0 (write0 (write1 (write0 r))))))) +)\H:IO->IO +(\m:(IO->IO)->IO m + \r:IO write1 (write0 (write1 (write0 (write0 (write1 (write1 (write0 r))))))) +)\e:IO->IO +(\m:(IO->IO)->IO m + \r:IO write0 (write0 (write1 (write1 (write0 (write1 (write1 (write0 r))))))) +)\l:IO->IO +(\m:(IO->IO)->IO m + \r:IO write1 (write1 (write1 (write1 (write0 (write1 (write1 (write0 r))))))) +)\o:IO->IO +(\m:(IO->IO)->IO m + \r:IO write0 (write0 (write1 (write1 (write0 (write1 (write0 (write0 r))))))) +)\comma:IO->IO +(\m:(IO->IO)->IO m + \r:IO write0 (write0 (write0 (write0 (write0 (write1 (write0 (write0 r))))))) +)\space:IO->IO +(\m:(IO->IO)->IO m + \r:IO write1 (write1 (write1 (write0 (write1 (write1 (write1 (write0 r))))))) +)\w:IO->IO +(\m:(IO->IO)->IO m + \r:IO write0 (write1 (write0 (write0 (write1 (write1 (write1 (write0 r))))))) +)\r:IO->IO +(\m:(IO->IO)->IO m + \r:IO write0 (write0 (write1 (write0 (write0 (write1 (write1 (write0 r))))))) +)\d:IO->IO +(\m:(IO->IO)->IO m + \r:IO write1 (write0 (write0 (write0 (write0 (write1 (write0 (write0 r))))))) +)\excl:IO->IO +(\m:(IO->IO)->IO m + \r:IO write0 (write1 (write0 (write1 (write0 (write0 (write0 (write0 r))))))) +)\lf:IO->IO + +H (e (l (l (o (comma (space (w (o (r (l (d (excl (lf exit))))))))))))) 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) 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 |