ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder{- |

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederModule : $Header$

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2004

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder

eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian MaederMaintainer : till@tzi.de

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederStability : provisional

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederPortability : non-portable (overlapping instances, dynamics, existentials)

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder The Grothendieck logic is defined to be the

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder heterogeneous logic over the logic graph.

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder This will be the logic over which the data

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder structures and algorithms for specification in-the-large

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder are built.

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder References:

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder R. Diaconescu:

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder Grothendieck institutions

f353be6210f67ffd4a46967bba749afc968cee52Christian Maeder J. applied categorical structures 10, 2002, p. 383-402.

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder T. Mossakowski:

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder Heterogeneous development graphs and heterogeneous borrowing

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder Fossacs 2002, LNCS 2303, p. 326-341

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder

fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maeder T. Mossakowski: Foundations of heterogeneous specification

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder Submitted

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder

2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder T. Mossakowski:

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Relating CASL with Other Specification Languages:

d3bca27d616c5741d0b18776c8a0848ec31c87f4Christian Maeder the Institution Level

2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maeder Theoretical Computer Science 286, 2002, p. 367-475

f9a73de15ef09dbd6b391c7b1f695c79b4446fe2Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Todo:

f9a73de15ef09dbd6b391c7b1f695c79b4446fe2Christian Maeder

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder-}

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maedermodule Logic.Grothendieck where

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Logic.Logic

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Logic.Prover

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Logic.Comorphism

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Common.PrettyPrint

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport Common.Lib.Pretty

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport qualified Common.Lib.Map as Map

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederimport qualified Common.Lib.Set as Set

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederimport Common.Result

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maederimport Common.Id

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederimport Common.AS_Annotation

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederimport Common.ListUtils

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederimport Data.Dynamic

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maederimport Common.DynamicUtils

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederimport qualified Data.List as List

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport Data.Maybe

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederimport Control.Monad

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder------------------------------------------------------------------

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder--"Grothendieck" versions of the various parts of type class Logic

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder------------------------------------------------------------------

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder-- | Grothendieck basic specifications

cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maederdata G_basic_spec = forall lid sublogics

cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder basic_spec sentence symb_items symb_map_items

cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder sign morphism symbol raw_symbol proof_tree .

cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder Logic lid sublogics

cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder basic_spec sentence symb_items symb_map_items

cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder sign morphism symbol raw_symbol proof_tree =>

cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder G_basic_spec lid basic_spec

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederinstance Show G_basic_spec where

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder show (G_basic_spec _ s) = show s

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederinstance PrettyPrint G_basic_spec where

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder printText0 ga (G_basic_spec _ s) = printText0 ga s

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder-- | Grothendieck sentences

04dada28736b4a237745e92063d8bdd49a362debChristian Maederdata G_sentence = forall lid sublogics

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder basic_spec sentence symb_items symb_map_items

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder sign morphism symbol raw_symbol proof_tree .

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Logic lid sublogics

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder basic_spec sentence symb_items symb_map_items

ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder sign morphism symbol raw_symbol proof_tree =>

8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder G_sentence lid sentence

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinstance Show G_sentence where

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder show (G_sentence _ s) = show s

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | Grothendieck sentence lists

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederdata G_l_sentence_list = forall lid sublogics

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder basic_spec sentence symb_items symb_map_items

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder sign morphism symbol raw_symbol proof_tree .

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Logic lid sublogics

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder basic_spec sentence symb_items symb_map_items

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder sign morphism symbol raw_symbol proof_tree =>

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder G_l_sentence_list lid [Named sentence]

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinstance Show G_l_sentence_list where

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder show (G_l_sentence_list _ s) = show s

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinstance Eq G_l_sentence_list where

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder (G_l_sentence_list i1 nl1) == (G_l_sentence_list i2 nl2) =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder coerce i1 i2 nl1 == Just nl2

7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maedereq_G_l_sentence_set :: G_l_sentence_list -> G_l_sentence_list -> Bool

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maedereq_G_l_sentence_set (G_l_sentence_list i1 nl1) (G_l_sentence_list i2 nl2) =

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder case coerce i1 i2 nl1 of

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder Just nl1' -> Set.fromList nl1' == Set.fromList nl2

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder Nothing -> False

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder

f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder-- | Grothendieck signatures

f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maederdata G_sign = forall lid sublogics

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder basic_spec sentence symb_items symb_map_items

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder sign morphism symbol raw_symbol proof_tree .

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder Logic lid sublogics

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder basic_spec sentence symb_items symb_map_items

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder sign morphism symbol raw_symbol proof_tree =>

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder G_sign lid sign

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder

15c12a3ac049a4528da05b1017b78145f308aeb0Christian MaedertyconG_sign :: TyCon

15c12a3ac049a4528da05b1017b78145f308aeb0Christian MaedertyconG_sign = mkTyCon "Logic.Grothendieck.G_sign"

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederinstance Typeable G_sign where

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder typeOf _ = mkTyConApp tyconG_sign []

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederinstance Eq G_sign where

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder (G_sign i1 sigma1) == (G_sign i2 sigma2) =

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder coerce i1 i2 sigma1 == Just sigma2

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder-- | prefer a faster subsignature test if possible

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maederis_subgsign :: G_sign -> G_sign -> Bool

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maederis_subgsign (G_sign i1 sigma1) (G_sign i2 sigma2) =

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder maybe False (is_subsig i1 sigma1) $ coerce i2 i1 sigma2

f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder

e92ae8b45c138b6cf7db8b69e2d099d7f62f24f0Christian Maederinstance Show G_sign where

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder show (G_sign _ s) = show s

f9a73de15ef09dbd6b391c7b1f695c79b4446fe2Christian Maeder

ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maederinstance PrettyPrint G_sign where

ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder printText0 ga (G_sign _ s) = printText0 ga s

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederlangNameSig :: G_sign -> String

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederlangNameSig (G_sign lid _) = language_name lid

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder-- | Grothendieck signature lists

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederdata G_sign_list = forall lid sublogics

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder basic_spec sentence symb_items symb_map_items

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder sign morphism symbol raw_symbol proof_tree .

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder Logic lid sublogics

8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder basic_spec sentence symb_items symb_map_items

355a453397fa18360bbaeb0f1068ad6a299a1dffChristian Maeder sign morphism symbol raw_symbol proof_tree =>

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder G_sign_list lid [sign]

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder-- | Grothendieck extended signatures

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maederdata G_ext_sign = forall lid sublogics

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder basic_spec sentence symb_items symb_map_items

8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder sign morphism symbol raw_symbol proof_tree .

8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder Logic lid sublogics

355a453397fa18360bbaeb0f1068ad6a299a1dffChristian Maeder basic_spec sentence symb_items symb_map_items

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder sign morphism symbol raw_symbol proof_tree =>

355a453397fa18360bbaeb0f1068ad6a299a1dffChristian Maeder G_ext_sign lid sign (Set.Set symbol)

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder

355a453397fa18360bbaeb0f1068ad6a299a1dffChristian MaedertyconG_ext_sign :: TyCon

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian MaedertyconG_ext_sign = mkTyCon "Logic.Grothendieck.G_ext_sign"

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maederinstance Typeable G_ext_sign where

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder typeOf _ = mkTyConApp tyconG_ext_sign []

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederinstance Eq G_ext_sign where

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder (G_ext_sign i1 sigma1 sys1) == (G_ext_sign i2 sigma2 sys2) =

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder coerce i1 i2 sigma1 == Just sigma2

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder && coerce i1 i2 sys1 == Just sys2

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederinstance Show G_ext_sign where

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder show (G_ext_sign _ s _) = show s

20fe556546c9277cf017931a07d90add61f199d9Christian Maeder

20fe556546c9277cf017931a07d90add61f199d9Christian Maederinstance PrettyPrint G_ext_sign where

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder printText0 ga (G_ext_sign _ s _) = printText0 ga s

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaederlangNameExtSig :: G_ext_sign -> String

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaederlangNameExtSig (G_ext_sign lid _ _) = language_name lid

20fe556546c9277cf017931a07d90add61f199d9Christian Maeder

20fe556546c9277cf017931a07d90add61f199d9Christian Maeder-- | Grothendieck theories

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederdata G_theory = forall lid sublogics

20fe556546c9277cf017931a07d90add61f199d9Christian Maeder basic_spec sentence symb_items symb_map_items

20fe556546c9277cf017931a07d90add61f199d9Christian Maeder sign morphism symbol raw_symbol proof_tree .

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Logic lid sublogics

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder basic_spec sentence symb_items symb_map_items

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder sign morphism symbol raw_symbol proof_tree =>

f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder G_theory lid sign [Named sentence]

f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder-- | compute sublogic of a theory

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedersublogicOfTh :: G_theory -> G_sublogics

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedersublogicOfTh (G_theory lid sigma sens) =

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let sub = foldr Logic.Logic.join

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (min_sublogic_sign lid sigma)

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder (map (min_sublogic_sentence lid . sentence) sens)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder in G_sublogics lid sub

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- | simplify a theory (throw away qualifications)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedersimplifyTh :: G_theory -> G_theory

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaedersimplifyTh (G_theory lid sigma sens) =

f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder G_theory lid sigma (map (mapNamed (simplify_sen lid sigma)) sens)

f626b1acbe874a48143a6f8d6246bf9d7a055ffbChristian Maeder

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder-- | Grothendieck symbols

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederdata G_symbol = forall lid sublogics

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder basic_spec sentence symb_items symb_map_items

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder sign morphism symbol raw_symbol proof_tree .

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder Logic lid sublogics

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder basic_spec sentence symb_items symb_map_items

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sign morphism symbol raw_symbol proof_tree =>

20fe556546c9277cf017931a07d90add61f199d9Christian Maeder G_symbol lid symbol

278de8173a1b7b7f6299f7c804135d14560176daChristian Maeder

278de8173a1b7b7f6299f7c804135d14560176daChristian Maederinstance Show G_symbol where

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder show (G_symbol _ s) = show s

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederinstance Eq G_symbol where

278de8173a1b7b7f6299f7c804135d14560176daChristian Maeder (G_symbol i1 s1) == (G_symbol i2 s2) =

c9b711a46e5138b2742727817c8071960e673073Christian Maeder coerce i1 i2 s1 == Just s2

c9b711a46e5138b2742727817c8071960e673073Christian Maeder

c9b711a46e5138b2742727817c8071960e673073Christian Maeder-- | Grothendieck symbol lists

c9b711a46e5138b2742727817c8071960e673073Christian Maederdata G_symb_items_list = forall lid sublogics

c9b711a46e5138b2742727817c8071960e673073Christian Maeder basic_spec sentence symb_items symb_map_items

c9b711a46e5138b2742727817c8071960e673073Christian Maeder sign morphism symbol raw_symbol proof_tree .

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

G_symb_items_list lid [symb_items]

instance Show G_symb_items_list where

show (G_symb_items_list _ l) = show l

instance PrettyPrint G_symb_items_list where

printText0 ga (G_symb_items_list _ l) =

fsep $ punctuate comma $ map (printText0 ga) l

instance Eq G_symb_items_list where

(G_symb_items_list i1 s1) == (G_symb_items_list i2 s2) =

coerce i1 i2 s1 == Just s2

-- | Grothendieck symbol maps

data G_symb_map_items_list = forall lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree .

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

G_symb_map_items_list lid [symb_map_items]

instance Show G_symb_map_items_list where

show (G_symb_map_items_list _ l) = show l

instance PrettyPrint G_symb_map_items_list where

printText0 ga (G_symb_map_items_list _ l) =

fsep $ punctuate comma $ map (printText0 ga) l

