076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder{-# LANGUAGE UndecidableInstances #-}

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder{- |

81d182b21020b815887e9057959228546cf61b6bChristian MaederModule : $Header$

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederDescription : interface and class for logic translations

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : till@informatik.uni-bremen.de

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederStability : provisional

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederPortability : non-portable (via Logic)

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederCentral interface (type class) for logic translations (comorphisms) in Hets

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder These are just collections of

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder functions between (some of) the types of logics.

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder References: see Logic.hs

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-}

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule Logic.Comorphism

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder ( CompComorphism (..)

35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maeder , InclComorphism

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder , inclusion_logic

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder , inclusion_source_sublogic

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder , inclusion_target_sublogic

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , mkInclComorphism

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , mkIdComorphism

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , Comorphism (..)

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , targetSublogic

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder , map_sign

99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder , ext_map_sign

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , mapDefaultMorphism

99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder , wrapMapTheory

6e5180855658f12f9059d9041f447bf0935de344Christian Maeder , simpleTheoryMapping

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , mkTheoryMapping

8a1f427564a5ae2db32332512237ef645289c34dChristian Maeder , AnyComorphism (..)

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder , idComorphism

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder , isIdComorphism

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder , isModelTransportable

4e013227ed41ccd2e3d09dd44bedd651e1901f38Christian Maeder , hasModelExpansion

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder , isWeaklyAmalgamable

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , compComorphism

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder ) where

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maederimport Logic.Logic

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederimport Logic.Coerce

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maederimport Logic.ExtSign

76647324ed70f33b95a881b536d883daccf9568dChristian Maederimport Common.ExtSign

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Common.Result

529f678f015ae5276f87da63114cdce750b366aeChristian Maederimport Common.ProofUtils

529f678f015ae5276f87da63114cdce750b366aeChristian Maederimport Common.AS_Annotation

529f678f015ae5276f87da63114cdce750b366aeChristian Maederimport Common.Doc

529f678f015ae5276f87da63114cdce750b366aeChristian Maederimport Common.DocUtils

529f678f015ae5276f87da63114cdce750b366aeChristian Maederimport qualified Data.Set as Set

529f678f015ae5276f87da63114cdce750b366aeChristian Maederimport Data.Typeable

529f678f015ae5276f87da63114cdce750b366aeChristian Maeder

529f678f015ae5276f87da63114cdce750b366aeChristian Maederclass (Language cid,

529f678f015ae5276f87da63114cdce750b366aeChristian Maeder Logic lid1 sublogics1

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1

8a1f427564a5ae2db32332512237ef645289c34dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

529f678f015ae5276f87da63114cdce750b366aeChristian Maeder Logic lid2 sublogics2

b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2

529f678f015ae5276f87da63114cdce750b366aeChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Comorphism cid

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder where

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder -- source and target logic and sublogic

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

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder sourceLogic :: cid -> lid1

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder sourceSublogic :: cid -> sublogics1

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder targetLogic :: cid -> lid2

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder -- finer information of target sublogics corresponding to source sublogics

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder -- this function must be partial because mapTheory is partial

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder mapSublogic :: cid -> sublogics1 -> Maybe sublogics2

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder -- the translation functions are partial

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder -- because the target may be a sublanguage

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder -- cover theoroidal comorphisms as well

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder map_theory :: cid -> (sign1,[Named sentence1])

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder -> Result (sign2,[Named sentence2])

529f678f015ae5276f87da63114cdce750b366aeChristian Maeder map_morphism :: cid -> morphism1 -> Result morphism2

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2

b7941d1840cb336e11e7a7c0916f7b763c0366f0Christian Maeder -- also covers semi-comorphisms

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder -- with no sentence translation

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder -- - but these are spans!

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder map_sentence = failMapSentence

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder map_symbol :: cid -> sign1 -> symbol1 -> Set.Set symbol2

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder map_symbol = errMapSymbol

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder extractModel :: cid -> sign1 -> proof_tree2

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder -> Result (sign1, [Named sentence1])

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder extractModel cid _ _ = fail

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder $ "extractModel not implemented for comorphism "

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder ++ language_name cid

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder --properties of comorphisms

is_model_transportable :: cid -> Bool

-- a comorphism (\phi, \alpha, \beta) is model-transportable

-- if for any signature \Sigma,

-- any \Sigma-model M and any \phi(\Sigma)-model N

-- for any isomorphism h : \beta_\Sigma(N) -> M

-- there exists an isomorphism h': N -> M' such that \beta_\Sigma(h') = h

is_model_transportable _ = False

has_model_expansion :: cid -> Bool

has_model_expansion _ = False

is_weakly_amalgamable :: cid -> Bool

is_weakly_amalgamable _ = False

constituents :: cid -> [String]

constituents cid = [language_name cid]

isInclusionComorphism :: cid -> Bool

isInclusionComorphism _ = False

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

=> cid -> sublogics2

targetSublogic cid = maybe (top_sublogic $ targetLogic cid)

id $ mapSublogic cid $ sourceSublogic cid

-- | this function is base on 'map_theory' using no sentences as input

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

=> cid -> sign1 -> Result (sign2,[Named sentence2])

map_sign cid sign = wrapMapTheory cid (sign,[])

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

=> cid -> ExtSign sign1 symbol1

-> Result (ExtSign sign2 symbol2, [Named sentence2])

ext_map_sign cid (ExtSign sign _) = do

(sign2, sens2) <- map_sign cid sign

return (makeExtSign (targetLogic cid) sign2, sens2)

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

=> cid -> morphism1 -> Result morphism2

mapDefaultMorphism cid mor = do

(sig1, _) <- map_sign cid $ dom mor

(sig2, _) <- map_sign cid $ cod mor

inclusion (targetLogic cid) sig1 sig2

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

=> cid -> sign1 -> sentence1 -> Result sentence2

failMapSentence cid _ _ =

fail $ "Unsupported sentence translation " ++ show cid

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

=> cid -> sign1 -> symbol1 -> Set.Set symbol2

errMapSymbol cid _ _ = error $ "no symbol mapping for " ++ show cid

-- | use this function instead of 'map_theory'

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

=> cid -> (sign1, [Named sentence1])

-> Result (sign2, [Named sentence2])

wrapMapTheory cid (sign, sens) = let res = map_theory cid (sign, sens) in

if isIdComorphism $ Comorphism cid then res else case sourceSublogic cid of

sub -> case minSublogic sign of

sigLog -> case foldl join sigLog

$ map (minSublogic . sentence) sens of

senLog ->

if isSubElem senLog sub

then res

else fail $ "for '" ++ language_name cid ++

"' expected sublogic '" ++

sublogicName sub ++

"'\n but found sublogic '" ++

sublogicName senLog ++

"' with signature sublogic '" ++

sublogicName sigLog ++ "'\n" ++

show (vcat $ pretty sign : map

(print_named $ sourceLogic cid) sens)

simpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)

-> (sign1, [Named sentence1])

-> (sign2, [Named sentence2])

simpleTheoryMapping mapSig mapSen (sign,sens) =

(mapSig sign, map (mapNamed mapSen) sens)

mkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))

