{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
module Lab11 where

import           Control.Monad.State            ( State
                                                , evalState
                                                , state
                                                )
import           Data.Foldable                  ( toList )
import           Data.Maybe                     ( fromMaybe )
import           Prelude                 hiding ( lookup )

lookup :: Eq a => [(a, b)] -> a -> Maybe b
lookup [] _ = Nothing
lookup ((key, val) : xs) n | key == n  = Just val
                           | otherwise = lookup xs n

toCamelCaseF :: Functor f => f String -> f String
toCamelCaseF = fmap toCamelCase
 where
  toCamelCase :: String -> String
  toCamelCase = concat . map toUpperHead . words
  toUpperHead :: String -> String
  toUpperHead = \case
    ""      -> ""
    (h : t) -> toUpper h : t
  toUpper :: Char -> Char
  toUpper c = fromMaybe c (lookup upperRegistry c)
  upperRegistry :: [(Char, Char)]
  upperRegistry = zip ['a' .. 'z'] ['A' .. 'Z']

data DFA a = Automaton
  { dfaTransit :: a -> Char -> a
  , dfaInit    :: a
  , dfaFinal   :: a -> Bool
  }

evalDFA :: DFA a -> String -> (a, Bool)
evalDFA auto input = go input (dfaInit auto)
 where
  go []       state = (state, dfaFinal auto state)
  go (c : cs) state = go cs (dfaTransit auto state c)

data FloatStates = Before | Digit | Dot | First | Second | Fail

floatDfa :: DFA (Integer, Int, FloatStates)
floatDfa = Automaton
  { dfaTransit = transit
  , dfaInit    = (0, 0, Before)
  , dfaFinal   = \case
                   (_, _, Second) -> True
                   _              -> False
  }
 where
  digitRegistry = zip ['0' .. '9'] [0 .. 9]
  transit (start, exp, Before) c = case lookup digitRegistry c of
    Just v  -> (v, exp, Digit)
    Nothing -> (start, exp, Fail)
  transit (prev, exp, Digit) c = case lookup digitRegistry c of
    Just v  -> (prev * 10 + v, exp, Digit)
    Nothing -> if c == '.' then (prev, exp, Dot) else (prev, exp, Fail)
  transit (prev, exp, Dot) c = case lookup digitRegistry c of
    Just v  -> (prev * 10 + v, exp + 1, First)
    Nothing -> (prev, exp, Fail)
  transit (prev, exp, First) c = case lookup digitRegistry c of
    Just v  -> (prev * 10 + v, exp + 1, Second)
    Nothing -> (prev, exp, Fail)
  transit (prev, exp, Second) _ = (prev, exp, Fail)
  transit s                   _ = s

parseNum :: String -> Maybe Float
parseNum s = case evalDFA floatDfa s of
  ((val, exp, _), True) -> Just (fromInteger val / (10 ^ exp))
  _                     -> Nothing

parseNumF :: Functor f => f String -> f (Maybe Float)
parseNumF = fmap parseNum

parseIO :: IO ()
parseIO = putStrLn "Enter number:" >> parseNumF getLine >>= maybe parseIO print

{- TASKS -}

data Expr a
  = Atom a
  | Neg (Expr a)
  | And (Expr a) (Expr a)
  | Or (Expr a) (Expr a)
  deriving (Eq, Show, Functor, Foldable, Traversable)

eval :: Expr Bool -> Bool
eval (Atom b   ) = b
eval (Neg  e   ) = not (eval e)
eval (And e1 e2) = eval e1 && eval e2
eval (Or  e1 e2) = eval e1 || eval e2

subst :: Functor f => [String] -> f String -> f Bool
subst truths = fmap (`elem` truths)

-- for fun
genNames :: Expr () -> Expr String
genNames = flip evalState 0 . traverse bump where
  bump :: () -> State Integer String
  bump _ = state (\i -> (show i, i + 1))

fle :: Expr String
fle = And (Or (Neg (Atom "x")) (Atom "x")) (Atom "y")

subseqs :: [a] -> [[a]]
subseqs []       = [[]]
subseqs (x : xs) = subseqs xs ++ [ x : ys | ys <- subseqs xs ]

getAtoms :: Expr a -> [a]
getAtoms = toList

isTaut :: Expr String -> Bool
isTaut e = all (eval . flip subst e) . subseqs . getAtoms $ e

isSat :: Expr String -> Bool
isSat e = any (eval . flip subst e) . subseqs . getAtoms $ e
