module Exercise_9 where
  {-WETT-}

  type Name = String
  type Valuation = [(Name,Bool)]

  data Atom = T | Var Name
    deriving (Eq, Show)
  
  data Literal = Pos Atom | Neg Atom
    deriving (Eq, Show)
    -- e.g.: Pos $ Var "v1"      top     bottom
  
  data Form = L Literal | Form :&: Form | Form :|: Form
    deriving (Eq, Show)
    -- e.g.: (L (Pos (Var "v1")) :|: (Neg (Var "v2"))) :&: (L (Neg (Var "v1")) :|: L top) 
  
  type Clause = [Literal]
    -- e.g.: [Pos $ Var "v1", Neg $ Var "v2"]
  type ConjForm = [Clause]
    -- e.g.: [ [Pos $ Var "v1", Neg $ Var "v2"]  ,  [Neg $ Var "v1"] ]

-- Form = arbitrary formula (not necessarily in CNF!!!)   
-- disjunctive normal form      OR = v      DNF = (a AND b AND c) v (d AND e AND a AND b)
-- conjunctive normal form      AND         CNF = (a v b v c) AND (d v e v a v b)


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


  {-T9.3.3-}
  conjToForm :: ConjForm -> Form
  conjToForm [] = L top -- weil 'True' das neutrale Element für AND ist (verändert nichts)
  conjToForm ds = foldr ((:&:) . clauseToForm) (clauseToForm $ last ds) (init ds)

  clauseToForm :: Clause -> Form
  clauseToForm [] = L bottom -- weil 'False' das neutrale Element für OR ist (verändert nichts)
  clauseToForm ls = foldr ((:|:) . L) (L $ last ls) (init ls)

  
  {-T9.3.4-}
  substConj :: Valuation -> ConjForm -> ConjForm
  substConj = map . substClause
    
  substClause :: Valuation -> Clause -> Clause
  substClause = map . substLiteral

  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

  

  {-H9.2.1-}
  simpConj :: ConjForm -> ConjForm
  simpConj [] = []
  simpConj [[]] = [[]]
  simpConj (c:cs) =
    let
      simp1 = map help_simpClauseStart (c:cs)     -- simplified to '[top]' if containing one 'top' and removed every 'bottom'
      simp2 = help_simpConjForm simp1 []          -- removes every clause '[top]' and simplifies whole formula to [[]] if it contains an empty clause
    in
      simp2

  help_simpClauseStart c = help_simpClause c []
  help_simpClause :: Clause -> Clause -> Clause
  help_simpClause [] acc = acc
  help_simpClause (literal:ls) acc
      | literal == top      = help_simpClause [] [top]
      | literal == bottom   = help_simpClause ls acc
      | otherwise           = help_simpClause ls (acc ++ [literal])

  help_simpConjForm :: ConjForm -> ConjForm -> ConjForm
  help_simpConjForm [] acc = acc
  help_simpConjForm (c:cs) acc
      | c == []       = help_simpConjForm [] [[]]
      | c == [top]    = help_simpConjForm cs acc
      | otherwise     = help_simpConjForm cs (acc ++ [c])



  {-H9.2.2-}
  cnf :: Form -> ConjForm
  cnf (L a) = [[a]]
  cnf (a:&:b) = cnf a ++ cnf b
  cnf (a:|:b) = [ xs ++ ys | xs <- (cnf a), ys <- (cnf b) ] -- using list comprehension to return the cross product



  {-H9.2.3-}
  selectV :: ConjForm -> Maybe (Name, Bool)
  selectV conjF =
    case help_any_var conjF of
      Nothing -> Nothing
      Just n -> Just (n,True)


  -- returns 'Nothing' if 'conjF' contains no variables (= empty or only 'bottom' / 'top') and one variable otherwise
  help_any_var :: ConjForm -> Maybe (Name)
  help_any_var [] = Nothing
  help_any_var [[]] = Nothing
  help_any_var (xs:xss) =
    case help_search_clause xs of -- xs = clause
      Nothing -> help_any_var xss
      Just n -> Just n

  -- checks one 'Clause' for variables and returns the first it can find or 'Nothing' otherwise
  help_search_clause :: Clause -> Maybe (Name) 
  help_search_clause [] = Nothing
  help_search_clause ((Pos (Var n)) :xs) = Just n
  help_search_clause ((Neg (Var n)) :xs) = Just n
  help_search_clause (_:xs) = help_search_clause xs



  {-H9.2.5-}
  -- compare with the pseudo-code given on the Exercise-Sheet for easier understanding
  satConj :: ConjForm -> Maybe Valuation
  satConj [] = Just []
  satConj [[]] = Nothing
  satConj conjF = help_satConj conjF []

  help_satConj :: ConjForm -> Valuation -> Maybe Valuation
  help_satConj conjF acc =
    let
      simp_cnf = simpConj conjF -- 'simp_cnf' is the simplified conjF
      contains_emptyClause = or (map (==[]) simp_cnf)
    in  
      if simp_cnf == [] -- given cnf is solvable
      then Just acc
      else
        if contains_emptyClause -- given cnf is not solvable
        then Nothing
        else 
          case selectV simp_cnf of
            Nothing -> error "this case should never occur, because 'selectV' has to find a variable after 'simpConj' has been applied ('simpConj' would have simplified the cnf to [] / [[]] if there were no variables left)"
            Just (n,b) -> 
              let
                acc_T = (n,b) : acc
                subst_cnf_T = substConj acc_T simp_cnf -- assigns 'True' to the selected variable 'n', thus subsitutes all 'n's in the 'simp_cnf' with 'True'
                acc_F = (n, not b) : acc
                subst_cnf_F = substConj acc_F simp_cnf -- assigns 'False' to the selected variable 'n', thus subsitutes all 'n's in the 'simp_cnf' with 'False'
              in
                case help_satConj subst_cnf_T acc_T of -- recursive call with 'new' substituted cnf ('True')
                  Just res -> Just res
                  Nothing -> 
                    case help_satConj subst_cnf_F acc_F of -- recursive call with 'new' substituted cnf ('False')
                      Just res -> Just res
                      Nothing -> Nothing



  {-H9.2.6-}
  sat :: Form -> Maybe Valuation
  sat formula = satConj (cnf formula)



  {-TTEW-}