{-# LANGUAGE ExistentialQuantification, MultiParamTypeClasses
 , DeriveDataTypeable, GeneralizedNewtypeDeriving #-}
{- |
Module      :  ./Logic/Grothendieck.hs
Description :  Grothendieck logic (flattening of logic graph to a single logic)
Copyright   :  (c) Till Mossakowski, and Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (overlapping instances, dynamics, existentials)

Grothendieck logic (flattening of logic graph to a single logic)

The Grothendieck logic is defined to be the
   heterogeneous logic over the logic graph.
   This will be the logic over which the data
   structures and algorithms for specification in-the-large
   are built.

   This module heavily works with existential types, see
   <http://haskell.org/hawiki/ExistentialTypes> and chapter 7 of /Heterogeneous
   specification and the heterogeneous tool set/
   (<http://www.informatik.uni-bremen.de/~till/papers/habil.ps>).

   References:

   R. Diaconescu:
   Grothendieck institutions
   J. applied categorical structures 10, 2002, p. 383-402.

   T. Mossakowski:
   Comorphism-based Grothendieck institutions.
   In K. Diks, W. Rytter (Eds.), Mathematical foundations of computer science,
   LNCS 2420, pp. 593-604

   T. Mossakowski:
   Heterogeneous specification and the heterogeneous tool set.
-}

module Logic.Grothendieck
  ( G_basic_spec (..)
  , G_sign (..)
  , SigId (..)
  , startSigId
  , isHomSubGsign
  , isSubGsign
  , logicOfGsign
  , symsOfGsign
  , G_symbolmap (..)
  , G_mapofsymbol (..)
  , G_symbol (..)
  , G_symb_items_list (..)
  , G_symb_map_items_list (..)
  , G_sublogics (..)
  , isSublogic
  , isProperSublogic
  , joinSublogics
  , G_morphism (..)
  , MorId (..)
  , startMorId
  , mkG_morphism
  , lessSublogicComor
  , LogicGraph (..)
  , setCurLogic
  , setSyntax
  , setCurSublogic
  , emptyLogicGraph
  , lookupLogic
  , lookupCurrentLogic
  , lookupCurrentSyntax
  , lookupCompComorphism
  , lookupComorphism
  , lookupModification
  , GMorphism (..)
  , isHomogeneous
  , Grothendieck (..)
  , gEmbed
  , gEmbed2
  , gEmbedComorphism
  , homGsigDiff
  , gsigUnion
  , gsigManyUnion
  , gsigManyIntersect
  , homogeneousMorManyUnion
  , logicInclusion
  , logicUnion
  , updateMorIndex
  , toG_morphism
  , gSigCoerce
  , ginclusion
  , compInclusion
  , findComorphismPaths
  , logicGraph2Graph
  , findComorphism
  , isTransportable
  , Square (..)
  , LaxTriangle (..)
  , mkIdSquare
  , mkDefSquare
  , mirrorSquare
  , lookupSquare
  ) where

import Logic.Coerce
import Logic.Comorphism
import Logic.ExtSign
import Logic.Logic
import Logic.Modification
import Logic.Morphism

import ATerm.Lib

import Common.Doc
import Common.DocUtils
import Common.ExtSign
import Common.Id
import Common.IRI (IRI)
import Common.Lexer
import Common.Parsec
import Common.Result
import Common.Token
import Common.Utils
import Common.LibName
import Common.GraphAlgo

import Control.Monad (foldM)
import qualified Control.Monad.Fail as Fail
import Data.Maybe
import Data.Typeable
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap
import qualified Data.HashSet as HSet
import qualified Data.Heap as Heap

import Text.Printf

import Text.ParserCombinators.Parsec (Parser, parse, eof, (<|>))
-- for looking up modifications

-- * \"Grothendieck\" versions of the various parts of type class Logic

-- | Grothendieck basic specifications
data G_basic_spec = forall lid sublogics
        basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree .
        Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree =>
  G_basic_spec lid basic_spec
  deriving Typeable

instance Show G_basic_spec where
    show :: G_basic_spec -> String
show (G_basic_spec _ s :: basic_spec
s) = basic_spec -> String
forall a. Show a => a -> String
show basic_spec
s

instance Pretty G_basic_spec where
    pretty :: G_basic_spec -> Doc
pretty (G_basic_spec _ s :: basic_spec
s) = basic_spec -> Doc
forall a. Pretty a => a -> Doc
pretty basic_spec
s

instance GetRange G_basic_spec

-- dummy instances for development graphs
instance Ord G_basic_spec where
  compare :: G_basic_spec -> G_basic_spec -> Ordering
compare _ _ = Ordering
EQ

instance Eq G_basic_spec where
  _ == :: G_basic_spec -> G_basic_spec -> Bool
== _ = Bool
True

-- | index for signatures
newtype SigId = SigId Int
  deriving (Typeable, Int -> SigId -> ShowS
[SigId] -> ShowS
SigId -> String
(Int -> SigId -> ShowS)
-> (SigId -> String) -> ([SigId] -> ShowS) -> Show SigId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SigId] -> ShowS
$cshowList :: [SigId] -> ShowS
show :: SigId -> String
$cshow :: SigId -> String
showsPrec :: Int -> SigId -> ShowS
$cshowsPrec :: Int -> SigId -> ShowS
Show, SigId -> SigId -> Bool
(SigId -> SigId -> Bool) -> (SigId -> SigId -> Bool) -> Eq SigId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SigId -> SigId -> Bool
$c/= :: SigId -> SigId -> Bool
== :: SigId -> SigId -> Bool
$c== :: SigId -> SigId -> Bool
Eq, Eq SigId
Eq SigId =>
(SigId -> SigId -> Ordering)
-> (SigId -> SigId -> Bool)
-> (SigId -> SigId -> Bool)
-> (SigId -> SigId -> Bool)
-> (SigId -> SigId -> Bool)
-> (SigId -> SigId -> SigId)
-> (SigId -> SigId -> SigId)
-> Ord SigId
SigId -> SigId -> Bool
SigId -> SigId -> Ordering
SigId -> SigId -> SigId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SigId -> SigId -> SigId
$cmin :: SigId -> SigId -> SigId
max :: SigId -> SigId -> SigId
$cmax :: SigId -> SigId -> SigId
>= :: SigId -> SigId -> Bool
$c>= :: SigId -> SigId -> Bool
> :: SigId -> SigId -> Bool
$c> :: SigId -> SigId -> Bool
<= :: SigId -> SigId -> Bool
$c<= :: SigId -> SigId -> Bool
< :: SigId -> SigId -> Bool
$c< :: SigId -> SigId -> Bool
compare :: SigId -> SigId -> Ordering
$ccompare :: SigId -> SigId -> Ordering
$cp1Ord :: Eq SigId
Ord, Int -> SigId
SigId -> Int
SigId -> [SigId]
SigId -> SigId
SigId -> SigId -> [SigId]
SigId -> SigId -> SigId -> [SigId]
(SigId -> SigId)
-> (SigId -> SigId)
-> (Int -> SigId)
-> (SigId -> Int)
-> (SigId -> [SigId])
-> (SigId -> SigId -> [SigId])
-> (SigId -> SigId -> [SigId])
-> (SigId -> SigId -> SigId -> [SigId])
-> Enum SigId
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: SigId -> SigId -> SigId -> [SigId]
$cenumFromThenTo :: SigId -> SigId -> SigId -> [SigId]
enumFromTo :: SigId -> SigId -> [SigId]
$cenumFromTo :: SigId -> SigId -> [SigId]
enumFromThen :: SigId -> SigId -> [SigId]
$cenumFromThen :: SigId -> SigId -> [SigId]
enumFrom :: SigId -> [SigId]
$cenumFrom :: SigId -> [SigId]
fromEnum :: SigId -> Int
$cfromEnum :: SigId -> Int
toEnum :: Int -> SigId
$ctoEnum :: Int -> SigId
pred :: SigId -> SigId
$cpred :: SigId -> SigId
succ :: SigId -> SigId
$csucc :: SigId -> SigId
Enum, Typeable SigId
Typeable SigId =>
(ATermTable -> SigId -> IO (ATermTable, Int))
-> (ATermTable -> [SigId] -> IO (ATermTable, Int))
-> (Int -> ATermTable -> (ATermTable, SigId))
-> (Int -> ATermTable -> (ATermTable, [SigId]))
-> ShATermConvertible SigId
Int -> ATermTable -> (ATermTable, [SigId])
Int -> ATermTable -> (ATermTable, SigId)
ATermTable -> [SigId] -> IO (ATermTable, Int)
ATermTable -> SigId -> IO (ATermTable, Int)
forall t.
Typeable t =>
(ATermTable -> t -> IO (ATermTable, Int))
-> (ATermTable -> [t] -> IO (ATermTable, Int))
-> (Int -> ATermTable -> (ATermTable, t))
-> (Int -> ATermTable -> (ATermTable, [t]))
-> ShATermConvertible t
fromShATermList' :: Int -> ATermTable -> (ATermTable, [SigId])
$cfromShATermList' :: Int -> ATermTable -> (ATermTable, [SigId])
fromShATermAux :: Int -> ATermTable -> (ATermTable, SigId)
$cfromShATermAux :: Int -> ATermTable -> (ATermTable, SigId)
toShATermList' :: ATermTable -> [SigId] -> IO (ATermTable, Int)
$ctoShATermList' :: ATermTable -> [SigId] -> IO (ATermTable, Int)
toShATermAux :: ATermTable -> SigId -> IO (ATermTable, Int)
$ctoShATermAux :: ATermTable -> SigId -> IO (ATermTable, Int)
$cp1ShATermConvertible :: Typeable SigId
ShATermConvertible)

startSigId :: SigId
startSigId :: SigId
startSigId = Int -> SigId
SigId 0

{- | Grothendieck signatures with an lookup index. Zero indices
 indicate unknown ones. It would be nice to have special (may be
 negative) indices for empty signatures (one for every logic). -}
data G_sign = forall lid sublogics
        basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree .
        Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree => G_sign
    { ()
gSignLogic :: lid
    , ()
gSign :: ExtSign sign symbol
    , G_sign -> SigId
gSignSelfIdx :: SigId -- ^ index to lookup this 'G_sign' in sign map
    } deriving Typeable

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

instance Ord G_sign where
  compare :: G_sign -> G_sign -> Ordering
compare (G_sign l1 :: lid
l1 sigma1 :: ExtSign sign symbol
sigma1 s1 :: SigId
s1) (G_sign l2 :: lid
l2 sigma2 :: ExtSign sign symbol
sigma2 s2 :: SigId
s2) =
    if SigId
s1 SigId -> SigId -> Bool
forall a. Ord a => a -> a -> Bool
> SigId
startSigId Bool -> Bool -> Bool
&& SigId
s2 SigId -> SigId -> Bool
forall a. Ord a => a -> a -> Bool
> SigId
startSigId Bool -> Bool -> Bool
&& SigId
s1 SigId -> SigId -> Bool
forall a. Eq a => a -> a -> Bool
== SigId
s2 then Ordering
EQ else
    case AnyLogic -> AnyLogic -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (lid -> AnyLogic
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 -> AnyLogic
Logic lid
l1) (AnyLogic -> Ordering) -> AnyLogic -> Ordering
forall a b. (a -> b) -> a -> b
$ lid -> AnyLogic
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 -> AnyLogic
Logic lid
l2 of
      EQ -> Maybe (ExtSign sign symbol)
-> Maybe (ExtSign sign symbol) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (lid
-> lid
-> String
-> ExtSign sign symbol
-> Maybe (ExtSign sign symbol)
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
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
l1 lid
l2 "Eq G_sign" ExtSign sign symbol
sigma1) (Maybe (ExtSign sign symbol) -> Ordering)
-> Maybe (ExtSign sign symbol) -> Ordering
forall a b. (a -> b) -> a -> b
$ ExtSign sign symbol -> Maybe (ExtSign sign symbol)
forall a. a -> Maybe a
Just ExtSign sign symbol
sigma2
      r :: Ordering
r -> Ordering
r

-- | prefer a faster subsignature test if possible
isHomSubGsign :: G_sign -> G_sign -> Bool
isHomSubGsign :: G_sign -> G_sign -> Bool
isHomSubGsign (G_sign l1 :: lid
l1 sigma1 :: ExtSign sign symbol
sigma1 s1 :: SigId
s1) (G_sign l2 :: lid
l2 sigma2 :: ExtSign sign symbol
sigma2 s2 :: SigId
s2) =
    (SigId
s1 SigId -> SigId -> Bool
forall a. Ord a => a -> a -> Bool
> SigId
startSigId Bool -> Bool -> Bool
&& SigId
s2 SigId -> SigId -> Bool
forall a. Ord a => a -> a -> Bool
> SigId
startSigId Bool -> Bool -> Bool
&& SigId
s1 SigId -> SigId -> Bool
forall a. Eq a => a -> a -> Bool
== SigId
s2) Bool -> Bool -> Bool
||
    Bool
-> (ExtSign sign symbol -> Bool)
-> Maybe (ExtSign sign symbol)
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (lid -> ExtSign sign symbol -> ExtSign sign symbol -> Bool
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 -> ExtSign sign symbol -> ExtSign sign symbol -> Bool
ext_is_subsig lid
l1 ExtSign sign symbol
sigma1)
      (lid
-> lid
-> String
-> ExtSign sign symbol
-> Maybe (ExtSign sign symbol)
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
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
l2 lid
l1 "isHomSubGsign" ExtSign sign symbol
sigma2)

isSubGsign :: LogicGraph -> G_sign -> G_sign -> Bool
isSubGsign :: LogicGraph -> G_sign -> G_sign -> Bool
isSubGsign lg :: LogicGraph
lg (G_sign lid1 :: lid
lid1 (ExtSign sigma1 :: sign
sigma1 _) _)
               (G_sign lid2 :: lid
lid2 (ExtSign sigma2 :: sign
sigma2 _) _) =
  Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
==
  do Comorphism cid :: cid
cid <- Result AnyComorphism -> Maybe AnyComorphism
forall a. Result a -> Maybe a
resultToMaybe (Result AnyComorphism -> Maybe AnyComorphism)
-> Result AnyComorphism -> Maybe AnyComorphism
forall a b. (a -> b) -> a -> b
$
                         LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicInclusion LogicGraph
lg (lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid1) (lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid2)
     sign1
sigma1' <- lid -> lid1 -> String -> sign -> Maybe sign1
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 -> m sign2
coercePlainSign lid
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)
                "Grothendieck.isSubGsign: cannot happen" sign
sigma1
     sign2
sigma2' <- lid -> lid2 -> String -> sign -> Maybe sign2
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 -> m sign2
coercePlainSign lid
lid2 (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)
                "Grothendieck.isSubGsign: cannot happen" sign
sigma2
     (sign2, [Named sentence2])
sigma1t <- Result (sign2, [Named sentence2])
-> Maybe (sign2, [Named sentence2])
forall a. Result a -> Maybe a
resultToMaybe (Result (sign2, [Named sentence2])
 -> Maybe (sign2, [Named sentence2]))
-> Result (sign2, [Named sentence2])
-> Maybe (sign2, [Named sentence2])
forall a b. (a -> b) -> a -> b
$ 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
sigma1'
     Bool -> Maybe Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ lid2 -> sign2 -> sign2 -> Bool
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 -> Bool
is_subsig (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, [Named sentence2]) -> sign2
forall a b. (a, b) -> a
fst (sign2, [Named sentence2])
sigma1t) sign2
sigma2'

instance Show G_sign where
    show :: G_sign -> String
show (G_sign _ s :: ExtSign sign symbol
s _) = ExtSign sign symbol -> String
forall a. Show a => a -> String
show ExtSign sign symbol
s

instance Pretty G_sign where
    pretty :: G_sign -> Doc
pretty (G_sign _ (ExtSign s :: sign
s _) _) = sign -> Doc
forall a. Pretty a => a -> Doc
pretty sign
s

logicOfGsign :: G_sign -> AnyLogic
logicOfGsign :: G_sign -> AnyLogic
logicOfGsign (G_sign lid :: lid
lid _ _) = lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid

symsOfGsign :: G_sign -> Set.Set G_symbol
symsOfGsign :: G_sign -> Set G_symbol
symsOfGsign (G_sign lid :: lid
lid (ExtSign sgn :: sign
sgn _) _) = (symbol -> G_symbol) -> Set symbol -> Set G_symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (lid -> symbol -> G_symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> symbol -> G_symbol
G_symbol lid
lid)
    (Set symbol -> Set G_symbol) -> Set symbol -> Set G_symbol
forall a b. (a -> b) -> a -> b
$ lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
lid sign
sgn

-- | Grothendieck maps with symbol as keys
data G_symbolmap a = forall lid sublogics
        basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree .
        Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree =>
  G_symbolmap lid (Map.Map symbol a)
  deriving Typeable

instance Show a => Show (G_symbolmap a) where
    show :: G_symbolmap a -> String
show (G_symbolmap _ sm :: Map symbol a
sm) = Map symbol a -> String
forall a. Show a => a -> String
show Map symbol a
sm

instance (Typeable a, Ord a) => Eq (G_symbolmap a) where
    a :: G_symbolmap a
a == :: G_symbolmap a -> G_symbolmap a -> Bool
== b :: G_symbolmap a
b = G_symbolmap a -> G_symbolmap a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare G_symbolmap a
a G_symbolmap a
b Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance (Typeable a, Ord a) => Ord (G_symbolmap a) where
  compare :: G_symbolmap a -> G_symbolmap a -> Ordering
compare (G_symbolmap l1 :: lid
l1 sm1 :: Map symbol a
sm1) (G_symbolmap l2 :: lid
l2 sm2 :: Map symbol a
sm2) =
    case AnyLogic -> AnyLogic -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (lid -> AnyLogic
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 -> AnyLogic
Logic lid
l1) (AnyLogic -> Ordering) -> AnyLogic -> Ordering
forall a b. (a -> b) -> a -> b
$ lid -> AnyLogic
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 -> AnyLogic
Logic lid
l2 of
      EQ -> Map symbol a -> Map symbol a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (lid -> lid -> Map symbol a -> Map symbol a
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 a.
(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,
 Typeable a) =>
lid1 -> lid2 -> Map symbol1 a -> Map symbol2 a
coerceSymbolmap lid
l1 lid
l2 Map symbol a
sm1) Map symbol a
sm2
      r :: Ordering
r -> Ordering
r


-- | Grothendieck maps with symbol as values
data G_mapofsymbol a = forall lid sublogics
        basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree .
        Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree =>
  G_mapofsymbol lid (Map.Map a symbol)
  deriving Typeable

instance Show a => Show (G_mapofsymbol a) where
    show :: G_mapofsymbol a -> String
show (G_mapofsymbol _ sm :: Map a symbol
sm) = Map a symbol -> String
forall a. Show a => a -> String
show Map a symbol
sm

instance (Typeable a, Ord a) => Eq (G_mapofsymbol a) where
    a :: G_mapofsymbol a
a == :: G_mapofsymbol a -> G_mapofsymbol a -> Bool
== b :: G_mapofsymbol a
b = G_mapofsymbol a -> G_mapofsymbol a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare G_mapofsymbol a
a G_mapofsymbol a
b Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance (Typeable a, Ord a) => Ord (G_mapofsymbol a) where
  compare :: G_mapofsymbol a -> G_mapofsymbol a -> Ordering
compare (G_mapofsymbol l1 :: lid
l1 sm1 :: Map a symbol
sm1) (G_mapofsymbol l2 :: lid
l2 sm2 :: Map a symbol
sm2) =
    case AnyLogic -> AnyLogic -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (lid -> AnyLogic
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 -> AnyLogic
Logic lid
l1) (AnyLogic -> Ordering) -> AnyLogic -> Ordering
forall a b. (a -> b) -> a -> b
$ lid -> AnyLogic
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 -> AnyLogic
Logic lid
l2 of
      EQ -> Map a symbol -> Map a symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (lid -> lid -> Map a symbol -> Map a symbol
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 a.
(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,
 Typeable a) =>
lid1 -> lid2 -> Map a symbol1 -> Map a symbol2
coerceMapofsymbol lid
l1 lid
l2 Map a symbol
sm1) Map a symbol
sm2
      r :: Ordering
r -> Ordering
r


-- | Grothendieck symbols
data G_symbol = forall lid sublogics
        basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree .
        Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree =>
  G_symbol lid symbol
  deriving Typeable

instance GetRange G_symbol where
  getRange :: G_symbol -> Range
getRange (G_symbol _ s :: symbol
s) = symbol -> Range
forall a. GetRange a => a -> Range
getRange symbol
s
  rangeSpan :: G_symbol -> [Pos]
rangeSpan (G_symbol _ s :: symbol
s) = symbol -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan symbol
s

instance Show G_symbol where
    show :: G_symbol -> String
show (G_symbol _ s :: symbol
s) = symbol -> String
forall a. Show a => a -> String
show symbol
s

instance Pretty G_symbol where
    pretty :: G_symbol -> Doc
pretty (G_symbol _ s :: symbol
s) = symbol -> Doc
forall a. Pretty a => a -> Doc
pretty symbol
s

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

instance Ord G_symbol where
  compare :: G_symbol -> G_symbol -> Ordering
compare (G_symbol l1 :: lid
l1 s1 :: symbol
s1) (G_symbol l2 :: lid
l2 s2 :: symbol
s2) =
    case AnyLogic -> AnyLogic -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (lid -> AnyLogic
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 -> AnyLogic
Logic lid
l1) (AnyLogic -> Ordering) -> AnyLogic -> Ordering
forall a b. (a -> b) -> a -> b
$ lid -> AnyLogic
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 -> AnyLogic
Logic lid
l2 of
      EQ -> symbol -> symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (lid -> lid -> symbol -> symbol
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 lid
l1 lid
l2 symbol
s1) symbol
s2
      r :: Ordering
r -> Ordering
r

-- | Grothendieck symbol lists
data G_symb_items_list = forall lid sublogics
        basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree .
        Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree =>
        G_symb_items_list lid [symb_items]
  deriving Typeable

instance GetRange G_symb_items_list

instance Show G_symb_items_list where
    show :: G_symb_items_list -> String
show (G_symb_items_list _ l :: [symb_items]
l) = [symb_items] -> String
forall a. Show a => a -> String
show [symb_items]
l

instance Pretty G_symb_items_list where
    pretty :: G_symb_items_list -> Doc
pretty (G_symb_items_list _ l :: [symb_items]
l) = [symb_items] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [symb_items]
l

instance Eq G_symb_items_list where
  (G_symb_items_list i1 :: lid
i1 s1 :: [symb_items]
s1) == :: G_symb_items_list -> G_symb_items_list -> Bool
== (G_symb_items_list i2 :: lid
i2 s2 :: [symb_items]
s2) =
     lid -> lid -> String -> [symb_items] -> Maybe [symb_items]
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 -> [symb_items1] -> m [symb_items2]
coerceSymbItemsList lid
i1 lid
i2 "Eq G_symb_items_list" [symb_items]
s1 Maybe [symb_items] -> Maybe [symb_items] -> Bool
forall a. Eq a => a -> a -> Bool
== [symb_items] -> Maybe [symb_items]
forall a. a -> Maybe a
Just [symb_items]
s2

-- | Grothendieck symbol maps
data G_symb_map_items_list = forall lid sublogics
        basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree .
        Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree =>
        G_symb_map_items_list lid [symb_map_items]
  deriving Typeable

instance GetRange G_symb_map_items_list

instance Show G_symb_map_items_list where
    show :: G_symb_map_items_list -> String
show (G_symb_map_items_list _ l :: [symb_map_items]
l) = [symb_map_items] -> String
forall a. Show a => a -> String
show [symb_map_items]
l

instance Pretty G_symb_map_items_list where
    pretty :: G_symb_map_items_list -> Doc
pretty (G_symb_map_items_list _ l :: [symb_map_items]
l) = [symb_map_items] -> Doc
forall a. Pretty a => [a] -> Doc
ppWithCommas [symb_map_items]
l

instance Eq G_symb_map_items_list where
  (G_symb_map_items_list i1 :: lid
i1 s1 :: [symb_map_items]
s1) == :: G_symb_map_items_list -> G_symb_map_items_list -> Bool
== (G_symb_map_items_list i2 :: lid
i2 s2 :: [symb_map_items]
s2) =
     lid -> lid -> String -> [symb_map_items] -> Maybe [symb_map_items]
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 -> [symb_map_items1] -> m [symb_map_items2]
coerceSymbMapItemsList lid
i1 lid
i2 "Eq G_symb_map_items_list" [symb_map_items]
s1 Maybe [symb_map_items] -> Maybe [symb_map_items] -> Bool
forall a. Eq a => a -> a -> Bool
== [symb_map_items] -> Maybe [symb_map_items]
forall a. a -> Maybe a
Just [symb_map_items]
s2

-- | Grothendieck sublogics
data G_sublogics = forall lid sublogics
        basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree .
        Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree =>
        G_sublogics lid sublogics
  deriving Typeable

instance Show G_sublogics where
    show :: G_sublogics -> String
show (G_sublogics lid :: lid
lid sub :: sublogics
sub) = lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid String -> ShowS
forall a. [a] -> [a] -> [a]
++ case sublogics -> String
forall l. SublogicName l => l -> String
sublogicName sublogics
sub of
      [] -> ""
      h :: String
h -> '.' Char -> ShowS
forall a. a -> [a] -> [a]
: String
h

instance Eq G_sublogics where
    g1 :: G_sublogics
g1 == :: G_sublogics -> G_sublogics -> Bool
== g2 :: G_sublogics
g2 = G_sublogics -> G_sublogics -> Ordering
forall a. Ord a => a -> a -> Ordering
compare G_sublogics
g1 G_sublogics
g2 Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord G_sublogics where
    compare :: G_sublogics -> G_sublogics -> Ordering
compare (G_sublogics lid1 :: lid
lid1 l1 :: sublogics
l1) (G_sublogics lid2 :: lid
lid2 l2 :: sublogics
l2) =
      case AnyLogic -> AnyLogic -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid1) (AnyLogic -> Ordering) -> AnyLogic -> Ordering
forall a b. (a -> b) -> a -> b
$ lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid2 of
        EQ -> sublogics -> sublogics -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (lid -> lid -> sublogics -> sublogics
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 lid
lid1 lid
lid2 sublogics
l1) sublogics
l2
        r :: Ordering
r -> Ordering
r

isSublogic :: G_sublogics -> G_sublogics -> Bool
isSublogic :: G_sublogics -> G_sublogics -> Bool
isSublogic (G_sublogics lid1 :: lid
lid1 l1 :: sublogics
l1) (G_sublogics lid2 :: lid
lid2 l2 :: sublogics
l2) =
    sublogics -> sublogics -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem (lid -> lid -> sublogics -> sublogics
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 lid
lid1 lid
lid2 sublogics
l1) sublogics
l2

isProperSublogic :: G_sublogics -> G_sublogics -> Bool
isProperSublogic :: G_sublogics -> G_sublogics -> Bool
isProperSublogic a :: G_sublogics
a b :: G_sublogics
b = G_sublogics -> G_sublogics -> Bool
isSublogic G_sublogics
a G_sublogics
b Bool -> Bool -> Bool
&& G_sublogics
a G_sublogics -> G_sublogics -> Bool
forall a. Eq a => a -> a -> Bool
/= G_sublogics
b

joinSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics
joinSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics
joinSublogics (G_sublogics lid1 :: lid
lid1 l1 :: sublogics
l1) (G_sublogics lid2 :: lid
lid2 l2 :: sublogics
l2) =
    case lid -> lid -> String -> sublogics -> Maybe sublogics
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 -> sublogics1 -> m sublogics2
coerceSublogic lid
lid1 lid
lid2 "coerce Sublogic" sublogics
l1 of
      Just sl :: sublogics
sl -> G_sublogics -> Maybe G_sublogics
forall a. a -> Maybe a
Just (lid -> sublogics -> G_sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> G_sublogics
G_sublogics lid
lid2 (sublogics -> sublogics -> sublogics
forall l. SemiLatticeWithTop l => l -> l -> l
lub sublogics
sl sublogics
l2))
      Nothing -> Maybe G_sublogics
forall a. Maybe a
Nothing

-- | index for morphisms
newtype MorId = MorId Int
  deriving (Typeable, Int -> MorId -> ShowS
[MorId] -> ShowS
MorId -> String
(Int -> MorId -> ShowS)
-> (MorId -> String) -> ([MorId] -> ShowS) -> Show MorId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MorId] -> ShowS
$cshowList :: [MorId] -> ShowS
show :: MorId -> String
$cshow :: MorId -> String
showsPrec :: Int -> MorId -> ShowS
$cshowsPrec :: Int -> MorId -> ShowS
Show, MorId -> MorId -> Bool
(MorId -> MorId -> Bool) -> (MorId -> MorId -> Bool) -> Eq MorId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MorId -> MorId -> Bool
$c/= :: MorId -> MorId -> Bool
== :: MorId -> MorId -> Bool
$c== :: MorId -> MorId -> Bool
Eq, Eq MorId
Eq MorId =>
(MorId -> MorId -> Ordering)
-> (MorId -> MorId -> Bool)
-> (MorId -> MorId -> Bool)
-> (MorId -> MorId -> Bool)
-> (MorId -> MorId -> Bool)
-> (MorId -> MorId -> MorId)
-> (MorId -> MorId -> MorId)
-> Ord MorId
MorId -> MorId -> Bool
MorId -> MorId -> Ordering
MorId -> MorId -> MorId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: MorId -> MorId -> MorId
$cmin :: MorId -> MorId -> MorId
max :: MorId -> MorId -> MorId
$cmax :: MorId -> MorId -> MorId
>= :: MorId -> MorId -> Bool
$c>= :: MorId -> MorId -> Bool
> :: MorId -> MorId -> Bool
$c> :: MorId -> MorId -> Bool
<= :: MorId -> MorId -> Bool
$c<= :: MorId -> MorId -> Bool
< :: MorId -> MorId -> Bool
$c< :: MorId -> MorId -> Bool
compare :: MorId -> MorId -> Ordering
$ccompare :: MorId -> MorId -> Ordering
$cp1Ord :: Eq MorId
Ord, Int -> MorId
MorId -> Int
MorId -> [MorId]
MorId -> MorId
MorId -> MorId -> [MorId]
MorId -> MorId -> MorId -> [MorId]
(MorId -> MorId)
-> (MorId -> MorId)
-> (Int -> MorId)
-> (MorId -> Int)
-> (MorId -> [MorId])
-> (MorId -> MorId -> [MorId])
-> (MorId -> MorId -> [MorId])
-> (MorId -> MorId -> MorId -> [MorId])
-> Enum MorId
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: MorId -> MorId -> MorId -> [MorId]
$cenumFromThenTo :: MorId -> MorId -> MorId -> [MorId]
enumFromTo :: MorId -> MorId -> [MorId]
$cenumFromTo :: MorId -> MorId -> [MorId]
enumFromThen :: MorId -> MorId -> [MorId]
$cenumFromThen :: MorId -> MorId -> [MorId]
enumFrom :: MorId -> [MorId]
$cenumFrom :: MorId -> [MorId]
fromEnum :: MorId -> Int
$cfromEnum :: MorId -> Int
toEnum :: Int -> MorId
$ctoEnum :: Int -> MorId
pred :: MorId -> MorId
$cpred :: MorId -> MorId
succ :: MorId -> MorId
$csucc :: MorId -> MorId
Enum, Typeable MorId
Typeable MorId =>
(ATermTable -> MorId -> IO (ATermTable, Int))
-> (ATermTable -> [MorId] -> IO (ATermTable, Int))
-> (Int -> ATermTable -> (ATermTable, MorId))
-> (Int -> ATermTable -> (ATermTable, [MorId]))
-> ShATermConvertible MorId
Int -> ATermTable -> (ATermTable, [MorId])
Int -> ATermTable -> (ATermTable, MorId)
ATermTable -> [MorId] -> IO (ATermTable, Int)
ATermTable -> MorId -> IO (ATermTable, Int)
forall t.
Typeable t =>
(ATermTable -> t -> IO (ATermTable, Int))
-> (ATermTable -> [t] -> IO (ATermTable, Int))
-> (Int -> ATermTable -> (ATermTable, t))
-> (Int -> ATermTable -> (ATermTable, [t]))
-> ShATermConvertible t
fromShATermList' :: Int -> ATermTable -> (ATermTable, [MorId])
$cfromShATermList' :: Int -> ATermTable -> (ATermTable, [MorId])
fromShATermAux :: Int -> ATermTable -> (ATermTable, MorId)
$cfromShATermAux :: Int -> ATermTable -> (ATermTable, MorId)
toShATermList' :: ATermTable -> [MorId] -> IO (ATermTable, Int)
$ctoShATermList' :: ATermTable -> [MorId] -> IO (ATermTable, Int)
toShATermAux :: ATermTable -> MorId -> IO (ATermTable, Int)
$ctoShATermAux :: ATermTable -> MorId -> IO (ATermTable, Int)
$cp1ShATermConvertible :: Typeable MorId
ShATermConvertible)

startMorId :: MorId
startMorId :: MorId
startMorId = Int -> MorId
MorId 0

{- | Homogeneous Grothendieck signature morphisms with indices. For
the domain index it would be nice it showed also the emptiness. -}
data G_morphism = forall lid sublogics
        basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree .
        Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree => G_morphism
    { ()
gMorphismLogic :: lid
    , ()
gMorphism :: morphism
    , G_morphism -> MorId
gMorphismSelfIdx :: MorId -- ^ lookup index in morphism map
    } deriving Typeable

instance Show G_morphism where
    show :: G_morphism -> String
show (G_morphism _ m :: morphism
m _) = morphism -> String
forall a. Show a => a -> String
show morphism
m

instance Pretty G_morphism where
    pretty :: G_morphism -> Doc
pretty (G_morphism _ m :: morphism
m _) = morphism -> Doc
forall a. Pretty a => a -> Doc
pretty morphism
m

mkG_morphism :: forall lid sublogics
        basic_spec sentence symb_items symb_map_items
         sign morphism symbol raw_symbol proof_tree .
        Logic lid sublogics
         basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree
  => lid -> morphism -> G_morphism
mkG_morphism :: lid -> morphism -> G_morphism
mkG_morphism l :: lid
l m :: morphism
m = lid -> morphism -> MorId -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> MorId -> G_morphism
G_morphism lid
l morphism
m MorId
startMorId

-- | check if sublogic fits for comorphism
lessSublogicComor :: G_sublogics -> AnyComorphism -> Bool
lessSublogicComor :: G_sublogics -> AnyComorphism -> Bool
lessSublogicComor (G_sublogics lid1 :: lid
lid1 sub1 :: sublogics
sub1) (Comorphism cid :: cid
cid) =
    let lid2 :: lid1
lid2 = 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
    in lid1 -> AnyLogic
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 -> AnyLogic
Logic lid1
lid2 AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
== lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid1
        Bool -> Bool -> Bool
&& sublogics1 -> sublogics1 -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem (lid -> lid1 -> sublogics -> 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 lid
lid1 lid1
lid2 sublogics
sub1) (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)

type SublogicBasedTheories = Map.Map IRI (LibName, String)

-- | Logic graph
data LogicGraph = LogicGraph
    { LogicGraph -> Map String AnyLogic
logics :: Map.Map String AnyLogic
    , LogicGraph -> String
currentLogic :: String
    , LogicGraph -> Maybe IRI
currentSyntax :: Maybe IRI
    , LogicGraph -> Maybe G_sublogics
currentSublogic :: Maybe G_sublogics
    , LogicGraph -> Maybe (LibName, String)
currentTargetBase :: Maybe (LibName, String)
    , LogicGraph -> Map AnyLogic SublogicBasedTheories
sublogicBasedTheories :: Map.Map AnyLogic SublogicBasedTheories
    , LogicGraph -> Map String AnyComorphism
comorphisms :: Map.Map String AnyComorphism
    , LogicGraph -> Map (String, String) AnyComorphism
inclusions :: Map.Map (String, String) AnyComorphism
    , LogicGraph -> Map (String, String) (AnyComorphism, AnyComorphism)
unions :: Map.Map (String, String) (AnyComorphism, AnyComorphism)
    , LogicGraph -> Map String AnyMorphism
morphisms :: Map.Map String AnyMorphism
    , LogicGraph -> Map String AnyModification
modifications :: Map.Map String AnyModification
    , LogicGraph -> Map (AnyComorphism, AnyComorphism) [Square]
squares :: Map.Map (AnyComorphism, AnyComorphism) [Square]
    , LogicGraph -> Map String AnyComorphism
qTATranslations :: Map.Map String AnyComorphism
    , LogicGraph -> Map String IRI
prefixes :: Map.Map String IRI
    , LogicGraph -> Bool
dolOnly :: Bool
    } deriving Int -> LogicGraph -> ShowS
[LogicGraph] -> ShowS
LogicGraph -> String
(Int -> LogicGraph -> ShowS)
-> (LogicGraph -> String)
-> ([LogicGraph] -> ShowS)
-> Show LogicGraph
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LogicGraph] -> ShowS
$cshowList :: [LogicGraph] -> ShowS
show :: LogicGraph -> String
$cshow :: LogicGraph -> String
showsPrec :: Int -> LogicGraph -> ShowS
$cshowsPrec :: Int -> LogicGraph -> ShowS
Show

emptyLogicGraph :: LogicGraph
emptyLogicGraph :: LogicGraph
emptyLogicGraph = LogicGraph :: Map String AnyLogic
-> String
-> Maybe IRI
-> Maybe G_sublogics
-> Maybe (LibName, String)
-> Map AnyLogic SublogicBasedTheories
-> Map String AnyComorphism
-> Map (String, String) AnyComorphism
-> Map (String, String) (AnyComorphism, AnyComorphism)
-> Map String AnyMorphism
-> Map String AnyModification
-> Map (AnyComorphism, AnyComorphism) [Square]
-> Map String AnyComorphism
-> Map String IRI
-> Bool
-> LogicGraph
LogicGraph
    { logics :: Map String AnyLogic
logics = Map String AnyLogic
forall k a. Map k a
Map.empty
    , currentLogic :: String
currentLogic = "CASL"
    , currentSyntax :: Maybe IRI
currentSyntax = Maybe IRI
forall a. Maybe a
Nothing
    , currentSublogic :: Maybe G_sublogics
currentSublogic = Maybe G_sublogics
forall a. Maybe a
Nothing
    , currentTargetBase :: Maybe (LibName, String)
currentTargetBase = Maybe (LibName, String)
forall a. Maybe a
Nothing
    , sublogicBasedTheories :: Map AnyLogic SublogicBasedTheories
sublogicBasedTheories = Map AnyLogic SublogicBasedTheories
forall k a. Map k a
Map.empty
    , comorphisms :: Map String AnyComorphism
comorphisms = Map String AnyComorphism
forall k a. Map k a
Map.empty
    , inclusions :: Map (String, String) AnyComorphism
inclusions = Map (String, String) AnyComorphism
forall k a. Map k a
Map.empty
    , unions :: Map (String, String) (AnyComorphism, AnyComorphism)
unions = Map (String, String) (AnyComorphism, AnyComorphism)
forall k a. Map k a
Map.empty
    , morphisms :: Map String AnyMorphism
morphisms = Map String AnyMorphism
forall k a. Map k a
Map.empty
    , modifications :: Map String AnyModification
modifications = Map String AnyModification
forall k a. Map k a
Map.empty
    , squares :: Map (AnyComorphism, AnyComorphism) [Square]
squares = Map (AnyComorphism, AnyComorphism) [Square]
forall k a. Map k a
Map.empty
    , qTATranslations :: Map String AnyComorphism
qTATranslations = Map String AnyComorphism
forall k a. Map k a
Map.empty
    , prefixes :: Map String IRI
prefixes = Map String IRI
forall k a. Map k a
Map.empty
    , dolOnly :: Bool
dolOnly = Bool
False
    }

setCurLogicAux :: String -> LogicGraph -> LogicGraph
setCurLogicAux :: String -> LogicGraph -> LogicGraph
setCurLogicAux s :: String
s lg :: LogicGraph
lg = LogicGraph
lg { currentLogic :: String
currentLogic = String
s }

setCurLogic :: String -> LogicGraph -> LogicGraph
setCurLogic :: String -> LogicGraph -> LogicGraph
setCurLogic s :: String
s lg :: LogicGraph
lg = if String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== LogicGraph -> String
currentLogic LogicGraph
lg then
       LogicGraph
lg else Maybe IRI -> LogicGraph -> LogicGraph
setSyntaxAux Maybe IRI
forall a. Maybe a
Nothing (LogicGraph -> LogicGraph) -> LogicGraph -> LogicGraph
forall a b. (a -> b) -> a -> b
$ String -> LogicGraph -> LogicGraph
setCurLogicAux String
s LogicGraph
lg

setSyntaxAux :: Maybe IRI -> LogicGraph -> LogicGraph
setSyntaxAux :: Maybe IRI -> LogicGraph -> LogicGraph
setSyntaxAux s :: Maybe IRI
s lg :: LogicGraph
lg = LogicGraph
lg { currentSyntax :: Maybe IRI
currentSyntax = Maybe IRI
s }

setSyntax :: Maybe IRI -> LogicGraph -> LogicGraph
setSyntax :: Maybe IRI -> LogicGraph -> LogicGraph
setSyntax s :: Maybe IRI
s lg :: LogicGraph
lg = if Maybe IRI -> Bool
forall a. Maybe a -> Bool
isNothing Maybe IRI
s then LogicGraph
lg else Maybe IRI -> LogicGraph -> LogicGraph
setSyntaxAux Maybe IRI
s LogicGraph
lg

setCurSublogic :: Maybe G_sublogics -> LogicGraph -> LogicGraph
setCurSublogic :: Maybe G_sublogics -> LogicGraph -> LogicGraph
setCurSublogic s :: Maybe G_sublogics
s lg :: LogicGraph
lg = LogicGraph
lg { currentSublogic :: Maybe G_sublogics
currentSublogic = Maybe G_sublogics
s }

instance Pretty LogicGraph where
    pretty :: LogicGraph -> Doc
pretty lg :: LogicGraph
lg = String -> Doc
text ("current logic is: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ LogicGraph -> String
currentLogic LogicGraph
lg)
       Doc -> Doc -> Doc
$+$ String -> Doc
text "all logics:"
       Doc -> Doc -> Doc
$+$ [Doc] -> Doc
sepByCommas ((String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text ([String] -> [Doc]) -> [String] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Map String AnyLogic -> [String]
forall k a. Map k a -> [k]
Map.keys (Map String AnyLogic -> [String])
-> Map String AnyLogic -> [String]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
lg)
       Doc -> Doc -> Doc
$+$ String -> Doc
text "comorphism inclusions:"
       Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((AnyComorphism -> Doc) -> [AnyComorphism] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map AnyComorphism -> Doc
forall a. Pretty a => a -> Doc
pretty ([AnyComorphism] -> [Doc]) -> [AnyComorphism] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Map (String, String) AnyComorphism -> [AnyComorphism]
forall k a. Map k a -> [a]
Map.elems (Map (String, String) AnyComorphism -> [AnyComorphism])
-> Map (String, String) AnyComorphism -> [AnyComorphism]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map (String, String) AnyComorphism
inclusions LogicGraph
lg)
       Doc -> Doc -> Doc
$+$ String -> Doc
text "all comorphisms:"
       Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat ((AnyComorphism -> Doc) -> [AnyComorphism] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map AnyComorphism -> Doc
forall a. Pretty a => a -> Doc
pretty ([AnyComorphism] -> [Doc]) -> [AnyComorphism] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Map String AnyComorphism -> [AnyComorphism]
forall k a. Map k a -> [a]
Map.elems (Map String AnyComorphism -> [AnyComorphism])
-> Map String AnyComorphism -> [AnyComorphism]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyComorphism
comorphisms LogicGraph
lg)

-- | find a logic in a logic graph
lookupLogic :: Fail.MonadFail m => String -> String -> LogicGraph -> m AnyLogic
lookupLogic :: String -> String -> LogicGraph -> m AnyLogic
lookupLogic error_prefix :: String
error_prefix logname :: String
logname logicGraph :: LogicGraph
logicGraph =
    case String -> Map String AnyLogic -> Maybe AnyLogic
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
logname (Map String AnyLogic -> Maybe AnyLogic)
-> Map String AnyLogic -> Maybe AnyLogic
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
logicGraph of
    Nothing -> String -> m AnyLogic
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m AnyLogic) -> String -> m AnyLogic
forall a b. (a -> b) -> a -> b
$ String
error_prefix String -> ShowS
forall a. [a] -> [a] -> [a]
++ "unknown logic: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
logname
    Just lid :: AnyLogic
lid -> AnyLogic -> m AnyLogic
forall (m :: * -> *) a. Monad m => a -> m a
return AnyLogic
lid

lookupCurrentLogic :: Fail.MonadFail m => String -> LogicGraph -> m AnyLogic
lookupCurrentLogic :: String -> LogicGraph -> m AnyLogic
lookupCurrentLogic msg :: String
msg lg :: LogicGraph
lg = String -> String -> LogicGraph -> m AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> String -> LogicGraph -> m AnyLogic
lookupLogic (String
msg String -> ShowS
forall a. [a] -> [a] -> [a]
++ " ") (LogicGraph -> String
currentLogic LogicGraph
lg) LogicGraph
lg

lookupCurrentSyntax :: Fail.MonadFail m => String -> LogicGraph
  -> m (AnyLogic, Maybe IRI)
lookupCurrentSyntax :: String -> LogicGraph -> m (AnyLogic, Maybe IRI)
lookupCurrentSyntax msg :: String
msg lg :: LogicGraph
lg = do
  AnyLogic
l <- String -> String -> LogicGraph -> m AnyLogic
forall (m :: * -> *).
MonadFail m =>
String -> String -> LogicGraph -> m AnyLogic
lookupLogic (String
msg String -> ShowS
forall a. [a] -> [a] -> [a]
++ " ") (LogicGraph -> String
currentLogic LogicGraph
lg) LogicGraph
lg
  (AnyLogic, Maybe IRI) -> m (AnyLogic, Maybe IRI)
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyLogic
l, LogicGraph -> Maybe IRI
currentSyntax LogicGraph
lg)

-- | union to two logics
logicUnion :: LogicGraph -> AnyLogic -> AnyLogic
           -> Result (AnyComorphism, AnyComorphism)
logicUnion :: LogicGraph
-> AnyLogic -> AnyLogic -> Result (AnyComorphism, AnyComorphism)
logicUnion lg :: LogicGraph
lg l1 :: AnyLogic
l1@(Logic lid1 :: lid
lid1) l2 :: AnyLogic
l2@(Logic lid2 :: lid
lid2) =
  case LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicInclusion LogicGraph
lg AnyLogic
l1 AnyLogic
l2 of
    Result _ (Just c :: AnyComorphism
c) -> (AnyComorphism, AnyComorphism)
-> Result (AnyComorphism, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyComorphism
c, AnyLogic -> AnyComorphism
idComorphism AnyLogic
l2)
    _ -> case LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicInclusion LogicGraph
lg AnyLogic
l2 AnyLogic
l1 of
      Result _ (Just c :: AnyComorphism
c) -> (AnyComorphism, AnyComorphism)
-> Result (AnyComorphism, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyLogic -> AnyComorphism
idComorphism AnyLogic
l1, AnyComorphism
c)
      _ -> case (String, String)
-> Map (String, String) (AnyComorphism, AnyComorphism)
-> Maybe (AnyComorphism, AnyComorphism)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (String
ln1, String
ln2) (LogicGraph -> Map (String, String) (AnyComorphism, AnyComorphism)
unions LogicGraph
lg) of
        Just u :: (AnyComorphism, AnyComorphism)
u -> (AnyComorphism, AnyComorphism)
-> Result (AnyComorphism, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyComorphism, AnyComorphism)
u
        Nothing -> case (String, String)
-> Map (String, String) (AnyComorphism, AnyComorphism)
-> Maybe (AnyComorphism, AnyComorphism)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (String
ln2, String
ln1) (LogicGraph -> Map (String, String) (AnyComorphism, AnyComorphism)
unions LogicGraph
lg) of
          Just (c2 :: AnyComorphism
c2, c1 :: AnyComorphism
c1) -> (AnyComorphism, AnyComorphism)
-> Result (AnyComorphism, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyComorphism
c1, AnyComorphism
c2)
          Nothing -> String -> Result (AnyComorphism, AnyComorphism)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (AnyComorphism, AnyComorphism))
-> String -> Result (AnyComorphism, AnyComorphism)
forall a b. (a -> b) -> a -> b
$ "Union of logics " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ln1 String -> ShowS
forall a. [a] -> [a] -> [a]
++
                     " and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ln2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " does not exist"
   where ln1 :: String
ln1 = lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid1
         ln2 :: String
ln2 = lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid2

-- | find a comorphism composition in a logic graph
lookupCompComorphism :: Fail.MonadFail m => [String] -> LogicGraph -> m AnyComorphism
lookupCompComorphism :: [String] -> LogicGraph -> m AnyComorphism
lookupCompComorphism nameList :: [String]
nameList logicGraph :: LogicGraph
logicGraph = do
  [AnyComorphism]
cs <- (String -> m AnyComorphism) -> [String] -> m [AnyComorphism]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> m AnyComorphism
forall (m :: * -> *). MonadFail m => String -> m AnyComorphism
lookupN [String]
nameList
  case [AnyComorphism]
cs of
    c :: AnyComorphism
c : cs1 :: [AnyComorphism]
cs1 -> (AnyComorphism -> AnyComorphism -> m AnyComorphism)
-> AnyComorphism -> [AnyComorphism] -> m AnyComorphism
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM AnyComorphism -> AnyComorphism -> m AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism AnyComorphism
c [AnyComorphism]
cs1
    _ -> String -> m AnyComorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Illegal empty comorphism composition"
  where
  lookupN :: String -> m AnyComorphism
lookupN name :: String
name =
    case String
name of
      'i' : 'd' : '_' : logic :: String
logic -> do
         let (mainLogic :: String
mainLogic, subLogicD :: String
subLogicD) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '.') String
logic
          -- subLogicD will begin with a . which has to be removed
             msublogic :: Maybe String
msublogic = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
subLogicD
                     then Maybe String
forall a. Maybe a
Nothing
                     else String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. [a] -> [a]
tail String
subLogicD
         Logic lid :: lid
lid <- m AnyLogic
-> (AnyLogic -> m AnyLogic) -> Maybe AnyLogic -> m AnyLogic
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> m AnyLogic
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Cannot find Logic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
mainLogic)) AnyLogic -> m AnyLogic
forall (m :: * -> *) a. Monad m => a -> m a
return
                 (Maybe AnyLogic -> m AnyLogic) -> Maybe AnyLogic -> m AnyLogic
forall a b. (a -> b) -> a -> b
$ String -> Map String AnyLogic -> Maybe AnyLogic
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
mainLogic (LogicGraph -> Map String AnyLogic
logics LogicGraph
logicGraph)
         case Maybe sublogics
-> (String -> Maybe sublogics) -> Maybe String -> Maybe sublogics
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (sublogics -> Maybe sublogics
forall a. a -> Maybe a
Just (sublogics -> Maybe sublogics) -> sublogics -> Maybe sublogics
forall a b. (a -> b) -> a -> b
$ 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) (lid -> String -> Maybe 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 -> String -> Maybe sublogics
parseSublogic lid
lid) Maybe String
msublogic of
           Nothing -> 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
$ String -> ShowS -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "missing sublogic"
                    ("unknown sublogic name " String -> ShowS
forall a. [a] -> [a] -> [a]
++) Maybe String
msublogic
           Just s :: sublogics
s -> 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
$ 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 (InclComorphism lid sublogics -> AnyComorphism)
-> InclComorphism lid sublogics -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ 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 sublogics
s
      _ -> m AnyComorphism
