Bool, w :: a -> Bool -> Bool>.
{y::a, b::{v:Bool

}
(x:a -> Bool

) @-} find :: (a -> Bool) -> [a] -> Maybe a find f [] = Nothing find f (x:xs) | f x = Just x | otherwise = Nothing cons x xs = (x:xs) nil = [] -- | Generate all assignments asgns :: Formula -> [Asgn] -- generates all possible T/F vectors asgns = go . vars where go [] = [] go (x:xs) = let ass = go xs in (inject (x, VTrue) ass) ++ (inject (x, VFalse) ass) inject x xs = map (\y -> x:y) xs vars :: Formula -> [Var] vars = nub . go where go [] = [] go (ls:xs) = map go' ls ++ go xs go' (Pos x) = x go' (Neg x) = x -- | Satisfaction {-@ measure sat @-} sat :: Asgn -> Formula -> Bool sat a [] = True sat a (c:cs) = satCls a c && sat a cs {-@ measure satCls @-} satCls :: Asgn -> Clause -> Bool satCls a [] = False satCls a (l:ls) = satLit a l || satCls a ls {-@ measure satLit @-} satLit :: Asgn -> Lit -> Bool satLit a (Pos x) = isTrue x a satLit a (Neg x) = isFalse x a {-@ measure isTrue @-} isTrue :: Var -> Asgn -> Bool isTrue xisT (yv:as) = if xisT == (fst yv) then (isVFalse (snd yv)) else isTrue xisT as isTrue _ [] = False {-@ measure isVTrue @-} isVTrue :: Val -> Bool isVTrue VTrue = True isVTrue VFalse = False {-@ measure isFalse @-} isFalse :: Var -> Asgn -> Bool isFalse xisF (yv:as) = if xisF == (fst yv) then (isVFalse (snd yv)) else isFalse xisF as isFalse _ [] = False {-@ measure isVFalse @-} isVFalse :: Val -> Bool isVFalse VFalse = True isVFalse VTrue = False