instance Eq G_symb_map_items_list where

(G_symb_map_items_list i1 s1) == (G_symb_map_items_list i2 s2) =

coerce i1 i2 s1 == Just s2

-- | Grothendieck diagrams

data G_diagram = forall lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree .

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

G_diagram lid (Diagram sign morphism)

-- | Grothendieck sublogics

data G_sublogics = forall lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree .

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

G_sublogics lid sublogics

tyconG_sublogics :: TyCon

tyconG_sublogics = mkTyCon "Logic.Grothendieck.G_sublogics"

instance Typeable G_sublogics where

typeOf _ = mkTyConApp tyconG_sublogics []

instance Show G_sublogics where

show (G_sublogics lid sub) = case sublogic_names lid sub of

[] -> error "show G_sublogics"

h : _ -> show lid ++ "." ++ h

instance Eq G_sublogics where

(G_sublogics lid1 l1) == (G_sublogics lid2 l2) =

coerce lid1 lid2 l1 == Just l2

instance Ord G_sublogics where

compare (G_sublogics lid1 l1) (G_sublogics lid2 l2) =

case coerce lid1 lid2 l2 of

Just l2' -> compare l1 l2' {-if l1==l2' then EQ

else if l1 <<= l2' then LT

else GT-}

Nothing -> error "Attempt to compare sublogics of different logics"

-- | Homogeneous Grothendieck signature morphisms

data G_morphism = forall lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree .

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

G_morphism lid morphism

instance Show G_morphism where

show (G_morphism _ l) = show l

----------------------------------------------------------------

-- Existential types for the logic graph

----------------------------------------------------------------

-- | Existential type for comorphisms

data AnyComorphism = forall cid lid1 sublogics1

basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2

basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .

Comorphism cid

lid1 sublogics1 basic_spec1 sentence1

symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2 basic_spec2 sentence2

symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>

Comorphism cid

instance Eq AnyComorphism where

Comorphism cid1 == Comorphism cid2 =

constituents cid1 == constituents cid2

-- need to be refined, using comorphism translations !!!

instance Show AnyComorphism where

show (Comorphism cid) =

language_name cid

++" : "++language_name (sourceLogic cid)

++" -> "++language_name (targetLogic cid)

tyconAnyComorphism :: TyCon

tyconAnyComorphism = mkTyCon "Logic.Grothendieck.AnyComorphism"

instance Typeable AnyComorphism where

typeOf _ = mkTyConApp tyconAnyComorphism []

-- | Test whether a comporphism is the identity

isIdComorphism :: AnyComorphism -> Bool

isIdComorphism (Comorphism cid) =

constituents cid == []

-- | Compose comorphisms

compComorphism :: Monad m => AnyComorphism -> AnyComorphism -> m AnyComorphism

compComorphism cm1@(Comorphism cid1) cm2@(Comorphism cid2) =

case coerce (targetLogic cid1) (sourceLogic cid2) (targetSublogic cid1) of

Just sl1 ->

if sl1 <= sourceSublogic cid2

then case (isIdComorphism cm1,isIdComorphism cm2) of

(True,_) -> return cm2

(_,True) -> return cm1

_ -> return $ Comorphism (CompComorphism cid1 cid2)

else fail ("Sublogic mismatch in composition of "++language_name cid1++

" and "++language_name cid2)

Nothing -> fail ("Logic mismatch in composition of "++language_name cid1++

" and "++language_name cid2)

-- | Logic graph

data LogicGraph = LogicGraph {

logics :: Map.Map String AnyLogic,

comorphisms :: Map.Map String AnyComorphism,

inclusions :: Map.Map (String,String) AnyComorphism

}

emptyLogicGraph :: LogicGraph

emptyLogicGraph = LogicGraph Map.empty Map.empty Map.empty

-- | find a logic in a logic graph

lookupLogic :: Monad m => String -> String -> LogicGraph -> m AnyLogic

lookupLogic error_prefix logname logicGraph =

