tarski.rs

tarski.rs

use std::collections::HashMap;
use std::env;
use std::fs;

#[derive(Debug)]
enum Formula {
    Atom(char),
    Not(Box<Formula>),
    And(Box<Formula>, Box<Formula>),
}

impl std::fmt::Display for Formula {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Formula::Atom(c) => write!(f, "{}", c),
            Formula::Not(sub) => write!(f, "¬{}", sub),
            Formula::And(left, right) => write!(f, "({} ∧ {})", left, right),
        }
    }
}

fn parse_formula(input: &str) -> Result<(Formula, &str), String> {
    if input.is_empty() {
        return Err("Unexpected end of input".to_string());
    }

    let mut chars = input.chars();
    let first = chars.next().unwrap();
    let first_len = first.len_utf8();

    match first {
        // Atomic proposition: single uppercase letter
        ch if ch.is_ascii_uppercase() => {
            let rest = &input[first_len..];
            Ok((Formula::Atom(ch), rest))
        }
        // Negation: ¬ followed by a formula
        '¬' => {
            let (sub, rest) = parse_formula(&input[first_len..])?;
            Ok((Formula::Not(Box::new(sub)), rest))
        }
        // Parenthesized formula (for grouping or binary conjunction)
        '(' => {
            let (left, after_left) = parse_formula(&input[1..])?;

            // Check if this is a conjunction (P ∧ Q)
            if after_left.starts_with('∧') {
                let after_op = &after_left['∧'.len_utf8()..];
                let (right, after_right) = parse_formula(after_op)?;

                if !after_right.starts_with(')') {
                    return Err("Expected ')' after right-hand side of ∧".to_string());
                }
                let rest = &after_right[1..];
                Ok((Formula::And(Box::new(left), Box::new(right)), rest))
            }
            // Otherwise it's just a grouped formula: (φ)
            else if after_left.starts_with(')') {
                let rest = &after_left[1..];
                Ok((left, rest))
            } else {
                Err("Expected '∧' or ')' after subformula inside parentheses".to_string())
            }
        }
        _ => Err(format!("Unexpected character: {}", first)),
    }
}

fn parse(input: &str) -> Result<Formula, String> {
    // Remove all whitespace so the parser sees clean tokens (¬, ∧, (, ), letters)
    let cleaned: String = input.chars().filter(|c| !c.is_whitespace()).collect();
    let (formula, rest) = parse_formula(&cleaned)?;
    if rest.is_empty() {
        Ok(formula)
    } else {
        Err(format!("Extra characters after formula: {}", rest))
    }
}

impl Formula {
    fn evaluate(&self, assignment: &HashMap<char, bool>) -> bool {
        match self {
            Formula::Atom(c) => *assignment.get(c).unwrap_or(&false),
            Formula::Not(sub) => !sub.evaluate(assignment),
            Formula::And(left, right) => left.evaluate(assignment) && right.evaluate(assignment),
        }
    }
}

fn main() {
    // Hardcoded truth assignment (the "interpretation" in Tarski's semantics)
    // Change these values or add more letters as needed.
    let mut assignment: HashMap<char, bool> = HashMap::new();
    assignment.insert('P', true);
    assignment.insert('Q', false);
    assignment.insert('R', true);
    // Example: P is true, Q is false, R is true

    // Read the formula from a file (first command-line argument, or default to "formula.txt")
    let filename = env::args().nth(1).unwrap_or_else(|| "formula.txt".to_string());
    let content = match fs::read_to_string(&filename) {
        Ok(c) => c,
        Err(e) => {
            eprintln!("Error reading file '{}': {}", filename, e);
            return;
        }
    };

    // Parse using the grammar described in the tweet:
    // - Atoms: P, Q, R, ...
    // - ¬φ
    // - (φ ∧ ψ)
    // - Parentheses for grouping
    let formula = match parse(&content) {
        Ok(f) => f,
        Err(e) => {
            eprintln!("Parse error: {}", e);
            eprintln!("Make sure the formula is a well-formed formula using only:");
            eprintln!("  - Uppercase letters (P, Q, R, ...)");
            eprintln!("  - ¬ (negation)");
            eprintln!("  - ∧ (conjunction)");
            eprintln!("  - Parentheses for every binary ∧, e.g. (P ∧ ¬Q)");
            eprintln!("Example content for formula.txt:");
            eprintln!("(P ∧ ¬Q)");
            return;
        }
    };

    // Evaluate exactly as Tarski's semantic definition:
    // - Look up atoms in the truth assignment
    // - ¬ flips the truth value (recursively)
    // - ∧ applies logical and (recursively on both sides)
    let truth_value = formula.evaluate(&assignment);

    println!("Parsed formula : {}", formula);
    println!("Truth assignment used: {:?}", assignment);
    println!("Truth value     : {}", truth_value);
}