649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa{-# OPTIONS -fglasgow-exts #-}

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksamodule GMP.ModalK where

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport GMP.GMPAS

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport GMP.ModalLogic

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaimport qualified Data.Set as Set

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksadata Krules = KR Int

deriving Show

instance ModalLogic ModalK Krules where

contrClause p ma =

let n = Set.difference ma p

in [Mimplies (Set.toList p) [aux]|aux <- Set.toList n]

flagML _ = Sqr

parseIndex = return (ModalK ())

matchR (Mimplies n p) =

case p of

[] -> []

_ -> [KR (length n)]

guessClause r =

case r of

KR 0 -> [Pimplies [1] []]

KR n -> [Pimplies [n+1] [1..n]]

-------------------------------------------------------------------------------

-------------------------------------------------------------------------------