308 lines
7.2 KiB
Rust
308 lines
7.2 KiB
Rust
// -*- rust -*-
|
|
|
|
#[doc = "
|
|
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 bit operations which is fast
|
|
on current cpus.
|
|
"];
|
|
|
|
import tri;
|
|
|
|
export four, 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;
|
|
|
|
#[doc = "
|
|
The type of fourrternary logic values
|
|
|
|
It may be thought of as tuple `(y, x)` of two bools
|
|
"]
|
|
type four = u8;
|
|
|
|
const b0: u8 = 1u8;
|
|
const b1: u8 = 2u8;
|
|
const b01: u8 = 3u8;
|
|
|
|
#[doc = "Logic value `(0, 0)` for bottom (neither true or false)"]
|
|
const none: four = 0u8;
|
|
|
|
#[doc = "Logic value `(0, 1)` for truth"]
|
|
const true: four = 1u8;
|
|
|
|
#[doc = "Logic value `(1, 0)` for falsehood"]
|
|
const false: four = 2u8;
|
|
|
|
#[doc = "Logic value `(1, 1)` for top (both true and false)"]
|
|
const both: four = 3u8;
|
|
|
|
#[doc = "
|
|
Negation/Inverse
|
|
|
|
Returns `'(v.y, v.x)`
|
|
"]
|
|
pure fn not(v: four) -> four { ((v << 1u8) | (v >> 1u8)) & b01 }
|
|
|
|
#[doc = "
|
|
Conjunction
|
|
|
|
Returns `(a.x | b.x, a.y & b.y)`
|
|
"]
|
|
pure fn and(a: four, b: four) -> four { ((a & b) & b0) | ((a | b) & b1) }
|
|
|
|
#[doc = "
|
|
Disjunction
|
|
|
|
Returns `(a.x & b.x, a.y | b.y)`
|
|
"]
|
|
pure fn or(a: four, b: four) -> four { ((a | b) & b0) | ((a & b) & b1) }
|
|
|
|
#[doc = "
|
|
Classic exclusive or
|
|
|
|
Returns `or(and(a, not(b)), and(not(a), b))`
|
|
"]
|
|
pure fn xor(a: four, b: four) -> four { or(and(a, not(b)), and(not(a), b)) }
|
|
|
|
#[doc = "
|
|
Strong implication (from `a` strongly follows `b`)
|
|
|
|
Returns `( x1 & y2, !x1 | x2)`
|
|
"]
|
|
pure fn implies(a: four, b: four) -> four {
|
|
((a << 1u8) & b & b1) | (((!a) | b) & b0)
|
|
}
|
|
|
|
#[doc = "
|
|
Classic (material) implication in the logic
|
|
(from `a` materially follows `b`)
|
|
|
|
Returns `or(not(a), b)`
|
|
"]
|
|
pure fn implies_materially(a: four, b: four) -> four { or(not(a), b) }
|
|
|
|
#[doc = "
|
|
Returns true if truth values `a` and `b` are indistinguishable in the logic
|
|
"]
|
|
pure fn eq(a: four, b: four) -> bool { a == b }
|
|
|
|
#[doc = "
|
|
Returns true if truth values `a` and `b` are distinguishable in the logic
|
|
"]
|
|
pure fn ne(a: four, b: four) -> bool { a != b }
|
|
|
|
#[doc = "
|
|
Returns true if `v` represents truth in the logic (is `true` or `both`)
|
|
"]
|
|
pure fn is_true(v: four) -> bool { (v & b0) != 0u8 }
|
|
|
|
#[doc = "
|
|
Returns true if `v` represents falsehood in the logic (is `false` or `none`)
|
|
"]
|
|
pure fn is_false(v: four) -> bool { (v & b0) == 0u8 }
|
|
|
|
#[doc = "Parse logic value from `s`"]
|
|
pure fn from_str(s: str) -> four {
|
|
alt check s {
|
|
"none" { none }
|
|
"false" { four::false }
|
|
"true" { four::true }
|
|
"both" { both }
|
|
}
|
|
}
|
|
|
|
#[doc = "Convert `v` into a string"]
|
|
pure fn to_str(v: four) -> str {
|
|
// FIXME replace with consts as soon as that works
|
|
alt check v {
|
|
0u8 { "none" }
|
|
1u8 { "true" }
|
|
2u8 { "false" }
|
|
3u8 { "both" }
|
|
}
|
|
}
|
|
|
|
#[doc = "
|
|
Iterates over all truth values by passing them to `blk` in an unspecified
|
|
order
|
|
"]
|
|
fn all_values(blk: fn(v: four)) {
|
|
blk(both);
|
|
blk(four::true);
|
|
blk(four::false);
|
|
blk(none);
|
|
}
|
|
|
|
#[doc = "
|
|
Returns an `u8` whose first bit is set if `if_true(v)` holds
|
|
"]
|
|
fn to_bit(v: four) -> u8 { v & b0 }
|
|
|
|
#[doc = "
|
|
Returns a trit of `v` (`both` and `none` are both coalesced into
|
|
`trit::unknown`)
|
|
"]
|
|
fn to_trit(v: four) -> tri::tri { v & (v ^ not(v)) }
|
|
|
|
#[cfg(test)]
|
|
mod tests {
|
|
|
|
fn eq1(a: four, b: four) -> bool { four::eq(a , b) }
|
|
fn ne1(a: four, b: four) -> bool { four::ne(a , b) }
|
|
|
|
fn eq2(a: four, b: four) -> 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) -> (bool, bool) {
|
|
alt check 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(debug, 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 };
|
|
}
|
|
}
|
|
}
|
|
|
|
// Local Variables:
|
|
// mode: rust;
|
|
// fill-column: 78;
|
|
// indent-tabs-mode: nil
|
|
// c-basic-offset: 4
|
|
// buffer-file-coding-system: utf-8-unix
|
|
// End:
|