{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE MonoLocalBinds #-}
{- |
Module      :  ./Logic/Modification.hs
Description :  interface (type class) for comorphism modifications in Hets
Copyright   :  (c) Mihai Codescu, Uni Bremen 2002-2004
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  mcodescu@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (via Logic)

Interface (type class) for comorphism modifications in Hets
-}

module Logic.Modification where

import Logic.Logic
import Logic.Comorphism
import Common.Result
import qualified Control.Monad.Fail as Fail
import Data.Typeable

-- | comorphism modifications
class (Language lid, Comorphism cid1
            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,
          Comorphism cid2
            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
            |
           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 Int -> IdModif lid -> ShowS
[IdModif lid] -> ShowS
IdModif lid -> String
(Int -> IdModif lid -> ShowS)
-> (IdModif lid -> String)
-> ([IdModif lid] -> ShowS)
-> Show (IdModif lid)
forall lid. Show lid => Int -> IdModif lid -> ShowS
forall lid. Show lid => [IdModif lid] -> ShowS
forall lid. Show lid => IdModif lid -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IdModif lid] -> ShowS
$cshowList :: forall lid. Show lid => [IdModif lid] -> ShowS
show :: IdModif lid -> String
$cshow :: forall lid. Show lid => IdModif lid -> String
showsPrec :: Int -> IdModif lid -> ShowS
$cshowsPrec :: forall lid. Show lid => Int -> IdModif lid -> ShowS
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 -> sign1 -> Result morphism2
tauSigma (IdModif cid :: cid
cid) sigma :: sign1
sigma = do (sigma1 :: sign2
sigma1, _) <- cid -> sign1 -> Result (sign2, [Named sentence2])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sign1 -> Result (sign2, [Named sentence2])
map_sign cid
cid sign1
sigma
                                   morphism2 -> Result morphism2
forall (m :: * -> *) a. Monad m => a -> m a
return (sign2 -> morphism2
forall object morphism.
Category object morphism =>
object -> morphism
ide sign2
sigma1)
 sourceComorphism :: IdModif cid -> cid
sourceComorphism (IdModif cid :: cid
cid) = cid
cid
 targetComorphism :: IdModif cid -> cid
targetComorphism (IdModif cid :: cid
cid) = cid
cid

-- | vertical composition of modifications
data VerCompModif lid1 lid2 = VerCompModif lid1 lid2 deriving Int -> VerCompModif lid1 lid2 -> ShowS
[VerCompModif lid1 lid2] -> ShowS
VerCompModif lid1 lid2 -> String
(Int -> VerCompModif lid1 lid2 -> ShowS)
-> (VerCompModif lid1 lid2 -> String)
-> ([VerCompModif lid1 lid2] -> ShowS)
-> Show (VerCompModif lid1 lid2)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall lid1 lid2.
(Show lid1, Show lid2) =>
Int -> VerCompModif lid1 lid2 -> ShowS
forall lid1 lid2.
(Show lid1, Show lid2) =>
[VerCompModif lid1 lid2] -> ShowS
forall lid1 lid2.
(Show lid1, Show lid2) =>
VerCompModif lid1 lid2 -> String
showList :: [VerCompModif lid1 lid2] -> ShowS
$cshowList :: forall lid1 lid2.
(Show lid1, Show lid2) =>
[VerCompModif lid1 lid2] -> ShowS
show :: VerCompModif lid1 lid2 -> String
$cshow :: forall lid1 lid2.
(Show lid1, Show lid2) =>
VerCompModif lid1 lid2 -> String
showsPrec :: Int -> VerCompModif lid1 lid2 -> ShowS
$cshowsPrec :: forall lid1 lid2.
(Show lid1, Show lid2) =>
Int -> VerCompModif lid1 lid2 -> ShowS
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 lid2 -> cid1
sourceComorphism (VerCompModif lid1 :: lid1
lid1 _) = lid1 -> cid1
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 =>
lid -> cid1
sourceComorphism lid1
lid1
 targetComorphism :: VerCompModif lid1 lid2 -> cid4
targetComorphism (VerCompModif _ lid2 :: lid2
lid2) = lid2 -> cid4
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 =>
lid -> cid2
targetComorphism lid2
lid2
 tauSigma :: VerCompModif lid1 lid2 -> sign1 -> Result morphism2
tauSigma (VerCompModif lid1 :: lid1
lid1 lid2 :: lid2
lid2) sigma :: sign1
sigma = do
   morphism2
mor1 <- lid1 -> sign1 -> Result morphism2
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 =>
lid -> sign1 -> Result morphism2
tauSigma lid1
lid1 sign1
sigma
   case sign1 -> Maybe sign5
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast sign1
sigma of
     Nothing -> String -> Result morphism2
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Cannot compose modifications"
     Just sigma1 :: sign5
sigma1 -> do
       morphism6
mor3 <- lid2 -> sign5 -> Result morphism6
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 =>
lid -> sign1 -> Result morphism2
tauSigma lid2
lid2 sign5
sigma1
       case morphism6 -> Maybe morphism2
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast morphism6
mor3 of
         Nothing -> String -> Result morphism2
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Cannot compose modifications"
         Just mor2 :: morphism2
mor2 -> morphism2 -> morphism2 -> Result morphism2
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp morphism2
mor1 morphism2
mor2

-- | horizontal composition of modifications
data HorCompModif lid1 lid2 = HorCompModif lid1 lid2 deriving Int -> HorCompModif lid1 lid2 -> ShowS
[HorCompModif lid1 lid2] -> ShowS
HorCompModif lid1 lid2 -> String
(Int -> HorCompModif lid1 lid2 -> ShowS)
-> (HorCompModif lid1 lid2 -> String)
-> ([HorCompModif lid1 lid2] -> ShowS)
-> Show (HorCompModif lid1 lid2)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall lid1 lid2.
(Show lid1, Show lid2) =>
Int -> HorCompModif lid1 lid2 -> ShowS
forall lid1 lid2.
(Show lid1, Show lid2) =>
[HorCompModif lid1 lid2] -> ShowS
forall lid1 lid2.
(Show lid1, Show lid2) =>
HorCompModif lid1 lid2 -> String
showList :: [HorCompModif lid1 lid2] -> ShowS
$cshowList :: forall lid1 lid2.
(Show lid1, Show lid2) =>
[HorCompModif lid1 lid2] -> ShowS
show :: HorCompModif lid1 lid2 -> String
$cshow :: forall lid1 lid2.
(Show lid1, Show lid2) =>
HorCompModif lid1 lid2 -> String
showsPrec :: Int -> HorCompModif lid1 lid2 -> ShowS
$cshowsPrec :: forall lid1 lid2.
(Show lid1, Show lid2) =>
Int -> HorCompModif lid1 lid2 -> ShowS
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 cid1 cid3
sourceComorphism (HorCompModif lid1 :: lid1
lid1 lid2 :: lid2
lid2) =
       cid1 -> cid3 -> CompComorphism cid1 cid3
forall cid1 cid2. cid1 -> cid2 -> CompComorphism cid1 cid2
CompComorphism (lid1 -> cid1
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 =>
lid -> cid1
sourceComorphism lid1
lid1) (lid2 -> cid3
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 =>
lid -> cid1
sourceComorphism lid2
lid2)
   targetComorphism :: HorCompModif lid1 lid2 -> CompComorphism cid2 cid4
targetComorphism (HorCompModif lid1 :: lid1
lid1 lid2 :: lid2
lid2) =
       cid2 -> cid4 -> CompComorphism cid2 cid4
forall cid1 cid2. cid1 -> cid2 -> CompComorphism cid1 cid2
CompComorphism (lid1 -> cid2
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 =>
lid -> cid2
targetComorphism lid1
lid1) (lid2 -> cid4
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 =>
lid -> cid2
targetComorphism lid2
lid2)
   tauSigma :: HorCompModif lid1 lid2 -> sign1 -> Result morphism6
tauSigma (HorCompModif lid1 :: lid1
lid1 lid2 :: lid2
lid2) sigma1 :: sign1
sigma1 = do
     morphism2
mor2 <- lid1 -> sign1 -> Result morphism2
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 =>
lid -> sign1 -> Result morphism2
tauSigma lid1
lid1 sign1
sigma1
     case morphism2 -> Maybe morphism5
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast morphism2
mor2 of
       Nothing -> String -> Result morphism6
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Cannot compose modifications"
       Just mor5 :: morphism5
mor5 -> do
         morphism6
mor6 <- cid3 -> morphism5 -> Result morphism6
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> morphism1 -> Result morphism2
map_morphism (lid2 -> cid3
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 =>
lid -> cid1
sourceComorphism lid2
lid2) morphism5
mor5
         case sign1 -> Maybe sign3
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast sign1
sigma1 of
           Nothing -> String -> Result morphism6
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Cannot compose modifications"
           Just sigma3 :: sign3
sigma3 -> do
             (sigma4 :: sign4
sigma4, _) <- cid2 -> sign3 -> Result (sign4, [Named sentence4])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sign1 -> Result (sign2, [Named sentence2])
map_sign (lid1 -> cid2
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 =>
lid -> cid2
targetComorphism lid1
lid1) sign3
sigma3
             case sign4 -> Maybe sign5
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast sign4
sigma4 of
               Nothing -> String -> Result morphism6
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Cannot compose modifications"
               Just sigma5 :: sign5
sigma5 -> lid2 -> sign5 -> Result morphism6
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 =>
lid -> sign1 -> Result morphism2
tauSigma lid2
lid2 sign5
sigma5 Result morphism6
-> (morphism6 -> Result morphism6) -> Result morphism6
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= morphism6 -> morphism6 -> Result morphism6
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp morphism6
mor6

-- | 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 Eq AnyModification where
  m1 :: AnyModification
m1 == :: AnyModification -> AnyModification -> Bool
== m2 :: AnyModification
m2 = AnyModification -> AnyModification -> Ordering
forall a. Ord a => a -> a -> Ordering
compare AnyModification
m1 AnyModification
m2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord AnyModification where
  compare :: AnyModification -> AnyModification -> Ordering
compare (Modification lid1 :: lid
lid1) (Modification lid2 :: lid
lid2) =
    String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid1) (String -> Ordering) -> String -> Ordering
forall a b. (a -> b) -> a -> b
$ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid2
    -- maybe needs to be more elaborate

instance Show AnyModification where
   show :: AnyModification -> String
show (Modification lid :: lid
lid) = lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid
     String -> ShowS
forall a. [a] -> [a] -> [a]
++ ":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ cid1 -> String
forall lid. Language lid => lid -> String
language_name (lid -> cid1
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 =>
lid -> cid1
sourceComorphism lid
lid)
     String -> ShowS
forall a. [a] -> [a] -> [a]
++ "=>" String -> ShowS
forall a. [a] -> [a] -> [a]
++ cid2 -> String
forall lid. Language lid => lid -> String
language_name (lid -> cid2
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 =>
lid -> cid2
targetComorphism lid
lid)

idModification :: AnyComorphism -> AnyModification
idModification :: AnyComorphism -> AnyModification
idModification (Comorphism cid :: cid
cid) = IdModif cid -> 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 =>
lid -> AnyModification
Modification (cid -> IdModif cid
forall lid. lid -> IdModif lid
IdModif cid
cid)

-- | vertical compositions of modifications

vertCompModification :: Fail.MonadFail m => AnyModification -> AnyModification
                     -> m AnyModification
vertCompModification :: AnyModification -> AnyModification -> m AnyModification
vertCompModification (Modification lid1 :: lid
lid1) (Modification lid2 :: lid
lid2) =
   let cid1 :: cid2
