mirror of
https://github.com/rust-lang/rust.git
synced 2024-11-22 23:04:33 +00:00
Marijn Haverbeke
parent
fda7bb6721
commit
a65af017ca
@ -1,307 +0,0 @@
|
||||
// -*- 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:
|
||||
@ -14,7 +14,7 @@ use core(vers = "0.2");
|
||||
import core::*;
|
||||
|
||||
export net, uv;
|
||||
export c_vec, four, tri, util;
|
||||
export c_vec, util;
|
||||
export bitv, deque, fun_treemap, list, map, smallintmap, sort, treemap, ufind;
|
||||
export rope, arena;
|
||||
export ebml, dbg, getopts, json, rand, sha1, term, time, prettyprint;
|
||||
@ -33,8 +33,6 @@ mod uv_hl;
|
||||
// Utility modules
|
||||
|
||||
mod c_vec;
|
||||
mod four;
|
||||
mod tri;
|
||||
mod util;
|
||||
|
||||
|
||||
|
||||
@ -1,251 +0,0 @@
|
||||
// -*- rust -*-
|
||||
|
||||
#[doc = "
|
||||
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 bit operations which is fast
|
||||
on current cpus.
|
||||
"];
|
||||
|
||||
export tri, true, false, unknown;
|
||||
export not, and, or, xor, implies, eq, ne, is_true, is_false;
|
||||
export from_str, to_str, all_values, to_bit;
|
||||
|
||||
#[doc = "The type of ternary logic values"]
|
||||
type tri = u8;
|
||||
|
||||
const b0: u8 = 1u8;
|
||||
const b1: u8 = 2u8;
|
||||
const b01: u8 = 3u8;
|
||||
|
||||
#[doc = "Logic value for unknown (maybe true xor maybe false)"]
|
||||
const unknown: tri = 0u8;
|
||||
|
||||
#[doc = "Logic value for truth"]
|
||||
const true: tri = 1u8;
|
||||
|
||||
#[doc = "Logic value for falsehood"]
|
||||
const false: tri = 2u8;
|
||||
|
||||
#[doc = "Negation/Inverse"]
|
||||
pure fn not(v: tri) -> tri { ((v << 1u8) | (v >> 1u8)) & b01 }
|
||||
|
||||
#[doc = "Conjunction"]
|
||||
pure fn and(a: tri, b: tri) -> tri { ((a | b) & b1) | ((a & b) & b0) }
|
||||
|
||||
#[doc = "Disjunction"]
|
||||
pure fn or(a: tri, b: tri) -> tri { ((a & b) & b1) | ((a | b) & b0) }
|
||||
|
||||
#[doc = "Exclusive or"]
|
||||
pure fn xor(a: tri, b: tri) -> tri {
|
||||
let anb = a & b;
|
||||
let aob = a & not(b);
|
||||
ret ((anb & b1) | (anb << 1u8) | (aob >> 1u8) | (aob & b0)) & b01;
|
||||
}
|
||||
|
||||
#[doc = "Classic implication, i.e. from `a` follows `b`"]
|
||||
pure fn implies(a: tri, b: tri) -> tri {
|
||||
ret ((a & b1) >> 1u8) | (b & b0) | ((a << 1u8) & b & b1);
|
||||
}
|
||||
|
||||
#[doc = "
|
||||
# Return value
|
||||
|
||||
true if truth values `a` and `b` are indistinguishable in the logic
|
||||
"]
|
||||
pure fn eq(a: tri, b: tri) -> bool { a == b }
|
||||
|
||||
#[doc = "
|
||||
# Return value
|
||||
|
||||
true if truth values `a` and `b` are distinguishable in the logic
|
||||
"]
|
||||
pure fn ne(a: tri, b: tri) -> bool { a != b }
|
||||
|
||||
#[doc = "
|
||||
# Return value
|
||||
|
||||
true if `v` represents truth in the logic
|
||||
"]
|
||||
pure fn is_true(v: tri) -> bool { v == tri::true }
|
||||
|
||||
#[doc = "
|
||||
# Return value
|
||||
|
||||
true if `v` represents false in the logic
|
||||
"]
|
||||
pure fn is_false(v: tri) -> bool { v == tri::false }
|
||||
|
||||
#[doc = "
|
||||
# Return value
|
||||
|
||||
true if `v` represents the unknown state in the logic
|
||||
"]
|
||||
pure fn is_unknown(v: tri) -> bool { v == unknown }
|
||||
|
||||
#[doc = "Parse logic value from `s`"]
|
||||
pure fn from_str(s: str) -> tri {
|
||||
alt check s {
|
||||
"unknown" { unknown }
|
||||
"true" { tri::true }
|
||||
"false" { tri::false }
|
||||
}
|
||||
}
|
||||
|
||||
#[doc = "Convert `v` into a string"]
|
||||
pure fn to_str(v: tri) -> str {
|
||||
// FIXME replace with consts as soon as that works
|
||||
alt check v {
|
||||
0u8 { "unknown" }
|
||||
1u8 { "true" }
|
||||
2u8 { "false" }
|
||||
}
|
||||
}
|
||||
|
||||
#[doc = "
|
||||
Iterates over all truth values by passing them to `blk`
|
||||
in an unspecified order
|
||||
"]
|
||||
fn all_values(blk: fn(v: tri)) {
|
||||
blk(tri::false);
|
||||
blk(unknown);
|
||||
blk(tri::true);
|
||||
}
|
||||
|
||||
#[doc = "
|
||||
# Return value
|
||||
|
||||
An u8 whose first bit is set if `if_true(v)` holds
|
||||
"]
|
||||
fn to_bit(v: tri) -> u8 { v & b0 }
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
|
||||
pure fn eq1(a: tri::tri, b: tri::tri) -> bool { tri::eq(a , b) }
|
||||
pure fn ne1(a: tri::tri, b: tri::tri) -> bool { tri::ne(a , b) }
|
||||
|
||||
pure fn eq2(a: tri::tri, b: tri::tri) -> 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 };
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Local Variables:
|
||||
// mode: rust;
|
||||
// fill-column: 78;
|
||||
// indent-tabs-mode: nil
|
||||
// c-basic-offset: 4
|
||||
// buffer-file-coding-system: utf-8-unix
|
||||
// End:
|
||||
Loading…
Reference in New Issue
Block a user