-- needs ghc -fglasgow-exts

{- HetCATS/Grothendieck.hs

$Id$

Till Mossakowski

The Grothendieck logic is defined to be the

heterogeneous logic over the logic graph.

This will be the logic over which the data

structures and algorithms for specification in-the-large

are built.

References:

R. Diaconescu:

Grothendieck institutions

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

T. Mossakowski:

Heterogeneous development graphs and heterogeneous borrowing

Fossacs 2002, LNCS 2303, p. 326-341

T. Mossakowski: Foundations of heterogeneous specification

Submitted

T. Mossakowski:

Relating CASL with Other Specification Languages:

the Institution Level

Theoretical Computer Science 286, 2002, p. 367-475

Todo:

-}

module Logic.Grothendieck where

import Logic.Logic

import Logic.Comorphism

import Common.PrettyPrint

import Common.Lib.Pretty

import qualified Common.Lib.Map as Map

import Common.PPUtils (fsep_latex, comma_latex)

import Common.Result

import Common.Id

import Common.Named

import Data.Dynamic

import Common.ATerm.Lib

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

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

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

data G_basic_spec = 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_basic_spec lid basic_spec

instance Show G_basic_spec where

show (G_basic_spec _ s) = show s

instance PrettyPrint G_basic_spec where

printText0 ga (G_basic_spec _ s) = printText0 ga s

printLatex0 ga (G_basic_spec _ s) = printLatex0 ga s

data G_sentence = 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_sentence lid sentence

instance Show G_sentence where

show (G_sentence _ s) = show s

data G_l_sentence_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_l_sentence lid [Named sentence]

data G_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_sign lid sign

instance Typeable G_sign where

typeOf _ = mkAppTy (mkTyCon "G_sign") []

instance Eq G_sign where

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

coerce i1 i2 sigma1 == Just sigma2

instance Show G_sign where

show (G_sign _ s) = show s

data G_sign_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_sign_list lid [sign]

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

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

printLatex0 ga (G_symb_items_list _ l) =

fsep_latex $ punctuate comma_latex $ map (printLatex0 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

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

printLatex0 ga (G_symb_map_items_list _ l) =

fsep_latex $ punctuate comma_latex $ map (printLatex0 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

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)

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

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

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

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

type LogicGraph = (Map.Map String AnyLogic,Map.Map String AnyComorphism)

lookupLogic :: String -> String -> LogicGraph -> AnyLogic

lookupLogic error_prefix logname (logics,_) =

case Map.lookup logname logics of

Nothing -> error (error_prefix++"logic "++logname++" unknown")

Just lid -> lid

lookupComorphism :: String -> String -> LogicGraph -> AnyComorphism

lookupComorphism error_prefix coname (_,comorphisms) =

case Map.lookup coname comorphisms of

Nothing -> error (error_prefix++"logic "++coname++" unknown")

Just cid -> cid

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

instance Typeable (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)

instance Show (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)

{- This does not work due to needed ordering:

instance Functor Set where

fmap = mapSet

instance Monad Set where

return = unitSet

m >>= k = unionManySets (setToList (fmap k m))

-}

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

-- The Grothendieck signature category

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

-- composition in diagrammatic order

compAnyComorphism :: AnyComorphism -> AnyComorphism -> Maybe AnyComorphism

compAnyComorphism = undefined

{-

(Comorphism (r1 :: Comorphism 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 (r2 :: Comorphism lid3 sublogics3 basic_spec3 sentence3

symb_items3 symb_map_items3

sign3 morphism3 symbol3 raw_symbol3 proof_tree3

lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4

sign4 morphism4 symbol4 raw_symbol4 proof_tree4)) =

do r3 <- coerce (target r1) (source r2) r2 :: Maybe(

Comorphism lid2 sublogics2 basic_spec2 sentence2

symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2

lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4

sign4 morphism4 symbol4 raw_symbol4 proof_tree4)

r4 <- comp_Comorphism r1 r3

return (Comorphism r4)

-}

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

{-

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

GMHomInclusion lid sign sign

| GMHetInclusion G_sign G_sign

-}

instance Eq GMorphism where

(GMorphism cid1 sigma1 mor1) ==

(GMorphism cid2 sigma2 mor2)

= maybe False id

(do s <- coerce cid1 cid2 "x"

return (s==Just "x")

sigma2' <- coerce (sourceLogic cid1) (sourceLogic cid2) sigma2

mor2' <- coerce (targetLogic cid1) (targetLogic cid2) mor2

return (sigma1 == sigma2' && mor1==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 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' lid1' lid2' <-

(coerce lid2 lid3 $ ComorphismAux r1 lid1 lid2)

:: Maybe (AnyComorphismAux lid5 sublogics1

basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid6 sublogics2

basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2)

-- r1' <- coerce lid2 lid3 r1

let r3 = CompComorphism r1' r2

-- lid5 = targetLogic r3

-- mor1' <- coerce lid2 lid3 mor1

-- mor1'' <- map_morphism r2 mor1'

-- mor <- comp lid5 mor2 mor1''

return undefined

-- return (GMorphism r3 undefined undefined) --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

ideGrothendieck (G_sign lid sigma) =

GMorphism (IdComorphism lid) sigma (ide lid sigma)

domGrothendieck (GMorphism cid sigma _mor) = G_sign (sourceLogic cid) sigma

codGrothendieck (GMorphism cid _sigma mor) =

G_sign lid (cod lid mor)

where lid = targetLogic cid

gEmbed :: G_morphism -> GMorphism

gEmbed _ = error "gEmbed"

--gEmbed (G_morphism lid mor) =

-- GMorphism lid lid (id_Comorphism lid) (dom lid mor) mor

-- homogeneous Union of two Grothendieck signatures

homogeneousGsigUnion :: Pos -> G_sign -> G_sign -> Result G_sign

--homogeneousGsigUnion _ sign _ = return 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 (sign:_) = return sign

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 _ (m:_) = return m

{-

homogeneousMorManyUnion pos (G_morphism lid mor : gmors) = do

mors <- let coerce_lid (G_morphism lid1 mor1) =

rcoerce lid lid1 pos mor1

in sequence (map coerce_lid gmors)

bigMor <- let mor_union s1 s2 = do

s1' <- s1

morphism_union lid s1' s2

in foldl mor_union (return mor) mors

return (G_morphism lid bigMor)

-}

inclusion :: G_sign -> G_sign -> GMorphism

inclusion (G_sign _lid1 _sigma1) (G_sign _lid2 _sigma2) = error "inclusion"