Grothendieck.hs revision 7f34aa86290d0260e0bc00c64e4548ae4e941c5e
e83ed59502a681713982f25c559aae77a4145734Christian Maeder-- needs ghc -fglasgow-exts
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski{- HetCATS/Grothendieck.hs
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder $Id$
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu Till Mossakowski
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder The Grothendieck logic is defined to be the
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder heterogeneous logic over the logic graph.
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder This will be the logic over which the data
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder structures and algorithms for specification in-the-large
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski are built.
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder References:
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder R. Diaconescu:
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Grothendieck institutions
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder J. applied categorical structures 10, 2002, p. 383-402.
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder T. Mossakowski:
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Heterogeneous development graphs and heterogeneous borrowing
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Fossacs 2002, LNCS 2303, p. 326-341
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder T. Mossakowski: Foundations of heterogeneous specification
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Submitted
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder T. Mossakowski:
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Relating CASL with Other Specification Languages:
e83ed59502a681713982f25c559aae77a4145734Christian Maeder the Institution Level
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Theoretical Computer Science 286, 2002, p. 367-475
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Todo:
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
e83ed59502a681713982f25c559aae77a4145734Christian Maedermodule Grothendieck where
e83ed59502a681713982f25c559aae77a4145734Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Logic
e83ed59502a681713982f25c559aae77a4145734Christian Maederimport LogicRepr
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport PrettyPrint
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Pretty
e83ed59502a681713982f25c559aae77a4145734Christian Maederimport PPUtils (fsep_latex, comma_latex)
e83ed59502a681713982f25c559aae77a4145734Christian Maederimport Result
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Id
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder------------------------------------------------------------------
e83ed59502a681713982f25c559aae77a4145734Christian Maeder--"Grothendieck" versions of the various parts of type class Logic
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder------------------------------------------------------------------
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
e83ed59502a681713982f25c559aae77a4145734Christian Maederdata G_basic_spec = forall lid sublogics
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec sentence symb_items symb_map_items
e83ed59502a681713982f25c559aae77a4145734Christian Maeder sign morphism symbol raw_symbol proof_tree .
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Logic lid sublogics
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec sentence symb_items symb_map_items
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign morphism symbol raw_symbol proof_tree =>
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder G_basic_spec lid basic_spec
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Show G_basic_spec where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder show (G_basic_spec _ s) = show s
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance PrettyPrint G_basic_spec where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder printText0 ga (G_basic_spec _ s) = printText0 ga s
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder printLatex0 ga (G_basic_spec _ s) = printLatex0 ga s
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Eq G_basic_spec where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (G_basic_spec i1 s1) == (G_basic_spec i2 s2) =
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder coerce i1 i2 s1 == Just s2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederdata G_sentence = forall lid sublogics
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder basic_spec sentence symb_items symb_map_items
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign morphism symbol raw_symbol proof_tree .
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder Logic lid sublogics
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder basic_spec sentence symb_items symb_map_items
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder sign morphism symbol raw_symbol proof_tree =>
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder G_sentence lid sentence
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder
35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maederinstance Show G_sentence where
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski show (G_sentence _ s) = show s
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederdata G_l_sentence_list = forall lid sublogics
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder basic_spec sentence symb_items symb_map_items
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign morphism symbol raw_symbol proof_tree .
07b1bf56f3a486f26d69514d05b73100abb25a0eChristian Maeder Logic lid sublogics
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec sentence symb_items symb_map_items
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign morphism symbol raw_symbol proof_tree =>
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder G_l_sentence lid [(String,sentence)]
e83ed59502a681713982f25c559aae77a4145734Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maederdata G_sign = forall lid sublogics
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder basic_spec sentence symb_items symb_map_items
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign morphism symbol raw_symbol proof_tree .
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Logic lid sublogics
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec sentence symb_items symb_map_items
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski G_sign lid sign
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski
e33e3b425e953236b4617870f995d263ac35b883Christian Maederinstance Eq G_sign where
58564afba8f0bb6b57783c4b440d0b666edf5f67Christian Maeder (G_sign i1 sigma1) == (G_sign i2 sigma2) =
e83ed59502a681713982f25c559aae77a4145734Christian Maeder coerce i1 i2 sigma1 == Just sigma2
e33e3b425e953236b4617870f995d263ac35b883Christian Maeder
3a3bbc51abf804d91bc9d8e0f2ce745cfae4c9c7Christian Maederinstance Show G_sign where
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski show (G_sign _ s) = show s
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowskidata G_sign_list = forall lid sublogics
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder basic_spec sentence symb_items symb_map_items
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder sign morphism symbol raw_symbol proof_tree .
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder Logic lid sublogics
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder basic_spec sentence symb_items symb_map_items
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder sign morphism symbol raw_symbol proof_tree =>
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder G_sign_list lid [sign]
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maederdata G_symbol = forall lid sublogics
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder basic_spec sentence symb_items symb_map_items
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder sign morphism symbol raw_symbol proof_tree .
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder Logic lid sublogics
a8f68a4ea736953bbac7d06a8b4c0613e04b1d3bTill Mossakowski basic_spec sentence symb_items symb_map_items
a8f68a4ea736953bbac7d06a8b4c0613e04b1d3bTill Mossakowski sign morphism symbol raw_symbol proof_tree =>
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder G_symbol lid symbol
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maederinstance Show G_symbol where
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder show (G_symbol _ s) = show s
743178d5294deadc2ed15e56b5e58ca0e7101fe4Christian Maeder
72b8c0349a58cf0eb361cb5bb410d95a0372900acmaederinstance Eq G_symbol where
aa0f5bca984ed6ea99f01dffdb78885083a36d78cmaeder (G_symbol i1 s1) == (G_symbol i2 s2) =
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder coerce i1 i2 s1 == Just s2
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maederdata G_symb_items_list = forall lid sublogics
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder basic_spec sentence symb_items symb_map_items
743178d5294deadc2ed15e56b5e58ca0e7101fe4Christian Maeder sign morphism symbol raw_symbol proof_tree .
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder Logic lid sublogics
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder basic_spec sentence symb_items symb_map_items
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder sign morphism symbol raw_symbol proof_tree =>
f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder G_symb_items_list lid [symb_items]
743178d5294deadc2ed15e56b5e58ca0e7101fe4Christian Maeder
aa0f5bca984ed6ea99f01dffdb78885083a36d78cmaederinstance Show G_symb_items_list where
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski show (G_symb_items_list _ l) = show l
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maederinstance PrettyPrint G_symb_items_list where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder printText0 ga (G_symb_items_list _ l) =
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder fsep $ punctuate comma $ map (printText0 ga) l
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder printLatex0 ga (G_symb_items_list _ l) =
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder fsep_latex $ punctuate comma_latex $ map (printLatex0 ga) l
1865083b72c1307e9040d78c2743abd5a54ee260Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maederinstance Eq G_symb_items_list where
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder (G_symb_items_list i1 s1) == (G_symb_items_list i2 s2) =
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder coerce i1 i2 s1 == Just s2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederdata G_symb_map_items_list = forall lid sublogics
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maeder basic_spec sentence symb_items symb_map_items
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign morphism symbol raw_symbol proof_tree .
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder Logic lid sublogics
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder basic_spec sentence symb_items symb_map_items
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign morphism symbol raw_symbol proof_tree =>
e83ed59502a681713982f25c559aae77a4145734Christian Maeder G_symb_map_items_list lid [symb_map_items]
e83ed59502a681713982f25c559aae77a4145734Christian Maeder
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maederinstance Show G_symb_map_items_list where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder show (G_symb_map_items_list _ l) = show l
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maederinstance PrettyPrint G_symb_map_items_list where
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder printText0 ga (G_symb_map_items_list _ l) =
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder fsep $ punctuate comma $ map (printText0 ga) l
dc427a9450cd7b463717a2255c804afa47a54365Christian Maeder
dc427a9450cd7b463717a2255c804afa47a54365Christian Maeder printLatex0 ga (G_symb_map_items_list _ l) =
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder fsep_latex $ punctuate comma_latex $ map (printLatex0 ga) l
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
dc427a9450cd7b463717a2255c804afa47a54365Christian Maederinstance Eq G_symb_map_items_list where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (G_symb_map_items_list i1 s1) == (G_symb_map_items_list i2 s2) =
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder coerce i1 i2 s1 == Just s2
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maederdata G_diagram = forall lid sublogics
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder basic_spec sentence symb_items symb_map_items
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign morphism symbol raw_symbol proof_tree .
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Logic lid sublogics
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder basic_spec sentence symb_items symb_map_items
e83ed59502a681713982f25c559aae77a4145734Christian Maeder sign morphism symbol raw_symbol proof_tree =>
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder G_diagram lid (Diagram sign morphism)
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederdata G_sublogics = forall lid sublogics
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder basic_spec sentence symb_items symb_map_items
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign morphism symbol raw_symbol proof_tree .
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder Logic lid sublogics
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec sentence symb_items symb_map_items
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign morphism symbol raw_symbol proof_tree =>
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder G_sublogics lid sublogics
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Show G_sublogics where
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder show (G_sublogics _ l) = show l
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maederdata G_morphism = forall lid sublogics
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder basic_spec sentence symb_items symb_map_items
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign morphism symbol raw_symbol proof_tree .
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder Logic lid sublogics
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder basic_spec sentence symb_items symb_map_items
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign morphism symbol raw_symbol proof_tree =>
e83ed59502a681713982f25c559aae77a4145734Christian Maeder G_morphism lid morphism
e83ed59502a681713982f25c559aae77a4145734Christian Maeder
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maederinstance Show G_morphism where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder show (G_morphism _ l) = show l
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder----------------------------------------------------------------
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder-- Existential types for the logic graph
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder----------------------------------------------------------------
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maederdata AnyLogic = forall lid sublogics
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder basic_spec sentence symb_items symb_map_items
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign morphism symbol raw_symbol proof_tree .
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder Logic lid sublogics
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder basic_spec sentence symb_items symb_map_items
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign morphism symbol raw_symbol proof_tree =>
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Logic lid
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
585094c4284ed39eb8024cc1178c823c403200faChristian Maederdata AnyRepresentation = forall lid1 sublogics1
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e83ed59502a681713982f25c559aae77a4145734Christian Maeder lid2 sublogics2
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (Logic lid1 sublogics1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Logic lid2 sublogics2
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski basic_spec2 sentence2 symb_items2 symb_map_items2
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder Repr(LogicRepr lid1 sublogics1 basic_spec1 sentence1
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder symb_items1 symb_map_items1
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder lid2 sublogics2 basic_spec2 sentence2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder symb_items2 symb_map_items2
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder
e83ed59502a681713982f25c559aae77a4145734Christian Maeder
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maedertype LogicGraph = ([AnyLogic],[AnyRepresentation])
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder{- This does not work due to needed ordering:
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maederinstance Functor Set where
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder fmap = mapSet
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maederinstance Monad Set where
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder return = unitSet
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder m >>= k = unionManySets (setToList (fmap k m))
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder-}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder
e83ed59502a681713982f25c559aae77a4145734Christian Maeder------------------------------------------------------------------
7325bbe03797fd413af504fb3fac109b2c652a7bChristian Maeder-- The Grothendieck signature category
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder------------------------------------------------------------------
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder-- composition in diagrammatic order
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedercomp_anyrepr :: AnyRepresentation -> AnyRepresentation -> Maybe AnyRepresentation
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maedercomp_anyrepr
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder (Repr (r1 :: LogicRepr lid1 sublogics1 basic_spec1 sentence1
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maeder symb_items1 symb_map_items1
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
7325bbe03797fd413af504fb3fac109b2c652a7bChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2))
585094c4284ed39eb8024cc1178c823c403200faChristian Maeder (Repr (r2 :: LogicRepr lid3 sublogics3 basic_spec3 sentence3
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder symb_items3 symb_map_items3
e83ed59502a681713982f25c559aae77a4145734Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski sign4 morphism4 symbol4 raw_symbol4 proof_tree4)) =
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder do r3 <- coerce (target r1) (source r2) r2 :: Maybe(
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder LogicRepr lid2 sublogics2 basic_spec2 sentence2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder symb_items2 symb_map_items2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e83ed59502a681713982f25c559aae77a4145734Christian Maeder lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4)
7e4157a70efe2acab30dbe5079bba6db90923785Christian Maeder r4 <- comp_repr r1 r3
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski return (Repr r4)
e5298e75aafb75fe522b24c0ff1919f581980335Christian Maeder
e5298e75aafb75fe522b24c0ff1919f581980335Christian Maederdata GMorphism = forall lid1 sublogics1
e5298e75aafb75fe522b24c0ff1919f581980335Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
7fc5ecf094ed7ad8f6dd878e719ef95c0b2a5da0Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e5298e75aafb75fe522b24c0ff1919f581980335Christian Maeder lid2 sublogics2
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
90bf4bf40789422552e566b73738ba5efae144c3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
e5298e75aafb75fe522b24c0ff1919f581980335Christian Maeder (Logic lid1 sublogics1
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1
e83ed59502a681713982f25c559aae77a4145734Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Logic lid2 sublogics2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder GMorphism lid1 lid2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (LogicRepr lid1 sublogics1 basic_spec1 sentence1
1320edfb75af112d509a6ce0a4c02425da7fed4dChristian Maeder symb_items1 symb_map_items1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
1320edfb75af112d509a6ce0a4c02425da7fed4dChristian Maeder lid2 sublogics2 basic_spec2 sentence2
1600a2e47d5ed599df94d20411f0767fb6d68587Christian Maeder symb_items2 symb_map_items2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign1 morphism2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
57c51f0673511217c416090de812b779612e7551Christian Maederinstance Eq GMorphism where
(GMorphism lid1 lid2 r1 sigma1 mor1) == (GMorphism lid3 lid4 r2 sigma2 mor2)
= maybe False id
(do r2' <- coerce lid1 lid3 r2
sigma2' <- coerce lid1 lid3 sigma2
mor2' <- coerce lid2 lid4 mor2
return (r1 == r2' && sigma1 == sigma2' && mor1==mor2'))
data Grothendieck = Grothendieck deriving Show
instance Language Grothendieck where
instance Show GMorphism where
show (GMorphism _ _ r s m) = show r ++ "(" ++ show s ++ ")" ++ show m
instance Category Grothendieck G_sign GMorphism where
ide _ (G_sign lid sigma) =
GMorphism lid lid (id_repr lid) sigma (ide lid sigma)
comp _
(GMorphism lid1 lid2 r1 sigma1 mor1)
(GMorphism lid3 lid4 r2 _sigma2 mor2) =
do r2' <- coerce lid2 lid3 r2
r3 <- comp_repr r1 r2'
mor1' <- coerce lid2 lid3 mor1
mor1'' <- map_morphism r2 mor1'
mor <- comp lid4 mor2 mor1''
return (GMorphism lid1 lid4 r3 sigma1 mor)
dom _ (GMorphism lid1 _lid2 _r sigma _mor) = G_sign lid1 sigma
cod _ (GMorphism _lid1 lid2 _r _sigma mor) = G_sign lid2 (cod lid2 mor)
legal_obj _ (G_sign lid sigma) = legal_obj lid sigma
legal_mor _ (GMorphism _lid1 lid2 r sigma mor) =
legal_mor lid2 mor && case map_sign r sigma of
Just (sigma',_) -> sigma' == cod lid2 mor
Nothing -> False
gEmbed :: G_morphism -> GMorphism
gEmbed (G_morphism lid mor) =
GMorphism lid lid (id_repr lid) (dom lid mor) mor
-- homogeneous Union of two Grothendieck signatures
homogeneousGsigUnion :: Pos -> G_sign -> G_sign -> Result G_sign
homogeneousGsigUnion pos (G_sign lid1 sigma1) (G_sign lid2 sigma2) = do
sigma2' <- rcoerce lid2 lid1 pos sigma2
sigma3 <- signature_union lid1 sigma1 sigma2'
return (G_sign lid1 sigma3)
-- homogeneous Union of a list of Grothendieck signatures
homogeneousGsigManyUnion :: Pos -> [G_sign] -> Result G_sign
homogeneousGsigManyUnion pos [] =
fatal_error "homogeneous union of emtpy list of signatures" pos
homogeneousGsigManyUnion pos (G_sign lid sigma : gsigmas) = do
sigmas <- let coerce_lid (G_sign lid1 sigma1) =
rcoerce lid lid1 pos sigma1
in sequence (map coerce_lid gsigmas)
bigSigma <- let sig_union s1 s2 = do
s1' <- s1
signature_union lid s1' s2
in foldl sig_union (return sigma) sigmas
return (G_sign lid bigSigma)
-- homogeneous Union of a list of morphisms
homogeneousMorManyUnion :: Pos -> [G_morphism] -> Result G_morphism
homogeneousMorManyUnion pos [] =
fatal_error "homogeneous union of emtpy list of morphisms" pos
homogeneousMorManyUnion pos (G_morphism lid mor : gmors) = do
mors <- let coerce_lid (G_morphism lid1 mor1) =
rcoerce lid lid1 pos mor1
in sequence (map coerce_lid gmors)
bigMor <- let mor_union s1 s2 = do
s1' <- s1
morphism_union lid s1' s2
in foldl mor_union (return mor) mors
return (G_morphism lid bigMor)
inclusion :: G_sign -> G_sign -> GMorphism
inclusion (G_sign _lid1 _sigma1) (G_sign _lid2 _sigma2) = error "inclusion"