Logic.hs

{-# LANGUAGE TypeFamilies, FlexibleInstances #-}
module Logic where

import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.List (nub)

data Logic = Logic :& Logic
           | Logic :| Logic
           | Not Logic
           | Logic :=> Logic
           | Value Bool
           | Variable Int
           deriving (Eq, Ord, Show, Read)

class Proposition a where
    type Evaluation a
    evaluate :: a -> Evaluation a
    satisfy' :: Int -> a -> [Map Int Bool]

instance Proposition Logic where
    type Evaluation Logic = Bool
    evaluate (Value b) = b
    evaluate (l :& r)  = evaluate l && evaluate r
    evaluate (l :| r)  = evaluate l || evaluate r
    evaluate (Not t)   = not $ evaluate t
    evaluate (l :=> r) = not (evaluate l) || evaluate r
    evaluate (Variable _) = error "Can't evaluate a variable"
    satisfy' _ = satisfyLogic

instance Proposition a => Proposition (Logic -> a) where
    type Evaluation (Logic -> a) = Bool -> Evaluation a
    evaluate f b = evaluate (f (Value b))
    satisfy' i f = satisfy' (i + 1) (f (Variable i))

compatible :: Map Int Bool -> Map Int Bool -> Bool
compatible l r = all cond $ Map.keys l
    where cond n = fromMaybe True $ (==) <$> Map.lookup n l <*> Map.lookup n r

satisfyLogic :: Logic -> [Map Int Bool]
satisfyLogic (Variable n)   = [Map.singleton n True]
satisfyLogic (l :& r)  = [Map.union a b | a <- satisfyLogic l, b <- satisfyLogic r, compatible a b]
satisfyLogic (l :| r)  = nub $ satisfyLogic l ++ satisfyLogic r
satisfyLogic (Not t)   = map (Map.map not) $ satisfyLogic t
satisfyLogic (l :=> r) = satisfyLogic (Not l :| r)
satisfyLogic (Value _) = error "Can't satisfy a value"

satisfy :: Proposition p => p -> [Map Int Bool]
satisfy = satisfy' 0