-> (AnyComorphism -> m AnyComorphism)
-> Maybe AnyComorphism
-> m AnyComorphism
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> m AnyComorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Cannot find logic comorphism " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name)) AnyComorphism -> m AnyComorphism
forall (m :: * -> *) a. Monad m => a -> m a
return
             (Maybe AnyComorphism -> m AnyComorphism)
-> Maybe AnyComorphism -> m AnyComorphism
forall a b. (a -> b) -> a -> b
$ String -> Map String AnyComorphism -> Maybe AnyComorphism
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
name (LogicGraph -> Map String AnyComorphism
comorphisms LogicGraph
logicGraph)

-- | find a comorphism in a logic graph
lookupComorphism :: Fail.MonadFail m => String -> LogicGraph -> m AnyComorphism
lookupComorphism :: String -> LogicGraph -> m AnyComorphism
lookupComorphism = [String] -> LogicGraph -> m AnyComorphism
forall (m :: * -> *).
MonadFail m =>
[String] -> LogicGraph -> m AnyComorphism
lookupCompComorphism ([String] -> LogicGraph -> m AnyComorphism)
-> (String -> [String]) -> String -> LogicGraph -> m AnyComorphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> [String]
forall a. Eq a => a -> [a] -> [[a]]
splitOn ';'

-- | find a modification in a logic graph
lookupModification :: (Fail.MonadFail m) => String -> LogicGraph -> m AnyModification
lookupModification :: String -> LogicGraph -> m AnyModification
lookupModification input :: String
input lG :: LogicGraph
lG
        = case Parsec String () (m AnyModification)
-> String -> String -> Either ParseError (m AnyModification)
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse (LogicGraph -> Parsec String () (m AnyModification)
forall (m :: * -> *).
MonadFail m =>
LogicGraph -> Parser (m AnyModification)
parseModif LogicGraph
lG Parsec String () (m AnyModification)
-> ParsecT String () Identity ()
-> Parsec String () (m AnyModification)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof) "" String
input of
            Left err :: ParseError
err -> String -> m AnyModification
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m AnyModification) -> String -> m AnyModification
forall a b. (a -> b) -> a -> b
$ ParseError -> String
forall a. Show a => a -> String
show ParseError
err
            Right x :: m AnyModification
x -> m AnyModification
x

parseModif :: (Fail.MonadFail m) => LogicGraph -> Parser (m AnyModification)
parseModif :: LogicGraph -> Parser (m AnyModification)
parseModif lG :: LogicGraph
lG = do
  (xs :: [Maybe AnyModification]
xs, _) <- GenParser Char () (Maybe AnyModification)
-> GenParser Char () Token
-> GenParser Char () ([Maybe AnyModification], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy (LogicGraph -> GenParser Char () (Maybe AnyModification)
forall (m :: * -> *).
MonadFail m =>
LogicGraph -> Parser (m AnyModification)
vertcomp LogicGraph
lG) GenParser Char () Token
forall st. GenParser Char st Token
crossT
  let r :: Maybe (m AnyModification)
r = do
        [AnyModification]
y <- [Maybe AnyModification] -> Maybe [AnyModification]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Maybe AnyModification]
xs
        case [AnyModification]
y of
          m :: AnyModification
m : ms :: [AnyModification]
ms -> m AnyModification -> Maybe (m AnyModification)
forall (m :: * -> *) a. Monad m => a -> m a
return (m AnyModification -> Maybe (m AnyModification))
-> m AnyModification -> Maybe (m AnyModification)
forall a b. (a -> b) -> a -> b
$ (AnyModification -> AnyModification -> m AnyModification)
-> AnyModification -> [AnyModification] -> m AnyModification
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM AnyModification -> AnyModification -> m AnyModification
forall (m :: * -> *).
MonadFail m =>
AnyModification -> AnyModification -> m AnyModification
horCompModification AnyModification
m [AnyModification]
ms
          _ -> Maybe (m AnyModification)
forall a. Maybe a
Nothing
  case Maybe (m AnyModification)
r of
    Nothing -> String -> Parser (m AnyModification)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Illegal empty horizontal composition"
    Just m :: m AnyModification
m -> m AnyModification -> Parser (m AnyModification)
forall (m :: * -> *) a. Monad m => a -> m a
return m AnyModification
m

vertcomp :: (Fail.MonadFail m) => LogicGraph -> Parser (m AnyModification)
vertcomp :: LogicGraph -> Parser (m AnyModification)
vertcomp lG :: LogicGraph
lG = do
  (xs :: [Maybe AnyModification]
xs, _) <- GenParser Char () (Maybe AnyModification)
-> GenParser Char () Token
-> GenParser Char () ([Maybe AnyModification], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy (LogicGraph -> GenParser Char () (Maybe AnyModification)
forall (m :: * -> *).
MonadFail m =>
LogicGraph -> Parser (m AnyModification)
pm LogicGraph
lG) GenParser Char () Token
forall st. GenParser Char st Token
semiT
  let r :: Maybe (m AnyModification)
r = do
        [AnyModification]
y <- [Maybe AnyModification] -> Maybe [AnyModification]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Maybe AnyModification]
xs
        case [AnyModification]
y of
          m :: AnyModification
m : ms :: [AnyModification]
ms -> m AnyModification -> Maybe (m AnyModification)
forall (m :: * -> *) a. Monad m => a -> m a
return (m AnyModification -> Maybe (m AnyModification))
-> m AnyModification -> Maybe (m AnyModification)
forall a b. (a -> b) -> a -> b
$ (AnyModification -> AnyModification -> m AnyModification)
-> AnyModification -> [AnyModification] -> m AnyModification
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM AnyModification -> AnyModification -> m AnyModification
forall (m :: * -> *).
MonadFail m =>
AnyModification -> AnyModification -> m AnyModification
vertCompModification AnyModification
m [AnyModification]
ms
          _ -> Maybe (m AnyModification)
forall a. Maybe a
Nothing
             -- r has type Maybe (m AnyModification)
  case Maybe (m AnyModification)
r of
    Nothing -> String -> Parser (m AnyModification)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Illegal empty vertical composition"
    Just m :: m AnyModification
m -> m AnyModification -> Parser (m AnyModification)
forall (m :: * -> *) a. Monad m => a -> m a
return m AnyModification
m

pm :: (Fail.MonadFail m) => LogicGraph -> Parser (m AnyModification)
pm :: LogicGraph -> Parser (m AnyModification)
pm lG :: LogicGraph
lG = LogicGraph -> Parser (m AnyModification)
forall (m :: * -> *).
MonadFail m =>
LogicGraph -> Parser (m AnyModification)
parseName LogicGraph
lG Parser (m AnyModification)
-> Parser (m AnyModification) -> Parser (m AnyModification)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> LogicGraph -> Parser (m AnyModification)
forall (m :: * -> *).
MonadFail m =>
LogicGraph -> Parser (m AnyModification)
bracks LogicGraph
lG

bracks :: (Fail.MonadFail m) => LogicGraph -> Parser (m AnyModification)
bracks :: LogicGraph -> Parser (m AnyModification)
bracks lG :: LogicGraph
lG = do
  GenParser Char () Token
forall st. GenParser Char st Token
oParenT
  m AnyModification
modif <- LogicGraph -> Parser (m AnyModification)
forall (m :: * -> *).
MonadFail m =>
LogicGraph -> Parser (m AnyModification)
parseModif LogicGraph
lG
  GenParser Char () Token
forall st. GenParser Char st Token
cParenT
  m AnyModification -> Parser (m AnyModification)
forall (m :: * -> *) a. Monad m => a -> m a
return m AnyModification
modif

parseIdentity :: (Fail.MonadFail m) => LogicGraph -> Parser (m AnyModification)
parseIdentity :: LogicGraph -> Parser (m AnyModification)
parseIdentity lG :: LogicGraph
lG = do
  String -> CharParser () String
forall st. String -> CharParser st String
tryString "id_"
  Token
tok <- GenParser Char () Token
forall st. GenParser Char st Token
simpleId
  let name :: String
name = Token -> String
tokStr Token
tok
  case String -> Map String AnyComorphism -> Maybe AnyComorphism
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
name (LogicGraph -> Map String AnyComorphism
comorphisms LogicGraph
lG) of
    Nothing -> String -> Parser (m AnyModification)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Parser (m AnyModification))
-> String -> Parser (m AnyModification)
forall a b. (a -> b) -> a -> b
$ "Cannot find comorphism" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name
    Just x :: AnyComorphism
x -> m AnyModification -> Parser (m AnyModification)
forall (m :: * -> *) a. Monad m => a -> m a
return (m AnyModification -> Parser (m AnyModification))
-> m AnyModification -> Parser (m AnyModification)
forall a b. (a -> b) -> a -> b
$ AnyModification -> m AnyModification
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyModification -> m AnyModification)
-> AnyModification -> m AnyModification
forall a b. (a -> b) -> a -> b
$ AnyComorphism -> AnyModification
idModification AnyComorphism
x

parseName :: (Fail.MonadFail m) => LogicGraph -> Parser (m AnyModification)
parseName :: LogicGraph -> Parser (m AnyModification)
parseName lG :: LogicGraph
lG = LogicGraph -> Parser (m AnyModification)
forall (m :: * -> *).
MonadFail m =>
LogicGraph -> Parser (m AnyModification)
parseIdentity LogicGraph
lG Parser (m AnyModification)
-> Parser (m AnyModification) -> Parser (m AnyModification)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
  Token
tok <- GenParser Char () Token
forall st. GenParser Char st Token
simpleId
  let name :: String
name = Token -> String
tokStr Token
tok
  case String -> Map String AnyModification -> Maybe AnyModification
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
name (LogicGraph -> Map String AnyModification
modifications LogicGraph
lG) of
    Nothing -> String -> Parser (m AnyModification)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Parser (m AnyModification))
-> String -> Parser (m AnyModification)
forall a b. (a -> b) -> a -> b
$ "Cannot find modification" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name
    Just x :: AnyModification
x -> m AnyModification -> Parser (m AnyModification)
forall (m :: * -> *) a. Monad m => a -> m a
return (m AnyModification -> Parser (m AnyModification))
-> m AnyModification -> Parser (m AnyModification)
forall a b. (a -> b) -> a -> b
$ AnyModification -> m AnyModification
forall (m :: * -> *) a. Monad m => a -> m a
return AnyModification
x

-- * The Grothendieck signature category

