module Exercises1 where
import LFPMC
import Data.List

{- Exercise 1
   Write implementations of

   contradiction :: Form -> Bool

   tautology :: Form -> Bool

   -- logical entailment 
   entails :: Form -> Form -> Bool

   -- logical equivalence
   equiv :: Form -> Form -> Bool

Next, check for correctness          -}

{- Exercise 2: Check the definition of powlist for correctness -}

powlist :: Eq a => [a] -> [[a]]
powlist [] = [[]]
powlist (x:xs) = powlist xs ++ map (x:) (powlist xs)

{- Exercise 3: define allVls :: Form -> [[Name]] -}

{- Exercise 4: define names2valuation and valuation2names -}

{- Exercise 5: define evl :: [Name] -> Form -> Bool -}

{- Exercise 6: define s5eval :: [[Name]] -> Frm -> Bool -}

data Frm = Prp Name
         | Ng  Frm
         | Cj [Frm]
         | Dj [Frm]
         | Imp Frm Frm 
         | Eqv Frm Frm
         | Box Frm
         | Diam Frm
         deriving Eq

{- Exercise 7: define

  upd :: Frm -> [[Name]] -> [[Name]]

  upds :: [Frm] -> [[Name]] -> [[Name]]

-}