content: {-# LANGUAGE ExistentialQuantification, MultiParamTypeClasses
   , DeriveDataTypeable, GeneralizedNewtypeDeriving #-}
  {- |
  Module      :  ./Logic/Grothendieck.hs
  Description :  Grothendieck logic (flattening of logic graph to a single logic)
  Copyright   :  (c) Till Mossakowski, and Uni Bremen 2002-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  till@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  non-portable (overlapping instances, dynamics, existentials)
  
  Grothendieck logic (flattening of logic graph to a single logic)
  
  The Grothendieck logic is defined to be the
     heterogeneous logic over the logic graph.
     This will be the logic over which the data
     structures and algorithms for specification in-the-large
     are built.
  
     This module heavily works with existential types, see
     <http://haskell.org/hawiki/ExistentialTypes> and chapter 7 of /Heterogeneous
     specification and the heterogeneous tool set/
     (<http://www.informatik.uni-bremen.de/~till/papers/habil.ps>).
  
     References:
  
     R. Diaconescu:
     Grothendieck institutions
     J. applied categorical structures 10, 2002, p. 383-402.
  
     T. Mossakowski:
     Comorphism-based Grothendieck institutions.
     In K. Diks, W. Rytter (Eds.), Mathematical foundations of computer science,
     LNCS 2420, pp. 593-604
  
     T. Mossakowski:
     Heterogeneous specification and the heterogeneous tool set.
  -}
  
  module Logic.Grothendieck
    ( G_basic_spec (..)
    , G_sign (..)
    , SigId (..)
    , startSigId
    , isHomSubGsign
    , isSubGsign
    , logicOfGsign
    , symsOfGsign
    , G_symbolmap (..)
    , G_mapofsymbol (..)
    , G_symbol (..)
    , G_symb_items_list (..)
    , G_symb_map_items_list (..)
    , G_sublogics (..)
    , isSublogic
    , isProperSublogic
    , joinSublogics
    , G_morphism (..)
    , MorId (..)
    , startMorId
    , mkG_morphism
    , lessSublogicComor
    , LogicGraph (..)
    , setCurLogic
    , setSyntax
    , setCurSublogic
    , emptyLogicGraph
    , lookupLogic
    , lookupCurrentLogic
    , lookupCurrentSyntax
    , lookupCompComorphism
    , lookupComorphism
    , lookupModification
    , GMorphism (..)
    , isHomogeneous
    , Grothendieck (..)
    , gEmbed
    , gEmbed2
    , gEmbedComorphism
    , homGsigDiff
    , gsigUnion
    , gsigManyUnion
    , gsigManyIntersect
    , homogeneousMorManyUnion
    , logicInclusion
    , logicUnion
    , updateMorIndex
    , toG_morphism
    , gSigCoerce
    , ginclusion
    , compInclusion
    , findComorphismPaths
    , logicGraph2Graph
    , findComorphism
    , isTransportable
    , Square (..)
    , LaxTriangle (..)
    , mkIdSquare
    , mkDefSquare
    , mirrorSquare
    , lookupSquare
    ) where
  
  import Logic.Coerce
  import Logic.Comorphism
  import Logic.ExtSign
  import Logic.Logic
  import Logic.Modification
  import Logic.Morphism
  
  import ATerm.Lib
  
  import Common.Doc
  import Common.DocUtils
  import Common.ExtSign
  import Common.Id
  import Common.IRI (IRI)
  import Common.Lexer
  import Common.Parsec
  import Common.Result
  import Common.Token
  import Common.Utils
  import Common.LibName
  import Common.GraphAlgo
  
  import Control.Monad (foldM)
  import qualified Control.Monad.Fail as Fail
  import Data.Maybe
  import Data.Typeable
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import qualified Data.HashMap.Strict as HMap
  import qualified Data.HashSet as HSet
  import qualified Data.Heap as Heap
  
  import Text.Printf
  
  import Text.ParserCombinators.Parsec (Parser, parse, eof, (<|>))
  -- for looking up modifications
  
  -- * \"Grothendieck\" versions of the various parts of type class Logic
  
  -- | Grothendieck basic specifications
  data G_basic_spec = forall lid sublogics
          basic_spec sentence symb_items symb_map_items
           sign morphism symbol raw_symbol proof_tree .
          Logic lid sublogics
           basic_spec sentence symb_items symb_map_items
            sign morphism symbol raw_symbol proof_tree =>
    G_basic_spec lid basic_spec
    deriving Typeable
  
  instance Show G_basic_spec where
      show (G_basic_spec _ s) = show s
  
  instance Pretty G_basic_spec where
      pretty (G_basic_spec _ s) = pretty s
  
  instance GetRange G_basic_spec
  
  -- dummy instances for development graphs
  instance Ord G_basic_spec where
    compare _ _ = EQ
  
  instance Eq G_basic_spec where
    _ == _ = True
  
  -- | index for signatures
  newtype SigId = SigId Int
    deriving (Typeable, Show, Eq, Ord, Enum, ShATermConvertible)
  
  startSigId :: SigId
  startSigId = SigId 0
  
  {- | Grothendieck signatures with an lookup index. Zero indices
   indicate unknown ones. It would be nice to have special (may be
   negative) indices for empty signatures (one for every logic). -}
  data G_sign = forall lid sublogics
          basic_spec sentence symb_items symb_map_items
           sign morphism symbol raw_symbol proof_tree .
          Logic lid sublogics
           basic_spec sentence symb_items symb_map_items
            sign morphism symbol raw_symbol proof_tree => G_sign
      { gSignLogic :: lid
      , gSign :: ExtSign sign symbol
      , gSignSelfIdx :: SigId -- ^ index to lookup this 'G_sign' in sign map
      } deriving Typeable
  
  instance Eq G_sign where
    a == b = compare a b == EQ
  
  instance Ord G_sign where
    compare (G_sign l1 sigma1 s1) (G_sign l2 sigma2 s2) =
      if s1 > startSigId && s2 > startSigId && s1 == s2 then EQ else
      case compare (Logic l1) $ Logic l2 of
        EQ -> compare (coerceSign l1 l2 "Eq G_sign" sigma1) $ Just sigma2
        r -> r
  
  -- | prefer a faster subsignature test if possible
  isHomSubGsign :: G_sign -> G_sign -> Bool
  isHomSubGsign (G_sign l1 sigma1 s1) (G_sign l2 sigma2 s2) =
      (s1 > startSigId && s2 > startSigId && s1 == s2) ||
      maybe False (ext_is_subsig l1 sigma1)
        (coerceSign l2 l1 "isHomSubGsign" sigma2)
  
  isSubGsign :: LogicGraph -> G_sign -> G_sign -> Bool
  isSubGsign lg (G_sign lid1 (ExtSign sigma1 _) _)
                 (G_sign lid2 (ExtSign sigma2 _) _) =
    Just True ==
    do Comorphism cid <- resultToMaybe $
                           logicInclusion lg (Logic lid1) (Logic lid2)
       sigma1' <- coercePlainSign lid1 (sourceLogic cid)
                  "Grothendieck.isSubGsign: cannot happen" sigma1
       sigma2' <- coercePlainSign lid2 (targetLogic cid)
                  "Grothendieck.isSubGsign: cannot happen" sigma2
       sigma1t <- resultToMaybe $ map_sign cid sigma1'
       return $ is_subsig (targetLogic cid) (fst sigma1t) sigma2'
  
  instance Show G_sign where
      show (G_sign _ s _) = show s
  
  instance Pretty G_sign where
      pretty (G_sign _ (ExtSign s _) _) = pretty s
  
  logicOfGsign :: G_sign -> AnyLogic
  logicOfGsign (G_sign lid _ _) = Logic lid
  
  symsOfGsign :: G_sign -> Set.Set G_symbol
  symsOfGsign (G_sign lid (ExtSign sgn _) _) = Set.map (G_symbol lid)
      $ symset_of lid sgn
  
  -- | Grothendieck maps with symbol as keys
  data G_symbolmap a = forall lid sublogics
          basic_spec sentence symb_items symb_map_items
           sign morphism symbol raw_symbol proof_tree .
          Logic lid sublogics
           basic_spec sentence symb_items symb_map_items
            sign morphism symbol raw_symbol proof_tree =>
    G_symbolmap lid (Map.Map symbol a)
    deriving Typeable
  
  instance Show a => Show (G_symbolmap a) where
      show (G_symbolmap _ sm) = show sm
  
  instance (Typeable a, Ord a) => Eq (G_symbolmap a) where
      a == b = compare a b == EQ
  
  instance (Typeable a, Ord a) => Ord (G_symbolmap a) where
    compare (G_symbolmap l1 sm1) (G_symbolmap l2 sm2) =
      case compare (Logic l1) $ Logic l2 of
        EQ -> compare (coerceSymbolmap l1 l2 sm1) sm2
        r -> r
  
  
  -- | Grothendieck maps with symbol as values
  data G_mapofsymbol a = forall lid sublogics
          basic_spec sentence symb_items symb_map_items
           sign morphism symbol raw_symbol proof_tree .
          Logic lid sublogics
           basic_spec sentence symb_items symb_map_items
            sign morphism symbol raw_symbol proof_tree =>
    G_mapofsymbol lid (Map.Map a symbol)
    deriving Typeable
  
  instance Show a => Show (G_mapofsymbol a) where
      show (G_mapofsymbol _ sm) = show sm
  
  instance (Typeable a, Ord a) => Eq (G_mapofsymbol a) where
      a == b = compare a b == EQ
  
  instance (Typeable a, Ord a) => Ord (G_mapofsymbol a) where
    compare (G_mapofsymbol l1 sm1) (G_mapofsymbol l2 sm2) =
      case compare (Logic l1) $ Logic l2 of
        EQ -> compare (coerceMapofsymbol l1 l2 sm1) sm2
        r -> r
  
  
  -- | Grothendieck symbols
  data G_symbol = forall lid sublogics
          basic_spec sentence symb_items symb_map_items
           sign morphism symbol raw_symbol proof_tree .
          Logic lid sublogics
           basic_spec sentence symb_items symb_map_items
            sign morphism symbol raw_symbol proof_tree =>
    G_symbol lid symbol
    deriving Typeable
  
  instance GetRange G_symbol where
    getRange (G_symbol _ s) = getRange s
    rangeSpan (G_symbol _ s) = rangeSpan s
  
  instance Show G_symbol where
      show (G_symbol _ s) = show s
  
  instance Pretty G_symbol where
      pretty (G_symbol _ s) = pretty s
  
  instance Eq G_symbol where
      a == b = compare a b == EQ
  
  instance Ord G_symbol where
    compare (G_symbol l1 s1) (G_symbol l2 s2) =
      case compare (Logic l1) $ Logic l2 of
        EQ -> compare (coerceSymbol l1 l2 s1) s2
        r -> r
  
  -- | Grothendieck symbol lists
  data G_symb_items_list = forall lid sublogics
          basic_spec sentence symb_items symb_map_items
           sign morphism symbol raw_symbol proof_tree .
          Logic lid sublogics
           basic_spec sentence symb_items symb_map_items
            sign morphism symbol raw_symbol proof_tree =>
          G_symb_items_list lid [symb_items]
    deriving Typeable
  
  instance GetRange G_symb_items_list
  
  instance Show G_symb_items_list where
      show (G_symb_items_list _ l) = show l
  
  instance Pretty G_symb_items_list where
      pretty (G_symb_items_list _ l) = ppWithCommas l
  
  instance Eq G_symb_items_list where
    (G_symb_items_list i1 s1) == (G_symb_items_list i2 s2) =
       coerceSymbItemsList i1 i2 "Eq G_symb_items_list" s1 == Just s2
  
  -- | Grothendieck symbol maps
  data G_symb_map_items_list = forall lid sublogics
          basic_spec sentence symb_items symb_map_items
           sign morphism symbol raw_symbol proof_tree .
          Logic lid sublogics
           basic_spec sentence symb_items symb_map_items
            sign morphism symbol raw_symbol proof_tree =>
          G_symb_map_items_list lid [symb_map_items]
    deriving Typeable
  
  instance GetRange G_symb_map_items_list
  
  instance Show G_symb_map_items_list where
      show (G_symb_map_items_list _ l) = show l
  
  instance Pretty G_symb_map_items_list where
      pretty (G_symb_map_items_list _ l) = ppWithCommas l
  
  instance Eq G_symb_map_items_list where
    (G_symb_map_items_list i1 s1) == (G_symb_map_items_list i2 s2) =
       coerceSymbMapItemsList i1 i2 "Eq G_symb_map_items_list" s1 == Just s2
  
  -- | Grothendieck sublogics
  data G_sublogics = forall lid sublogics
          basic_spec sentence symb_items symb_map_items
           sign morphism symbol raw_symbol proof_tree .
          Logic lid sublogics
           basic_spec sentence symb_items symb_map_items
            sign morphism symbol raw_symbol proof_tree =>
          G_sublogics lid sublogics
    deriving Typeable
  
  instance Show G_sublogics where
      show (G_sublogics lid sub) = language_name lid ++ case sublogicName sub of
        [] -> ""
        h -> '.' : h
  
  instance Eq G_sublogics where
      g1 == g2 = compare g1 g2 == EQ
  
  instance Ord G_sublogics where
      compare (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
        case compare (Logic lid1) $ Logic lid2 of
          EQ -> compare (forceCoerceSublogic lid1 lid2 l1) l2
          r -> r
  
  isSublogic :: G_sublogics -> G_sublogics -> Bool
  isSublogic (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
      isSubElem (forceCoerceSublogic lid1 lid2 l1) l2
  
  isProperSublogic :: G_sublogics -> G_sublogics -> Bool
  isProperSublogic a b = isSublogic a b && a /= b
  
  joinSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics
  joinSublogics (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
      case coerceSublogic lid1 lid2 "coerce Sublogic" l1 of
        Just sl -> Just (G_sublogics lid2 (lub sl l2))
        Nothing -> Nothing
  
  -- | index for morphisms
  newtype MorId = MorId Int
    deriving (Typeable, Show, Eq, Ord, Enum, ShATermConvertible)
  
  startMorId :: MorId
  startMorId = MorId 0
  
  {- | Homogeneous Grothendieck signature morphisms with indices. For
  the domain index it would be nice it showed also the emptiness. -}
  data G_morphism = forall lid sublogics
          basic_spec sentence symb_items symb_map_items
           sign morphism symbol raw_symbol proof_tree .
          Logic lid sublogics
           basic_spec sentence symb_items symb_map_items
            sign morphism symbol raw_symbol proof_tree => G_morphism
      { gMorphismLogic :: lid
      , gMorphism :: morphism
      , gMorphismSelfIdx :: MorId -- ^ lookup index in morphism map
      } deriving Typeable
  
  instance Show G_morphism where
      show (G_morphism _ m _) = show m
  
  instance Pretty G_morphism where
      pretty (G_morphism _ m _) = pretty m
  
  mkG_morphism :: forall lid sublogics
          basic_spec sentence symb_items symb_map_items
           sign morphism symbol raw_symbol proof_tree .
          Logic lid sublogics
           basic_spec sentence symb_items symb_map_items
            sign morphism symbol raw_symbol proof_tree
    => lid -> morphism -> G_morphism
  mkG_morphism l m = G_morphism l m startMorId
  
  -- | check if sublogic fits for comorphism
  lessSublogicComor :: G_sublogics -> AnyComorphism -> Bool
  lessSublogicComor (G_sublogics lid1 sub1) (Comorphism cid) =
      let lid2 = sourceLogic cid
      in Logic lid2 == Logic lid1
          && isSubElem (forceCoerceSublogic lid1 lid2 sub1) (sourceSublogic cid)
  
  type SublogicBasedTheories = Map.Map IRI (LibName, String)
  
  -- | Logic graph
  data LogicGraph = LogicGraph
      { logics :: Map.Map String AnyLogic
      , currentLogic :: String
      , currentSyntax :: Maybe IRI
      , currentSublogic :: Maybe G_sublogics
      , currentTargetBase :: Maybe (LibName, String)
      , sublogicBasedTheories :: Map.Map AnyLogic SublogicBasedTheories
      , comorphisms :: Map.Map String AnyComorphism
      , inclusions :: Map.Map (String, String) AnyComorphism
      , unions :: Map.Map (String, String) (AnyComorphism, AnyComorphism)
      , morphisms :: Map.Map String AnyMorphism
      , modifications :: Map.Map String AnyModification
      , squares :: Map.Map (AnyComorphism, AnyComorphism) [Square]
      , qTATranslations :: Map.Map String AnyComorphism
      , prefixes :: Map.Map String IRI
      , dolOnly :: Bool
      } deriving Show
  
  emptyLogicGraph :: LogicGraph
  emptyLogicGraph = LogicGraph
      { logics = Map.empty
      , currentLogic = "CASL"
      , currentSyntax = Nothing
      , currentSublogic = Nothing
      , currentTargetBase = Nothing
      , sublogicBasedTheories = Map.empty
      , comorphisms = Map.empty
      , inclusions = Map.empty
      , unions = Map.empty
      , morphisms = Map.empty
      , modifications = Map.empty
      , squares = Map.empty
      , qTATranslations = Map.empty
      , prefixes = Map.empty
      , dolOnly = False
      }
  
  setCurLogicAux :: String -> LogicGraph -> LogicGraph
  setCurLogicAux s lg = lg { currentLogic = s }
  
  setCurLogic :: String -> LogicGraph -> LogicGraph
  setCurLogic s lg = if s == currentLogic lg then
         lg else setSyntaxAux Nothing $ setCurLogicAux s lg
  
  setSyntaxAux :: Maybe IRI -> LogicGraph -> LogicGraph
  setSyntaxAux s lg = lg { currentSyntax = s }
  
  setSyntax :: Maybe IRI -> LogicGraph -> LogicGraph
  setSyntax s lg = if isNothing s then lg else setSyntaxAux s lg
  
  setCurSublogic :: Maybe G_sublogics -> LogicGraph -> LogicGraph
  setCurSublogic s lg = lg { currentSublogic = s }
  
  instance Pretty LogicGraph where
      pretty lg = text ("current logic is: " ++ currentLogic lg)
         $+$ text "all logics:"
         $+$ sepByCommas (map text $ Map.keys $ logics lg)
         $+$ text "comorphism inclusions:"
         $+$ vcat (map pretty $ Map.elems $ inclusions lg)
         $+$ text "all comorphisms:"
         $+$ vcat (map pretty $ Map.elems $ comorphisms lg)
  
  -- | find a logic in a logic graph
  lookupLogic :: Fail.MonadFail m => String -> String -> LogicGraph -> m AnyLogic
  lookupLogic error_prefix logname logicGraph =
      case Map.lookup logname $ logics logicGraph of
      Nothing -> Fail.fail $ error_prefix ++ "unknown logic: " ++ logname
      Just lid -> return lid
  
  lookupCurrentLogic :: Fail.MonadFail m => String -> LogicGraph -> m AnyLogic
  lookupCurrentLogic msg lg = lookupLogic (msg ++ " ") (currentLogic lg) lg
  
  lookupCurrentSyntax :: Fail.MonadFail m => String -> LogicGraph
    -> m (AnyLogic, Maybe IRI)
  lookupCurrentSyntax msg lg = do
    l <- lookupLogic (msg ++ " ") (currentLogic lg) lg
    return (l, currentSyntax lg)
  
  -- | union to two logics
  logicUnion :: LogicGraph -> AnyLogic -> AnyLogic
             -> Result (AnyComorphism, AnyComorphism)
  logicUnion lg l1@(Logic lid1) l2@(Logic lid2) =
    case logicInclusion lg l1 l2 of
      Result _ (Just c) -> return (c, idComorphism l2)
      _ -> case logicInclusion lg l2 l1 of
        Result _ (Just c) -> return (idComorphism l1, c)
        _ -> case Map.lookup (ln1, ln2) (unions lg) of
          Just u -> return u
          Nothing -> case Map.lookup (ln2, ln1) (unions lg) of
            Just (c2, c1) -> return (c1, c2)
            Nothing -> Fail.fail $ "Union of logics " ++ ln1 ++
                       " and " ++ ln2 ++ " does not exist"
     where ln1 = language_name lid1
           ln2 = language_name lid2
  
  -- | find a comorphism composition in a logic graph
  lookupCompComorphism :: Fail.MonadFail m => [String] -> LogicGraph -> m AnyComorphism
  lookupCompComorphism nameList logicGraph = do
    cs <- mapM lookupN nameList
    case cs of
      c : cs1 -> foldM compComorphism c cs1
      _ -> Fail.fail "Illegal empty comorphism composition"
    where
    lookupN name =
      case name of
        'i' : 'd' : '_' : logic -> do
           let (mainLogic, subLogicD) = span (/= '.') logic
            -- subLogicD will begin with a . which has to be removed
               msublogic = if null subLogicD
                       then Nothing
                       else Just $ tail subLogicD
           Logic lid <- maybe (Fail.fail ("Cannot find Logic " ++ mainLogic)) return
                   $ Map.lookup mainLogic (logics logicGraph)
           case maybe (Just $ top_sublogic lid) (parseSublogic lid) msublogic of
             Nothing -> Fail.fail $ maybe "missing sublogic"
                      ("unknown sublogic name " ++) msublogic
             Just s -> return $ Comorphism $ mkIdComorphism lid s
        _ -> maybe (Fail.fail ("Cannot find logic comorphism " ++ name)) return
               $ Map.lookup name (comorphisms logicGraph)
  
  -- | find a comorphism in a logic graph
  lookupComorphism :: Fail.MonadFail m => String -> LogicGraph -> m AnyComorphism
  lookupComorphism = lookupCompComorphism . splitOn ';'
  
  -- | find a modification in a logic graph
  lookupModification :: (Fail.MonadFail m) => String -> LogicGraph -> m AnyModification
  lookupModification input lG
          = case parse (parseModif lG << eof) "" input of
              Left err -> Fail.fail $ show err
              Right x -> x
  
  parseModif :: (Fail.MonadFail m) => LogicGraph -> Parser (m AnyModification)
  parseModif lG = do
    (xs, _) <- separatedBy (vertcomp lG) crossT
    let r = do
          y <- sequence xs
          case y of
            m : ms -> return $ foldM horCompModification m ms
            _ -> Nothing
    case r of
      Nothing -> Fail.fail "Illegal empty horizontal composition"
      Just m -> return m
  
  vertcomp :: (Fail.MonadFail m) => LogicGraph -> Parser (m AnyModification)
  vertcomp lG = do
    (xs, _) <- separatedBy (pm lG) semiT
    let r = do
          y <- sequence xs
          case y of
            m : ms -> return $ foldM vertCompModification m ms
            _ -> Nothing
               -- r has type Maybe (m AnyModification)
    case r of
      Nothing -> Fail.fail "Illegal empty vertical composition"
      Just m -> return m
  
  pm :: (Fail.MonadFail m) => LogicGraph -> Parser (m AnyModification)
  pm lG = parseName lG <|> bracks lG
  
  bracks :: (Fail.MonadFail m) => LogicGraph -> Parser (m AnyModification)
  bracks lG = do
    oParenT
    modif <- parseModif lG
    cParenT
    return modif
  
  parseIdentity :: (Fail.MonadFail m) => LogicGraph -> Parser (m AnyModification)
  parseIdentity lG = do
    tryString "id_"
    tok <- simpleId
    let name = tokStr tok
    case Map.lookup name (comorphisms lG) of
      Nothing -> Fail.fail $ "Cannot find comorphism" ++ name
      Just x -> return $ return $ idModification x
  
  parseName :: (Fail.MonadFail m) => LogicGraph -> Parser (m AnyModification)
  parseName lG = parseIdentity lG <|> do
    tok <- simpleId
    let name = tokStr tok
    case Map.lookup name (modifications lG) of
      Nothing -> Fail.fail $ "Cannot find modification" ++ name
      Just x -> return $ return x
  
  -- * The Grothendieck signature category
  
  -- | Grothendieck signature morphisms with indices
  data GMorphism = 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 => GMorphism
      { gMorphismComor :: cid
      , gMorphismSign :: ExtSign sign1 symbol1
      , gMorphismSignIdx :: SigId -- ^ 'G_sign' index of source signature
      , gMorphismMor :: morphism2
      , gMorphismMorIdx :: MorId  -- ^ `G_morphism index of target morphism
      } deriving Typeable
  
  instance Eq GMorphism where
      a == b = compare a b == EQ
  
  instance Ord GMorphism where
    compare (GMorphism cid1 sigma1 in1 mor1 in1')
      (GMorphism cid2 sigma2 in2 mor2 in2') =
        case compare (Comorphism cid1, G_sign (sourceLogic cid1) sigma1 in1)
              (Comorphism cid2, G_sign (sourceLogic cid2) sigma2 in2) of
          EQ -> if in1' > startMorId && in2' > startMorId && in1' == in2'
            then EQ else
            compare (coerceMorphism (targetLogic cid1) (targetLogic cid2)
                     "Ord GMorphism.coerceMorphism" mor1) (Just mor2)
            -- this coersion will succeed, because cid1 and cid2 are equal
          r -> r
  
  isHomogeneous :: GMorphism -> Bool
  isHomogeneous (GMorphism cid _ _ _ _) =
    isIdComorphism (Comorphism cid)
  
  data Grothendieck = Grothendieck deriving (Typeable, Show)
  
  instance Language Grothendieck
  
  instance Show GMorphism where
      show (GMorphism cid s _ m _) =
        show (Comorphism cid) ++ "(" ++ show s ++ ")" ++ show m
  
  instance Pretty GMorphism where
      pretty (GMorphism cid (ExtSign s _) _ m _) = let c = Comorphism cid in fsep
        [ text $ show c
        , if isIdComorphism c then empty else specBraces $ space <> pretty s
        , pretty m ]
  
  -- signature category of the Grothendieck institution
  instance Category G_sign GMorphism where
    ide (G_sign lid sigma@(ExtSign s _) ind) =
      GMorphism (mkIdComorphism lid (top_sublogic lid))
                sigma ind (ide s) startMorId
    -- composition of Grothendieck signature morphisms
    composeMorphisms (GMorphism r1 sigma1 ind1 mor1 _)
         (GMorphism r2 _sigma2 _ mor2 _) =
      do let lid1 = sourceLogic r1
             lid2 = targetLogic r1
             lid3 = sourceLogic r2
             lid4 = targetLogic r2
         -- if the second comorphism is the identity then simplify immediately
         if isIdComorphism (Comorphism r2) then do
             mor2' <- coerceMorphism lid4 lid2 "Grothendieck.comp" mor2
             mor' <- composeMorphisms mor1 mor2'
             return (GMorphism r1 sigma1 ind1 mor' startMorId)
           else do
           {- coercion between target of first and
           source of second Grothendieck morphism -}
           mor1' <- coerceMorphism lid2 lid3 "Grothendieck.comp" mor1
           {- map signature morphism component of first Grothendieck morphism
           along the comorphism component of the second one ... -}
           mor1'' <- map_morphism r2 mor1'
           {- and then compose the result with the signature morphism component
           of first one -}
           mor <- composeMorphisms mor1'' mor2
           -- also if the first comorphism is the identity...
           if isIdComorphism (Comorphism r1) &&
             case coerceSublogic lid2 lid3 "Grothendieck.comp"
                                (targetSublogic r1) of
               Just sl1 -> maybe False
                                (isSubElem (targetSublogic r2))
                                (mapSublogic r2 sl1)
               _ -> False
                 -- ... then things simplify ...
             then do
               sigma1' <- coerceSign lid1 lid3 "Grothendieck.comp" sigma1
               return (GMorphism r2 sigma1' ind1 mor startMorId)
             else return $ GMorphism (CompComorphism r1 r2)
                  sigma1 ind1 mor startMorId
    dom (GMorphism r sigma ind _mor _) =
      G_sign (sourceLogic r) sigma ind
    cod (GMorphism r (ExtSign _ _) _ mor _) =
      let lid2 = targetLogic r
          sig2 = cod mor
      in G_sign lid2 (makeExtSign lid2 sig2) startSigId
    isInclusion (GMorphism cid _ _ mor _) =
      isInclusionComorphism cid && isInclusion mor
    legal_mor (GMorphism r (ExtSign s _) _ mor _) = do
      legal_mor mor
      case maybeResult $ map_sign r s of
        Just (sigma', _) | sigma' == cod mor -> return ()
        _ -> Fail.fail "legal_mor.GMorphism2"
  
  -- | Embedding of homogeneous signature morphisms as Grothendieck sig mors
  gEmbed2 :: G_sign -> G_morphism -> GMorphism
  gEmbed2 (G_sign lid2 sig si) (G_morphism lid mor ind) =
    let cid = mkIdComorphism lid (top_sublogic lid)
        Just sig1 = coerceSign lid2 (sourceLogic cid) "gEmbed2" sig
    in GMorphism cid sig1 si mor ind
  
  -- | Embedding of homogeneous signature morphisms as Grothendieck sig mors
  gEmbed :: G_morphism -> GMorphism
  gEmbed (G_morphism lid mor ind) = let sig = dom mor in
    GMorphism (mkIdComorphism lid (top_sublogic lid))
                  (makeExtSign lid sig) startSigId mor ind
  
  -- | Embedding of comorphisms as Grothendieck sig mors
  gEmbedComorphism :: AnyComorphism -> G_sign -> Result GMorphism
  gEmbedComorphism (Comorphism cid) (G_sign lid sig ind) = do
    sig'@(ExtSign s _) <- coerceSign lid (sourceLogic cid) "gEmbedComorphism" sig
    (sigTar, _) <- map_sign cid s
    return (GMorphism cid sig' ind (ide sigTar) startMorId)
  
  -- | heterogeneous union of two Grothendieck signatures
  gsigUnion :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
  gsigUnion lg both gsig1@(G_sign lid1 (ExtSign sigma1 _) _)
            gsig2@(G_sign lid2 (ExtSign sigma2 _) _) =
   if Logic lid1 == Logic lid2
      then homogeneousGsigUnion both gsig1 gsig2
      else do
        (Comorphism cid1, Comorphism cid2) <-
              logicUnion lg (Logic lid1) (Logic lid2)
        let lidS1 = sourceLogic cid1
            lidS2 = sourceLogic cid2
            lidT1 = targetLogic cid1
            lidT2 = targetLogic cid2
        sigma1' <- coercePlainSign lid1 lidS1 "Union of signaturesa" sigma1
        sigma2' <- coercePlainSign lid2 lidS2 "Union of signaturesb" sigma2
        (sigma1'', _) <- map_sign cid1 sigma1'  -- where to put axioms???
        (sigma2'', _) <- map_sign cid2 sigma2'  -- where to put axioms???
        sigma2''' <- coercePlainSign lidT2 lidT1 "Union of signaturesc" sigma2''
        sigma3 <- signature_union lidT1 sigma1'' sigma2'''
        return $ G_sign lidT1 (ExtSign sigma3 $ symset_of lidT1
                              $ if both then sigma3 else sigma2''') startSigId
  
  -- | homogeneous Union of two Grothendieck signatures
  homogeneousGsigUnion :: Bool -> G_sign -> G_sign -> Result G_sign
  homogeneousGsigUnion both (G_sign lid1 sigma1 _) (G_sign lid2 sigma2 _) = do
    sigma2'@(ExtSign sig2 _) <- coerceSign lid2 lid1 "Union of signatures" sigma2
    sigma3@(ExtSign sig3 _) <- ext_signature_union lid1 sigma1 sigma2'
    return $ G_sign lid1
               (if both then sigma3 else ExtSign sig3 $ symset_of lid1 sig2)
           startSigId
  
  homGsigDiff :: G_sign -> G_sign -> Result G_sign
  homGsigDiff (G_sign lid1 (ExtSign s1 _) _) (G_sign lid2 (ExtSign s2 _) _) = do
    s3 <- coercePlainSign lid2 lid1 "hom differerence of signatures" s2
    s4 <- signatureDiff lid1 s1 s3
    return $ G_sign lid1 (makeExtSign lid1 s4) startSigId
  
  -- | union of a list of Grothendieck signatures
  gsigManyUnion :: LogicGraph -> [G_sign] -> Result G_sign
  gsigManyUnion _ [] =
    Fail.fail "union of emtpy list of signatures"
  gsigManyUnion lg (gsigma : gsigmas) =
    foldM (gsigUnion lg True) gsigma gsigmas
  
  -- | homogeneous Union of a list of morphisms
  homogeneousMorManyUnion :: [G_morphism] -> Result G_morphism
  homogeneousMorManyUnion [] =
    Fail.fail "homogeneous union of emtpy list of morphisms"
  homogeneousMorManyUnion (gmor : gmors) =
    foldM ( \ (G_morphism lid2 mor2 _) (G_morphism lid1 mor1 _) -> do
              mor1' <- coerceMorphism lid1 lid2 "homogeneousMorManyUnion" mor1
              mor <- morphism_union lid2 mor1' mor2
              return (G_morphism lid2 mor startMorId)) gmor gmors
  
  -- | intersection of a list of Grothendieck signatures
  gsigManyIntersect :: LogicGraph -> [G_sign] -> Result G_sign
  gsigManyIntersect _ [] =
    Fail.fail "intersection of emtpy list of signatures"
  gsigManyIntersect lg (gsigma : gsigmas) =
    foldM (gsigIntersect lg True) gsigma gsigmas
  
  -- | heterogeneous union of two Grothendieck signatures
  gsigIntersect :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
  gsigIntersect _lg both gsig1@(G_sign lid1 (ExtSign _sigma1 _) _)
            gsig2@(G_sign lid2 (ExtSign _sigma2 _) _) =
   if Logic lid1 == Logic lid2
      then homogeneousGsigIntersect both gsig1 gsig2
      else error "intersection of heterogeneous signatures is not supported yet"
  
  -- | homogeneous intersection of two Grothendieck signatures
  homogeneousGsigIntersect :: Bool -> G_sign -> G_sign -> Result G_sign
  homogeneousGsigIntersect _both (G_sign lid1 sigma1@(ExtSign _sig1 syms1) _) (G_sign lid2 sigma2 _) = do
    sigma2'@(ExtSign sig2 _) <- coerceSign lid2 lid1 "Intersection of signatures" sigma2
    ExtSign sig3 _ <- ext_signature_intersect lid1 sigma1 sigma2'
    let syms2 = symset_of lid1 sig2
        symI = Set.intersection syms1 syms2
    return $ G_sign lid1
               (ExtSign sig3 symI)
           startSigId
  
  -- | inclusion between two logics
  logicInclusion :: LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
  logicInclusion logicGraph l1@(Logic lid1) (Logic lid2) =
       let ln1 = language_name lid1
           ln2 = language_name lid2 in
       if ln1 == ln2 then
         return (idComorphism l1)
        else case Map.lookup (ln1, ln2) (inclusions logicGraph) of
             Just (Comorphism i) ->
                 return (Comorphism i)
             Nothing ->
                 Fail.fail ("No inclusion from " ++ ln1 ++ " to " ++ ln2 ++ " found")
  
  updateMorIndex :: MorId -> GMorphism -> GMorphism
  updateMorIndex i (GMorphism cid sign si mor _) = GMorphism cid sign si mor i
  
  toG_morphism :: GMorphism -> G_morphism
  toG_morphism (GMorphism cid _ _ mor i) = G_morphism (targetLogic cid) mor i
  
  gSigCoerce :: LogicGraph -> G_sign -> AnyLogic
             -> Result (G_sign, AnyComorphism)
  gSigCoerce lg g@(G_sign lid1 sigma1 _) l2@(Logic lid2) =
    if Logic lid1 == Logic lid2
      then return (g, idComorphism l2) else do
      cmor@(Comorphism i) <- logicInclusion lg (Logic lid1) l2
      ExtSign sigma1' sy <-
          coerceSign lid1 (sourceLogic i) "gSigCoerce of signature" sigma1
      (sigma1'', _) <- map_sign i sigma1'
      sys <- return . Set.unions . map (map_symbol i sigma1') $ Set.toList sy
      let lid = targetLogic i
      return (G_sign lid (ExtSign sigma1'' sys) startSigId, cmor)
  
  -- | inclusion morphism between two Grothendieck signatures
  ginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism
  ginclusion = inclusionAux True
  
  inclusionAux :: Bool -> LogicGraph -> G_sign -> G_sign -> Result GMorphism
  inclusionAux guard lg (G_sign lid1 sigma1 ind) (G_sign lid2 sigma2 _) = do
      Comorphism i <- logicInclusion lg (Logic lid1) (Logic lid2)
      ext1@(ExtSign sigma1' _) <-
          coerceSign lid1 (sourceLogic i) "Inclusion of signatures" sigma1
      (sigma1'', _) <- map_sign i sigma1'
      ExtSign sigma2' _ <-
          coerceSign lid2 (targetLogic i) "Inclusion of signatures" sigma2
      mor <- (if guard then inclusion else subsig_inclusion)
          (targetLogic i) sigma1'' sigma2'
      return (GMorphism i ext1 ind mor startMorId)
  
  genCompInclusion :: (G_sign -> G_sign -> Result GMorphism)
                   -> GMorphism -> GMorphism -> Result GMorphism
  genCompInclusion f mor1 mor2 = do
    let sigma1 = cod mor1
        sigma2 = dom mor2
    incl <- f sigma1 sigma2
    mor <- composeMorphisms mor1 incl
    composeMorphisms mor mor2
  
  {- | Composition of two Grothendieck signature morphisms
  with intermediate inclusion -}
  compInclusion :: LogicGraph -> GMorphism -> GMorphism -> Result GMorphism
  compInclusion = genCompInclusion . inclusionAux False
  
  -- | Find compositions of comorphisms starting from a give logic
  -- | use wheted graph of logics to optimize search
  findComorphismPaths :: LogicGraph -> G_sublogics -> [AnyComorphism]
  findComorphismPaths lg gsubl = nubOrd $ findComorphismCompositions lg gsubl
  
  -- | graph representation of the logic graph
  logicGraph2Graph :: LogicGraph
                      -> Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism
  logicGraph2Graph lg =
   let relevantMorphisms = filter (\x -> hasModelExpansion x && isRps x && isEps x) . Map.elems 
                           $ comorphisms lg
   in Graph {
    neighbours = \ (G_sublogics lid sl, c1) ->
    let coerce c = forceCoerceSublogic lid (sourceLogic c)
    in Data.Maybe.mapMaybe
        (\ (Comorphism c) -> maybe Nothing (\ sl1 -> Just (Comorphism c,
         (G_sublogics (targetLogic c) sl1, Just $ Comorphism c)))
                  (mapSublogic c (coerce c sl))) $
        filter (\ (Comorphism c) -> Logic (sourceLogic c) == Logic lid
        && isSubElem (coerce c sl) (sourceSublogic c)
        && (case c1 of
              Just (Comorphism c1') -> show c1' /= show c
              _ -> True)) relevantMorphisms,
    weight = \ (Comorphism c) -> if Logic (sourceLogic c) ==
                                   Logic (targetLogic c) then 1 else 3
   }
  
  -- | finds first comorphism with a matching sublogic
  findComorphism :: Fail.MonadFail m => G_sublogics -> [AnyComorphism] -> m AnyComorphism
  findComorphism _ [] = Fail.fail "No matching comorphism found"
  findComorphism gsl@(G_sublogics lid sub) (Comorphism cid : rest) =
      let l2 = sourceLogic cid in
      if Logic lid == Logic l2
        && isSubElem (forceCoerceSublogic lid l2 sub) (sourceSublogic cid)
      then return $ Comorphism cid
      else findComorphism gsl rest
  
  {- | check transportability of Grothendieck signature morphisms
  (currently returns false for heterogeneous morphisms) -}
  isTransportable :: GMorphism -> Bool
  isTransportable (GMorphism cid _ ind1 mor ind2) =
      ind1 > startSigId && ind2 > startMorId
      && isModelTransportable (Comorphism cid)
      && is_transportable (targetLogic cid) mor
  
  -- * Lax triangles and weakly amalgamable squares of lax triangles
  
  {- a lax triangle looks like:
              laxTarget
    i -------------------------------------> k
                    ^  laxModif
                   | |
    i ------------- > j -------------------> k
         laxFst              laxSnd
  
  and I_k is quasi-semi-exact -}
  
  data LaxTriangle = LaxTriangle {
                       laxModif :: AnyModification,
                       laxFst, laxSnd, laxTarget :: AnyComorphism
                     } deriving (Show, Eq, Ord)
  {- a weakly amalgamable square of lax triangles
  consists of two lax triangles with the same laxTarget -}
  
  data Square = Square {
                   leftTriangle, rightTriangle :: LaxTriangle
                } deriving (Show, Eq, Ord)
  
  -- for deriving Eq, first equality for modifications is needed
  
  mkIdSquare :: AnyLogic -> Square
  mkIdSquare (Logic lid) = let
     idCom = Comorphism (mkIdComorphism lid (top_sublogic lid))
     idMod = idModification idCom
     idTriangle = LaxTriangle {
                   laxModif = idMod,
                   laxFst = idCom,
                   laxSnd = idCom,
                   laxTarget = idCom}
   in Square {leftTriangle = idTriangle, rightTriangle = idTriangle}
  
  mkDefSquare :: AnyComorphism -> Square
  mkDefSquare c1@(Comorphism cid1) = let
    idComS = Comorphism $ mkIdComorphism (sourceLogic cid1) $
             top_sublogic $ sourceLogic cid1
    idComT = Comorphism $ mkIdComorphism (targetLogic cid1) $
             top_sublogic $ targetLogic cid1
    idMod = idModification c1
    lTriangle = LaxTriangle {
                 laxModif = idMod,
                 laxFst = c1,
                 laxSnd = idComS,
                 laxTarget = c1
                }
    rTriangle = LaxTriangle {
                 laxModif = idMod,
                 laxFst = idComT,
                 laxSnd = c1,
                 laxTarget = c1
                }
   in Square {leftTriangle = lTriangle, rightTriangle = rTriangle}
  
  mirrorSquare :: Square -> Square
  mirrorSquare s = Square {
                   leftTriangle = rightTriangle s,
                   rightTriangle = leftTriangle s}
  
  lookupSquare :: AnyComorphism -> AnyComorphism -> LogicGraph -> Result [Square]
  lookupSquare com1 com2 lg = maybe (Fail.fail "lookupSquare") return $ do
    sqL1 <- Map.lookup (com1, com2) $ squares lg
    sqL2 <- Map.lookup (com2, com1) $ squares lg
    return $ nubOrd $ sqL1 ++ map mirrorSquare sqL2
    -- maybe adjusted if comparing AnyModifications change
  
  -- | algo for searching comorphism paths
  weight_limit :: Int
  weight_limit = 4
  
  times_logic_in_branch :: Int
  times_logic_in_branch = 3
  
  data SearchNode = SearchNode
    { nodeId :: Int,
      parentId :: Int,
      logicName :: String,
      -- to check wether comorphism already used in branch
      usedComorphisms :: HSet.HashSet String,
      -- number of time particular logic is used in branch
      timesLogicUsed :: HMap.HashMap String Int,
      -- all comorphism composition in current branch, latest one in the head of the list
      cCompositions :: [AnyComorphism],
      -- name of comorphism though wich we get this node from parent
      comName :: String,
      -- weight of comorphism leading to that node
      comWeight :: Int
    }
    deriving (Show)
  
  data SearchState = SearchState
    {
      searchNodes :: HMap.HashMap Int SearchNode,
      -- ids of nodes who are currently leaves in search tree
      leaves :: HSet.HashSet Int,
      -- distances of nodes in priority queues to root node
      distance :: HMap.HashMap Int Int,
      -- priority queue of nodes according their distances: higher distance - higher priority
      pQueue :: Heap.MinPrioHeap Int Int,
      -- map logic map to comorphis with it as source logic
      logicToComorphisms :: HMap.HashMap String [String],
      -- this field = <last node id in searchNodes> + 1.
      -- used for proper id generation of children nodes
      nextNodeId :: Int
    }
  
  initState :: LogicGraph -> G_sublogics -> SearchState
  initState lg (G_sublogics lid sub) =
    SearchState
      { leaves = HSet.empty,
        searchNodes =
          HMap.fromList
            [ ( 0,
                SearchNode
                  0
                  (-1)
                  (language_name lid)
                  HSet.empty
                  HMap.empty
                  [Comorphism $ mkIdComorphism lid sub]
                  []
                  0
              )
            ],
        distance = HMap.fromList [(0, 0)],
        pQueue = Heap.fromList [(0, 0)],
        logicToComorphisms = mapLogicsToComorphisms lg,
        nextNodeId = 1
      }
  
  findComorphismCompositions :: LogicGraph -> G_sublogics -> [AnyComorphism]
  findComorphismCompositions lg gsubl =
    processSearchState lg (initState lg gsubl)
  
  processSearchState :: LogicGraph -> SearchState -> [AnyComorphism]
  processSearchState lg state@(SearchState ns ls _ pq _ _) = case Heap.view pq of
    Nothing -> getComorphismCompositions ns ls
    Just ((dist, nId), pq') ->
      let curNode =
            fromMaybe
              ( error $
                  printf "processSearchState, incorrect nId=%d" nId
              )
              $ HMap.lookup nId ns
          -- remove parent node from global map of nodes
          -- as we don't need it there anymore so GC can utilize
          -- it if required
          ns' = HMap.delete (parentId curNode) ns
          -- remove parent node from set of leaves and put current node there
          ls' = HSet.insert nId $ HSet.delete (parentId curNode) ls
       in processSearchState lg $
            processNeighbours
              lg
              nId
              dist
              ( state
                  { searchNodes = ns',
                    leaves = ls',
                    pQueue = pq'
                  }
              )
  
  getComorphismCompositions ::
    HMap.HashMap Int SearchNode -> -- nodes of search graph
    HSet.HashSet Int -> -- leaves in this graph
    [AnyComorphism]
  getComorphismCompositions sNodes lvs =
    let res =
          concat $
            map
              ( \i ->
                  let leaf = HMap.lookup i sNodes
                   in reverse $
                        cCompositions $
                          fromMaybe
                            ( error $
                                printf "getComorphismComositions, incorrect i=%d key for HashMap" i
                            )
                            $ leaf
              )
              $ HSet.toList $ lvs
     in res
  
  getComorphism :: LogicGraph -> String -> AnyComorphism
  getComorphism lg cn =
    fromMaybe (error (printf "getComorphism, incorrect comorphismName=%s key for HashMap" cn)) $
      Map.lookup cn (comorphisms lg)
  
  getTargetLogicName :: AnyComorphism -> String
  getTargetLogicName (Comorphism cid) = language_name $ targetLogic cid
  
  -- | given node in tree generate candidate nodes and put them in priority queue
  processNeighbours :: LogicGraph -> Int -> Int -> SearchState -> SearchState
  processNeighbours lg nId dist state@(SearchState ns _ ds pq ltcs nni) =
    let curNode =
          fromMaybe (error $ printf "processNeighbours, incorrect nId=%d key for HashMap" nId) $
            HMap.lookup nId ns
        lName = logicName curNode
        comCandidates = HMap.lookupDefault [] lName ltcs
        comCandidates' = filter (\name -> not $ HSet.member name (usedComorphisms curNode)) comCandidates
        -- create SearchNodes when possible due to restrictions and add ids later
        -- this code can be expressed as map (create_SearchNode) $ filter (can_create_SearchNode?)
        -- but implemented this way without map-filter separation
        childrenNodes =
          catMaybes $
            map
              ( \name ->
                  let c = getComorphism lg name
                      targetLogicName = getTargetLogicName c
                      tlu = HMap.lookupDefault 0 targetLogicName (timesLogicUsed curNode)
                      newComposition =
                        compComorphism (head $ cCompositions curNode) c
                      cw = HMap.lookupDefault (maxWeight + 1) name comorphismWeight
                   in if (isJust newComposition && tlu <= times_logic_in_branch && cw + dist <= weight_limit)
                        then
                          Just $
                            SearchNode
                              { nodeId = -1, -- dummy value for now, changed later in processNeighbours
                                parentId = nId,
                                logicName = targetLogicName,
                                usedComorphisms = HSet.insert name (usedComorphisms curNode),
                                timesLogicUsed = HMap.insert targetLogicName (tlu + 1) (timesLogicUsed curNode),
                                cCompositions = (fromJust newComposition) : (cCompositions curNode),
                                comName = name,
                                comWeight = cw
                              }
                        else Nothing
              )
              comCandidates'
  
        -- add ids to SearchNodes
        (childrenNodes', next_nni) = foldl (\(acc, i) sn -> (sn{ nodeId = i } : acc, i + 1)) ([], nni) childrenNodes
  
        -- update map of nodes
        ns' = foldl (\_ns sn -> HMap.insert (nodeId sn) sn _ns) ns childrenNodes'
        -- update distances in SearchState
        ds' = foldl (\_ds sn -> HMap.insert (nodeId sn) (dist + comWeight sn) _ds) ds childrenNodes'
        -- update priority queue
        pq' = foldl (\_pq sn -> Heap.insert (dist + comWeight sn, nodeId sn) _pq) pq childrenNodes'
     in state {searchNodes = ns', distance = ds', pQueue = pq', nextNodeId = next_nni}
  
  mapLogicsToComorphisms :: LogicGraph -> HMap.HashMap String [String]
  mapLogicsToComorphisms lg =
    foldr
      ( \(cName, Comorphism cId) acc ->
          let sourceLogicName = language_name $ sourceLogic cId
              l = HMap.lookupDefault [] sourceLogicName acc
           in HMap.insert sourceLogicName (cName : l) acc
      )
      HMap.empty
      $ Map.toList $ comorphisms lg
  
  -- | assign weights to comorphisms
  
  maxWeight :: Int
  maxWeight = 5
  
  comorphismWeight :: HMap.HashMap String Int
  comorphismWeight =
    HMap.fromList
      [ ("CASL2CoCASL", 5),
        ("CASL2CspCASL", 5),
        ("CASL2ExtModal", 5),
        ("CASL2HasCASL", 5),
        ("CASL2Hybrid", 5),
        ("CASL2Modal", 5),
        ("CASL2VSE", 5),
        ("CASL2VSEImport", 5),
        ("CASL2VSERefine", 5),
        ("HasCASL2IsabelleDeprecated", 5),
        ("OWL22NeSyPatterns", 5),
        ("CASL_DL2CASL", 4),
        ("CASL2Propositional", 4),
        ("CASL2OWL", 4),
        ("OWL22CommonLogic", 4),
        ("Propositional2CommonLogic", 4),
        ("Propositional2OWL2", 4),
        ("Propositional2QBF", 4),
        ("SoftFOL2CommonLogic", 4),
        ("THFP_P2HasCASL", 3),
        ("CspCASL2Modal", 3),
        ("OWL22CASL", 2),
        ("Propositional2CASL", 2),
        ("CoCASL2Isabelle", 2),
        ("CommonLogic2Isabelle", 2),
        ("CASL2Isabelle", 2),
        ("CommonLogicModuleElimination", 2),
        ("CspCASL2CspCASL_Failure", 2),
        ("CspCASL2CspCASL_Trace", 2),
        ("HasCASL2IsabelleOption", 2),
        ("THFP2THF0", 2),
        ("THFP_P2THFP", 2),
        ("Adl2CASL", 1),
        ("CASL2NNF", 1),
        ("CASL2PCFOL", 1),
        ("CASL2PCFOLTopSort", 1),
        ("CASL2Prenex", 1),
        ("CASL2Skolem", 1),
        ("CASL2SoftFOL", 1),
        ("CASL2SoftFOLInduction", 1),
        ("CASL2SoftFOLInduction2", 1),
        ("CASL2SubCFOL", 1),
        ("CASL2SubCFOLNoMembershipOrCast", 1),
        ("CASL2SubCFOLSubsortBottoms", 1),
        ("CASL2TPTP_FOF", 1),
        ("CLFol2CFOL", 1),
        ("CLFull2CFOL", 1),
        ("CLImp2CFOL", 1),
        ("CLSeq2CFOL", 1),
        ("CoCASL2CoPCFOL", 1),
        ("CoCASL2CoSubCFOL", 1),
        ("CSMOF2CASL", 1),
        ("DFOL2CASL", 1),
        ("DMU2OWL2", 1),
        ("ExtModal2CASL", 1),
        ("ExtModal2ExtModalNoSubsorts", 1),
        ("ExtModal2ExtModalTotal", 1),
        ("ExtModal2HasCASL", 1),
        ("ExtModal2OWL", 1),
        ("ExtModal2OWL", 1),
        ("HasCASL2HasCASLPrograms", 1),
        ("HasCASL2THFP_P", 1),
        ("HolLight2Isabelle", 1),
        ("Hybrid2CASL", 1),
        ("Maude2CASL", 1),
        ("Modal2CASL", 1),
        ("MonadicTranslation", 1),
        ("NormalisingTranslation", 1),
        ("QBF2Propositional", 1),
        ("QVTR2CASL", 1),
        ("RelScheme2CASL", 1)
      ]
  