Grothendieck.hs revision 6ccaeced9d4aa7b1c0268eea85e2b6118ee1dff7
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{-# LANGUAGE ExistentialQuantification, MultiParamTypeClasses
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , DeriveDataTypeable, GeneralizedNewtypeDeriving #-}
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski{- |
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiModule : $Header$
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederDescription : Grothendieck logic (flattening of logic graph to a single logic)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : till@informatik.uni-bremen.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable (overlapping instances, dynamics, existentials)
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiGrothendieck logic (flattening of logic graph to a single logic)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiThe Grothendieck logic is defined to be the
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski heterogeneous logic over the logic graph.
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski This will be the logic over which the data
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski structures and algorithms for specification in-the-large
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder are built.
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder This module heavily works with existential types, see
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder <http://haskell.org/hawiki/ExistentialTypes> and chapter 7 of /Heterogeneous
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder specification and the heterogeneous tool set/
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (<http://www.informatik.uni-bremen.de/~till/papers/habil.ps>).
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder References:
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder R. Diaconescu:
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder Grothendieck institutions
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski J. applied categorical structures 10, 2002, p. 383-402.
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder T. Mossakowski:
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Comorphism-based Grothendieck institutions.
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder In K. Diks, W. Rytter (Eds.), Mathematical foundations of computer science,
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder LNCS 2420, pp. 593-604
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder T. Mossakowski:
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Heterogeneous specification and the heterogeneous tool set.
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-}
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskimodule Logic.Grothendieck
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ( G_basic_spec (..)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder , G_sign (..)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , SigId (..)
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich , startSigId
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder , isHomSubGsign
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich , isSubGsign
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich , logicOfGsign
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich , G_symbolmap (..)
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich , G_mapofsymbol (..)
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich , G_symbol (..)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , G_symb_items_list (..)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , G_symb_map_items_list (..)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , G_sublogics (..)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , isProperSublogic
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , joinSublogics
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , G_morphism (..)
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu , MorId (..)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski , startMorId
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski , mkG_morphism
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , lessSublogicComor
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder , LogicGraph (..)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , setCurLogic
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , emptyLogicGraph
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , lookupLogic
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , lookupCurrentLogic
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , lookupCompComorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , lookupComorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , lookupModification
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , GMorphism (..)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , isHomogeneous
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , isHomInclusion
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , Grothendieck (..)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , gEmbed
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , gEmbed2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , gEmbedComorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , gsigUnion
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , gsigManyUnion
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , homogeneousMorManyUnion
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , logicInclusion
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , logicUnion
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , updateMorIndex
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , toG_morphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , gSigCoerce
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , ginclusion
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , compInclusion
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , findComorphismPaths
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , findComorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , isTransportable
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , Square (..)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , LaxTriangle (..)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , mkIdSquare
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , mkDefSquare
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , mirrorSquare
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , lookupSquare
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ) where
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport Logic.Coerce
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Logic.Comorphism
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederimport Logic.ExtSign
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederimport Logic.Logic
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport Logic.Modification
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maederimport Logic.Morphism
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport ATerm.Lib
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Common.Doc
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Common.DocUtils
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Common.ExtSign
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Common.Id
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Common.Lexer
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Common.Parsec
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.Result
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.Token
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Common.Utils
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Control.Monad (foldM)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederimport Data.Maybe (mapMaybe)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Data.Typeable
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Data.Map as Map
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Text.ParserCombinators.Parsec (Parser, parse, eof, (<|>))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- for looking up modifications
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- * \"Grothendieck\" versions of the various parts of type class Logic
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- | Grothendieck basic specifications
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederdata G_basic_spec = forall lid sublogics
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder basic_spec sentence symb_items symb_map_items
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski sign morphism symbol raw_symbol proof_tree .
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder Logic lid sublogics
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder basic_spec sentence symb_items symb_map_items
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign morphism symbol raw_symbol proof_tree =>
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder G_basic_spec lid basic_spec
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder deriving Typeable
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance Show G_basic_spec where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder show (G_basic_spec _ s) = show s
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance Pretty G_basic_spec where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pretty (G_basic_spec _ s) = pretty s
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance GetRange G_basic_spec
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- dummy instances for development graphs
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Ord G_basic_spec where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare _ _ = EQ
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance Eq G_basic_spec where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ == _ = True
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- | index for signatures
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maedernewtype SigId = SigId Int
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder deriving (Typeable, Show, Eq, Ord, Enum, ShATermConvertible)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederstartSigId :: SigId
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederstartSigId = SigId 0
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder{- | Grothendieck signatures with an lookup index. Zero indices
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder indicate unknown ones. It would be nice to have special (may be
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder negative) indices for empty signatures (one for every logic). -}
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederdata G_sign = forall lid sublogics
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder basic_spec sentence symb_items symb_map_items
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sign morphism symbol raw_symbol proof_tree .
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Logic lid sublogics
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder basic_spec sentence symb_items symb_map_items
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sign morphism symbol raw_symbol proof_tree => G_sign
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski { gSignLogic :: lid
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , gSign :: ExtSign sign symbol
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , gSignSelfIdx :: SigId -- ^ index to lookup this 'G_sign' in sign map
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder } deriving Typeable
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance Eq G_sign where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski a == b = compare a b == EQ
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance Ord G_sign where
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder compare (G_sign l1 sigma1 s1) (G_sign l2 sigma2 s2) =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder if s1 > startSigId && s2 > startSigId && s1 == s2 then EQ else
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case compare (language_name l1) $ language_name l2 of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder EQ -> compare (coerceSign l1 l2 "Eq G_sign" sigma1) $ Just sigma2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder r -> r
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | prefer a faster subsignature test if possible
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederisHomSubGsign :: G_sign -> G_sign -> Bool
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederisHomSubGsign (G_sign l1 sigma1 s1) (G_sign l2 sigma2 s2) =
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder (s1 > startSigId && s2 > startSigId && s1 == s2) ||
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder maybe False (ext_is_subsig l1 sigma1)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (coerceSign l2 l1 "isHomSubGsign" sigma2)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederisSubGsign :: LogicGraph -> G_sign -> G_sign -> Bool
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederisSubGsign lg (G_sign lid1 (ExtSign sigma1 _) _)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (G_sign lid2 (ExtSign sigma2 _) _) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Just True ==
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder do Comorphism cid <- resultToMaybe $
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder logicInclusion lg (Logic lid1) (Logic lid2)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder sigma1' <- coercePlainSign lid1 (sourceLogic cid)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder "Grothendieck.isSubGsign: cannot happen" sigma1
3df765bba27034f17ba60ee9b90d7dbd3643ea9eChristian Maeder sigma2' <- coercePlainSign lid2 (targetLogic cid)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder "Grothendieck.isSubGsign: cannot happen" sigma2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder sigma1t <- resultToMaybe $ map_sign cid sigma1'
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return $ is_subsig (targetLogic cid) (fst sigma1t) sigma2'
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance Show G_sign where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder show (G_sign _ s _) = show s
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance Pretty G_sign where
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder pretty (G_sign _ (ExtSign s _) _) = pretty s
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederlogicOfGsign :: G_sign -> AnyLogic
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederlogicOfGsign (G_sign lid _ _) = Logic lid
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder-- | Grothendieck maps with symbol as keys
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederdata G_symbolmap a = forall lid sublogics
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder basic_spec sentence symb_items symb_map_items
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder sign morphism symbol raw_symbol proof_tree .
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Logic lid sublogics
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder basic_spec sentence symb_items symb_map_items
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder sign morphism symbol raw_symbol proof_tree =>
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder G_symbolmap lid (Map.Map symbol a)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder deriving Typeable
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maederinstance Show a => Show (G_symbolmap a) where
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder show (G_symbolmap _ sm) = show sm
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maederinstance (Typeable a, Ord a) => Eq (G_symbolmap a) where
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder a == b = compare a b == EQ
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maederinstance (Typeable a, Ord a) => Ord (G_symbolmap a) where
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder compare (G_symbolmap l1 sm1) (G_symbolmap l2 sm2) =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder case compare (language_name l1) $ language_name l2 of
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder EQ -> compare (coerceSymbolmap l1 l2 sm1) sm2
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder r -> r
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- | Grothendieck maps with symbol as values
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederdata G_mapofsymbol a = forall lid sublogics
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder basic_spec sentence symb_items symb_map_items
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign morphism symbol raw_symbol proof_tree .
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Logic lid sublogics
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder basic_spec sentence symb_items symb_map_items
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder sign morphism symbol raw_symbol proof_tree =>
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder G_mapofsymbol lid (Map.Map a symbol)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder deriving Typeable
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederinstance Show a => Show (G_mapofsymbol a) where
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder show (G_mapofsymbol _ sm) = show sm
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederinstance (Typeable a, Ord a) => Eq (G_mapofsymbol a) where
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder a == b = compare a b == EQ
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance (Typeable a, Ord a) => Ord (G_mapofsymbol a) where
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder compare (G_mapofsymbol l1 sm1) (G_mapofsymbol l2 sm2) =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder case compare (language_name l1) $ language_name l2 of
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder EQ -> compare (coerceMapofsymbol l1 l2 sm1) sm2
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder r -> r
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder-- | Grothendieck symbols
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederdata G_symbol = forall lid sublogics
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder basic_spec sentence symb_items symb_map_items
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign morphism symbol raw_symbol proof_tree .
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Logic lid sublogics
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder basic_spec sentence symb_items symb_map_items
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder sign morphism symbol raw_symbol proof_tree =>
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder G_symbol lid symbol
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder deriving Typeable
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance GetRange G_symbol where
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder getRange (G_symbol _ s) = getRange s
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder rangeSpan (G_symbol _ s) = rangeSpan s
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiinstance Show G_symbol where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder show (G_symbol _ s) = show s
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiinstance Pretty G_symbol where
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder pretty (G_symbol _ s) = pretty s
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance Eq G_symbol where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder a == b = compare a b == EQ
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederinstance Ord G_symbol where
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder compare (G_symbol l1 s1) (G_symbol l2 s2) =
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder case compare (language_name l1) $ language_name l2 of
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder EQ -> compare (coerceSymbol l1 l2 s1) s2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder r -> r
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- | Grothendieck symbol lists
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maederdata G_symb_items_list = forall lid sublogics
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder basic_spec sentence symb_items symb_map_items
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder sign morphism symbol raw_symbol proof_tree .
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Logic lid sublogics
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder basic_spec sentence symb_items symb_map_items
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign morphism symbol raw_symbol proof_tree =>
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder G_symb_items_list lid [symb_items]
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder deriving Typeable
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance GetRange G_symb_items_list
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maederinstance Show G_symb_items_list where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder show (G_symb_items_list _ l) = show l
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maederinstance Pretty G_symb_items_list where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder pretty (G_symb_items_list _ l) = ppWithCommas l
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maederinstance Eq G_symb_items_list where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (G_symb_items_list i1 s1) == (G_symb_items_list i2 s2) =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder coerceSymbItemsList i1 i2 "Eq G_symb_items_list" s1 == Just s2
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder-- | Grothendieck symbol maps
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maederdata G_symb_map_items_list = forall lid sublogics
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder basic_spec sentence symb_items symb_map_items
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sign morphism symbol raw_symbol proof_tree .
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian Maeder Logic lid sublogics
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski basic_spec sentence symb_items symb_map_items
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder sign morphism symbol raw_symbol proof_tree =>
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski G_symb_map_items_list lid [symb_map_items]
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder deriving Typeable
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiinstance GetRange G_symb_map_items_list
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiinstance Show G_symb_map_items_list where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder show (G_symb_map_items_list _ l) = show l
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiinstance Pretty G_symb_map_items_list where
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski pretty (G_symb_map_items_list _ l) = ppWithCommas l
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance Eq G_symb_map_items_list where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (G_symb_map_items_list i1 s1) == (G_symb_map_items_list i2 s2) =
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski coerceSymbMapItemsList i1 i2 "Eq G_symb_map_items_list" s1 == Just s2
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski-- | Grothendieck sublogics
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maederdata G_sublogics = forall lid sublogics
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder basic_spec sentence symb_items symb_map_items
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder sign morphism symbol raw_symbol proof_tree .
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Logic lid sublogics
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder basic_spec sentence symb_items symb_map_items
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder sign morphism symbol raw_symbol proof_tree =>
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder G_sublogics lid sublogics
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder deriving Typeable
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maederinstance Show G_sublogics where
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder show (G_sublogics lid sub) = language_name lid ++ case sublogicName sub of
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder [] -> ""
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder h -> '.' : h
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maederinstance Eq G_sublogics where
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder g1 == g2 = compare g1 g2 == EQ
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiinstance Ord G_sublogics where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder compare (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder case compare (language_name lid1) $ language_name lid2 of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder EQ -> compare (forceCoerceSublogic lid1 lid2 l1) l2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder r -> r
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
243b39800f5ea9033daca8ce5475531d114e1877Christian MaederisProperSublogic :: G_sublogics -> G_sublogics -> Bool
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiisProperSublogic a@(G_sublogics lid1 l1) b@(G_sublogics lid2 l2) =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder isSubElem (forceCoerceSublogic lid1 lid2 l1) l2 && a /= b
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederjoinSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics
746440cc1b984a852f5864235b8fa3930963a081Christian MaederjoinSublogics (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder case coerceSublogic lid1 lid2 "coerce Sublogic" l1 of
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Just sl -> Just (G_sublogics lid2 (join sl l2))
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Nothing -> Nothing
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder-- | index for morphisms
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maedernewtype MorId = MorId Int
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder deriving (Typeable, Show, Eq, Ord, Enum, ShATermConvertible)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederstartMorId :: MorId
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederstartMorId = MorId 0
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder{- | Homogeneous Grothendieck signature morphisms with indices. For
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederthe domain index it would be nice it showed also the emptiness. -}
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederdata G_morphism = forall lid sublogics
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder basic_spec sentence symb_items symb_map_items
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder sign morphism symbol raw_symbol proof_tree .
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Logic lid sublogics
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder basic_spec sentence symb_items symb_map_items
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder sign morphism symbol raw_symbol proof_tree => G_morphism
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder { gMorphismLogic :: lid
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder , gMorphism :: morphism
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder , gMorphismSelfIdx :: MorId -- ^ lookup index in morphism map
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder } deriving Typeable
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederinstance Show G_morphism where
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder show (G_morphism _ m _) = show m
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederinstance Pretty G_morphism where
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder pretty (G_morphism _ m _) = pretty m
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaedermkG_morphism :: forall lid sublogics
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder basic_spec sentence symb_items symb_map_items
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder sign morphism symbol raw_symbol proof_tree .
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Logic lid sublogics
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder basic_spec sentence symb_items symb_map_items
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder sign morphism symbol raw_symbol proof_tree
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder => lid -> morphism -> G_morphism
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaedermkG_morphism l m = G_morphism l m startMorId
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder-- | check if sublogic fits for comorphism
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederlessSublogicComor :: G_sublogics -> AnyComorphism -> Bool
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederlessSublogicComor (G_sublogics lid1 sub1) (Comorphism cid) =
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder let lid2 = sourceLogic cid
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder in language_name lid2 == language_name lid1
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder && isSubElem (forceCoerceSublogic lid1 lid2 sub1) (sourceSublogic cid)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder-- | Logic graph
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederdata LogicGraph = LogicGraph
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder { logics :: Map.Map String AnyLogic
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder , currentLogic :: String
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder , comorphisms :: Map.Map String AnyComorphism
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder , inclusions :: Map.Map (String, String) AnyComorphism
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder , unions :: Map.Map (String, String) (AnyComorphism, AnyComorphism)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder , morphisms :: Map.Map String AnyMorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , modifications :: Map.Map String AnyModification
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , squares :: Map.Map (AnyComorphism, AnyComorphism) [Square]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , qTATranslations :: Map.Map String AnyComorphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder } deriving Show
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederemptyLogicGraph :: LogicGraph
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederemptyLogicGraph = LogicGraph
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { logics = Map.empty
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , currentLogic = "CASL"
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder , comorphisms = Map.empty
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , inclusions = Map.empty
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till Mossakowski , unions = Map.empty
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , morphisms = Map.empty
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , modifications = Map.empty
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till Mossakowski , squares = Map.empty
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till Mossakowski , qTATranslations = Map.empty }
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till Mossakowski
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till MossakowskisetCurLogic :: String -> LogicGraph -> LogicGraph
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till MossakowskisetCurLogic s lg = lg { currentLogic = s }
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowskiinstance Pretty LogicGraph where
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski pretty lg = text ("current logic is: " ++ currentLogic lg)
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski $+$ text "all logics:"
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski $+$ sepByCommas (map text $ Map.keys $ logics lg)
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski $+$ text "comorphism inclusions:"
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang $+$ vcat (map pretty $ Map.elems $ inclusions lg)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder $+$ text "all comorphisms:"
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang $+$ vcat (map pretty $ Map.elems $ comorphisms lg)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang-- | find a logic in a logic graph
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskilookupLogic :: Monad m => String -> String -> LogicGraph -> m AnyLogic
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WanglookupLogic error_prefix logname logicGraph =
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang case Map.lookup logname $ logics logicGraph of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Nothing -> fail $ error_prefix ++ " in LogicGraph logic \""
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang ++ logname ++ "\" unknown"
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Just lid -> return lid
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WanglookupCurrentLogic :: Monad m => String -> LogicGraph -> m AnyLogic
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WanglookupCurrentLogic msg lg = lookupLogic msg (currentLogic lg) lg
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang-- | union to two logics
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WanglogicUnion :: LogicGraph -> AnyLogic -> AnyLogic
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder -> Result (AnyComorphism, AnyComorphism)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WanglogicUnion lg l1@(Logic lid1) l2@(Logic lid2) =
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang case logicInclusion lg l1 l2 of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Result _ (Just c) -> return (c, idComorphism l2)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang _ -> case logicInclusion lg l2 l1 of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Result _ (Just c) -> return (idComorphism l1, c)
_ -> case Map.lookup (ln1, ln2) (unions lg) of
Just u -> return u
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
ln2 = language_name lid2
-- | find a comorphism composition in a logic graph
lookupCompComorphism :: Monad m => [String] -> LogicGraph -> m AnyComorphism
lookupCompComorphism nameList logicGraph = do
cs <- mapM lookupN nameList
case cs of
c : cs1 -> foldM compComorphism c cs1
_ -> fail "Illegal empty comorphism composition"
where
lookupN name =
case name of
'i' : 'd' : '_' : logic -> do
let (mainLogic, subLogicD) = span (/= '.') logic
-- subLogicD will begin with a . which has to be removed
sublogic <- if null subLogicD
then fail $ "missing sublogic for " ++ logic
else return $ tail subLogicD
Logic lid <- maybe (fail ("Cannot find Logic " ++ mainLogic)) return
$ Map.lookup mainLogic (logics logicGraph)
case filter (\ s -> sublogic == sublogicName s)
$ all_sublogics lid of
[] -> fail $ "unknown sublogic name " ++ sublogic
s : _ -> return $ Comorphism $ mkIdComorphism lid s
_ -> maybe (fail ("Cannot find logic comorphism " ++ name)) return
$ Map.lookup name (comorphisms logicGraph)
-- | 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
Right x -> x
parseModif :: (Monad m) => LogicGraph -> Parser (m AnyModification)
parseModif lG = do
(xs, _) <- separatedBy (vertcomp lG) crossT
let r = do
y <- sequence xs
case y of
m : ms -> return $ foldM horCompModification m ms
_ -> Nothing
case r of
Nothing -> fail "Illegal empty horizontal composition"
Just m -> return m
vertcomp :: (Monad m) => LogicGraph -> Parser (m AnyModification)
vertcomp lG = do
(xs, _) <- separatedBy (pm lG) semiT
let r = do
y <- sequence xs
case y of
m : ms -> return $ foldM vertCompModification m ms
_ -> Nothing
-- r has type Maybe (m AnyModification)
case r of
Nothing -> fail "Illegal empty vertical composition"
Just m -> return m
pm :: (Monad m) => LogicGraph -> Parser (m AnyModification)
pm lG = parseName lG <|> bracks lG
bracks :: (Monad m) => LogicGraph -> Parser (m AnyModification)
bracks lG = do
oParenT
modif <- parseModif lG
cParenT
return modif
parseIdentity :: (Monad m) => LogicGraph -> Parser (m AnyModification)
parseIdentity lG = do
tryString "id_"
tok <- simpleId
let name = tokStr tok
case Map.lookup name (comorphisms lG) of
Nothing -> fail $ "Cannot find comorphism" ++ name
Just x -> return $ return $ idModification x
parseName :: (Monad m) => LogicGraph -> Parser (m AnyModification)
parseName lG = parseIdentity lG <|> do
tok <- simpleId
let name = tokStr tok
case Map.lookup name (modifications lG) of
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
lid2 sublogics2
basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
Comorphism cid
lid1 sublogics1 basic_spec1 sentence1
symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2
symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => GMorphism
{ gMorphismComor :: cid
, gMorphismSign :: ExtSign sign1 symbol1
, gMorphismSignIdx :: SigId -- ^ 'G_sign' index of source signature
, gMorphismMor :: morphism2
, gMorphismMorIdx :: MorId -- ^ `G_morphism index of target morphism
} deriving Typeable
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'
then EQ else
compare (coerceMorphism (targetLogic cid1) (targetLogic cid2)
"Ord GMorphism.coerceMorphism" mor1) (Just mor2)
-- this coersion will succeed, because cid1 and cid2 are equal
r -> r
isHomogeneous :: GMorphism -> Bool
isHomogeneous (GMorphism cid _ _ _ _) =
isIdComorphism (Comorphism cid)
isHomInclusion :: GMorphism -> Bool
isHomInclusion gm@(GMorphism _ _ _ mor _) =
isHomogeneous gm && isInclusion mor
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
[ text $ show c
, if isIdComorphism c then empty else specBraces $ space <> pretty s
, pretty m ]
-- 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
lid2 = targetLogic r1
lid3 = sourceLogic r2
lid4 = targetLogic r2
-- if the second comorphism is the identity then simplify immediately
if isIdComorphism (Comorphism r2) then do
mor2' <- coerceMorphism lid4 lid2 "Grothendieck.comp" mor2
mor' <- composeMorphisms mor1 mor2'
return (GMorphism r1 sigma1 ind1 mor' startMorId)
else do
{- coercion between target of first and
source of second Grothendieck morphism -}
mor1' <- coerceMorphism lid2 lid3 "Grothendieck.comp" mor1
{- 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
of first one -}
mor <- composeMorphisms mor1'' mor2
-- also if the first comorphism is the identity...
if isIdComorphism (Comorphism r1) &&
case coerceSublogic lid2 lid3 "Grothendieck.comp"
(targetSublogic r1) of
Just sl1 -> maybe False
(isSubElem (targetSublogic r2))
(mapSublogic r2 sl1)
_ -> False
-- ... then things simplify ...
then do
sigma1' <- coerceSign lid1 lid3 "Grothendieck.comp" sigma1
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 _) =
let lid2 = targetLogic r
sig2 = cod mor
in G_sign lid2 (makeExtSign lid2 sig2) startSigId
legal_mor (GMorphism r (ExtSign s _) _ mor _) =
legal_mor mor &&
case maybeResult $ map_sign r s of
Just (sigma', _) -> sigma' == cod mor
Nothing -> False
-- | 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 -> G_sign -> G_sign -> Result G_sign
gsigUnion lg gsig1@(G_sign lid1 (ExtSign sigma1 _) _)
gsig2@(G_sign lid2 (ExtSign sigma2 _) _) =
if language_name lid1 == language_name lid2
then homogeneousGsigUnion gsig1 gsig2
else do
(Comorphism cid1, Comorphism cid2) <-
logicUnion lg (Logic lid1) (Logic lid2)
let lidS1 = sourceLogic cid1
lidS2 = sourceLogic cid2
lidT1 = targetLogic cid1
lidT2 = targetLogic cid2
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 (makeExtSign lidT1 sigma3) startSigId)
-- | homogeneous Union of two Grothendieck signatures
homogeneousGsigUnion :: G_sign -> G_sign -> Result G_sign
homogeneousGsigUnion (G_sign lid1 sigma1 _) (G_sign lid2 sigma2 _) = do
sigma2' <- coerceSign lid2 lid1 "Union of signaturesd" sigma2
sigma3 <- ext_signature_union lid1 sigma1 sigma2'
return (G_sign lid1 sigma3 startSigId)
-- | union of a list of Grothendieck signatures
gsigManyUnion :: LogicGraph -> [G_sign] -> Result G_sign
gsigManyUnion _ [] =
fail "union of emtpy list of signatures"
gsigManyUnion lg (gsigma : gsigmas) =
foldM (gsigUnion lg) 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
-- | 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
if ln1 == ln2 then
return (idComorphism l1)
else case Map.lookup (ln1, ln2) (inclusions logicGraph) of
Just (Comorphism i) ->
return (Comorphism i)
Nothing ->
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 language_name lid1 == language_name lid2
then return (g, idComorphism l2) else do
cmor@(Comorphism i) <- logicInclusion lg (Logic lid1) l2
ExtSign sigma1' _ <-
coerceSign lid1 (sourceLogic i) "gSigCoerce of signature" sigma1
(sigma1'', _) <- map_sign i sigma1'
let lid = targetLogic i
return (G_sign lid (makeExtSign lid sigma1'') 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'
ExtSign sigma2' _ <-
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
let sigma1 = cod mor1
sigma2 = dom mor2
incl <- f sigma1 sigma2
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])]
where
idc = Comorphism (mkIdComorphism lid sub)
coMors = Map.elems $ comorphisms lg
-- compute possible compositions, but only up to depth 3
iterateComp n l =
if n > 1 || l == newL then newL else iterateComp (n + 1) newL
where
newL = nubOrd $ l ++ concatMap extend l
-- extend comorphism list in all directions, but no cylces
extend (coMor, cmps) =
let addCoMor c =
case compComorphism coMor c of
Nothing -> Nothing
Just c1 -> Just (c1, c : cmps)
in mapMaybe addCoMor $ filter (not . (`elem` cmps)) coMors
-- | 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
if language_name lid == language_name l2
&& 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:
laxTarget
i -------------------------------------> k
^ laxModif
| |
i ------------- > j -------------------> k
laxFst laxSnd
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 -}
data Square = Square {
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 {
laxModif = idMod,
laxFst = idCom,
laxSnd = idCom,
laxTarget = idCom}
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 {
laxModif = idMod,
laxFst = c1,
laxSnd = idComS,
laxTarget = c1
}
rTriangle = LaxTriangle {
laxModif = idMod,
laxFst = idComT,
laxSnd = c1,
laxTarget = c1
}
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
sqL1 <- Map.lookup (com1, com2) $ squares lg
sqL2 <- Map.lookup (com2, com1) $ squares lg
return $ nubOrd $ sqL1 ++ map mirrorSquare sqL2
-- maybe adjusted if comparing AnyModifications change