8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova{- |

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaModule : $Header$

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovaCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2004

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina SojakovaLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina Sojakova

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaMaintainer : till@tzi.de

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaStability : provisional

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaPortability : non-portable (overlapping instances, dynamics, existentials)

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova The Grothendieck logic is defined to be the

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova heterogeneous logic over the logic graph.

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova This will be the logic over which the data

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova structures and algorithms for specification in-the-large

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova are built.

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova References:

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova R. Diaconescu:

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Grothendieck institutions

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova J. applied categorical structures 10, 2002, p. 383-402.

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova T. Mossakowski:

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Heterogeneous development graphs and heterogeneous borrowing

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova Fossacs 2002, LNCS 2303, p. 326-341

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova T. Mossakowski: Foundations of heterogeneous specification

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova Submitted

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova T. Mossakowski:

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova Relating CASL with Other Specification Languages:

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova the Institution Level

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova Theoretical Computer Science 286, 2002, p. 367-475

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Todo:

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-}

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovamodule Logic.Grothendieck where

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaimport Logic.Logic

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Logic.Prover

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Logic.Comorphism

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.PrettyPrint

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.Lib.Pretty

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport qualified Common.Lib.Map as Map

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport qualified Common.Lib.Set as Set

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Common.Result

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.Id

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Common.AS_Annotation

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport Common.ListUtils

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Data.Dynamic

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaimport Common.DynamicUtils

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport qualified Data.List as List

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaimport Data.Maybe

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovaimport Control.Monad

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovaimport Common.Lib.Parsec.Pos -- for testing purposes

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova------------------------------------------------------------------

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova--"Grothendieck" versions of the various parts of type class Logic

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova------------------------------------------------------------------

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova-- | Grothendieck basic specifications

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovadata G_basic_spec = forall lid sublogics

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova basic_spec sentence symb_items symb_map_items

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova sign morphism symbol raw_symbol proof_tree .

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova Logic lid sublogics

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova basic_spec sentence symb_items symb_map_items

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova sign morphism symbol raw_symbol proof_tree =>

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova G_basic_spec lid basic_spec

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovainstance Show G_basic_spec where

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova show (G_basic_spec _ s) = show s

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakovainstance PrettyPrint G_basic_spec where

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova printText0 ga (G_basic_spec _ s) = printText0 ga s

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova-- | Grothendieck sentences

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata G_sentence = forall lid sublogics

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova basic_spec sentence symb_items symb_map_items

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova sign morphism symbol raw_symbol proof_tree .

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova Logic lid sublogics

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova basic_spec sentence symb_items symb_map_items

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova sign morphism symbol raw_symbol proof_tree =>

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova G_sentence lid sentence

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakovainstance Show G_sentence where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova show (G_sentence _ s) = show s

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova-- | Grothendieck sentence lists

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata G_l_sentence_list = forall lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Logic lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree =>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova G_l_sentence_list lid [Named sentence]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Show G_l_sentence_list where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova show (G_l_sentence_list _ s) = show s

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Eq G_l_sentence_list where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (G_l_sentence_list i1 nl1) == (G_l_sentence_list i2 nl2) =

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova coerce i1 i2 nl1 == Just nl2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaeq_G_l_sentence_set :: G_l_sentence_list -> G_l_sentence_list -> Bool

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakovaeq_G_l_sentence_set (G_l_sentence_list i1 nl1) (G_l_sentence_list i2 nl2) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case coerce i1 i2 nl1 of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just nl1' -> Set.fromList nl1' == Set.fromList nl2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> False

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | Grothendieck signatures

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata G_sign = forall lid sublogics

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Logic lid sublogics

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree =>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova G_sign lid sign

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovatyconG_sign :: TyCon

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovatyconG_sign = mkTyCon "Logic.Grothendieck.G_sign"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Typeable G_sign where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf _ = mkTyConApp tyconG_sign []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Eq G_sign where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (G_sign i1 sigma1) == (G_sign i2 sigma2) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova coerce i1 i2 sigma1 == Just sigma2

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | prefer a faster subsignature test if possible

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakovais_subgsign :: G_sign -> G_sign -> Bool

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovais_subgsign (G_sign i1 sigma1) (G_sign i2 sigma2) =

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova maybe False (is_subsig i1 sigma1) $ coerce i2 i1 sigma2

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovainstance Show G_sign where

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova show (G_sign _ s) = show s

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance PrettyPrint G_sign where

