Public paste
Undefined
By: Guest | Date: Feb 15 2014 18:34 | Format: Haskell | Expires: never | Size: 637 B | Hits: 995

  1. module Ex12_QBF2 where
  2.  
  3. import DTC
  4. import Ex12_QBF1
  5.  
  6. data Disjunction a = Disjunction a a
  7. data ExistQuantor a = ExistQuantor a
  8.  
  9. instance Functor Disjunction where
  10.         fmap f (Disjunction x y) = Disjunction (f x) (f y)
  11. instance Functor ExistQuantor where
  12.         fmap f (ExistQuantor a) = ExistQuantor (f a)
  13.        
  14. instance EvalBQF Disjunction where
  15.         evalFormula (Disjunction x y) = x || y
  16. instance EvalBQF ExistQuantor where
  17.         evalFormula (ExistQuantor e) = e
  18.  
  19. disj :: (Disjunction :<: f) => Mu f -> Mu f -> Mu f
  20. disj x y = inject (Disjunction x y)
  21.  
  22. exists :: (ExistQuantor :<: f) => Mu f -> Mu f
  23. exists x = inject (ExistQuantor x)