{-# LANGUAGE TupleSections #-}
{-# LANGUAGE LambdaCase #-}
module Exercise_9 where
{- WETT -}

import Control.Applicative
import Control.Monad
import Data.List
import Data.Maybe
import Data.Function
import qualified Data.IntMap.Strict as IntMap
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set

type Name = String
type Valuation = [(Name,Bool)]
data Atom = T | Var Name
  deriving (Eq, Show)
data Literal = Pos Atom | Neg Atom
  deriving (Eq, Show)
data Form = L Literal | Form :&: Form | Form :|: Form
  deriving (Eq, Show)
type Clause = [Literal]
type ConjForm = [Clause]

lmap :: (Atom -> Atom) -> (Literal -> Literal)
lmap f (Pos a) = Pos (f a)
lmap f (Neg a) = Neg (f a)

{-T9.3.2-}
top :: Literal
top = Pos T

bottom :: Literal
bottom = Neg T

{-T9.3.3-}
clauseToForm :: Clause -> Form
clauseToForm [] = L bottom
clauseToForm ls = foldr ((:|:) . L) (L $ last ls) (init ls)

conjToForm :: ConjForm -> Form
conjToForm [] = L top
conjToForm ds = foldr ((:&:) . clauseToForm) (clauseToForm $ last ds) (init ds)

{-T9.3.4-}
substLiteral :: Valuation -> Literal -> Literal
substLiteral v l@(Pos (Var n)) = case lookup n v of
  Just b -> if b then top else bottom
  Nothing -> l
substLiteral v l@(Neg (Var n)) = case lookup n v of
  Just b -> if b then bottom else top
  Nothing -> l
substLiteral v l = l

substClause :: Valuation -> Clause -> Clause
substClause = map . substLiteral

substConj :: Valuation -> ConjForm -> ConjForm
substConj = map . substClause

{-H9.2.1-}

simpClause :: Clause -> Clause
simpClause c =
  if top `elem` c then [top]
  else filter (/= bottom) c


simpConj :: ConjForm -> ConjForm
simpConj cs =
  if null `any` simpChildren then pure []
  else filter (/= [top]) simpChildren
  where simpChildren = simpClause <$> cs

{-H9.2.2-}
cnf :: Form -> ConjForm
cnf (L l) = pure [l]
cnf (a :|: b) = [ ai ++ bi | ai <- cnf a, bi <- cnf b ]
cnf (a :&: b) = cnf a ++ cnf b

{-H9.2.3-}

getAtom :: Literal -> Maybe (Name, Bool)
getAtom (Pos (Var b)) = Just (b, True)
getAtom (Neg (Var b)) = Just (b, False)
getAtom _ = Nothing

selectVUnit :: Clause -> Maybe (Name, Bool)
selectVUnit [x] = getAtom x
selectVUnit _ = Nothing

selectVPure :: ConjForm -> Maybe (Name, Bool)
selectVPure cs = (fmap (, True) $ listToMaybe (true \\ false))
             <|> (fmap (, False) $ listToMaybe (false \\ true))
  where literals = nub $ catMaybes $ map getAtom $ concat cs
        true = map fst $ filter snd $ literals
        false = map fst $ filter (not . snd) $ literals

selectV :: ConjForm -> Maybe (Name, Bool)
selectV cs = msum (selectVUnit <$> cs) <|> selectVPure cs

{-H9.2.4-}


-- this really isn't a good solution, but judging by some previous weeks,
-- I think there's a good chance these are free points. Welp ¯\_(ツ)_/¯

cfrom :: Bool -> Literal
cfrom True = Pos T
cfrom False = Neg T

getSatVar :: Literal -> Maybe (String, Bool)
getSatVar (Pos T) = Nothing
getSatVar (Neg T) = Nothing
getSatVar (Pos (Var v)) = Just (v, True)
getSatVar (Neg (Var v)) = Just (v, False)


findPLR :: ConjForm -> [(String, Bool)]
findPLR c = fmap (\(l, r) -> (l, fromJust r)) $ filter (isJust . snd) $ Map.toList digested
  where digested = foldl' (flip updater) Map.empty (catMaybes $ getSatVar <$> concat c)
        updater :: (String, Bool) -> Map.Map String (Maybe Bool) -> Map.Map String (Maybe Bool)
        updater (var, val) = Map.alter (
            \case Just (Just val') ->
                     if val == val'
                     then (Just (Just val))
                     else (Just Nothing)         -- on conflict set to explicit Nothing
                  Just Nothing -> Just Nothing   -- ... which captures
                  Nothing -> Just (Just val)) var

applyClause :: Valuation -> Clause -> Clause
applyClause vals = map (
  \case Pos a -> (case a of T -> Pos T
                            Var v -> Pos (Var v) `fromMaybe` (cfrom <$> lookup v vals))
        Neg a -> (case a of T -> Neg T
                            Var v -> Neg (Var v) `fromMaybe` ((cfrom . not) <$> lookup v vals))
  )

apply :: Valuation -> ConjForm -> ConjForm
apply v = map (applyClause v)

satConjWith :: Valuation -> ConjForm -> Maybe Valuation
satConjWith v f =
  if null f then Just v
  else if f == [[]] then Nothing
  else msum (map (\o -> satConjWith (o:v) (simpConj $ apply [o] f)) (fromJust choices))
  where -- One-Literal rule: If a clause has one literal, we must satisfy it.
        anyOLR = fmap pure $ msum $ map (getSatVar . head) $ filter (\x -> length x == 1) f

        -- Pure-Literal rule: If a variable only one “sort” of occurrence, we can safely set it that way.
        anyPLR = fmap pure $ listToMaybe $ findPLR f

        -- “Two-Literal rule”: case distinction over (a :|: b), since these
        -- intuitively seem to lead to huge search space reductions.
        anyTLR = fmap (\a -> [(a, True), (a, False)])
                 $ msum $ map (fmap fst . getSatVar . head) $ filter (\x -> length x == 2) f

        -- Just get a variable from somewhere.
        fallback = fmap (\a -> [(a, True), (a, False)])
                   $ msum $ map (fmap fst . getSatVar) $ concat f

        choices = msum [anyOLR, anyPLR, anyTLR, fallback]


satConj :: ConjForm -> Maybe Valuation
satConj v
  | null v' = Just [] -- we want to simplify _before_ recursing down, so we
                      -- have to do it in the “outermost” case too
  | otherwise = satConjWith [] v'
  where v' = simpConj v

sat :: Form -> Maybe Valuation
sat = satConj . cnf


{- TTEW -}