-> (sign1 -> sentence1 -> m sentence2)

-> (sign1, [Named sentence1])

-> m (sign2, [Named sentence2])

mkTheoryMapping mapSig mapSen (sign,sens) = do

(sign',sens') <- mapSig sign

sens'' <- mapM (mapNamedM $ mapSen sign) sens

return (sign', nameAndDisambiguate $ sens' ++ sens'')

data InclComorphism lid sublogics = InclComorphism

{ inclusion_logic :: lid

, inclusion_source_sublogic :: sublogics

, inclusion_target_sublogic :: sublogics }

deriving Show

-- | construction of an identity comorphism

mkIdComorphism :: (Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree) =>

lid -> sublogics -> InclComorphism lid sublogics

mkIdComorphism lid sub = InclComorphism

{ inclusion_logic = lid

, inclusion_source_sublogic = sub

, inclusion_target_sublogic = sub }

-- | construction of an inclusion comorphism

mkInclComorphism :: (Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree,

Monad m) =>

lid -> sublogics -> sublogics

-> m (InclComorphism lid sublogics)

mkInclComorphism lid srcSub trgSub =

if isSubElem srcSub trgSub

then return $ InclComorphism

{ inclusion_logic = lid

, inclusion_source_sublogic = srcSub

, inclusion_target_sublogic = trgSub }

else fail ("mkInclComorphism: first sublogic must be a "++

"subElem of the second sublogic")

instance (Language lid, Eq sublogics, Show sublogics, SublogicName sublogics)

=> Language (InclComorphism lid sublogics) where

language_name (InclComorphism lid sub_src sub_trg) =

let sblName = sublogicName sub_src

lname = language_name lid

in if sub_src == sub_trg

then "id_" ++ lname ++

if null sblName

then "" else "." ++ sblName

else "incl_" ++ lname ++ ":" ++

sblName ++ "->" ++ sublogicName sub_trg

instance Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

Comorphism (InclComorphism 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 = inclusion_logic

targetLogic = inclusion_logic

sourceSublogic = inclusion_source_sublogic

mapSublogic cid subl =

if isSubElem subl $ inclusion_source_sublogic cid

then Just subl

else Nothing

map_theory _ = return

map_morphism _ = return

map_sentence _ = \_ -> return

map_symbol _ _ = Set.singleton

constituents cid =

if inclusion_source_sublogic cid

== inclusion_target_sublogic cid

then []

else [language_name cid]

is_model_transportable _ = True

has_model_expansion _ = True

is_weakly_amalgamable _ = True

isInclusionComorphism _ = True

data CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show

instance (Language cid1, Language cid2)

=> Language (CompComorphism cid1 cid2) where

language_name (CompComorphism cid1 cid2) =

language_name cid1 ++ ";" ++ language_name cid2

instance (Comorphism cid1

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 cid2

lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4

sign4 morphism4 symbol4 raw_symbol4 proof_tree4

lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

sign3 morphism3 symbol3 raw_symbol3 proof_tree3)

=> Comorphism (CompComorphism cid1 cid2)

lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where

sourceLogic (CompComorphism cid1 _) =

sourceLogic cid1

targetLogic (CompComorphism _ cid2) =

targetLogic cid2

sourceSublogic (CompComorphism cid1 _) =

sourceSublogic cid1

mapSublogic (CompComorphism cid1 cid2) sl =

mapSublogic cid1 sl >>=

(\ y -> mapSublogic cid2 $

forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2) y)

map_sentence (CompComorphism cid1 cid2) =

\si1 se1 ->

do (si2,_) <- map_sign cid1 si1

se2 <- map_sentence cid1 si1 se1

(si2', se2') <- coerceBasicTheory

(targetLogic cid1) (sourceLogic cid2)

"Mapping sentence along comorphism" (si2, [makeNamed "" se2])

case se2' of

[x] -> map_sentence cid2 si2' $ sentence x

_ -> error "CompComorphism.map_sentence"

map_theory (CompComorphism cid1 cid2) =

\ti1 ->

do ti2 <- map_theory cid1 ti1

ti2' <- coerceBasicTheory (targetLogic cid1) (sourceLogic cid2)

"Mapping theory along comorphism" ti2

wrapMapTheory cid2 ti2'

map_morphism (CompComorphism cid1 cid2) = \ m1 ->

do m2 <- map_morphism cid1 m1

m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2)

"Mapping signature morphism along comorphism"m2

map_morphism cid2 m3

map_symbol (CompComorphism cid1 cid2) sig1 = let

th = map_sign cid1 sig1 in

case maybeResult th of

Nothing -> error "failed translating signature"

Just (sig2', _) -> let

th2 = coerceBasicTheory

(targetLogic cid1) (sourceLogic cid2)

"Mapping symbol along comorphism" (sig2', [])

in case maybeResult th2 of

Nothing -> error "failed coercing"

Just (sig2, _) ->

\ s1 ->

let mycast = coerceSymbol (targetLogic cid1) (sourceLogic cid2)

in Set.unions

(map (map_symbol cid2 sig2 . mycast)

(Set.toList (map_symbol cid1 sig1 s1)))

extractModel (CompComorphism cid1 cid2) sign pt3 =

let lid1 = sourceLogic cid1

lid3 = sourceLogic cid2

in if language_name lid1 == language_name lid3 then do

bTh1 <- map_sign cid1 sign

(sign1, _) <-

coerceBasicTheory (targetLogic cid1) lid3 "extractModel1" bTh1

bTh2 <- extractModel cid2 sign1 pt3

coerceBasicTheory lid3 lid1 "extractModel2" bTh2

else fail $ "extractModel not implemented for comorphism composition with "

++ language_name cid1

constituents (CompComorphism cid1 cid2) =

constituents cid1 ++ constituents cid2

is_model_transportable (CompComorphism cid1 cid2) =

is_model_transportable cid1 && is_model_transportable cid2

has_model_expansion (CompComorphism cid1 cid2) =

has_model_expansion cid1 && has_model_expansion cid2

is_weakly_amalgamable (CompComorphism cid1 cid2) =

is_weakly_amalgamable cid1 && is_weakly_amalgamable cid2

isInclusionComorphism (CompComorphism cid1 cid2) =

isInclusionComorphism cid1 && isInclusionComorphism cid2

-- * Comorphisms and 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 deriving Typeable -- used for GTheory

instance Eq AnyComorphism where

a == b = compare a b == EQ

instance Ord AnyComorphism where

compare (Comorphism cid1) (Comorphism cid2) = compare

(language_name cid1, constituents cid1)

(language_name cid2, constituents cid2)

-- maybe needs to be refined, using comorphism translations?

instance Show AnyComorphism where

show (Comorphism cid) = language_name cid

++ " : " ++ language_name (sourceLogic cid)

++ " -> " ++ language_name (targetLogic cid)

instance Pretty AnyComorphism where

pretty = text . show

-- | compute the identity comorphism for a logic

idComorphism :: AnyLogic -> AnyComorphism

idComorphism (Logic lid) = Comorphism (mkIdComorphism lid (top_sublogic lid))

-- | Test whether a comporphism is the identity

isIdComorphism :: AnyComorphism -> Bool

isIdComorphism (Comorphism cid) = null $ constituents cid

-- * Properties of comorphisms

-- | Test whether a comorphism is model-transportable

isModelTransportable :: AnyComorphism -> Bool

isModelTransportable (Comorphism cid) = is_model_transportable cid

-- | Test whether a comorphism has model expansion

hasModelExpansion :: AnyComorphism -> Bool

hasModelExpansion (Comorphism cid) = has_model_expansion cid

-- | Test whether a comorphism is weakly amalgamable

isWeaklyAmalgamable :: AnyComorphism -> Bool

isWeaklyAmalgamable (Comorphism cid) = is_weakly_amalgamable cid

-- | Compose comorphisms

compComorphism :: Monad m => AnyComorphism -> AnyComorphism -> m AnyComorphism

compComorphism (Comorphism cid1) (Comorphism cid2) =

let l1 = targetLogic cid1

l2 = sourceLogic cid2

msg = "ogic mismatch in composition of " ++ language_name cid1

++ " and " ++ language_name cid2

in

if language_name l1 == language_name l2 then

if isSubElem (forceCoerceSublogic l1 l2 $ targetSublogic cid1)

$ sourceSublogic cid2

then {- case (isIdComorphism cm1,isIdComorphism cm2) of

(True,_) -> return cm2

(_,True) -> return cm1

_ -> -} return $ Comorphism (CompComorphism cid1 cid2)

else fail $ "Subl" ++ msg

else fail $ "L" ++ msg