// -*- 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: