7a8401ce858002b67e8f4198fde45a1562696ccbChristian Maeder{-# OPTIONS -fno-warn-missing-methods #-}

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- HetCATS/Modal/Logic_Modal.hs

e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian Maeder $Id

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu Authors: Wiebke Herding

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder Year: 2003

34bff097c14521b5e57ce37279a34256e1f78aa5Klaus Luettich-}

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maedermodule Modal.Logic_Modal where

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maederimport Logic.Logic

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederimport Common.Id

c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herdingimport FiniteMap

c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herdingimport Common.Lib.Set

c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herdingimport Data.Maybe

c2db39a683438b0f3d484519f4c93db26eec9d2eWiebke Herdingimport Modal.AS_Modal

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederdata Modal = Modal deriving (Show)

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder

2bb4c0b7bc54ce51e68bff86b3a19be16e0f0449Christian Maederinstance Language Modal where -- default definition is okay

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder

40f1a7ea3e3ed12cbeca205918b645dabed0402aChristian Maedertype Sign = Set Id

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederinstance Show Sign where

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maedertype Morphism = (Sign, FiniteMap Id Id, Sign)

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maederinstance Category Modal Sign Morphism

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder where

2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder -- ide :: id -> object -> morphism

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder ide Modal sigma = (sigma, listToFM [(i,i) | i<- toList sigma], sigma)

ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder -- comp :: id -> morphism -> morphism -> Maybe morphism

a10ff6125d62484ec5961c8a5d9d1c5a3e14fa66Christian Maeder comp Modal (sigma1 ,m1,_) (_,m2,sigma2) =

99cf1c277851e5ac7725b8b18980284d9e9aeb99Christian Maeder Just (sigma1,plusFM m1 m2,sigma2)

e374cd77f3dbe95289afa9431d36a8a8a8fdc81fChristian Maeder -- dom, cod :: id -> morphism -> object

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang dom Modal (sigma,_,_) = sigma

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang cod Modal (_,_,sigma) = sigma

99cf1c277851e5ac7725b8b18980284d9e9aeb99Christian Maeder -- legal_obj :: id -> object -> Bool

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder legal_obj Modal _ = True

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang -- legal_mor :: id -> morphism -> Bool

c64f180c7a3053a773d91a00226073d565fab46bChristian Maeder legal_mor Modal (sigma,m,_)

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder | keysFM m == toList sigma = True

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder | True = False

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang-- abstract syntax, parsing (and printing)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder-- instance Syntax Modal BASIC_SPEC

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang-- SYMB_ITEMS SYMB_MAP_ITEMS

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang-- where

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder-- parse_basic_spec :: id -> Maybe(ParseFun basic_spec)

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder-- parse_symb_items :: id -> Maybe(ParseFun symb_items)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang-- parse_symb_map_items :: id -> Maybe(ParseFun symb_map_items)

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder

1a11b3b997a32ebf7d52758dea143ef361fd9d5bChristian Maeder

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder