Public paste
Undefined
By: Guest | Date: Feb 15 2014 12:06 | Format: None | Expires: never | Size: 3.49 KB | Hits: 915

  1. {-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, IncoherentInstances, DeriveFunctor, StandaloneDeriving  #-}
  2.  
  3. module Ex12_QBF1 where
  4. import Data.List
  5.  
  6. -------- Aufgabe 1 --------
  7.  
  8. data BConst x = BConst Bool
  9. data BConj x = BConj (BExp x) (BExp x)
  10. data BNeg x = BNeg (BExp x)
  11. data BVar x = BVar [Char]
  12. data BForall x = BForall (BExp x) (BExp x)
  13.  
  14. class BExp x where
  15.     evalBExpAlg :: Algebra BExp Bool
  16.  
  17. instance BExp BConst where
  18.     evalBExpAlg (BConst x) = x
  19. instance BExp BConj where
  20.     evalBExpAlg (BConj x1 x2) = (evalBExpAlg x1) && (evalBExpAlg x2)
  21. instance BExp BNeg where
  22.     evalBExpAlg (BNeg x) = not (evalBExpAlg x)
  23. instance BExp BVar where
  24.     evalBExpAlg (BVar x) = undefined
  25. instance BExp BForall where
  26.     evalBExpAlg (BForall x1 x2) = evalBExpVar x1 x2
  27.  
  28. --data BExp x = BConst Bool | BConj (BExp x) (BExp x) | BNeg (BExp x) | BVar [Char] | BForall (BExp x) (BExp x)
  29. --deriving instance Show x => Show (BExp x)
  30. --deriving instance Eq x => Eq (BExp x)
  31.  
  32.  
  33. --instance Functor BExp where
  34. --    fmap f (BConst b) = BConst b
  35. --    fmap f (BConj x1 x2) = BConj (f (evalBExpAlg x1)) (f (evalBExpAlg x2))
  36. --    fmap f (BVar x) = BVar (f x)
  37. --    fmap f (BNeg x) = BNeg (f (evalBExpAlg x))
  38.  
  39. type Algebra f a = f a -> a
  40.  
  41. --evalBExpAlg :: Algebra BExp Bool
  42. --evalBExpAlg (BConst x) = x
  43. --evalBExpAlg (BConj x1 x2) = (evalBExpAlg x1) && (evalBExpAlg x2)
  44. --evalBExpAlg (BNeg x) = not (evalBExpAlg x)
  45. --evalBExpAlg (BVar x) = undefined--lookupVar x
  46. --evalBExpAlg (BForall x1 x2) = evalBExpVar x1 x2
  47.  
  48. subExpList :: (BExp x) -> [BExp x]
  49. subExpList (BConst x) = [BConst x]
  50. subExpList (BVar x) = [BVar x]
  51. subExpList (BConj x y) = [BConj x y]++(subExpList x)++(subExpList y)
  52. subExpList (BNeg x) = [BNeg x]++(subExpList x)
  53.  
  54. expListContains :: [BExp x] -> (BExp x) -> Bool
  55. expListContains [] _ = False
  56. expListContains [BVar x] (BVar y) = if x == y then True else False
  57. expListContains ((BVar x):xs) (BVar y) | x == y = True
  58.                                     | otherwise = expListContains xs (BVar y)
  59.  
  60. -- Unfortunately doesn't work: "Couldn't match type 'x' with 'Bool'. 'x' is a rigid type variable..."
  61. evalBExpVar :: (BExp x) -> (BExp x) -> Bool
  62. evalBExpVar (BVar x1) x2 | expContains x2 (BVar x1) = undefined --evalBExpAlg (replaceVar x2 (BVar x1) (BConst True)) && evalBExpAlg (replaceVar x2 (BVar x1) (BConst False))
  63.  
  64. expContains :: BExp x -> BExp x -> Bool
  65. expContains (BConst x) (BConst y ) = if x == y then True else False
  66. expContains (BVar x) (BVar y ) = if x == y then True else False
  67. expContains (BNeg x) (BNeg y) = expContains x y
  68. expContains (BConj x1 x2) (BConj y1 y2) = (expContains x1 y1) && (expContains x2 y2)
  69. expContains (BForall x1 x2) (BForall y1 y2) = (expContains x1 y1) && (expContains x2 y2)
  70. 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
  71.  
  72. nextSubExp :: (BExp x) -> Int -> (BExp x)
  73. nextSubExp (BConst x) _ = (BConst x)
  74. nextSubExp (BVar x) _ = (BVar x)
  75. nextSubExp (BNeg x) _ = x
  76. nextSubExp (BConj x1 x2) 1 = x1
  77. nextSubExp (BConj x1 x2) 2 = x2
  78. nextSubExp (BForall x1 x2) 1 = x1
  79. nextSubExp (BForall x1 x2) 2 = x2
  80.  
  81. replaceVar :: (BExp x) -> (BExp x) -> (BExp Bool) -> (BExp x)
  82. replaceVar x (BVar y) (BConst z) = undefined
  83.  
  84.  
  85. testExp = BNeg (BConj (BConj (BConst True) (BConst False)) (BConj (BConst False) (BConst False)))
  86. testExp2 = BForall (BVar "x1") (BConj (BConst False) (BConst True))
  87.