{- | Module : $Header$

- Description : Abstract syntax for the Compositional Modal Prover

- Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen

- License : GPLv2 or higher, see LICENSE.txt

- Maintainer : g.calin@jacobs-alumni.de

- Stability : provisional

- Portability : non-portable (various -fglasgow-exts extensions)

-

- Provides data structures used by the Compositional Prover -}

{-# LANGUAGE ScopedTypeVariables, MultiParamTypeClasses,

FunctionalDependencies #-}

module ModalLogic where

import qualified Data.Map as Map

-- | Datatype for holding modal formulae of a certain type

data Boole a = F | T | Not (Boole a) | And (Boole a) (Boole a) | At a

deriving (Eq, Ord, Show)

-- | Datatype for a modal formulae of type "l" wrapped under K modal logic

data K l = K (Boole l) deriving (Eq, Ord, Show)

-- | Datatype for the "rules" of K modal logic

data RK = RK Int deriving Show

-- | Datatype for a modal formulae of type "l" wrapped under KD modal logic

data KD l = KD (Boole l) deriving (Eq, Ord, Show)

-- | Datatype for the "rules" of KD modal logic

data RKD = RKDPos Int | RKDNeg Int deriving Show

-- | Datatype for a modal formulae of type "l" wrapped under Graded ML

data G l = G Int (Boole l) deriving (Eq, Ord, Show)

-- | Datatype for the "rules" of Graded ML

data RG = RG [Int] [Int] deriving Show

{- | Datatype for combined Segala logics

data Segala = S (KD (K Segala)) deriving (Eq, Show) -}

-- | Datatype for propositional clauses

data Clause a = Implies [a] [a] deriving (Eq, Ord, Show)

-- | Datatype for substitutions

data Subst a = Subst (Map.Map Int a) deriving (Eq, Show)

-- | Logic Class

class Logic a b | a -> b, b -> a where

-- | Match a certain clause against the rule(s) of the pertaining logic

match :: Clause (a c) -> [(b, Subst (Boole c))]

-- | Generate all clauses out of a specific (CNF) rule of the logic

clauses :: b -> [Clause Int]

-- | Generate all subclauses out of a certain (CNF) clause

subclauses :: Ord c => Clause (a c) -> [Clause (a c)]

-- | Logic instance for K modal logic

instance Logic K RK where

match ((Implies n p) :: Clause (K c)) =

let i = length n; cStrip (K x) = x

substHead = (i + 1, cStrip (head p))

substTail = zip [1 .. i] (map cStrip n)

in [(RK i, Subst (Map.fromList (substHead : substTail)))]

clauses (RK n) = [Implies [1 .. n] [n + 1]]

subclauses (Implies n p) = [Implies n [l] | l <- p]

-- | Logic instance for KD modal logic

instance Logic KD RKD where

match ((Implies n p) :: Clause (KD c)) =

let i = length n; cStrip (KD x) = x

substHead = (i + 1, cStrip (head p))

substTail = zip [1 .. i] (map cStrip n)

in [(RKDPos i, Subst (Map.fromList (substHead : substTail)))]

clauses (RKDPos n) = case n of

0 -> [Implies [] [1]]

_ -> [Implies [1 .. n] [n + 1]]

clauses (RKDNeg n) = [Implies [1 .. n] []]

subclauses (Implies n p) = [Implies n [l] | l <- p]

-- | Logic instance for Graded Modal Logic

instance Logic G RG where

match ((Implies n p) :: Clause (G c)) = []

clauses (RG u v) = []

subclauses (Implies n p) = []