a3a6b6ebe9c2d1dc3554e44779dc7361a90e7617Kristina Sojakova printText0 ga (G_sign _ s) = printText0 ga s

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina SojakovalangNameSig :: G_sign -> String

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovalangNameSig (G_sign lid _) = language_name lid

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova-- | Grothendieck signature lists

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakovadata G_sign_list = forall lid sublogics

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova basic_spec sentence symb_items symb_map_items

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova sign morphism symbol raw_symbol proof_tree .

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova Logic lid sublogics

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova basic_spec sentence symb_items symb_map_items

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova sign morphism symbol raw_symbol proof_tree =>

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova G_sign_list lid [sign]

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova-- | Grothendieck extended signatures

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovadata G_ext_sign = forall lid sublogics

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova basic_spec sentence symb_items symb_map_items

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova sign morphism symbol raw_symbol proof_tree .

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova Logic lid sublogics

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova basic_spec sentence symb_items symb_map_items

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova sign morphism symbol raw_symbol proof_tree =>

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova G_ext_sign lid sign (Set.Set symbol)

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovatyconG_ext_sign :: TyCon

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatyconG_ext_sign = mkTyCon "Logic.Grothendieck.G_ext_sign"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Typeable G_ext_sign where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf _ = mkTyConApp tyconG_ext_sign []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Eq G_ext_sign where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (G_ext_sign i1 sigma1 sys1) == (G_ext_sign i2 sigma2 sys2) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova coerce i1 i2 sigma1 == Just sigma2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova && coerce i1 i2 sys1 == Just sys2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Show G_ext_sign where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova show (G_ext_sign _ s _) = show s

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance PrettyPrint G_ext_sign where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova printText0 ga (G_ext_sign _ s _) = printText0 ga s

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovalangNameExtSig :: G_ext_sign -> String

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovalangNameExtSig (G_ext_sign lid _ _) = language_name lid

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | Grothendieck theories

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata G_theory = forall lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Logic lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree =>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova G_theory lid sign [Named sentence]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | compute sublogic of a theory

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasublogicOfTh :: G_theory -> G_sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasublogicOfTh (G_theory lid sigma sens) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let sub = foldr Logic.Logic.join

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (min_sublogic_sign lid sigma)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (map (min_sublogic_sentence lid . sentence) sens)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in G_sublogics lid sub

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | simplify a theory (throw away qualifications)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasimplifyTh :: G_theory -> G_theory

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovasimplifyTh (G_theory lid sigma sens) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova G_theory lid sigma (map (mapNamed (simplify_sen lid sigma)) sens)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | Grothendieck symbols

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata G_symbol = forall lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Logic lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree =>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova G_symbol lid symbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Show G_symbol where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova show (G_symbol _ s) = show s

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Eq G_symbol where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (G_symbol i1 s1) == (G_symbol i2 s2) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova coerce i1 i2 s1 == Just s2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | Grothendieck symbol lists

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata G_symb_items_list = forall lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Logic lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree =>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova G_symb_items_list lid [symb_items]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Show G_symb_items_list where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova show (G_symb_items_list _ l) = show l

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance PrettyPrint G_symb_items_list where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova printText0 ga (G_symb_items_list _ l) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova fsep $ punctuate comma $ map (printText0 ga) l

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Eq G_symb_items_list where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (G_symb_items_list i1 s1) == (G_symb_items_list i2 s2) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova coerce i1 i2 s1 == Just s2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | Grothendieck symbol maps

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata G_symb_map_items_list = forall lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Logic lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree =>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova G_symb_map_items_list lid [symb_map_items]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Show G_symb_map_items_list where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova show (G_symb_map_items_list _ l) = show l

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance PrettyPrint G_symb_map_items_list where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova printText0 ga (G_symb_map_items_list _ l) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova fsep $ punctuate comma $ map (printText0 ga) l

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Eq G_symb_map_items_list where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (G_symb_map_items_list i1 s1) == (G_symb_map_items_list i2 s2) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova coerce i1 i2 s1 == Just s2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | Grothendieck diagrams

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata G_diagram = forall lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Logic lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree =>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova G_diagram lid (Diagram sign morphism)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | Grothendieck sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata G_sublogics = forall lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Logic lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree =>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova G_sublogics lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatyconG_sublogics :: TyCon

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovatyconG_sublogics = mkTyCon "Logic.Grothendieck.G_sublogics"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Typeable G_sublogics where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova typeOf _ = mkTyConApp tyconG_sublogics []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Show G_sublogics where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova show (G_sublogics lid sub) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova show lid++"."++head (sublogic_names lid sub)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Eq G_sublogics where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova (G_sublogics lid1 l1) == (G_sublogics lid2 l2) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova coerce lid1 lid2 l1 == Just l2

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Ord G_sublogics where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova compare (G_sublogics lid1 l1) (G_sublogics lid2 l2) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case coerce lid1 lid2 l2 of

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else if l1 <<= l2' then LT

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else GT-}

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- | Homogeneous Grothendieck signature morphisms

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata G_morphism = forall lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree .

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Logic lid sublogics

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova basic_spec sentence symb_items symb_map_items

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova sign morphism symbol raw_symbol proof_tree =>

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova G_morphism lid morphism

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovainstance Show G_morphism where

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova show (G_morphism _ l) = show l

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova----------------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- Existential types for the logic graph

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova----------------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

-- | 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 =

language_name cid1 == language_name 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) =

case language_name cid of

'i':'d':'_':_ -> True

_ -> False

-- | 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

= coerce cid1 cid2 (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 morphism between two Grothendieck signatures

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

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

let ln1 = language_name lid1

ln2 = language_name lid2 in

if ln1==ln2 then do

sigma2' <- rcoerce lid1 lid2 (newPos "s" 0 0) sigma2

mor <- inclusion lid1 sigma1 sigma2'

return (GMorphism (IdComorphism lid1 (top_sublogic lid1)) sigma1 mor)

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

Just (Comorphism i) -> do

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)

Nothing -> Result [Diag FatalError

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

(newPos "t" 0 0)] Nothing

-- | 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::[(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::[AnyComorphism]) =

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

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

-- | Grothendieck sublogics

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)