A GSV-style update semantics that validates double-negation elimination

Update.hs

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

type E = Int

type G = [Int]

newtype W = W Int deriving (Integral,Real,Enum,Num,Ord,Eq,Show)

type T = Bool

type C = [W]

type Upd = (C,G) -> [(T,W,G)]

_isHappy :: W -> E -> T
_isHappy n n' = if even n then even n' else odd n'

__isHappy :: E -> Upd
__isHappy x (ws,g) = [(_isHappy w x,w,g) | w <- ws]

initS :: (C,G)
initS = (W <$> [0..4],[])

__isHappy 0 initS

dom = [0..3]

posExt :: [(Bool,W,G)] -> [(Bool,W,G)]
posExt m = [(True,w,g) | (True,w,g) <- m]

-- This still needs to be tweaked; worlds in which nothing is true of the scope should be paired with false.

__some :: (E -> Upd) -> Upd
__some k (c,g) =
    let m = concat [k x (c,x:g) | x <- dom]
    in
    posExt m

(__some __isHappy) initS

positiveUpd :: (C,G) -> Upd -> [(C,G)]
positiveUpd (c,g) u =
    let m = posExt $ u (c,g)
    in
    [([w | (_,w,g) <- m],g) | (_,_,g) <- m]

positiveUpd initS (__some __isHappy)

__not :: Upd -> Upd
__not u m = [(not t,w,g)| (t,w,g) <- u m]

__and :: Upd -> Upd -> Upd
__and u u' m = concat [ u' m' | m' <- positiveUpd m u]

__poss :: Upd -> Upd
__poss u (c,g) = if posExt (u (c,g)) /= [] then [(True,w,g)|w <- c] else [(False,w,g)|w <- c]