- {-# 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))
Undefined
By: Guest | Date: Feb 15 2014 12:06 | Format: None | Expires: never | Size: 3.49 KB | Hits: 915
Latest pastes
1 days ago
1 days ago
2 days ago
4 days ago
5 days ago