Grothendieck.hs revision 247eefa106a467b872521724ff7bf4af5c27220d
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{-# LANGUAGE ExistentialQuantification, MultiParamTypeClasses
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , DeriveDataTypeable, GeneralizedNewtypeDeriving #-}
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett{- |
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederModule : $Header$
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederDescription : Grothendieck logic (flattening of logic graph to a single logic)
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachLicense : GPLv2 or higher, see LICENSE.txt
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederMaintainer : till@informatik.uni-bremen.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : non-portable (overlapping instances, dynamics, existentials)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettGrothendieck logic (flattening of logic graph to a single logic)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett
78718c37b1a50086a27e0f031db4cf82bea934aeChristian MaederThe Grothendieck logic is defined to be the
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach heterogeneous logic over the logic graph.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach This will be the logic over which the data
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach structures and algorithms for specification in-the-large
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach are built.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder This module heavily works with existential types, see
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <http://haskell.org/hawiki/ExistentialTypes> and chapter 7 of /Heterogeneous
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder specification and the heterogeneous tool set/
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (<http://www.informatik.uni-bremen.de/~till/papers/habil.ps>).
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach References:
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder R. Diaconescu:
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Grothendieck institutions
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett J. applied categorical structures 10, 2002, p. 383-402.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach T. Mossakowski:
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder Comorphism-based Grothendieck institutions.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach In K. Diks, W. Rytter (Eds.), Mathematical foundations of computer science,
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder LNCS 2420, pp. 593-604
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblett
04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett T. Mossakowski:
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Heterogeneous specification and the heterogeneous tool set.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-}
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblettmodule Logic.Grothendieck
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder ( G_basic_spec (..)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , G_sign (..)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , SigId (..)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , startSigId
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , isHomSubGsign
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , isSubGsign
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , logicOfGsign
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett , symsOfGsign
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , G_symbolmap (..)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , G_mapofsymbol (..)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , G_symbol (..)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , G_symb_items_list (..)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , G_symb_map_items_list (..)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , G_sublogics (..)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , isSublogic
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett , isProperSublogic
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , joinSublogics
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , G_morphism (..)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , MorId (..)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , startMorId
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , mkG_morphism
a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian Maeder , lessSublogicComor
a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian Maeder , LogicGraph (..)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , setCurLogic
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , setSyntax
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , setCurSublogic
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , emptyLogicGraph
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , lookupLogic
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , lookupCurrentLogic
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , lookupCurrentSyntax
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , lookupCompComorphism
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , lookupComorphism
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , lookupModification
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , GMorphism (..)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , isHomogeneous
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , Grothendieck (..)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , gEmbed
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , gEmbed2
a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian Maeder , gEmbedComorphism
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder , homGsigDiff
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , gsigUnion
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett , gsigManyUnion
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , homogeneousMorManyUnion
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett , logicInclusion
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly , logicUnion
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett , updateMorIndex
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett , toG_morphism
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , gSigCoerce
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , ginclusion
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , compInclusion
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , findComorphismPaths
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder , logicGraph2Graph
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder , findComorphism
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett , isTransportable
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett , Square (..)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , LaxTriangle (..)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , mkIdSquare
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , mkDefSquare
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , mirrorSquare
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder , lookupSquare
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ) where
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Logic.Coerce
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Logic.Comorphism
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Logic.ExtSign
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Logic.Logic
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Logic.Modification
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Logic.Morphism
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettimport ATerm.Lib
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.Doc
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettimport Common.DocUtils
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport Common.ExtSign
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport Common.Id
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport Common.IRI (IRI)
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maederimport Common.Lexer
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maederimport Common.Parsec
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maederimport Common.Result
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maederimport Common.Token
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maederimport Common.Utils
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport Common.LibName
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport Common.GraphAlgo
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettimport Control.Monad (foldM)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettimport Data.Maybe
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettimport Data.Typeable
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maederimport qualified Data.Map as Map
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettimport qualified Data.Set as Set
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettimport Text.ParserCombinators.Parsec (Parser, parse, eof, (<|>))
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- for looking up modifications
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- * \"Grothendieck\" versions of the various parts of type class Logic
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | Grothendieck basic specifications
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederdata G_basic_spec = forall lid sublogics
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly basic_spec sentence symb_items symb_map_items
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sign morphism symbol raw_symbol proof_tree .
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Logic lid sublogics
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly basic_spec sentence symb_items symb_map_items
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly sign morphism symbol raw_symbol proof_tree =>
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly G_basic_spec lid basic_spec
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly deriving Typeable
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance Show G_basic_spec where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly show (G_basic_spec _ s) = show s
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maederinstance Pretty G_basic_spec where
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett pretty (G_basic_spec _ s) = pretty s
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance GetRange G_basic_spec
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- dummy instances for development graphs
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance Ord G_basic_spec where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder compare _ _ = EQ
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance Eq G_basic_spec where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly _ == _ = True
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | index for signatures
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maedernewtype SigId = SigId Int
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder deriving (Typeable, Show, Eq, Ord, Enum, ShATermConvertible)
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederstartSigId :: SigId
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillystartSigId = SigId 0
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly{- | Grothendieck signatures with an lookup index. Zero indices
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder indicate unknown ones. It would be nice to have special (may be
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly negative) indices for empty signatures (one for every logic). -}
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillydata G_sign = forall lid sublogics
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly basic_spec sentence symb_items symb_map_items
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly sign morphism symbol raw_symbol proof_tree .
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Logic lid sublogics
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly basic_spec sentence symb_items symb_map_items
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly sign morphism symbol raw_symbol proof_tree => G_sign
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly { gSignLogic :: lid
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , gSign :: ExtSign sign symbol
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , gSignSelfIdx :: SigId -- ^ index to lookup this 'G_sign' in sign map
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly } deriving Typeable
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance Eq G_sign where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly a == b = compare a b == EQ
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance Ord G_sign where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder compare (G_sign l1 sigma1 s1) (G_sign l2 sigma2 s2) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder if s1 > startSigId && s2 > startSigId && s1 == s2 then EQ else
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case compare (Logic l1) $ Logic l2 of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly EQ -> compare (coerceSign l1 l2 "Eq G_sign" sigma1) $ Just sigma2
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly r -> r
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | prefer a faster subsignature test if possible
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyisHomSubGsign :: G_sign -> G_sign -> Bool
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyisHomSubGsign (G_sign l1 sigma1 s1) (G_sign l2 sigma2 s2) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (s1 > startSigId && s2 > startSigId && s1 == s2) ||
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly maybe False (ext_is_subsig l1 sigma1)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (coerceSign l2 l1 "isHomSubGsign" sigma2)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyisSubGsign :: LogicGraph -> G_sign -> G_sign -> Bool
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettisSubGsign lg (G_sign lid1 (ExtSign sigma1 _) _)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (G_sign lid2 (ExtSign sigma2 _) _) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Just True ==
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder do Comorphism cid <- resultToMaybe $
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder logicInclusion lg (Logic lid1) (Logic lid2)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sigma1' <- coercePlainSign lid1 (sourceLogic cid)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Grothendieck.isSubGsign: cannot happen" sigma1
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett sigma2' <- coercePlainSign lid2 (targetLogic cid)
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett "Grothendieck.isSubGsign: cannot happen" sigma2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sigma1t <- resultToMaybe $ map_sign cid sigma1'
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ is_subsig (targetLogic cid) (fst sigma1t) sigma2'
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance Show G_sign where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly show (G_sign _ s _) = show s
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance Pretty G_sign where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly pretty (G_sign _ (ExtSign s _) _) = pretty s
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillylogicOfGsign :: G_sign -> AnyLogic
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillylogicOfGsign (G_sign lid _ _) = Logic lid
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillysymsOfGsign :: G_sign -> Set.Set G_symbol
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillysymsOfGsign (G_sign lid (ExtSign sgn _) _) = Set.map (G_symbol lid)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly $ symset_of lid sgn
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | Grothendieck maps with symbol as keys
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederdata G_symbolmap a = forall lid sublogics
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder basic_spec sentence symb_items symb_map_items
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sign morphism symbol raw_symbol proof_tree .
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Logic lid sublogics
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder basic_spec sentence symb_items symb_map_items
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly sign morphism symbol raw_symbol proof_tree =>
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly G_symbolmap lid (Map.Map symbol a)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly deriving Typeable
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance Show a => Show (G_symbolmap a) where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly show (G_symbolmap _ sm) = show sm
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance (Typeable a, Ord a) => Eq (G_symbolmap a) where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder a == b = compare a b == EQ
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance (Typeable a, Ord a) => Ord (G_symbolmap a) where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder compare (G_symbolmap l1 sm1) (G_symbolmap l2 sm2) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case compare (Logic l1) $ Logic l2 of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder EQ -> compare (coerceSymbolmap l1 l2 sm1) sm2
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder r -> r
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | Grothendieck maps with symbol as values
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederdata G_mapofsymbol a = forall lid sublogics
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly basic_spec sentence symb_items symb_map_items
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign morphism symbol raw_symbol proof_tree .
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett Logic lid sublogics
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett basic_spec sentence symb_items symb_map_items
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sign morphism symbol raw_symbol proof_tree =>
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly G_mapofsymbol lid (Map.Map a symbol)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly deriving Typeable
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance Show a => Show (G_mapofsymbol a) where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder show (G_mapofsymbol _ sm) = show sm
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance (Typeable a, Ord a) => Eq (G_mapofsymbol a) where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder a == b = compare a b == EQ
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblettinstance (Typeable a, Ord a) => Ord (G_mapofsymbol a) where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett compare (G_mapofsymbol l1 sm1) (G_mapofsymbol l2 sm2) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly case compare (Logic l1) $ Logic l2 of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder EQ -> compare (coerceMapofsymbol l1 l2 sm1) sm2
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder r -> r
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | Grothendieck symbols
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederdata G_symbol = forall lid sublogics
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett basic_spec sentence symb_items symb_map_items
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett sign morphism symbol raw_symbol proof_tree .
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett Logic lid sublogics
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder basic_spec sentence symb_items symb_map_items
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sign morphism symbol raw_symbol proof_tree =>
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder G_symbol lid symbol
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder deriving Typeable
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyinstance GetRange G_symbol where
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett getRange (G_symbol _ s) = getRange s
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly rangeSpan (G_symbol _ s) = rangeSpan s
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett
06a77f038c0e1740672274377901d37d0113226dLiam O'Reillyinstance Show G_symbol where
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly show (G_symbol _ s) = show s
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyinstance Pretty G_symbol where
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly pretty (G_symbol _ s) = pretty s
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett
842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance Eq G_symbol where
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder a == b = compare a b == EQ
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettinstance Ord G_symbol where
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder compare (G_symbol l1 s1) (G_symbol l2 s2) =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case compare (Logic l1) $ Logic l2 of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly EQ -> compare (coerceSymbol l1 l2 s1) s2
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett r -> r
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | Grothendieck symbol lists
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillydata G_symb_items_list = forall lid sublogics
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett basic_spec sentence symb_items symb_map_items
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sign morphism symbol raw_symbol proof_tree .
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Logic lid sublogics
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly basic_spec sentence symb_items symb_map_items
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sign morphism symbol raw_symbol proof_tree =>
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett G_symb_items_list lid [symb_items]
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly deriving Typeable
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyinstance GetRange G_symb_items_list
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettinstance Show G_symb_items_list where
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly show (G_symb_items_list _ l) = show l
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly
842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance Pretty G_symb_items_list where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder pretty (G_symb_items_list _ l) = ppWithCommas l
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance Eq G_symb_items_list where
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett (G_symb_items_list i1 s1) == (G_symb_items_list i2 s2) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly coerceSymbItemsList i1 i2 "Eq G_symb_items_list" s1 == Just s2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | Grothendieck symbol maps
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederdata G_symb_map_items_list = forall lid sublogics
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly basic_spec sentence symb_items symb_map_items
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sign morphism symbol raw_symbol proof_tree .
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Logic lid sublogics
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly basic_spec sentence symb_items symb_map_items
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign morphism symbol raw_symbol proof_tree =>
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder G_symb_map_items_list lid [symb_map_items]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder deriving Typeable
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance GetRange G_symb_map_items_list
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyinstance Show G_symb_map_items_list where
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly show (G_symb_map_items_list _ l) = show l
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance Pretty G_symb_map_items_list where
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly pretty (G_symb_map_items_list _ l) = ppWithCommas l
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettinstance Eq G_symb_map_items_list where
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (G_symb_map_items_list i1 s1) == (G_symb_map_items_list i2 s2) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly coerceSymbMapItemsList i1 i2 "Eq G_symb_map_items_list" s1 == Just s2
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | Grothendieck sublogics
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillydata G_sublogics = forall lid sublogics
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly basic_spec sentence symb_items symb_map_items
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett sign morphism symbol raw_symbol proof_tree .
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Logic lid sublogics
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly basic_spec sentence symb_items symb_map_items
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sign morphism symbol raw_symbol proof_tree =>
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder G_sublogics lid sublogics
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly deriving Typeable
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance Show G_sublogics where
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett show (G_sublogics lid sub) = language_name lid ++ case sublogicName sub of
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly [] -> ""
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly h -> '.' : h
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly
842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance Eq G_sublogics where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder g1 == g2 = compare g1 g2 == EQ
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyinstance Ord G_sublogics where
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly compare (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett case compare (Logic lid1) $ Logic lid2 of
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly EQ -> compare (forceCoerceSublogic lid1 lid2 l1) l2
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly r -> r
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyisSublogic :: G_sublogics -> G_sublogics -> Bool
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisSublogic (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett isSubElem (forceCoerceSublogic lid1 lid2 l1) l2
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett
842ae753ab848a8508c4832ab64296b929167a97Christian MaederisProperSublogic :: G_sublogics -> G_sublogics -> Bool
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederisProperSublogic a b = isSublogic a b && a /= b
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyjoinSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyjoinSublogics (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett case coerceSublogic lid1 lid2 "coerce Sublogic" l1 of
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Just sl -> Just (G_sublogics lid2 (join sl l2))
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Nothing -> Nothing
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | index for morphisms
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maedernewtype MorId = MorId Int
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly deriving (Typeable, Show, Eq, Ord, Enum, ShATermConvertible)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillystartMorId :: MorId
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillystartMorId = MorId 0
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Homogeneous Grothendieck signature morphisms with indices. For
842ae753ab848a8508c4832ab64296b929167a97Christian Maederthe domain index it would be nice it showed also the emptiness. -}
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillydata G_morphism = forall lid sublogics
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly basic_spec sentence symb_items symb_map_items
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett sign morphism symbol raw_symbol proof_tree .
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Logic lid sublogics
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly basic_spec sentence symb_items symb_map_items
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign morphism symbol raw_symbol proof_tree => G_morphism
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett { gMorphismLogic :: lid
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , gMorphism :: morphism
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , gMorphismSelfIdx :: MorId -- ^ lookup index in morphism map
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder } deriving Typeable
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance Show G_morphism where
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly show (G_morphism _ m _) = show m
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance Pretty G_morphism where
a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett pretty (G_morphism _ m _) = pretty m
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedermkG_morphism :: forall lid sublogics
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder basic_spec sentence symb_items symb_map_items
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sign morphism symbol raw_symbol proof_tree .
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Logic lid sublogics
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly basic_spec sentence symb_items symb_map_items
7996f5f893cc14b5e22fdb7ec90a3474ba3c51abAndy Gimblett sign morphism symbol raw_symbol proof_tree
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly => lid -> morphism -> G_morphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymkG_morphism l m = G_morphism l m startMorId
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | check if sublogic fits for comorphism
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederlessSublogicComor :: G_sublogics -> AnyComorphism -> Bool
06a77f038c0e1740672274377901d37d0113226dLiam O'ReillylessSublogicComor (G_sublogics lid1 sub1) (Comorphism cid) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let lid2 = sourceLogic cid
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly in Logic lid2 == Logic lid1
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly && isSubElem (forceCoerceSublogic lid1 lid2 sub1) (sourceSublogic cid)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillytype SublogicBasedTheories = Map.Map IRI (LibName, String)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- | Logic graph
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederdata LogicGraph = LogicGraph
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder { logics :: Map.Map String AnyLogic
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , currentLogic :: String
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly , currentSyntax :: Maybe IRI
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , currentSublogic :: Maybe G_sublogics
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , currentTargetBase :: Maybe (LibName, String)
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly , sublogicBasedTheories :: Map.Map AnyLogic SublogicBasedTheories
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , comorphisms :: Map.Map String AnyComorphism
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , inclusions :: Map.Map (String, String) AnyComorphism
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , unions :: Map.Map (String, String) (AnyComorphism, AnyComorphism)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , morphisms :: Map.Map String AnyMorphism
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , modifications :: Map.Map String AnyModification
06a77f038c0e1740672274377901d37d0113226dLiam O'Reilly , squares :: Map.Map (AnyComorphism, AnyComorphism) [Square]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , qTATranslations :: Map.Map String AnyComorphism
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , prefixes :: Map.Map String IRI
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder } deriving Show
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy GimblettemptyLogicGraph :: LogicGraph
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy GimblettemptyLogicGraph = LogicGraph
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder { logics = Map.empty
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett , currentLogic = "CASL"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , currentSyntax = Nothing
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , currentSublogic = Nothing
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , currentTargetBase = Nothing
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , sublogicBasedTheories = Map.empty
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , comorphisms = Map.empty
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , inclusions = Map.empty
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , unions = Map.empty
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , morphisms = Map.empty
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , modifications = Map.empty
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , squares = Map.empty
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly , qTATranslations = Map.empty
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , prefixes = Map.empty }
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedersetCurLogicAux :: String -> LogicGraph -> LogicGraph
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedersetCurLogicAux s lg = lg { currentLogic = s }
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettsetCurLogic :: String -> LogicGraph -> LogicGraph
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy GimblettsetCurLogic s lg = if s == currentLogic lg then
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder lg else setSyntaxAux Nothing $ setCurLogicAux s lg
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillysetSyntaxAux :: Maybe IRI -> LogicGraph -> LogicGraph
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillysetSyntaxAux s lg = lg { currentSyntax = s }
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillysetSyntax :: Maybe IRI -> LogicGraph -> LogicGraph
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillysetSyntax s lg = if isNothing s then lg else setSyntaxAux s lg
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaedersetCurSublogic :: Maybe G_sublogics -> LogicGraph -> LogicGraph
842ae753ab848a8508c4832ab64296b929167a97Christian MaedersetCurSublogic s lg = lg { currentSublogic = s }
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance Pretty LogicGraph where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly pretty lg = text ("current logic is: " ++ currentLogic lg)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly $+$ text "all logics:"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly $+$ sepByCommas (map text $ Map.keys $ logics lg)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly $+$ text "comorphism inclusions:"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly $+$ vcat (map pretty $ Map.elems $ inclusions lg)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly $+$ text "all comorphisms:"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder $+$ vcat (map pretty $ Map.elems $ comorphisms lg)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | find a logic in a logic graph
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillylookupLogic :: Monad m => String -> String -> LogicGraph -> m AnyLogic
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillylookupLogic error_prefix logname logicGraph =
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder case Map.lookup logname $ logics logicGraph of
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Nothing -> fail $ error_prefix ++ "unknown logic: " ++ logname
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just lid -> return lid
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederlookupCurrentLogic :: Monad m => String -> LogicGraph -> m AnyLogic
842ae753ab848a8508c4832ab64296b929167a97Christian MaederlookupCurrentLogic msg lg = lookupLogic (msg ++ " ") (currentLogic lg) lg
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillylookupCurrentSyntax :: Monad m => String -> LogicGraph
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -> m (AnyLogic, Maybe IRI)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillylookupCurrentSyntax msg lg = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder l <- lookupLogic (msg ++ " ") (currentLogic lg) lg
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return (l, currentSyntax lg)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder-- | union to two logics
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederlogicUnion :: LogicGraph -> AnyLogic -> AnyLogic
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder -> Result (AnyComorphism, AnyComorphism)
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaederlogicUnion lg l1@(Logic lid1) l2@(Logic lid2) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case logicInclusion lg l1 l2 of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Result _ (Just c) -> return (c, idComorphism l2)
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder _ -> case logicInclusion lg l2 l1 of
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder Result _ (Just c) -> return (idComorphism l1, c)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder _ -> case Map.lookup (ln1, ln2) (unions lg) of
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett Just u -> return u
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Nothing -> case Map.lookup (ln2, ln1) (unions lg) of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just (c2, c1) -> return (c1, c2)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Nothing -> fail $ "Union of logics " ++ ln1 ++
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder " and " ++ ln2 ++ " does not exist"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder where ln1 = language_name lid1
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder ln2 = language_name lid2
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | find a comorphism composition in a logic graph
842ae753ab848a8508c4832ab64296b929167a97Christian MaederlookupCompComorphism :: Monad m => [String] -> LogicGraph -> m AnyComorphism
842ae753ab848a8508c4832ab64296b929167a97Christian MaederlookupCompComorphism nameList logicGraph = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder cs <- mapM lookupN nameList
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case cs of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder c : cs1 -> foldM compComorphism c cs1
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder _ -> fail "Illegal empty comorphism composition"
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett where
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder lookupN name =
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder case name of
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder 'i' : 'd' : '_' : logic -> do
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder let (mainLogic, subLogicD) = span (/= '.') logic
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder -- subLogicD will begin with a . which has to be removed
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder msublogic = if null subLogicD
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder then Nothing
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder else Just $ tail subLogicD
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder Logic lid <- maybe (fail ("Cannot find Logic " ++ mainLogic)) return
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder $ Map.lookup mainLogic (logics logicGraph)
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder case maybe (Just $ top_sublogic lid) (parseSublogic lid) msublogic of
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder Nothing -> fail $ maybe "missing sublogic"
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder ("unknown sublogic name " ++) msublogic
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder Just s -> return $ Comorphism $ mkIdComorphism lid s
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder _ -> maybe (fail ("Cannot find logic comorphism " ++ name)) return
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder $ Map.lookup name (comorphisms logicGraph)
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder-- | find a comorphism in a logic graph
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederlookupComorphism :: Monad m => String -> LogicGraph -> m AnyComorphism
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederlookupComorphism = lookupCompComorphism . splitOn ';'
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder-- | find a modification in a logic graph
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederlookupModification :: (Monad m) => String -> LogicGraph -> m AnyModification
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederlookupModification input lG
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder = case parse (parseModif lG << eof) "" input of
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder Left err -> fail $ show err
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder Right x -> x
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederparseModif :: (Monad m) => LogicGraph -> Parser (m AnyModification)
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian MaederparseModif lG = do
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder (xs, _) <- separatedBy (vertcomp lG) crossT
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder let r = do
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder y <- sequence xs
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder case y of
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder m : ms -> return $ foldM horCompModification m ms
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder _ -> Nothing
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder case r of
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Nothing -> fail "Illegal empty horizontal composition"
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett Just m -> return m
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maedervertcomp :: (Monad m) => LogicGraph -> Parser (m AnyModification)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maedervertcomp lG = do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (xs, _) <- separatedBy (pm lG) semiT
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly let r = do
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly y <- sequence xs
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly case y of
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly m : ms -> return $ foldM vertCompModification m ms
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly _ -> Nothing
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -- r has type Maybe (m AnyModification)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly case r of
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Nothing -> fail "Illegal empty vertical composition"
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Just m -> return m
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillypm :: (Monad m) => LogicGraph -> Parser (m AnyModification)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillypm lG = parseName lG <|> bracks lG
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillybracks :: (Monad m) => LogicGraph -> Parser (m AnyModification)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reillybracks lG = do
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly oParenT
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly modif <- parseModif lG
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly cParenT
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly return modif
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederparseIdentity :: (Monad m) => LogicGraph -> Parser (m AnyModification)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederparseIdentity lG = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder tryString "id_"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder tok <- simpleId
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly let name = tokStr tok
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly case Map.lookup name (comorphisms lG) of
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly Nothing -> fail $ "Cannot find comorphism" ++ name
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Just x -> return $ return $ idModification x
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederparseName :: (Monad m) => LogicGraph -> Parser (m AnyModification)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederparseName lG = parseIdentity lG <|> do
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly tok <- simpleId
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly let name = tokStr tok
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly case Map.lookup name (modifications lG) of
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Nothing -> fail $ "Cannot find modification" ++ name
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly Just x -> return $ return x
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- * The Grothendieck signature category
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly-- | Grothendieck signature morphisms with indices
2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reillydata GMorphism = forall cid lid1 sublogics1
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly basic_spec1 sentence1 symb_items1 symb_map_items1
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly lid2 sublogics2
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Comorphism cid
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder lid1 sublogics1 basic_spec1 sentence1
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder symb_items1 symb_map_items1
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett lid2 sublogics2 basic_spec2 sentence2
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett symb_items2 symb_map_items2
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => GMorphism
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly { gMorphismComor :: cid
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , gMorphismSign :: ExtSign sign1 symbol1
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly , gMorphismSignIdx :: SigId -- ^ 'G_sign' index of source signature
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly , gMorphismMor :: morphism2
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder , gMorphismMorIdx :: MorId -- ^ `G_morphism index of target morphism
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly } deriving Typeable
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance Eq GMorphism where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder a == b = compare a b == EQ
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance Ord GMorphism where
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly compare (GMorphism cid1 sigma1 in1 mor1 in1')
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly (GMorphism cid2 sigma2 in2 mor2 in2') =
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly case compare (Comorphism cid1, G_sign (sourceLogic cid1) sigma1 in1)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly (Comorphism cid2, G_sign (sourceLogic cid2) sigma2 in2) of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder EQ -> if in1' > startMorId && in2' > startMorId && in1' == in2'
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly then EQ else
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly compare (coerceMorphism (targetLogic cid1) (targetLogic cid2)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly "Ord GMorphism.coerceMorphism" mor1) (Just mor2)
9f31535736c3d43a98f0157efaa7f87ea73c9be0Liam O'Reilly -- this coersion will succeed, because cid1 and cid2 are equal
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder r -> r
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederisHomogeneous :: GMorphism -> Bool
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederisHomogeneous (GMorphism cid _ _ _ _) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder isIdComorphism (Comorphism cid)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederdata Grothendieck = Grothendieck deriving (Typeable, Show)
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblettinstance Language Grothendieck
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett
842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance Show GMorphism where
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder show (GMorphism cid s _ m _) =
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett show (Comorphism cid) ++ "(" ++ show s ++ ")" ++ show m
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance Pretty GMorphism where
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder pretty (GMorphism cid (ExtSign s _) _ m _) = let c = Comorphism cid in fsep
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder [ text $ show c
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett , if isIdComorphism c then empty else specBraces $ space <> pretty s
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblett , pretty m ]
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- signature category of the Grothendieck institution
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederinstance Category G_sign GMorphism where
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder ide (G_sign lid sigma@(ExtSign s _) ind) =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder GMorphism (mkIdComorphism lid (top_sublogic lid))
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sigma ind (ide s) startMorId
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- composition of Grothendieck signature morphisms
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder composeMorphisms (GMorphism r1 sigma1 ind1 mor1 _)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (GMorphism r2 _sigma2 _ mor2 _) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder do let lid1 = sourceLogic r1
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder lid2 = targetLogic r1
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder lid3 = sourceLogic r2
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder lid4 = targetLogic r2
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- if the second comorphism is the identity then simplify immediately
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder if isIdComorphism (Comorphism r2) then do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder mor2' <- coerceMorphism lid4 lid2 "Grothendieck.comp" mor2
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder mor' <- composeMorphisms mor1 mor2'
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return (GMorphism r1 sigma1 ind1 mor' startMorId)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder else do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder {- coercion between target of first and
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder source of second Grothendieck morphism -}
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder mor1' <- coerceMorphism lid2 lid3 "Grothendieck.comp" mor1
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder {- map signature morphism component of first Grothendieck morphism
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder along the comorphism component of the second one ... -}
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder mor1'' <- map_morphism r2 mor1'
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder {- and then compose the result with the signature morphism component
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder of first one -}
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder mor <- composeMorphisms mor1'' mor2
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- also if the first comorphism is the identity...
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder if isIdComorphism (Comorphism r1) &&
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case coerceSublogic lid2 lid3 "Grothendieck.comp"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (targetSublogic r1) of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just sl1 -> maybe False
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (isSubElem (targetSublogic r2))
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (mapSublogic r2 sl1)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder _ -> False
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -- ... then things simplify ...
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder then do
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett sigma1' <- coerceSign lid1 lid3 "Grothendieck.comp" sigma1
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return (GMorphism r2 sigma1' ind1 mor startMorId)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder else return $ GMorphism (CompComorphism r1 r2)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sigma1 ind1 mor startMorId
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder dom (GMorphism r sigma ind _mor _) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder G_sign (sourceLogic r) sigma ind
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder cod (GMorphism r (ExtSign _ _) _ mor _) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let lid2 = targetLogic r
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sig2 = cod mor
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder in G_sign lid2 (makeExtSign lid2 sig2) startSigId
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett isInclusion (GMorphism cid _ _ mor _) =
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett isInclusionComorphism cid && isInclusion mor
a731366827a80af216ce6bfd4aa6388260577791Andy Gimblett legal_mor (GMorphism r (ExtSign s _) _ mor _) = do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder legal_mor mor
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case maybeResult $ map_sign r s of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just (sigma', _) | sigma' == cod mor -> return ()
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder _ -> fail "legal_mor.GMorphism2"
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | Embedding of homogeneous signature morphisms as Grothendieck sig mors
842ae753ab848a8508c4832ab64296b929167a97Christian MaedergEmbed2 :: G_sign -> G_morphism -> GMorphism
842ae753ab848a8508c4832ab64296b929167a97Christian MaedergEmbed2 (G_sign lid2 sig si) (G_morphism lid mor ind) =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let cid = mkIdComorphism lid (top_sublogic lid)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just sig1 = coerceSign lid2 (sourceLogic cid) "gEmbed2" sig
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder in GMorphism cid sig1 si mor ind
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | Embedding of homogeneous signature morphisms as Grothendieck sig mors
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedergEmbed :: G_morphism -> GMorphism
842ae753ab848a8508c4832ab64296b929167a97Christian MaedergEmbed (G_morphism lid mor ind) = let sig = dom mor in
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett GMorphism (mkIdComorphism lid (top_sublogic lid))
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett (makeExtSign lid sig) startSigId mor ind
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | Embedding of comorphisms as Grothendieck sig mors
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedergEmbedComorphism :: AnyComorphism -> G_sign -> Result GMorphism
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillygEmbedComorphism (Comorphism cid) (G_sign lid sig ind) = do
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sig'@(ExtSign s _) <- coerceSign lid (sourceLogic cid) "gEmbedComorphism" sig
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (sigTar, _) <- map_sign cid s
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder return (GMorphism cid sig' ind (ide sigTar) startMorId)
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- | heterogeneous union of two Grothendieck signatures
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillygsigUnion :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillygsigUnion lg both gsig1@(G_sign lid1 (ExtSign sigma1 _) _)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder gsig2@(G_sign lid2 (ExtSign sigma2 _) _) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder if Logic lid1 == Logic lid2
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly then homogeneousGsigUnion both gsig1 gsig2
bba1e274cf727c39b4f1dd8970539a2bb967f20fLiam O'Reilly else do
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (Comorphism cid1, Comorphism cid2) <-
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly logicUnion lg (Logic lid1) (Logic lid2)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly let lidS1 = sourceLogic cid1
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder lidS2 = sourceLogic cid2
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder lidT1 = targetLogic cid1
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly lidT2 = targetLogic cid2
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sigma1' <- coercePlainSign lid1 lidS1 "Union of signaturesa" sigma1
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sigma2' <- coercePlainSign lid2 lidS2 "Union of signaturesb" sigma2
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (sigma1'', _) <- map_sign cid1 sigma1' -- where to put axioms???
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (sigma2'', _) <- map_sign cid2 sigma2' -- where to put axioms???
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sigma2''' <- coercePlainSign lidT2 lidT1 "Union of signaturesc" sigma2''
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sigma3 <- signature_union lidT1 sigma1'' sigma2'''
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder return $ G_sign lidT1 (ExtSign sigma3 $ symset_of lidT1
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly $ if both then sigma3 else sigma2''') startSigId
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- | homogeneous Union of two Grothendieck signatures
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'ReillyhomogeneousGsigUnion :: Bool -> G_sign -> G_sign -> Result G_sign
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederhomogeneousGsigUnion both (G_sign lid1 sigma1 _) (G_sign lid2 sigma2 _) = do
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sigma2'@(ExtSign sig2 _) <- coerceSign lid2 lid1 "Union of signatures" sigma2
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder sigma3@(ExtSign sig3 _) <- ext_signature_union lid1 sigma1 sigma2'
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly return $ G_sign lid1
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett (if both then sigma3 else ExtSign sig3 $ symset_of lid1 sig2)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder startSigId
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederhomGsigDiff :: G_sign -> G_sign -> Result G_sign
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederhomGsigDiff (G_sign lid1 (ExtSign s1 _) _) (G_sign lid2 (ExtSign s2 _) _) = do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder s3 <- coercePlainSign lid2 lid1 "hom differerence of signatures" s2
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett s4 <- signatureDiff lid1 s1 s3
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett return $ G_sign lid1 (makeExtSign lid1 s4) startSigId
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- | union of a list of Grothendieck signatures
842ae753ab848a8508c4832ab64296b929167a97Christian MaedergsigManyUnion :: LogicGraph -> [G_sign] -> Result G_sign
c679188b6762edb198e353f724e77c74aa64a7e4Andy GimblettgsigManyUnion _ [] =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fail "union of emtpy list of signatures"
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedergsigManyUnion lg (gsigma : gsigmas) =
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett foldM (gsigUnion lg True) gsigma gsigmas
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | homogeneous Union of a list of morphisms
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederhomogeneousMorManyUnion :: [G_morphism] -> Result G_morphism
842ae753ab848a8508c4832ab64296b929167a97Christian MaederhomogeneousMorManyUnion [] =
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett fail "homogeneous union of emtpy list of morphisms"
c679188b6762edb198e353f724e77c74aa64a7e4Andy GimbletthomogeneousMorManyUnion (gmor : gmors) =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder foldM ( \ (G_morphism lid2 mor2 _) (G_morphism lid1 mor1 _) -> do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder mor1' <- coerceMorphism lid1 lid2 "homogeneousMorManyUnion" mor1
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder mor <- morphism_union lid2 mor1' mor2
c679188b6762edb198e353f724e77c74aa64a7e4Andy Gimblett return (G_morphism lid2 mor startMorId)) gmor gmors
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | inclusion between two logics
c679188b6762edb198e353f724e77c74aa64a7e4Andy GimblettlogicInclusion :: LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederlogicInclusion logicGraph l1@(Logic lid1) (Logic lid2) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let ln1 = language_name lid1
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder ln2 = language_name lid2 in
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder if ln1 == ln2 then
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett return (idComorphism l1)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder else case Map.lookup (ln1, ln2) (inclusions logicGraph) of
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Just (Comorphism i) ->
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return (Comorphism i)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Nothing ->
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder fail ("No inclusion from " ++ ln1 ++ " to " ++ ln2 ++ " found")
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederupdateMorIndex :: MorId -> GMorphism -> GMorphism
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy GimblettupdateMorIndex i (GMorphism cid sign si mor _) = GMorphism cid sign si mor i
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett
5b5db1d788d5240070930175f1322dab56279f99Andy GimbletttoG_morphism :: GMorphism -> G_morphism
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedertoG_morphism (GMorphism cid _ _ mor i) = G_morphism (targetLogic cid) mor i
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedergSigCoerce :: LogicGraph -> G_sign -> AnyLogic
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder -> Result (G_sign, AnyComorphism)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettgSigCoerce lg g@(G_sign lid1 sigma1 _) l2@(Logic lid2) =
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett if Logic lid1 == Logic lid2
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett then return (g, idComorphism l2) else do
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett cmor@(Comorphism i) <- logicInclusion lg (Logic lid1) l2
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett ExtSign sigma1' sy <-
c909c215242232fe78ce335e677e6f22264a0ee9Christian Maeder coerceSign lid1 (sourceLogic i) "gSigCoerce of signature" sigma1
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett (sigma1'', _) <- map_sign i sigma1'
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett sys <- return . Set.unions . map (map_symbol i sigma1') $ Set.toList sy
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder let lid = targetLogic i
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder return (G_sign lid (ExtSign sigma1'' sys) startSigId, cmor)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder-- | inclusion morphism between two Grothendieck signatures
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederginclusion = inclusionAux True
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett
5b5db1d788d5240070930175f1322dab56279f99Andy GimblettinclusionAux :: Bool -> LogicGraph -> G_sign -> G_sign -> Result GMorphism
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian MaederinclusionAux guard lg (G_sign lid1 sigma1 ind) (G_sign lid2 sigma2 _) = do
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder Comorphism i <- logicInclusion lg (Logic lid1) (Logic lid2)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder ext1@(ExtSign sigma1' _) <-
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett coerceSign lid1 (sourceLogic i) "Inclusion of signatures" sigma1
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett (sigma1'', _) <- map_sign i sigma1'
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett ExtSign sigma2' _ <-
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett coerceSign lid2 (targetLogic i) "Inclusion of signatures" sigma2
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett mor <- (if guard then inclusion else subsig_inclusion)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (targetLogic i) sigma1'' sigma2'
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder return (GMorphism i ext1 ind mor startMorId)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
842ae753ab848a8508c4832ab64296b929167a97Christian MaedergenCompInclusion :: (G_sign -> G_sign -> Result GMorphism)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder -> GMorphism -> GMorphism -> Result GMorphism
842ae753ab848a8508c4832ab64296b929167a97Christian MaedergenCompInclusion f mor1 mor2 = do
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let sigma1 = cod mor1
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder sigma2 = dom mor2
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder incl <- f sigma1 sigma2
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder mor <- composeMorphisms mor1 incl
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder composeMorphisms mor mor2
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- | Composition of two Grothendieck signature morphisms
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettwith intermediate inclusion -}
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedercompInclusion :: LogicGraph -> GMorphism -> GMorphism -> Result GMorphism
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedercompInclusion = genCompInclusion . inclusionAux False
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- | Find all (composites of) comorphisms starting from a given logic
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederfindComorphismPaths :: LogicGraph -> G_sublogics -> [AnyComorphism]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederfindComorphismPaths lg (G_sublogics lid sub) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder nubOrd $ map fst $ iterateComp (0 :: Int) [(idc, [idc])]
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder where
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett idc = Comorphism (mkIdComorphism lid sub)
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly coMors = filter hasModelExpansion . Map.elems $ comorphisms lg
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett -- compute possible compositions, but only up to depth 4
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett iterateComp n l =
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett if n > 2 || l == newL then newL else iterateComp (n + 1) newL
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett where
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett newL = nubOrd $ l ++ concatMap extend l
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett -- extend comorphism list in all directions, but no cylces
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett extend (coMor, cmps) =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let addCoMor c =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder case compComorphism coMor c of
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett Nothing -> Nothing
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett Just c1 -> Just (c1, c : cmps)
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder in mapMaybe addCoMor $ filter (not . (`elem` cmps)) coMors
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder-- | graph representation of the logic graph
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillylogicGraph2Graph :: LogicGraph
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett -> Graph (G_sublogics,Maybe AnyComorphism) AnyComorphism
5b5db1d788d5240070930175f1322dab56279f99Andy GimblettlogicGraph2Graph lg =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let relevantMorphisms = filter hasModelExpansion . Map.elems $ comorphisms lg
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder in Graph {
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder neighbours = \(G_sublogics lid sl,c1) ->
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder let coerce c = forceCoerceSublogic lid (sourceLogic c)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder in Data.Maybe.catMaybes $
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder map (\(Comorphism c) -> maybe Nothing (\sl1 -> Just (Comorphism c,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (G_sublogics (targetLogic c) sl1, Just $ Comorphism c)))
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (mapSublogic c (coerce c sl))) $
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder filter (\(Comorphism c) -> Logic (sourceLogic c) == Logic lid
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder && isSubElem (coerce c sl) (sourceSublogic c)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder && (case c1 of Just (Comorphism c1') -> (show c1') /= (show c)
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder _ -> True)) relevantMorphisms,
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder weight = \(Comorphism c) -> if Logic (sourceLogic c) ==
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder 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
if Logic lid == Logic 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