{- |
Module      :  ./Comorphisms/HetLogicGraph.hs
Description :  Compute graph with logics and interesting sublogics
Copyright   :  (c) Klaus Luettich and Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  unstable
Portability :  non-portable

Assembles the computation of or the pre-computed het Sublogic Graph.
-}

module Comorphisms.HetLogicGraph
  ( HetSublogicGraph (..)
  , hetSublogicGraph
  , hsg_union
  ) where

import Comorphisms.LogicGraph

import qualified Common.Lib.Rel as Rel
import Common.Utils (keepMins)

import Logic.Logic
import Logic.Prover
import Logic.Comorphism
import Logic.Grothendieck
import Logic.Coerce

import Control.Monad
import qualified Control.Monad.Fail as Fail

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe
import Data.List

{- | Heterogenous Sublogic Graph
this graph only contains interesting Sublogics plus comorphisms relating
these sublogics; a comorphism might be mentioned multiple times -}
data HetSublogicGraph = HetSublogicGraph
    { HetSublogicGraph -> Map String G_sublogics
sublogicNodes :: Map.Map String G_sublogics
    , HetSublogicGraph -> Map (String, String) [AnyComorphism]
comorphismEdges :: Map.Map (String, String) [AnyComorphism]}

emptyHetSublogicGraph :: HetSublogicGraph
emptyHetSublogicGraph :: HetSublogicGraph
emptyHetSublogicGraph = Map String G_sublogics
-> Map (String, String) [AnyComorphism] -> HetSublogicGraph
HetSublogicGraph Map String G_sublogics
forall k a. Map k a
Map.empty Map (String, String) [AnyComorphism]
forall k a. Map k a
Map.empty

toTopSublogicAndProverSupported :: Map.Map String G_sublogics
  -> AnyLogic -> IO (Map.Map String G_sublogics)
toTopSublogicAndProverSupported :: Map String G_sublogics -> AnyLogic -> IO (Map String G_sublogics)
toTopSublogicAndProverSupported mp :: Map String G_sublogics
mp (Logic lid :: lid
lid) = do
  [ProverTemplate
   (Theory sign sentence proof_tree)
   sentence
   morphism
   sublogics
   proof_tree]
ps <- (ProverTemplate
   (Theory sign sentence proof_tree)
   sentence
   morphism
   sublogics
   proof_tree
 -> IO Bool)
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
-> IO
     [ProverTemplate
        (Theory sign sentence proof_tree)
        sentence
        morphism
        sublogics
        proof_tree]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Maybe String -> Bool) -> IO (Maybe String) -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing (IO (Maybe String) -> IO Bool)
-> (ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree
    -> IO (Maybe String))
-> ProverTemplate
     (Theory sign sentence proof_tree)
     sentence
     morphism
     sublogics
     proof_tree
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProverTemplate
  (Theory sign sentence proof_tree)
  sentence
  morphism
  sublogics
  proof_tree
-> IO (Maybe String)
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> IO (Maybe String)
proverUsable) ([ProverTemplate
    (Theory sign sentence proof_tree)
    sentence
    morphism
    sublogics
    proof_tree]
 -> IO
      [ProverTemplate
         (Theory sign sentence proof_tree)
         sentence
         morphism
         sublogics
         proof_tree])
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
-> IO
     [ProverTemplate
        (Theory sign sentence proof_tree)
        sentence
        morphism
        sublogics
        proof_tree]
forall a b. (a -> b) -> a -> b
$ lid
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
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 -> [Prover sign sentence morphism sublogics proof_tree]
provers lid
lid
  [ConsChecker sign sentence sublogics morphism proof_tree]
cs <- (ConsChecker sign sentence sublogics morphism proof_tree
 -> IO Bool)
-> [ConsChecker sign sentence sublogics morphism proof_tree]
-> IO [ConsChecker sign sentence sublogics morphism proof_tree]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Maybe String -> Bool) -> IO (Maybe String) -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing (IO (Maybe String) -> IO Bool)
-> (ConsChecker sign sentence sublogics morphism proof_tree
    -> IO (Maybe String))
-> ConsChecker sign sentence sublogics morphism proof_tree
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConsChecker sign sentence sublogics morphism proof_tree
-> IO (Maybe String)
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree
-> IO (Maybe String)
ccUsable) ([ConsChecker sign sentence sublogics morphism proof_tree]
 -> IO [ConsChecker sign sentence sublogics morphism proof_tree])
-> [ConsChecker sign sentence sublogics morphism proof_tree]
-> IO [ConsChecker sign sentence sublogics morphism proof_tree]
forall a b. (a -> b) -> a -> b
$ lid -> [ConsChecker sign sentence sublogics morphism proof_tree]
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 -> [ConsChecker sign sentence sublogics morphism proof_tree]
cons_checkers lid
lid
  let toGSLPair :: sublogics -> (String, G_sublogics)
toGSLPair sl :: sublogics
sl = let gsl :: G_sublogics
gsl = 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
lid sublogics
sl in (G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
gsl, G_sublogics
gsl)
      top_gsl :: (String, G_sublogics)
top_gsl = sublogics -> (String, G_sublogics)
forall 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 =>
sublogics -> (String, G_sublogics)
toGSLPair (sublogics -> (String, G_sublogics))
-> sublogics -> (String, G_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
      prv_sls :: [sublogics]
prv_sls = (ProverTemplate
   (Theory sign sentence proof_tree)
   sentence
   morphism
   sublogics
   proof_tree
 -> sublogics)
-> [ProverTemplate
      (Theory sign sentence proof_tree)
      sentence
      morphism
      sublogics
      proof_tree]
-> [sublogics]
forall a b. (a -> b) -> [a] -> [b]
map ProverTemplate
  (Theory sign sentence proof_tree)
  sentence
  morphism
  sublogics
  proof_tree
-> sublogics
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> sublogics
proverSublogic [ProverTemplate
   (Theory sign sentence proof_tree)
   sentence
   morphism
   sublogics
   proof_tree]
ps [sublogics] -> [sublogics] -> [sublogics]
forall a. [a] -> [a] -> [a]
++ (ConsChecker sign sentence sublogics morphism proof_tree
 -> sublogics)
-> [ConsChecker sign sentence sublogics morphism proof_tree]
-> [sublogics]
forall a b. (a -> b) -> [a] -> [b]
map ConsChecker sign sentence sublogics morphism proof_tree
-> sublogics
forall sign sentence sublogics morphism proof_tree.
ConsChecker sign sentence sublogics morphism proof_tree
-> sublogics
ccSublogic [ConsChecker sign sentence sublogics morphism proof_tree]
cs
  Map String G_sublogics -> IO (Map String G_sublogics)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map String G_sublogics -> IO (Map String G_sublogics))
-> ([(String, G_sublogics)] -> Map String G_sublogics)
-> [(String, G_sublogics)]
-> IO (Map String G_sublogics)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String G_sublogics
-> Map String G_sublogics -> Map String G_sublogics
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map String G_sublogics
mp (Map String G_sublogics -> Map String G_sublogics)
-> ([(String, G_sublogics)] -> Map String G_sublogics)
-> [(String, G_sublogics)]
-> Map String G_sublogics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, G_sublogics)] -> Map String G_sublogics
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, G_sublogics)] -> IO (Map String G_sublogics))
-> [(String, G_sublogics)] -> IO (Map String G_sublogics)
forall a b. (a -> b) -> a -> b
$ (String, G_sublogics)
top_gsl (String, G_sublogics)
-> [(String, G_sublogics)] -> [(String, G_sublogics)]
forall a. a -> [a] -> [a]
: (sublogics -> (String, G_sublogics))
-> [sublogics] -> [(String, G_sublogics)]
forall a b. (a -> b) -> [a] -> [b]
map sublogics -> (String, G_sublogics)
forall 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 =>
sublogics -> (String, G_sublogics)
toGSLPair [sublogics]
prv_sls

{- |
   initial version of a logic graph based on ticket #336
-}
hetSublogicGraph :: IO HetSublogicGraph
hetSublogicGraph :: IO HetSublogicGraph
hetSublogicGraph = do
  let insP :: (String, a) -> Map String a -> Map String a
insP = (String -> a -> Map String a -> Map String a)
-> (String, a) -> Map String a -> Map String a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> a -> Map String a -> Map String a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert
      toGsl :: Logic
                     lid
                     sublogics
                     basic_spec
                     sentence
                     symb_items
                     symb_map_items
                     sign
                     morphism
                     symbol
                     raw_symbol
                     proof_tree =>
                   lid -> sublogics -> G_sublogics
      toGsl :: lid -> sublogics -> G_sublogics
toGsl = 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
      toPair :: b -> (String, b)
toPair gsl :: b
gsl = (b -> String
forall a. Show a => a -> String
show b
gsl, b
gsl)
      srcSubl :: AnyComorphism -> Map String G_sublogics -> Map String G_sublogics
srcSubl acm :: AnyComorphism
acm nmp :: Map String G_sublogics
nmp = case AnyComorphism
acm of
             Comorphism cm :: cid
cm ->
              let srcSL :: sublogics1
srcSL = 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
cm
                  srcLid :: lid1
srcLid = 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
cm
                  srcGsl :: G_sublogics
srcGsl = lid1 -> sublogics1 -> 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
toGsl lid1
srcLid sublogics1
srcSL
              in (String, G_sublogics)
-> Map String G_sublogics -> Map String G_sublogics
forall a. (String, a) -> Map String a -> Map String a
insP (G_sublogics -> (String, G_sublogics)
forall b. Show b => b -> (String, b)
toPair G_sublogics
srcGsl) Map String G_sublogics
nmp
      initialInterestingSublogics :: (AnyComorphism -> Map String G_sublogics -> Map String G_sublogics)
-> IO (Map String G_sublogics)
initialInterestingSublogics sl :: AnyComorphism -> Map String G_sublogics -> Map String G_sublogics
sl = do
        Map String G_sublogics
m1 <- (Map String G_sublogics -> AnyLogic -> IO (Map String G_sublogics))
-> Map String G_sublogics
-> [AnyLogic]
-> IO (Map String G_sublogics)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map String G_sublogics -> AnyLogic -> IO (Map String G_sublogics)
toTopSublogicAndProverSupported Map String G_sublogics
forall k a. Map k a
Map.empty
          ([AnyLogic] -> IO (Map String G_sublogics))
-> (Map String AnyLogic -> [AnyLogic])
-> Map String AnyLogic
-> IO (Map String G_sublogics)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String AnyLogic -> [AnyLogic]
forall k a. Map k a -> [a]
Map.elems (Map String AnyLogic -> IO (Map String G_sublogics))
-> Map String AnyLogic -> IO (Map String G_sublogics)
forall a b. (a -> b) -> a -> b
$ LogicGraph -> Map String AnyLogic
logics LogicGraph
logicGraph
        Map String G_sublogics -> IO (Map String G_sublogics)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map String G_sublogics -> IO (Map String G_sublogics))
-> (Map String G_sublogics -> Map String G_sublogics)
-> Map String G_sublogics
-> IO (Map String G_sublogics)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String G_sublogics
-> Map String G_sublogics -> Map String G_sublogics
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map String G_sublogics
m1 (Map String G_sublogics -> IO (Map String G_sublogics))
-> Map String G_sublogics -> IO (Map String G_sublogics)
forall a b. (a -> b) -> a -> b
$ (AnyComorphism -> Map String G_sublogics -> Map String G_sublogics)
-> Map String G_sublogics
-> [AnyComorphism]
-> Map String G_sublogics
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr AnyComorphism -> Map String G_sublogics -> Map String G_sublogics
sl Map String G_sublogics
forall k a. Map k a
Map.empty [AnyComorphism]
comorphismList
  Map String G_sublogics
is <- (AnyComorphism -> Map String G_sublogics -> Map String G_sublogics)
-> IO (Map String G_sublogics)
initialInterestingSublogics AnyComorphism -> Map String G_sublogics -> Map String G_sublogics
srcSubl
  HetSublogicGraph -> IO HetSublogicGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (HetSublogicGraph -> IO HetSublogicGraph)
-> (HetSublogicGraph -> HetSublogicGraph)
-> HetSublogicGraph
-> IO HetSublogicGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetSublogicGraph -> HetSublogicGraph
removeDuplicateComorphisms
    (HetSublogicGraph -> HetSublogicGraph)
-> (HetSublogicGraph -> HetSublogicGraph)
-> HetSublogicGraph
-> HetSublogicGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetSublogicGraph -> HetSublogicGraph
addHomogeneousInclusions
    (HetSublogicGraph -> HetSublogicGraph)
-> (HetSublogicGraph -> HetSublogicGraph)
-> HetSublogicGraph
-> HetSublogicGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetSublogicGraph -> HetSublogicGraph
reduceToWellSupported
    (HetSublogicGraph -> HetSublogicGraph)
-> (HetSublogicGraph -> HetSublogicGraph)
-> HetSublogicGraph
-> HetSublogicGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetSublogicGraph -> HetSublogicGraph
removeLoops
    (HetSublogicGraph -> HetSublogicGraph)
-> (HetSublogicGraph -> HetSublogicGraph)
-> HetSublogicGraph
-> HetSublogicGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetSublogicGraph -> HetSublogicGraph
addComorphismEdges (HetSublogicGraph -> IO HetSublogicGraph)
-> HetSublogicGraph -> IO HetSublogicGraph
forall a b. (a -> b) -> a -> b
$
                   HetSublogicGraph
emptyHetSublogicGraph
                     { sublogicNodes :: Map String G_sublogics
sublogicNodes =
                           Map String G_sublogics
-> Map String G_sublogics -> Map String G_sublogics
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map String G_sublogics
is
                                     (Map String G_sublogics -> Map String G_sublogics
compute_preImageOfG_sublogics
                                             Map String G_sublogics
is)}


{- | adds the interesting comorphisms without adding new nodes;
considering as start and end points only existing nodes -}
addComorphismEdges :: HetSublogicGraph -> HetSublogicGraph
addComorphismEdges :: HetSublogicGraph -> HetSublogicGraph
addComorphismEdges hsg :: HetSublogicGraph
hsg = (G_sublogics -> HetSublogicGraph -> HetSublogicGraph)
-> HetSublogicGraph -> Map String G_sublogics -> HetSublogicGraph
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr G_sublogics -> HetSublogicGraph -> HetSublogicGraph
insComs HetSublogicGraph
hsg (Map String G_sublogics -> HetSublogicGraph)
-> Map String G_sublogics -> HetSublogicGraph
forall a b. (a -> b) -> a -> b
$ HetSublogicGraph -> Map String G_sublogics
sublogicNodes HetSublogicGraph
hsg
    where insComs :: G_sublogics -> HetSublogicGraph -> HetSublogicGraph
insComs gsl :: G_sublogics
gsl h :: HetSublogicGraph
h = (AnyComorphism -> HetSublogicGraph -> HetSublogicGraph)
-> HetSublogicGraph -> [AnyComorphism] -> HetSublogicGraph
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (G_sublogics
-> AnyComorphism -> HetSublogicGraph -> HetSublogicGraph
insCom G_sublogics
gsl) HetSublogicGraph
h [AnyComorphism]
comorphismList
          insCom :: G_sublogics
-> AnyComorphism -> HetSublogicGraph -> HetSublogicGraph
insCom gsl :: G_sublogics
gsl acm :: AnyComorphism
acm hsg' :: HetSublogicGraph
hsg' =
             case AnyComorphism
acm of
               Comorphism cm :: cid
cm ->
                case G_sublogics
gsl of
                  G_sublogics g_lid sl ->
                    if lid1 -> String
forall lid. Language lid => lid -> String
language_name (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cm) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= lid -> String
forall lid. Language lid => lid -> String
language_name lid
g_lid
                    then HetSublogicGraph
hsg'
                    else HetSublogicGraph
-> (sublogics2 -> HetSublogicGraph)
-> Maybe sublogics2
-> HetSublogicGraph
forall b a. b -> (a -> b) -> Maybe a -> b
maybe HetSublogicGraph
hsg' (HetSublogicGraph
-> G_sublogics -> AnyComorphism -> G_sublogics -> HetSublogicGraph
addEdge HetSublogicGraph
hsg' G_sublogics
gsl AnyComorphism
acm (G_sublogics -> HetSublogicGraph)
-> (sublogics2 -> G_sublogics) -> sublogics2 -> HetSublogicGraph
forall b c a. (b -> c) -> (a -> b) -> a -> 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
cm))
                               (lid -> lid1 -> String -> sublogics -> 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 lid
g_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
cm) "aCE" sublogics
sl
                                Maybe sublogics1
-> (sublogics1 -> Maybe sublogics2) -> Maybe sublogics2
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= cid -> sublogics1 -> Maybe sublogics2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sublogics1 -> Maybe sublogics2
mapSublogic cid
cm)
          addEdge :: HetSublogicGraph
-> G_sublogics -> AnyComorphism -> G_sublogics -> HetSublogicGraph
addEdge hsg' :: HetSublogicGraph
hsg' srcGsl :: G_sublogics
srcGsl acm :: AnyComorphism
acm trgGsl :: G_sublogics
trgGsl =
              (G_sublogics -> HetSublogicGraph -> HetSublogicGraph)
-> HetSublogicGraph -> [G_sublogics] -> HetSublogicGraph
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ x :: G_sublogics
x -> HetSublogicGraph -> Maybe HetSublogicGraph -> HetSublogicGraph
forall a. a -> Maybe a -> a
fromMaybe (String -> HetSublogicGraph
forall a. HasCallStack => String -> a
error ("insertion of " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                         AnyComorphism -> String
forall a. Show a => a -> String
show AnyComorphism
acm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " failed!")) (Maybe HetSublogicGraph -> HetSublogicGraph)
-> (HetSublogicGraph -> Maybe HetSublogicGraph)
-> HetSublogicGraph
-> HetSublogicGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                           G_sublogics
-> G_sublogics
-> AnyComorphism
-> HetSublogicGraph
-> Maybe HetSublogicGraph
forall (m :: * -> *).
MonadFail m =>
G_sublogics
-> G_sublogics
-> AnyComorphism
-> HetSublogicGraph
-> m HetSublogicGraph
insertEdge G_sublogics
srcGsl G_sublogics
x AnyComorphism
acm) HetSublogicGraph
hsg' ([G_sublogics] -> HetSublogicGraph)
-> [G_sublogics] -> HetSublogicGraph
forall a b. (a -> b) -> a -> b
$
                    G_sublogics -> [G_sublogics]
minimalSuperGsl G_sublogics
trgGsl
          minimalSuperGsl :: G_sublogics -> [G_sublogics]
minimalSuperGsl gsl :: G_sublogics
gsl =
              if String -> Map String G_sublogics -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member (G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
gsl) (Map String G_sublogics -> Bool) -> Map String G_sublogics -> Bool
forall a b. (a -> b) -> a -> b
$ HetSublogicGraph -> Map String G_sublogics
sublogicNodes HetSublogicGraph
hsg
              then [G_sublogics
gsl]
              else case (Set G_sublogics -> Bool) -> [Set G_sublogics] -> [Set G_sublogics]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: Set G_sublogics
x -> Set G_sublogics -> Int
forall a. Set a -> Int
Set.size
                                        ((G_sublogics -> Bool) -> Set G_sublogics -> Set G_sublogics
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (G_sublogics -> G_sublogics -> Bool
sameLogic G_sublogics
gsl) Set G_sublogics
x) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0) ([Set G_sublogics] -> [Set G_sublogics])
-> [Set G_sublogics] -> [Set G_sublogics]
forall a b. (a -> b) -> a -> b
$
                                 Map String G_sublogics -> [Set G_sublogics]
partSetSameLogic (Map String G_sublogics -> [Set G_sublogics])
-> Map String G_sublogics -> [Set G_sublogics]
forall a b. (a -> b) -> a -> b
$ HetSublogicGraph -> Map String G_sublogics
sublogicNodes HetSublogicGraph
hsg of
                              [] -> String -> [G_sublogics]
forall a. HasCallStack => String -> a
error "no appropiate superlogics"
                              [x :: Set G_sublogics
x] -> (G_sublogics -> G_sublogics -> Bool)
-> [G_sublogics] -> [G_sublogics]
forall a. (a -> a -> Bool) -> [a] -> [a]
keepMins G_sublogics -> G_sublogics -> Bool
isProperSublogic ([G_sublogics] -> [G_sublogics]) -> [G_sublogics] -> [G_sublogics]
forall a b. (a -> b) -> a -> b
$
                                     (G_sublogics -> Bool) -> [G_sublogics] -> [G_sublogics]
forall a. (a -> Bool) -> [a] -> [a]
filter (G_sublogics -> G_sublogics -> Bool
isProperSublogic G_sublogics
gsl) ([G_sublogics] -> [G_sublogics]) -> [G_sublogics] -> [G_sublogics]
forall a b. (a -> b) -> a -> b
$
                                     Set G_sublogics -> [G_sublogics]
forall a. Set a -> [a]
Set.toList Set G_sublogics
x
                              _ -> String -> [G_sublogics]
forall a. HasCallStack => String -> a
error "to many sets"

{- | compute all the pre-images of the list of G_sublogics
under all suitable comorphisms -}
compute_preImageOfG_sublogics :: Map.Map String G_sublogics
             -- ^ initial interesting sublogics
                              -> Map.Map String G_sublogics
compute_preImageOfG_sublogics :: Map String G_sublogics -> Map String G_sublogics
compute_preImageOfG_sublogics =
    Map String G_sublogics
-> Map String G_sublogics
-> Map String G_sublogics
-> Map String G_sublogics
iterComor Map String G_sublogics
forall k a. Map k a
Map.empty Map String G_sublogics
forall k a. Map k a
Map.empty
    where iterComor :: Map String G_sublogics
-> Map String G_sublogics
-> Map String G_sublogics
-> Map String G_sublogics
iterComor newSublMap :: Map String G_sublogics
newSublMap alreadyTried :: Map String G_sublogics
alreadyTried queue :: Map String G_sublogics
queue
           | Map String G_sublogics -> Bool
forall k a. Map k a -> Bool
Map.null Map String G_sublogics
queue = Map String G_sublogics
newSublMap
           | Bool
otherwise =
               case Map String G_sublogics
-> ((String, G_sublogics), Map String G_sublogics)
forall k a. Map k a -> ((k, a), Map k a)
Map.deleteFindMin Map String G_sublogics
queue of
                 ((k :: String
k, gsl :: G_sublogics
gsl), q' :: Map String G_sublogics
q') ->
                     case G_sublogics -> Map String G_sublogics -> Map String G_sublogics
calcPreImage G_sublogics
gsl Map String G_sublogics
forall k a. Map k a
Map.empty of
                       nMap :: Map String G_sublogics
nMap -> let alreadyTried' :: Map String G_sublogics
alreadyTried' =
                                       String
-> G_sublogics -> Map String G_sublogics -> Map String G_sublogics
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
k G_sublogics
gsl Map String G_sublogics
alreadyTried
                                   newInter :: Map String G_sublogics
newInter = (String -> Map String G_sublogics -> Map String G_sublogics)
-> Map String G_sublogics -> [String] -> Map String G_sublogics
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> Map String G_sublogics -> Map String G_sublogics
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Map String G_sublogics
nMap
                                                    (Map String G_sublogics -> [String]
forall k a. Map k a -> [k]
Map.keys Map String G_sublogics
alreadyTried')
                               in Map String G_sublogics
-> Map String G_sublogics
-> Map String G_sublogics
-> Map String G_sublogics
iterComor (Map String G_sublogics
-> Map String G_sublogics -> Map String G_sublogics
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map String G_sublogics
nMap Map String G_sublogics
newSublMap)
                                            Map String G_sublogics
alreadyTried'
                                            (Map String G_sublogics
-> Map String G_sublogics -> Map String G_sublogics
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map String G_sublogics
newInter Map String G_sublogics
q')
          calcPreImage :: G_sublogics -> Map String G_sublogics -> Map String G_sublogics
calcPreImage gsl :: G_sublogics
gsl sublMap :: Map String G_sublogics
sublMap =
              (Map String G_sublogics -> AnyComorphism -> Map String G_sublogics)
-> Map String G_sublogics
-> [AnyComorphism]
-> Map String G_sublogics
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (G_sublogics
-> Map String G_sublogics
-> AnyComorphism
-> Map String G_sublogics
preImageOf G_sublogics
gsl) Map String G_sublogics
sublMap [AnyComorphism]
comorphismList
          preImageOf :: G_sublogics
-> Map String G_sublogics
-> AnyComorphism
-> Map String G_sublogics
preImageOf gsl :: G_sublogics
gsl sublMap :: Map String G_sublogics
sublMap acm :: AnyComorphism
acm =
              case AnyComorphism
acm of
               Comorphism cm :: cid
cm ->
                 case G_sublogics
gsl of
                  G_sublogics g_lid _ ->
                     if lid1 -> String
forall lid. Language lid => lid -> String
language_name (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cm) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= lid -> String
forall lid. Language lid => lid -> String
language_name lid
g_lid
                        then Map String G_sublogics
sublMap
                        else (G_sublogics -> Map String G_sublogics -> Map String G_sublogics)
-> Map String G_sublogics
-> [G_sublogics]
-> Map String G_sublogics
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ preImg :: G_sublogics
preImg -> String
-> G_sublogics -> Map String G_sublogics -> Map String G_sublogics
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
preImg)
                                                           G_sublogics
preImg )
                                     Map String G_sublogics
sublMap (AnyComorphism -> G_sublogics -> [G_sublogics]
lookupPreImage AnyComorphism
acm G_sublogics
gsl)

removeDuplicateComorphisms :: HetSublogicGraph
                           -> HetSublogicGraph
removeDuplicateComorphisms :: HetSublogicGraph -> HetSublogicGraph
removeDuplicateComorphisms hsg :: HetSublogicGraph
hsg =
      HetSublogicGraph
hsg {comorphismEdges :: Map (String, String) [AnyComorphism]
comorphismEdges = ([AnyComorphism] -> Bool)
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Bool -> Bool
not (Bool -> Bool)
-> ([AnyComorphism] -> Bool) -> [AnyComorphism] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyComorphism] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (Map (String, String) [AnyComorphism]
 -> Map (String, String) [AnyComorphism])
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
forall a b. (a -> b) -> a -> b
$
                             ([AnyComorphism] -> [AnyComorphism])
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map [AnyComorphism] -> [AnyComorphism]
forall a. Eq a => [a] -> [a]
nub (Map (String, String) [AnyComorphism]
 -> Map (String, String) [AnyComorphism])
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
forall a b. (a -> b) -> a -> b
$ HetSublogicGraph -> Map (String, String) [AnyComorphism]
comorphismEdges HetSublogicGraph
hsg }

hsg_union :: HetSublogicGraph
          -> HetSublogicGraph
          -> HetSublogicGraph
hsg_union :: HetSublogicGraph -> HetSublogicGraph -> HetSublogicGraph
hsg_union hsg1 :: HetSublogicGraph
hsg1 hsg2 :: HetSublogicGraph
hsg2 =
    HetSublogicGraph :: Map String G_sublogics
-> Map (String, String) [AnyComorphism] -> HetSublogicGraph
HetSublogicGraph { sublogicNodes :: Map String G_sublogics
sublogicNodes = Map String G_sublogics
-> Map String G_sublogics -> Map String G_sublogics
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (HetSublogicGraph -> Map String G_sublogics
sublogicNodes HetSublogicGraph
hsg1)
                                                (HetSublogicGraph -> Map String G_sublogics
sublogicNodes HetSublogicGraph
hsg2)
                     , comorphismEdges :: Map (String, String) [AnyComorphism]
comorphismEdges =
                         ([AnyComorphism] -> [AnyComorphism] -> [AnyComorphism])
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith [AnyComorphism] -> [AnyComorphism] -> [AnyComorphism]
forall a. [a] -> [a] -> [a]
(++) (HetSublogicGraph -> Map (String, String) [AnyComorphism]
comorphismEdges HetSublogicGraph
hsg1)
                                            (HetSublogicGraph -> Map (String, String) [AnyComorphism]
comorphismEdges HetSublogicGraph
hsg2)
                     }

compute_mapSublogic_preImage :: AnyComorphism
                             -> (AnyComorphism,
                                 Map.Map G_sublogics (Set.Set G_sublogics))
compute_mapSublogic_preImage :: AnyComorphism -> (AnyComorphism, Map G_sublogics (Set G_sublogics))
compute_mapSublogic_preImage (Comorphism cid :: cid
cid) =
    case Map G_sublogics (Set G_sublogics)
-> Map G_sublogics (Set G_sublogics)
onlyMaximal_preImage (Map G_sublogics (Set G_sublogics)
 -> Map G_sublogics (Set G_sublogics))
-> Map G_sublogics (Set G_sublogics)
-> Map G_sublogics (Set G_sublogics)
forall a b. (a -> b) -> a -> b
$ cid -> Map G_sublogics (Set G_sublogics)
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 -> Map G_sublogics (Set G_sublogics)
mapSublogic_preImage cid
cid of
      preImageMap :: Map G_sublogics (Set G_sublogics)
preImageMap -> (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, Map G_sublogics (Set G_sublogics)
preImageMap)

comorPreImages :: [(AnyComorphism, Map.Map G_sublogics (Set.Set G_sublogics))]
comorPreImages :: [(AnyComorphism, Map G_sublogics (Set G_sublogics))]
comorPreImages = (AnyComorphism
 -> (AnyComorphism, Map G_sublogics (Set G_sublogics)))
-> [AnyComorphism]
-> [(AnyComorphism, Map G_sublogics (Set G_sublogics))]
forall a b. (a -> b) -> [a] -> [b]
map AnyComorphism -> (AnyComorphism, Map G_sublogics (Set G_sublogics))
compute_mapSublogic_preImage [AnyComorphism]
comorphismList

lookupPreImage :: AnyComorphism -> G_sublogics -> [G_sublogics]
lookupPreImage :: AnyComorphism -> G_sublogics -> [G_sublogics]
lookupPreImage acm :: AnyComorphism
acm gsl :: G_sublogics
gsl =
    case AnyComorphism
-> [(AnyComorphism, Map G_sublogics (Set G_sublogics))]
-> Maybe (Map G_sublogics (Set G_sublogics))
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup AnyComorphism
acm [(AnyComorphism, Map G_sublogics (Set G_sublogics))]
comorPreImages of
      Nothing -> String -> [G_sublogics]
forall a. HasCallStack => String -> a
error "unknown Comorphism"
      Just preImageMap :: Map G_sublogics (Set G_sublogics)
preImageMap -> [G_sublogics]
-> (Set G_sublogics -> [G_sublogics])
-> Maybe (Set G_sublogics)
-> [G_sublogics]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Set G_sublogics -> [G_sublogics]
forall a. Set a -> [a]
Set.toList (Maybe (Set G_sublogics) -> [G_sublogics])
-> Maybe (Set G_sublogics) -> [G_sublogics]
forall a b. (a -> b) -> a -> b
$ G_sublogics
-> Map G_sublogics (Set G_sublogics) -> Maybe (Set G_sublogics)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup G_sublogics
gsl Map G_sublogics (Set G_sublogics)
preImageMap

-- | pre-image of a function relative to the list values
preImage :: (Ord a, Ord b) => (a -> b) -> [a] -> Map.Map b (Set.Set a)
preImage :: (a -> b) -> [a] -> Map b (Set a)
preImage func :: a -> b
func = (Map b (Set a) -> a -> Map b (Set a))
-> Map b (Set a) -> [a] -> Map b (Set a)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map b (Set a) -> a -> Map b (Set a)
ins Map b (Set a)
forall k a. Map k a
Map.empty
    where ins :: Map b (Set a) -> a -> Map b (Set a)
ins mp :: Map b (Set a)
mp v :: a
v = (Set a -> Set a -> Set a)
-> b -> Set a -> Map b (Set a) -> Map b (Set a)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union (a -> b
func a
v) (a -> Set a
forall a. a -> Set a
Set.singleton a
v) Map b (Set a)
mp

preImageMaybe :: (Ord a, Ord b) =>
                 (a -> Maybe b) -> [a]
              -> Map.Map b (Set.Set a)
preImageMaybe :: (a -> Maybe b) -> [a] -> Map b (Set a)
preImageMaybe f :: a -> Maybe b
f vs :: [a]
vs =
    ((Maybe b -> b) -> Map (Maybe b) (Set a) -> Map b (Set a)
forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysMonotonic Maybe b -> b
forall a. HasCallStack => Maybe a -> a
fromJust (Map (Maybe b) (Set a) -> Map b (Set a))
-> (Map (Maybe b) (Set a) -> Map (Maybe b) (Set a))
-> Map (Maybe b) (Set a)
-> Map b (Set a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe b -> Map (Maybe b) (Set a) -> Map (Maybe b) (Set a)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Maybe b
forall a. Maybe a
Nothing) (Map (Maybe b) (Set a) -> Map b (Set a))
-> Map (Maybe b) (Set a) -> Map b (Set a)
forall a b. (a -> b) -> a -> b
$ (a -> Maybe b) -> [a] -> Map (Maybe b) (Set a)
forall a b. (Ord a, Ord b) => (a -> b) -> [a] -> Map b (Set a)
preImage a -> Maybe b
f [a]
vs

mapSublogic_preImage :: (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 -> Map.Map G_sublogics (Set.Set G_sublogics)
mapSublogic_preImage :: cid -> Map G_sublogics (Set G_sublogics)
mapSublogic_preImage cid :: cid
cid =
    (sublogics2
 -> Set sublogics1
 -> Map G_sublogics (Set G_sublogics)
 -> Map G_sublogics (Set G_sublogics))
-> Map G_sublogics (Set G_sublogics)
-> Map sublogics2 (Set sublogics1)
-> Map G_sublogics (Set G_sublogics)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey sublogics2
-> Set sublogics1
-> Map G_sublogics (Set G_sublogics)
-> Map G_sublogics (Set G_sublogics)
forall lid sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 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
  lid
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
sublogics2
-> Set sublogics1
-> Map G_sublogics (Set G_sublogics)
-> Map G_sublogics (Set G_sublogics)
toG_sublogics Map G_sublogics (Set G_sublogics)
forall k a. Map k a
Map.empty (Map sublogics2 (Set sublogics1)
 -> Map G_sublogics (Set G_sublogics))
-> Map sublogics2 (Set sublogics1)
-> Map G_sublogics (Set G_sublogics)
forall a b. (a -> b) -> a -> b
$
    (sublogics1 -> Maybe sublogics2)
-> [sublogics1] -> Map sublogics2 (Set sublogics1)
forall a b.
(Ord a, Ord b) =>
(a -> Maybe b) -> [a] -> Map b (Set a)
preImageMaybe (cid -> sublogics1 -> Maybe sublogics2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sublogics1 -> Maybe sublogics2
mapSublogic cid
cid) ([sublogics1] -> Map sublogics2 (Set sublogics1))
-> [sublogics1] -> Map sublogics2 (Set 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]
all_sublogics (lid1 -> [sublogics1]) -> lid1 -> [sublogics1]
forall a b. (a -> b) -> a -> b
$ cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid1
sourceLogic cid
cid
    where toG_sublogics :: sublogics2
-> Set sublogics1
-> Map G_sublogics (Set G_sublogics)
-> Map G_sublogics (Set G_sublogics)
toG_sublogics s2 :: sublogics2
s2 set_s1 :: Set sublogics1
set_s1 =
             G_sublogics
-> Set G_sublogics
-> Map G_sublogics (Set G_sublogics)
-> Map G_sublogics (Set G_sublogics)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (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
cid) sublogics2
s2)
                        ((sublogics1 -> G_sublogics) -> Set sublogics1 -> Set G_sublogics
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (lid -> sublogics1 -> 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 -> 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 cid
cid)) Set sublogics1
set_s1)

onlyMaximal_preImage :: Map.Map G_sublogics (Set.Set G_sublogics)
                     -> Map.Map G_sublogics (Set.Set G_sublogics)
onlyMaximal_preImage :: Map G_sublogics (Set G_sublogics)
-> Map G_sublogics (Set G_sublogics)
onlyMaximal_preImage = (Set G_sublogics -> Set G_sublogics)
-> Map G_sublogics (Set G_sublogics)
-> Map G_sublogics (Set G_sublogics)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Set G_sublogics -> Set G_sublogics
shrink
    where shrink :: Set G_sublogics -> Set G_sublogics
shrink st :: Set G_sublogics
st = [G_sublogics] -> Set G_sublogics
forall a. Ord a => [a] -> Set a
Set.fromList ([G_sublogics] -> Set G_sublogics)
-> [G_sublogics] -> Set G_sublogics
forall a b. (a -> b) -> a -> b
$ [G_sublogics] -> [G_sublogics] -> [G_sublogics]
shrink' [] ([G_sublogics] -> [G_sublogics]) -> [G_sublogics] -> [G_sublogics]
forall a b. (a -> b) -> a -> b
$ Set G_sublogics -> [G_sublogics]
forall a. Set a -> [a]
Set.elems Set G_sublogics
st
          shrink' :: [G_sublogics] -> [G_sublogics] -> [G_sublogics]
shrink' acc :: [G_sublogics]
acc [] = [G_sublogics]
acc
          shrink' acc :: [G_sublogics]
acc (x :: G_sublogics
x : xs :: [G_sublogics]
xs) = if (G_sublogics -> Bool) -> [G_sublogics] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (G_sublogics -> G_sublogics -> Bool
isProperSublogic G_sublogics
x) ([G_sublogics]
xs [G_sublogics] -> [G_sublogics] -> [G_sublogics]
forall a. [a] -> [a] -> [a]
++ [G_sublogics]
acc)
                               then [G_sublogics] -> [G_sublogics] -> [G_sublogics]
shrink' [G_sublogics]
acc [G_sublogics]
xs
                               else [G_sublogics] -> [G_sublogics] -> [G_sublogics]
shrink' (G_sublogics
x G_sublogics -> [G_sublogics] -> [G_sublogics]
forall a. a -> [a] -> [a]
: [G_sublogics]
acc) [G_sublogics]
xs

{- | inserts an edge into the graph without checking if the
sublogic pair is compatible with the comorphism;
but both nodes must be already present in the graph -}
insertEdge :: (Fail.MonadFail m) =>
              G_sublogics -> G_sublogics
           -> AnyComorphism -> HetSublogicGraph
           -> m HetSublogicGraph
insertEdge :: G_sublogics
-> G_sublogics
-> AnyComorphism
-> HetSublogicGraph
-> m HetSublogicGraph
insertEdge src :: G_sublogics
src trg :: G_sublogics
trg acm :: AnyComorphism
acm hsg :: HetSublogicGraph
hsg =
    if String -> Map String G_sublogics -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member (G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
src) (HetSublogicGraph -> Map String G_sublogics
sublogicNodes HetSublogicGraph
hsg) Bool -> Bool -> Bool
&&
       String -> Map String G_sublogics -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member (G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
src) (HetSublogicGraph -> Map String G_sublogics
sublogicNodes HetSublogicGraph
hsg)
    then HetSublogicGraph -> m HetSublogicGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (HetSublogicGraph -> m HetSublogicGraph)
-> HetSublogicGraph -> m HetSublogicGraph
forall a b. (a -> b) -> a -> b
$
         HetSublogicGraph
hsg { comorphismEdges :: Map (String, String) [AnyComorphism]
comorphismEdges = ([AnyComorphism] -> [AnyComorphism] -> [AnyComorphism])
-> (String, String)
-> [AnyComorphism]
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [AnyComorphism] -> [AnyComorphism] -> [AnyComorphism]
forall a. [a] -> [a] -> [a]
(++)
                                                (G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
src, G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
trg) [AnyComorphism
acm] (Map (String, String) [AnyComorphism]
 -> Map (String, String) [AnyComorphism])
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
forall a b. (a -> b) -> a -> b
$
                                                HetSublogicGraph -> Map (String, String) [AnyComorphism]
comorphismEdges HetSublogicGraph
hsg }
    else String -> m HetSublogicGraph
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Comorphisms.HetLogicGraph: insertEdge: both nodes need " String -> String -> String
forall a. [a] -> [a] -> [a]
++
               "to be present")

removeLoops :: HetSublogicGraph -> HetSublogicGraph
removeLoops :: HetSublogicGraph -> HetSublogicGraph
removeLoops hsg :: HetSublogicGraph
hsg = HetSublogicGraph
hsg { comorphismEdges :: Map (String, String) [AnyComorphism]
comorphismEdges =
                            ((String, String) -> [AnyComorphism] -> Bool)
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ (s :: String
s, t :: String
t) _ -> String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
t) (Map (String, String) [AnyComorphism]
 -> Map (String, String) [AnyComorphism])
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
forall a b. (a -> b) -> a -> b
$
                            HetSublogicGraph -> Map (String, String) [AnyComorphism]
comorphismEdges HetSublogicGraph
hsg}

reduceToWellSupported :: HetSublogicGraph -> HetSublogicGraph
reduceToWellSupported :: HetSublogicGraph -> HetSublogicGraph
reduceToWellSupported hsg :: HetSublogicGraph
hsg =
    HetSublogicGraph
hsg { sublogicNodes :: Map String G_sublogics
sublogicNodes = Map String G_sublogics
wellSupN
        , comorphismEdges :: Map (String, String) [AnyComorphism]
comorphismEdges = Map (String, String) [AnyComorphism]
wellSupE }
    where wellSupN :: Map String G_sublogics
wellSupN = (G_sublogics -> Bool)
-> Map String G_sublogics -> Map String G_sublogics
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter G_sublogics -> Bool
isWellSupN (Map String G_sublogics -> Map String G_sublogics)
-> Map String G_sublogics -> Map String G_sublogics
forall a b. (a -> b) -> a -> b
$ HetSublogicGraph -> Map String G_sublogics
sublogicNodes HetSublogicGraph
hsg
          wellSupE :: Map (String, String) [AnyComorphism]
wellSupE = ((String, String) -> [AnyComorphism] -> Bool)
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (String, String) -> [AnyComorphism] -> Bool
forall p. (String, String) -> p -> Bool
isWellSupE (Map (String, String) [AnyComorphism]
 -> Map (String, String) [AnyComorphism])
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
forall a b. (a -> b) -> a -> b
$ HetSublogicGraph -> Map (String, String) [AnyComorphism]
comorphismEdges HetSublogicGraph
hsg
          isWellSupN :: G_sublogics -> Bool
isWellSupN (G_sublogics lid :: lid
lid _) =
              lid -> 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 -> Bool
hasProver lid
lid Bool -> Bool -> Bool
|| (case lid -> Stability
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 -> Stability
stability lid
lid of
                                     Stable -> Bool
True
                                     Testing -> Bool
True
                                     _ -> Bool
False)
          isWellSupE :: (String, String) -> p -> Bool
isWellSupE (s :: String
s, t :: String
t) _ = String -> Map String G_sublogics -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member String
s Map String G_sublogics
wellSupN Bool -> Bool -> Bool
&& String -> Map String G_sublogics -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member String
t Map String G_sublogics
wellSupN
          hasProver :: lid -> Bool
hasProver lid :: lid
lid = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Prover sign sentence morphism sublogics proof_tree] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Prover sign sentence morphism sublogics proof_tree] -> Bool)
-> [Prover sign sentence morphism sublogics proof_tree] -> Bool
forall a b. (a -> b) -> a -> b
$ lid -> [Prover sign sentence morphism sublogics proof_tree]
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 -> [Prover sign sentence morphism sublogics proof_tree]
provers lid
lid

sameLogic :: G_sublogics -> G_sublogics -> Bool
sameLogic :: G_sublogics -> G_sublogics -> Bool
sameLogic (G_sublogics lid1 :: lid
lid1 _) (G_sublogics lid2 :: lid
lid2 _) =
    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

partSetSameLogic :: Map.Map String G_sublogics
                 -> [Set.Set G_sublogics]
partSetSameLogic :: Map String G_sublogics -> [Set G_sublogics]
partSetSameLogic = (G_sublogics -> G_sublogics -> Bool)
-> Set G_sublogics -> [Set G_sublogics]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [Set a]
Rel.partSet G_sublogics -> G_sublogics -> Bool
sameLogic (Set G_sublogics -> [Set G_sublogics])
-> (Map String G_sublogics -> Set G_sublogics)
-> Map String G_sublogics
-> [Set G_sublogics]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [G_sublogics] -> Set G_sublogics
forall a. Ord a => [a] -> Set a
Set.fromList ([G_sublogics] -> Set G_sublogics)
-> (Map String G_sublogics -> [G_sublogics])
-> Map String G_sublogics
-> Set G_sublogics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String G_sublogics -> [G_sublogics]
forall k a. Map k a -> [a]
Map.elems

