Created
October 23, 2025 11:02
-
-
Save Kaisia-Estrel/0af6168340db7ecd0dc9598519997da9 to your computer and use it in GitHub Desktop.
Just a truth table generator I made using haskell operators, I havent properly defined precedence so you might have to properly parenthesize everything
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE BlockArguments #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE ImpredicativeTypes #-} | |
| {-# LANGUAGE LambdaCase #-} | |
| module Main (main) where | |
| import Data.Function (on) | |
| import Data.List (intercalate, nub, sortBy, subsequences, transpose) | |
| data Var = P | Q | R | |
| deriving (Show, Eq) | |
| data Prop | |
| = Xor Prop Prop | |
| | LVar Var | |
| | Or Prop Prop | |
| | And Prop Prop | |
| | Imply Prop Prop | |
| | Bicon Prop Prop | |
| | Converse Prop Prop | |
| | Not Prop | |
| deriving (Eq) | |
| instance Show Prop where | |
| show (LVar v) = show v | |
| show (Xor l b) = "(" ++ show l ++ " xor " ++ show b ++ ")" | |
| show (Or l b) = "(" ++ show l ++ " or " ++ show b ++ ")" | |
| show (And l b) = "(" ++ show l ++ " and " ++ show b ++ ")" | |
| show (Imply l b) = "(" ++ show l ++ " arrow.double " ++ show b ++ ")" | |
| show (Bicon l b) = "(" ++ show l ++ " arrow.l.r.double " ++ show b ++ ")" | |
| show (Converse l b) = "(" ++ show l ++ " arrow.r.double " ++ show b ++ ")" | |
| show (Not l) = "not " ++ show l | |
| p, q, r :: Prop | |
| p = LVar P | |
| q = LVar Q | |
| r = LVar R | |
| (⊕) :: Prop -> Prop -> Prop | |
| x ⊕ y = Xor x y | |
| (∧) :: Prop -> Prop -> Prop | |
| x ∧ y = And x y | |
| (∨) :: Prop -> Prop -> Prop | |
| x ∨ y = Or x y | |
| (-->) :: Prop -> Prop -> Prop | |
| x --> y = Imply x y | |
| (<--) :: Prop -> Prop -> Prop | |
| x <-- y = Converse x y | |
| (<->) :: Prop -> Prop -> Prop | |
| x <-> y = Bicon x y | |
| lnot :: Prop -> Prop | |
| lnot x = Not x | |
| splitCompound :: Prop -> [Prop] | |
| splitCompound = sortBy sorter . nub . splitCompound' | |
| where | |
| sorter (LVar P) _ = LT | |
| sorter (LVar Q) (LVar P) = GT | |
| sorter (LVar Q) (LVar Q) = EQ | |
| sorter (LVar Q) _ = LT | |
| sorter (LVar R) (LVar P) = GT | |
| sorter (LVar R) (LVar Q) = GT | |
| sorter (LVar R) (LVar R) = EQ | |
| sorter (LVar R) _ = LT | |
| sorter x y = (compare `on` (length . show)) x y | |
| splitCompound' x@(Or l b) = splitCompound l ++ splitCompound b ++ [x] | |
| splitCompound' x@(And l b) = splitCompound l ++ splitCompound b ++ [x] | |
| splitCompound' x@(Imply l b) = splitCompound l ++ splitCompound b ++ [x] | |
| splitCompound' x@(Bicon l b) = splitCompound l ++ splitCompound b ++ [x] | |
| splitCompound' x@(Converse l b) = splitCompound l ++ splitCompound b ++ [x] | |
| splitCompound' x@(Xor l b) = splitCompound l ++ splitCompound b ++ [x] | |
| splitCompound' x@(Not l) = splitCompound l ++ [x] | |
| splitCompound' x@(LVar _) = [x] | |
| imply :: Bool -> Bool -> Bool | |
| imply False _ = True | |
| imply True x = x | |
| converse :: Bool -> Bool -> Bool | |
| converse True _ = True | |
| converse False x = not x | |
| eval :: [Prop] -> Prop -> Bool | |
| eval xs (LVar v) = elem (LVar v) xs | |
| eval xs (Or a b) = eval xs a || eval xs b | |
| eval xs (And a b) = eval xs a && eval xs b | |
| eval xs (Bicon a b) = eval xs a == eval xs b | |
| eval xs (Imply a b) = eval xs a `imply` eval xs b | |
| eval xs (Converse a b) = eval xs a `converse` eval xs b | |
| eval xs (Not a) = not $ eval xs a | |
| eval xs (Xor a b) = | |
| let | |
| a' = eval xs a | |
| b' = eval xs b | |
| in | |
| a' || b' && a' /= b' | |
| truthTable :: [Prop] -> [[Bool]] | |
| truthTable xs = | |
| let | |
| vars = takeWhile (\case (LVar _) -> True; _ -> False) xs | |
| varCols = reverse $ subsequences vars | |
| in | |
| transpose $ map (\stmnt -> map (`eval` stmnt) varCols) xs | |
| typstTable :: Prop -> IO () | |
| typstTable l = do | |
| let headers = splitCompound l | |
| let tbl = typstTable' headers (truthTable headers) | |
| putStrLn $ "=== $" ++ show l ++ "$" | |
| putStrLn tbl | |
| typstTable' :: [Prop] -> [[Bool]] -> String | |
| typstTable' headers rows = | |
| "#table(\n" | |
| ++ (" columns: " ++ show (length headers) ++ ",\n") | |
| ++ (" table.header(" ++ intercalate "," (map (\x -> "$" ++ show x ++ "$") headers) ++ "),\n") | |
| ++ unlines (map (mappend " " . concatMap (\x -> if x then "$T$," else "$F$,")) rows) | |
| ++ "\n)" | |
| quicksort (x : xs) = | |
| quicksort (filter (< x) xs) ++ [x] ++ quicksort (filter (>= x) xs) | |
| quicksort [] = [] | |
| take' :: (Eq t, Num t) => t -> ([a] -> [a]) | |
| take' _ [] = [] | |
| take' 0 _ = [] | |
| take' n (x : xs) = x : take' (n - 1) xs | |
| main :: IO () | |
| main = do | |
| typstTable $ ((p ∧ q) --> r) --> (p --> (q --> r)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment