{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable
  , FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}
{- |
Module      :  ./Logic/Comorphism.hs
Description :  interface and class for logic translations
Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (via Logic)

Central interface (type class) for logic translations (comorphisms) in Hets
   These are just collections of
   functions between (some of) the types of logics.

   References: see Logic.hs
-}

module Logic.Comorphism
    ( CompComorphism (..)
    , InclComorphism
    , inclusion_logic
    , inclusion_source_sublogic
    , inclusion_target_sublogic
    , mkInclComorphism
    , mkIdComorphism
    , Comorphism (..)
    , targetSublogic
    , map_sign
    , wrapMapTheory
    , wrapMapTheoryPossiblyLossy
    , mkTheoryMapping
    , AnyComorphism (..)
    , idComorphism
    , isIdComorphism
    , isModelTransportable
    , hasModelExpansion
    , isEps
    , isRps
    , isWeaklyAmalgamable
    , compComorphism
    ) where

import Logic.Logic
import Logic.Coerce

import Common.AS_Annotation
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.LibName
import Common.ProofUtils
import Common.Result
import qualified Control.Monad.Fail as Fail

import Data.Data
import Data.Maybe
import qualified Data.Set as Set

class (Language cid,
       Logic lid1 sublogics1
        basic_spec1 sentence1 symb_items1 symb_map_items1
        sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
       Logic 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 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
  where
    {- source and target logic and sublogic
    the source sublogic is the maximal one for which the comorphism works -}
    sourceLogic :: cid -> lid1
    sourceSublogic :: cid -> sublogics1
    sourceSublogic cid :: cid
cid = lid1 -> sublogics1
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 -> sublogics
top_sublogic (lid1 -> sublogics1) -> lid1 -> sublogics1
forall a b. (a -> b) -> a -> b
$ cid -> lid1
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 cid
cid
    {- needed for lossy translations. Is stricter than sourceSublogic.
       Should be merged with sourceSublogic once #1706 has been fixed. -}
    sourceSublogicLossy :: cid -> sublogics1
    sourceSublogicLossy = cid -> sublogics1
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 -> sublogics1
sourceSublogic
    minSourceTheory :: cid -> Maybe (LibName, String)
    minSourceTheory _ = Maybe (LibName, String)
forall a. Maybe a
Nothing
    targetLogic :: cid -> lid2
    {- finer information of target sublogics corresponding to source sublogics
    this function must be partial because mapTheory is partial -}
    mapSublogic :: cid -> sublogics1 -> Maybe sublogics2
    mapSublogic cid :: cid
cid _ = sublogics2 -> Maybe sublogics2
forall a. a -> Maybe a
Just (sublogics2 -> Maybe sublogics2) -> sublogics2 -> Maybe sublogics2
forall a b. (a -> b) -> a -> b
$ lid2 -> sublogics2
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 -> sublogics
top_sublogic (lid2 -> sublogics2) -> lid2 -> sublogics2
forall a b. (a -> b) -> a -> b
$ cid -> lid2
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 cid
cid
    {- the translation functions are partial
    because the target may be a sublanguage
    map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
    cover theoroidal comorphisms as well -}
    map_theory :: cid -> (sign1, [Named sentence1])
                      -> Result (sign2, [Named sentence2])
    -- map_theory but also consider sentence marks
    mapMarkedTheory :: cid -> (sign1, [Named sentence1])
                      -> Result (sign2, [Named sentence2])
    mapMarkedTheory cid :: cid
cid (sig :: sign1
sig, sens :: [Named sentence1]
sens) = do
      (sig2 :: sign2
sig2, sens2 :: [Named sentence2]
sens2) <- cid
-> (sign1, [Named sentence1]) -> 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, [Named sentence1]) -> Result (sign2, [Named sentence2])
map_theory cid
cid (sign1
sig, (Named sentence1 -> Named sentence1)
-> [Named sentence1] -> [Named sentence1]
forall a b. (a -> b) -> [a] -> [b]
map Named sentence1 -> Named sentence1
forall s. Named s -> Named s
unmark [Named sentence1]
sens)
      (sign2, [Named sentence2]) -> Result (sign2, [Named sentence2])
forall (m :: * -> *) a. Monad m => a -> m a
return (sign2
sig2, (Named sentence2 -> Named sentence2)
-> [Named sentence2] -> [Named sentence2]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Named sentence2 -> Named sentence2
forall s. String -> Named s -> Named s
markSen (String -> Named sentence2 -> Named sentence2)
-> String -> Named sentence2 -> Named sentence2
forall a b. (a -> b) -> a -> b
$ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid) [Named sentence2]
sens2)
    map_morphism :: cid -> morphism1 -> Result morphism2
    map_morphism = cid -> morphism1 -> Result morphism2
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
mapDefaultMorphism
    map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
          {- also covers semi-comorphisms
          with no sentence translation
          - but these are spans! -}
    map_sentence = cid -> sign1 -> sentence1 -> Result 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 -> sentence1 -> Result sentence2
failMapSentence
    map_symbol :: cid -> sign1 -> symbol1 -> Set.Set symbol2
    map_symbol = cid -> sign1 -> symbol1 -> Set symbol2
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 -> symbol1 -> Set symbol2
errMapSymbol
    extractModel :: cid -> sign1 -> proof_tree2
                 -> Result (sign1, [Named sentence1])
    extractModel cid :: cid
cid _ _ = String -> Result (sign1, [Named sentence1])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail
      (String -> Result (sign1, [Named sentence1]))
-> String -> Result (sign1, [Named sentence1])
forall a b. (a -> b) -> a -> b
$ "extractModel not implemented for comorphism "
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid
    -- properties of comorphisms
    is_model_transportable :: cid -> Bool
    {- a comorphism (\phi, \alpha, \beta) is model-transportable
    if for any signature \Sigma,
    any \Sigma-model M and any \phi(\Sigma)-model N
    for any isomorphism           h : \beta_\Sigma(N) -> M
    there exists an isomorphism   h': N -> M' such that \beta_\Sigma(h') = h -}
    is_model_transportable _ = Bool
False
    has_model_expansion :: cid -> Bool
    has_model_expansion _ = Bool
False
    is_weakly_amalgamable :: cid -> Bool
    is_weakly_amalgamable _ = Bool
False
    constituents :: cid -> [String]
    constituents cid :: cid
cid = [cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid]
    isInclusionComorphism :: cid -> Bool
    isInclusionComorphism _ = Bool
False
    -- reduction preserves satisfaction
    rps :: cid -> Bool
    rps _ = Bool
True
    -- expansion preserves satisfaction
    eps :: cid -> Bool
    eps _ = Bool
True
    -- a comorphism is a generalized theoroidal comorphism (GTC)
    -- if the presence of an axiom in a theory
    -- impacts on the signature of the translated theory along the GTC
    isGTC :: cid -> Bool 
    isGTC _ = Bool
False

targetSublogic :: 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 -> sublogics2
targetSublogic :: cid -> sublogics2
targetSublogic cid :: cid
cid = sublogics2 -> Maybe sublogics2 -> sublogics2
forall a. a -> Maybe a -> a
fromMaybe (lid2 -> sublogics2
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 -> sublogics
top_sublogic (lid2 -> sublogics2) -> lid2 -> sublogics2
forall a b. (a -> b) -> a -> b
$ cid -> lid2
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 cid
cid)
                           (Maybe sublogics2 -> sublogics2) -> Maybe sublogics2 -> sublogics2
forall a b. (a -> b) -> a -> b
$ cid -> sublogics1 -> Maybe sublogics2
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 -> sublogics1 -> Maybe sublogics2
mapSublogic cid
cid (sublogics1 -> Maybe sublogics2) -> sublogics1 -> Maybe sublogics2
forall a b. (a -> b) -> a -> b
$ cid -> sublogics1
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 -> sublogics1
sourceSublogic cid
cid

-- | this function is based on 'map_theory' using no sentences as input
map_sign :: 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 -> sign1 -> Result (sign2, [Named sentence2])
map_sign cid :: cid
cid sign :: sign1
sign = cid
-> (sign1, [Named sentence1]) -> 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, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory cid
cid (sign1
sign, [])

mapDefaultMorphism :: 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
mapDefaultMorphism :: cid -> morphism1 -> Result morphism2
mapDefaultMorphism cid :: cid
cid mor :: morphism1
mor = do
  (sig1 :: sign2
sig1, _) <- 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 -> Result (sign2, [Named sentence2]))
-> sign1 -> Result (sign2, [Named sentence2])
forall a b. (a -> b) -> a -> b
$ morphism1 -> sign1
forall object morphism.
Category object morphism =>
morphism -> object
dom morphism1
mor
  (sig2 :: sign2
sig2, _) <- 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 -> Result (sign2, [Named sentence2]))
-> sign1 -> Result (sign2, [Named sentence2])
forall a b. (a -> b) -> a -> b
$ morphism1 -> sign1
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism1
mor
  lid2 -> sign2 -> sign2 -> Result morphism2
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result morphism
inclusion (cid -> lid2
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 cid
cid) sign2
sig1 sign2
sig2

failMapSentence :: 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 -> sentence1 -> Result sentence2
failMapSentence :: cid -> sign1 -> sentence1 -> Result sentence2
failMapSentence cid :: cid
cid _ _ =
    String -> Result sentence2
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result sentence2) -> String -> Result sentence2
forall a b. (a -> b) -> a -> b
$ "Unsupported sentence translation " String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid -> String
forall a. Show a => a -> String
show cid
cid

errMapSymbol :: 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 -> symbol1 -> Set.Set symbol2
errMapSymbol :: cid -> sign1 -> symbol1 -> Set symbol2
errMapSymbol cid :: cid
cid _ _ = String -> Set symbol2
forall a. HasCallStack => String -> a
error (String -> Set symbol2) -> String -> Set symbol2
forall a b. (a -> b) -> a -> b
$ "no symbol mapping for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid -> String
forall a. Show a => a -> String
show cid
cid

-- | use this function instead of 'mapMarkedTheory'
wrapMapTheoryPossiblyLossy :: 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
            => Bool -> cid -> (sign1, [Named sentence1])
                   -> Result (sign2, [Named sentence2])
wrapMapTheoryPossiblyLossy :: Bool
-> cid
-> (sign1, [Named sentence1])
-> Result (sign2, [Named sentence2])
wrapMapTheoryPossiblyLossy lossy :: Bool
lossy cid :: cid
cid (sign :: sign1
sign, sens :: [Named sentence1]
sens) =
  let res :: Result (sign2, [Named sentence2])
res = cid
-> (sign1, [Named sentence1]) -> 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, [Named sentence1]) -> Result (sign2, [Named sentence2])
mapMarkedTheory cid
cid (sign1
sign, [Named sentence1]
sens)
      lid1 :: lid1
lid1 = cid -> lid1
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 cid
cid
      thDoc :: String
thDoc = Doc -> String
forall a. Show a => a -> String
show ([Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ sign1 -> Doc
forall a. Pretty a => a -> Doc
pretty sign1
sign Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Named sentence1 -> Doc) -> [Named sentence1] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (lid1 -> Named sentence1 -> Doc
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> Named sentence -> Doc
print_named lid1
lid1) [Named sentence1]
sens)
  in
  if AnyComorphism -> Bool
isIdComorphism (AnyComorphism -> Bool) -> AnyComorphism -> Bool
forall a b. (a -> b) -> a -> b
$ cid -> AnyComorphism
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 -> AnyComorphism
Comorphism cid
cid
  then Result (sign2, [Named sentence2])
res
  else let sub :: sublogics1
sub = if Bool
lossy then cid -> sublogics1
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 -> sublogics1
sourceSublogicLossy cid
cid else cid -> sublogics1
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 -> sublogics1
sourceSublogic cid
cid
           sigLog :: sublogics1
sigLog = sign1 -> sublogics1
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic sign1
sign
           senLog :: sublogics1
senLog = (sublogics1 -> sublogics1 -> sublogics1)
-> sublogics1 -> [sublogics1] -> sublogics1
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl sublogics1 -> sublogics1 -> sublogics1
forall l. SemiLatticeWithTop l => l -> l -> l
lub sublogics1
sigLog ([sublogics1] -> sublogics1) -> [sublogics1] -> sublogics1
forall a b. (a -> b) -> a -> b
$ (Named sentence1 -> sublogics1)
-> [Named sentence1] -> [sublogics1]
forall a b. (a -> b) -> [a] -> [b]
map (sentence1 -> sublogics1
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic (sentence1 -> sublogics1)
-> (Named sentence1 -> sentence1) -> Named sentence1 -> sublogics1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named sentence1 -> sentence1
forall s a. SenAttr s a -> s
sentence) [Named sentence1]
sens
           isInSub :: SenAttr item a -> Bool
isInSub s :: SenAttr item a
s = sublogics1 -> sublogics1 -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem (item -> sublogics1
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic (item -> sublogics1) -> item -> sublogics1
forall a b. (a -> b) -> a -> b
$ SenAttr item a -> item
forall s a. SenAttr s a -> s
sentence SenAttr item a
s) sublogics1
sub 
           sensLossy :: [Named sentence1]
sensLossy = (Named sentence1 -> Bool) -> [Named sentence1] -> [Named sentence1]
forall a. (a -> Bool) -> [a] -> [a]
filter Named sentence1 -> Bool
forall item a.
MinSublogic sublogics1 item =>
SenAttr item a -> Bool
isInSub [Named sentence1]
sens
           resLossy :: Result (sign2, [Named sentence2])
resLossy = cid
-> (sign1, [Named sentence1]) -> 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, [Named sentence1]) -> Result (sign2, [Named sentence2])
mapMarkedTheory cid
cid (sign1
sign, [Named sentence1]
sensLossy)
        in if sublogics1 -> sublogics1 -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem sublogics1
senLog sublogics1
sub
                 then Result (sign2, [Named sentence2])
res
                 else
                    if Bool
lossy Bool -> Bool -> Bool
&& sublogics1 -> sublogics1 -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem sublogics1
sigLog sublogics1
sub
                    then Result (sign2, [Named sentence2])
resLossy 
                    else [Diagnosis]
-> Maybe (sign2, [Named sentence2])
-> Result (sign2, [Named sentence2])
forall a. [Diagnosis] -> Maybe a -> Result a
Result
                     [ DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Hint String
thDoc Range
nullRange
                     , DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error
                         ("for '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid String -> String -> String
forall a. [a] -> [a] -> [a]
++
                              "' expected sublogic '" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                              sublogics1 -> String
forall l. SublogicName l => l -> String
sublogicName sublogics1
sub String -> String -> String
forall a. [a] -> [a] -> [a]
++
                              "'\n but found sublogic '" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                              sublogics1 -> String
forall l. SublogicName l => l -> String
sublogicName sublogics1
senLog String -> String -> String
forall a. [a] -> [a] -> [a]
++
                              "' with signature sublogic '" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                              sublogics1 -> String
forall l. SublogicName l => l -> String
sublogicName sublogics1
sigLog String -> String -> String
forall a. [a] -> [a] -> [a]
++ "'") Range
nullRange] Maybe (sign2, [Named sentence2])
forall a. Maybe a
Nothing

wrapMapTheory :: 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, [Named sentence1])
                   -> Result (sign2, [Named sentence2])
wrapMapTheory :: cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory = Bool
-> cid
-> (sign1, [Named sentence1])
-> 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 =>
Bool
-> cid
-> (sign1, [Named sentence1])
-> Result (sign2, [Named sentence2])
wrapMapTheoryPossiblyLossy Bool
False

mkTheoryMapping :: Monad m => (sign1 -> m (sign2, [Named sentence2]))
                   -> (sign1 -> sentence1 -> m sentence2)
                   -> (sign1, [Named sentence1])
                   -> m (sign2, [Named sentence2])
mkTheoryMapping :: (sign1 -> m (sign2, [Named sentence2]))
-> (sign1 -> sentence1 -> m sentence2)
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
mkTheoryMapping mapSig :: sign1 -> m (sign2, [Named sentence2])
mapSig mapSen :: sign1 -> sentence1 -> m sentence2
mapSen (sign :: sign1
sign, sens :: [Named sentence1]
sens) = do
       (sign' :: sign2
sign', sens' :: [Named sentence2]
sens') <- sign1 -> m (sign2, [Named sentence2])
mapSig sign1
sign
       [Named sentence2]
sens'' <- (Named sentence1 -> m (Named sentence2))
-> [Named sentence1] -> m [Named sentence2]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((sentence1 -> m sentence2)
-> Named sentence1 -> m (Named sentence2)
forall (m :: * -> *) s t.
Monad m =>
(s -> m t) -> Named s -> m (Named t)
mapNamedM (sign1 -> sentence1 -> m sentence2
mapSen sign1
sign) (Named sentence1 -> m (Named sentence2))
-> (Named sentence1 -> Named sentence1)
-> Named sentence1
-> m (Named sentence2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named sentence1 -> Named sentence1
forall s. Named s -> Named s
unmark) [Named sentence1]
sens
       (sign2, [Named sentence2]) -> m (sign2, [Named sentence2])
forall (m :: * -> *) a. Monad m => a -> m a
return (sign2
sign', [Named sentence2] -> [Named sentence2]
forall a. [Named a] -> [Named a]
nameAndDisambiguate
         ([Named sentence2] -> [Named sentence2])
-> [Named sentence2] -> [Named sentence2]
forall a b. (a -> b) -> a -> b
$ (Named sentence2 -> Named sentence2)
-> [Named sentence2] -> [Named sentence2]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Named sentence2 -> Named sentence2
forall s. String -> Named s -> Named s
markSen "SignatureProperty") [Named sentence2]
sens' [Named sentence2] -> [Named sentence2] -> [Named sentence2]
forall a. [a] -> [a] -> [a]
++ [Named sentence2]
sens'')

data InclComorphism lid sublogics = InclComorphism
  { InclComorphism lid sublogics -> lid
inclusion_logic :: lid
  , InclComorphism lid sublogics -> sublogics
inclusion_source_sublogic :: sublogics
  , InclComorphism lid sublogics -> sublogics
inclusion_target_sublogic :: sublogics }
  deriving (Int -> InclComorphism lid sublogics -> String -> String
[InclComorphism lid sublogics] -> String -> String
InclComorphism lid sublogics -> String
(Int -> InclComorphism lid sublogics -> String -> String)
-> (InclComorphism lid sublogics -> String)
-> ([InclComorphism lid sublogics] -> String -> String)
-> Show (InclComorphism lid sublogics)
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
forall lid sublogics.
(Show lid, Show sublogics) =>
Int -> InclComorphism lid sublogics -> String -> String
forall lid sublogics.
(Show lid, Show sublogics) =>
[InclComorphism lid sublogics] -> String -> String
forall lid sublogics.
(Show lid, Show sublogics) =>
InclComorphism lid sublogics -> String
showList :: [InclComorphism lid sublogics] -> String -> String
$cshowList :: forall lid sublogics.
(Show lid, Show sublogics) =>
[InclComorphism lid sublogics] -> String -> String
show :: InclComorphism lid sublogics -> String
$cshow :: forall lid sublogics.
(Show lid, Show sublogics) =>
InclComorphism lid sublogics -> String
showsPrec :: Int -> InclComorphism lid sublogics -> String -> String
$cshowsPrec :: forall lid sublogics.
(Show lid, Show sublogics) =>
Int -> InclComorphism lid sublogics -> String -> String
Show, Typeable, Typeable (InclComorphism lid sublogics)
Constr
DataType
Typeable (InclComorphism lid sublogics) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> InclComorphism lid sublogics
 -> c (InclComorphism lid sublogics))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r)
    -> Constr
    -> c (InclComorphism lid sublogics))
-> (InclComorphism lid sublogics -> Constr)
-> (InclComorphism lid sublogics -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d))
    -> Maybe (c (InclComorphism lid sublogics)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (InclComorphism lid sublogics)))
-> ((forall b. Data b => b -> b)
    -> InclComorphism lid sublogics -> InclComorphism lid sublogics)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> InclComorphism lid sublogics
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> InclComorphism lid sublogics
    -> r)
-> (forall u.
    (forall d. Data d => d -> u)
    -> InclComorphism lid sublogics -> [u])
-> (forall u.
    Int
    -> (forall d. Data d => d -> u)
    -> InclComorphism lid sublogics
    -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> InclComorphism lid sublogics
    -> m (InclComorphism lid sublogics))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> InclComorphism lid sublogics
    -> m (InclComorphism lid sublogics))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> InclComorphism lid sublogics
    -> m (InclComorphism lid sublogics))
-> Data (InclComorphism lid sublogics)
InclComorphism lid sublogics -> Constr
InclComorphism lid sublogics -> DataType
(forall b. Data b => b -> b)
-> InclComorphism lid sublogics -> InclComorphism lid sublogics
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> InclComorphism lid sublogics
-> c (InclComorphism lid sublogics)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r)
-> Constr
-> c (InclComorphism lid sublogics)
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InclComorphism lid sublogics))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int
-> (forall d. Data d => d -> u)
-> InclComorphism lid sublogics
-> u
forall u.
(forall d. Data d => d -> u) -> InclComorphism lid sublogics -> [u]
forall lid sublogics.
(Data lid, Data sublogics) =>
Typeable (InclComorphism lid sublogics)
forall lid sublogics.
(Data lid, Data sublogics) =>
InclComorphism lid sublogics -> Constr
forall lid sublogics.
(Data lid, Data sublogics) =>
InclComorphism lid sublogics -> DataType
forall lid sublogics.
(Data lid, Data sublogics) =>
(forall b. Data b => b -> b)
-> InclComorphism lid sublogics -> InclComorphism lid sublogics
forall lid sublogics u.
(Data lid, Data sublogics) =>
Int
-> (forall d. Data d => d -> u)
-> InclComorphism lid sublogics
-> u
forall lid sublogics u.
(Data lid, Data sublogics) =>
(forall d. Data d => d -> u) -> InclComorphism lid sublogics -> [u]
forall lid sublogics r r'.
(Data lid, Data sublogics) =>
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> InclComorphism lid sublogics
-> r
forall lid sublogics r r'.
(Data lid, Data sublogics) =>
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> InclComorphism lid sublogics
-> r
forall lid sublogics (m :: * -> *).
(Data lid, Data sublogics, Monad m) =>
(forall d. Data d => d -> m d)
-> InclComorphism lid sublogics -> m (InclComorphism lid sublogics)
forall lid sublogics (m :: * -> *).
(Data lid, Data sublogics, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> InclComorphism lid sublogics -> m (InclComorphism lid sublogics)
forall lid sublogics (c :: * -> *).
(Data lid, Data sublogics) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r)
-> Constr
-> c (InclComorphism lid sublogics)
forall lid sublogics (c :: * -> *).
(Data lid, Data sublogics) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> InclComorphism lid sublogics
-> c (InclComorphism lid sublogics)
forall lid sublogics (t :: * -> *) (c :: * -> *).
(Data lid, Data sublogics, Typeable t) =>
(forall d. Data d => c (t d))
-> Maybe (c (InclComorphism lid sublogics))
forall lid sublogics (t :: * -> * -> *) (c :: * -> *).
(Data lid, Data sublogics, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InclComorphism lid sublogics))
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> InclComorphism lid sublogics
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> InclComorphism lid sublogics
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> InclComorphism lid sublogics -> m (InclComorphism lid sublogics)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> InclComorphism lid sublogics -> m (InclComorphism lid sublogics)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r)
-> Constr
-> c (InclComorphism lid sublogics)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> InclComorphism lid sublogics
-> c (InclComorphism lid sublogics)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d))
-> Maybe (c (InclComorphism lid sublogics))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InclComorphism lid sublogics))
$cInclComorphism :: Constr
$tInclComorphism :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> InclComorphism lid sublogics -> m (InclComorphism lid sublogics)
$cgmapMo :: forall lid sublogics (m :: * -> *).
(Data lid, Data sublogics, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> InclComorphism lid sublogics -> m (InclComorphism lid sublogics)
gmapMp :: (forall d. Data d => d -> m d)
-> InclComorphism lid sublogics -> m (InclComorphism lid sublogics)
$cgmapMp :: forall lid sublogics (m :: * -> *).
(Data lid, Data sublogics, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> InclComorphism lid sublogics -> m (InclComorphism lid sublogics)
gmapM :: (forall d. Data d => d -> m d)
-> InclComorphism lid sublogics -> m (InclComorphism lid sublogics)
$cgmapM :: forall lid sublogics (m :: * -> *).
(Data lid, Data sublogics, Monad m) =>
(forall d. Data d => d -> m d)
-> InclComorphism lid sublogics -> m (InclComorphism lid sublogics)
gmapQi :: Int
-> (forall d. Data d => d -> u)
-> InclComorphism lid sublogics
-> u
$cgmapQi :: forall lid sublogics u.
(Data lid, Data sublogics) =>
Int
-> (forall d. Data d => d -> u)
-> InclComorphism lid sublogics
-> u
gmapQ :: (forall d. Data d => d -> u) -> InclComorphism lid sublogics -> [u]
$cgmapQ :: forall lid sublogics u.
(Data lid, Data sublogics) =>
(forall d. Data d => d -> u) -> InclComorphism lid sublogics -> [u]
gmapQr :: (r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> InclComorphism lid sublogics
-> r
$cgmapQr :: forall lid sublogics r r'.
(Data lid, Data sublogics) =>
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> InclComorphism lid sublogics
-> r
gmapQl :: (r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> InclComorphism lid sublogics
-> r
$cgmapQl :: forall lid sublogics r r'.
(Data lid, Data sublogics) =>
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> InclComorphism lid sublogics
-> r
gmapT :: (forall b. Data b => b -> b)
-> InclComorphism lid sublogics -> InclComorphism lid sublogics
$cgmapT :: forall lid sublogics.
(Data lid, Data sublogics) =>
(forall b. Data b => b -> b)
-> InclComorphism lid sublogics -> InclComorphism lid sublogics
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InclComorphism lid sublogics))
$cdataCast2 :: forall lid sublogics (t :: * -> * -> *) (c :: * -> *).
(Data lid, Data sublogics, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InclComorphism lid sublogics))
dataCast1 :: (forall d. Data d => c (t d))
-> Maybe (c (InclComorphism lid sublogics))
$cdataCast1 :: forall lid sublogics (t :: * -> *) (c :: * -> *).
(Data lid, Data sublogics, Typeable t) =>
(forall d. Data d => c (t d))
-> Maybe (c (InclComorphism lid sublogics))
dataTypeOf :: InclComorphism lid sublogics -> DataType
$cdataTypeOf :: forall lid sublogics.
(Data lid, Data sublogics) =>
InclComorphism lid sublogics -> DataType
toConstr :: InclComorphism lid sublogics -> Constr
$ctoConstr :: forall lid sublogics.
(Data lid, Data sublogics) =>
InclComorphism lid sublogics -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r)
-> Constr
-> c (InclComorphism lid sublogics)
$cgunfold :: forall lid sublogics (c :: * -> *).
(Data lid, Data sublogics) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r)
-> Constr
-> c (InclComorphism lid sublogics)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> InclComorphism lid sublogics
-> c (InclComorphism lid sublogics)
$cgfoldl :: forall lid sublogics (c :: * -> *).
(Data lid, Data sublogics) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> InclComorphism lid sublogics
-> c (InclComorphism lid sublogics)
$cp1Data :: forall lid sublogics.
(Data lid, Data sublogics) =>
Typeable (InclComorphism lid sublogics)
Data)

-- | construction of an identity comorphism
mkIdComorphism :: (Logic lid sublogics
                      basic_spec sentence symb_items symb_map_items
                      sign morphism symbol raw_symbol proof_tree) =>
                  lid -> sublogics -> InclComorphism lid sublogics
mkIdComorphism :: lid -> sublogics -> InclComorphism lid sublogics
mkIdComorphism lid :: lid
lid sub :: sublogics
sub = InclComorphism :: forall lid sublogics.
lid -> sublogics -> sublogics -> InclComorphism lid sublogics
InclComorphism
  { inclusion_logic :: lid
inclusion_logic = lid
lid
  , inclusion_source_sublogic :: sublogics
inclusion_source_sublogic = sublogics
sub
  , inclusion_target_sublogic :: sublogics
inclusion_target_sublogic = sublogics
sub }

-- | construction of an inclusion comorphism
mkInclComorphism :: (Logic lid sublogics
                           basic_spec sentence symb_items symb_map_items
                           sign morphism symbol raw_symbol proof_tree,
                     Fail.MonadFail m) =>
                    lid -> sublogics -> sublogics
                 -> m (InclComorphism lid sublogics)
mkInclComorphism :: lid -> sublogics -> sublogics -> m (InclComorphism lid sublogics)
mkInclComorphism lid :: lid
lid srcSub :: sublogics
srcSub trgSub :: sublogics
trgSub =
    if sublogics -> sublogics -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem sublogics
srcSub sublogics
trgSub
    then InclComorphism lid sublogics -> m (InclComorphism lid sublogics)
forall (m :: * -> *) a. Monad m => a -> m a
return InclComorphism :: forall lid sublogics.
lid -> sublogics -> sublogics -> InclComorphism lid sublogics
InclComorphism
      { inclusion_logic :: lid
inclusion_logic = lid
lid
      , inclusion_source_sublogic :: sublogics
inclusion_source_sublogic = sublogics
srcSub
      , inclusion_target_sublogic :: sublogics
inclusion_target_sublogic = sublogics
trgSub }
    else String -> m (InclComorphism lid sublogics)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("mkInclComorphism: first sublogic must be a " String -> String -> String
forall a. [a] -> [a] -> [a]
++
               "subElem of the second sublogic")

instance (Language lid, Eq sublogics, Show sublogics, SublogicName sublogics)
    => Language (InclComorphism lid sublogics) where
        language_name :: InclComorphism lid sublogics -> String
language_name (InclComorphism lid :: lid
lid sub_src :: sublogics
sub_src sub_trg :: sublogics
sub_trg) =
            let sblName :: String
sblName = sublogics -> String
forall l. SublogicName l => l -> String
sublogicName sublogics
sub_src
                lname :: String
lname = lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid
            in if sublogics
sub_src sublogics -> sublogics -> Bool
forall a. Eq a => a -> a -> Bool
== sublogics
sub_trg
               then "id_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
lname String -> String -> String
forall a. [a] -> [a] -> [a]
++
                    if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
sblName then "" else '.' Char -> String -> String
forall a. a -> [a] -> [a]
: String
sblName
               else "incl_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
lname String -> String -> String
forall a. [a] -> [a] -> [a]
++ ':'
                    Char -> String -> String
forall a. a -> [a] -> [a]
: String
sblName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "->" String -> String -> String
forall a. [a] -> [a] -> [a]
++ sublogics -> String
forall l. SublogicName l => l -> String
sublogicName sublogics
sub_trg

instance Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree =>
         Comorphism (InclComorphism lid sublogics)
          lid sublogics
          basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree
          lid sublogics
          basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree
         where
           sourceLogic :: InclComorphism lid sublogics -> lid
sourceLogic = InclComorphism lid sublogics -> lid
forall lid sublogics. InclComorphism lid sublogics -> lid
inclusion_logic
           targetLogic :: InclComorphism lid sublogics -> lid
targetLogic = InclComorphism lid sublogics -> lid
forall lid sublogics. InclComorphism lid sublogics -> lid
inclusion_logic
           sourceSublogic :: InclComorphism lid sublogics -> sublogics
sourceSublogic = InclComorphism lid sublogics -> sublogics
forall lid sublogics. InclComorphism lid sublogics -> sublogics
inclusion_source_sublogic
           mapSublogic :: InclComorphism lid sublogics -> sublogics -> Maybe sublogics
mapSublogic cid :: InclComorphism lid sublogics
cid subl :: sublogics
subl =
               if sublogics -> sublogics -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem sublogics
subl (sublogics -> Bool) -> sublogics -> Bool
forall a b. (a -> b) -> a -> b
$ InclComorphism lid sublogics -> sublogics
forall lid sublogics. InclComorphism lid sublogics -> sublogics
inclusion_source_sublogic InclComorphism lid sublogics
cid
               then sublogics -> Maybe sublogics
forall a. a -> Maybe a
Just sublogics
subl
               else Maybe sublogics
forall a. Maybe a
Nothing
           map_theory :: InclComorphism lid sublogics
-> (sign, [Named sentence]) -> Result (sign, [Named sentence])
map_theory _ = (sign, [Named sentence]) -> Result (sign, [Named sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return
           map_morphism :: InclComorphism lid sublogics -> morphism -> Result morphism
map_morphism _ = morphism -> Result morphism
forall (m :: * -> *) a. Monad m => a -> m a
return
           map_sentence :: InclComorphism lid sublogics -> sign -> sentence -> Result sentence
map_sentence _ _ = sentence -> Result sentence
forall (m :: * -> *) a. Monad m => a -> m a
return
           map_symbol :: InclComorphism lid sublogics -> sign -> symbol -> Set symbol
map_symbol _ _ = symbol -> Set symbol
forall a. a -> Set a
Set.singleton
           constituents :: InclComorphism lid sublogics -> [String]
constituents cid :: InclComorphism lid sublogics
cid =
               if InclComorphism lid sublogics -> sublogics
forall lid sublogics. InclComorphism lid sublogics -> sublogics
inclusion_source_sublogic InclComorphism lid sublogics
cid
                      sublogics -> sublogics -> Bool
forall a. Eq a => a -> a -> Bool
== InclComorphism lid sublogics -> sublogics
forall lid sublogics. InclComorphism lid sublogics -> sublogics
inclusion_target_sublogic InclComorphism lid sublogics
cid
               then []
               else [InclComorphism lid sublogics -> String
forall lid. Language lid => lid -> String
language_name InclComorphism lid sublogics
cid]
           is_model_transportable :: InclComorphism lid sublogics -> Bool
is_model_transportable _ = Bool
True
           has_model_expansion :: InclComorphism lid sublogics -> Bool
has_model_expansion _ = Bool
True
           is_weakly_amalgamable :: InclComorphism lid sublogics -> Bool
is_weakly_amalgamable _ = Bool
True
           isInclusionComorphism :: InclComorphism lid sublogics -> Bool
isInclusionComorphism _ = Bool
True

data CompComorphism cid1 cid2 = CompComorphism cid1 cid2
  deriving (Int -> CompComorphism cid1 cid2 -> String -> String
[CompComorphism cid1 cid2] -> String -> String
CompComorphism cid1 cid2 -> String
(Int -> CompComorphism cid1 cid2 -> String -> String)
-> (CompComorphism cid1 cid2 -> String)
-> ([CompComorphism cid1 cid2] -> String -> String)
-> Show (CompComorphism cid1 cid2)
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
forall cid1 cid2.
(Show cid1, Show cid2) =>
Int -> CompComorphism cid1 cid2 -> String -> String
forall cid1 cid2.
(Show cid1, Show cid2) =>
[CompComorphism cid1 cid2] -> String -> String
forall cid1 cid2.
(Show cid1, Show cid2) =>
CompComorphism cid1 cid2 -> String
showList :: [CompComorphism cid1 cid2] -> String -> String
$cshowList :: forall cid1 cid2.
(Show cid1, Show cid2) =>
[CompComorphism cid1 cid2] -> String -> String
show :: CompComorphism cid1 cid2 -> String
$cshow :: forall cid1 cid2.
(Show cid1, Show cid2) =>
CompComorphism cid1 cid2 -> String
showsPrec :: Int -> CompComorphism cid1 cid2 -> String -> String
$cshowsPrec :: forall cid1 cid2.
(Show cid1, Show cid2) =>
Int -> CompComorphism cid1 cid2 -> String -> String
Show, Typeable, Typeable (CompComorphism cid1 cid2)
Constr
DataType
Typeable (CompComorphism cid1 cid2) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> CompComorphism cid1 cid2
 -> c (CompComorphism cid1 cid2))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (CompComorphism cid1 cid2))
-> (CompComorphism cid1 cid2 -> Constr)
-> (CompComorphism cid1 cid2 -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d))
    -> Maybe (c (CompComorphism cid1 cid2)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (CompComorphism cid1 cid2)))
-> ((forall b. Data b => b -> b)
    -> CompComorphism cid1 cid2 -> CompComorphism cid1 cid2)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> CompComorphism cid1 cid2
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> CompComorphism cid1 cid2
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> CompComorphism cid1 cid2 -> [u])
-> (forall u.
    Int
    -> (forall d. Data d => d -> u) -> CompComorphism cid1 cid2 -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2))
-> Data (CompComorphism cid1 cid2)
CompComorphism cid1 cid2 -> Constr
CompComorphism cid1 cid2 -> DataType
(forall b. Data b => b -> b)
-> CompComorphism cid1 cid2 -> CompComorphism cid1 cid2
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> CompComorphism cid1 cid2
-> c (CompComorphism cid1 cid2)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CompComorphism cid1 cid2)
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CompComorphism cid1 cid2))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int
-> (forall d. Data d => d -> u) -> CompComorphism cid1 cid2 -> u
forall u.
(forall d. Data d => d -> u) -> CompComorphism cid1 cid2 -> [u]
forall cid1 cid2.
(Data cid1, Data cid2) =>
Typeable (CompComorphism cid1 cid2)
forall cid1 cid2.
(Data cid1, Data cid2) =>
CompComorphism cid1 cid2 -> Constr
forall cid1 cid2.
(Data cid1, Data cid2) =>
CompComorphism cid1 cid2 -> DataType
forall cid1 cid2.
(Data cid1, Data cid2) =>
(forall b. Data b => b -> b)
-> CompComorphism cid1 cid2 -> CompComorphism cid1 cid2
forall cid1 cid2 u.
(Data cid1, Data cid2) =>
Int
-> (forall d. Data d => d -> u) -> CompComorphism cid1 cid2 -> u
forall cid1 cid2 u.
(Data cid1, Data cid2) =>
(forall d. Data d => d -> u) -> CompComorphism cid1 cid2 -> [u]
forall cid1 cid2 r r'.
(Data cid1, Data cid2) =>
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> CompComorphism cid1 cid2
-> r
forall cid1 cid2 r r'.
(Data cid1, Data cid2) =>
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> CompComorphism cid1 cid2
-> r
forall cid1 cid2 (m :: * -> *).
(Data cid1, Data cid2, Monad m) =>
(forall d. Data d => d -> m d)
-> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2)
forall cid1 cid2 (m :: * -> *).
(Data cid1, Data cid2, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2)
forall cid1 cid2 (c :: * -> *).
(Data cid1, Data cid2) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CompComorphism cid1 cid2)
forall cid1 cid2 (c :: * -> *).
(Data cid1, Data cid2) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> CompComorphism cid1 cid2
-> c (CompComorphism cid1 cid2)
forall cid1 cid2 (t :: * -> *) (c :: * -> *).
(Data cid1, Data cid2, Typeable t) =>
(forall d. Data d => c (t d))
-> Maybe (c (CompComorphism cid1 cid2))
forall cid1 cid2 (t :: * -> * -> *) (c :: * -> *).
(Data cid1, Data cid2, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CompComorphism cid1 cid2))
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> CompComorphism cid1 cid2
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> CompComorphism cid1 cid2
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CompComorphism cid1 cid2)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> CompComorphism cid1 cid2
-> c (CompComorphism cid1 cid2)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d))
-> Maybe (c (CompComorphism cid1 cid2))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CompComorphism cid1 cid2))
$cCompComorphism :: Constr
$tCompComorphism :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2)
$cgmapMo :: forall cid1 cid2 (m :: * -> *).
(Data cid1, Data cid2, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2)
gmapMp :: (forall d. Data d => d -> m d)
-> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2)
$cgmapMp :: forall cid1 cid2 (m :: * -> *).
(Data cid1, Data cid2, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2)
gmapM :: (forall d. Data d => d -> m d)
-> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2)
$cgmapM :: forall cid1 cid2 (m :: * -> *).
(Data cid1, Data cid2, Monad m) =>
(forall d. Data d => d -> m d)
-> CompComorphism cid1 cid2 -> m (CompComorphism cid1 cid2)
gmapQi :: Int
-> (forall d. Data d => d -> u) -> CompComorphism cid1 cid2 -> u
$cgmapQi :: forall cid1 cid2 u.
(Data cid1, Data cid2) =>
Int
-> (forall d. Data d => d -> u) -> CompComorphism cid1 cid2 -> u
gmapQ :: (forall d. Data d => d -> u) -> CompComorphism cid1 cid2 -> [u]
$cgmapQ :: forall cid1 cid2 u.
(Data cid1, Data cid2) =>
(forall d. Data d => d -> u) -> CompComorphism cid1 cid2 -> [u]
gmapQr :: (r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> CompComorphism cid1 cid2
-> r
$cgmapQr :: forall cid1 cid2 r r'.
(Data cid1, Data cid2) =>
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> CompComorphism cid1 cid2
-> r
gmapQl :: (r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> CompComorphism cid1 cid2
-> r
$cgmapQl :: forall cid1 cid2 r r'.
(Data cid1, Data cid2) =>
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> CompComorphism cid1 cid2
-> r
gmapT :: (forall b. Data b => b -> b)
-> CompComorphism cid1 cid2 -> CompComorphism cid1 cid2
$cgmapT :: forall cid1 cid2.
(Data cid1, Data cid2) =>
(forall b. Data b => b -> b)
-> CompComorphism cid1 cid2 -> CompComorphism cid1 cid2
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CompComorphism cid1 cid2))
$cdataCast2 :: forall cid1 cid2 (t :: * -> * -> *) (c :: * -> *).
(Data cid1, Data cid2, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CompComorphism cid1 cid2))
dataCast1 :: (forall d. Data d => c (t d))
-> Maybe (c (CompComorphism cid1 cid2))
$cdataCast1 :: forall cid1 cid2 (t :: * -> *) (c :: * -> *).
(Data cid1, Data cid2, Typeable t) =>
(forall d. Data d => c (t d))
-> Maybe (c (CompComorphism cid1 cid2))
dataTypeOf :: CompComorphism cid1 cid2 -> DataType
$cdataTypeOf :: forall cid1 cid2.
(Data cid1, Data cid2) =>
CompComorphism cid1 cid2 -> DataType
toConstr :: CompComorphism cid1 cid2 -> Constr
$ctoConstr :: forall cid1 cid2.
(Data cid1, Data cid2) =>
CompComorphism cid1 cid2 -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CompComorphism cid1 cid2)
$cgunfold :: forall cid1 cid2 (c :: * -> *).
(Data cid1, Data cid2) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CompComorphism cid1 cid2)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> CompComorphism cid1 cid2
-> c (CompComorphism cid1 cid2)
$cgfoldl :: forall cid1 cid2 (c :: * -> *).
(Data cid1, Data cid2) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> CompComorphism cid1 cid2
-> c (CompComorphism cid1 cid2)
$cp1Data :: forall cid1 cid2.
(Data cid1, Data cid2) =>
Typeable (CompComorphism cid1 cid2)
Data)

instance (Language cid1, Language cid2)
          => Language (CompComorphism cid1 cid2) where
   language_name :: CompComorphism cid1 cid2 -> String
language_name (CompComorphism cid1 :: cid1
cid1 cid2 :: cid2
cid2) =
     cid1 -> String
forall lid. Language lid => lid -> String
language_name cid1
cid1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ ";" String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid2 -> String
forall lid. Language lid => lid -> String
language_name cid2
cid2

instance (Comorphism cid1
            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 cid2
            lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
                sign4 morphism4 symbol4 raw_symbol4 proof_tree4
            lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
                sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
          => Comorphism (CompComorphism cid1 cid2)
              lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
              sign1 morphism1 symbol1 raw_symbol1 proof_tree1
              lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
              sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
   sourceLogic :: CompComorphism cid1 cid2 -> lid1
sourceLogic (CompComorphism cid1 :: cid1
cid1 _) =
     cid1 -> lid1
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
cid1
   targetLogic :: CompComorphism cid1 cid2 -> lid3
targetLogic (CompComorphism _ cid2 :: cid2
cid2) =
     cid2 -> lid3
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 cid2
cid2
   sourceSublogic :: CompComorphism cid1 cid2 -> sublogics1
sourceSublogic (CompComorphism cid1 :: cid1
cid1 _) =
     cid1 -> sublogics1
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 -> sublogics1
sourceSublogic cid1
cid1
   mapSublogic :: CompComorphism cid1 cid2 -> sublogics1 -> Maybe sublogics3
mapSublogic (CompComorphism cid1 :: cid1
cid1 cid2 :: cid2
cid2) sl :: sublogics1
sl =
         cid1 -> sublogics1 -> Maybe sublogics2
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 -> sublogics1 -> Maybe sublogics2
mapSublogic cid1
cid1 sublogics1
sl Maybe sublogics2
-> (sublogics2 -> Maybe sublogics3) -> Maybe sublogics3
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
           cid2 -> sublogics4 -> Maybe sublogics3
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 -> sublogics1 -> Maybe sublogics2
mapSublogic cid2
cid2 (sublogics4 -> Maybe sublogics3)
-> (sublogics2 -> sublogics4) -> sublogics2 -> Maybe sublogics3
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            lid2 -> lid4 -> sublogics2 -> sublogics4
forall 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.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
lid1 -> lid2 -> sublogics1 -> sublogics2
forceCoerceSublogic (cid1 -> lid2
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) (cid2 -> lid4
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 cid2
cid2)
   map_sentence :: CompComorphism cid1 cid2 -> sign1 -> sentence1 -> Result sentence3
map_sentence (CompComorphism cid1 :: cid1
cid1 cid2 :: cid2
cid2) si1 :: sign1
si1 se1 :: sentence1
se1 =
         do (si2 :: sign2
si2, _) <- cid1 -> 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 cid1
cid1 sign1
si1
            sentence2
se2 <- cid1 -> sign1 -> sentence1 -> Result 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 -> sentence1 -> Result sentence2
map_sentence cid1
cid1 sign1
si1 sentence1
se1
            (si2' :: sign4
si2', se2' :: [Named sentence4]
se2') <- lid2
-> lid4
-> String
-> (sign2, [Named sentence2])
-> Result (sign4, [Named sentence4])
forall 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 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory
                (cid1 -> lid2
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) (cid2 -> lid4
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 cid2
cid2)
                "Mapping sentence along comorphism" (sign2
si2, [String -> sentence2 -> Named sentence2
forall a s. a -> s -> SenAttr s a
makeNamed "" sentence2
se2])
            case [Named sentence4]
se2' of
                [x :: Named sentence4
x] -> cid2 -> sign4 -> sentence4 -> Result sentence3
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 -> sentence1 -> Result sentence2
map_sentence cid2
cid2 sign4
si2' (sentence4 -> Result sentence3) -> sentence4 -> Result sentence3
forall a b. (a -> b) -> a -> b
$ Named sentence4 -> sentence4
forall s a. SenAttr s a -> s
sentence Named sentence4
x
                _ -> String -> Result sentence3
forall a. HasCallStack => String -> a
error "CompComorphism.map_sentence"

   map_theory :: CompComorphism cid1 cid2
-> (sign1, [Named sentence1]) -> Result (sign3, [Named sentence3])
map_theory (CompComorphism cid1 :: cid1
cid1 cid2 :: cid2
cid2) ti1 :: (sign1, [Named sentence1])
ti1 =
         do (sign2, [Named sentence2])
ti2 <- cid1
-> (sign1, [Named sentence1]) -> 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, [Named sentence1]) -> Result (sign2, [Named sentence2])
map_theory cid1
cid1 (sign1, [Named sentence1])
ti1
            (sign4, [Named sentence4])
ti2' <- lid2
-> lid4
-> String
-> (sign2, [Named sentence2])
-> Result (sign4, [Named sentence4])
forall 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 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory (cid1 -> lid2
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) (cid2 -> lid4
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 cid2
cid2)
                        "Mapping theory along comorphism" (sign2, [Named sentence2])
ti2
            cid2
-> (sign4, [Named sentence4]) -> Result (sign3, [Named sentence3])
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, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory cid2
cid2 (sign4, [Named sentence4])
ti2'

   map_morphism :: CompComorphism cid1 cid2 -> morphism1 -> Result morphism3
map_morphism (CompComorphism cid1 :: cid1
cid1 cid2 :: cid2
cid2) m1 :: morphism1
m1 =
       do morphism2
m2 <- cid1 -> morphism1 -> Result morphism2
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 cid1
cid1 morphism1
m1
          morphism4
m3 <- lid2 -> lid4 -> String -> morphism2 -> Result morphism4
forall 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 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> String -> morphism1 -> m morphism2
coerceMorphism (cid1 -> lid2
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) (cid2 -> lid4
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 cid2
cid2)
                  "Mapping signature morphism along comorphism" morphism2
m2
          cid2 -> morphism4 -> Result morphism3
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 cid2
cid2 morphism4
m3

   map_symbol :: CompComorphism cid1 cid2 -> sign1 -> symbol1 -> Set symbol3
map_symbol (CompComorphism cid1 :: cid1
cid1 cid2 :: cid2
cid2) sig1 :: sign1
sig1 = let
     th :: Result (sign2, [Named sentence2])
th = cid1 -> 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 cid1
cid1 sign1
sig1 in
    case Result (sign2, [Named sentence2])
-> Maybe (sign2, [Named sentence2])
forall a. Result a -> Maybe a
maybeResult Result (sign2, [Named sentence2])
th of
     Nothing -> String -> symbol1 -> Set symbol3
forall a. HasCallStack => String -> a
error "failed translating signature"
     Just (sig2' :: sign2
sig2', _) -> let
       th2 :: Result (sign4, [Named sentence4])
th2 = lid2
-> lid4
-> String
-> (sign2, [Named sentence2])
-> Result (sign4, [Named sentence4])
forall 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 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory
                (cid1 -> lid2
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) (cid2 -> lid4
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 cid2
cid2)
                "Mapping symbol along comorphism" (sign2
sig2', [])
       in case Result (sign4, [Named sentence4])
-> Maybe (sign4, [Named sentence4])
forall a. Result a -> Maybe a
maybeResult Result (sign4, [Named sentence4])
th2 of
           Nothing -> String -> symbol1 -> Set symbol3
forall a. HasCallStack => String -> a
error "failed coercing"
           Just (sig2 :: sign4
sig2, _) ->
            \ s1 :: symbol1
s1 ->
              let mycast :: symbol2 -> symbol4
mycast = lid2 -> lid4 -> symbol2 -> symbol4
forall 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.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
lid1 -> lid2 -> symbol1 -> symbol2
coerceSymbol (cid1 -> lid2
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) (cid2 -> lid4
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 cid2
cid2)
              in [Set symbol3] -> Set symbol3
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
                ((symbol2 -> Set symbol3) -> [symbol2] -> [Set symbol3]
forall a b. (a -> b) -> [a] -> [b]
map (cid2 -> sign4 -> symbol4 -> Set symbol3
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 -> symbol1 -> Set symbol2
map_symbol cid2
cid2 sign4
sig2 (symbol4 -> Set symbol3)
-> (symbol2 -> symbol4) -> symbol2 -> Set symbol3
forall b c a. (b -> c) -> (a -> b) -> a -> c
. symbol2 -> symbol4
mycast)
                 (Set symbol2 -> [symbol2]
forall a. Set a -> [a]
Set.toList (cid1 -> sign1 -> symbol1 -> Set symbol2
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 -> symbol1 -> Set symbol2
map_symbol cid1
cid1 sign1
sig1 symbol1
s1)))

   extractModel :: CompComorphism cid1 cid2
-> sign1 -> proof_tree3 -> Result (sign1, [Named sentence1])
extractModel (CompComorphism cid1 :: cid1
cid1 cid2 :: cid2
cid2) sign :: sign1
sign pt3 :: proof_tree3
pt3 =
     let lid1 :: lid1
lid1 = cid1 -> lid1
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
cid1
         lid3 :: lid4
lid3 = cid2 -> lid4
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 cid2
cid2
     in if lid1 -> String
forall lid. Language lid => lid -> String
language_name lid1
lid1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== lid4 -> String
forall lid. Language lid => lid -> String
language_name lid4
lid3 then do
         (sign2, [Named sentence2])
bTh1 <- cid1 -> 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 cid1
cid1 sign1
sign
         (sign1 :: sign4
sign1, _) <-
           lid2
-> lid4
-> String
-> (sign2, [Named sentence2])
-> Result (sign4, [Named sentence4])
forall 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 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory (cid1 -> lid2
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) lid4
lid3 "extractModel1" (sign2, [Named sentence2])
bTh1
         (sign4, [Named sentence4])
bTh2 <- cid2 -> sign4 -> proof_tree3 -> 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 -> proof_tree2 -> Result (sign1, [Named sentence1])
extractModel cid2
cid2 sign4
sign1 proof_tree3
pt3
         lid4
-> lid1
-> String
-> (sign4, [Named sentence4])
-> Result (sign1, [Named sentence1])
forall 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 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid4
lid3 lid1
lid1 "extractModel2" (sign4, [Named sentence4])
bTh2
     else String -> Result (sign1, [Named sentence1])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (sign1, [Named sentence1]))
-> String -> Result (sign1, [Named sentence1])
forall a b. (a -> b) -> a -> b
$ "extractModel not implemented for comorphism composition with "
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid1 -> String
forall lid. Language lid => lid -> String
language_name cid1
cid1
   constituents :: CompComorphism cid1 cid2 -> [String]
constituents (CompComorphism cid1 :: cid1
cid1 cid2 :: cid2
cid2) =
      cid1 -> [String]
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 -> [String]
constituents cid1
cid1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ cid2 -> [String]
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 -> [String]
constituents cid2
cid2

   is_model_transportable :: CompComorphism cid1 cid2 -> Bool
is_model_transportable (CompComorphism cid1 :: cid1
cid1 cid2 :: cid2
cid2) =
       cid1 -> Bool
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 -> Bool
is_model_transportable cid1
cid1 Bool -> Bool -> Bool
&& cid2 -> Bool
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 -> Bool
is_model_transportable cid2
cid2

   has_model_expansion :: CompComorphism cid1 cid2 -> Bool
has_model_expansion (CompComorphism cid1 :: cid1
cid1 cid2 :: cid2
cid2) =
        cid1 -> Bool
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 -> Bool
has_model_expansion cid1
cid1 Bool -> Bool -> Bool
&& cid2 -> Bool
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 -> Bool
has_model_expansion cid2
cid2

   is_weakly_amalgamable :: CompComorphism cid1 cid2 -> Bool
is_weakly_amalgamable (CompComorphism cid1 :: cid1
cid1 cid2 :: cid2
cid2) =
        cid1 -> Bool
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 -> Bool
is_weakly_amalgamable cid1
cid1 Bool -> Bool -> Bool
&& cid2 -> Bool
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 -> Bool
is_weakly_amalgamable cid2
cid2
   isInclusionComorphism :: CompComorphism cid1 cid2 -> Bool
isInclusionComorphism (CompComorphism cid1 :: cid1
cid1 cid2 :: cid2
cid2) =
       cid1 -> Bool
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 -> Bool
isInclusionComorphism cid1
cid1 Bool -> Bool -> Bool
&& cid2 -> Bool
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 -> Bool
isInclusionComorphism cid2
cid2

-- * Comorphisms and existential types for the logic graph

-- | Existential type for comorphisms
data AnyComorphism = 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 =>
      Comorphism cid deriving Typeable -- used for GTheory

instance Eq AnyComorphism where
    a :: AnyComorphism
a == :: AnyComorphism -> AnyComorphism -> Bool
== b :: AnyComorphism
b = AnyComorphism -> AnyComorphism -> Ordering
forall a. Ord a => a -> a -> Ordering
compare AnyComorphism
a AnyComorphism
b Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord AnyComorphism where
  compare :: AnyComorphism -> AnyComorphism -> Ordering
compare (Comorphism cid1 :: cid
cid1) (Comorphism cid2 :: cid
cid2) = (String, [String]) -> (String, [String]) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
     (cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid1, cid -> [String]
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 -> [String]
constituents cid
cid1)
     (cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid2, cid -> [String]
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 -> [String]
constituents cid
cid2)
  -- maybe needs to be refined, using comorphism translations?

instance Show AnyComorphism where
  show :: AnyComorphism -> String
show (Comorphism cid :: cid
cid) = cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ " : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ lid1 -> String
forall lid. Language lid => lid -> String
language_name (cid -> lid1
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 cid
cid)
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ lid2 -> String
forall lid. Language lid => lid -> String
language_name (cid -> lid2
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 cid
cid)

instance Pretty AnyComorphism where
  pretty :: AnyComorphism -> Doc
pretty = String -> Doc
text (String -> Doc)
-> (AnyComorphism -> String) -> AnyComorphism -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnyComorphism -> String
forall a. Show a => a -> String
show

-- | compute the identity comorphism for a logic
idComorphism :: AnyLogic -> AnyComorphism
idComorphism :: AnyLogic -> AnyComorphism
idComorphism (Logic lid :: lid
lid) = InclComorphism lid sublogics -> AnyComorphism
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 -> AnyComorphism
Comorphism (lid -> sublogics -> InclComorphism lid 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 =>
lid -> sublogics -> InclComorphism lid sublogics
mkIdComorphism lid
lid (lid -> 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 =>
lid -> sublogics
top_sublogic lid
lid))

-- | Test whether a comporphism is the identity
isIdComorphism :: AnyComorphism -> Bool
isIdComorphism :: AnyComorphism -> Bool
isIdComorphism (Comorphism cid :: cid
cid) = [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ cid -> [String]
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 -> [String]
constituents cid
cid

-- * Properties of comorphisms

-- | Test whether a comorphism is model-transportable
isModelTransportable :: AnyComorphism -> Bool
isModelTransportable :: AnyComorphism -> Bool
isModelTransportable (Comorphism cid :: cid
cid) = cid -> Bool
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 -> Bool
is_model_transportable cid
cid

-- | Test whether a comorphism has model expansion
hasModelExpansion :: AnyComorphism -> Bool
hasModelExpansion :: AnyComorphism -> Bool
hasModelExpansion (Comorphism cid :: cid
cid) = cid -> Bool
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 -> Bool
has_model_expansion cid
cid

-- | Test whether a comorphism is weakly amalgamable
isWeaklyAmalgamable :: AnyComorphism -> Bool
isWeaklyAmalgamable :: AnyComorphism -> Bool
isWeaklyAmalgamable (Comorphism cid :: cid
cid) = cid -> Bool
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 -> Bool
is_weakly_amalgamable cid
cid

-- | Tests whether a comorphism is rps or eps

isEps :: AnyComorphism -> Bool
isEps :: AnyComorphism -> Bool
isEps (Comorphism cid :: cid
cid) = cid -> Bool
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 -> Bool
eps cid
cid

isRps :: AnyComorphism -> Bool
isRps :: AnyComorphism -> Bool
isRps (Comorphism cid :: cid
cid) = cid -> Bool
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 -> Bool
rps cid
cid


-- | Compose comorphisms
compComorphism :: Fail.MonadFail m => AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism :: AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (Comorphism cid1 :: cid
cid1) (Comorphism cid2 :: cid
cid2) =
   let l1 :: lid2
l1 = cid -> lid2
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 cid
cid1
       l2 :: lid1
l2 = cid -> lid1
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 cid
cid2
       msg :: String
msg = "ogic mismatch in composition of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid1
                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ " and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid2
   in
   if lid2 -> String
forall lid. Language lid => lid -> String
language_name lid2
l1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== lid1 -> String
forall lid. Language lid => lid -> String
language_name lid1
l2 then
      if sublogics1 -> sublogics1 -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem (lid2 -> lid1 -> sublogics2 -> sublogics1
forall 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.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
lid1 -> lid2 -> sublogics1 -> sublogics2
forceCoerceSublogic lid2
l1 lid1
l2 (sublogics2 -> sublogics1) -> sublogics2 -> sublogics1
forall a b. (a -> b) -> a -> b
$ cid -> sublogics2
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 -> sublogics2
targetSublogic cid
cid1)
            (sublogics1 -> Bool) -> sublogics1 -> Bool
forall a b. (a -> b) -> a -> b
$ cid -> sublogics1
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 -> sublogics1
sourceSublogic cid
cid2
       then AnyComorphism -> m AnyComorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyComorphism -> m AnyComorphism)
-> AnyComorphism -> m AnyComorphism
forall a b. (a -> b) -> a -> b
$ CompComorphism cid cid -> AnyComorphism
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 -> AnyComorphism
Comorphism (cid -> cid -> CompComorphism cid cid
forall cid1 cid2. cid1 -> cid2 -> CompComorphism cid1 cid2
CompComorphism cid
cid1 cid
cid2)
       else String -> m AnyComorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m AnyComorphism) -> String -> m AnyComorphism
forall a b. (a -> b) -> a -> b
$ "Subl" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (Expected sublogic "
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ sublogics1 -> String
forall l. SublogicName l => l -> String
sublogicName (cid -> sublogics1
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 -> sublogics1
sourceSublogic cid
cid2)
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ " but found sublogic "
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ sublogics2 -> String
forall l. SublogicName l => l -> String
sublogicName (cid -> sublogics2
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 -> sublogics2
targetSublogic cid
cid1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
    else String -> m AnyComorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m AnyComorphism) -> String -> m AnyComorphism
forall a b. (a -> b) -> a -> b
$ 'L' Char -> String -> String
forall a. a -> [a] -> [a]
: String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (Expected logic "
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ lid1 -> String
forall lid. Language lid => lid -> String
language_name lid1
l2
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ " but found logic "
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ lid2 -> String
forall lid. Language lid => lid -> String
language_name lid2
l1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"