PROPOSITIONS

results

miles@laptop:~/Projects/tableaux $ rustc test.rs && ./test
T
F
~(T)
~(F)
(T) ^ (T)
(T) v (T)
(T) -> (T)
((T) v (T)) ^ (T)
True
False
Not(True)
Not(False)
And(True, True)
Or(True, True)
Implies(True, True)
And(Or(True, True), True)

test.rs

#![feature(box_patterns)]
#![feature(box_syntax)]

use std::fmt;

#[derive(Debug)]
enum Proposition {
    True,
    False,
    Not(Box<Proposition>),
    And(Box<Proposition>, Box<Proposition>),
    Or(Box<Proposition>, Box<Proposition>),
    Implies(Box<Proposition>, Box<Proposition>),
}

impl fmt::Display for Proposition {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        match *self {
            Proposition::True => write!(f, "T"),
            Proposition::False => write!(f, "F"),
            Proposition::Not(ref p) => write!(f, "~({})", p),
            Proposition::And(ref l, ref r) => write!(f, "({}) ^ ({})", l, r),
            Proposition::Or(ref l, ref r) => write!(f, "({}) v ({})", l, r),
            Proposition::Implies(ref ante, ref cons) => write!(f, "({}) -> ({})", ante, cons),
            //_ => unimplemented!(),
        }
    }
}

macro_rules! prop {
    [($($t:tt)*)] => (prop![$($t)*]);
    [T] => (Proposition::True);
    [F] => (Proposition::False);
    [!$e:tt] => (Proposition::Not(box prop![$e]));
    [$e:tt ^ $f:tt] => (Proposition::And(box prop![$e], box prop![$f]));
    [$e:tt v $f:tt] => (Proposition::Or(box prop![$e], box prop![$f]));
    [$e:tt -> $f:tt] => (Proposition::Implies(box prop![$e], box prop![$f]));
}

fn main() {
    println!("{}", prop!(T));
    println!("{}", prop!(F));
    println!("{}", prop!(!T));
    println!("{}", prop!(!F));
    println!("{}", prop!(T ^ T));
    println!("{}", prop!(T v T));
    println!("{}", prop!(T -> T));
    println!("{}", prop!((T v T) ^ T));
    println!("{:?}", prop!(T));
    println!("{:?}", prop!(F));
    println!("{:?}", prop!(!T));
    println!("{:?}", prop!(!F));
    println!("{:?}", prop!(T ^ T));
    println!("{:?}", prop!(T v T));
    println!("{:?}", prop!(T -> T));
    println!("{:?}", prop!((T v T) ^ T));
}