{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

{- |

Module : $Header$

Description : interface (type class) for logic projections (morphisms) in Hets

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

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : till@tzi.de

Stability : provisional

Portability : non-portable (via Logic)

Interface (type class) for logic projections (morphisms) in Hets

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 qualified Common.Lib.Set as Set

import Data.Maybe

import Common.DynamicUtils

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.Set symbol2

-- morConstituents not needed, because composition only via lax triangles

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

morSourceLogic (IdMorphism lid _sub) = lid

morTargetLogic (IdMorphism lid _sub) = lid

morSourceSublogic (IdMorphism _lid sub) = sub

morTargetSublogic (IdMorphism _lid sub) = sub

morMapSublogic _ _ =

error "Logic.Morphism.IdMorphism.morMapSublogic"

morMap_sign _ = Just

morMap_morphism _ = Just

morMap_sentence _ = \_ -> Just

morMap_symbol _ = Set.singleton

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

InducingComorphism 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