Modification.hs revision 4d7d53fec6b551333c79da6ae3b8ca2af0a741ab
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- |
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederModule : $Header$
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederDescription : interface (type class) for comorphism modifications in Hets
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederCopyright : (c) Mihai Codescu, Uni Bremen 2002-2004
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederMaintainer : mcodescu@informatik.uni-bremen.de
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederStability : provisional
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederPortability : non-portable (via Logic)
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederInterface (type class) for comorphism modifications in Hets
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-}
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
64cdaaeebee54e4f2eea562e19f4b362051d5650Christian Maedermodule Logic.Modification where
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Logic.Logic
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Logic.Comorphism
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Common.Result
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Data.Typeable
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-- | comorphism modifications
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass (Language lid, Comorphism cid1
4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
2bbcdec13d8fd4b862cea292617cba1dca78f513Christian Maeder Comorphism cid2
d186477ec3542a00bf4b0735a063fa2604c893eeChristian Maeder log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
704862436e50e42e50e5b84fd7cd2c1b65f62483Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3
64cdaaeebee54e4f2eea562e19f4b362051d5650Christian Maeder log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
sign4 morphism4 symbol4 raw_symbol4 proof_tree4)
=> Modification lid cid1 cid2
log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2
log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
sign3 morphism3 symbol3 raw_symbol3 proof_tree3
log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
sign4 morphism4 symbol4 raw_symbol4 proof_tree4
|
lid -> cid1 cid2
log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2
log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
sign3 morphism3 symbol3 raw_symbol3 proof_tree3
log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
sign4 morphism4 symbol4 raw_symbol4 proof_tree4
where
tauSigma :: lid -> sign1 -> Result morphism2
-- in the instances morphism2 and morphism4 will be the same
-- casts needed
-- component of the natural transformation
sourceComorphism :: lid -> cid1
targetComorphism :: lid -> cid2
data IdModif lid = IdModif lid deriving Show
instance Language lid => Language (IdModif lid)
instance Comorphism cid
log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2
=> Modification (IdModif cid) cid cid
log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2
log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2
where
tauSigma (IdModif cid) sigma = do (sigma1, _) <- map_sign cid sigma
return (ide sigma1)
sourceComorphism (IdModif cid) = cid
targetComorphism (IdModif cid) = cid
-- | vertical composition of modifications
data VerCompModif lid1 lid2 = VerCompModif lid1 lid2 deriving Show
instance (Language lid1, Language lid2) => Language (VerCompModif lid1 lid2)
instance (Modification lid1 cid1 cid2
log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2
log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
sign3 morphism3 symbol3 raw_symbol3 proof_tree3
log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
sign4 morphism4 symbol4 raw_symbol4 proof_tree4,
Modification lid2 cid3 cid4
log5 sublogics5 basic_spec5 sentence5 symb_items5 symb_map_items5
sign5 morphism5 symbol5 raw_symbol5 proof_tree5
log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6
sign6 morphism6 symbol6 raw_symbol6 proof_tree6
log7 sublogics7 basic_spec7 sentence7 symb_item7 symb_map_items7
sign7 morphism7 symbol7 raw_symbol7 proof_tree7
log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8
sign8 morphism8 symbol8 raw_symbol8 proof_tree8
)
=> Modification (VerCompModif lid1 lid2) cid1 cid4
log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2
log7 sublogics7 basic_spec7 sentence7 symb_item7 symb_map_items7
sign7 morphism7 symbol7 raw_symbol7 proof_tree7
log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8
sign8 morphism8 symbol8 raw_symbol8 proof_tree8
where
sourceComorphism (VerCompModif lid1 _) = sourceComorphism lid1
targetComorphism (VerCompModif _ lid2) = targetComorphism lid2
tauSigma (VerCompModif lid1 lid2) sigma = do
mor1 <- tauSigma lid1 sigma
case cast sigma of
Nothing -> fail "Cannot compose modifications"
Just sigma1 -> do
mor3 <- tauSigma lid2 sigma1
case cast mor3 of
Nothing -> fail "Cannot compose modifications"
Just mor2 -> comp mor1 mor2
-- | horizontal composition of modifications
data HorCompModif lid1 lid2 = HorCompModif lid1 lid2 deriving Show
instance (Language lid1, Language lid2) => Language (HorCompModif lid1 lid2)
instance (Modification lid1 cid1 cid2
log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2
log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
sign3 morphism3 symbol3 raw_symbol3 proof_tree3
log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
sign4 morphism4 symbol4 raw_symbol4 proof_tree4,
Modification lid2 cid3 cid4
log5 sublogics5 basic_spec5 sentence5 symb_items5 symb_map_items5
sign5 morphism5 symbol5 raw_symbol5 proof_tree5
log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6
sign6 morphism6 symbol6 raw_symbol6 proof_tree6
log7 sublogics7 basic_spec7 sentence7 symb_items7 symb_map_items7
sign7 morphism7 symbol7 raw_symbol7 proof_tree7
log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8
sign8 morphism8 symbol8 raw_symbol8 proof_tree8,
Comorphism (CompComorphism cid1 cid3)
log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6
sign6 morphism6 symbol6 raw_symbol6 proof_tree6,
Comorphism (CompComorphism cid2 cid4)
log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
sign3 morphism3 symbol3 raw_symbol3 proof_tree3
log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8
sign8 morphism8 symbol8 raw_symbol8 proof_tree8)
=> Modification (HorCompModif lid1 lid2) (CompComorphism cid1 cid3)
(CompComorphism cid2 cid4)
log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6
sign6 morphism6 symbol6 raw_symbol6 proof_tree6
log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
sign3 morphism3 symbol3 raw_symbol3 proof_tree3
log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8
sign8 morphism8 symbol8 raw_symbol8 proof_tree8
where
sourceComorphism (HorCompModif lid1 lid2) =
CompComorphism (sourceComorphism lid1) (sourceComorphism lid2)
targetComorphism (HorCompModif lid1 lid2) =
CompComorphism (targetComorphism lid1) (targetComorphism lid2)
tauSigma (HorCompModif lid1 lid2) sigma1 = do
mor2 <- tauSigma lid1 sigma1
case cast mor2 of
Nothing -> fail "Cannot compose modifications"
Just mor5 -> do
mor6 <- map_morphism (sourceComorphism lid2) mor5
case cast sigma1 of
Nothing -> fail "Cannot compose modifications"
Just sigma3 -> do
(sigma4, _) <- map_sign (targetComorphism lid1) sigma3
case cast sigma4 of
Nothing -> fail "Cannot compose modifications"
Just sigma5 ->do
mor61 <- tauSigma lid2 sigma5
comp mor6 mor61
-- | Modifications
data AnyModification = forall
lid cid1 cid2
log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2
log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
sign3 morphism3 symbol3 raw_symbol3 proof_tree3
log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
sign4 morphism4 symbol4 raw_symbol4 proof_tree4.
Modification lid cid1 cid2
log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2
log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
sign3 morphism3 symbol3 raw_symbol3 proof_tree3
log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
sign4 morphism4 symbol4 raw_symbol4 proof_tree4
=> Modification lid
instance Show AnyModification where
show (Modification lid) = language_name lid
++ ":" ++ language_name (sourceComorphism lid)
++ "=>" ++ language_name (targetComorphism lid)
idModification :: AnyComorphism -> AnyModification
idModification (Comorphism cid) = Modification (IdModif cid)
-- | vertical compositions of modifications
vertCompModification :: Monad m => AnyModification -> AnyModification
-> m AnyModification
vertCompModification (Modification lid1) (Modification lid2) =
let cid1 = targetComorphism lid1
cid2 = sourceComorphism lid2
in
if language_name cid1 == language_name cid2
then return $ Modification (VerCompModif lid1 lid2)
else fail $ "Comorphism mismatch in composition of" ++ language_name lid1
++ "and" ++ language_name lid2
-- | horizontal composition of modifications
horCompModification :: Monad m => AnyModification -> AnyModification
-> m AnyModification
horCompModification (Modification lid1) (Modification lid2) =
let cid1 = sourceComorphism lid1
cid2 = sourceComorphism lid2
in if language_name (targetLogic cid1) == language_name (sourceLogic cid2)
then return $ Modification (HorCompModif lid1 lid2)
else fail $ "Logic mismatch in composition of" ++ language_name lid1
++ "and" ++ language_name lid2