addHomogeneousInclusions :: HetSublogicGraph -> HetSublogicGraph
addHomogeneousInclusions :: HetSublogicGraph -> HetSublogicGraph
addHomogeneousInclusions hsg :: HetSublogicGraph
hsg =
    HetSublogicGraph
hsg {comorphismEdges :: Map (String, String) [AnyComorphism]
comorphismEdges = ([AnyComorphism] -> [AnyComorphism] -> [AnyComorphism])
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith [AnyComorphism] -> [AnyComorphism] -> [AnyComorphism]
forall a. [a] -> [a] -> [a]
(++) Map (String, String) [AnyComorphism]
homogeneousIncls (Map (String, String) [AnyComorphism]
 -> Map (String, String) [AnyComorphism])
-> Map (String, String) [AnyComorphism]
-> Map (String, String) [AnyComorphism]
forall a b. (a -> b) -> a -> b
$
                                              HetSublogicGraph -> Map (String, String) [AnyComorphism]
comorphismEdges HetSublogicGraph
hsg}
    where homogeneousIncls :: Map (String, String) [AnyComorphism]
homogeneousIncls = ([AnyComorphism] -> [AnyComorphism] -> [AnyComorphism])
-> [Map (String, String) [AnyComorphism]]
-> Map (String, String) [AnyComorphism]
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith [AnyComorphism] -> [AnyComorphism] -> [AnyComorphism]
forall a. [a] -> [a] -> [a]
(++) ([Map (String, String) [AnyComorphism]]
 -> Map (String, String) [AnyComorphism])
-> [Map (String, String) [AnyComorphism]]
-> Map (String, String) [AnyComorphism]
forall a b. (a -> b) -> a -> b
$
                             (Set G_sublogics -> Map (String, String) [AnyComorphism])
-> [Set G_sublogics] -> [Map (String, String) [AnyComorphism]]
forall a b. (a -> b) -> [a] -> [b]
map Set G_sublogics -> Map (String, String) [AnyComorphism]
toMap ([Set G_sublogics] -> [Map (String, String) [AnyComorphism]])
-> [Set G_sublogics] -> [Map (String, String) [AnyComorphism]]
forall a b. (a -> b) -> a -> b
$ Map String G_sublogics -> [Set G_sublogics]
partSetSameLogic (Map String G_sublogics -> [Set G_sublogics])
-> Map String G_sublogics -> [Set G_sublogics]
forall a b. (a -> b) -> a -> b
$ HetSublogicGraph -> Map String G_sublogics
sublogicNodes HetSublogicGraph
hsg
          toMap :: Set G_sublogics -> Map (String, String) [AnyComorphism]
toMap s :: Set G_sublogics
s = [((String, String), [AnyComorphism])]
-> Map (String, String) [AnyComorphism]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((String, String), [AnyComorphism])]
 -> Map (String, String) [AnyComorphism])
-> [((String, String), [AnyComorphism])]
-> Map (String, String) [AnyComorphism]
forall a b. (a -> b) -> a -> b
$ ((G_sublogics, G_sublogics) -> ((String, String), [AnyComorphism]))
-> [(G_sublogics, G_sublogics)]
-> [((String, String), [AnyComorphism])]
forall a b. (a -> b) -> [a] -> [b]
map (G_sublogics, G_sublogics) -> ((String, String), [AnyComorphism])
toIncComor ([(G_sublogics, G_sublogics)]
 -> [((String, String), [AnyComorphism])])
-> [(G_sublogics, G_sublogics)]
-> [((String, String), [AnyComorphism])]
forall a b. (a -> b) -> a -> b
$
                    Rel G_sublogics -> [(G_sublogics, G_sublogics)]
forall a. Rel a -> [(a, a)]
Rel.toList (Rel G_sublogics -> [(G_sublogics, G_sublogics)])
-> Rel G_sublogics -> [(G_sublogics, G_sublogics)]
forall a b. (a -> b) -> a -> b
$ Rel G_sublogics -> Rel G_sublogics
forall a. Ord a => Rel a -> Rel a
Rel.intransKernel (Rel G_sublogics -> Rel G_sublogics)
-> Rel G_sublogics -> Rel G_sublogics
forall a b. (a -> b) -> a -> b
$ [(G_sublogics, G_sublogics)] -> Rel G_sublogics
forall a. Ord a => [(a, a)] -> Rel a
Rel.fromList
                    [ (G_sublogics
x, G_sublogics
y) | G_sublogics
x <- Set G_sublogics -> [G_sublogics]
forall a. Set a -> [a]
Set.toList Set G_sublogics
s
                            , G_sublogics
y <- Set G_sublogics -> [G_sublogics]
forall a. Set a -> [a]
Set.toList Set G_sublogics
s
                            , G_sublogics -> G_sublogics -> Bool
isProperSublogic G_sublogics
x G_sublogics
y ]
          toIncComor :: (G_sublogics, G_sublogics) -> ((String, String), [AnyComorphism])
toIncComor (x :: G_sublogics
x@(G_sublogics lid1 :: lid
lid1 sub1 :: sublogics
sub1)
                     , y :: G_sublogics
y@(G_sublogics lid2 sub2)) =
                 ( (G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
x, G_sublogics -> String
forall a. Show a => a -> String
show G_sublogics
y)
                 , [AnyComorphism
-> (InclComorphism lid sublogics -> AnyComorphism)
-> Maybe (InclComorphism lid sublogics)
-> AnyComorphism
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> AnyComorphism
forall a. HasCallStack => String -> a
error (String -> AnyComorphism) -> String -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ "addHomogeneousInclusions: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                   "should be an inclusion")
                         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 (Maybe (InclComorphism lid sublogics) -> AnyComorphism)
-> Maybe (InclComorphism lid sublogics) -> AnyComorphism
forall a b. (a -> b) -> a -> b
$
                          lid
-> sublogics -> sublogics -> Maybe (InclComorphism lid sublogics)
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree (m :: * -> *).
(Logic
   lid
   sublogics
   basic_spec
   sentence
   symb_items
   symb_map_items
   sign
   morphism
   symbol
   raw_symbol
   proof_tree,
 MonadFail m) =>
lid -> sublogics -> sublogics -> m (InclComorphism lid sublogics)
mkInclComorphism lid
lid1 sublogics
sub1 (sublogics -> Maybe (InclComorphism lid sublogics))
-> sublogics -> Maybe (InclComorphism lid sublogics)
forall a b. (a -> b) -> a -> b
$
                             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
lid2 lid
lid1 sublogics
sub2])