```{- |
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 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
(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
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,
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)
-> 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 :: * -> *).
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
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
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
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
(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,
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])
```