8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder , FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuDescription : interface (type class) for comorphism modifications in Hets
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuCopyright : (c) Mihai Codescu, Uni Bremen 2002-2004
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : mcodescu@informatik.uni-bremen.de
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuStability : provisional
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuPortability : non-portable (via Logic)
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai CodescuInterface (type class) for comorphism modifications in Hets
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | comorphism modifications
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescuclass (Language lid, Comorphism cid1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Comorphism cid2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign3 morphism3 symbol3 raw_symbol3 proof_tree3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign4 morphism4 symbol4 raw_symbol4 proof_tree4)
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu => Modification lid cid1 cid2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
da955132262baab309a50fdffe228c9efe68251dCui Jian sign2 morphism2 symbol2 raw_symbol2 proof_tree2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign3 morphism3 symbol3 raw_symbol3 proof_tree3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign4 morphism4 symbol4 raw_symbol4 proof_tree4
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu lid -> cid1 cid2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign3 morphism3 symbol3 raw_symbol3 proof_tree3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign4 morphism4 symbol4 raw_symbol4 proof_tree4
da955132262baab309a50fdffe228c9efe68251dCui Jian tauSigma :: lid -> sign1 -> Result morphism2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder {- in the instances morphism2 and morphism4 will be the same
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder component of the natural transformation -}
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sourceComorphism :: lid -> cid1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu targetComorphism :: lid -> cid2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederdata IdModif lid = IdModif lid deriving Show
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescuinstance Language lid => Language (IdModif lid)
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescuinstance Comorphism cid
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu => Modification (IdModif cid) cid cid
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2
2df3a08c43f067ba532151ade20b1e4e2d2efd90Mihai Codescu tauSigma (IdModif cid) sigma = do (sigma1, _) <- map_sign cid sigma
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder return (ide sigma1)
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sourceComorphism (IdModif cid) = cid
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu targetComorphism (IdModif cid) = cid
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | vertical composition of modifications
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescudata VerCompModif lid1 lid2 = VerCompModif lid1 lid2 deriving Show
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescuinstance (Language lid1, Language lid2) => Language (VerCompModif lid1 lid2)
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescuinstance (Modification lid1 cid1 cid2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign3 morphism3 symbol3 raw_symbol3 proof_tree3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
da955132262baab309a50fdffe228c9efe68251dCui Jian sign4 morphism4 symbol4 raw_symbol4 proof_tree4,
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Modification lid2 cid3 cid4
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log5 sublogics5 basic_spec5 sentence5 symb_items5 symb_map_items5
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign5 morphism5 symbol5 raw_symbol5 proof_tree5
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign6 morphism6 symbol6 raw_symbol6 proof_tree6
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log7 sublogics7 basic_spec7 sentence7 symb_item7 symb_map_items7
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign7 morphism7 symbol7 raw_symbol7 proof_tree7
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8
da955132262baab309a50fdffe228c9efe68251dCui Jian sign8 morphism8 symbol8 raw_symbol8 proof_tree8
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu => Modification (VerCompModif lid1 lid2) cid1 cid4
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log7 sublogics7 basic_spec7 sentence7 symb_item7 symb_map_items7
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign7 morphism7 symbol7 raw_symbol7 proof_tree7
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8
da955132262baab309a50fdffe228c9efe68251dCui Jian sign8 morphism8 symbol8 raw_symbol8 proof_tree8
2df3a08c43f067ba532151ade20b1e4e2d2efd90Mihai Codescu sourceComorphism (VerCompModif lid1 _) = sourceComorphism lid1
2df3a08c43f067ba532151ade20b1e4e2d2efd90Mihai Codescu targetComorphism (VerCompModif _ lid2) = targetComorphism lid2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu tauSigma (VerCompModif lid1 lid2) sigma = do
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder mor1 <- tauSigma lid1 sigma
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder case cast sigma of
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Nothing -> fail "Cannot compose modifications"
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Just sigma1 -> do
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder mor3 <- tauSigma lid2 sigma1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder case cast mor3 of
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Nothing -> fail "Cannot compose modifications"
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Just mor2 -> comp mor1 mor2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | horizontal composition of modifications
da955132262baab309a50fdffe228c9efe68251dCui Jiandata HorCompModif lid1 lid2 = HorCompModif lid1 lid2 deriving Show
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescuinstance (Language lid1, Language lid2) => Language (HorCompModif lid1 lid2)
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescuinstance (Modification lid1 cid1 cid2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign3 morphism3 symbol3 raw_symbol3 proof_tree3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
da955132262baab309a50fdffe228c9efe68251dCui Jian sign4 morphism4 symbol4 raw_symbol4 proof_tree4,
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Modification lid2 cid3 cid4
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log5 sublogics5 basic_spec5 sentence5 symb_items5 symb_map_items5
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign5 morphism5 symbol5 raw_symbol5 proof_tree5
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign6 morphism6 symbol6 raw_symbol6 proof_tree6
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log7 sublogics7 basic_spec7 sentence7 symb_items7 symb_map_items7
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign7 morphism7 symbol7 raw_symbol7 proof_tree7
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8
da955132262baab309a50fdffe228c9efe68251dCui Jian sign8 morphism8 symbol8 raw_symbol8 proof_tree8,
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Comorphism (CompComorphism cid1 cid3)
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign6 morphism6 symbol6 raw_symbol6 proof_tree6,
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu Comorphism (CompComorphism cid2 cid4)
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign3 morphism3 symbol3 raw_symbol3 proof_tree3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign8 morphism8 symbol8 raw_symbol8 proof_tree8)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder => Modification (HorCompModif lid1 lid2) (CompComorphism cid1 cid3)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (CompComorphism cid2 cid4)
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6
da955132262baab309a50fdffe228c9efe68251dCui Jian sign6 morphism6 symbol6 raw_symbol6 proof_tree6
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign3 morphism3 symbol3 raw_symbol3 proof_tree3
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu sign8 morphism8 symbol8 raw_symbol8 proof_tree8
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sourceComorphism (HorCompModif lid1 lid2) =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder CompComorphism (sourceComorphism lid1) (sourceComorphism lid2)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder targetComorphism (HorCompModif lid1 lid2) =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder CompComorphism (targetComorphism lid1) (targetComorphism lid2)
fe649b05d4faaf8ba7b408384843d33e5937ef31Mihai Codescu tauSigma (HorCompModif lid1 lid2) sigma1 = do
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder mor2 <- tauSigma lid1 sigma1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder case cast mor2 of
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Nothing -> fail "Cannot compose modifications"
4d7d53fec6b551333c79da6ae3b8ca2af0a741abChristian Maeder Just mor5 -> do
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder mor6 <- map_morphism (sourceComorphism lid2) mor5
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder case cast sigma1 of
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Nothing -> fail "Cannot compose modifications"
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Just sigma3 -> do
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (sigma4, _) <- map_sign (targetComorphism lid1) sigma3
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder case cast sigma4 of
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Nothing -> fail "Cannot compose modifications"
09943dce50b9804d3729d0b989f07202205986e0Christian Maeder Just sigma5 -> tauSigma lid2 sigma5 >>= comp mor6
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | Modifications
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederdata AnyModification = forall
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid cid1 cid2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4 .
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Modification lid cid1 cid2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder => Modification lid
36f69d35e01d2d6b6bdc165b49661f2a80af8687Mihai Codescuinstance Eq AnyModification where
09943dce50b9804d3729d0b989f07202205986e0Christian Maeder m1 == m2 = compare m1 m2 == EQ
09943dce50b9804d3729d0b989f07202205986e0Christian Maederinstance Ord AnyModification where
09943dce50b9804d3729d0b989f07202205986e0Christian Maeder compare (Modification lid1) (Modification lid2) =
09943dce50b9804d3729d0b989f07202205986e0Christian Maeder compare (language_name lid1) $ language_name lid2
09943dce50b9804d3729d0b989f07202205986e0Christian Maeder -- maybe needs to be more elaborate
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Show AnyModification where
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder show (Modification lid) = language_name lid
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ++ ":" ++ language_name (sourceComorphism lid)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ++ "=>" ++ language_name (targetComorphism lid)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederidModification :: AnyComorphism -> AnyModification
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederidModification (Comorphism cid) = Modification (IdModif cid)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | vertical compositions of modifications
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedervertCompModification :: Monad m => AnyModification -> AnyModification
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -> m AnyModification
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedervertCompModification (Modification lid1) (Modification lid2) =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder let cid1 = targetComorphism lid1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder cid2 = sourceComorphism lid2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder if language_name cid1 == language_name cid2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder then return $ Modification (VerCompModif lid1 lid2)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder else fail $ "Comorphism mismatch in composition of" ++ language_name lid1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ "and" ++ language_name lid2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | horizontal composition of modifications
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederhorCompModification :: Monad m => AnyModification -> AnyModification
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -> m AnyModification
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederhorCompModification (Modification lid1) (Modification lid2) =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder let cid1 = sourceComorphism lid1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder cid2 = sourceComorphism lid2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder in if language_name (targetLogic cid1) == language_name (sourceLogic cid2)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder then return $ Modification (HorCompModif lid1 lid2)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder else fail $ "Logic mismatch in composition of" ++ language_name lid1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ++ "and" ++ language_name lid2