Propositional Logic checker using "Continuations."

Logic.hs

module Logic where

-- https://www.ps.uni-saarland.de/~duchier/python/continuations.html

import Prelude hiding (and, lookup, not, or)

import Control.Monad.State

import Data.IntMap

type Binding = IntMap Bool

type Cont r = State Binding (r -> r)

class Formula a where
    satisfy :: a -> Cont (r -> r)
    falsify :: a -> Cont (r -> r)

data Negation p = Negation p

instance Formula p => Formula (Negation p) where
    satisfy (Negation p) = falsify p
    falsify (Negation p) = satisfy p

data Conjunction p q = Conjunction p q

instance (Formula p, Formula q) => Formula (Conjunction p q) where
    satisfy (Conjunction p q) = do
        p <- satisfy p
        q <- satisfy q
        return $ \yes no -> p (q yes) no

    falsify (Conjunction p q) = do
        p <- falsify p
        q <- falsify q
        return $ \yes no -> p yes (q yes no)

data Disjunction p q = Disjunction p q

instance (Formula p, Formula q) => Formula (Disjunction p q) where
    satisfy (Disjunction p q) = falsify (Conjunction (Negation p) (Negation q))
    falsify (Disjunction p q) = satisfy (Conjunction (Negation p) (Negation q))

data Variable = Variable Int

assign :: Bool -> Variable -> Cont (r -> r)
assign value (Variable var) = do
    bindings <- get
    case lookup var bindings of
        Just value'
            | value == value' -> return $ \yes no -> yes no
            | otherwise       -> return $ \yes no -> no
        Nothing -> do
            modify (insert var value)
            return $ \yes no -> yes no

instance Formula Variable where
    satisfy = assign True
    falsify = assign False

isValid :: Formula a => a -> Bool
isValid formula = evalState (falsify formula) empty (const False) True

and :: p -> q -> Conjunction p q
and = Conjunction

or :: p -> q -> Disjunction p q
or  = Disjunction

not :: p -> Negation p
not = Negation

impl :: p -> q -> Disjunction (Negation p) q
impl p q = or (not p) q

p, q, r :: Variable
p = Variable 0
q = Variable 1
r = Variable 2

-- isValid $ or p (not p)
-- isValid $ impl (not (not p)) p
-- isValid $ impl (impl (impl p q) p) p
-- isValid $ impl (impl p q) (or (not p) q)
-- isValid $ impl (not (and (not p) (not q))) (or p q)
-- isValid $ impl (and (or p q) (and (impl p r) (impl q r))) r