1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{- |

d3d15411081a9ac4a84d409079153135bb30442aDaniel CalegariModule : $Header$

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2004

d3d15411081a9ac4a84d409079153135bb30442aDaniel CalegariLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari

d3d15411081a9ac4a84d409079153135bb30442aDaniel CalegariMaintainer : till@tzi.de

d3d15411081a9ac4a84d409079153135bb30442aDaniel CalegariStability : provisional

d3d15411081a9ac4a84d409079153135bb30442aDaniel CalegariPortability : non-portable (overlapping instances, dynamics, existentials)

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari The Grothendieck logic is defined to be the

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari heterogeneous logic over the logic graph.

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari This will be the logic over which the data

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari structures and algorithms for specification in-the-large

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari are built.

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari References:

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari R. Diaconescu:

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Grothendieck institutions

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari J. applied categorical structures 10, 2002, p. 383-402.

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari T. Mossakowski:

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari Heterogeneous development graphs and heterogeneous borrowing

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari Fossacs 2002, LNCS 2303, p. 326-341

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder T. Mossakowski: Foundations of heterogeneous specification

a58d43a4b2864a25ab74b96758fb9d98f18eeed7Daniel Calegari Submitted

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari T. Mossakowski:

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari Relating CASL with Other Specification Languages:

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari the Institution Level

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Theoretical Computer Science 286, 2002, p. 367-475

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Todo:

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari-}

a58d43a4b2864a25ab74b96758fb9d98f18eeed7Daniel Calegari

a58d43a4b2864a25ab74b96758fb9d98f18eeed7Daniel Calegarimodule Logic.Grothendieck where

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegariimport Logic.Logic

a58d43a4b2864a25ab74b96758fb9d98f18eeed7Daniel Calegariimport Logic.Prover

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegariimport Logic.Comorphism

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariimport Common.PrettyPrint

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariimport Common.Lib.Pretty

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariimport qualified Common.Lib.Map as Map

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport qualified Common.Lib.Set as Set

a58d43a4b2864a25ab74b96758fb9d98f18eeed7Daniel Calegariimport Common.Result

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariimport Common.Id

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.AS_Annotation

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.ListUtils

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.Dynamic

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegariimport qualified Data.List as List

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegariimport Data.Maybe

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariimport Control.Monad

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport Common.Lib.Parsec.Pos -- for testing purposes

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari------------------------------------------------------------------

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder--"Grothendieck" versions of the various parts of type class Logic

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder------------------------------------------------------------------

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | Grothendieck basic specifications

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata G_basic_spec = forall lid sublogics

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder basic_spec sentence symb_items symb_map_items

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari sign morphism symbol raw_symbol proof_tree .

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Logic lid sublogics

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari basic_spec sentence symb_items symb_map_items

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari sign morphism symbol raw_symbol proof_tree =>

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari G_basic_spec lid basic_spec

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance Show G_basic_spec where

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari show (G_basic_spec _ s) = show s

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance PrettyPrint G_basic_spec where

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari printText0 ga (G_basic_spec _ s) = printText0 ga s

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | Grothendieck sentences

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegaridata G_sentence = forall lid sublogics

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari basic_spec sentence symb_items symb_map_items

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign morphism symbol raw_symbol proof_tree .

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic lid sublogics

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder basic_spec sentence symb_items symb_map_items

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari sign morphism symbol raw_symbol proof_tree =>

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari G_sentence lid sentence

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegariinstance Show G_sentence where

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari show (G_sentence _ s) = show s

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari-- | Grothendieck sentence lists

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegaridata G_l_sentence_list = forall lid sublogics

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari basic_spec sentence symb_items symb_map_items

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari sign morphism symbol raw_symbol proof_tree .

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari Logic lid sublogics

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder basic_spec sentence symb_items symb_map_items

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari sign morphism symbol raw_symbol proof_tree =>

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari G_l_sentence_list lid [Named sentence]

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegariinstance Show G_l_sentence_list where

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari show (G_l_sentence_list _ s) = show s

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegariinstance Eq G_l_sentence_list where

eb06c6332e2e2ef6f5d1cdd74c5ce7abbd23de28Daniel Calegari (G_l_sentence_list i1 nl1) == (G_l_sentence_list i2 nl2) =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder coerce i1 i2 nl1 == Just nl2

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegarieq_G_l_sentence_set :: G_l_sentence_list -> G_l_sentence_list -> Bool

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegarieq_G_l_sentence_set (G_l_sentence_list i1 nl1) (G_l_sentence_list i2 nl2) =

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari case coerce i1 i2 nl1 of

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Just nl1' -> Set.fromList nl1' == Set.fromList nl2

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Nothing -> False

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari-- | Grothendieck signatures

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegaridata G_sign = forall lid sublogics

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari basic_spec sentence symb_items symb_map_items

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari sign morphism symbol raw_symbol proof_tree .

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari Logic lid sublogics

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder basic_spec sentence symb_items symb_map_items

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign morphism symbol raw_symbol proof_tree =>

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder G_sign lid sign

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

d3d15411081a9ac4a84d409079153135bb30442aDaniel CalegarityconG_sign :: TyCon

d3d15411081a9ac4a84d409079153135bb30442aDaniel CalegarityconG_sign = mkTyCon "Logic.Grothendieck.G_sign"

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance Typeable G_sign where

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder typeOf _ = mkTyConApp tyconG_sign []