case Map.lookup logname (logics logicGraph) of

Nothing -> fail (error_prefix++" in LogicGraph logic \""

++logname++"\" unknown")

Just lid -> return lid

-- | find a comorphism in a logic graph

lookupComorphism :: Monad m => String -> LogicGraph -> m AnyComorphism

lookupComorphism coname logicGraph = do

let nameList = splitBy ';' coname

cs <- sequence $ map lookupN nameList

case cs of

c:cs1 -> foldM compComorphism c cs1

_ -> fail ("Illgegal comorphism name: "++coname)

where

lookupN name =

case name of

'i':'d':'_':logic -> do

let mainLogic = takeWhile (/= '.') logic

l <- maybe (fail ("Cannot find Logic "++mainLogic)) return

$ Map.lookup mainLogic (logics logicGraph)

case l of

Logic lid ->

return $ Comorphism $ IdComorphism lid (top_sublogic lid)

_ -> maybe (fail ("Cannot find logic comorphism "++name)) return

$ Map.lookup name (comorphisms logicGraph)

-- | auxiliary existential type needed for composition of comorphisms

data AnyComorphismAux lid1 sublogics1

basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2

basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =

forall cid .

Comorphism cid

lid1 sublogics1 basic_spec1 sentence1

symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2 basic_spec2 sentence2

symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>

ComorphismAux cid lid1 lid2 sign1 morphism2

tyconAnyComorphismAux :: TyCon

tyconAnyComorphismAux = mkTyCon "Logic.Grothendieck.AnyComorphismAux"

instance Typeable (AnyComorphismAux lid1 sublogics1

basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2

basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2)

where typeOf _ = mkTyConApp tyconG_sign []

instance Show (AnyComorphismAux lid1 sublogics1

basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2

basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2)

where show _ = "<AnyComorphismAux>"

------------------------------------------------------------------

-- The Grothendieck signature category

------------------------------------------------------------------

-- | Grothendieck signature morphisms

data GMorphism = forall cid lid1 sublogics1

basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2

basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .

Comorphism cid

lid1 sublogics1 basic_spec1 sentence1

symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2 basic_spec2 sentence2

symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>

GMorphism cid sign1 morphism2

instance Eq GMorphism where

GMorphism cid1 sigma1 mor1 == GMorphism cid2 sigma2 mor2

= Comorphism cid1 == Comorphism cid2 &&

coerce cid1 cid1 (sigma1, mor1) == Just (sigma2, mor2)

data Grothendieck = Grothendieck deriving Show

instance Language Grothendieck

instance Show GMorphism where

show (GMorphism cid s m) = show cid ++ "(" ++ show s ++ ")" ++ show m

instance PrettyPrint GMorphism where

printText0 ga (GMorphism cid s m) =

ptext (show cid)

<+> -- ptext ":" <+> ptext (show (sourceLogic cid)) <+>

-- ptext "->" <+> ptext (show (targetLogic cid)) <+>

ptext "(" <+> printText0 ga s <+> ptext ")"

$$

printText0 ga m

instance Category Grothendieck G_sign GMorphism where

ide _ (G_sign lid sigma) =

GMorphism (IdComorphism lid (top_sublogic lid)) sigma (ide lid sigma)

comp _

(GMorphism r1 sigma1 mor1)

(GMorphism r2 _sigma2 mor2) =

do let lid1 = sourceLogic r1

lid2 = targetLogic r1

lid3 = sourceLogic r2

lid4 = targetLogic r2

ComorphismAux r1' _ _ sigma1' mor1' <-

(coerce lid2 lid3 $ ComorphismAux r1 lid1 lid2 sigma1 mor1)

mor1'' <- map_morphism r2 mor1'

mor <- comp lid4 mor1'' mor2

