SPLA.hs

type E = Int
type T = Bool
type S = [E]
type R = [E] -> T
type Var = S -> E

data Form = Rel R [Var] | Ex | Not Form | And Form Form

eval :: Form -> S -> T
eval (Rel r ts) = \e -> r [t e | t <- ts]
eval  Ex        = \e -> not (null e)
eval (Not p   ) = \e -> null [e' | e' <- dom p, eval p (e'++e)]
eval (And p q ) = \e -> eval p (drop (n q) e) && eval q e

n :: Form -> Int
n (Rel r ts) = 0
n  Ex        = 1
n (Not p   ) = 0
n (And p q ) = n p + n q

dom :: Form -> [S]
dom p = sequence (replicate (n p) univ)

minSat :: Form -> [S]
minSat p = filter (eval p) (dom p)

p :: Int -> Var
p n e = e!!n

--

univ :: [E]
univ = [1..5]

likes :: R
likes [x,y] = x < y

test = minSat $ And (And Ex Ex) (Not (Rel likes [p 0, p 1]))