a58d43a4b2864a25ab74b96758fb9d98f18eeed7Daniel Calegari

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance Eq G_sign where

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari (G_sign i1 sigma1) == (G_sign i2 sigma2) =

a58d43a4b2864a25ab74b96758fb9d98f18eeed7Daniel Calegari coerce i1 i2 sigma1 == Just sigma2

a58d43a4b2864a25ab74b96758fb9d98f18eeed7Daniel Calegari

1a38107941725211e7c3f051f7a8f5e12199f03acmaederinstance Show G_sign where

a58d43a4b2864a25ab74b96758fb9d98f18eeed7Daniel Calegari show (G_sign _ s) = show s

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance PrettyPrint G_sign where

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari printText0 ga (G_sign _ s) = printText0 ga s

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

d3d15411081a9ac4a84d409079153135bb30442aDaniel CalegarilangNameSig :: G_sign -> String

d3d15411081a9ac4a84d409079153135bb30442aDaniel CalegarilangNameSig (G_sign lid _) = language_name lid

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari-- | Grothendieck signature lists

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata G_sign_list = forall lid sublogics

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder basic_spec sentence symb_items symb_map_items

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari sign morphism symbol raw_symbol proof_tree .

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Logic lid sublogics

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari basic_spec sentence symb_items symb_map_items

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign morphism symbol raw_symbol proof_tree =>

d3d15411081a9ac4a84d409079153135bb30442aDaniel Calegari G_sign_list lid [sign]

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari

acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari-- | Grothendieck extended signatures

data G_ext_sign = 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_ext_sign lid sign (Set.Set symbol)

tyconG_ext_sign :: TyCon

tyconG_ext_sign = mkTyCon "Logic.Grothendieck.G_ext_sign"

instance Typeable G_ext_sign where

typeOf _ = mkTyConApp tyconG_ext_sign []

instance Eq G_ext_sign where

(G_ext_sign i1 sigma1 sys1) == (G_ext_sign i2 sigma2 sys2) =

coerce i1 i2 sigma1 == Just sigma2

&& coerce i1 i2 sys1 == Just sys2

instance Show G_ext_sign where

show (G_ext_sign _ s _) = show s

instance PrettyPrint G_ext_sign where

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

langNameExtSig :: G_ext_sign -> String

langNameExtSig (G_ext_sign lid _ _) = language_name lid

-- | Grothendieck symbols

data G_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_symbol lid symbol

instance Show G_symbol where

show (G_symbol _ s) = show s

instance Eq G_symbol where

(G_symbol i1 s1) == (G_symbol i2 s2) =

coerce i1 i2 s1 == Just s2

-- | Grothendieck symbol lists

data G_symb_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_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

instance Show G_sublogics where

show (G_sublogics _ l) = show l

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

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)

-- | 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 :: AnyComorphism -> AnyComorphism -> Maybe AnyComorphism

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

if language_name (targetLogic cid1) ==

language_name (sourceLogic cid2)

then case (isIdComorphism cm1,isIdComorphism cm2) of

(True,_) -> Just cm2

(_,True) -> Just cm1

_ -> Just $ Comorphism (CompComorphism cid1 cid2)

else Nothing

-- | Compose comorphisms, deliver a Result

compComorphismRes :: AnyComorphism -> AnyComorphism -> Result AnyComorphism

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

maybeToResult nullPos

("Cannot compose comorphism "++language_name cid1++

" with "++language_name cid2)

(compComorphism cm1 cm2)

-- | 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 :: String -> String -> LogicGraph -> AnyLogic

lookupLogic error_prefix logname logicGraph =

case Map.lookup logname (logics logicGraph) of

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

++logname++"\" unknown")

Just lid -> lid

-- | find a comorphism in a logic graph

lookupComorphism :: String -> LogicGraph -> Result AnyComorphism

lookupComorphism coname logicGraph = do

let nameList = splitBy ';' coname

cs <- sequence $ map lookupN nameList

case cs of

c:cs1 -> foldM compComorphismRes c cs1

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

where

lookupN name =

case name of

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

l <- maybeToResult

nullPos ("Cannot find logic "++logic)

$ Map.lookup logic (logics logicGraph)

case l of

Logic lid -> return $ Comorphism $ IdComorphism lid

_ -> maybeToResult

nullPos ("Cannot find logic comorphism "++name)

$ 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) 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) (dom lid mor) mor

-- | heterogeneous union of two Grothendieck signatures

-- the left signature determines the result logic

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

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

if language_name lid1 == language_name lid2

then homogeneousGsigUnion pos 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' <- rcoerce lid1 lid1' pos sigma1

sigma2' <- rcoerce lid2 lid2' pos sigma2

(sigma2'',_) <- maybeToResult pos "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 :: 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

adjustPos pos $ 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) 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' <- rcoerce lid (sourceLogic cid) nullPos sens

sens'' <- maybeToResult nullPos "Could not map sentences"

$ sequence $ map (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' <- resultToMaybe $ rcoerce lid1 lid2 nullPos 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 -> AnyLogic -> [AnyComorphism]

findComorphismPaths lg (Logic lid) =

iterateComp (0::Int) [Comorphism (IdComorphism lid)]

where

coMors = comorphisms lg

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

iterateComp n l =

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

where

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

extend coMor = catMaybes $ map (compComorphism coMor) $ Map.elems $ 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)