-- for looking up modifications
-- * \"Grothendieck\" versions of the various parts of type class Logic
-- | Grothendieck basic specifications
data G_basic_spec = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_basic_spec lid basic_spec
instance Show G_basic_spec where
show (G_basic_spec _ s) = show s
instance Pretty G_basic_spec where
pretty (G_basic_spec _ s) = pretty s
instance GetRange G_basic_spec
-- dummy instances for development graphs
instance Ord G_basic_spec where
instance Eq G_basic_spec where
-- | index for signatures
newtype SigId = SigId Int
deriving (Typeable, Show, Eq, Ord, Enum, ShATermConvertible)
{- | Grothendieck signatures with an lookup index. Zero indices
indicate unknown ones. It would be nice to have special (may be
negative) indices for empty signatures (one for every logic). -}
data G_sign = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree => G_sign
, gSign :: ExtSign sign symbol
, gSignSelfIdx :: SigId -- ^ index to lookup this 'G_sign' in sign map
a == b = compare a b == EQ
instance Ord G_sign where
compare (G_sign l1 sigma1 s1) (G_sign l2 sigma2 s2) =
if s1 > startSigId && s2 > startSigId && s1 == s2 then EQ else
case compare (Logic l1) $ Logic l2 of
EQ -> compare (coerceSign l1 l2 "Eq G_sign" sigma1) $ Just sigma2
-- | prefer a faster subsignature test if possible
isHomSubGsign :: G_sign -> G_sign -> Bool
isHomSubGsign (G_sign l1 sigma1 s1) (G_sign l2 sigma2 s2) =
(s1 > startSigId && s2 > startSigId && s1 == s2) ||
maybe False (ext_is_subsig l1 sigma1)
(coerceSign l2 l1 "isHomSubGsign" sigma2)
isSubGsign :: LogicGraph -> G_sign -> G_sign -> Bool
isSubGsign lg (G_sign lid1 (ExtSign sigma1 _) _)
(G_sign lid2 (ExtSign sigma2 _) _) =
do Comorphism cid <- resultToMaybe $
logicInclusion lg (Logic lid1) (Logic lid2)
sigma1' <- coercePlainSign lid1 (sourceLogic cid)
sigma2' <- coercePlainSign lid2 (targetLogic cid)
sigma1t <- resultToMaybe $ map_sign cid sigma1'
return $ is_subsig (targetLogic cid) (fst sigma1t) sigma2'
instance Show G_sign where
show (G_sign _ s _) = show s
instance Pretty G_sign where
pretty (G_sign _ (ExtSign s _) _) = pretty s
logicOfGsign :: G_sign -> AnyLogic
logicOfGsign (G_sign lid _ _) = Logic lid
symsOfGsign :: G_sign ->
Set.Set G_symbol
symsOfGsign (G_sign lid (ExtSign sgn _) _) =
Set.map (G_symbol lid)
-- | Grothendieck maps with symbol as keys
data G_symbolmap a = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
instance Show a => Show (G_symbolmap a) where
show (G_symbolmap _ sm) = show sm
instance (Typeable a, Ord a) => Eq (G_symbolmap a) where
a == b = compare a b == EQ
instance (Typeable a, Ord a) => Ord (G_symbolmap a) where
compare (G_symbolmap l1 sm1) (G_symbolmap l2 sm2) =
case compare (Logic l1) $ Logic l2 of
EQ -> compare (coerceSymbolmap l1 l2 sm1) sm2
-- | Grothendieck maps with symbol as values
data G_mapofsymbol a = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_mapofsymbol lid (
Map.Map a symbol)
instance Show a => Show (G_mapofsymbol a) where
show (G_mapofsymbol _ sm) = show sm
instance (Typeable a, Ord a) => Eq (G_mapofsymbol a) where
a == b = compare a b == EQ
instance (Typeable a, Ord a) => Ord (G_mapofsymbol a) where
compare (G_mapofsymbol l1 sm1) (G_mapofsymbol l2 sm2) =
case compare (Logic l1) $ Logic l2 of
EQ -> compare (coerceMapofsymbol l1 l2 sm1) sm2
-- | Grothendieck symbols
data G_symbol = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
instance GetRange G_symbol where
getRange (G_symbol _ s) = getRange s
rangeSpan (G_symbol _ s) = rangeSpan s
instance Show G_symbol where
show (G_symbol _ s) = show s
instance Pretty G_symbol where
pretty (G_symbol _ s) = pretty s
instance Eq G_symbol where
a == b = compare a b == EQ
instance Ord G_symbol where
compare (G_symbol l1 s1) (G_symbol l2 s2) =
case compare (Logic l1) $ Logic l2 of
EQ -> compare (coerceSymbol l1 l2 s1) s2
-- | Grothendieck symbol lists
data G_symb_items_list = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_symb_items_list lid [symb_items]
instance GetRange G_symb_items_list
instance Show G_symb_items_list where
show (G_symb_items_list _ l) = show l
instance Pretty G_symb_items_list where
pretty (G_symb_items_list _ l) = ppWithCommas l
instance Eq G_symb_items_list where
(G_symb_items_list i1 s1) == (G_symb_items_list i2 s2) =
coerceSymbItemsList i1 i2 "Eq G_symb_items_list" s1 == Just s2
-- | Grothendieck symbol maps
data G_symb_map_items_list = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_symb_map_items_list lid [symb_map_items]
instance GetRange G_symb_map_items_list
instance Show G_symb_map_items_list where
show (G_symb_map_items_list _ l) = show l
instance Pretty G_symb_map_items_list where
pretty (G_symb_map_items_list _ l) = ppWithCommas l
instance Eq G_symb_map_items_list where
(G_symb_map_items_list i1 s1) == (G_symb_map_items_list i2 s2) =
coerceSymbMapItemsList i1 i2 "Eq G_symb_map_items_list" s1 == Just s2
-- | Grothendieck sublogics
data G_sublogics = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_sublogics lid sublogics
instance Show G_sublogics where
show (G_sublogics lid sub) = language_name lid ++ case sublogicName sub of
instance Eq G_sublogics where
g1 == g2 = compare g1 g2 == EQ
instance Ord G_sublogics where
compare (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
case compare (Logic lid1) $ Logic lid2 of
EQ -> compare (forceCoerceSublogic lid1 lid2 l1) l2
isSublogic :: G_sublogics -> G_sublogics -> Bool
isSublogic (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
isSubElem (forceCoerceSublogic lid1 lid2 l1) l2
isProperSublogic :: G_sublogics -> G_sublogics -> Bool
isProperSublogic a b = isSublogic a b && a /= b
joinSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics
joinSublogics (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
case coerceSublogic lid1 lid2 "coerce Sublogic" l1 of
Just sl -> Just (G_sublogics lid2 (lub sl l2))
newtype MorId = MorId Int
deriving (Typeable, Show, Eq, Ord, Enum, ShATermConvertible)
{- | Homogeneous Grothendieck signature morphisms with indices. For
the domain index it would be nice it showed also the emptiness. -}
data G_morphism = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree => G_morphism
, gMorphismSelfIdx :: MorId -- ^ lookup index in morphism map
instance Show G_morphism where
show (G_morphism _ m _) = show m
instance Pretty G_morphism where
pretty (G_morphism _ m _) = pretty m
mkG_morphism :: forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree
=> lid -> morphism -> G_morphism
mkG_morphism l m = G_morphism l m startMorId
-- | check if sublogic fits for comorphism
lessSublogicComor :: G_sublogics -> AnyComorphism -> Bool
lessSublogicComor (G_sublogics lid1 sub1) (Comorphism cid) =
let lid2 = sourceLogic cid
in Logic lid2 == Logic lid1
&& isSubElem (forceCoerceSublogic lid1 lid2 sub1) (sourceSublogic cid)
type SublogicBasedTheories =
Map.Map IRI (LibName, String)
data LogicGraph = LogicGraph
{ logics ::
Map.Map String AnyLogic
, currentSyntax :: Maybe IRI
, currentSublogic :: Maybe G_sublogics
, currentTargetBase :: Maybe (LibName, String)
, sublogicBasedTheories ::
Map.Map AnyLogic SublogicBasedTheories
, comorphisms ::
Map.Map String AnyComorphism
, inclusions ::
Map.Map (String, String) AnyComorphism
, unions ::
Map.Map (String, String) (AnyComorphism, AnyComorphism)
, morphisms ::
Map.Map String AnyMorphism
, modifications ::
Map.Map String AnyModification
, squares ::
Map.Map (AnyComorphism, AnyComorphism) [Square]
, qTATranslations ::
Map.Map String AnyComorphism
emptyLogicGraph :: LogicGraph
emptyLogicGraph = LogicGraph
, currentSyntax = Nothing
, currentSublogic = Nothing
, currentTargetBase = Nothing
setCurLogicAux :: String -> LogicGraph -> LogicGraph
setCurLogicAux s lg = lg { currentLogic = s }
setCurLogic :: String -> LogicGraph -> LogicGraph
setCurLogic s lg = if s == currentLogic lg then
lg else setSyntaxAux Nothing $ setCurLogicAux s lg
setSyntaxAux :: Maybe IRI -> LogicGraph -> LogicGraph
setSyntaxAux s lg = lg { currentSyntax = s }
setSyntax :: Maybe IRI -> LogicGraph -> LogicGraph
setSyntax s lg = if isNothing s then lg else setSyntaxAux s lg
setCurSublogic :: Maybe G_sublogics -> LogicGraph -> LogicGraph
setCurSublogic s lg = lg { currentSublogic = s }
instance Pretty LogicGraph where
pretty lg = text ("current logic is: " ++ currentLogic lg)
$+$ sepByCommas (map text $
Map.keys $ logics lg)
$+$ text "comorphism inclusions:"
$+$ vcat (map pretty $
Map.elems $ inclusions lg)
$+$ text "all comorphisms:"
$+$ vcat (map pretty $
Map.elems $ comorphisms lg)
-- | find a logic in a logic graph
lookupLogic :: Monad m => String -> String -> LogicGraph -> m AnyLogic
lookupLogic error_prefix logname logicGraph =
Nothing -> fail $ error_prefix ++ "unknown logic: " ++ logname
lookupCurrentLogic :: Monad m => String -> LogicGraph -> m AnyLogic
lookupCurrentLogic msg lg = lookupLogic (msg ++ " ") (currentLogic lg) lg
lookupCurrentSyntax :: Monad m => String -> LogicGraph
-> m (AnyLogic, Maybe IRI)
lookupCurrentSyntax msg lg = do
l <- lookupLogic (msg ++ " ") (currentLogic lg) lg
return (l, currentSyntax lg)
logicUnion :: LogicGraph -> AnyLogic -> AnyLogic
-> Result (AnyComorphism, AnyComorphism)
logicUnion lg l1@(Logic lid1) l2@(Logic lid2) =
case logicInclusion lg l1 l2 of
Result _ (Just c) -> return (c, idComorphism l2)
_ -> case logicInclusion lg l2 l1 of
Result _ (Just c) -> return (idComorphism l1, c)
Nothing -> case
Map.lookup (ln2, ln1) (unions lg) of
Just (c2, c1) -> return (c1, c2)
Nothing -> fail $ "Union of logics " ++ ln1 ++
" and " ++ ln2 ++ " does not exist"
where ln1 = language_name lid1
-- | find a comorphism composition in a logic graph
lookupCompComorphism :: Monad m => [String] -> LogicGraph -> m AnyComorphism
lookupCompComorphism nameList logicGraph = do
cs <- mapM lookupN nameList
c : cs1 -> foldM compComorphism c cs1
_ -> fail "Illegal empty comorphism composition"
'i' : 'd' : '_' : logic -> do
let (mainLogic, subLogicD) = span (/= '.') logic
-- subLogicD will begin with a . which has to be removed
msublogic = if null subLogicD
else Just $ tail subLogicD
Logic lid <- maybe (fail ("Cannot find Logic " ++ mainLogic)) return
case maybe (Just $ top_sublogic lid) (parseSublogic lid) msublogic of
Nothing -> fail $ maybe "missing sublogic"
("unknown sublogic name " ++) msublogic
Just s -> return $ Comorphism $ mkIdComorphism lid s
_ -> maybe (fail ("Cannot find logic comorphism " ++ name)) return
-- | find a comorphism in a logic graph
lookupComorphism :: Monad m => String -> LogicGraph -> m AnyComorphism
lookupComorphism = lookupCompComorphism . splitOn ';'
-- | find a modification in a logic graph
lookupModification :: (Monad m) => String -> LogicGraph -> m AnyModification
lookupModification input lG
= case parse (parseModif lG << eof) "" input of
Left err -> fail $ show err
parseModif :: (Monad m) => LogicGraph -> Parser (m AnyModification)
(xs, _) <- separatedBy (vertcomp lG) crossT
m : ms -> return $ foldM horCompModification m ms
Nothing -> fail "Illegal empty horizontal composition"
vertcomp :: (Monad m) => LogicGraph -> Parser (m AnyModification)
(xs, _) <- separatedBy (pm lG) semiT
m : ms -> return $ foldM vertCompModification m ms
-- r has type Maybe (m AnyModification)
Nothing -> fail "Illegal empty vertical composition"
pm :: (Monad m) => LogicGraph -> Parser (m AnyModification)
pm lG = parseName lG <|> bracks lG
bracks :: (Monad m) => LogicGraph -> Parser (m AnyModification)
parseIdentity :: (Monad m) => LogicGraph -> Parser (m AnyModification)
Nothing -> fail $ "Cannot find comorphism" ++ name
Just x -> return $ return $ idModification x
parseName :: (Monad m) => LogicGraph -> Parser (m AnyModification)
parseName lG = parseIdentity lG <|> do
Nothing -> fail $ "Cannot find modification" ++ name
Just x -> return $ return x
-- * The Grothendieck signature category
-- | Grothendieck signature morphisms with indices
data GMorphism = forall cid lid1 sublogics1
basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
lid1 sublogics1 basic_spec1 sentence1
symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2
symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => GMorphism
, gMorphismSign :: ExtSign sign1 symbol1
, gMorphismSignIdx :: SigId -- ^ 'G_sign' index of source signature
, gMorphismMor :: morphism2
, gMorphismMorIdx :: MorId -- ^ `G_morphism index of target morphism
instance Eq GMorphism where
a == b = compare a b == EQ
instance Ord GMorphism where
compare (GMorphism cid1 sigma1 in1 mor1 in1')
(GMorphism cid2 sigma2 in2 mor2 in2') =
case compare (Comorphism cid1, G_sign (sourceLogic cid1) sigma1 in1)
(Comorphism cid2, G_sign (sourceLogic cid2) sigma2 in2) of
EQ -> if in1' > startMorId && in2' > startMorId && in1' == in2'
compare (coerceMorphism (targetLogic cid1) (targetLogic cid2)
-- this coersion will succeed, because cid1 and cid2 are equal
isHomogeneous :: GMorphism -> Bool
isHomogeneous (GMorphism cid _ _ _ _) =
isIdComorphism (Comorphism cid)
data Grothendieck = Grothendieck deriving (Typeable, Show)
instance Language Grothendieck
instance Show GMorphism where
show (GMorphism cid s _ m _) =
show (Comorphism cid) ++ "(" ++ show s ++ ")" ++ show m
instance Pretty GMorphism where
pretty (GMorphism cid (ExtSign s _) _ m _) = let c = Comorphism cid in fsep
, if isIdComorphism c then empty else specBraces $ space <> pretty s
-- signature category of the Grothendieck institution
instance Category G_sign GMorphism where
ide (G_sign lid sigma@(ExtSign s _) ind) =
GMorphism (mkIdComorphism lid (top_sublogic lid))
sigma ind (ide s) startMorId
-- composition of Grothendieck signature morphisms
composeMorphisms (GMorphism r1 sigma1 ind1 mor1 _)
(GMorphism r2 _sigma2 _ mor2 _) =
do let lid1 = sourceLogic r1
-- if the second comorphism is the identity then simplify immediately
if isIdComorphism (Comorphism r2) then do
mor' <- composeMorphisms mor1 mor2'
return (GMorphism r1 sigma1 ind1 mor' startMorId)
{- coercion between target of first and
source of second Grothendieck morphism -}
{- map signature morphism component of first Grothendieck morphism
along the comorphism component of the second one ... -}
mor1'' <- map_morphism r2 mor1'
{- and then compose the result with the signature morphism component
mor <- composeMorphisms mor1'' mor2
-- also if the first comorphism is the identity...
if isIdComorphism (Comorphism r1) &&
(isSubElem (targetSublogic r2))
-- ... then things simplify ...
return (GMorphism r2 sigma1' ind1 mor startMorId)
else return $ GMorphism (CompComorphism r1 r2)
sigma1 ind1 mor startMorId
dom (GMorphism r sigma ind _mor _) =
G_sign (sourceLogic r) sigma ind
cod (GMorphism r (ExtSign _ _) _ mor _) =
in G_sign lid2 (makeExtSign lid2 sig2) startSigId
isInclusion (GMorphism cid _ _ mor _) =
isInclusionComorphism cid && isInclusion mor
legal_mor (GMorphism r (ExtSign s _) _ mor _) = do
case maybeResult $ map_sign r s of
Just (sigma', _) | sigma' == cod mor -> return ()
-- | Embedding of homogeneous signature morphisms as Grothendieck sig mors
gEmbed2 :: G_sign -> G_morphism -> GMorphism
gEmbed2 (G_sign lid2 sig si) (G_morphism lid mor ind) =
let cid = mkIdComorphism lid (top_sublogic lid)
Just sig1 = coerceSign lid2 (sourceLogic cid) "gEmbed2" sig
in GMorphism cid sig1 si mor ind
-- | Embedding of homogeneous signature morphisms as Grothendieck sig mors
gEmbed :: G_morphism -> GMorphism
gEmbed (G_morphism lid mor ind) = let sig = dom mor in
GMorphism (mkIdComorphism lid (top_sublogic lid))
(makeExtSign lid sig) startSigId mor ind
-- | Embedding of comorphisms as Grothendieck sig mors
gEmbedComorphism :: AnyComorphism -> G_sign -> Result GMorphism
gEmbedComorphism (Comorphism cid) (G_sign lid sig ind) = do
sig'@(ExtSign s _) <- coerceSign lid (sourceLogic cid) "gEmbedComorphism" sig
(sigTar, _) <- map_sign cid s
return (GMorphism cid sig' ind (ide sigTar) startMorId)
-- | heterogeneous union of two Grothendieck signatures
gsigUnion :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
gsigUnion lg both gsig1@(G_sign lid1 (ExtSign sigma1 _) _)
gsig2@(G_sign lid2 (ExtSign sigma2 _) _) =
if Logic lid1 == Logic lid2
then homogeneousGsigUnion both gsig1 gsig2
(Comorphism cid1, Comorphism cid2) <-
logicUnion lg (Logic lid1) (Logic lid2)
let lidS1 = sourceLogic cid1
sigma1' <- coercePlainSign lid1 lidS1 "Union of signaturesa" sigma1
sigma2' <- coercePlainSign lid2 lidS2 "Union of signaturesb" sigma2
(sigma1'', _) <- map_sign cid1 sigma1' -- where to put axioms???
(sigma2'', _) <- map_sign cid2 sigma2' -- where to put axioms???
sigma2''' <- coercePlainSign lidT2 lidT1 "Union of signaturesc" sigma2''
sigma3 <- signature_union lidT1 sigma1'' sigma2'''
return $ G_sign lidT1 (ExtSign sigma3 $ symset_of lidT1
$ if both then sigma3 else sigma2''') startSigId
-- | homogeneous Union of two Grothendieck signatures
homogeneousGsigUnion :: Bool -> G_sign -> G_sign -> Result G_sign
homogeneousGsigUnion both (G_sign lid1 sigma1 _) (G_sign lid2 sigma2 _) = do
sigma2'@(ExtSign sig2 _) <- coerceSign lid2 lid1 "Union of signatures" sigma2
sigma3@(ExtSign sig3 _) <- ext_signature_union lid1 sigma1 sigma2'
(if both then sigma3 else ExtSign sig3 $ symset_of lid1 sig2)
homGsigDiff :: G_sign -> G_sign -> Result G_sign
homGsigDiff (G_sign lid1 (ExtSign s1 _) _) (G_sign lid2 (ExtSign s2 _) _) = do
s3 <- coercePlainSign lid2 lid1 "hom differerence of signatures" s2
s4 <- signatureDiff lid1 s1 s3
return $ G_sign lid1 (makeExtSign lid1 s4) startSigId
-- | union of a list of Grothendieck signatures
gsigManyUnion :: LogicGraph -> [G_sign] -> Result G_sign
fail "union of emtpy list of signatures"
gsigManyUnion lg (gsigma : gsigmas) =
foldM (gsigUnion lg True) gsigma gsigmas
-- | homogeneous Union of a list of morphisms
homogeneousMorManyUnion :: [G_morphism] -> Result G_morphism
homogeneousMorManyUnion [] =
fail "homogeneous union of emtpy list of morphisms"
homogeneousMorManyUnion (gmor : gmors) =
foldM ( \ (G_morphism lid2 mor2 _) (G_morphism lid1 mor1 _) -> do
mor1' <- coerceMorphism lid1 lid2 "homogeneousMorManyUnion" mor1
mor <- morphism_union lid2 mor1' mor2
return (G_morphism lid2 mor startMorId)) gmor gmors
-- | intersection of a list of Grothendieck signatures
gsigManyIntersect :: LogicGraph -> [G_sign] -> Result G_sign
fail "intersection of emtpy list of signatures"
gsigManyIntersect lg (gsigma : gsigmas) =
foldM (gsigIntersect lg True) gsigma gsigmas
-- | heterogeneous union of two Grothendieck signatures
gsigIntersect :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
gsigIntersect lg both gsig1@(G_sign lid1 (ExtSign sigma1 _) _)
gsig2@(G_sign lid2 (ExtSign sigma2 _) _) =
if Logic lid1 == Logic lid2
then homogeneousGsigIntersect both gsig1 gsig2
else error "intersection of heterogeneous signatures is not supported yet"
-- | homogeneous intersection of two Grothendieck signatures
homogeneousGsigIntersect :: Bool -> G_sign -> G_sign -> Result G_sign
homogeneousGsigIntersect both (G_sign lid1 sigma1@(ExtSign sig1 syms1) _) (G_sign lid2 sigma2 _) = do
sigma2'@(ExtSign sig2 _) <- coerceSign lid2 lid1 "Intersection of signatures" sigma2
sigma3@(ExtSign sig3 _) <- ext_signature_intersect lid1 sigma1 sigma2'
let syms2 = symset_of lid1 sig2
-- | inclusion between two logics
logicInclusion :: LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicInclusion logicGraph l1@(Logic lid1) (Logic lid2) =
let ln1 = language_name lid1
ln2 = language_name lid2 in
else case
Map.lookup (ln1, ln2) (inclusions logicGraph) of
fail ("No inclusion from " ++ ln1 ++ " to " ++ ln2 ++ " found")
updateMorIndex :: MorId -> GMorphism -> GMorphism
updateMorIndex i (GMorphism cid sign si mor _) = GMorphism cid sign si mor i
toG_morphism :: GMorphism -> G_morphism
toG_morphism (GMorphism cid _ _ mor i) = G_morphism (targetLogic cid) mor i
gSigCoerce :: LogicGraph -> G_sign -> AnyLogic
-> Result (G_sign, AnyComorphism)
gSigCoerce lg g@(G_sign lid1 sigma1 _) l2@(Logic lid2) =
if Logic lid1 == Logic lid2
then return (g, idComorphism l2) else do
cmor@(Comorphism i) <- logicInclusion lg (Logic lid1) l2
coerceSign lid1 (sourceLogic i) "gSigCoerce of signature" sigma1
(sigma1'', _) <- map_sign i sigma1'
return (G_sign lid (ExtSign sigma1'' sys) startSigId, cmor)
-- | inclusion morphism between two Grothendieck signatures
ginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion = inclusionAux True
inclusionAux :: Bool -> LogicGraph -> G_sign -> G_sign -> Result GMorphism
inclusionAux guard lg (G_sign lid1 sigma1 ind) (G_sign lid2 sigma2 _) = do
Comorphism i <- logicInclusion lg (Logic lid1) (Logic lid2)
ext1@(ExtSign sigma1' _) <-
coerceSign lid1 (sourceLogic i) "Inclusion of signatures" sigma1
(sigma1'', _) <- map_sign i sigma1'
coerceSign lid2 (targetLogic i) "Inclusion of signatures" sigma2
mor <- (if guard then inclusion else subsig_inclusion)
(targetLogic i) sigma1'' sigma2'
return (GMorphism i ext1 ind mor startMorId)
genCompInclusion :: (G_sign -> G_sign -> Result GMorphism)
-> GMorphism -> GMorphism -> Result GMorphism
genCompInclusion f mor1 mor2 = do
mor <- composeMorphisms mor1 incl
composeMorphisms mor mor2
{- | Composition of two Grothendieck signature morphisms
with intermediate inclusion -}
compInclusion :: LogicGraph -> GMorphism -> GMorphism -> Result GMorphism
compInclusion = genCompInclusion . inclusionAux False
-- | Find all (composites of) comorphisms starting from a given logic
findComorphismPaths :: LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismPaths lg (G_sublogics lid sub) =
nubOrd $ map fst $ iterateComp (0 :: Int) [(idc, [idc])]
idc = Comorphism (mkIdComorphism lid sub)
-- compute possible compositions, but only up to depth 4
if n > 2 || l == newL then newL else iterateComp (n + 1) newL
newL = nubOrd $ l ++ concatMap extend l
-- extend comorphism list in all directions, but no cylces
case compComorphism coMor c of
Just c1 -> Just (c1, c : cmps)
in mapMaybe addCoMor $ filter (not . (`elem` cmps)) coMors
-- | graph representation of the logic graph
logicGraph2Graph :: LogicGraph
-> Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism
let relevantMorphisms = filter hasModelExpansion .
Map.elems $ comorphisms lg
neighbours = \ (G_sublogics lid sl, c1) ->
let coerce c = forceCoerceSublogic lid (sourceLogic c)
(\ (Comorphism c) -> maybe Nothing (\ sl1 -> Just (Comorphism c,
(G_sublogics (targetLogic c) sl1, Just $ Comorphism c)))
(mapSublogic c (coerce c sl))) $
filter (\ (Comorphism c) -> Logic (sourceLogic c) == Logic lid
&& isSubElem (coerce c sl) (sourceSublogic c)
Just (Comorphism c1') -> show c1' /= show c
_ -> True)) relevantMorphisms,
weight = \ (Comorphism c) -> if Logic (sourceLogic c) ==
Logic (targetLogic c) then 1 else 3
-- | finds first comorphism with a matching sublogic
findComorphism :: Monad m => G_sublogics -> [AnyComorphism] -> m AnyComorphism
findComorphism _ [] = fail "No matching comorphism found"
findComorphism gsl@(G_sublogics lid sub) (Comorphism cid : rest) =
let l2 = sourceLogic cid in
&& isSubElem (forceCoerceSublogic lid l2 sub) (sourceSublogic cid)
then return $ Comorphism cid
else findComorphism gsl rest
{- | check transportability of Grothendieck signature morphisms
(currently returns false for heterogeneous morphisms) -}
isTransportable :: GMorphism -> Bool
isTransportable (GMorphism cid _ ind1 mor ind2) =
ind1 > startSigId && ind2 > startMorId
&& isModelTransportable (Comorphism cid)
&& is_transportable (targetLogic cid) mor
-- * Lax triangles and weakly amalgamable squares of lax triangles
{- a lax triangle looks like:
i -------------------------------------> k
i ------------- > j -------------------> k
and I_k is quasi-semi-exact -}
data LaxTriangle = LaxTriangle {
laxModif :: AnyModification,
laxFst, laxSnd, laxTarget :: AnyComorphism
} deriving (Show, Eq, Ord)
{- a weakly amalgamable square of lax triangles
consists of two lax triangles with the same laxTarget -}
leftTriangle, rightTriangle :: LaxTriangle
} deriving (Show, Eq, Ord)
-- for deriving Eq, first equality for modifications is needed
mkIdSquare :: AnyLogic -> Square
mkIdSquare (Logic lid) = let
idCom = Comorphism (mkIdComorphism lid (top_sublogic lid))
idMod = idModification idCom
idTriangle = LaxTriangle {
in Square {leftTriangle = idTriangle, rightTriangle = idTriangle}
mkDefSquare :: AnyComorphism -> Square
mkDefSquare c1@(Comorphism cid1) = let
idComS = Comorphism $ mkIdComorphism (sourceLogic cid1) $
top_sublogic $ sourceLogic cid1
idComT = Comorphism $ mkIdComorphism (targetLogic cid1) $
top_sublogic $ targetLogic cid1
idMod = idModification c1
lTriangle = LaxTriangle {
rTriangle = LaxTriangle {
in Square {leftTriangle = lTriangle, rightTriangle = rTriangle}
mirrorSquare :: Square -> Square
mirrorSquare s = Square {
leftTriangle = rightTriangle s,
rightTriangle = leftTriangle s}
lookupSquare :: AnyComorphism -> AnyComorphism -> LogicGraph -> Result [Square]
lookupSquare com1 com2 lg = maybe (fail "lookupSquare") return $ do
return $ nubOrd $ sqL1 ++ map mirrorSquare sqL2
-- maybe adjusted if comparing AnyModifications change