From e8456ff880c5aa72171183e0b0043ca731a086fa Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Thu, 23 Feb 2023 14:25:27 +0100
Subject: Additions to standard library

Mainly new binary encoding and corresponding functions
---
 std/Unary.bruijn | 57 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)
 create mode 100644 std/Unary.bruijn

(limited to 'std/Unary.bruijn')

diff --git a/std/Unary.bruijn b/std/Unary.bruijn
new file mode 100644
index 0000000..cf72e3b
--- /dev/null
+++ b/std/Unary.bruijn
@@ -0,0 +1,57 @@
+# MIT License, Copyright (c) 2022 Marvin Borner
+# classic Church style numerals
+
+:import std/Logic .
+
+zero [[0]]
+
+# returns true if a unary number is zero
+zero? [0 [[[0]]] [[1]]] ⧗ Unary → Boolean
+
+=?‣ zero?
+
+:test (=?(+0u)) (true)
+:test (=?(+42u)) (false)
+
+# adds 1 to a unary number
+inc [[[1 (2 1 0)]]] ⧗ Unary → Unary
+
+++‣ inc
+
+:test (++(+0u)) ((+1u))
+:test (++(+1u)) ((+2u))
+:test (++(+42u)) ((+43u))
+
+# subs 1 from a unary number
+dec [[[2 [[0 (1 3)]] [1] [0]]]] ⧗ Unary → Unary
+
+--‣ dec
+
+:test (--(+0u)) ((+0u))
+:test (--(+1u)) ((+0u))
+:test (--(+42u)) ((+41u))
+
+# adds two unary numbers
+add [[[[3 1 (2 1 0)]]]] ⧗ Unary → Unary → Unary
+
+…+… add
+
+:test ((+0u) + (+2u)) ((+2u))
+:test ((+5u) + (+3u)) ((+8u))
+
+# muls two unary numbers
+mul [[[2 (1 0)]]] ⧗ Unary → Unary → Unary
+
+…⋅… mul
+
+:test ((+0u) ⋅ (+2u)) ((+0u))
+:test ((+2u) ⋅ (+3u)) ((+6u))
+
+# exponentiates two unary numbers
+# gives 1 if exponent is 0
+exp [[0 1]] ⧗ Unary → Unary → Unary
+
+…^… exp
+
+:test ((+1u) ^ (+0u)) ((+1u))
+:test ((+2u) ^ (+3u)) ((+8u))
-- 
cgit v1.2.3