{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, IncoherentInstances, DeriveFunctor, StandaloneDeriving  #-}

 

module Ex12_QBF1 where

import Data.List

 

-------- Aufgabe 1 --------

 

data BConst x = BConst Bool

data BConj x = BConj (BExp x) (BExp x)

data BNeg x = BNeg (BExp x)

data BVar x = BVar [Char]

data BForall x = BForall (BExp x) (BExp x)

 

class BExp x where

    evalBExpAlg :: Algebra BExp Bool

 

instance BExp BConst where

    evalBExpAlg (BConst x) = x

instance BExp BConj where

    evalBExpAlg (BConj x1 x2) = (evalBExpAlg x1) && (evalBExpAlg x2)

instance BExp BNeg where

    evalBExpAlg (BNeg x) = not (evalBExpAlg x)

instance BExp BVar where

    evalBExpAlg (BVar x) = undefined

instance BExp BForall where

    evalBExpAlg (BForall x1 x2) = evalBExpVar x1 x2

 

--data BExp x = BConst Bool | BConj (BExp x) (BExp x) | BNeg (BExp x) | BVar [Char] | BForall (BExp x) (BExp x)

--deriving instance Show x => Show (BExp x)

--deriving instance Eq x => Eq (BExp x)

 

 

--instance Functor BExp where

--    fmap f (BConst b) = BConst b

--    fmap f (BConj x1 x2) = BConj (f (evalBExpAlg x1)) (f (evalBExpAlg x2))

--    fmap f (BVar x) = BVar (f x)

--    fmap f (BNeg x) = BNeg (f (evalBExpAlg x))

 

type Algebra f a = f a -> a

 

--evalBExpAlg :: Algebra BExp Bool

--evalBExpAlg (BConst x) = x

--evalBExpAlg (BConj x1 x2) = (evalBExpAlg x1) && (evalBExpAlg x2)

--evalBExpAlg (BNeg x) = not (evalBExpAlg x)

--evalBExpAlg (BVar x) = undefined--lookupVar x

--evalBExpAlg (BForall x1 x2) = evalBExpVar x1 x2

 

subExpList :: (BExp x) -> [BExp x]

subExpList (BConst x) = [BConst x]

subExpList (BVar x) = [BVar x]

subExpList (BConj x y) = [BConj x y]++(subExpList x)++(subExpList y)

subExpList (BNeg x) = [BNeg x]++(subExpList x)

 

expListContains :: [BExp x] -> (BExp x) -> Bool

expListContains [] _ = False

expListContains [BVar x] (BVar y) = if x == y then True else False

expListContains ((BVar x):xs) (BVar y) | x == y = True

                                    | otherwise = expListContains xs (BVar y)

 

-- Unfortunately doesn't work: "Couldn't match type 'x' with 'Bool'. 'x' is a rigid type variable..."

evalBExpVar :: (BExp x) -> (BExp x) -> Bool

evalBExpVar (BVar x1) x2 | expContains x2 (BVar x1) = undefined --evalBExpAlg (replaceVar x2 (BVar x1) (BConst True)) && evalBExpAlg (replaceVar x2 (BVar x1) (BConst False))

 

expContains :: BExp x -> BExp x -> Bool

expContains (BConst x) (BConst y ) = if x == y then True else False

expContains (BVar x) (BVar y ) = if x == y then True else False

expContains (BNeg x) (BNeg y) = expContains x y

expContains (BConj x1 x2) (BConj y1 y2) = (expContains x1 y1) && (expContains x2 y2)

expContains (BForall x1 x2) (BForall y1 y2) = (expContains x1 y1) && (expContains x2 y2)

expContains x y = expContains (nextSubExp x 1) (nextSubExp y 1) && expContains (nextSubExp x 2) (nextSubExp y 2) -- not the same expression type at top level

 

nextSubExp :: (BExp x) -> Int -> (BExp x)

nextSubExp (BConst x) _ = (BConst x)

nextSubExp (BVar x) _ = (BVar x)

nextSubExp (BNeg x) _ = x

nextSubExp (BConj x1 x2) 1 = x1

nextSubExp (BConj x1 x2) 2 = x2

nextSubExp (BForall x1 x2) 1 = x1

nextSubExp (BForall x1 x2) 2 = x2

 

replaceVar :: (BExp x) -> (BExp x) -> (BExp Bool) -> (BExp x)

replaceVar x (BVar y) (BConst z) = undefined

 

 

testExp = BNeg (BConj (BConj (BConst True) (BConst False)) (BConj (BConst False) (BConst False)))

testExp2 = BForall (BVar "x1") (BConj (BConst False) (BConst True))