{-|

Module : $Header$

Copyright : (c) Till Mossakowski, Uni Bremen 2002-2004

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

Maintainer : hets@tzi.de

Stability : provisional

Portability : non-portable (via Logic)

Provides data structures for institution morphisms.

These are just collections of

functions between (some of) the types of logics.

-}

{- References: see Logic.hs

Todo:

morphism modifications / representation maps

-}

module Logic.Morphism where

import Logic.Logic

import Logic.Comorphism

import Common.Lib.Set

import Data.Maybe

import Data.Dynamic

import Common.DynamicUtils

import Common.AS_Annotation (Named, mapNamedM)

class (Language cid,

Logic lid1 sublogics1

basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

Logic lid2 sublogics2

basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>

Morphism 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

| cid -> lid1, cid -> lid2

where

-- source and target logic and sublogic

-- the source sublogic is the maximal one for which the comorphism works

-- the target sublogic is the resulting one

morSourceLogic :: cid -> lid1

morSourceSublogic :: cid -> sublogics1

morTargetLogic :: cid -> lid2

morTargetSublogic :: cid -> sublogics2

-- finer information of target sublogics corresponding to source sublogics

morMapSublogic :: cid -> sublogics1 -> sublogics2

-- default implementation

morMapSublogic cid _ = targetSublogic cid

-- the translation functions are partial

-- because the target may be a sublanguage

-- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2

-- we do not cover theoroidal morphisms,

-- since there are no relevant examples and they do not compose nicely

-- no mapping of theories, since signatrures and sentences are mapped

-- contravariantly

morMap_sign :: cid -> sign1 -> Maybe sign2

morMap_morphism :: cid -> morphism1 -> Maybe morphism2

morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1

-- also covers semi-morphisms ??

-- with no sentence translation

-- - but these are spans!

morMap_symbol :: cid -> symbol1 -> Set symbol2

morConstituents :: cid -> [String]

-- default implementation

morConstituents cid = [language_name cid]

-- identity morphisms

data IdMorphism lid sublogics =

IdMorphism lid sublogics deriving Show

idMorphismTc :: TyCon

idMorphismTc = mkTyCon "Logic.Morphism.IdMorphism"

instance Typeable (IdMorphism lid sub) where

typeOf _ = mkTyConApp idMorphismTc []

instance Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

Language (IdMorphism lid sublogics) where

language_name (IdMorphism lid sub) =

case sublogic_names lid sub of

[] -> error "language_name IdMorphism"

h : _ -> "id_" ++ language_name lid ++ "." ++ h

instance Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

Morphism (IdMorphism lid sublogics)

lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

where

sourceLogic (IdMorphism lid _sub) = lid

targetLogic (IdMorphism lid _sub) = lid

sourceSublogic (IdMorphism _lid sub) = sub

targetSublogic (IdMorphism _lid sub) = sub

map_sign _ = \sigma -> Just(sigma,[])

map_morphism _ = Just

map_sentence _ = \_ -> Just

map_symbol _ = single

constituents _ = []

-- composition not needed, use lax triangles instead

-- comorphisms inducing morphisms

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

MorphismInducing 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

where

indMorMap_sign :: cid -> sign2 -> Maybe sign1

indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1

epsilon :: cid -> sign2 -> Maybe morphism2