truthy.ts

/**
 * @classAndrew
 * Shunting-Yard logical expression truth table generator
 * 9 September 2021
 */

interface BoolRefJSON {
    [name: string]: boolean;
};

const precedence = {
    '~': 4,
    '&': 3,
    '|': 2,
    '^': 2,
    "->": 1,
    "<->": 0,
    // for the sake of identifying what isn't a variable
    '(': null,
    ')': null,
};

function parse(expr: string): [string[], BoolRefJSON] {
    let tokens: string[] = tokenize(expr);
    let stack: string[] = [];
    let opstack: string[] = [];

    const boolRefs = {};

    /** Shunting yard */
    for (let i = 0; i < tokens.length; i++) {
        if (precedence[tokens[i]] === undefined) {
            stack.push(tokens[i]);
            boolRefs[tokens[i]] = 0;
        }
        else if (tokens[i] == '~') {
            opstack.push(tokens[i]);
        }
        else if (precedence[tokens[i]] !== null) {
            const op1 = tokens[i];
            let op2 = opstack[opstack.length-1];

            while (opstack.length && opstack[opstack.length-1] == op2 && op2 != "(" && precedence[op1] <= precedence[op2]) {
                stack.push(opstack.pop());
                op2 = opstack[opstack.length-1];
            }

            opstack.push(op1);
        }
        else if (tokens[i] == '(') {
            opstack.push(tokens[i]);
        }
        else if (tokens[i] == ')') {
            while (opstack.length && opstack[opstack.length-1] != '(') {
                stack.push(opstack.pop());
            }
            
            opstack.pop();

            if (opstack[opstack.length-1] == '~') {
                stack.push(opstack.pop());
            }
        }
    }

    while (opstack.length) stack.push(opstack.pop());
    
    return [stack, boolRefs];
}

const states = {
    none: 0, 
    iff: 1,
    if: 2,
};

function tokenize(expr: string): string[] {
    let tokens: string[] = [];
    let i = 0;

    let buffer = [];
    let state = states.none;

    while (i < expr.length) {
        if (state == states.none) {
            // *should* handle -> and <->, everything else is one character
            if (expr[i] == "<") {
                state = states.iff;
            }
            else if (expr[i] == "-") {   
                state = states.if;
            }

            if (buffer.length > 0)
                tokens.push(buffer.join(""));
            buffer = [];      
        }

        // end of an iff or if 
        if (expr[i] == ">") {
            state = states.none;
        }

        if (expr[i] != ' ') // ignore whitespace
            buffer.push(expr[i]);

        i++;
    }

    tokens.push(buffer.join(""));

    return tokens;
}

function templ(refs: BoolRefJSON, p: any, q: any, op: string) {
    if (op == "~") {
        return (refs[p] !== undefined) ? 
            `~${p}` : `~(${p})`
    }
    
    const a = p[0] == "~" && refs[p.slice(1)] !== undefined;
    const b = q[0] == "~" && refs[q.slice(1)] !== undefined;

    return `${refs[p] !== undefined || a ? p : `(${p})`}${op}${refs[q] !== undefined || b ? q : `(${q})`}`;
}

class Table {
    rows: string[][];
    header = [];
    rpn: string[];
    refs: BoolRefJSON

    constructor(parsed: [string[], BoolRefJSON]) {
        this.rpn = parsed[0];
        this.refs = parsed[1];
        this.header = Object.keys(this.refs);
        this.rows = new Array<string[]>(1 << this.header.length);

        let stack = []
        // E
        // duplicated code but we need to get header row
        for (let i = 0; i < this.rpn.length; i++) {
            if (precedence[this.rpn[i]] === undefined) { // if variable
                stack.push(this.rpn[i]);
                continue;
            }

            let p = 0; let q = 0;

            switch (this.rpn[i]) {
                case '~':
                    // stack.push("~"+stack.pop());
                    stack.push(templ(this.refs, stack.pop(), null, '~'));
                    break;
                case '&':
                    q = stack.pop();
                    // stack.push(stack.pop()+"&"+q);
                    stack.push(templ(this.refs, stack.pop(), q, '&'));
                    break;
                case '|':
                    q = stack.pop();
                    // stack.push(stack.pop()+"|"+q);
                    stack.push(templ(this.refs, stack.pop(), q, '|'));
                    break;
                case '^':
                    q = stack.pop();
                    // stack.push(stack.pop()+"^"+q);
                    stack.push(templ(this.refs, stack.pop(), q, '^'));
                    break;
                case "->":
                    q = stack.pop();
                    p = stack.pop();
                    // stack.push(p+"->"+q);
                    stack.push(templ(this.refs, p, q, "->"));
                    break;
                case "<->":
                    q = stack.pop();
                    p = stack.pop();
                    //stack.push(p+"<->"+q);
                    stack.push(templ(this.refs, p, q, "<->"));
                    break;
            }

            this.header.push(stack[stack.length-1]);
        }

        this.eval();
    }

    eval() {
        const keys = Object.keys(this.refs);
        // bitset trick
        for (let seq = 0; seq < (1 << keys.length); seq++) {
            this.rows[seq] = []; // initialize the row
            for (let i = 0; i < keys.length; i++) {
                const on = +!!(seq & (1 << i)); // bitmask
                this.rows[seq].push("FT"[on]);
                this.refs[keys[i]] = !!on;
            }
            
            const stack = [];

            for (let i = 0; i < this.rpn.length; i++) {
                if (precedence[this.rpn[i]] === undefined) { // if variable
                    stack.push(this.refs[this.rpn[i]]);
                    continue;
                }

                let p = 0; let q = 0;

                switch (this.rpn[i]) {
                    case '~':
                        stack.push(!stack.pop());
                        break;
                    case '&':
                        stack.push(stack.pop() & stack.pop());
                        break;
                    case '|':
                        stack.push(stack.pop() | stack.pop());
                        break;
                    case "->":
                        q = stack.pop();
                        p = stack.pop();
                        stack.push(+!p | q);
                        break;
                    case "<->":
                        q = stack.pop();
                        p = stack.pop();
                        stack.push((p & q) | (+!p & +!q));
                        break;
                    case '^':
                        q = stack.pop();
                        stack.push(stack.pop()^q);
                        break;
                }
                this.rows[seq].push("FT"[+stack[stack.length-1]]);
            }
        }
    }
}

// const testStr1 = "T & F | T -> T";
// const testStr2 = "T & F <-> F | T <-> T";
// const testStr3 = "p & ((q -> r) | p) <-> ~q";
// const testStr4 = "p & ((q -> r) | p)";

// console.log(tokenize(testStr1));
// console.log(tokenize(testStr2));
// console.log(tokenize(testStr3));
// console.log(parse(testStr3));
// console.log(new Table(parse(testStr3)));

export {Table, parse};