Compilers for contrarians

[+] Show Prelude

infixr 9 . , !! , ! infixl 7 * , `div` , `mod` infixl 6 + , - infixr 5 ++ infixl 4 <*> , <$> , <* , *> infix 4 == , /= , <= , >= , < , > infixl 3 && , <|> infixl 2 || infixl 1 >> , >>= , & infixr 1 =<< infixr 0 $ isEOF = (0 /=) <$> isEOFInt class Ring a where (+) :: a -> a -> a (-) :: a -> a -> a (*) :: a -> a -> a fromInt :: Int -> a class Integral a where div :: a -> a -> a mod :: a -> a -> a quot :: a -> a -> a rem :: a -> a -> a instance Ring Int where (+) = intAdd (-) = intSub (*) = intMul fromInt = id instance Integral Int where div = intDiv mod = intMod quot = intQuot rem = intRem instance Ring Word where (+) = wordAdd (-) = wordSub (*) = wordMul fromInt = wordFromInt instance Integral Word where div = wordDiv mod = wordMod quot = wordQuot rem = wordRem instance Eq Word where (==) = wordEq instance Ord Word where (<=) = wordLE data Word64 = Word64 Word Word instance Ring Word64 where Word64 a b + Word64 c d = uncurry Word64 $ word64Add a b c d Word64 a b - Word64 c d = uncurry Word64 $ word64Sub a b c d Word64 a b * Word64 c d = uncurry Word64 $ word64Mul a b c d fromInt x = Word64 (wordFromInt x) (wordFromInt 0) instance Eq Word64 where Word64 a b == Word64 c d = a == c && b == d instance Ord Word64 where Word64 a b <= Word64 c d | b == d = a <= c | True = b <= d f $ x = f x x & f = f x id x = x const x y = x flip f x y = f y x class Functor f where fmap :: (a -> b) -> f a -> f b class Applicative f where pure :: a -> f a (<*>) :: f (a -> b) -> f a -> f b class Monad m where return :: a -> m a (>>=) :: m a -> (a -> m b) -> m b (<$>) = fmap liftA2 f x y = f <$> x <*> y (*>) = liftA2 \x y -> y (<*) = liftA2 \x y -> x (>>) f g = f >>= \_ -> g (=<<) = flip (>>=) bool f t b = if b then t else f class Eq a where (==) :: a -> a -> Bool instance Eq Int where (==) = intEq instance Eq Char where (==) = charEq instance Eq Bool where True == True = True False == False = True _ == _ = False instance Show Bool where show True = "True" show False = "False" class Ord a where (<=) :: a -> a -> Bool x <= y = case compare x y of LT -> True EQ -> True GT -> False compare :: a -> a -> Ordering compare x y = if x <= y then if y <= x then EQ else LT else GT instance Ord Int where (<=) = intLE instance Ord Char where (<=) = charLE data Ordering = LT | GT | EQ min a b = if a <= b then a else b max a b = if b <= a then a else b instance Ord a => Ord [a] where xs <= ys = case xs of [] -> True x:xt -> case ys of [] -> False y:yt -> case compare x y of LT -> True GT -> False EQ -> xt <= yt instance (Eq a, Eq b) => Eq (a, b) where (x1, y1) == (x2, y2) = x1 == x2 && y1 == y2 instance (Ord a, Ord b) => Ord (a, b) where (x1, y1) <= (x2, y2) = if x1 <= x2 then if x2 <= x1 then y1 <= y2 else True else False (>=) = flip (<=) x > y = y <= x && y /= x x < y = x <= y && x /= y data Maybe a = Nothing | Just a data Either a b = Left a | Right b fst (x, y) = x snd (x, y) = y uncurry f (x, y) = f x y first f (x, y) = (f x, y) second f (x, y) = (x, f y) not a = if a then False else True x /= y = not $ x == y (.) f g x = f (g x) infixl 0 |> infixr 0 <| infixl 9 .> infixr 9 <. (<.) = (.) (.>) = flip (.) (|>) = (&) (<|) = ($) (||) f g = if f then True else g (&&) f g = if f then g else False instance Eq a => Eq [a] where xs == ys = case xs of [] -> case ys of [] -> True _ -> False x:xt -> case ys of [] -> False y:yt -> x == y && xt == yt null [] = True null _ = False init [x] = [] init (x:xs) = x : init xs last [x] = x last (_:xs) = last xs take 0 xs = [] take _ [] = [] take n (h:t) = h : take (n - 1) t drop n xs | n <= 0 = xs drop _ [] = [] drop n (_:xs) = drop (n-1) xs length = foldr (\_ n -> n + 1) 0 splitAt n xs = (take n xs, drop n xs) lines "" = [] lines s = let (l, rest) = break (== '\n') s in l : case rest of [] -> [] (_:s') -> lines s' unlines [] = [] unlines (l:ls) = l ++ '\n' : unlines ls maybe n j m = case m of Nothing -> n; Just x -> j x instance Functor Maybe where fmap f = maybe Nothing (Just . f) instance Applicative Maybe where pure = Just mf <*> mx = maybe Nothing (\f -> maybe Nothing (Just . f) mx) mf instance Monad Maybe where return = Just mf >>= mg = maybe Nothing mg mf foldr c n l = case l of [] -> n h:t -> c h (foldr c n t) mapM f = foldr (\a rest -> liftA2 (:) (f a) rest) (pure []) mapM_ f = foldr ((>>) . f) (pure ()) foldM f z0 xs = foldr (\x k z -> f z x >>= k) pure xs z0 instance Functor IO where fmap f x = ioPure f <*> x instance Applicative IO where pure = ioPure f <*> x = ioBind f \g -> ioBind x \y -> ioPure (g y) instance Monad IO where return = ioPure ; (>>=) = ioBind putStr = mapM_ putChar putStrLn s = putStr s >> putChar '\n' error s = unsafePerformIO $ putStr s >> putChar '\n' >> exitSuccess undefined = error "undefined" foldr1 c l@(h:t) = maybe undefined id $ foldr (\x m -> Just $ maybe x (c x) m) Nothing l foldl f a bs = foldr (\b g x -> g (f x b)) (\x -> x) bs a foldl1 f (h:t) = foldl f h t reverse = foldl (flip (:)) [] elem k xs = foldr (\x t -> x == k || t) False xs find f xs = foldr (\x t -> if f x then Just x else t) Nothing xs (++) = flip (foldr (:)) concat = foldr (++) [] map = flip (foldr . ((:) .)) [] concatMap = (concat .) . map and = foldr (&&) True or = foldr (||) False all f = and . map f any f = or . map f (x:xt) !! n = if n == 0 then x else xt !! (n - 1) instance Functor [] where fmap = map instance Applicative [] where pure = (:[]); f <*> x = concatMap (<$> x) f instance Monad [] where return = (:[]); (>>=) = flip concatMap lookup s = foldr (\(k, v) t -> if s == k then Just v else t) Nothing iterate f x = x : iterate f (f x) zipWith _ [] _ = [] zipWith _ _ [] = [] zipWith f (x:xt) (y:yt) = f x y : zipWith f xt yt zip = zipWith (,) head (h:_) = h tail (_:t) = t repeat x = x : repeat x cycle = concat . repeat data State s a = State (s -> (a, s)) runState (State f) = f instance Functor (State s) where fmap f = \(State h) -> State (first f . h) instance Applicative (State s) where pure a = State (a,) (State f) <*> (State x) = State \s -> flip uncurry (f s) \g s' -> first g $ x s' instance Monad (State s) where return a = State (a,) (State h) >>= f = State $ uncurry (runState . f) . h evalState m s = fst $ runState m s get = State \s -> (s, s) put n = State \s -> ((), n) either l r e = case e of Left x -> l x; Right x -> r x instance Functor (Either a) where fmap f e = either Left (Right . f) e instance Applicative (Either a) where pure = Right ef <*> ex = case ef of Left s -> Left s Right f -> either Left (Right . f) ex instance Monad (Either a) where return = Right ex >>= f = either Left f ex -- Map. data Map k a = Tip | Bin Int k a (Map k a) (Map k a) size m = case m of Tip -> 0 ; Bin sz _ _ _ _ -> sz node k x l r = Bin (1 + size l + size r) k x l r singleton k x = Bin 1 k x Tip Tip singleL k x l (Bin _ rk rkx rl rr) = node rk rkx (node k x l rl) rr doubleL k x l (Bin _ rk rkx (Bin _ rlk rlkx rll rlr) rr) = node rlk rlkx (node k x l rll) (node rk rkx rlr rr) singleR k x (Bin _ lk lkx ll lr) r = node lk lkx ll (node k x lr r) doubleR k x (Bin _ lk lkx ll (Bin _ lrk lrkx lrl lrr)) r = node lrk lrkx (node lk lkx ll lrl) (node k x lrr r) balance k x l r = f k x l r where f | size l + size r <= 1 = node | 5 * size l + 3 <= 2 * size r = case r of Tip -> node Bin sz _ _ rl rr -> if 2 * size rl + 1 <= 3 * size rr then singleL else doubleL | 5 * size r + 3 <= 2 * size l = case l of Tip -> node Bin sz _ _ ll lr -> if 2 * size lr + 1 <= 3 * size ll then singleR else doubleR | True = node insert kx x t = case t of Tip -> singleton kx x Bin sz ky y l r -> case compare kx ky of LT -> balance ky y (insert kx x l) r GT -> balance ky y l (insert kx x r) EQ -> Bin sz kx x l r insertWith f kx x t = case t of Tip -> singleton kx x Bin sy ky y l r -> case compare kx ky of LT -> balance ky y (insertWith f kx x l) r GT -> balance ky y l (insertWith f kx x r) EQ -> Bin sy kx (f x y) l r mlookup kx t = case t of Tip -> Nothing Bin _ ky y l r -> case compare kx ky of LT -> mlookup kx l GT -> mlookup kx r EQ -> Just y fromList = foldl (\t (k, x) -> insert k x t) Tip fromListWith f = foldl (\t (k, x) -> insertWith f k x t) Tip member k t = maybe False (const True) $ mlookup k t t!k = maybe undefined id $ mlookup k t foldrWithKey f = go where go z t = case t of Tip -> z Bin _ kx x l r -> go (f kx x (go z r)) l toAscList = foldrWithKey (\k x xs -> (k,x):xs) [] getContents = isEOF >>= \b -> if b then pure [] else getChar >>= \c -> (c:) <$> getContents interact f = f <$> getContents >>= putStr abs x = if 0 <= x then x else 0 - x print = putStrLn . show class Alternative f where empty :: f a ; (<|>) :: f a -> f a -> f a instance Alternative Maybe where empty = Nothing ; l <|> r = maybe r Just l instance Alternative [] where empty = [] ; (<|>) = (++) guard False = empty guard True = pure () asum = foldr (<|>) empty intersperse _ [] = [] intersperse x (a:at) = a : foldr (\h t -> [x, h] ++ t) [] at otherwise = True unwords [] = "" unwords ws = foldr1 (\w s -> w ++ ' ':s) ws isSpace c = elem (ord c) [32, 9, 10, 11, 12, 13] span _ [] = ([], []) span p xs@(x:xt) | p x = first (x:) $ span p xt | otherwise = ([],xs) break p = span (not . p) dropWhile _ [] = [] dropWhile p xs@(x:xt) | p x = dropWhile p xt | otherwise = xs takeWhile _ [] = [] takeWhile p xs@(x:xt) | p x = x : takeWhile p xt | True = [] words s = case dropWhile isSpace s of "" -> [] s' -> w : words s'' where (w, s'') = break isSpace s' filter _ [] = [] filter p (x:xt) | p x = x : filter p xt | otherwise = filter p xt class Show a where showsPrec :: Int -> a -> String -> String showsPrec _ x = (show x++) show :: a -> String show x = shows x "" showList :: [a] -> String -> String showList = showList__ shows shows = showsPrec 0 showList__ _ [] s = "[]" ++ s showList__ showx (x:xs) s = '[' : showx x (showl xs) where showl [] = ']' : s showl (y:ys) = ',' : showx y (showl ys) showInt_ n | 0 == n = id | True = showInt_ (n`div`10) . (chr (48+n`mod`10):) instance Show a => Show [a] where showsPrec _ = showList instance Show Int where showsPrec _ n | 0 == n = ('0':) | 1 <= n = showInt_ n | True = ('-':) . showInt_ (0 - n) -- Fails for INT_MIN. showWord_ n | 0 == n = id | True = showWord_ (n`div`10) . (chr (48+(intFromWord $ n`mod`10)):) instance Show Word where showsPrec _ n | 0 == n = ('0':) | True = showWord_ n instance Show Char where showsPrec _ '\'' = ("'\\''"++) showsPrec _ c = ('\'':) . showLitChar c . ('\'':) showList s = ('"':) . foldr (.) id (map showLitChar s) . ('"':) instance (Show a, Show b) => Show (a, b) where showsPrec _ (a, b) = showParen True $ shows a . (',':) . shows b showLitChar '\n' = ("\\n"++) showLitChar c = (c:) showParen b f = if b then ('(':) . f . (')':) else f class Enum a where succ :: a -> a pred :: a -> a toEnum :: Int -> a fromEnum :: a -> Int enumFrom :: a -> [a] enumFrom = iterate succ enumFromTo :: a -> a -> [a] instance Enum Int where succ = (+1) pred = flip (-) 1 toEnum = id fromEnum = id enumFromTo lo hi = takeWhile (<= hi) $ enumFrom lo instance Enum Integer where succ = (+1) pred = flip (-) 1 toEnum = fromInt fromEnum (Integer xsgn xs) = intFromWord $ fst $ mpView xs enumFromTo lo hi = takeWhile (<= hi) $ enumFrom lo instance Enum Char where succ = chr . (+1) . ord pred = chr . (+(0-1)) . ord toEnum = chr fromEnum = ord enumFromTo lo hi = takeWhile (<= hi) $ enumFrom lo data Integer = Integer Bool [Word] instance Ring Integer where Integer xsgn xs + Integer ysgn ys | xsgn == ysgn = Integer xsgn $ mpAdd xs ys | True = case mpCompare xs ys of LT -> mpCanon ysgn $ mpSub ys xs _ -> mpCanon xsgn $ mpSub xs ys Integer xsgn xs - Integer ysgn ys | xsgn /= ysgn = Integer xsgn $ mpAdd xs ys | True = case mpCompare xs ys of LT -> mpCanon (not ysgn) $ mpSub ys xs _ -> mpCanon xsgn $ mpSub xs ys Integer xsgn xs * Integer ysgn ys = Integer (xsgn == ysgn) $ mpMul xs ys fromInt x | 0 <= x = Integer True $ if x == 0 then [] else [wordFromInt x] | True = Integer False [wordFromInt $ 0 - x] instance Integral Integer where -- TODO: Trucate `div` towards zero. div (Integer xsgn xs) (Integer ysgn ys) = mpCanon0 (xsgn == ysgn) $ fst $ mpDivMod xs ys mod (Integer xsgn xs) (Integer ysgn ys) = mpCanon0 ysgn $ snd $ mpDivMod xs ys quot (Integer xsgn xs) (Integer ysgn ys) = mpCanon0 (xsgn == ysgn) $ fst $ mpDivMod xs ys rem (Integer xsgn xs) (Integer ysgn ys) = mpCanon0 ysgn $ snd $ mpDivMod xs ys instance Eq Integer where Integer xsgn xs == Integer ysgn ys = xsgn == ysgn && xs == ys instance Ord Integer where compare (Integer xsgn xs) (Integer ysgn ys) | xsgn = if ysgn then mpCompare xs ys else GT | True = if ysgn then LT else mpCompare ys xs instance Show Integer where showsPrec _ (Integer xsgn xs) = (if xsgn then id else ('-':)) . mpBase 10 xs mpView [] = (0, []) mpView (x:xt) = (x, xt) mpCanon sgn xs = mpCanon0 sgn $ reverse $ dropWhile (0 ==) $ reverse xs mpCanon0 sgn xs = case xs of [] -> Integer True [] _ -> Integer sgn xs mpCompare [] [] = EQ mpCompare [] _ = LT mpCompare _ [] = GT mpCompare (x:xt) (y:yt) = case mpCompare xt yt of EQ -> compare x y o -> o mpAdc [] [] c = ([], c) mpAdc xs ys c = first (lo:) $ mpAdc xt yt hi where (x, xt) = mpView xs (y, yt) = mpView ys (lo,hi) = uncurry (word64Add c 0) $ word64Add x 0 y 0 mpAdd xs ys | c == 0 = zs | True = zs ++ [c] where (zs, c) = mpAdc xs ys 0 mpSub xs ys = fst $ mpSbb xs ys 0 mpSbb xs ys b = go xs ys b where go [] [] b = ([], b) go xs ys b = first (lo:) $ go xt yt $ 1 - hi where (x, xt) = mpView xs (y, yt) = mpView ys (lo,hi) = uncurry word64Sub (word64Sub x 1 y 0) b 0 mpMulWord _ [] c = if c == 0 then [] else [c] mpMulWord x (y:yt) c = lo:mpMulWord x yt hi where (lo, hi) = uncurry (word64Add c 0) $ word64Mul x 0 y 0 mpMul [] _ = [] mpMul (x:xt) ys = case mpMulWord x ys 0 of [] -> [] z:zs -> z:mpAdd zs (mpMul xt ys) mpDivModWord xs y = first (reverse . dropWhile (0 ==)) $ go 0 $ reverse xs where go r [] = ([], r) go n (x:xt) = first (q:) $ go r xt where q = fst $ word64Div x n y 0 r = fst $ word64Mod x n y 0 mpBase _ [] = ('0':) mpBase b xs = go xs where go [] = id go xs = go q . shows r where (q, r) = mpDivModWord xs b mpDivMod xs ys = first (reverse . dropWhile (== 0)) $ go us where s = mpDivScale $ last ys us = mpMulWord s (xs ++ [0]) 0 vs = mpMulWord s ys 0 (v1:_) = reverse vs vlen = length vs go us | ulen <= vlen = ([], fst $ mpDivModWord us s) | True = first (q:) $ go $ lsbs ++ init ds where ulen = length us (u0:u1:_) = reverse us (lsbs, msbs) = splitAt (ulen - vlen - 1) us (ql, qh) = word64Div u1 u0 v1 0 q0 = if 1 <= qh then (0-1) else ql (q, ds) = foldr const undefined [(q, ds) | q <- iterate (- 1) q0, let (ds, bor) = mpSbb msbs (mpMulWord q vs 0) 0, bor == 0] mpDivScale n = fst $ word64Div 0 1 (n + 1) 0

Program: 🌐 e ℙ ♛ Lindon ⍋ ⬢ Gray Hilbert Douady Enigma

Run Linkify

main = putStrLn "Hello, World!"

-- Digits of e. See http://miranda.org.uk/examples.
mkdigit n | n <= 9 = chr (n + ord '0')
norm c (d:e:x)
  | e `mod` c + 10 <= c = d + e  `div` c : e' `mod` c : x'
  | otherwise           = d + e' `div` c : e' `mod` c : x'
  where (e':x') = norm (c+1) (e:x)
convert x = mkdigit h:convert t
  where (h:t) = norm 2 (0:map (10*) x)
edigits = "2." ++ convert (repeat 1)
main = putStr $ take 1024 edigits

primes = sieve [2..]
sieve (p:x) = p : sieve [n | n <- x, n `mod` p /= 0]
main = print $ take 100 $ primes

-- Eight queens puzzle. See http://miranda.org.uk/examples.
safe q b = and[not $ q==p || abs(q-p)==i|(p,i) <- zip b [1..]]
queens sz = go sz where
  go 0 = [[]]
  go n = [q:b | b <- go (n - 1), q <- [1..sz], safe q b]
main = print $ queens 8

-- King, are you glad you are king?
main = interact $ unwords . reverse . words

main = interact $ unwords . sorta . words
sorta [] = []
sorta (x:xt) = sorta (filter (<= x) xt) ++ [x] ++ sorta (filter (> x) xt)

-- https://fivethirtyeight.com/features/can-you-escape-this-enchanted-maze/
maze = fromList $ concat $ zipWith row [0..]
  [ "."
  , "IF"
  , " BLUE"
  , "Z ASKS"
  , "AMY EE"
  , "DANCES"
  , " QUEEN"
  , "   Z O"
  , "     O"
  ]
  where
  row r s = concat $ zipWith (cell r) [0..] s
  cell r c x | x /= ' '  = [((r, c), x)]
             | otherwise = []
dirs = [(1, 0), (0, 0-1), (0-1, 0-1), (0-1, 0), (0, 1), (1, 1)]
turn f x = take 2 $ tail $ dropWhile (/= x) $ cycle $ f dirs
data Hex = Hex (Int, Int) (Int, Int) String
step (Hex (x, y) (xd, yd) path) =
  [Hex pos' (xd', yd') (c:path) | (xd', yd') <- next (xd, yd),
    let pos' = (x + xd', y + yd'), member pos' maze]
  where
  c = maze!(x, y)
  next = turn $ if elem c "AEIOUY" then id else reverse

bfs moves = case asum $ won <$> moves of
  Nothing -> bfs $ step =<< moves
  Just soln -> reverse soln
  where
  won (Hex pos _ path)
    | maze!pos == '.' && elem 'M' path = Just path
    | otherwise = Nothing

main = putStrLn $ bfs [Hex (5, 0) (1, 1) ""]

-- Gray code.
gray 0 = [""]
gray n = ('0':) <$> gray (n - 1) <|> reverse (('1':) <$> gray (n - 1))
main = putStrLn $ unwords $ gray 4

-- Theorem prover based on a Hilbert system.
-- https://crypto.stanford.edu/~blynn/compiler/hilsys.html
data Term = Var String | Fun String [Term]

data FO = Top | Bot | Atom String [Term]
  | Not FO | FO :/\ FO | FO :\/ FO | FO :==> FO | FO :<=> FO
  | Forall String FO | Exists String FO
data Theorem = Theorem FO
instance Eq Term where
  t1 == t2 = case t1 of
    Var s1 -> case t2 of
      Var s2 -> s1 == s2
      Fun _ _ -> False
    Fun f1 as1 -> case t2 of
      Var _ -> False
      Fun f2 as2 -> f1 == f2 && as1 == as2

instance Eq FO where  -- `deriving Eq` is sorely missed.
  Top == Top = True
  Bot == Bot = True
  (Atom s1 ts1) == (Atom s2 ts2) = s1 == s2 && ts1 == ts2
  (Not x1) == (Not x2) = x1 == x2
  (x1 :/\ y1) == (x2 :/\ y2) = x1 == x2 && y1 == y2
  (x1 :\/ y1) == (x2 :\/ y2) = x1 == x2 && y1 == y2
  (x1 :==> y1) == (x2 :==> y2) = x1 == x2 && y1 == y2
  (x1 :<=> y1) == (x2 :<=> y2) = x1 == x2 && y1 == y2
  (Forall s1 f1) == (Forall s2 f2) = s1 == s2 && f1 == f2
  (Exists s1 f1) == (Exists s2 f2) = s1 == s2 && f1 == f2
  _ == _ = False

instance Show Term where
  showsPrec _ = \case
    Var s -> (s ++)
    Fun s ts -> (s ++) . showParen (not $ null ts)
      (foldr (.) id $ intersperse (", "++) $ map shows ts)

instance Show FO where
  showsPrec p = \case
    Top -> ('1':)
    Bot -> ('0':)
    Atom s ts -> shows $ Fun s ts
    Not x -> ('~':) . showsPrec 4 x
    x :/\ y -> showParen (p > 3) $ showsPrec 3 x . (" /\\ " ++) . showsPrec 3 y
    x :\/ y -> showParen (p > 2) $ showsPrec 2 x . (" \\/ " ++) . showsPrec 2 y
    x :==> y -> showParen (p > 1) $ showsPrec 2 x . (" ==> " ++) . showsPrec 1 y
    x :<=> y -> showParen (p > 1) $ showsPrec 2 x . (" <=> " ++) . showsPrec 1 y
    Forall s x -> showParen (p > 0) $ ("forall " ++) . (s++) . (". "++) . showsPrec 0 x
    Exists s x -> showParen (p > 0) $ ("exists " ++) . (s++) . (". "++) . showsPrec 0 x
occurs s t = s == t || case t of
  Var _ -> False
  Fun _ args -> any (occurs s) args
isFree t = \case
  Top -> False
  Bot -> False
  Atom _ ts -> any (occurs t) ts
  Not x -> isFree t x
  x :/\ y -> isFree t x || isFree t y
  x :\/ y -> isFree t x || isFree t y
  x :==> y -> isFree t x || isFree t y
  x :<=> y -> isFree t x || isFree t y
  Forall v x -> not (occurs (Var v) t) && isFree t x
  Exists v x -> not (occurs (Var v) t) && isFree t x
s =: t = Atom "=" [s, t]
ponens (Theorem (p :==> q)) (Theorem p') | p == p' = Theorem q
gen x (Theorem t) = Theorem $ Forall x t
axiomK p q        = Theorem $ p :==> (q :==> p)
axiomS p q r      = Theorem $ (p :==> (q :==> r)) :==> ((p :==> q) :==> (p :==> r))
axiomLEM p        = Theorem $ ((p :==> Bot) :==> Bot) :==> p
axiomAllImp x p q = Theorem $ Forall x (p :==> q) :==> (Forall x p :==> Forall x q)
axiomImpAll x p | isFree (Var x) p = Theorem $ p :==> Forall x p
axiomExEq x t | occurs (Var x) t = Theorem $ Exists x $ Var x =: t
axiomRefl t       = Theorem $ t =: t
axiomFunCong  f ls rs = Theorem $ foldr (:==>) (Fun f ls =: Fun f rs) $ zipWith (=:) ls rs
axiomPredCong p ls rs = Theorem $ foldr (:==>) (Atom p ls :==> Atom p rs) $ zipWith (=:) ls rs
axiomIffImp1 p q = Theorem $ (p :<=> q) :==> (p :==> q)
axiomIffImp2 p q = Theorem $ (p :<=> q) :==> (q :==> p)
axiomImpIff p q  = Theorem $ (p :==> q) :==> ((q :==> p) :==> (p :<=> q))
axiomTrue        = Theorem $ Top :<=> (Bot :==> Bot)
axiomNot p       = Theorem $ Not p :<=> (p :==> Bot)
axiomAnd p q     = Theorem $ (p :/\ q) :<=> ((p :==> (q :==> Bot)) :==> Bot)
axiomOr p q      = Theorem $ (p :\/ q) :<=> Not (Not p :/\ Not q)
axiomExists x p  = Theorem $ Exists x p :<=> Not (Forall x $ Not p)
-- |-  p ==> p
impRefl p = ponens (ponens
  (axiomS p (p :==> p) p)
  (axiomK p $ p :==> p))
  (axiomK p p)

-- |- p ==> p ==> q  /  |- p ==> q
impDedup th@(Theorem (p :==> (_ :==> q))) = ponens (ponens (axiomS p p q) th) (impRefl p)

-- |- q  /  |- p ==> q
addAssum p th@(Theorem f) = ponens (axiomK f p) th

-- |- q ==> r  /  |- (p ==> q) ==> (p ==> r)
impAddAssum p th@(Theorem (q :==> r)) = ponens (axiomS p q r) (addAssum p th)

-- |- p ==> q  |- q ==> r  /  |- p ==> r
impTrans th1@(Theorem (p :==> _)) th2 = ponens (impAddAssum p th2) th1

-- |- p ==> r  /  |- p ==> q ==> r
impInsert q th@(Theorem (p :==> r)) = impTrans th (axiomK r q)

-- |- p ==> q ==> r  /  |- q ==> p ==> r
impSwap th@(Theorem (p :==> (q :==> r))) = impTrans (axiomK q p) $ ponens (axiomS p q r) th

-- |- (q ==> r) ==> (p ==> q) ==> (p ==> r)
impTransTh p q r = impTrans (axiomK (q :==> r) p) (axiomS p q r)

-- |- p ==> q  /  |- (p ==> r) ==> (q ==> r)
impAddConcl r th@(Theorem (p :==> q)) = ponens (impSwap (impTransTh p q r)) th

-- |- (p ==> q ==> r) ==> (q ==> p ==> r)
impSwapTh p q r = impTrans (axiomS p q r) $ impAddConcl (p :==> r) $ axiomK q p

-- |- (p ==> q ==> r) ==> (s ==> t ==> u)  /  |- (q ==> p ==> r) ==> (t ==> s ==> u)
impSwap2 th@(Theorem ((p :==> (q :==> r)) :==> (s :==> (t :==> u))))
  = impTrans (impSwapTh q p r) (impTrans th (impSwapTh s t u))

-- |- p ==> q ==> r  |- p ==> q  /  |- p ==> r
rightMP ith th = impDedup (impTrans th (impSwap ith))

-- |- p <=> q  /  |- p ==> q
iffImp1 th@(Theorem (p :<=> q)) = ponens (axiomIffImp1 p q) th

-- |- p <=> q  /  |- q ==> p
iffImp2 th@(Theorem (p :<=> q)) = ponens (axiomIffImp2 p q) th

-- |- p ==> q  |- q ==> p  /  |- p <=> q
impAntisym th1@(Theorem (p :==> q)) th2 = ponens (ponens (axiomImpIff p q) th1) th2

-- |- p ==> (q ==> 0) ==> 0  /  |- p ==> q
rightDoubleNeg th@(Theorem (p :==> ((_ :==> Bot) :==> Bot))) = impTrans th $ axiomLEM p

-- |- 0 ==> p
exFalso p = rightDoubleNeg $ axiomK Bot (p :==> Bot)

-- |- 1
truth = ponens (iffImp2 axiomTrue) (impRefl Bot)

-- |- s = t ==> t = s
eqSym s t = let
  rth = axiomRefl s
  f th = ponens (impSwap th) rth
  in f $ f $ axiomPredCong "=" [s, s] [t, s]

-- |- s = t ==> t = u ==> s = u
eqTrans s t u = let
  th1 = axiomPredCong "=" [t, u] [s, u]
  th2 = ponens (impSwap th1) (axiomRefl u)
  in impTrans (eqSym s t) th2

examples =
  [ axiomOr (Atom "x" []) (Atom "y" [])
  , impTransTh (Atom "Foo" []) (Atom "Bar" []) (Atom "Baz" [])
  , eqSym (Var "a") (Var "b")
  , eqTrans (Var "x") (Var "y") (Var "z")
  ]

concl (Theorem t) = t
main = mapM_ (putStr . flip shows "\n" . concl) examples

-- Based on https://sametwice.com/4_line_mandelbrot.
prec = 16384
infixl 7 #
x # y = x * y `div` prec
sqAdd (x, y) (a, b) = (a#a - b#b + x, 2*(a#b) + y)
norm (x, y) = x#x + y#y
douady p = null . dropWhile (\z -> norm z < 4*prec) . take 30 $ iterate (sqAdd p) (0, 0)
main = putStr $ unlines
  [[if douady (616*x - 2*prec, 1502*y - 18022)
    then '*' else ' ' | x <- [0..79]] | y <- [0..23]]

-- https://crypto.stanford.edu/~blynn/haskell/enigma.html
wI   = ("EKMFLGDQVZNTOWYHXUSPAIBRCJ", "Q")
wII  = ("AJDKSIRUXBLHWTMCQGZNPYFVOE", "E")
wIII = ("BDFHJLCPRTXVZNYEIWGAKMUSQO", "V")
wIV  = ("ESOVPZJAYQUIRHXLNFTGKDCMWB", "J")
wV   = ("VZBRGITYUPSDNHLXAWMJQOFECK", "Z")
ukwA = "EJMZALYXVBWFCRQUONTSPIKHGD"
ukwB = "YRUHQSLDPXNGOKMIEBFZCWVJAT"
ukwC = "FVPJIAOYEDRZXWGCTKUQSBNMHL"

abc = ['A'..'Z']
abc2 = abc ++ abc
sub p x   = maybe x id $ lookup x $ zip abc p
unsub p x = maybe x id $ lookup x $ zip p abc
shift k   = sub   $ dropWhile (/= k) $ abc2
unshift k = unsub $ dropWhile (/= k) $ abc2
conjugateSub p k = unshift k . sub p . shift k
rotorSubs gs = zipWith conjugateSub (fst <$> rotors) gs
rotors = [wI, wII, wIII]
zap gs = unsub p . sub ukwB . sub p where
  p = foldr1 (.) (rotorSubs gs) <$> abc
turn gs@[_, g2, g3] = zipWith (bool id $ shift 'B') bs gs where
  [_, n2, n3] = snd <$> rotors
  bs = [g2 `elem` n2, g2 `elem` n2 || g3 `elem` n3, True]
enigma grundstellung = zipWith zap $ tail $ iterate turn grundstellung
main = interact $ enigma "AAA"