Grothendieck.hs revision 3b4439aa37e4229ad6e83d46bd303c2799784c80
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder-- needs ghc -fglasgow-exts
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Till Mossakowski
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder The Grothendieck logic is defined to be the
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder heterogeneous logic over the logic graph.
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder This will be the logic over which the data
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder structures and algorithms for specification in-the-large
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder R. Diaconescu:
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Grothendieck institutions
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder J. applied categorical structures 10, 2002, p. 383-402.
a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maeder T. Mossakowski:
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder Heterogeneous development graphs and heterogeneous borrowing
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich Fossacs 2002, LNCS 2303, p. 326-341
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder T. Mossakowski: Foundations of heterogeneous specification
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder T. Mossakowski:
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich Relating CASL with Other Specification Languages:
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder the Institution Level
74eed04be26f549d2f7ca35c370e1c03879b28b1Christian Maeder Theoretical Computer Science 286, 2002, p. 367-475
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maedermodule Grothendieck where
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport LogicRepr
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maederimport PrettyPrint
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederimport PPUtils (fsep_latex, comma_latex)
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder------------------------------------------------------------------
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder--"Grothendieck" versions of the various parts of type class Logic
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder------------------------------------------------------------------
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maederdata G_basic_spec = forall lid sublogics
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder basic_spec sentence symb_items symb_map_items
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder sign morphism symbol raw_symbol .
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder Logic lid sublogics
05a62e84edac8c64de04f8349dee418598d216b9Christian Maeder basic_spec sentence symb_items symb_map_items
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maeder sign morphism symbol raw_symbol =>
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder G_basic_spec lid basic_spec
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederinstance Show G_basic_spec where
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder show (G_basic_spec _ s) = show s
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederinstance PrettyPrint G_basic_spec where
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder printText0 ga (G_basic_spec _ s) = printText0 ga s
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder printLatex0 ga (G_basic_spec _ s) = printLatex0 ga s
b5da047a9a875dec3f968b6c0df96af326f90fa9Alexis Tsogiasinstance Eq G_basic_spec where
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder (G_basic_spec i1 s1) == (G_basic_spec i2 s2) =
6a2dad705deefd1b7a7e09b84fd2d75f2213be47Christian Maeder coerce i1 i2 s1 == Just s2
363939beade943a02b31004cea09dec34fa8a6d9Christian Maederdata G_sentence = forall lid sublogics
014dc30f64ec25e4790cca987d4d1e6635430510Christian Maeder basic_spec sentence symb_items symb_map_items
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich sign morphism symbol raw_symbol .
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian Maeder Logic lid sublogics
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian Maeder basic_spec sentence symb_items symb_map_items
feca1d35123d8c31aee238c9ce79947b0bf65494Christian Maeder sign morphism symbol raw_symbol =>
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder G_sentence lid sentence
c8012b9719c73f08418af7a0b4ba28fa1d200631Christian Maederinstance Show G_sentence where
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder show (G_sentence _ s) = show s
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederdata G_l_sentence_list = forall lid sublogics
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder basic_spec sentence symb_items symb_map_items
23ffcc44ca8612feccbd8fda63fa5be7ab5f9dc3Christian Maeder sign morphism symbol raw_symbol .
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Logic lid sublogics
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder basic_spec sentence symb_items symb_map_items
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder sign morphism symbol raw_symbol =>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder G_l_sentence lid [(String,sentence)]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederdata G_sign = forall lid sublogics
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder basic_spec sentence symb_items symb_map_items
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder sign morphism symbol raw_symbol .
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Logic lid sublogics
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder basic_spec sentence symb_items symb_map_items
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder sign morphism symbol raw_symbol =>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder G_sign lid sign
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinstance Eq G_sign where
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (G_sign i1 sigma1) == (G_sign i2 sigma2) =
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder coerce i1 i2 sigma1 == Just sigma2
2d130d212db7208777ca896a7ecad619a8944971Christian Maederinstance Show G_sign where
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder show (G_sign _ s) = show s
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maederdata G_sign_list = forall lid sublogics
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder basic_spec sentence symb_items symb_map_items
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder sign morphism symbol raw_symbol .
b363eb04791e7f735633b9b4088502c2bc50ebfcChristian Maeder Logic lid sublogics
a42fbfe7becf0eae2d624123eb0db73a794593f0Christian Maeder basic_spec sentence symb_items symb_map_items
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maeder sign morphism symbol raw_symbol =>
1cd4f6541984962658add5cfaa9f28a93879881bChristian Maeder G_sign_list lid [sign]
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederdata G_symbol = forall lid sublogics
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder basic_spec sentence symb_items symb_map_items
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder sign morphism symbol raw_symbol .
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Logic lid sublogics
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder basic_spec sentence symb_items symb_map_items
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder sign morphism symbol raw_symbol =>
a9b59eb2ce961014974276cdae0e9df4419bd212Christian Maeder G_symbol lid symbol
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederinstance Show G_symbol where
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder show (G_symbol _ s) = show s
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederinstance Eq G_symbol where
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder (G_symbol i1 s1) == (G_symbol i2 s2) =
dc679edd4ca027663212afdf00926ae2ce19b555Christian Maeder coerce i1 i2 s1 == Just s2
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederdata G_symb_items_list = forall lid sublogics
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder basic_spec sentence symb_items symb_map_items
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder sign morphism symbol raw_symbol .
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Logic lid sublogics
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder basic_spec sentence symb_items symb_map_items
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder sign morphism symbol raw_symbol =>
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder G_symb_items_list lid [symb_items]
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettichinstance Show G_symb_items_list where
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder show (G_symb_items_list _ l) = show l
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinstance PrettyPrint G_symb_items_list where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder printText0 ga (G_symb_items_list _ l) =
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder fsep $ punctuate comma $ map (printText0 ga) l
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder printLatex0 ga (G_symb_items_list _ l) =
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder fsep_latex $ punctuate comma_latex $ map (printLatex0 ga) l
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maederinstance Eq G_symb_items_list where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (G_symb_items_list i1 s1) == (G_symb_items_list i2 s2) =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder coerce i1 i2 s1 == Just s2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederdata G_symb_map_items_list = forall lid sublogics
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder basic_spec sentence symb_items symb_map_items
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder sign morphism symbol raw_symbol .
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Logic lid sublogics
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder basic_spec sentence symb_items symb_map_items
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder sign morphism symbol raw_symbol =>
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder G_symb_map_items_list lid [symb_map_items]
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maederinstance Show G_symb_map_items_list where
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder show (G_symb_map_items_list _ l) = show l
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maederinstance PrettyPrint G_symb_map_items_list where
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder printText0 ga (G_symb_map_items_list _ l) =
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder fsep $ punctuate comma $ map (printText0 ga) l
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maeder printLatex0 ga (G_symb_map_items_list _ l) =
eb74267cf39e4e95f9eeb5c765f4c8dac33971b4Christian Maeder fsep_latex $ punctuate comma_latex $ map (printLatex0 ga) l
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederinstance Eq G_symb_map_items_list where
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder (G_symb_map_items_list i1 s1) == (G_symb_map_items_list i2 s2) =
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder coerce i1 i2 s1 == Just s2
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederdata G_diagram = forall lid sublogics
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder basic_spec sentence symb_items symb_map_items
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder sign morphism symbol raw_symbol .
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder Logic lid sublogics
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder basic_spec sentence symb_items symb_map_items
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder sign morphism symbol raw_symbol =>
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder G_diagram lid (Diagram sign morphism)
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maederdata G_sublogics = forall lid sublogics
b2ac5a92cf36382e8deea5661c1964566caf72b3Christian Maeder basic_spec sentence symb_items symb_map_items
6cd33d6101fb1b93baa6d86fac158af18a115108Christian Maeder sign morphism symbol raw_symbol .
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Logic lid sublogics
10883d13973c46cac98964b66ace7a52b2d059abChristian Maeder basic_spec sentence symb_items symb_map_items
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder sign morphism symbol raw_symbol =>
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder G_sublogics lid sublogics
0e5b095a19790411e5352fa7cf57cb0388e70472Christian Maederdata G_morphism = forall lid sublogics
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder basic_spec sentence symb_items symb_map_items
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder sign morphism symbol raw_symbol .
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder Logic lid sublogics
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder basic_spec sentence symb_items symb_map_items
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder sign morphism symbol raw_symbol =>
f1a913f880e409e7327b5deae95738b5448379a1Christian Maeder G_morphism lid morphism
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder----------------------------------------------------------------
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder-- Existential types for the logic graph
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder----------------------------------------------------------------
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maederdata AnyLogic = forall lid sublogics
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder basic_spec sentence symb_items symb_map_items
328a85c807f2a95c3f147d10b05927eaf862ebebChristian Maeder sign morphism symbol raw_symbol .
a6db617ca58eb6a0587b6366e913107dfecb71b5Heng Jiang Logic lid sublogics
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett basic_spec sentence symb_items symb_map_items
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder sign morphism symbol raw_symbol =>
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maederdata AnyRepresentation = forall lid1 sublogics1
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers basic_spec1 sentence1 symb_items1 symb_map_items1
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder sign1 morphism1 symbol1 raw_symbol1
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder lid2 sublogics2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder sign2 morphism2 symbol2 raw_symbol2 .
d6697ad2479099b816203fd2c36f593c72c73c76Christian Maeder (Logic lid1 sublogics1
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder sign1 morphism1 symbol1 raw_symbol1,
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder Logic lid2 sublogics2
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers basic_spec2 sentence2 symb_items2 symb_map_items2
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder sign2 morphism2 symbol2 raw_symbol2) =>
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder Repr(LogicRepr lid1 sublogics1 basic_spec1 sentence1
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder symb_items1 symb_map_items1
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder sign1 morphism1 symbol1 raw_symbol1
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder lid2 sublogics2 basic_spec2 sentence2
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder symb_items2 symb_map_items2
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder sign2 morphism2 symbol2 raw_symbol2)
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maedertype LogicGraph = ([AnyLogic],[AnyRepresentation])
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder{- This does not work due to needed ordering:
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maederinstance Functor Set where
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder fmap = mapSet
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maederinstance Monad Set where
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder return = unitSet
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder m >>= k = unionManySets (setToList (fmap k m))
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder------------------------------------------------------------------
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- The Grothendieck signature category
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder------------------------------------------------------------------
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder-- composition in diagrammatic order
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maedercomp_anyrepr :: AnyRepresentation -> AnyRepresentation -> Maybe AnyRepresentation
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maeder (Repr (r1 :: LogicRepr lid1 sublogics1 basic_spec1 sentence1
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder symb_items1 symb_map_items1
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder sign1 morphism1 symbol1 raw_symbol1
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder sign2 morphism2 symbol2 raw_symbol2))
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder (Repr (r2 :: LogicRepr lid3 sublogics3 basic_spec3 sentence3
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder symb_items3 symb_map_items3
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder sign3 morphism3 symbol3 raw_symbol3
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder sign4 morphism4 symbol4 raw_symbol4)) =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder do r3 <- coerce (target r1) (source r2) r2 :: Maybe(
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder LogicRepr lid2 sublogics2 basic_spec2 sentence2
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder symb_items2 symb_map_items2
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder sign2 morphism2 symbol2 raw_symbol2
254df6f22d01eacf7c57b85729e0445747b630d9Christian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder sign4 morphism4 symbol4 raw_symbol4)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder r4 <- comp_repr r1 r3
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder return (Repr r4)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederdata GMorphism = forall lid1 sublogics1
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder sign1 morphism1 symbol1 raw_symbol1
aded505f9b42cc38975559c2a5d175ae95de436bChristian Maeder lid2 sublogics2
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder sign2 morphism2 symbol2 raw_symbol2 .
4fc9de0da898448f1d3597ebbd8c04a066464c21Christian Maeder (Logic lid1 sublogics1
df5eb1b8e587946c9d072f4ee6ac7d001719b034Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder sign1 morphism1 symbol1 raw_symbol1,
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder Logic lid2 sublogics2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder sign2 morphism2 symbol2 raw_symbol2) =>
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder GMorphism lid1 lid2
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder (LogicRepr lid1 sublogics1 basic_spec1 sentence1
01e278bdd7dce13b9303ed3d79683d83c89d09f9Liam O'Reilly symb_items1 symb_map_items1
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder sign1 morphism1 symbol1 raw_symbol1
5ad5dffe06818a13e1632b1119fbca7881085fc1Dominik Luecke lid2 sublogics2 basic_spec2 sentence2
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder symb_items2 symb_map_items2
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder sign2 morphism2 symbol2 raw_symbol2)
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder sign1 morphism2
31d6d9286988dc31639d105841296759aeb743e0Jonathan von Schroederinstance Eq GMorphism where
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu (GMorphism lid1 lid2 r1 sigma1 mor1) == (GMorphism lid3 lid4 r2 sigma2 mor2)
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder = maybe False id
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder (do r2' <- coerce lid1 lid3 r2
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder sigma2' <- coerce lid1 lid3 sigma2
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder mor2' <- coerce lid2 lid4 mor2
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke return (r1 == r2' && sigma1 == sigma2' && mor1==mor2'))
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maederdata Grothendieck = Grothendieck deriving Show
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maederinstance Language Grothendieck where
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederinstance Category Grothendieck G_sign GMorphism where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ide _ (G_sign lid sigma) =
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder GMorphism lid lid (id_repr lid) sigma (ide lid sigma)
5afff1a0f62394414c33b06141175b3ab0b117a5Christian Maeder (GMorphism lid1 lid2 r1 sigma1 mor1)
5afff1a0f62394414c33b06141175b3ab0b117a5Christian Maeder (GMorphism lid3 lid4 r2 sigma2 mor2) =
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder do r2' <- coerce lid2 lid3 r2
1b3a2f98d1cd01fc9e0591f69507e20526727559Dominik Luecke r3 <- comp_repr r1 r2'
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich mor1' <- coerce lid2 lid3 mor1
247cc88aa55d0a7b6831767cd593ea885c6747a0Christian Maeder mor1'' <- map_morphism r2 mor1'
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder mor <- comp lid4 mor2 mor1''
f8e1a1eca871a26a535a4ee7d51902ba94b1db1eChristian Maeder return (GMorphism lid1 lid4 r3 sigma1 mor)
ea3bff3e547a1ac714d4db39c5efef95e02b2e7dChristian Maeder dom _ (GMorphism lid1 lid2 r sigma mor) = G_sign lid1 sigma
dd6f22b9dcff2695181b86372e4df03d5b96e92dKristina Sojakova cod _ (GMorphism lid1 lid2 r sigma mor) = G_sign lid2 (cod lid2 mor)
005e0f0c6b0cc898003b03801158c208f3071fc5Kristina Sojakova legal_obj _ (G_sign lid sigma) = legal_obj lid sigma
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich legal_mor _ (GMorphism lid1 lid2 r sigma mor) =
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder legal_mor lid2 mor && case map_sign r sigma of
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder Just (sigma',_) -> sigma' == cod lid2 mor
23b4e542dca35852f58d1fb3f7d9078c1de5ab06Christian Maeder Nothing -> False
76b9b2974795a6fb31f242fd032de3ff66df6204Christian MaedergEmbed :: G_morphism -> GMorphism
8a78868bae2ec6838c87366c35c57e109154c51eChristian MaedergEmbed (G_morphism lid mor) =
624e6701e0deb7ac6c03c0cba0190fbc5033cf93Ewaryst Schulz GMorphism lid lid (id_repr lid) (dom lid mor) mor
6b75c206b317eb30a08d88a8f27e0295ffeb1546Christian Maeder-- homogeneous Union of two Grothendieck signatures
6b75c206b317eb30a08d88a8f27e0295ffeb1546Christian MaederhomogeneousGsigUnion :: Pos -> G_sign -> G_sign -> Result G_sign
48aa0645e25883048369afc02aac3f49b14a50daChristian MaederhomogeneousGsigUnion pos (G_sign lid1 sigma1) (G_sign lid2 sigma2) = do
01645eac73dbc789392674930adc5745c935f3a0Christian Maeder sigma2' <- rcoerce lid2 lid1 pos sigma2
01645eac73dbc789392674930adc5745c935f3a0Christian Maeder sigma3 <- signature_union lid1 sigma1 sigma2'
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder return (G_sign lid1 sigma3)
b5da047a9a875dec3f968b6c0df96af326f90fa9Alexis Tsogias-- homogeneous Union of a list of Grothendieck signatures
b5da047a9a875dec3f968b6c0df96af326f90fa9Alexis TsogiashomogeneousGsigManyUnion :: Pos -> [G_sign] -> Result G_sign
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederhomogeneousGsigManyUnion pos [] =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder fatal_error "homogeneous union of emtpy list of signatures" pos
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederhomogeneousGsigManyUnion pos (G_sign lid sigma : gsigmas) = do
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder sigmas <- let coerce_lid (G_sign lid1 sigma1) =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder rcoerce lid lid1 pos sigma1
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder in sequence (map coerce_lid gsigmas)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder bigSigma <- let sig_union s1 s2 = do
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder signature_union lid s1' s2
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder in foldl sig_union (return sigma) sigmas
7a3fe82695aa32657693e05712f84d7f81672f2eJonathan von Schroeder return (G_sign lid bigSigma)
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu-- homogeneous Union of a list of morphisms
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai CodescuhomogeneousMorManyUnion :: Pos -> [G_morphism] -> Result G_morphism
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai CodescuhomogeneousMorManyUnion pos [] =
1535e1d8c82db5f7e2402261983c4c2ef39f4f39Mihai Codescu fatal_error "homogeneous union of emtpy list of morphisms" pos
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederhomogeneousMorManyUnion pos (G_morphism lid mor : gmors) = do
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder mors <- let coerce_lid (G_morphism lid1 mor1) =
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder rcoerce lid lid1 pos mor1
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder in sequence (map coerce_lid gmors)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder bigMor <- let mor_union s1 s2 = do
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder morphism_union lid s1' s2
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder in foldl mor_union (return mor) mors
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maeder return (G_morphism lid bigMor)
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederinclusion :: G_sign -> G_sign -> GMorphism
456238178f89e5a3de2988ee6c8af924297d52d9Christian Maederinclusion (G_sign lid1 sigma1) (G_sign lid2 sigma2) = undefined