# Josua Kugler, Christian Merten

library(tidyverse)
library(rlang)

variables <- LETTERS[1:7]
names(variables) <- variables
prop_ops <- exprs(`(`,`!`,`&`,`|`,`<=`,`>=`,`==`)
prop_ops_str <- sapply(prop_ops, expr_text)
ops_expr_str <- c("==", "<=", ">=", "&", "|", "!")
ops_print_str <- c("\u2194","\u2190","\u2192","\u2227","\u2228","\u00AC")
names(ops_print_str) <- ops_expr_str

flip <- function(f) function(x,y) f(y,x)
implies <- function(A, B) (!A) | B

validate_Prop <- function(e) {
    stopifnot("class must be Prop" = "Prop" %in% class(e))
    stopifnot("only numbers 0 and 1 allowed" = !str_detect(expr_text(e), "[2-9]"))
    stopifnot("invalid operator or variable" = all(all.names(e) %in% c(variables, ops_expr_str, "(", ")")))
    e
}

Prop <- function(x) {
    e <- enexpr(x)
    if (typeof(e) == "symbol") e <- expr(( (!!e) ))
    validate_Prop(structure(e, class="Prop"))
}

tochar <- function(p) str_replace_all(expr_text(p), fixed(ops_print_str))

print.Prop <- function(p) {
    cat(tochar(p), "\n")
    invisible(p)
}

interprete <- function(prop, vars, append=FALSE) {
    res <- as.logical(eval_tidy(prop, c(as.list(vars),
                                        `>=` = implies,
                                        `<=` = flip(implies))))
    var <- tochar(prop)
    if(append) add_column(vars, (!!sym(var)) := res)
    else res
}

combinations <- do.call(expand.grid, lapply(variables, function(v) c(0,1)))

is_tautology <- function(prop) {
    all(interprete(prop, combinations))
}