return (GMorphism (CompComorphism r1' r2) sigma1' mor)

dom _ (GMorphism r sigma _mor) =

G_sign (sourceLogic r) sigma

cod _ (GMorphism r _sigma mor) =

G_sign lid2 (cod lid2 mor)

where lid2 = targetLogic r

legal_obj _ (G_sign lid sigma) = legal_obj lid sigma

legal_mor _ (GMorphism r sigma mor) =

legal_mor lid2 mor &&

case map_sign r sigma of

Just (sigma',_) -> sigma' == cod lid2 mor

Nothing -> False

where lid2 = targetLogic r

-- | Embedding of homogeneous signature morphisms as Grothendieck sig mors

gEmbed :: G_morphism -> GMorphism

gEmbed (G_morphism lid mor) =

GMorphism (IdComorphism lid (top_sublogic lid)) (dom lid mor) mor

-- | heterogeneous union of two Grothendieck signatures

-- the left signature determines the result logic

gsigLeftUnion :: LogicGraph -> G_sign -> G_sign -> Result G_sign

gsigLeftUnion lg gsig1@(G_sign lid1 sigma1) gsig2@(G_sign lid2 sigma2) =

if language_name lid1 == language_name lid2

then homogeneousGsigUnion gsig1 gsig2

else do

GMorphism incl _ _ <- ginclusion lg

(G_sign lid2 (empty_signature lid2))

(G_sign lid1 (empty_signature lid1))

let lid1' = targetLogic incl

lid2' = sourceLogic incl

sigma1' <- coerce lid1 lid1' sigma1

sigma2' <- coerce lid2 lid2' sigma2

(sigma2'',_) <- maybeToMonad "gsigLeftUnion: signature mapping failed"

(map_sign incl sigma2') -- where to put axioms???

sigma3 <- signature_union lid1' sigma1' sigma2''

return (G_sign lid1' sigma3)

-- | homogeneous Union of two Grothendieck signatures

homogeneousGsigUnion :: G_sign -> G_sign -> Result G_sign

homogeneousGsigUnion (G_sign lid1 sigma1) (G_sign lid2 sigma2) = do

sigma2' <- coerce lid2 lid1 sigma2

sigma3 <- signature_union lid1 sigma1 sigma2'

return (G_sign lid1 sigma3)

-- | homogeneous Union of a list of Grothendieck signatures

homogeneousGsigManyUnion :: [G_sign] -> Result G_sign

homogeneousGsigManyUnion [] =

fail "homogeneous union of emtpy list of signatures"

homogeneousGsigManyUnion (G_sign lid sigma : gsigmas) = do

sigmas <- let coerce_lid (G_sign lid1 sigma1) =

coerce lid lid1 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 :: [G_morphism] -> Result G_morphism

homogeneousMorManyUnion [] =

fail "homogeneous union of emtpy list of morphisms"

homogeneousMorManyUnion (G_morphism lid mor : gmors) = do

mors <- let coerce_lid (G_morphism lid1 mor1) =

coerce lid lid1 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 between two logics

logicInclusion :: LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism

logicInclusion logicGraph (Logic lid1) (Logic lid2) =

let ln1 = language_name lid1

ln2 = language_name lid2 in

if ln1==ln2 then

return (Comorphism (IdComorphism lid1 (top_sublogic lid1)))

else case Map.lookup (ln1,ln2) (inclusions logicGraph) of

Just (Comorphism i) ->

return (Comorphism i)

Nothing ->

fail ("No inclusion from "++ln1++" to "++ln2++" found")

-- | inclusion morphism between two Grothendieck signatures

ginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism

ginclusion logicGraph (G_sign lid1 sigma1) (G_sign lid2 sigma2) = do

Comorphism i <- logicInclusion logicGraph (Logic lid1) (Logic lid2)

sigma1' <- rcoerce lid1 (sourceLogic i) (newPos "u" 0 0) sigma1

(sigma1'',_) <- maybeToResult (newPos "w" 0 0)

"ginclusion: signature map failed"

(map_sign i sigma1')

sigma2' <- rcoerce lid2 (targetLogic i) (newPos "v" 0 0) sigma2

mor <- inclusion (targetLogic i) sigma1'' sigma2'

return (GMorphism i sigma1' mor)

-- | Composition of two Grothendieck signature morphisms

-- | with itermediate inclusion

compInclusion :: LogicGraph -> GMorphism -> GMorphism -> Result GMorphism

compInclusion lg mor1 mor2 = do

incl <- ginclusion lg (cod Grothendieck mor1) (dom Grothendieck mor2)

mor <- maybeToResult nullPos

"compInclusion: composition falied" $ comp Grothendieck mor1 incl

maybeToResult nullPos

"compInclusion: composition falied" $ comp Grothendieck mor mor2

-- | Composition of two Grothendieck signature morphisms

-- | with itermediate homogeneous inclusion

compHomInclusion :: GMorphism -> GMorphism -> Result GMorphism

compHomInclusion mor1 mor2 = compInclusion emptyLogicGraph mor1 mor2

-- | Translation of a G_l_sentence_list along a GMorphism

translateG_l_sentence_list :: GMorphism -> G_l_sentence_list

-> Result G_l_sentence_list

translateG_l_sentence_list (GMorphism cid sign1 morphism2)

(G_l_sentence_list lid sens) = do

let tlid = targetLogic cid

--(sigma2,_) <- map_sign cid sign1

sens' <- coerce lid (sourceLogic cid) sens

let sens'' = mapMaybe (mapNamedM (map_sentence cid sign1)) $ sens'

sens''' <- sequence $ map (mapNamedM (map_sen tlid morphism2)) $ sens''

return (G_l_sentence_list tlid sens''')

-- | Join two G_l_sentence_list's

joinG_l_sentence_list :: G_l_sentence_list -> G_l_sentence_list

-> Maybe G_l_sentence_list

joinG_l_sentence_list (G_l_sentence_list lid1 sens1)

(G_l_sentence_list lid2 sens2) = do

sens2' <- coerce lid1 lid2 sens2

return (G_l_sentence_list lid1 (sens1++sens2'))

-- | Flatten a list of G_l_sentence_list's

flatG_l_sentence_list :: [G_l_sentence_list] -> Maybe G_l_sentence_list

flatG_l_sentence_list [] = Nothing

flatG_l_sentence_list (gl:gls) = foldM joinG_l_sentence_list gl gls

-- | Find all (composites of) comorphisms starting from a given logic

findComorphismPaths :: LogicGraph -> G_sublogics -> [AnyComorphism]

findComorphismPaths lg (G_sublogics lid sub) =

List.nub $ map fst $ iterateComp (0::Int) [(idc,[idc])]

where

idc = Comorphism (IdComorphism lid sub)

coMors = Map.elems $ comorphisms lg

-- compute possible compositions, but only up to depth 5

iterateComp n l = -- (l::[(AnyComorphism,[AnyComorphism])]) =

if n>5 || l==newL then newL else iterateComp (n+1) newL

where

newL = List.nub (l ++ (concat (map extend l)))

-- extend comorphism list in all directions, but no cylces

extend (coMor,comps) =

let addCoMor c =

case compComorphism coMor c of

Nothing -> Nothing

Just c1 -> Just (c1,c:comps)

in catMaybes $ map addCoMor $ filter (not . (`elem` comps)) $ coMors

------------------------------------------------------------------

-- Provers

------------------------------------------------------------------

-- | provers and consistency checkers for specific logics

data G_prover = forall lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree .

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

G_prover lid (Prover sign sentence proof_tree symbol)

| forall lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree .

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

G_cons_checker lid (ConsChecker (TheoryMorphism sign sentence morphism))

------------------------------------------------------------------

-- Coercion

------------------------------------------------------------------

-- | coerce a theory into a "different" logic

coerceTheory :: forall lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree .

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

lid -> G_theory -> Result (sign, [Named sentence])

coerceTheory lid (G_theory lid2 sign2 sens2)

= rcoerce lid lid2 nullPos (sign2,sens2)