{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

-- | This module provides conversion from S5 models and structures to their more general K equivalents.
module SMCDEL.Translations.Convert where

import qualified Data.Map.Strict as M

import SMCDEL.Language (agentsOf)
import SMCDEL.Internal.Help
import SMCDEL.Explicit.K
import SMCDEL.Explicit.S5
import SMCDEL.Symbolic.K
import SMCDEL.Symbolic.S5

class Convertable a b where
  convert :: a -> b

-- | Every S5 Kripke model is also a general Kripke model.
-- This replaces each partition \(\sim_i\) with a relation \(R_i\).
instance Convertable PointedModelS5 PointedModel where
  convert :: PointedModelS5 -> PointedModel
convert s5m :: PointedModelS5
s5m@(KrMS5 [World]
worlds [(Agent, Partition)]
rels [(World, Assignment)]
vals, World
cur) = (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM Map World (Map Prp Bool, Map Agent [World])
m, World
cur) where
    m :: Map World (Map Prp Bool, Map Agent [World])
m = [(World, (Map Prp Bool, Map Agent [World]))]
-> Map World (Map Prp Bool, Map Agent [World])
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (World
w,(World -> Map Prp Bool
valFor World
w, World -> Map Agent [World]
relsFor World
w)) | World
w <- [World]
worlds ]
    valFor :: World -> Map Prp Bool
valFor World
w = Assignment -> Map Prp Bool
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(World, Assignment)]
vals [(World, Assignment)] -> World -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! World
w)
    relsFor :: World -> Map Agent [World]
relsFor World
w = [(Agent, [World])] -> Map Agent [World]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Agent
i, Partition -> [World]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Partition -> [World]) -> Partition -> [World]
forall a b. (a -> b) -> a -> b
$ ([World] -> Bool) -> Partition -> Partition
forall a. (a -> Bool) -> [a] -> [a]
filter (World -> [World] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem World
w) ([(Agent, Partition)]
rels [(Agent, Partition)] -> Agent -> Partition
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i))
                           | Agent
i <- PointedModelS5 -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf PointedModelS5
s5m ]

-- | Every knowledge structure is also a belief structure.
-- We replace each \(O_i\) with \(\Omega_i := \bigwedge_{p \in O_i} (p \leftrightarrow p')\).
instance Convertable KnowScene BelScene where
  convert :: KnowScene -> BelScene
convert (KnS [Prp]
voc Bdd
law [(Agent, [Prp])]
obs, [Prp]
s) = ([Prp] -> Bdd -> Map Agent RelBDD -> BelStruct
BlS [Prp]
voc Bdd
law Map Agent RelBDD
obsLaws, [Prp]
s) where
    obsLaws :: Map Agent RelBDD
obsLaws = [(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Agent
i, [Prp] -> RelBDD
allsamebdd [Prp]
ob) | (Agent
i,[Prp]
ob) <- [(Agent, [Prp])]
obs ]