cid1 = lid -> cid2
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 =>
lid -> cid2
targetComorphism lid
lid1
       cid2 :: cid1
cid2 = lid -> cid1
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 =>
lid -> cid1
sourceComorphism lid
lid2
   in
    if cid2 -> String
forall lid. Language lid => lid -> String
language_name cid2
cid1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== cid1 -> String
forall lid. Language lid => lid -> String
language_name cid1
cid2
    then AnyModification -> m AnyModification
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyModification -> m AnyModification)
-> AnyModification -> m AnyModification
forall a b. (a -> b) -> a -> b
$ VerCompModif lid lid -> 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 =>
lid -> AnyModification
Modification (lid -> lid -> VerCompModif lid lid
forall lid1 lid2. lid1 -> lid2 -> VerCompModif lid1 lid2
VerCompModif lid
lid1 lid
lid2)
    else String -> m AnyModification
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m AnyModification) -> String -> m AnyModification
forall a b. (a -> b) -> a -> b
$ "Comorphism mismatch in composition of" String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid1
             String -> ShowS
forall a. [a] -> [a] -> [a]
++ "and" String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid2

-- | horizontal composition of modifications

horCompModification :: Fail.MonadFail m => AnyModification -> AnyModification
                    -> m AnyModification
horCompModification :: AnyModification -> AnyModification -> m AnyModification
horCompModification (Modification lid1 :: lid
lid1) (Modification lid2 :: lid
lid2) =
   let cid1 :: cid1
cid1 = lid -> cid1
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 =>
lid -> cid1
sourceComorphism lid
lid1
       cid2 :: cid1
cid2 = lid -> cid1
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 =>
lid -> cid1
sourceComorphism lid
lid2
   in if log2 -> String
forall lid. Language lid => lid -> String
language_name (cid1 -> log2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid1
cid1) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== log1 -> String
forall lid. Language lid => lid -> String
language_name (cid1 -> log1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid1
cid2)
      then AnyModification -> m AnyModification
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyModification -> m AnyModification)
-> AnyModification -> m AnyModification
forall a b. (a -> b) -> a -> b
$ HorCompModif lid lid -> 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 =>
lid -> AnyModification
Modification (lid -> lid -> HorCompModif lid lid
forall lid1 lid2. lid1 -> lid2 -> HorCompModif lid1 lid2
HorCompModif lid
lid1 lid
lid2)
      else String -> m AnyModification
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m AnyModification) -> String -> m AnyModification
forall a b. (a -> b) -> a -> b
$ "Logic mismatch in composition of" String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid1
               String -> ShowS
forall a. [a] -> [a] -> [a]
++ "and" String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid2