aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--bruijn.cabal2
-rw-r--r--std/Logic.bruijn104
-rw-r--r--std/Logic/Binary.bruijn102
-rw-r--r--std/Logic/Ternary.bruijn62
4 files changed, 169 insertions, 101 deletions
diff --git a/bruijn.cabal b/bruijn.cabal
index 7b92d04..e2909c1 100644
--- a/bruijn.cabal
+++ b/bruijn.cabal
@@ -35,6 +35,8 @@ data-files:
std/String.bruijn
std/test_all.sh
std/AIT/Beavers.bruijn
+ std/Logic/Binary.bruijn
+ std/Logic/Ternary.bruijn
std/Number/Binary.bruijn
std/Number/Bruijn.bruijn
std/Number/Conversion.bruijn
diff --git a/std/Logic.bruijn b/std/Logic.bruijn
index b16595c..171b52b 100644
--- a/std/Logic.bruijn
+++ b/std/Logic.bruijn
@@ -1,102 +1,4 @@
-# MIT License, Copyright (c) 2022 Marvin Borner
+# MIT License, Copyright (c) 2024 Marvin Borner
+# this is just a reference to the boolean implementation
-:import std/Combinator .
-
-# true
-true k ⧗ Boolean
-
-# false
-false ki ⧗ Boolean
-
-# inverts boolean value
-# equivalent of [0 ⇒ false]
-not! c ⧗ Boolean → Boolean
-
-¬‣ not!
-
-:test (¬true) (false)
-:test (¬false) (true)
-
-# true if both args are true
-and? [[0 1 0]] ⧗ Boolean → Boolean → Boolean
-
-…⋀?… and?
-
-:test (true ⋀? true) (true)
-:test (true ⋀? false) (false)
-:test (false ⋀? true) (false)
-:test (false ⋀? false) (false)
-
-# true if not both args are true
-nand? [[1 0 1 false true]] ⧗ Boolean → Boolean → Boolean
-
-:test (nand? true true) (false)
-:test (nand? true false) (true)
-:test (nand? false true) (true)
-:test (nand? false false) (true)
-
-# true if one of the args is true
-or? m ⧗ Boolean → Boolean → Boolean
-
-…⋁?… or?
-
-:test (true ⋁? true) (true)
-:test (true ⋁? false) (true)
-:test (false ⋁? true) (true)
-:test (false ⋁? false) (false)
-
-# true if both args are false
-nor? [[1 1 0 false true]] ⧗ Boolean → Boolean → Boolean
-
-:test (nor? true true) (false)
-:test (nor? true false) (false)
-:test (nor? false true) (false)
-:test (nor? false false) (true)
-
-# true if args are not same bools
-xor? [[0 (1 false 0) 1]] ⧗ Boolean → Boolean → Boolean
-
-:test (xor? true true) (false)
-:test (xor? true false) (true)
-:test (xor? false true) (true)
-:test (xor? false false) (false)
-
-# true if both args are same bools
-xnor? [[0 1 (1 0 true)]] ⧗ Boolean → Boolean → Boolean
-
-:test (xnor? true true) (true)
-:test (xnor? true false) (false)
-:test (xnor? false true) (false)
-:test (xnor? false false) (true)
-
-# if first arg is true, exec first exp; else second exp
-# this function is generally redundant
-# I personally just write (exp? case-T case-F) directly
-if [[[2 1 0]]] ⧗ Boolean → a → b → c
-
-…?…:… if
-
-:test (if true true false) (true)
-:test (true ? true : false) (true)
-:test (if false true false) (false)
-:test (false ? true : false) (false)
-
-# mathematical implies definition
-implies [[1 0 true]] ⧗ Boolean → Boolean → Boolean
-
-…⇒?… implies
-
-:test (true ⇒? true) (true)
-:test (true ⇒? false) (false)
-:test (false ⇒? true) (true)
-:test (false ⇒? false) (true)
-
-# mathematical iff (if and only if) definition
-iff xnor? ⧗ Boolean → Boolean → Boolean
-
-…⇔?… iff
-
-:test (true ⇔? true) (true)
-:test (true ⇔? false) (false)
-:test (false ⇔? true) (false)
-:test (false ⇔? false) (true)
+:input std/Logic/Binary .
diff --git a/std/Logic/Binary.bruijn b/std/Logic/Binary.bruijn
new file mode 100644
index 0000000..b16595c
--- /dev/null
+++ b/std/Logic/Binary.bruijn
@@ -0,0 +1,102 @@
+# MIT License, Copyright (c) 2022 Marvin Borner
+
+:import std/Combinator .
+
+# true
+true k ⧗ Boolean
+
+# false
+false ki ⧗ Boolean
+
+# inverts boolean value
+# equivalent of [0 ⇒ false]
+not! c ⧗ Boolean → Boolean
+
+¬‣ not!
+
+:test (¬true) (false)
+:test (¬false) (true)
+
+# true if both args are true
+and? [[0 1 0]] ⧗ Boolean → Boolean → Boolean
+
+…⋀?… and?
+
+:test (true ⋀? true) (true)
+:test (true ⋀? false) (false)
+:test (false ⋀? true) (false)
+:test (false ⋀? false) (false)
+
+# true if not both args are true
+nand? [[1 0 1 false true]] ⧗ Boolean → Boolean → Boolean
+
+:test (nand? true true) (false)
+:test (nand? true false) (true)
+:test (nand? false true) (true)
+:test (nand? false false) (true)
+
+# true if one of the args is true
+or? m ⧗ Boolean → Boolean → Boolean
+
+…⋁?… or?
+
+:test (true ⋁? true) (true)
+:test (true ⋁? false) (true)
+:test (false ⋁? true) (true)
+:test (false ⋁? false) (false)
+
+# true if both args are false
+nor? [[1 1 0 false true]] ⧗ Boolean → Boolean → Boolean
+
+:test (nor? true true) (false)
+:test (nor? true false) (false)
+:test (nor? false true) (false)
+:test (nor? false false) (true)
+
+# true if args are not same bools
+xor? [[0 (1 false 0) 1]] ⧗ Boolean → Boolean → Boolean
+
+:test (xor? true true) (false)
+:test (xor? true false) (true)
+:test (xor? false true) (true)
+:test (xor? false false) (false)
+
+# true if both args are same bools
+xnor? [[0 1 (1 0 true)]] ⧗ Boolean → Boolean → Boolean
+
+:test (xnor? true true) (true)
+:test (xnor? true false) (false)
+:test (xnor? false true) (false)
+:test (xnor? false false) (true)
+
+# if first arg is true, exec first exp; else second exp
+# this function is generally redundant
+# I personally just write (exp? case-T case-F) directly
+if [[[2 1 0]]] ⧗ Boolean → a → b → c
+
+…?…:… if
+
+:test (if true true false) (true)
+:test (true ? true : false) (true)
+:test (if false true false) (false)
+:test (false ? true : false) (false)
+
+# mathematical implies definition
+implies [[1 0 true]] ⧗ Boolean → Boolean → Boolean
+
+…⇒?… implies
+
+:test (true ⇒? true) (true)
+:test (true ⇒? false) (false)
+:test (false ⇒? true) (true)
+:test (false ⇒? false) (true)
+
+# mathematical iff (if and only if) definition
+iff xnor? ⧗ Boolean → Boolean → Boolean
+
+…⇔?… iff
+
+:test (true ⇔? true) (true)
+:test (true ⇔? false) (false)
+:test (false ⇔? true) (false)
+:test (false ⇔? false) (true)
diff --git a/std/Logic/Ternary.bruijn b/std/Logic/Ternary.bruijn
new file mode 100644
index 0000000..71fb5ac
--- /dev/null
+++ b/std/Logic/Ternary.bruijn
@@ -0,0 +1,62 @@
+# MIT License, Copyright (c) 2023 Marvin Borner
+
+# true
+true [[[0]]]
+
+# maybe (true-ish)
+maybe [[[1]]]
+
+# false
+false [[[2]]]
+
+# inverts trit value
+¬‣ [0 true maybe false] ⧗ Trit → Trit
+
+:test (¬true) (false)
+:test (¬maybe) (maybe)
+:test (¬false) (true)
+
+# true if both args are true-ish
+and? [[1 (0 1 1 1) (0 0 0 1) (0 0 0 0)]] ⧗ Trit → Trit → Trit
+
+…⋀?… and?
+
+:test (true ⋀? true) (true)
+:test (true ⋀? maybe) (maybe)
+:test (true ⋀? false) (false)
+:test (maybe ⋀? true) (maybe)
+:test (maybe ⋀? maybe) (maybe)
+:test (maybe ⋀? false) (false)
+:test (false ⋀? true) (false)
+:test (false ⋀? maybe) (false)
+:test (false ⋀? false) (false)
+
+# true if one of the args is true-ish
+or? [[1 (0 0 0 0) (0 1 0 0) (0 1 1 1)]] ⧗ Trit → Trit → Trit
+
+…⋁?… or?
+
+:test (true ⋁? true) (true)
+:test (true ⋁? maybe) (true)
+:test (true ⋁? false) (true)
+:test (maybe ⋁? true) (true)
+:test (maybe ⋁? maybe) (maybe)
+:test (maybe ⋁? false) (maybe)
+:test (false ⋁? true) (true)
+:test (false ⋁? maybe) (maybe)
+:test (false ⋁? false) (false)
+
+# mathematical iff (if and only if) definition
+iff [[1 (0 true 0 1) (0 1 1 1) (0 0 0 0)]] ⧗ Trit → Trit → Trit
+
+…⇔?… iff
+
+:test (true ⇔? true) (true)
+:test (true ⇔? maybe) (maybe)
+:test (true ⇔? false) (false)
+:test (maybe ⇔? true) (maybe)
+:test (maybe ⇔? maybe) (maybe)
+:test (maybe ⇔? false) (maybe)
+:test (false ⇔? true) (false)
+:test (false ⇔? maybe) (maybe)
+:test (false ⇔? false) (true)