-- | Grothendieck signature morphisms with indices
data GMorphism = forall cid lid1 sublogics1
        basic_spec1 sentence1 symb_items1 symb_map_items1
        sign1 morphism1 symbol1 raw_symbol1 proof_tree1
        lid2 sublogics2
        basic_spec2 sentence2 symb_items2 symb_map_items2
        sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
      Comorphism cid
        lid1 sublogics1 basic_spec1 sentence1
        symb_items1 symb_map_items1
        sign1 morphism1 symbol1 raw_symbol1 proof_tree1
        lid2 sublogics2 basic_spec2 sentence2
        symb_items2 symb_map_items2
        sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => GMorphism
    { ()
gMorphismComor :: cid
    , ()
gMorphismSign :: ExtSign sign1 symbol1
    , GMorphism -> SigId
gMorphismSignIdx :: SigId -- ^ 'G_sign' index of source signature
    , ()
gMorphismMor :: morphism2
    , GMorphism -> MorId
gMorphismMorIdx :: MorId  -- ^ `G_morphism index of target morphism
    } deriving Typeable

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

instance Ord GMorphism where
  compare :: GMorphism -> GMorphism -> Ordering
compare (GMorphism cid1 :: cid
cid1 sigma1 :: ExtSign sign1 symbol1
sigma1 in1 :: SigId
in1 mor1 :: morphism2
mor1 in1' :: MorId
in1')
    (GMorphism cid2 :: cid
cid2 sigma2 :: ExtSign sign1 symbol1
sigma2 in2 :: SigId
in2 mor2 :: morphism2
mor2 in2' :: MorId
in2') =
      case (AnyComorphism, G_sign) -> (AnyComorphism, G_sign) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (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
cid1, lid1 -> ExtSign sign1 symbol1 -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign (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
cid1) ExtSign sign1 symbol1
sigma1 SigId
in1)
            (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
cid2, lid1 -> ExtSign sign1 symbol1 -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign (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) ExtSign sign1 symbol1
sigma2 SigId
in2) of
        EQ -> if MorId
in1' MorId -> MorId -> Bool
forall a. Ord a => a -> a -> Bool
> MorId
startMorId Bool -> Bool -> Bool
&& MorId
in2' MorId -> MorId -> Bool
forall a. Ord a => a -> a -> Bool
> MorId
startMorId Bool -> Bool -> Bool
&& MorId
in1' MorId -> MorId -> Bool
forall a. Eq a => a -> a -> Bool
== MorId
in2'
          then Ordering
EQ else
          Maybe morphism2 -> Maybe morphism2 -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (lid2 -> lid2 -> String -> morphism2 -> Maybe morphism2
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 (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) (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
cid2)
                   "Ord GMorphism.coerceMorphism" morphism2
mor1) (morphism2 -> Maybe morphism2
forall a. a -> Maybe a
Just morphism2
mor2)
          -- this coersion will succeed, because cid1 and cid2 are equal
        r :: Ordering
r -> Ordering
r

isHomogeneous :: GMorphism -> Bool
isHomogeneous :: GMorphism -> Bool
isHomogeneous (GMorphism cid :: cid
cid _ _ _ _) =
  AnyComorphism -> Bool
isIdComorphism (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)

data Grothendieck = Grothendieck deriving (Typeable, Int -> Grothendieck -> ShowS
[Grothendieck] -> ShowS
Grothendieck -> String
(Int -> Grothendieck -> ShowS)
-> (Grothendieck -> String)
-> ([Grothendieck] -> ShowS)
-> Show Grothendieck
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Grothendieck] -> ShowS
$cshowList :: [Grothendieck] -> ShowS
show :: Grothendieck -> String
$cshow :: Grothendieck -> String
showsPrec :: Int -> Grothendieck -> ShowS
$cshowsPrec :: Int -> Grothendieck -> ShowS
Show)

instance Language Grothendieck

instance Show GMorphism where
    show :: GMorphism -> String
show (GMorphism cid :: cid
cid s :: ExtSign sign1 symbol1
s _ m :: morphism2
m _) =
      AnyComorphism -> String
forall a. Show a => a -> String
show (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) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ExtSign sign1 symbol1 -> String
forall a. Show a => a -> String
show ExtSign sign1 symbol1
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")" String -> ShowS
forall a. [a] -> [a] -> [a]
++ morphism2 -> String
forall a. Show a => a -> String
show morphism2
m

instance Pretty GMorphism where
    pretty :: GMorphism -> Doc
pretty (GMorphism cid :: cid
cid (ExtSign s :: sign1
s _) _ m :: morphism2
m _) = let c :: AnyComorphism
c = 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 in [Doc] -> Doc
fsep
      [ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ AnyComorphism -> String
forall a. Show a => a -> String
show AnyComorphism
c
      , if AnyComorphism -> Bool
isIdComorphism AnyComorphism
c then Doc
empty else Doc -> Doc
specBraces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> sign1 -> Doc
forall a. Pretty a => a -> Doc
pretty sign1
s
      , morphism2 -> Doc
forall a. Pretty a => a -> Doc
pretty morphism2
m ]

-- signature category of the Grothendieck institution
instance Category G_sign GMorphism where
  ide :: G_sign -> GMorphism
ide (G_sign lid :: lid
lid sigma :: ExtSign sign symbol
sigma@(ExtSign s :: sign
s _) ind :: SigId
ind) =
    InclComorphism lid sublogics
-> ExtSign sign symbol -> SigId -> morphism -> MorId -> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism (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))
              ExtSign sign symbol
sigma SigId
ind (sign -> morphism
forall object morphism.
Category object morphism =>
object -> morphism
ide sign
s) MorId
startMorId
  -- composition of Grothendieck signature morphisms
  composeMorphisms :: GMorphism -> GMorphism -> Result GMorphism
composeMorphisms (GMorphism r1 :: cid
r1 sigma1 :: ExtSign sign1 symbol1
sigma1 ind1 :: SigId
ind1 mor1 :: morphism2
mor1 _)
       (GMorphism r2 :: cid
r2 _sigma2 :: ExtSign sign1 symbol1
_sigma2 _ mor2 :: morphism2
mor2 _) =
    do let 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
r1
           lid2 :: lid2
lid2 = 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
r1
           lid3 :: lid1
lid3 = 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
r2
           lid4 :: lid2
lid4 = 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
r2
       -- if the second comorphism is the identity then simplify immediately
       if AnyComorphism -> Bool
isIdComorphism (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
r2) then do
           morphism2
mor2' <- lid2 -> lid2 -> String -> morphism2 -> Result morphism2
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 lid2
lid4 lid2
lid2 "Grothendieck.comp" morphism2
mor2
           morphism2
mor' <- morphism2 -> morphism2 -> Result morphism2
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms morphism2
mor1 morphism2
mor2'
           GMorphism -> Result GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
r1 ExtSign sign1 symbol1
sigma1 SigId
ind1 morphism2
mor' MorId
startMorId)
         else do
         {- coercion between target of first and
         source of second Grothendieck morphism -}
         morphism1
mor1' <- lid2 -> lid1 -> String -> morphism2 -> Result morphism1
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 lid2
lid2 lid1
lid3 "Grothendieck.comp" morphism2
mor1
         {- map signature morphism component of first Grothendieck morphism
         along the comorphism component of the second one ... -}
         morphism2
mor1'' <- 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
map_morphism cid
r2 morphism1
mor1'
         {- and then compose the result with the signature morphism component
         of first one -}
         morphism2
mor <- morphism2 -> morphism2 -> Result morphism2
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms morphism2
mor1'' morphism2
mor2
         -- also if the first comorphism is the identity...
         if AnyComorphism -> Bool
isIdComorphism (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
r1) Bool -> Bool -> Bool
&&
           case lid2 -> lid1 -> String -> sublogics2 -> Maybe 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 (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 -> sublogics1 -> m sublogics2
coerceSublogic lid2
lid2 lid1
lid3 "Grothendieck.comp"
                              (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
r1) of
             Just sl1 :: sublogics1
sl1 -> Bool -> (sublogics2 -> Bool) -> Maybe sublogics2 -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False
                              (sublogics2 -> sublogics2 -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem (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
r2))
                              (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
r2 sublogics1
sl1)
             _ -> Bool
False
               -- ... then things simplify ...
           then do
             ExtSign sign1 symbol1
sigma1' <- lid1
-> lid1
-> String
-> ExtSign sign1 symbol1
-> Result (ExtSign sign1 symbol1)
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
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid1
lid1 lid1
lid3 "Grothendieck.comp" ExtSign sign1 symbol1
sigma1
             GMorphism -> Result GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
r2 ExtSign sign1 symbol1
sigma1' SigId
ind1 morphism2
mor MorId
startMorId)
           else GMorphism -> Result GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism -> Result GMorphism) -> GMorphism -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ CompComorphism cid cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism (cid -> cid -> CompComorphism cid cid
forall cid1 cid2. cid1 -> cid2 -> CompComorphism cid1 cid2
CompComorphism cid
r1 cid
r2)
                ExtSign sign1 symbol1
sigma1 SigId
ind1 morphism2
mor MorId
startMorId
  dom :: GMorphism -> G_sign
dom (GMorphism r :: cid
r sigma :: ExtSign sign1 symbol1
sigma ind :: SigId
ind _mor :: morphism2
_mor _) =
    lid1 -> ExtSign sign1 symbol1 -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign (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
r) ExtSign sign1 symbol1
sigma SigId
ind
  cod :: GMorphism -> G_sign
cod (GMorphism r :: cid
r (ExtSign _ _) _ mor :: morphism2
mor _) =
    let lid2 :: lid2
lid2 = 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
r
        sig2 :: sign2
sig2 = morphism2 -> sign2
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism2
mor
    in lid2 -> ExtSign sign2 symbol2 -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign lid2
lid2 (lid2 -> sign2 -> ExtSign sign2 symbol2
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 -> sign -> ExtSign sign symbol
makeExtSign lid2
lid2 sign2
sig2) SigId
startSigId
  isInclusion :: GMorphism -> Bool
isInclusion (GMorphism cid :: cid
cid _ _ mor :: morphism2
mor _) =
    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
isInclusionComorphism cid
cid Bool -> Bool -> Bool
&& morphism2 -> Bool
forall object morphism.
Category object morphism =>
morphism -> Bool
isInclusion morphism2
mor
  legal_mor :: GMorphism -> Result ()
legal_mor (GMorphism r :: cid
r (ExtSign s :: sign1
s _) _ mor :: morphism2
mor _) = do
    morphism2 -> Result ()
forall object morphism.
Category object morphism =>
morphism -> Result ()
legal_mor morphism2
mor
    case Result (sign2, [Named sentence2])
-> Maybe (sign2, [Named sentence2])
forall a. Result a -> Maybe a
maybeResult (Result (sign2, [Named sentence2])
 -> Maybe (sign2, [Named sentence2]))
-> Result (sign2, [Named sentence2])
-> Maybe (sign2, [Named sentence2])
forall a b. (a -> b) -> a -> b
$ 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
r sign1
s of
      Just (sigma' :: sign2
sigma', _) | sign2
sigma' sign2 -> sign2 -> Bool
forall a. Eq a => a -> a -> Bool
== morphism2 -> sign2
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism2
mor -> () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      _ -> String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "legal_mor.GMorphism2"

-- | Embedding of homogeneous signature morphisms as Grothendieck sig mors
gEmbed2 :: G_sign -> G_morphism -> GMorphism
gEmbed2 :: G_sign -> G_morphism -> GMorphism
gEmbed2 (G_sign lid2 :: lid
lid2 sig :: ExtSign sign symbol
sig si :: SigId
si) (G_morphism lid :: lid
lid mor :: morphism
mor ind :: MorId
ind) =
  let cid :: InclComorphism lid sublogics
cid = 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)
      Just sig1 :: ExtSign sign symbol
sig1 = lid
-> lid
-> String
-> ExtSign sign symbol
-> Maybe (ExtSign sign symbol)
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
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid2 (InclComorphism lid sublogics -> lid
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 InclComorphism lid sublogics
cid) "gEmbed2" ExtSign sign symbol
sig
  in InclComorphism lid sublogics
-> ExtSign sign symbol -> SigId -> morphism -> MorId -> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism InclComorphism lid sublogics
cid ExtSign sign symbol
sig1 SigId
si morphism
mor MorId
ind

-- | Embedding of homogeneous signature morphisms as Grothendieck sig mors
gEmbed :: G_morphism -> GMorphism
gEmbed :: G_morphism -> GMorphism
gEmbed (G_morphism lid :: lid
lid mor :: morphism
mor ind :: MorId
ind) = let sig :: sign
sig = morphism -> sign
forall object morphism.
Category object morphism =>
morphism -> object
dom morphism
mor in
  InclComorphism lid sublogics
-> ExtSign sign symbol -> SigId -> morphism -> MorId -> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism (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))
                (lid -> sign -> ExtSign sign symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign lid
lid sign
sig) SigId
startSigId morphism
mor MorId
ind

-- | Embedding of comorphisms as Grothendieck sig mors
gEmbedComorphism :: AnyComorphism -> G_sign -> Result GMorphism
gEmbedComorphism :: AnyComorphism -> G_sign -> Result GMorphism
gEmbedComorphism (Comorphism cid :: cid
cid) (G_sign lid :: lid
lid sig :: ExtSign sign symbol
sig ind :: SigId
ind) = do
  sig' :: ExtSign sign1 symbol1
sig'@(ExtSign s :: sign1
s _) <- lid
-> lid1
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign1 symbol1)
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
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid (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) "gEmbedComorphism" ExtSign sign symbol
sig
  (sigTar :: sign2
sigTar, _) <- 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
s
  GMorphism -> Result GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
cid ExtSign sign1 symbol1
sig' SigId
ind (sign2 -> morphism2
forall object morphism.
Category object morphism =>
object -> morphism
ide sign2
sigTar) MorId
startMorId)

-- | heterogeneous union of two Grothendieck signatures
gsigUnion :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
gsigUnion :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
gsigUnion lg :: LogicGraph
lg both :: Bool
both gsig1 :: G_sign
gsig1@(G_sign lid1 :: lid
lid1 (ExtSign sigma1 :: sign
sigma1 _) _)
          gsig2 :: G_sign
gsig2@(G_sign lid2 :: lid
lid2 (ExtSign sigma2 :: sign
sigma2 _) _) =
 if lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid1 AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
== lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid2
    then Bool -> G_sign -> G_sign -> Result G_sign
homogeneousGsigUnion Bool
both G_sign
gsig1 G_sign
gsig2
    else do
      (Comorphism cid1 :: cid
cid1, Comorphism cid2 :: cid
cid2) <-
            LogicGraph
-> AnyLogic -> AnyLogic -> Result (AnyComorphism, AnyComorphism)
logicUnion LogicGraph
lg (lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid1) (lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid2)
      let lidS1 :: lid1
lidS1 = 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
cid1
          lidS2 :: lid1
lidS2 = 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
          lidT1 :: lid2
lidT1 = 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
          lidT2 :: lid2
lidT2 = 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
cid2
      sign1
sigma1' <- lid -> lid1 -> String -> sign -> Result sign1
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 -> m sign2
coercePlainSign lid
lid1 lid1
lidS1 "Union of signaturesa" sign
sigma1
      sign1
sigma2' <- lid -> lid1 -> String -> sign -> Result sign1
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 -> m sign2
coercePlainSign lid
lid2 lid1
lidS2 "Union of signaturesb" sign
sigma2
      (sigma1'' :: sign2
sigma1'', _) <- cid -> sign1 -> Result (sign2, [Named sentence2])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sign1 -> Result (sign2, [Named sentence2])
map_sign cid
cid1 sign1
sigma1'  -- where to put axioms???
      (sigma2'' :: sign2
sigma2'', _) <- 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
cid2 sign1
sigma2'  -- where to put axioms???
      sign2
sigma2''' <- lid2 -> lid2 -> String -> sign2 -> Result sign2
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 -> m sign2
coercePlainSign lid2
lidT2 lid2
lidT1 "Union of signaturesc" sign2
sigma2''
      sign2
sigma3 <- lid2 -> sign2 -> sign2 -> Result sign2
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 sign
signature_union lid2
lidT1 sign2
sigma1'' sign2
sigma2'''
      G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign -> Result G_sign) -> G_sign -> Result G_sign
forall a b. (a -> b) -> a -> b
$ lid2 -> ExtSign sign2 symbol2 -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign lid2
lidT1 (sign2 -> Set symbol2 -> ExtSign sign2 symbol2
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign sign2
sigma3 (Set symbol2 -> ExtSign sign2 symbol2)
-> Set symbol2 -> ExtSign sign2 symbol2
forall a b. (a -> b) -> a -> b
$ lid2 -> sign2 -> Set symbol2
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid2
lidT1
                            (sign2 -> Set symbol2) -> sign2 -> Set symbol2
forall a b. (a -> b) -> a -> b
$ if Bool
both then sign2
sigma3 else sign2
sigma2''') SigId
startSigId

-- | homogeneous Union of two Grothendieck signatures
homogeneousGsigUnion :: Bool -> G_sign -> G_sign -> Result G_sign
homogeneousGsigUnion :: Bool -> G_sign -> G_sign -> Result G_sign
homogeneousGsigUnion both :: Bool
both (G_sign lid1 :: lid
lid1 sigma1 :: ExtSign sign symbol
sigma1 _) (G_sign lid2 :: lid
lid2 sigma2 :: ExtSign sign symbol
sigma2 _) = do
  sigma2' :: ExtSign sign symbol
sigma2'@(ExtSign sig2 :: sign
sig2 _) <- lid
-> lid
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign symbol)
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
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid2 lid
lid1 "Union of signatures" ExtSign sign symbol
sigma2
  sigma3 :: ExtSign sign symbol
sigma3@(ExtSign sig3 :: sign
sig3 _) <- lid
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result (ExtSign sign symbol)
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result (ExtSign sign symbol)
ext_signature_union lid
lid1 ExtSign sign symbol
sigma1 ExtSign sign symbol
sigma2'
  G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign -> Result G_sign) -> G_sign -> Result G_sign
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign lid
lid1
             (if Bool
both then ExtSign sign symbol
sigma3 else sign -> Set symbol -> ExtSign sign symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign sign
sig3 (Set symbol -> ExtSign sign symbol)
-> Set symbol -> ExtSign sign symbol
forall a b. (a -> b) -> a -> b
$ lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
lid1 sign
sig2)
         SigId
startSigId

homGsigDiff :: G_sign -> G_sign -> Result G_sign
homGsigDiff :: G_sign -> G_sign -> Result G_sign
homGsigDiff (G_sign lid1 :: lid
lid1 (ExtSign s1 :: sign
s1 _) _) (G_sign lid2 :: lid
lid2 (ExtSign s2 :: sign
s2 _) _) = do
  sign
s3 <- lid -> lid -> String -> sign -> Result sign
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 -> m sign2
coercePlainSign lid
lid2 lid
lid1 "hom differerence of signatures" sign
s2
  sign
s4 <- lid -> sign -> sign -> Result sign
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 sign
signatureDiff lid
lid1 sign
s1 sign
s3
  G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign -> Result G_sign) -> G_sign -> Result G_sign
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign lid
lid1 (lid -> sign -> ExtSign sign symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign lid
lid1 sign
s4) SigId
startSigId

-- | union of a list of Grothendieck signatures
gsigManyUnion :: LogicGraph -> [G_sign] -> Result G_sign
gsigManyUnion :: LogicGraph -> [G_sign] -> Result G_sign
gsigManyUnion _ [] =
  String -> Result G_sign
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "union of emtpy list of signatures"
gsigManyUnion lg :: LogicGraph
lg (gsigma :: G_sign
gsigma : gsigmas :: [G_sign]
gsigmas) =
  (G_sign -> G_sign -> Result G_sign)
-> G_sign -> [G_sign] -> Result G_sign
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
gsigUnion LogicGraph
lg Bool
True) G_sign
gsigma [G_sign]
gsigmas

-- | homogeneous Union of a list of morphisms
homogeneousMorManyUnion :: [G_morphism] -> Result G_morphism
homogeneousMorManyUnion :: [G_morphism] -> Result G_morphism
homogeneousMorManyUnion [] =
  String -> Result G_morphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "homogeneous union of emtpy list of morphisms"
homogeneousMorManyUnion (gmor :: G_morphism
gmor : gmors :: [G_morphism]
gmors) =
  (G_morphism -> G_morphism -> Result G_morphism)
-> G_morphism -> [G_morphism] -> Result G_morphism
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ( \ (G_morphism lid2 :: lid
lid2 mor2 :: morphism
mor2 _) (G_morphism lid1 mor1 _) -> do
            morphism
mor1' <- lid -> lid -> String -> morphism -> Result morphism
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 lid
lid1 lid
lid2 "homogeneousMorManyUnion" morphism
mor1
            morphism
mor <- lid -> morphism -> morphism -> Result morphism
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 -> morphism -> morphism -> Result morphism
morphism_union lid
lid2 morphism
mor1' morphism
mor2
            G_morphism -> Result G_morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (lid -> morphism -> MorId -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> MorId -> G_morphism
G_morphism lid
lid2 morphism
mor MorId
startMorId)) G_morphism
gmor [G_morphism]
gmors

-- | intersection of a list of Grothendieck signatures
gsigManyIntersect :: LogicGraph -> [G_sign] -> Result G_sign
gsigManyIntersect :: LogicGraph -> [G_sign] -> Result G_sign
gsigManyIntersect _ [] =
  String -> Result G_sign
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "intersection of emtpy list of signatures"
gsigManyIntersect lg :: LogicGraph
lg (gsigma :: G_sign
gsigma : gsigmas :: [G_sign]
gsigmas) =
  (G_sign -> G_sign -> Result G_sign)
-> G_sign -> [G_sign] -> Result G_sign
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
gsigIntersect LogicGraph
lg Bool
True) G_sign
gsigma [G_sign]
gsigmas

-- | heterogeneous union of two Grothendieck signatures
gsigIntersect :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
gsigIntersect :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
gsigIntersect _lg :: LogicGraph
_lg both :: Bool
both gsig1 :: G_sign
gsig1@(G_sign lid1 :: lid
lid1 (ExtSign _sigma1 :: sign
_sigma1 _) _)
          gsig2 :: G_sign
gsig2@(G_sign lid2 :: lid
lid2 (ExtSign _sigma2 :: sign
_sigma2 _) _) =
 if lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid1 AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
== lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid2
    then Bool -> G_sign -> G_sign -> Result G_sign
homogeneousGsigIntersect Bool
both G_sign
gsig1 G_sign
gsig2
    else String -> Result G_sign
forall a. HasCallStack => String -> a
error "intersection of heterogeneous signatures is not supported yet"

-- | homogeneous intersection of two Grothendieck signatures
homogeneousGsigIntersect :: Bool -> G_sign -> G_sign -> Result G_sign
homogeneousGsigIntersect :: Bool -> G_sign -> G_sign -> Result G_sign
homogeneousGsigIntersect _both :: Bool
_both (G_sign lid1 :: lid
lid1 sigma1 :: ExtSign sign symbol
sigma1@(ExtSign _sig1 :: sign
_sig1 syms1 :: Set symbol
syms1) _) (G_sign lid2 :: lid
lid2 sigma2 :: ExtSign sign symbol
sigma2 _) = do
  sigma2' :: ExtSign sign symbol
sigma2'@(ExtSign sig2 :: sign
sig2 _) <- lid
-> lid
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign symbol)
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
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid2 lid
lid1 "Intersection of signatures" ExtSign sign symbol
sigma2
  ExtSign sig3 :: sign
sig3 _ <- lid
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result (ExtSign sign symbol)
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result (ExtSign sign symbol)
ext_signature_intersect lid
lid1 ExtSign sign symbol
sigma1 ExtSign sign symbol
sigma2'
  let syms2 :: Set symbol
syms2 = lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
lid1 sign
sig2
      symI :: Set symbol
symI = Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set symbol
syms1 Set symbol
syms2
  G_sign -> Result G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign -> Result G_sign) -> G_sign -> Result G_sign
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign lid
lid1
             (sign -> Set symbol -> ExtSign sign symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign sign
sig3 Set symbol
symI)
         SigId
startSigId

-- | inclusion between two logics
logicInclusion :: LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicInclusion :: LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicInclusion logicGraph :: LogicGraph
logicGraph l1 :: AnyLogic
l1@(Logic lid1 :: lid
lid1) (Logic lid2 :: lid
lid2) =
     let ln1 :: String
ln1 = lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid1
         ln2 :: String
ln2 = lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid2 in
     if String
ln1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
ln2 then
       AnyComorphism -> Result AnyComorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (AnyLogic -> AnyComorphism
idComorphism AnyLogic
l1)
      else case (String, String)
-> Map (String, String) AnyComorphism -> Maybe AnyComorphism
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (String
ln1, String
ln2) (LogicGraph -> Map (String, String) AnyComorphism
inclusions LogicGraph
logicGraph) of
           Just (Comorphism i :: cid
i) ->
               AnyComorphism -> Result AnyComorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (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
i)
           Nothing ->
               String -> Result AnyComorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("No inclusion from " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ln1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ln2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " found")

updateMorIndex :: MorId -> GMorphism -> GMorphism
updateMorIndex :: MorId -> GMorphism -> GMorphism
updateMorIndex i :: MorId
i (GMorphism cid :: cid
cid sign :: ExtSign sign1 symbol1
sign si :: SigId
si mor :: morphism2
mor _) = cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
cid ExtSign sign1 symbol1
sign SigId
si morphism2
mor MorId
i

toG_morphism :: GMorphism -> G_morphism
toG_morphism :: GMorphism -> G_morphism
toG_morphism (GMorphism cid :: cid
cid _ _ mor :: morphism2
mor i :: MorId
i) = lid2 -> morphism2 -> MorId -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> MorId -> G_morphism
G_morphism (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) morphism2
mor MorId
i

gSigCoerce :: LogicGraph -> G_sign -> AnyLogic
           -> Result (G_sign, AnyComorphism)
gSigCoerce :: LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism)
gSigCoerce lg :: LogicGraph
lg g :: G_sign
g@(G_sign lid1 :: lid
lid1 sigma1 :: ExtSign sign symbol
sigma1 _) l2 :: AnyLogic
l2@(Logic lid2 :: lid
lid2) =
  if lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid1 AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
== lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid2
    then (G_sign, AnyComorphism) -> Result (G_sign, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign
g, AnyLogic -> AnyComorphism
idComorphism AnyLogic
l2) else do
    cmor :: AnyComorphism
cmor@(Comorphism i :: cid
i) <- LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicInclusion LogicGraph
lg (lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid1) AnyLogic
l2
    ExtSign sigma1' :: sign1
sigma1' sy :: Set symbol1
sy <-
        lid
-> lid1
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign1 symbol1)
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
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
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
i) "gSigCoerce of signature" ExtSign sign symbol
sigma1
    (sigma1'' :: sign2
sigma1'', _) <- cid -> sign1 -> Result (sign2, [Named sentence2])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sign1 -> Result (sign2, [Named sentence2])
map_sign cid
i sign1
sigma1'
    Set symbol2
sys <- Set symbol2 -> Result (Set symbol2)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set symbol2 -> Result (Set symbol2))
-> ([symbol1] -> Set symbol2) -> [symbol1] -> Result (Set symbol2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set symbol2] -> Set symbol2
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set symbol2] -> Set symbol2)
-> ([symbol1] -> [Set symbol2]) -> [symbol1] -> Set symbol2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (symbol1 -> Set symbol2) -> [symbol1] -> [Set symbol2]
forall a b. (a -> b) -> [a] -> [b]
map (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
map_symbol cid
i sign1
sigma1') ([symbol1] -> Result (Set symbol2))
-> [symbol1] -> Result (Set symbol2)
forall a b. (a -> b) -> a -> b
$ Set symbol1 -> [symbol1]
forall a. Set a -> [a]
Set.toList Set symbol1
sy
    let lid :: lid2
lid = 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
i
    (G_sign, AnyComorphism) -> Result (G_sign, AnyComorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (lid2 -> ExtSign sign2 symbol2 -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign lid2
lid (sign2 -> Set symbol2 -> ExtSign sign2 symbol2
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign sign2
sigma1'' Set symbol2
sys) SigId
startSigId, AnyComorphism
cmor)

-- | inclusion morphism between two Grothendieck signatures
ginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion = Bool -> LogicGraph -> G_sign -> G_sign -> Result GMorphism
inclusionAux Bool
True

inclusionAux :: Bool -> LogicGraph -> G_sign -> G_sign -> Result GMorphism
inclusionAux :: Bool -> LogicGraph -> G_sign -> G_sign -> Result GMorphism
inclusionAux guard :: Bool
guard lg :: LogicGraph
lg (G_sign lid1 :: lid
lid1 sigma1 :: ExtSign sign symbol
sigma1 ind :: SigId
ind) (G_sign lid2 :: lid
lid2 sigma2 :: ExtSign sign symbol
sigma2 _) = do
    Comorphism i :: cid
i <- LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicInclusion LogicGraph
lg (lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid1) (lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid2)
    ext1 :: ExtSign sign1 symbol1
ext1@(ExtSign sigma1' :: sign1
sigma1' _) <-
        lid
-> lid1
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign1 symbol1)
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
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
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
i) "Inclusion of signatures" ExtSign sign symbol
sigma1
    (sigma1'' :: sign2
sigma1'', _) <- cid -> sign1 -> Result (sign2, [Named sentence2])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sign1 -> Result (sign2, [Named sentence2])
map_sign cid
i sign1
sigma1'
    ExtSign sigma2' :: sign2
sigma2' _ <-
        lid
-> lid2
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign2 symbol2)
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
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid2 (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
i) "Inclusion of signatures" ExtSign sign symbol
sigma2
    morphism2
mor <- (if Bool
guard then 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 else 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
subsig_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
i) sign2
sigma1'' sign2
sigma2'
    GMorphism -> Result GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
i ExtSign sign1 symbol1
ext1 SigId
ind morphism2
mor MorId
startMorId)

genCompInclusion :: (G_sign -> G_sign -> Result GMorphism)
                 -> GMorphism -> GMorphism -> Result GMorphism
genCompInclusion :: (G_sign -> G_sign -> Result GMorphism)
-> GMorphism -> GMorphism -> Result GMorphism
genCompInclusion f :: G_sign -> G_sign -> Result GMorphism
f mor1 :: GMorphism
mor1 mor2 :: GMorphism
mor2 = do
  let sigma1 :: G_sign
sigma1 = GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
mor1
      sigma2 :: G_sign
sigma2 = GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
dom GMorphism
mor2
  GMorphism
incl <- G_sign -> G_sign -> Result GMorphism
f G_sign
sigma1 G_sign
sigma2
  GMorphism
mor <- GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms GMorphism
mor1 GMorphism
incl
  GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms GMorphism
mor GMorphism
mor2

{- | Composition of two Grothendieck signature morphisms
with intermediate inclusion -}
compInclusion :: LogicGraph -> GMorphism -> GMorphism -> Result GMorphism
compInclusion :: LogicGraph -> GMorphism -> GMorphism -> Result GMorphism
compInclusion = (G_sign -> G_sign -> Result GMorphism)
-> GMorphism -> GMorphism -> Result GMorphism
genCompInclusion ((G_sign -> G_sign -> Result GMorphism)
 -> GMorphism -> GMorphism -> Result GMorphism)
-> (LogicGraph -> G_sign -> G_sign -> Result GMorphism)
-> LogicGraph
-> GMorphism
-> GMorphism
-> Result GMorphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> LogicGraph -> G_sign -> G_sign -> Result GMorphism
inclusionAux Bool
False

-- | Find compositions of comorphisms starting from a give logic
-- | use wheted graph of logics to optimize search
findComorphismPaths :: LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismPaths :: LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismPaths lg :: LogicGraph
lg gsubl :: G_sublogics
gsubl = [AnyComorphism] -> [AnyComorphism]
forall a. Ord a => [a] -> [a]
nubOrd ([AnyComorphism] -> [AnyComorphism])
-> [AnyComorphism] -> [AnyComorphism]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismCompositions LogicGraph
lg G_sublogics
gsubl

-- | graph representation of the logic graph
logicGraph2Graph :: LogicGraph
                    -> Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism
logicGraph2Graph :: LogicGraph
-> Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism
logicGraph2Graph lg :: LogicGraph
lg =
 let relevantMorphisms :: [AnyComorphism]
relevantMorphisms = (AnyComorphism -> Bool) -> [AnyComorphism] -> [AnyComorphism]
forall a. (a -> Bool) -> [a] -> [a]
filter (\x :: AnyComorphism
x -> AnyComorphism -> Bool
hasModelExpansion AnyComorphism
x Bool -> Bool -> Bool
&& AnyComorphism -> Bool
isRps AnyComorphism
x Bool -> Bool -> Bool
&& AnyComorphism -> Bool
isEps AnyComorphism
x) ([AnyComorphism] -> [AnyComorphism])
-> (Map String AnyComorphism -> [AnyComorphism])
-> Map String AnyComorphism
-> [AnyComorphism]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String AnyComorphism -> [AnyComorphism]
forall k a. Map k a -> [a]
Map.elems 
                         (Map String AnyComorphism -> [AnyComorphism])
-> Map String AnyComorphism -> [AnyComorphism]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyComorphism
comorphisms LogicGraph
lg
 in Graph :: forall node edge.
(node -> [(edge, node)]) -> (edge -> Int) -> Graph node edge
Graph {
  neighbours :: (G_sublogics, Maybe AnyComorphism)
-> [(AnyComorphism, (G_sublogics, Maybe AnyComorphism))]
neighbours = \ (G_sublogics lid :: lid
lid sl :: sublogics
sl, c1 :: Maybe AnyComorphism
c1) ->
  let coerce :: cid -> sublogics1 -> sublogics1
coerce c :: cid
c = lid -> lid2 -> sublogics1 -> 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 lid
lid (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 -> lid1
sourceLogic cid
c)
  in (AnyComorphism
 -> Maybe (AnyComorphism, (G_sublogics, Maybe AnyComorphism)))
-> [AnyComorphism]
-> [(AnyComorphism, (G_sublogics, Maybe AnyComorphism))]
forall a b. (a -> Maybe b) -> [a] -> [b]
Data.Maybe.mapMaybe
      (\ (Comorphism c :: cid
c) -> Maybe (AnyComorphism, (G_sublogics, Maybe AnyComorphism))
-> (sublogics2
    -> Maybe (AnyComorphism, (G_sublogics, Maybe AnyComorphism)))
-> Maybe sublogics2
-> Maybe (AnyComorphism, (G_sublogics, Maybe AnyComorphism))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe (AnyComorphism, (G_sublogics, Maybe AnyComorphism))
forall a. Maybe a
Nothing (\ sl1 :: sublogics2
sl1 -> (AnyComorphism, (G_sublogics, Maybe AnyComorphism))
-> Maybe (AnyComorphism, (G_sublogics, Maybe AnyComorphism))
forall a. a -> Maybe a
Just (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
c,
       (lid2 -> sublogics2 -> G_sublogics
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sublogics -> G_sublogics
G_sublogics (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
c) sublogics2
sl1, AnyComorphism -> Maybe AnyComorphism
forall a. a -> Maybe a
Just (AnyComorphism -> Maybe AnyComorphism)
-> AnyComorphism -> Maybe AnyComorphism
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
c)))
                (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
c (cid -> sublogics -> sublogics1
forall cid lid2 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 sublogics1
       basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1
       symbol1 raw_symbol1 proof_tree1.
(Comorphism
   cid
   lid2
   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
   lid
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1) =>
cid -> sublogics1 -> sublogics1
coerce cid
c sublogics
sl))) ([AnyComorphism]
 -> [(AnyComorphism, (G_sublogics, Maybe AnyComorphism))])
-> [AnyComorphism]
-> [(AnyComorphism, (G_sublogics, Maybe AnyComorphism))]
forall a b. (a -> b) -> a -> b
$
      (AnyComorphism -> Bool) -> [AnyComorphism] -> [AnyComorphism]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Comorphism c :: cid
c) -> lid1 -> AnyLogic
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 -> AnyLogic
Logic (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
c) AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
== lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid
      Bool -> Bool -> Bool
&& sublogics1 -> sublogics1 -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem (cid -> sublogics -> sublogics1
forall cid lid2 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 sublogics1
       basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1
       symbol1 raw_symbol1 proof_tree1.
(Comorphism
   cid
   lid2
   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
   lid
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1) =>
cid -> sublogics1 -> sublogics1
coerce cid
c sublogics
sl) (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
c)
      Bool -> Bool -> Bool
&& (case Maybe AnyComorphism
c1 of
            Just (Comorphism c1' :: cid
c1') -> cid -> String
forall a. Show a => a -> String
show cid
c1' String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= cid -> String
forall a. Show a => a -> String
show cid
c
            _ -> Bool
True)) [AnyComorphism]
relevantMorphisms,
  weight :: AnyComorphism -> Int
weight = \ (Comorphism c :: cid
c) -> if lid1 -> AnyLogic
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 -> AnyLogic
Logic (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
c) AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
==
                                 lid2 -> AnyLogic
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 -> AnyLogic
Logic (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
c) then 1 else 3
 }

-- | finds first comorphism with a matching sublogic
findComorphism :: Fail.MonadFail m => G_sublogics -> [AnyComorphism] -> m AnyComorphism
findComorphism :: G_sublogics -> [AnyComorphism] -> m AnyComorphism
findComorphism _ [] = String -> m AnyComorphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "No matching comorphism found"
findComorphism gsl :: G_sublogics
gsl@(G_sublogics lid :: lid
lid sub :: sublogics
sub) (Comorphism cid :: cid
cid : rest :: [AnyComorphism]
rest) =
    let 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
cid in
    if lid -> AnyLogic
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 -> AnyLogic
Logic lid
lid AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
== lid1 -> AnyLogic
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 -> AnyLogic
Logic lid1
l2
      Bool -> Bool -> Bool
&& sublogics1 -> sublogics1 -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
isSubElem (lid -> lid1 -> sublogics -> 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 lid
lid lid1
l2 sublogics
sub) (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)
    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
$ 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
    else G_sublogics -> [AnyComorphism] -> m AnyComorphism
forall (m :: * -> *).
MonadFail m =>
G_sublogics -> [AnyComorphism] -> m AnyComorphism
findComorphism G_sublogics
gsl [AnyComorphism]
rest

{- | check transportability of Grothendieck signature morphisms
(currently returns false for heterogeneous morphisms) -}
isTransportable :: GMorphism -> Bool
isTransportable :: GMorphism -> Bool
isTransportable (GMorphism cid :: cid
cid _ ind1 :: SigId
ind1 mor :: morphism2
mor ind2 :: MorId
ind2) =
    SigId
ind1 SigId -> SigId -> Bool
forall a. Ord a => a -> a -> Bool
> SigId
startSigId Bool -> Bool -> Bool
&& MorId
ind2 MorId -> MorId -> Bool
forall a. Ord a => a -> a -> Bool
> MorId
startMorId
    Bool -> Bool -> Bool
&& AnyComorphism -> Bool
isModelTransportable (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)
    Bool -> Bool -> Bool
&& lid2 -> morphism2 -> Bool
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 -> morphism -> Bool
is_transportable (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) morphism2
mor

-- * Lax triangles and weakly amalgamable squares of lax triangles

{- a lax triangle looks like:
            laxTarget
  i -------------------------------------> k
                  ^  laxModif
                 | |
  i ------------- > j -------------------> k
       laxFst              laxSnd

and I_k is quasi-semi-exact -}

data LaxTriangle = LaxTriangle {
                     LaxTriangle -> AnyModification
laxModif :: AnyModification,
                     LaxTriangle -> AnyComorphism
laxFst, LaxTriangle -> AnyComorphism
laxSnd, LaxTriangle -> AnyComorphism
laxTarget :: AnyComorphism
                   } deriving (Int -> LaxTriangle -> ShowS
[LaxTriangle] -> ShowS
LaxTriangle -> String
(Int -> LaxTriangle -> ShowS)
-> (LaxTriangle -> String)
-> ([LaxTriangle] -> ShowS)
-> Show LaxTriangle
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LaxTriangle] -> ShowS
$cshowList :: [LaxTriangle] -> ShowS
show :: LaxTriangle -> String
$cshow :: LaxTriangle -> String
showsPrec :: Int -> LaxTriangle -> ShowS
$cshowsPrec :: Int -> LaxTriangle -> ShowS
Show, LaxTriangle -> LaxTriangle -> Bool
(LaxTriangle -> LaxTriangle -> Bool)
-> (LaxTriangle -> LaxTriangle -> Bool) -> Eq LaxTriangle
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LaxTriangle -> LaxTriangle -> Bool
$c/= :: LaxTriangle -> LaxTriangle -> Bool
== :: LaxTriangle -> LaxTriangle -> Bool
$c== :: LaxTriangle -> LaxTriangle -> Bool
Eq, Eq LaxTriangle
Eq LaxTriangle =>
(LaxTriangle -> LaxTriangle -> Ordering)
-> (LaxTriangle -> LaxTriangle -> Bool)
-> (LaxTriangle -> LaxTriangle -> Bool)
-> (LaxTriangle -> LaxTriangle -> Bool)
-> (LaxTriangle -> LaxTriangle -> Bool)
-> (LaxTriangle -> LaxTriangle -> LaxTriangle)
-> (LaxTriangle -> LaxTriangle -> LaxTriangle)
-> Ord LaxTriangle
LaxTriangle -> LaxTriangle -> Bool
LaxTriangle -> LaxTriangle -> Ordering
LaxTriangle -> LaxTriangle -> LaxTriangle
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: LaxTriangle -> LaxTriangle -> LaxTriangle
$cmin :: LaxTriangle -> LaxTriangle -> LaxTriangle
max :: LaxTriangle -> LaxTriangle -> LaxTriangle
$cmax :: LaxTriangle -> LaxTriangle -> LaxTriangle
>= :: LaxTriangle -> LaxTriangle -> Bool
$c>= :: LaxTriangle -> LaxTriangle -> Bool
> :: LaxTriangle -> LaxTriangle -> Bool
$c> :: LaxTriangle -> LaxTriangle -> Bool
<= :: LaxTriangle -> LaxTriangle -> Bool
$c<= :: LaxTriangle -> LaxTriangle -> Bool
< :: LaxTriangle -> LaxTriangle -> Bool
$c< :: LaxTriangle -> LaxTriangle -> Bool
compare :: LaxTriangle -> LaxTriangle -> Ordering
$ccompare :: LaxTriangle -> LaxTriangle -> Ordering
$cp1Ord :: Eq LaxTriangle
Ord)
{- a weakly amalgamable square of lax triangles
consists of two lax triangles with the same laxTarget -}

data Square = Square {
                 Square -> LaxTriangle
leftTriangle, Square -> LaxTriangle
rightTriangle :: LaxTriangle
              } deriving (Int -> Square -> ShowS
[Square] -> ShowS
Square -> String
(Int -> Square -> ShowS)
-> (Square -> String) -> ([Square] -> ShowS) -> Show Square
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Square] -> ShowS
$cshowList :: [Square] -> ShowS
show :: Square -> String
$cshow :: Square -> String
showsPrec :: Int -> Square -> ShowS
$cshowsPrec :: Int -> Square -> ShowS
Show, Square -> Square -> Bool
(Square -> Square -> Bool)
-> (Square -> Square -> Bool) -> Eq Square
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Square -> Square -> Bool
$c/= :: Square -> Square -> Bool
== :: Square -> Square -> Bool
$c== :: Square -> Square -> Bool
Eq, Eq Square
Eq Square =>
(Square -> Square -> Ordering)
-> (Square -> Square -> Bool)
-> (Square -> Square -> Bool)
-> (Square -> Square -> Bool)
-> (Square -> Square -> Bool)
-> (Square -> Square -> Square)
-> (Square -> Square -> Square)
-> Ord Square
Square -> Square -> Bool
Square -> Square -> Ordering
Square -> Square -> Square
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Square -> Square -> Square
$cmin :: Square -> Square -> Square
max :: Square -> Square -> Square
$cmax :: Square -> Square -> Square
>= :: Square -> Square -> Bool
$c>= :: Square -> Square -> Bool
> :: Square -> Square -> Bool
$c> :: Square -> Square -> Bool
<= :: Square -> Square -> Bool
$c<= :: Square -> Square -> Bool
< :: Square -> Square -> Bool
$c< :: Square -> Square -> Bool
compare :: Square -> Square -> Ordering
$ccompare :: Square -> Square -> Ordering
$cp1Ord :: Eq Square
Ord)

-- for deriving Eq, first equality for modifications is needed

mkIdSquare :: AnyLogic -> Square
mkIdSquare :: AnyLogic -> Square
mkIdSquare (Logic lid :: lid
lid) = let
   idCom :: AnyComorphism
idCom = 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))
   idMod :: AnyModification
idMod = AnyComorphism -> AnyModification
idModification AnyComorphism
idCom
   idTriangle :: LaxTriangle
idTriangle = LaxTriangle :: AnyModification
-> AnyComorphism -> AnyComorphism -> AnyComorphism -> LaxTriangle
LaxTriangle {
                 laxModif :: AnyModification
laxModif = AnyModification
idMod,
                 laxFst :: AnyComorphism
laxFst = AnyComorphism
idCom,
                 laxSnd :: AnyComorphism
laxSnd = AnyComorphism
idCom,
                 laxTarget :: AnyComorphism
laxTarget = AnyComorphism
idCom}
 in Square :: LaxTriangle -> LaxTriangle -> Square
Square {leftTriangle :: LaxTriangle
leftTriangle = LaxTriangle
idTriangle, rightTriangle :: LaxTriangle
rightTriangle = LaxTriangle
idTriangle}

mkDefSquare :: AnyComorphism -> Square
mkDefSquare :: AnyComorphism -> Square
mkDefSquare c1 :: AnyComorphism
c1@(Comorphism cid1 :: cid
cid1) = let
  idComS :: AnyComorphism
idComS = InclComorphism lid1 sublogics1 -> 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 (InclComorphism lid1 sublogics1 -> AnyComorphism)
-> InclComorphism lid1 sublogics1 -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ lid1 -> sublogics1 -> InclComorphism 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 -> InclComorphism lid sublogics
mkIdComorphism (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
cid1) (sublogics1 -> InclComorphism lid1 sublogics1)
-> sublogics1 -> InclComorphism lid1 sublogics1
forall a b. (a -> b) -> a -> b
$
           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
cid1
  idComT :: AnyComorphism
idComT = InclComorphism lid2 sublogics2 -> 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 (InclComorphism lid2 sublogics2 -> AnyComorphism)
-> InclComorphism lid2 sublogics2 -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ lid2 -> sublogics2 -> InclComorphism 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 -> InclComorphism lid sublogics
mkIdComorphism (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) (sublogics2 -> InclComorphism lid2 sublogics2)
-> sublogics2 -> InclComorphism lid2 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
cid1
  idMod :: AnyModification
idMod = AnyComorphism -> AnyModification
idModification AnyComorphism
c1
  lTriangle :: LaxTriangle
lTriangle = LaxTriangle :: AnyModification
-> AnyComorphism -> AnyComorphism -> AnyComorphism -> LaxTriangle
LaxTriangle {
               laxModif :: AnyModification
laxModif = AnyModification
idMod,
               laxFst :: AnyComorphism
laxFst = AnyComorphism
c1,
               laxSnd :: AnyComorphism
laxSnd = AnyComorphism
idComS,
               laxTarget :: AnyComorphism
laxTarget = AnyComorphism
c1
              }
  rTriangle :: LaxTriangle
rTriangle = LaxTriangle :: AnyModification
-> AnyComorphism -> AnyComorphism -> AnyComorphism -> LaxTriangle
LaxTriangle {
               laxModif :: AnyModification
laxModif = AnyModification
idMod,
               laxFst :: AnyComorphism
laxFst = AnyComorphism
idComT,
               laxSnd :: AnyComorphism
laxSnd = AnyComorphism
c1,
               laxTarget :: AnyComorphism
laxTarget = AnyComorphism
c1
              }
 in Square :: LaxTriangle -> LaxTriangle -> Square
Square {leftTriangle :: LaxTriangle
leftTriangle = LaxTriangle
lTriangle, rightTriangle :: LaxTriangle
rightTriangle = LaxTriangle
rTriangle}

mirrorSquare :: Square -> Square
mirrorSquare :: Square -> Square
mirrorSquare s :: Square
s = Square :: LaxTriangle -> LaxTriangle -> Square
Square {
                 leftTriangle :: LaxTriangle
leftTriangle = Square -> LaxTriangle
rightTriangle Square
s,
                 rightTriangle :: LaxTriangle
rightTriangle = Square -> LaxTriangle
leftTriangle Square
s}

lookupSquare :: AnyComorphism -> AnyComorphism -> LogicGraph -> Result [Square]
lookupSquare :: AnyComorphism -> AnyComorphism -> LogicGraph -> Result [Square]
lookupSquare com1 :: AnyComorphism
com1 com2 :: AnyComorphism
com2 lg :: LogicGraph
lg = Result [Square]
-> ([Square] -> Result [Square])
-> Maybe [Square]
-> Result [Square]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Result [Square]
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "lookupSquare") [Square] -> Result [Square]
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Square] -> Result [Square])
-> Maybe [Square] -> Result [Square]
forall a b. (a -> b) -> a -> b
$ do
  [Square]
sqL1 <- (AnyComorphism, AnyComorphism)
-> Map (AnyComorphism, AnyComorphism) [Square] -> Maybe [Square]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (AnyComorphism
com1, AnyComorphism
com2) (Map (AnyComorphism, AnyComorphism) [Square] -> Maybe [Square])
-> Map (AnyComorphism, AnyComorphism) [Square] -> Maybe [Square]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map (AnyComorphism, AnyComorphism) [Square]
squares LogicGraph
lg
  [Square]
sqL2 <- (AnyComorphism, AnyComorphism)
-> Map (AnyComorphism, AnyComorphism) [Square] -> Maybe [Square]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (AnyComorphism
com2, AnyComorphism
com1) (Map (AnyComorphism, AnyComorphism) [Square] -> Maybe [Square])
-> Map (AnyComorphism, AnyComorphism) [Square] -> Maybe [Square]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map (AnyComorphism, AnyComorphism) [Square]
squares LogicGraph
lg
  [Square] -> Maybe [Square]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Square] -> Maybe [Square]) -> [Square] -> Maybe [Square]
forall a b. (a -> b) -> a -> b
$ [Square] -> [Square]
forall a. Ord a => [a] -> [a]
nubOrd ([Square] -> [Square]) -> [Square] -> [Square]
forall a b. (a -> b) -> a -> b
$ [Square]
sqL1 [Square] -> [Square] -> [Square]
forall a. [a] -> [a] -> [a]
++ (Square -> Square) -> [Square] -> [Square]
forall a b. (a -> b) -> [a] -> [b]
map Square -> Square
mirrorSquare [Square]
sqL2
  -- maybe adjusted if comparing AnyModifications change

-- | algo for searching comorphism paths
weight_limit :: Int
weight_limit :: Int
weight_limit = 4

times_logic_in_branch :: Int
times_logic_in_branch :: Int
times_logic_in_branch = 3

data SearchNode = SearchNode
  { SearchNode -> Int
nodeId :: Int,
    SearchNode -> Int
parentId :: Int,
    SearchNode -> String
logicName :: String,
    -- to check wether comorphism already used in branch
    SearchNode -> HashSet String
usedComorphisms :: HSet.HashSet String,
    -- number of time particular logic is used in branch
    SearchNode -> HashMap String Int
timesLogicUsed :: HMap.HashMap String Int,
    -- all comorphism composition in current branch, latest one in the head of the list
    SearchNode -> [AnyComorphism]
cCompositions :: [AnyComorphism],
    -- name of comorphism though wich we get this node from parent
    SearchNode -> String
comName :: String,
    -- weight of comorphism leading to that node
    SearchNode -> Int
comWeight :: Int
  }
  deriving (Int -> SearchNode -> ShowS
[SearchNode] -> ShowS
SearchNode -> String
(Int -> SearchNode -> ShowS)
-> (SearchNode -> String)
-> ([SearchNode] -> ShowS)
-> Show SearchNode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SearchNode] -> ShowS
$cshowList :: [SearchNode] -> ShowS
show :: SearchNode -> String
$cshow :: SearchNode -> String
showsPrec :: Int -> SearchNode -> ShowS
$cshowsPrec :: Int -> SearchNode -> ShowS
Show)

data SearchState = SearchState
  {
    SearchState -> HashMap Int SearchNode
searchNodes :: HMap.HashMap Int SearchNode,
    -- ids of nodes who are currently leaves in search tree
    SearchState -> HashSet Int
leaves :: HSet.HashSet Int,
    -- distances of nodes in priority queues to root node
    SearchState -> HashMap Int Int
distance :: HMap.HashMap Int Int,
    -- priority queue of nodes according their distances: higher distance - higher priority
    SearchState -> MinPrioHeap Int Int
pQueue :: Heap.MinPrioHeap Int Int,
    -- map logic map to comorphis with it as source logic
    SearchState -> HashMap String [String]
logicToComorphisms :: HMap.HashMap String [String],
    -- this field = <last node id in searchNodes> + 1.
    -- used for proper id generation of children nodes
    SearchState -> Int
nextNodeId :: Int
  }

initState :: LogicGraph -> G_sublogics -> SearchState
initState :: LogicGraph -> G_sublogics -> SearchState
initState lg :: LogicGraph
lg (G_sublogics lid :: lid
lid sub :: sublogics
sub) =
  SearchState :: HashMap Int SearchNode
-> HashSet Int
-> HashMap Int Int
-> MinPrioHeap Int Int
-> HashMap String [String]
-> Int
-> SearchState
SearchState
    { leaves :: HashSet Int
leaves = HashSet Int
forall a. HashSet a
HSet.empty,
      searchNodes :: HashMap Int SearchNode
searchNodes =
        [(Int, SearchNode)] -> HashMap Int SearchNode
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HMap.fromList
          [ ( 0,
              Int
-> Int
-> String
-> HashSet String
-> HashMap String Int
-> [AnyComorphism]
-> String
-> Int
-> SearchNode
SearchNode
                0
                (-1)
                (lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid)
                HashSet String
forall a. HashSet a
HSet.empty
                HashMap String Int
forall k v. HashMap k v
HMap.empty
                [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 (InclComorphism lid sublogics -> AnyComorphism)
-> InclComorphism lid sublogics -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ 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 sublogics
sub]
                []
                0
            )
          ],
      distance :: HashMap Int Int
distance = [(Int, Int)] -> HashMap Int Int
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HMap.fromList [(0, 0)],
      pQueue :: MinPrioHeap Int Int
pQueue = [(Int, Int)] -> MinPrioHeap Int Int
forall pol item. HeapItem pol item => [item] -> Heap pol item
Heap.fromList [(0, 0)],
      logicToComorphisms :: HashMap String [String]
logicToComorphisms = LogicGraph -> HashMap String [String]
mapLogicsToComorphisms LogicGraph
lg,
      nextNodeId :: Int
nextNodeId = 1
    }

findComorphismCompositions :: LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismCompositions :: LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismCompositions lg :: LogicGraph
lg gsubl :: G_sublogics
gsubl =
  LogicGraph -> SearchState -> [AnyComorphism]
processSearchState LogicGraph
lg (LogicGraph -> G_sublogics -> SearchState
initState LogicGraph
lg G_sublogics
gsubl)

processSearchState :: LogicGraph -> SearchState -> [AnyComorphism]
processSearchState :: LogicGraph -> SearchState -> [AnyComorphism]
processSearchState lg :: LogicGraph
lg state :: SearchState
state@(SearchState ns :: HashMap Int SearchNode
ns ls :: HashSet Int
ls _ pq :: MinPrioHeap Int Int
pq _ _) = case MinPrioHeap Int Int -> Maybe ((Int, Int), MinPrioHeap Int Int)
forall pol item.
HeapItem pol item =>
Heap pol item -> Maybe (item, Heap pol item)
Heap.view MinPrioHeap Int Int
pq of
  Nothing -> HashMap Int SearchNode -> HashSet Int -> [AnyComorphism]
getComorphismCompositions HashMap Int SearchNode
ns HashSet Int
ls
  Just ((dist :: Int
dist, nId :: Int
nId), pq' :: MinPrioHeap Int Int
pq') ->
    let curNode :: SearchNode
curNode =
          SearchNode -> Maybe SearchNode -> SearchNode
forall a. a -> Maybe a -> a
fromMaybe
            ( String -> SearchNode
forall a. HasCallStack => String -> a
error (String -> SearchNode) -> String -> SearchNode
forall a b. (a -> b) -> a -> b
$
                String -> Int -> String
forall r. PrintfType r => String -> r
printf "processSearchState, incorrect nId=%d" Int
nId
            )
            (Maybe SearchNode -> SearchNode) -> Maybe SearchNode -> SearchNode
forall a b. (a -> b) -> a -> b
$ Int -> HashMap Int SearchNode -> Maybe SearchNode
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup Int
nId HashMap Int SearchNode
ns
        -- remove parent node from global map of nodes
        -- as we don't need it there anymore so GC can utilize
        -- it if required
        ns' :: HashMap Int SearchNode
ns' = Int -> HashMap Int SearchNode -> HashMap Int SearchNode
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
HMap.delete (SearchNode -> Int
parentId SearchNode
curNode) HashMap Int SearchNode
ns
        -- remove parent node from set of leaves and put current node there
        ls' :: HashSet Int
ls' = Int -> HashSet Int -> HashSet Int
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HSet.insert Int
nId (HashSet Int -> HashSet Int) -> HashSet Int -> HashSet Int
forall a b. (a -> b) -> a -> b
$ Int -> HashSet Int -> HashSet Int
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HSet.delete (SearchNode -> Int
parentId SearchNode
curNode) HashSet Int
ls
     in LogicGraph -> SearchState -> [AnyComorphism]
processSearchState LogicGraph
lg (SearchState -> [AnyComorphism]) -> SearchState -> [AnyComorphism]
forall a b. (a -> b) -> a -> b
$
          LogicGraph -> Int -> Int -> SearchState -> SearchState
processNeighbours
            LogicGraph
lg
            Int
nId
            Int
dist
            ( SearchState
state
                { searchNodes :: HashMap Int SearchNode
searchNodes = HashMap Int SearchNode
ns',
                  leaves :: HashSet Int
leaves = HashSet Int
ls',
                  pQueue :: MinPrioHeap Int Int
pQueue = MinPrioHeap Int Int
pq'
                }
            )

getComorphismCompositions ::
  HMap.HashMap Int SearchNode -> -- nodes of search graph
  HSet.HashSet Int -> -- leaves in this graph
  [AnyComorphism]
getComorphismCompositions :: HashMap Int SearchNode -> HashSet Int -> [AnyComorphism]
getComorphismCompositions sNodes :: HashMap Int SearchNode
sNodes lvs :: HashSet Int
lvs =
  let res :: [AnyComorphism]
res =
        [[AnyComorphism]] -> [AnyComorphism]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[AnyComorphism]] -> [AnyComorphism])
-> [[AnyComorphism]] -> [AnyComorphism]
forall a b. (a -> b) -> a -> b
$
          (Int -> [AnyComorphism]) -> [Int] -> [[AnyComorphism]]
forall a b. (a -> b) -> [a] -> [b]
map
            ( \i :: Int
i ->
                let leaf :: Maybe SearchNode
leaf = Int -> HashMap Int SearchNode -> Maybe SearchNode
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup Int
i HashMap Int SearchNode
sNodes
                 in [AnyComorphism] -> [AnyComorphism]
forall a. [a] -> [a]
reverse ([AnyComorphism] -> [AnyComorphism])
-> [AnyComorphism] -> [AnyComorphism]
forall a b. (a -> b) -> a -> b
$
                      SearchNode -> [AnyComorphism]
cCompositions (SearchNode -> [AnyComorphism]) -> SearchNode -> [AnyComorphism]
forall a b. (a -> b) -> a -> b
$
                        SearchNode -> Maybe SearchNode -> SearchNode
forall a. a -> Maybe a -> a
fromMaybe
                          ( String -> SearchNode
forall a. HasCallStack => String -> a
error (String -> SearchNode) -> String -> SearchNode
forall a b. (a -> b) -> a -> b
$
                              String -> Int -> String
forall r. PrintfType r => String -> r
printf "getComorphismComositions, incorrect i=%d key for HashMap" Int
i
                          )
                          (Maybe SearchNode -> SearchNode) -> Maybe SearchNode -> SearchNode
forall a b. (a -> b) -> a -> b
$ Maybe SearchNode
leaf
            )
            ([Int] -> [[AnyComorphism]]) -> [Int] -> [[AnyComorphism]]
forall a b. (a -> b) -> a -> b
$ HashSet Int -> [Int]
forall a. HashSet a -> [a]
HSet.toList (HashSet Int -> [Int]) -> HashSet Int -> [Int]
forall a b. (a -> b) -> a -> b
$ HashSet Int
lvs
   in [AnyComorphism]
res

getComorphism :: LogicGraph -> String -> AnyComorphism
getComorphism :: LogicGraph -> String -> AnyComorphism
getComorphism lg :: LogicGraph
lg cn :: String
cn =
  AnyComorphism -> Maybe AnyComorphism -> AnyComorphism
forall a. a -> Maybe a -> a
fromMaybe (String -> AnyComorphism
forall a. HasCallStack => String -> a
error (String -> ShowS
forall r. PrintfType r => String -> r
printf "getComorphism, incorrect comorphismName=%s key for HashMap" String
cn)) (Maybe AnyComorphism -> AnyComorphism)
-> Maybe AnyComorphism -> AnyComorphism
forall a b. (a -> b) -> a -> b
$
    String -> Map String AnyComorphism -> Maybe AnyComorphism
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
cn (LogicGraph -> Map String AnyComorphism
comorphisms LogicGraph
lg)

getTargetLogicName :: AnyComorphism -> String
getTargetLogicName :: AnyComorphism -> String
getTargetLogicName (Comorphism cid :: cid
cid) = lid2 -> String
forall lid. Language lid => lid -> String
language_name (lid2 -> String) -> lid2 -> String
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

-- | given node in tree generate candidate nodes and put them in priority queue
processNeighbours :: LogicGraph -> Int -> Int -> SearchState -> SearchState
processNeighbours :: LogicGraph -> Int -> Int -> SearchState -> SearchState
processNeighbours lg :: LogicGraph
lg nId :: Int
nId dist :: Int
dist state :: SearchState
state@(SearchState ns :: HashMap Int SearchNode
ns _ ds :: HashMap Int Int
ds pq :: MinPrioHeap Int Int
pq ltcs :: HashMap String [String]
ltcs nni :: Int
nni) =
  let curNode :: SearchNode
curNode =
        SearchNode -> Maybe SearchNode -> SearchNode
forall a. a -> Maybe a -> a
fromMaybe (String -> SearchNode
forall a. HasCallStack => String -> a
error (String -> SearchNode) -> String -> SearchNode
forall a b. (a -> b) -> a -> b
$ String -> Int -> String
forall r. PrintfType r => String -> r
printf "processNeighbours, incorrect nId=%d key for HashMap" Int
nId) (Maybe SearchNode -> SearchNode) -> Maybe SearchNode -> SearchNode
forall a b. (a -> b) -> a -> b
$
          Int -> HashMap Int SearchNode -> Maybe SearchNode
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup Int
nId HashMap Int SearchNode
ns
      lName :: String
lName = SearchNode -> String
logicName SearchNode
curNode
      comCandidates :: [String]
comCandidates = [String] -> String -> HashMap String [String] -> [String]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
HMap.lookupDefault [] String
lName HashMap String [String]
ltcs
      comCandidates' :: [String]
comCandidates' = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (\name :: String
name -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> HashSet String -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HSet.member String
name (SearchNode -> HashSet String
usedComorphisms SearchNode
curNode)) [String]
comCandidates
      -- create SearchNodes when possible due to restrictions and add ids later
      -- this code can be expressed as map (create_SearchNode) $ filter (can_create_SearchNode?)
      -- but implemented this way without map-filter separation
      childrenNodes :: [SearchNode]
childrenNodes =
        [Maybe SearchNode] -> [SearchNode]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe SearchNode] -> [SearchNode])
-> [Maybe SearchNode] -> [SearchNode]
forall a b. (a -> b) -> a -> b
$
          (String -> Maybe SearchNode) -> [String] -> [Maybe SearchNode]
forall a b. (a -> b) -> [a] -> [b]
map
            ( \name :: String
name ->
                let c :: AnyComorphism
c = LogicGraph -> String -> AnyComorphism
getComorphism LogicGraph
lg String
name
                    targetLogicName :: String
targetLogicName = AnyComorphism -> String
getTargetLogicName AnyComorphism
c
                    tlu :: Int
tlu = Int -> String -> HashMap String Int -> Int
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
HMap.lookupDefault 0 String
targetLogicName (SearchNode -> HashMap String Int
timesLogicUsed SearchNode
curNode)
                    newComposition :: Maybe AnyComorphism
newComposition =
                      AnyComorphism -> AnyComorphism -> Maybe AnyComorphism
forall (m :: * -> *).
MonadFail m =>
AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism ([AnyComorphism] -> AnyComorphism
forall a. [a] -> a
head ([AnyComorphism] -> AnyComorphism)
-> [AnyComorphism] -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ SearchNode -> [AnyComorphism]
cCompositions SearchNode
curNode) AnyComorphism
c
                    cw :: Int
cw = Int -> String -> HashMap String Int -> Int
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
HMap.lookupDefault (Int
maxWeight Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) String
name HashMap String Int
comorphismWeight
                 in if (Maybe AnyComorphism -> Bool
forall a. Maybe a -> Bool
isJust Maybe AnyComorphism
newComposition Bool -> Bool -> Bool
&& Int
tlu Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
times_logic_in_branch Bool -> Bool -> Bool
&& Int
cw Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
dist Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
weight_limit)
                      then
                        SearchNode -> Maybe SearchNode
forall a. a -> Maybe a
Just (SearchNode -> Maybe SearchNode) -> SearchNode -> Maybe SearchNode
forall a b. (a -> b) -> a -> b
$
                          SearchNode :: Int
-> Int
-> String
-> HashSet String
-> HashMap String Int
-> [AnyComorphism]
-> String
-> Int
-> SearchNode
SearchNode
                            { nodeId :: Int
nodeId = -1, -- dummy value for now, changed later in processNeighbours
                              parentId :: Int
parentId = Int
nId,
                              logicName :: String
logicName = String
targetLogicName,
                              usedComorphisms :: HashSet String
usedComorphisms = String -> HashSet String -> HashSet String
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HSet.insert String
name (SearchNode -> HashSet String
usedComorphisms SearchNode
curNode),
                              timesLogicUsed :: HashMap String Int
timesLogicUsed = String -> Int -> HashMap String Int -> HashMap String Int
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HMap.insert String
targetLogicName (Int
tlu Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (SearchNode -> HashMap String Int
timesLogicUsed SearchNode
curNode),
                              cCompositions :: [AnyComorphism]
cCompositions = (Maybe AnyComorphism -> AnyComorphism
forall a. HasCallStack => Maybe a -> a
fromJust Maybe AnyComorphism
newComposition) AnyComorphism -> [AnyComorphism] -> [AnyComorphism]
forall a. a -> [a] -> [a]
: (SearchNode -> [AnyComorphism]
cCompositions SearchNode
curNode),
                              comName :: String
comName = String
name,
                              comWeight :: Int
comWeight = Int
cw
                            }
                      else Maybe SearchNode
forall a. Maybe a
Nothing
            )
            [String]
comCandidates'

      -- add ids to SearchNodes
      (childrenNodes' :: [SearchNode]
childrenNodes', next_nni :: Int
next_nni) = (([SearchNode], Int) -> SearchNode -> ([SearchNode], Int))
-> ([SearchNode], Int) -> [SearchNode] -> ([SearchNode], Int)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\(acc :: [SearchNode]
acc, i :: Int
i) sn :: SearchNode
sn -> (SearchNode
sn{ nodeId :: Int
nodeId = Int
i } SearchNode -> [SearchNode] -> [SearchNode]
forall a. a -> [a] -> [a]
: [SearchNode]
acc, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) ([], Int
nni) [SearchNode]
childrenNodes

      -- update map of nodes
      ns' :: HashMap Int SearchNode
ns' = (HashMap Int SearchNode -> SearchNode -> HashMap Int SearchNode)
-> HashMap Int SearchNode -> [SearchNode] -> HashMap Int SearchNode
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\_ns :: HashMap Int SearchNode
_ns sn :: SearchNode
sn -> Int
-> SearchNode -> HashMap Int SearchNode -> HashMap Int SearchNode
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HMap.insert (SearchNode -> Int
nodeId SearchNode
sn) SearchNode
sn HashMap Int SearchNode
_ns) HashMap Int SearchNode
ns [SearchNode]
childrenNodes'
      -- update distances in SearchState
      ds' :: HashMap Int Int
ds' = (HashMap Int Int -> SearchNode -> HashMap Int Int)
-> HashMap Int Int -> [SearchNode] -> HashMap Int Int
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\_ds :: HashMap Int Int
_ds sn :: SearchNode
sn -> Int -> Int -> HashMap Int Int -> HashMap Int Int
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HMap.insert (SearchNode -> Int
nodeId SearchNode
sn) (Int
dist Int -> Int -> Int
forall a. Num a => a -> a -> a
+ SearchNode -> Int
comWeight SearchNode
sn) HashMap Int Int
_ds) HashMap Int Int
ds [SearchNode]
childrenNodes'
      -- update priority queue
      pq' :: HeapT (Prio FstMinPolicy (Int, Int)) Int
pq' = (HeapT (Prio FstMinPolicy (Int, Int)) Int
 -> SearchNode -> HeapT (Prio FstMinPolicy (Int, Int)) Int)
-> HeapT (Prio FstMinPolicy (Int, Int)) Int
-> [SearchNode]
-> HeapT (Prio FstMinPolicy (Int, Int)) Int
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\_pq :: HeapT (Prio FstMinPolicy (Int, Int)) Int
_pq sn :: SearchNode
sn -> (Int, Int) -> MinPrioHeap Int Int -> MinPrioHeap Int Int
forall pol item.
HeapItem pol item =>
item -> Heap pol item -> Heap pol item
Heap.insert (Int
dist Int -> Int -> Int
forall a. Num a => a -> a -> a
+ SearchNode -> Int
comWeight SearchNode
sn, SearchNode -> Int
nodeId SearchNode
sn) HeapT (Prio FstMinPolicy (Int, Int)) Int
MinPrioHeap Int Int
_pq) HeapT (Prio FstMinPolicy (Int, Int)) Int
MinPrioHeap Int Int
pq [SearchNode]
childrenNodes'
   in SearchState
state {searchNodes :: HashMap Int SearchNode
searchNodes = HashMap Int SearchNode
ns', distance :: HashMap Int Int
distance = HashMap Int Int
ds', pQueue :: MinPrioHeap Int Int
pQueue = HeapT (Prio FstMinPolicy (Int, Int)) Int
MinPrioHeap Int Int
pq', nextNodeId :: Int
nextNodeId = Int
next_nni}

mapLogicsToComorphisms :: LogicGraph -> HMap.HashMap String [String]
mapLogicsToComorphisms :: LogicGraph -> HashMap String [String]
mapLogicsToComorphisms lg :: LogicGraph
lg =
  ((String, AnyComorphism)
 -> HashMap String [String] -> HashMap String [String])
-> HashMap String [String]
-> [(String, AnyComorphism)]
-> HashMap String [String]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
    ( \(cName :: String
cName, Comorphism cId :: cid
cId) acc :: HashMap String [String]
acc ->
        let sourceLogicName :: String
sourceLogicName = lid1 -> String
forall lid. Language lid => lid -> String
language_name (lid1 -> String) -> lid1 -> String
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
            l :: [String]
l = [String] -> String -> HashMap String [String] -> [String]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
HMap.lookupDefault [] String
sourceLogicName HashMap String [String]
acc
         in String
-> [String] -> HashMap String [String] -> HashMap String [String]
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HMap.insert String
sourceLogicName (String
cName String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
l) HashMap String [String]
acc
    )
    HashMap String [String]
forall k v. HashMap k v
HMap.empty
    ([(String, AnyComorphism)] -> HashMap String [String])
-> [(String, AnyComorphism)] -> HashMap String [String]
forall a b. (a -> b) -> a -> b
$ Map String AnyComorphism -> [(String, AnyComorphism)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map String AnyComorphism -> [(String, AnyComorphism)])
-> Map String AnyComorphism -> [(String, AnyComorphism)]
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyComorphism
comorphisms LogicGraph
lg

-- | assign weights to comorphisms

maxWeight :: Int
maxWeight :: Int
maxWeight = 5

comorphismWeight :: HMap.HashMap String Int
comorphismWeight :: HashMap String Int
comorphismWeight =
  [(String, Int)] -> HashMap String Int
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HMap.fromList
    [ ("CASL2CoCASL", 5),
      ("CASL2CspCASL", 5),
      ("CASL2ExtModal", 5),
      ("CASL2HasCASL", 5),
      ("CASL2Hybrid", 5),
      ("CASL2Modal", 5),
      ("CASL2VSE", 5),
      ("CASL2VSEImport", 5),
      ("CASL2VSERefine", 5),
      ("HasCASL2IsabelleDeprecated", 5),
      ("OWL22NeSyPatterns", 5),
      ("CASL_DL2CASL", 4),
      ("CASL2Propositional", 4),
      ("CASL2OWL", 4),
      ("OWL22CommonLogic", 4),
      ("Propositional2CommonLogic", 4),
      ("Propositional2OWL2", 4),
      ("Propositional2QBF", 4),
      ("SoftFOL2CommonLogic", 4),
      ("THFP_P2HasCASL", 3),
      ("CspCASL2Modal", 3),
      ("OWL22CASL", 2),
      ("Propositional2CASL", 2),
      ("CoCASL2Isabelle", 2),
      ("CommonLogic2Isabelle", 2),
      ("CASL2Isabelle", 2),
      ("CommonLogicModuleElimination", 2),
      ("CspCASL2CspCASL_Failure", 2),
      ("CspCASL2CspCASL_Trace", 2),
      ("HasCASL2IsabelleOption", 2),
      ("THFP2THF0", 2),
      ("THFP_P2THFP", 2),
      ("Adl2CASL", 1),
      ("CASL2NNF", 1),
      ("CASL2PCFOL", 1),
      ("CASL2PCFOLTopSort", 1),
      ("CASL2Prenex", 1),
      ("CASL2Skolem", 1),
      ("CASL2SoftFOL", 1),
      ("CASL2SoftFOLInduction", 1),
      ("CASL2SoftFOLInduction2", 1),
      ("CASL2SubCFOL", 1),
      ("CASL2SubCFOLNoMembershipOrCast", 1),
      ("CASL2SubCFOLSubsortBottoms", 1),
      ("CASL2TPTP_FOF", 1),
      ("CLFol2CFOL", 1),
      ("CLFull2CFOL", 1),
      ("CLImp2CFOL", 1),
      ("CLSeq2CFOL", 1),
      ("CoCASL2CoPCFOL", 1),
      ("CoCASL2CoSubCFOL", 1),
      ("CSMOF2CASL", 1),
      ("DFOL2CASL", 1),
      ("DMU2OWL2", 1),
      ("ExtModal2CASL", 1),
      ("ExtModal2ExtModalNoSubsorts", 1),
      ("ExtModal2ExtModalTotal", 1),
      ("ExtModal2HasCASL", 1),
      ("ExtModal2OWL", 1),
      ("ExtModal2OWL", 1),
      ("HasCASL2HasCASLPrograms", 1),
      ("HasCASL2THFP_P", 1),
      ("HolLight2Isabelle", 1),
      ("Hybrid2CASL", 1),
      ("Maude2CASL", 1),
      ("Modal2CASL", 1),
      ("MonadicTranslation", 1),
      ("NormalisingTranslation", 1),
      ("QBF2Propositional", 1),
      ("QVTR2CASL", 1),
      ("RelScheme2CASL", 1)
    ]