stdlib: added (2,3,4)-valued logic ADTs

This is useful for writing caches and perhaps in typestate predicates.
It also adds a companion module for bool with from_str, to_str, ... fns.

8 files changed, 848 insertions, 2 deletions

diff --git a/src/lib/bool.rs b/src/lib/bool.rs
new file mode 100644
index 00000000000..68c798ceb23
--- /dev/null
+++ b/src/lib/bool.rs
@@ -0,0 +1,134 @@
+// -*- rust -*-
+
+/*
+Module: bool
+
+Classic Boolean logic reified as ADT
+*/
+
+export t;
+export not, and, or, xor, implies;
+export eq, ne, is_true, is_false;
+export from_str, to_str, all_values, to_bit;
+
+/*
+Type: t
+
+The type of boolean logic values
+*/
+type t = bool;
+
+/* Function: not
+
+Negation/Inverse
+*/
+pure fn not(v: t) -> t { !v }
+
+/* Function: and
+
+Conjunction
+*/
+pure fn and(a: t, b: t) -> t { a && b }
+
+/* Function: and
+
+Disjunction
+*/
+pure fn or(a: t, b: t) -> t { a || b }
+
+/*
+Function: xor
+
+Exclusive or, i.e. `or(and(a, not(b)), and(not(a), b))`
+*/
+pure fn xor(a: t, b: t) -> t { (a && !b) || (!a && b) }
+
+/*
+Function: implies
+
+Implication in the logic, i.e. from `a` follows `b`
+*/
+pure fn implies(a: t, b: t) -> t { !a || b }
+
+/*
+Predicate: eq
+
+Returns:
+
+true if truth values `a` and `b` are indistinguishable in the logic
+*/
+pure fn eq(a: t, b: t) -> bool { a == b }
+
+/*
+Predicate: ne
+
+Returns:
+
+true if truth values `a` and `b` are distinguishable in the logic
+*/
+pure fn ne(a: t, b: t) -> bool { a != b }
+
+/*
+Predicate: is_true
+
+Returns:
+
+true if `v` represents truth in the logic
+*/
+pure fn is_true(v: t) -> bool { v }
+
+/*
+Predicate: is_false
+
+Returns:
+
+true if `v` represents falsehood in the logic
+*/
+pure fn is_false(v: t) -> bool { !v }
+
+/*
+Function: from_str
+
+Parse logic value from `s`
+*/
+pure fn from_str(s: str) -> t {
+    alt s {
+      "true" { true }
+      "false" { false }
+    }
+}
+
+/*
+Function: to_str
+
+Convert `v` into a string
+*/
+pure fn to_str(v: t) -> str { if v { "true" } else { "false" } }
+
+/*
+Function: all_values
+
+Iterates over all truth values by passing them to `blk`
+in an unspecified order
+*/
+fn all_values(blk: block(v: t)) {
+    blk(true);
+    blk(false);
+}
+
+/*
+Function: to_bit
+
+Returns:
+
+An u8 whose first bit is set if `if_true(v)` holds
+*/
+fn to_bit(v: t) -> u8 { if v { 1u8 } else { 0u8 } }
+
+// Local Variables:
+// mode: rust;
+// fill-column: 78;
+// indent-tabs-mode: nil
+// c-basic-offset: 4
+// buffer-file-coding-system: utf-8-unix
+// End:
diff --git a/src/lib/four.rs b/src/lib/four.rs
new file mode 100644
index 00000000000..a1165caf864
--- /dev/null
+++ b/src/lib/four.rs
@@ -0,0 +1,229 @@
+// -*- rust -*-
+
+/*
+Module: four
+
+The fourrternary Belnap relevance logic FOUR represented as ADT
+
+This allows reasoning with four logic values (true, false, none, both)
+
+Implementation: Truth values are represented using a single u8 and
+all operations are done using bitshifting which is fast
+on current cpus.
+*/
+
+import tri;
+
+export t, none, true, false, both;
+export not, and, or, xor, implies, implies_materially;
+export eq, ne, is_true, is_false;
+export from_str, to_str, all_values, to_trit, to_bit;
+
+/*
+Type: t
+
+The type of fourrternary logic values
+
+It may be thought of as  tuple `(y, x)` of two bools
+
+*/
+type t = u8;
+
+const b0: u8  = 1u8;
+const b1: u8  = 2u8;
+const b01: u8 = 3u8;
+
+/*
+Constant: none
+
+Logic value `(0, 0)` for bottom (neither true or false)
+*/
+const none: t  = 0u8;
+
+/*
+Constant: true
+
+Logic value `(0, 1)` for truth
+*/
+const true: t  = 1u8;
+
+/*
+Constant: false
+
+Logic value `(1, 0)` for falsehood
+*/
+const false: t = 2u8;
+
+/*
+Constant: both
+
+Logic value `(1, 1)` for top (both true and false)
+*/
+const both: t  = 3u8;
+
+/* Function: not
+
+Negation/Inverse
+
+Returns:
+
+`'(v.y, v.x)`
+*/
+pure fn not(v: t) -> t { ((v << 1u8) | (v >> 1u8)) & b01 }
+
+/* Function: and
+
+Conjunction
+
+Returns:
+
+`(a.x | b.x, a.y & b.y)`
+*/
+pure fn and(a: t, b: t) -> t { ((a & b) & b0) | ((a | b) & b1) }
+
+/* Function: or
+
+Disjunction
+
+Returns:
+
+`(a.x & b.x, a.y | b.y)`
+*/
+pure fn or(a: t, b: t) -> t { ((a | b) & b0) | ((a & b) & b1) }
+
+/* Function: xor
+
+Classic exclusive or
+
+Returns:
+
+`or(and(a, not(b)), and(not(a), b))`
+*/
+pure fn xor(a: t, b: t) -> t { or(and(a, not(b)), and(not(a), b)) }
+
+/*
+Function: implies
+
+Strong implication (from `a` strongly follows `b`)
+
+Returns:
+
+`( x1 & y2, !x1 | x2)`
+*/
+pure fn implies(a: t, b: t) -> t { ((a << 1u8) & b & b1) | (((!a) | b) & b0) }
+
+/*
+Function: implies_materially
+
+Classic (material) implication in the logic
+(from `a` materially follows `b`)
+
+Returns:
+
+`or(not(a), b)`
+*/
+pure fn implies_materially(a: t, b: t) -> t { or(not(a), b) }
+
+/*
+Predicate: eq
+
+Returns:
+
+true if truth values `a` and `b` are indistinguishable in the logic
+*/
+pure fn eq(a: t, b: t) -> bool { a == b }
+
+/*
+Predicate: ne
+
+Returns:
+
+true if truth values `a` and `b` are distinguishable in the logic
+*/
+pure fn ne(a: t, b: t) -> bool { a != b }
+
+/*
+Predicate: is_true
+
+Returns:
+
+true if `v` represents truth in the logic (is `true` or `both`)
+*/
+pure fn is_true(v: t) -> bool { (v & b0) != 0u8 }
+
+/*
+Predicate: is_false
+
+Returns:
+
+true if `v` represents falsehood in the logic (is `false` or `none`)
+*/
+pure fn is_false(v: t) -> bool { (v & b0) == 0u8 }
+
+/*
+Function: from_str
+
+Parse logic value from `s`
+*/
+pure fn from_str(s: str) -> t {
+    alt s {
+      "none" { none }
+      "false" { four::false }
+      "true" { four::true }
+      "both" { both }
+    }
+}
+
+/*
+Function: to_str
+
+Convert `v` into a string
+*/
+pure fn to_str(v: t) -> str {
+    // FIXME replace with consts as soon as that works
+    alt v {
+      0u8 { "none" }
+      1u8 { "true" }
+      2u8 { "false" }
+      3u8 { "both" }
+    }
+}
+
+/*
+Function: all_values
+
+Iterates over all truth values by passing them to `blk`
+in an unspecified order
+*/
+fn all_values(blk: block(v: t)) {
+    blk(both);
+    blk(four::true);
+    blk(four::false);
+    blk(none);
+}
+
+/*
+Function: to_bit
+
+Returns:
+
+An u8 whose first bit is set if `if_true(v)` holds
+*/
+fn to_bit(v: t) -> u8 { v & b0 }
+
+/*
+Function: to_tri
+
+Returns:
+
+A trit of `v` (`both` and `none` are both coalesced into `trit::unknown`)
+*/
+fn to_trit(v: t) -> tri::t { v & (v ^ not(v)) }
+
+// Local Variables:
+// mode: rust;
+// fill-column: 78;
+// indent-tabs-mode: nil
+// c-basic-offset: 4
+// buffer-file-coding-system: utf-8-unix
+// End:
diff --git a/src/lib/std.rc b/src/lib/std.rc
index 9207f1cfdc9..87184d5e905 100644
--- a/src/lib/std.rc
+++ b/src/lib/std.rc
@@ -7,9 +7,9 @@
 #[license = "BSD"];
 
 
-export box, char, float, int, str, ptr, uint, u8, u32, u64, vec;
+export box, char, float, int, str, ptr, uint, u8, u32, u64, vec, bool;
 export comm, fs, io, net, run, sys, task;
-export ctypes, either, option, result, util;
+export ctypes, either, option, result, four, tri, util;
 export bitv, deque, fun_treemap, list, map, smallintmap, sort, treemap, ufind;
 export rope;
 export ebml, dbg, getopts, json, math, rand, sha1, term, time, unsafe;
@@ -30,6 +30,7 @@ mod uint;
 mod u8;
 mod u32;
 mod u64;
+mod bool;
 mod vec;
 
 
@@ -50,6 +51,8 @@ mod ctypes;
 mod either;
 mod option;
 mod result;
+mod four;
+mod tri;
 mod util;
 
 
diff --git a/src/lib/tri.rs b/src/lib/tri.rs
new file mode 100644
index 00000000000..27e24bb4f47
--- /dev/null
+++ b/src/lib/tri.rs
@@ -0,0 +1,188 @@
+// -*- rust -*-
+
+/*
+Module: tri
+
+ADT for the ternary Kleene logic K3
+
+This allows reasoning with three logic values (true, false, unknown)
+
+Implementation: Truth values are represented using a single u8 and
+all operations are done using bitshifting which is fast
+on current cpus.
+*/
+
+export t, true, false, unknown;
+export not, and, or, xor, implies, eq, ne, is_true, is_false;
+export from_str, to_str, all_values, to_bit;
+
+/*
+Type: t
+
+The type of ternary logic values
+*/
+type t = u8;
+
+const b0: u8  = 1u8;
+const b1: u8  = 2u8;
+const b01: u8 = 3u8;
+
+/*
+Constant: unknown
+
+Logic value for unknown (maybe true xor maybe false)
+*/
+const unknown: t = 0u8;
+
+/*
+Constant: true
+
+Logic value for truth
+*/
+const true: t = 1u8;
+
+/*
+Constant: false
+
+Logic value for falsehood
+*/
+const false: t = 2u8;
+
+/* Function: not
+
+Negation/Inverse
+*/
+pure fn not(v: t) -> t { ((v << 1u8) | (v >> 1u8)) & b01 }
+
+/* Function: and
+
+Conjunction
+*/
+pure fn and(a: t, b: t) -> t { ((a | b) & b1) | ((a & b) & b0) }
+
+/* Function: or
+
+Disjunction
+*/
+pure fn or(a: t, b: t) -> t { ((a & b) & b1) | ((a | b) & b0) }
+
+/*
+Function: xor
+
+Exclusive or
+*/
+pure fn xor(a: t, b: t) -> t {
+    let anb = a & b;
+    let aob = a & not(b);
+    ret ((anb & b1) | (anb << 1u8) | (aob >> 1u8) | (aob & b0)) & b01;
+}
+
+/*
+Function: implies
+
+Classic implication, i.e. from `a` follows `b`
+*/
+pure fn implies(a: t, b: t) -> t {
+    ret ((a & b1) >> 1u8) | (b & b0) | ((a << 1u8) & b & b1);
+}
+
+/*
+Predicate: eq
+
+Returns:
+
+true if truth values `a` and `b` are indistinguishable in the logic
+*/
+pure fn eq(a: t, b: t) -> bool {  a == b }
+
+/*
+Predicate: ne
+
+Returns:
+
+true if truth values `a` and `b` are distinguishable in the logic
+*/
+pure fn ne(a: t, b: t) -> bool { a != b }
+
+/*
+Predicate: is_true
+
+Returns:
+
+true if `v` represents truth in the logic
+*/
+pure fn is_true(v: t) -> bool { v == tri::true }
+
+/*
+Predicate: is_false
+
+Returns:
+
+true if `v` represents false in the logic
+*/
+pure fn is_false(v: t) -> bool { v == tri::false }
+
+/*
+Predicate: is_unknown
+
+Returns:
+
+true if `v` represents the unknown state in the logic
+*/
+pure fn is_unknown(v: t) -> bool { v == unknown }
+
+/*
+Function: from_str
+
+Parse logic value from `s`
+*/
+pure fn from_str(s: str) -> t {
+    alt s {
+      "unknown" { unknown }
+      "true" { tri::true }
+      "false" { tri::false }
+    }
+}
+
+/*
+Function: to_str
+
+Convert `v` into a string
+*/
+pure fn to_str(v: t) -> str {
+    // FIXME replace with consts as soon as that works
+    alt v {
+      0u8 { "unknown" }
+      1u8 { "true" }
+      2u8 { "false" }
+    }
+}
+
+/*
+Function: all_values
+
+Iterates over all truth values by passing them to `blk`
+in an unspecified order
+*/
+fn all_values(blk: block(v: t)) {
+    blk(tri::false);
+    blk(unknown);
+    blk(tri::true);
+}
+
+/*
+Function: to_bit
+
+Returns:
+
+An u8 whose first bit is set if `if_true(v)` holds
+*/
+fn to_bit(v: t) -> u8 { v & b0 }
+
+// Local Variables:
+// mode: rust;
+// fill-column: 78;
+// indent-tabs-mode: nil
+// c-basic-offset: 4
+// buffer-file-coding-system: utf-8-unix
+// End:
diff --git a/src/test/stdtest/bool.rs b/src/test/stdtest/bool.rs
new file mode 100644
index 00000000000..2f91b7aa1e1
--- /dev/null
+++ b/src/test/stdtest/bool.rs
@@ -0,0 +1,23 @@
+use std;
+
+import std::bool;
+
+#[test]
+fn test_bool_from_str() {
+    bool::all_values { |v|
+        assert v == bool::from_str(bool::to_str(v))
+    }
+}
+
+#[test]
+fn test_bool_to_str() {
+    assert bool::to_str(false) == "false";
+    assert bool::to_str(true) == "true";
+}
+
+#[test]
+fn test_bool_to_bit() {
+    bool::all_values { |v|
+        assert bool::to_bit(v) == if bool::is_true(v) { 1u8 } else { 0u8 };
+    }
+}
\ No newline at end of file
diff --git a/src/test/stdtest/four.rs b/src/test/stdtest/four.rs
new file mode 100644
index 00000000000..d0af7a393d3
--- /dev/null
+++ b/src/test/stdtest/four.rs
@@ -0,0 +1,149 @@
+use std;
+
+import std::tri;
+import std::four;
+
+fn eq1(a: four::t, b: four::t) -> bool { four::eq(a , b) }
+fn ne1(a: four::t, b: four::t) -> bool { four::ne(a , b) }
+
+fn eq2(a: four::t, b: four::t) -> bool { eq1( a, b ) && eq1( b, a ) }
+
+#[test]
+fn test_four_req_eq() {
+    four::all_values { |a|
+        four::all_values { |b|
+            assert if a == b { eq1( a, b ) } else { ne1( a, b ) };
+        }
+    }
+}
+
+#[test]
+fn test_four_and_symmetry() {
+    four::all_values { |a|
+        four::all_values { |b|
+            assert eq1( four::and(a ,b), four::and(b, a) );
+        }
+    }
+}
+
+#[test]
+fn test_four_xor_symmetry() {
+    four::all_values { |a|
+        four::all_values { |b|
+            assert eq1( four::and(a ,b), four::and(b, a) );
+        }
+    }
+}
+
+#[test]
+fn test_four_or_symmetry() {
+    four::all_values { |a|
+        four::all_values { |b|
+            assert eq1( four::or(a ,b), four::or(b, a) );
+        }
+    }
+}
+
+fn to_tup(v: four::t) -> (bool, bool) {
+    alt v {
+      0u8 { (false, false) }
+      1u8 { (false, true) }
+      2u8 { (true, false) }
+      3u8 { (true, true) }
+    }
+}
+
+#[test]
+fn test_four_not() {
+    four::all_values { |a|
+        let (x, y) = to_tup(a);
+        assert to_tup(four::not(a)) == (y, x);
+    };
+}
+
+
+#[test]
+fn test_four_and() {
+    four::all_values { |a|
+        four::all_values { |b|
+            let (y1, x1) = to_tup(a);
+            let (y2, x2) = to_tup(b);
+            let (y3, x3) = to_tup(four::and(a, b));
+
+            assert (x3, y3) == (x1 && x2, y1 || y2);
+        }
+    };
+}
+
+#[test]
+fn test_four_or() {
+    four::all_values { |a|
+        four::all_values { |b|
+            let (y1, x1) = to_tup(a);
+            let (y2, x2) = to_tup(b);
+            let (y3, x3) = to_tup(four::or(a, b));
+
+            assert (x3, y3) == (x1 || x2, y1 && y2);
+        }
+    };
+}
+
+#[test]
+fn test_four_implies() {
+    four::all_values { |a|
+        four::all_values { |b|
+            let (_, x1) = to_tup(a);
+            let (y2, x2) = to_tup(b);
+            let (y3, x3) = to_tup(four::implies(a, b));
+
+            assert (x3, y3) == (!x1 || x2, x1 && y2);
+        }
+    };
+}
+
+#[test]
+fn test_four_is_true() {
+    assert !four::is_true(four::none);
+    assert !four::is_true(four::false);
+    assert four::is_true(four::true);
+    assert four::is_true(four::both);
+}
+
+#[test]
+fn test_four_is_false() {
+    assert four::is_false(four::none);
+    assert four::is_false(four::false);
+    assert !four::is_false(four::true);
+    assert !four::is_false(four::both);
+}
+
+#[test]
+fn test_four_from_str() {
+    four::all_values { |v|
+        assert eq1( v, four::from_str(four::to_str(v)) );
+    }
+}
+
+#[test]
+fn test_four_to_str() {
+    assert four::to_str(four::none) == "none";
+    assert four::to_str(four::false) == "false";
+    assert four::to_str(four::true) == "true" ;
+    assert four::to_str(four::both) == "both";
+}
+
+#[test]
+fn test_four_to_tri() {
+    assert tri::eq( four::to_trit(four::true), tri::true );
+    assert tri::eq( four::to_trit(four::false), tri::false );
+    assert tri::eq( four::to_trit(four::none), tri::unknown );
+    log four::to_trit(four::both);
+    assert tri::eq( four::to_trit(four::both), tri::unknown );
+}
+
+#[test]
+fn test_four_to_bit() {
+    four::all_values { |v|
+        assert four::to_bit(v) == if four::is_true(v) { 1u8 } else { 0u8 };
+    }
+}
\ No newline at end of file
diff --git a/src/test/stdtest/stdtest.rc b/src/test/stdtest/stdtest.rc
index fd3722e1938..289c1221c92 100644
--- a/src/test/stdtest/stdtest.rc
+++ b/src/test/stdtest/stdtest.rc
@@ -1,12 +1,14 @@
 use std;
 
 mod bitv;
+mod bool;
 mod box;
 mod char;
 mod comm;
 mod deque;
 mod either;
 mod float;
+mod four;
 mod fs;
 mod getopts;
 mod int;
@@ -32,6 +34,7 @@ mod str;
 mod sys;
 mod task;
 mod test;
+mod tri;
 mod treemap;
 mod uint;
 mod unsafe;
diff --git a/src/test/stdtest/tri.rs b/src/test/stdtest/tri.rs
new file mode 100644
index 00000000000..4ea87c1270e
--- /dev/null
+++ b/src/test/stdtest/tri.rs
@@ -0,0 +1,117 @@
+use std;
+
+import std::tri;
+
+pure fn eq1(a: tri::t, b: tri::t) -> bool { tri::eq(a , b) }
+pure fn ne1(a: tri::t, b: tri::t) -> bool { tri::ne(a , b) }
+
+pure fn eq2(a: tri::t, b: tri::t) -> bool { eq1( a, b ) && eq1( b, a ) }
+
+#[test]
+fn test_eq2() {
+    tri::all_values { |a|
+        tri::all_values { |b|
+            assert if a == b { eq1( a, b ) } else { ne1( a, b ) }
+        }
+    }
+}
+
+#[test]
+fn test_tri_and_symmetry() {
+    tri::all_values { |a|
+        tri::all_values { |b|
+            assert eq1( tri::and(a ,b), tri::and(b, a) );
+        }
+    }
+}
+
+#[test]
+fn test_tri_or_symmetry() {
+    tri::all_values { |a|
+        tri::all_values { |b|
+            assert eq1( tri::or(a ,b), tri::or(b, a) );
+        }
+    }
+}
+
+#[test]
+fn test_tri_xor_symmetry() {
+    tri::all_values { |a|
+        tri::all_values { |b|
+            assert eq1( tri::xor(a ,b), tri::xor(b, a) );
+        }
+    }
+}
+
+#[test]
+fn test_tri_not() {
+    assert eq2( tri::not(tri::true), tri::false);
+    assert eq2( tri::not(tri::unknown), tri::unknown);
+    assert eq2( tri::not(tri::false), tri::true);
+}
+
+#[test]
+fn test_tri_and() {
+    assert eq2( tri::and(tri::true, tri::true), tri::true);
+    assert eq2( tri::and(tri::true, tri::false), tri::false);
+    assert eq2( tri::and(tri::true, tri::unknown), tri::unknown);
+    assert eq2( tri::and(tri::false, tri::false), tri::false);
+    assert eq2( tri::and(tri::false, tri::unknown), tri::false);
+    assert eq2( tri::and(tri::unknown, tri::unknown), tri::unknown);
+}
+
+#[test]
+fn test_tri_or() {
+    assert eq2( tri::or(tri::true, tri::true), tri::true);
+    assert eq2( tri::or(tri::true, tri::false), tri::true);
+    assert eq2( tri::or(tri::true, tri::unknown), tri::true);
+    assert eq2( tri::or(tri::false, tri::false), tri::false);
+    assert eq2( tri::or(tri::false, tri::unknown), tri::unknown);
+    assert eq2( tri::or(tri::unknown, tri::unknown), tri::unknown);
+}
+
+#[test]
+fn test_tri_xor() {
+    assert eq2( tri::xor(tri::true, tri::true), tri::false);
+    assert eq2( tri::xor(tri::false, tri::false), tri::false);
+    assert eq2( tri::xor(tri::true, tri::false), tri::true);
+    assert eq2( tri::xor(tri::true, tri::unknown), tri::unknown);
+    assert eq2( tri::xor(tri::false, tri::unknown), tri::unknown);
+    assert eq2( tri::xor(tri::unknown, tri::unknown), tri::unknown);
+}
+
+#[test]
+fn test_tri_implies() {
+    assert eq2( tri::implies(tri::false, tri::false), tri::true);
+    assert eq2( tri::implies(tri::false, tri::unknown), tri::true);
+    assert eq2( tri::implies(tri::false, tri::true), tri::true);
+
+    assert eq2( tri::implies(tri::unknown, tri::false), tri::unknown);
+    assert eq2( tri::implies(tri::unknown, tri::unknown), tri::unknown);
+    assert eq2( tri::implies(tri::unknown, tri::true), tri::true);
+
+    assert eq2( tri::implies(tri::true, tri::false), tri::false);
+    assert eq2( tri::implies(tri::true, tri::unknown), tri::unknown);
+    assert eq2( tri::implies(tri::true, tri::true), tri::true);
+}
+
+#[test]
+fn test_tri_from_str() {
+    tri::all_values { |v|
+        assert eq2( v, tri::from_str(tri::to_str(v)));
+    }
+}
+
+#[test]
+fn test_tri_to_str() {
+    assert tri::to_str(tri::false) == "false";
+    assert tri::to_str(tri::unknown) == "unknown";
+    assert tri::to_str(tri::true) == "true";
+}
+
+#[test]
+fn test_tri_to_bit() {
+    tri::all_values { |v|
+        assert tri::to_bit(v) == if tri::is_true(v) { 1u8 } else { 0u8 };
+    }
+}
\ No newline at end of file