Grothendieck.hs revision 2eb84fc82d3ffa9116bc471fda3742bd9e5a24bb
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder-- needs ghc -fglasgow-exts
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Till Mossakowski
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder The Grothendieck logic is defined to be the
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder heterogeneous logic over the logic graph.
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder This will be the logic over which the data
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder structures and algorithms for specification in-the-large
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder R. Diaconescu:
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Grothendieck institutions
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder J. applied categorical structures 10, 2002, p. 383-402.
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich T. Mossakowski:
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich Heterogeneous development graphs and heterogeneous borrowing
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich Fossacs 2002, LNCS 2303, p. 326-341
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder T. Mossakowski: Foundations of heterogeneous specification
01e383014b555bbcf639c0ca60c5810b3eff83c0Christian Maeder T. Mossakowski:
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski Relating CASL with Other Specification Languages:
9dac90ec2be2a72e03893095461960d483fe2fc2Christian Maeder the Institution Level
5e5d3e82af3bc2834f8718a52d9f45da80220273Dominik Luecke Theoretical Computer Science 286, 2002, p. 367-475
8410667510a76409aca9bb24ff0eda0420088274Christian Maederimport Common.PPUtils (fsep_latex, comma_latex)
4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder------------------------------------------------------------------
8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder--"Grothendieck" versions of the various parts of type class Logic
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich------------------------------------------------------------------
55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian Maederdata G_basic_spec = forall lid sublogics
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder basic_spec sentence symb_items symb_map_items
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder sign morphism symbol raw_symbol proof_tree .
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder Logic lid sublogics
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder basic_spec sentence symb_items symb_map_items
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder sign morphism symbol raw_symbol proof_tree =>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder G_basic_spec lid basic_spec
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maederinstance Show G_basic_spec where
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder show (G_basic_spec _ s) = show s
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maederinstance PrettyPrint G_basic_spec where
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder printText0 ga (G_basic_spec _ s) = printText0 ga s
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder printLatex0 ga (G_basic_spec _ s) = printLatex0 ga s
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederinstance Eq G_basic_spec where
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder (G_basic_spec i1 s1) == (G_basic_spec i2 s2) =
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder coerce i1 i2 s1 == Just s2
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederdata G_sentence = forall lid sublogics
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder basic_spec sentence symb_items symb_map_items
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder sign morphism symbol raw_symbol proof_tree .
c2fcc35abb03cf0b4ca4b050efeb10827f38c322Christian Maeder Logic lid sublogics
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder basic_spec sentence symb_items symb_map_items
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder sign morphism symbol raw_symbol proof_tree =>
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder G_sentence lid sentence
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maederinstance Show G_sentence where
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder show (G_sentence _ s) = show s
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettichdata G_l_sentence_list = forall lid sublogics
f8e1a1eca871a26a535a4ee7d51902ba94b1db1eChristian Maeder basic_spec sentence symb_items symb_map_items
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder sign morphism symbol raw_symbol proof_tree .
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder Logic lid sublogics
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder basic_spec sentence symb_items symb_map_items
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder sign morphism symbol raw_symbol proof_tree =>
8a28707e9155465c6f2236a06eac6580a65c7025Christian Maeder G_l_sentence lid [(String,sentence)]
797ccd67cb8ae127be097cd43448801b673e3b69Christian Maederdata G_sign = forall lid sublogics
797ccd67cb8ae127be097cd43448801b673e3b69Christian Maeder basic_spec sentence symb_items symb_map_items
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder sign morphism symbol raw_symbol proof_tree .
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder Logic lid sublogics
498aa48bdb931ab50990d3b74318a5db2312186cChristian Maeder basic_spec sentence symb_items symb_map_items
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder sign morphism symbol raw_symbol proof_tree =>
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder G_sign lid sign
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederinstance Typeable G_sign where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder typeOf _ = mkAppTy (mkTyCon "G_sign") []
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederinstance Eq G_sign where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (G_sign i1 sigma1) == (G_sign i2 sigma2) =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder coerce i1 i2 sigma1 == Just sigma2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinstance Show G_sign where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder show (G_sign _ s) = show s
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederdata G_sign_list = forall lid sublogics
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder basic_spec sentence symb_items symb_map_items
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder sign morphism symbol raw_symbol proof_tree .
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Logic lid sublogics
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder basic_spec sentence symb_items symb_map_items
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder sign morphism symbol raw_symbol proof_tree =>
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder G_sign_list lid [sign]
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maederdata G_symbol = forall lid sublogics
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder basic_spec sentence symb_items symb_map_items
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder sign morphism symbol raw_symbol proof_tree .
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder Logic lid sublogics
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder basic_spec sentence symb_items symb_map_items
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder sign morphism symbol raw_symbol proof_tree =>
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder G_symbol lid symbol
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederinstance Show G_symbol where
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder show (G_symbol _ s) = show s
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederinstance Eq G_symbol where
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder (G_symbol i1 s1) == (G_symbol i2 s2) =
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder coerce i1 i2 s1 == Just s2
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederdata G_symb_items_list = forall lid sublogics
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder basic_spec sentence symb_items symb_map_items
a9b59eb2ce961014974276cdae0e9df4419bd212Christian Maeder sign morphism symbol raw_symbol proof_tree .
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Logic lid sublogics
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder basic_spec sentence symb_items symb_map_items
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder sign morphism symbol raw_symbol proof_tree =>
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder G_symb_items_list lid [symb_items]
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederinstance Show G_symb_items_list where
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian 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) =
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder fsep $ punctuate comma $ map (printText0 ga) l
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder printLatex0 ga (G_symb_items_list _ l) =
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder fsep_latex $ punctuate comma_latex $ map (printLatex0 ga) l
4017ebc0f692820736d796af3110c3b3018c108aChristian Maederinstance Eq G_symb_items_list where
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder (G_symb_items_list i1 s1) == (G_symb_items_list i2 s2) =
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder coerce i1 i2 s1 == Just s2
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederdata G_symb_map_items_list = forall lid sublogics
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder basic_spec sentence symb_items symb_map_items
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder sign morphism symbol raw_symbol proof_tree .
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Logic lid sublogics
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder basic_spec sentence symb_items symb_map_items
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder sign morphism symbol raw_symbol proof_tree =>
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder G_symb_map_items_list lid [symb_map_items]
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maederinstance Show G_symb_map_items_list where
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder show (G_symb_map_items_list _ l) = show l
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederinstance PrettyPrint G_symb_map_items_list where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder printText0 ga (G_symb_map_items_list _ l) =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder fsep $ punctuate comma $ map (printText0 ga) l
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder printLatex0 ga (G_symb_map_items_list _ l) =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder fsep_latex $ punctuate comma_latex $ map (printLatex0 ga) l
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederinstance Eq G_symb_map_items_list where
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (G_symb_map_items_list i1 s1) == (G_symb_map_items_list i2 s2) =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder coerce i1 i2 s1 == Just s2
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maederdata G_diagram = forall lid sublogics
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder basic_spec sentence symb_items symb_map_items
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder sign morphism symbol raw_symbol proof_tree .
e6d5dbbc3308f05197868806e0b860f4f53875f1Christian Maeder Logic lid sublogics
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder basic_spec sentence symb_items symb_map_items
06ba24fa9695b698437546276f37aa5e1924ad1bChristian Maeder sign morphism symbol raw_symbol proof_tree =>
06ba24fa9695b698437546276f37aa5e1924ad1bChristian Maeder G_diagram lid (Diagram sign morphism)
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maederdata G_sublogics = forall lid sublogics
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder basic_spec sentence symb_items symb_map_items
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder sign morphism symbol raw_symbol proof_tree .
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder Logic lid sublogics
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder basic_spec sentence symb_items symb_map_items
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder sign morphism symbol raw_symbol proof_tree =>
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder G_sublogics lid sublogics
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance Show G_sublogics where
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder show (G_sublogics _ l) = show l
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederdata G_morphism = forall lid sublogics
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder basic_spec sentence symb_items symb_map_items
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder sign morphism symbol raw_symbol proof_tree .
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Logic lid sublogics
42b12fba6830ada5057949f825fc27edf5574e5fChristian Maeder basic_spec sentence symb_items symb_map_items
42b12fba6830ada5057949f825fc27edf5574e5fChristian Maeder sign morphism symbol raw_symbol proof_tree =>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder G_morphism lid morphism
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinstance Show G_morphism where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder show (G_morphism _ l) = show l
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder----------------------------------------------------------------
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder-- Existential types for the logic graph
93f5b72fdb9ee734caa750b43dd79bbb590dcd73Christian Maeder----------------------------------------------------------------
328a85c807f2a95c3f147d10b05927eaf862ebebChristian Maederdata AnyLogic = forall lid sublogics
a6db617ca58eb6a0587b6366e913107dfecb71b5Heng Jiang basic_spec sentence symb_items symb_map_items
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett sign morphism symbol raw_symbol proof_tree .
c5f2c55174d98e1a4595e041ad4ce35a16be76fdChristian Maeder Logic lid sublogics
5b818f10e11fc79def1fdd5c8a080d64a6438d87Christian Maeder basic_spec sentence symb_items symb_map_items
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers sign morphism symbol raw_symbol proof_tree =>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederdata AnyRepresentation = forall lid1 sublogics1
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers lid2 sublogics2
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder (Logic lid1 sublogics1
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder Logic lid2 sublogics2
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder Repr(LogicRepr lid1 sublogics1 basic_spec1 sentence1
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder symb_items1 symb_map_items1
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder lid2 sublogics2 basic_spec2 sentence2
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder symb_items2 symb_map_items2
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maedertype LogicGraph = ([AnyLogic],[AnyRepresentation])
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder{- This does not work due to needed ordering:
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maederinstance Functor Set where
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maeder fmap = mapSet
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maederinstance Monad Set where
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder return = unitSet
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder m >>= k = unionManySets (setToList (fmap k m))
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder------------------------------------------------------------------
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- The Grothendieck signature category
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder------------------------------------------------------------------
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder-- composition in diagrammatic order
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maedercomp_anyrepr :: AnyRepresentation -> AnyRepresentation -> Maybe AnyRepresentation
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder (Repr (r1 :: LogicRepr lid1 sublogics1 basic_spec1 sentence1
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder symb_items1 symb_map_items1
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
ac34194a668399bb8ef238da77c3a09e93fb253bChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2))
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder (Repr (r2 :: LogicRepr lid3 sublogics3 basic_spec3 sentence3
4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maeder symb_items3 symb_map_items3
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4)) =
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder do r3 <- coerce (target r1) (source r2) r2 :: Maybe(
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder LogicRepr lid2 sublogics2 basic_spec2 sentence2
01e278bdd7dce13b9303ed3d79683d83c89d09f9Liam O'Reilly symb_items2 symb_map_items2
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
5ad5dffe06818a13e1632b1119fbca7881085fc1Dominik Luecke lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4)
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder r4 <- comp_repr r1 r3
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder return (Repr r4)
00ccf62b4570513e965eb156ab5916ec816c5d2bDominik Lueckedata GMorphism = forall lid1 sublogics1
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke basic_spec1 sentence1 symb_items1 symb_map_items1
05a206508bc898f87fe6ab6e069814df3c29d303Dominik Luecke sign1 morphism1 symbol1 raw_symbol1 proof_tree1
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder lid2 sublogics2
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski basic_spec2 sentence2 symb_items2 symb_map_items2
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (Logic lid1 sublogics1
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
8c812cd83569e973f10cf69a342424ceabc07af9Christian Maeder Logic lid2 sublogics2
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
1b3a2f98d1cd01fc9e0591f69507e20526727559Dominik Luecke sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich GMorphism lid1 lid2
a6db617ca58eb6a0587b6366e913107dfecb71b5Heng Jiang (LogicRepr lid1 sublogics1 basic_spec1 sentence1
e39a1626bee36d6ad13a2c0014a80ef179a65bcbChristian Maeder symb_items1 symb_map_items1
f8e1a1eca871a26a535a4ee7d51902ba94b1db1eChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
abf2487c3aece95c371ea89ac64319370dcb6483Klaus Luettich lid2 sublogics2 basic_spec2 sentence2
c70ef4c3b3a62764f715510c9fd67dde3acfe454Christian Maeder symb_items2 symb_map_items2
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder sign1 morphism2
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder | forall lid sublogics
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder basic_spec sentence symb_items symb_map_items
b9b960bc75e34658e70c4a0231dbc6a6e7373f2dChristian Maeder sign morphism symbol raw_symbol proof_tree .
18a4d5cb6828f080db9c5f9551785c5151027271Christian Maeder Logic lid sublogics
846d851fc0c2c49e949763cd3407634ba0f726c0Christian Maeder basic_spec sentence symb_items symb_map_items
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder sign morphism symbol raw_symbol proof_tree =>
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder GMHomInclusion lid sign sign
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski | GMHetInclusion G_sign G_sign
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maederinstance Eq GMorphism where
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder (GMorphism lid1 lid2 r1 sigma1 mor1) == (GMorphism lid3 lid4 r2 sigma2 mor2)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder = maybe False id
70731e5459a18fc473bdc962ca94d1c12de974afChristian Maeder (do r2' <- coerce lid1 lid3 r2
edd1b7f4720bc2eea51fa0685417e1e4f3be4915Klaus Luettich sigma2' <- coerce lid1 lid3 sigma2
7809fb14d290d257ed6d46a2dd563227e227fcf3Christian Maeder mor2' <- coerce lid2 lid4 mor2
63e50b4c36074d5fb9de872c4007b688b4bce534Christian Maeder return (r1 == r2' && sigma1 == sigma2' && mor1==mor2'))
e059476130210dbb1896e753eb0a5e8c4f219f4aChristian Maederdata Grothendieck = Grothendieck deriving Show
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederinstance Language Grothendieck where
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maederinstance Show GMorphism where
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder show (GMorphism _ _ r s m) = show r ++ "(" ++ show s ++ ")" ++ show m
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinstance Category Grothendieck G_sign GMorphism where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ide _ (G_sign lid sigma) =
8d401657e07a01e10400265f508f75353a9fba4cChristian Maeder GMorphism lid lid (id_repr lid) sigma (ide lid sigma)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (GMorphism lid1 lid2 r1 sigma1 mor1)
6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maeder (GMorphism lid3 lid4 r2 _sigma2 mor2) =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder do r2' <- coerce lid2 lid3 r2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder r3 <- comp_repr r1 r2'
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich mor1' <- coerce lid2 lid3 mor1
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maeder mor1'' <- map_morphism r2 mor1'
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder mor <- comp lid4 mor2 mor1''
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder return (GMorphism lid1 lid4 r3 sigma1 mor)
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder dom _ (GMorphism lid1 _lid2 _r sigma _mor) = G_sign lid1 sigma
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder cod _ (GMorphism _lid1 lid2 _r _sigma mor) = G_sign lid2 (cod lid2 mor)
6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maeder legal_obj _ (G_sign lid sigma) = legal_obj lid sigma
dbe752ee940baae7f9f231f29c62284bb0f90a25Christian Maeder legal_mor _ (GMorphism _lid1 lid2 r sigma mor) =
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke legal_mor lid2 mor && case map_sign r sigma of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just (sigma',_) -> sigma' == cod lid2 mor
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke Nothing -> False
53818ced114da21321063fff307aa41c1ab31dd3Achim MahnkegEmbed :: G_morphism -> GMorphism
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedergEmbed (G_morphism lid mor) =
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder GMorphism lid lid (id_repr lid) (dom lid mor) mor
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich-- homogeneous Union of two Grothendieck signatures
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaederhomogeneousGsigUnion :: Pos -> G_sign -> G_sign -> Result G_sign
368c26b8ad68a4b2c42963626087667000c2eebfChristian MaederhomogeneousGsigUnion pos (G_sign lid1 sigma1) (G_sign lid2 sigma2) = do
368c26b8ad68a4b2c42963626087667000c2eebfChristian Maeder sigma2' <- rcoerce lid2 lid1 pos sigma2
368c26b8ad68a4b2c42963626087667000c2eebfChristian Maeder sigma3 <- signature_union lid1 sigma1 sigma2'
f443a57f2a8e0ca3daa7431b0c89a18ba52c337aChristian Maeder return (G_sign lid1 sigma3)
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder-- homogeneous Union of a list of Grothendieck signatures
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian MaederhomogeneousGsigManyUnion :: Pos -> [G_sign] -> Result G_sign
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till MossakowskihomogeneousGsigManyUnion pos [] =
7c99e334446bb97120e30e967baeeddfdd1278deKlaus Luettich fatal_error "homogeneous union of emtpy list of signatures" pos
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian MaederhomogeneousGsigManyUnion pos (G_sign lid sigma : gsigmas) = do
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder sigmas <- let coerce_lid (G_sign lid1 sigma1) =
6d549a835ffd3a11c3ed74e0f8fda30fda6a9528Christian Maeder rcoerce lid lid1 pos sigma1
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder in sequence (map coerce_lid gsigmas)
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder bigSigma <- let sig_union s1 s2 = do
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder signature_union lid s1' s2
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder in foldl sig_union (return sigma) sigmas
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder return (G_sign lid bigSigma)
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder-- homogeneous Union of a list of morphisms
27785f379d6810811b4e6d23feab18845fde9a98Christian MaederhomogeneousMorManyUnion :: Pos -> [G_morphism] -> Result G_morphism
b886e9e5db2098d0112cc4f70aeba232962939ddChristian MaederhomogeneousMorManyUnion pos [] =
c4451dc7da4a15726ba96179aecf046a5df5cae1Christian Maeder fatal_error "homogeneous union of emtpy list of morphisms" pos
c4451dc7da4a15726ba96179aecf046a5df5cae1Christian MaederhomogeneousMorManyUnion pos (G_morphism lid mor : gmors) = do
c4451dc7da4a15726ba96179aecf046a5df5cae1Christian Maeder mors <- let coerce_lid (G_morphism lid1 mor1) =
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder rcoerce lid lid1 pos mor1
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder in sequence (map coerce_lid gmors)
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder bigMor <- let mor_union s1 s2 = do
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder morphism_union lid s1' s2
33d042fe6a9eb27a4c48f840b80838f3e7d98e34Christian Maeder in foldl mor_union (return mor) mors
83394c6b6e6de128e71b67c9251ed7a84485d082Christian Maeder return (G_morphism lid bigMor)
fa21fba9ceb1ddf7b3efd54731a12ed8750191d8Christian Maederinclusion :: G_sign -> G_sign -> GMorphism
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederinclusion (G_sign _lid1 _sigma1) (G_sign _lid2 _sigma2) = error "inclusion"