solver.hs

{-# LANGUAGE DeriveFoldable, DeriveFunctor #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}

import Data.Foldable (toList)
import Data.List (nub)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (listToMaybe)
import Data.Monoid

{-| Propositions with variables of type @var@ -}
data Proposition var
  = Var var
  | Not (Proposition var)
  | And (Proposition var) (Proposition var)
  | Or (Proposition var) (Proposition var)
  | If (Proposition var) (Proposition var)
  | Iff (Proposition var) (Proposition var)
  deriving (Eq, Ord, Show, Read, Foldable, Functor)

deMorgan, deMorgan' :: Proposition Char
{-^ Example formulas: De Morgan's laws using the variables 'P' and 'Q' -}
deMorgan = Iff (Not (And (Var 'P') (Var 'Q'))) (Or (Not (Var 'P')) (Not (Var 'Q')))
deMorgan' = Iff (Not (Or (Var 'P') (Var 'Q'))) (And (Not (Var 'P')) (Not (Var 'Q')))

freeVars :: Eq var => Proposition var -> [var]
{-^ Given a 'Proposition' of @a@ return (as a list) the set of @a@s that occur within -}
freeVars = nub . toList

{-| A proposition over 'Bool's is also known as a predicate -}
type Predicate = Proposition Bool

{-| A context is a mapping from variables to actual values -}
type Ctx var = Map var Bool

eval :: Ord var => Ctx var -> Proposition var -> Bool
{-^ Given a context, compute the truth value of a proposition, e.g.:
eval (Map.fromList [('P',False),('Q',True)]) (And (Var 'P') (Var 'Q'))
False
-}
eval ctx prop = evalP $ fmap (ctx Map.!) prop
  where
    evalP = \case
        Var b -> b
        Not q -> not $ evalP q
        And p q -> evalP p && evalP q
        Or p q -> evalP p || evalP q
        If p q -> evalP p ==> evalP q
        Iff p q -> evalP p == evalP q

(==>) :: Bool -> Bool -> Bool; infix 4 ==>
{-^ Logical implication which short-circuits if first argument is False
>>> False ==> undefined
True
-}
False ==> _     = True
True  ==> False = False
True  ==> True  = True

valid :: Ord var => Proposition var -> Bool
{-^ Test if a proposition is valid/tautoligical (evaluates to @True@ in all possible contexts)
>>> valid deMorgan
True

>>> valid (Or (Var 'P') (Var 'Q'))
False
-}
valid = and . map fst . evalAll

allSat :: Ord var => Proposition var -> [Ctx var]
{-^ Get all satisfying assignments or the empty list if the predicate is unsatisfiable
>>> allSat (If (Var "foo") (Var "bar"))
[fromList [("bar",False),("foo",False)]
,fromList [("bar",True),("foo",False)]
,fromList [("bar",True),("foo",True)]]

>>> allSat (And (Var 1) (Not (Var 1)))
[]
-}
allSat = map snd . filter ((== True) . fst) . evalAll

sat :: Ord var => Proposition var -> Maybe (Ctx var)
{-^ Get a satisfying assignment, based on 'evalAll' -}
sat = listToMaybe . allSat

evalAll :: Ord var => Proposition var -> [(Bool, Ctx var)]
{-^ Evaluate a proposition with all possible contexts.
>>> evalAll (Iff (Var 2) (Var 3))
[(True,fromList [(2,False),(3,False)])
,(False,fromList [(2,False),(3,True)])
,(False,fromList [(2,True),(3,False)])
,(True,fromList [(2,True),(3,True)])]

NB: Brute force algorithm with O(c^n) time complexity where c is the cardinality of the symbolic
value (2 in the case of 'Bool') and n is the cardinality of the set of free variables
-}
evalAll p = let cs = ctxs p in zip (map (`eval` p) cs) cs

ctxs :: Ord var => Proposition var -> [Ctx var]
{-| Given a proposition, generate all possible contextsfor some symbolic type, e.g.:
>>> ctxs (And (Var 'P') (Var 'Q'))
[fromList [('P',False),('Q',False)]
,fromList [('P',False),('Q',True)]
,fromList [('P',True),('Q',False)]
,fromList [('P',True),('Q',True)]]
 -}
ctxs p = map (Map.fromList . zip vars) (allInst (length vars))
  where
    vars = freeVars p
    -- | Generate all possible instantiations, as in a truth table
    allInst = \case
        0 -> return []
        n -> do
          x <- [False,True]
          xs <- allInst (n-1)
          return (x : xs)




{- TODO: Figure out a nicer implementation of `evalP`, à la:

-- Not valid Haskell!! The gist is to replace every data constructor by the rhs
let magic = \case
        Var -> id
        Not -> not
        And -> (&&)
        Or -> (||)
        If -> (<=)
        Iff -> (==)

let compile = replace magic $ fmap ctx where ctx = \case 'P' -> False; 'Q' -> True

compile Iff (Not (And (Var 'P') (Var 'Q'))) (Or (Not (Var 'P')) (Not (Var 'Q')))
~> ((==) (not ((&&) (id True) (id False))) ((||) (not (id True)) (not (id False))))

-}