076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder , FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}

81d182b21020b815887e9057959228546cf61b6bChristian Maeder{- |

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederModule : $Header$

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederDescription : interface and class for logic translations

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederMaintainer : till@informatik.uni-bremen.de

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederStability : provisional

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable (via Logic)

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian MaederCentral interface (type class) for logic translations (comorphisms) in Hets

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder These are just collections of

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder functions between (some of) the types of logics.

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder References: see Logic.hs

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-}

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maedermodule Logic.Comorphism

35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maeder ( CompComorphism (..)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder , InclComorphism

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder , inclusion_logic

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder , inclusion_source_sublogic

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , inclusion_target_sublogic

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , mkInclComorphism

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , mkIdComorphism

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , Comorphism (..)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder , targetSublogic

99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder , map_sign

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , wrapMapTheory

99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder , mkTheoryMapping

6e5180855658f12f9059d9041f447bf0935de344Christian Maeder , AnyComorphism (..)

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder , idComorphism

8a1f427564a5ae2db32332512237ef645289c34dChristian Maeder , isIdComorphism

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder , isModelTransportable

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder , hasModelExpansion

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder , isWeaklyAmalgamable

1865083b72c1307e9040d78c2743abd5a54ee260Christian Maeder , compComorphism

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder ) where

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maederimport Logic.Logic

76647324ed70f33b95a881b536d883daccf9568dChristian Maederimport Logic.Coerce

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederimport Common.AS_Annotation

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maederimport Common.Doc

76647324ed70f33b95a881b536d883daccf9568dChristian Maederimport Common.DocUtils

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Common.Id

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederimport Common.LibName

8a1f427564a5ae2db32332512237ef645289c34dChristian Maederimport Common.ProofUtils

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederimport Common.Result

b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederimport Data.Data

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederimport Data.Maybe

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederimport qualified Data.Set as Set

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederclass (Language cid,

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder Logic lid1 sublogics1

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder Logic lid2 sublogics2

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder Comorphism cid

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

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

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder the source sublogic is the maximal one for which the comorphism works -}

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder sourceLogic :: cid -> lid1

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder sourceSublogic :: cid -> sublogics1

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder sourceSublogic cid = top_sublogic $ sourceLogic cid

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder minSourceTheory :: cid -> Maybe (LibName, String)

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder minSourceTheory _ = Nothing

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder targetLogic :: cid -> lid2

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder {- finer information of target sublogics corresponding to source sublogics

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder this function must be partial because mapTheory is partial -}

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder mapSublogic :: cid -> sublogics1 -> Maybe sublogics2

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder mapSublogic cid _ = Just $ top_sublogic $ targetLogic cid

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder {- the translation functions are partial

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder because the target may be a sublanguage

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder cover theoroidal comorphisms as well -}

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

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

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder -- map_theory but also consider sentence marks

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder mapMarkedTheory :: cid -> (sign1, [Named sentence1])

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

mapMarkedTheory cid (sig, sens) = do

(sig2, sens2) <- map_theory cid (sig, map unmark sens)

return (sig2, map (markSen $ language_name cid) sens2)

map_morphism :: cid -> morphism1 -> Result morphism2

map_morphism = mapDefaultMorphism

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

{- also covers semi-comorphisms

with no sentence translation

- but these are spans! -}

map_sentence = failMapSentence

map_symbol :: cid -> sign1 -> symbol1 -> Set.Set symbol2

map_symbol = errMapSymbol

extractModel :: cid -> sign1 -> proof_tree2

-> Result (sign1, [Named sentence1])

extractModel cid _ _ = fail

$ "extractModel not implemented for comorphism "

++ language_name cid

-- 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 = fromMaybe (top_sublogic $ targetLogic cid)

$ mapSublogic cid $ sourceSublogic cid

-- | this function is based 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, [])

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

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 = mapMarkedTheory cid (sign, sens)

lid1 = sourceLogic cid

thDoc = show (vcat $ pretty sign : map (print_named lid1) sens)

in

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

sub -> case minSublogic sign of

sigLog -> case foldl lub sigLog

$ map (minSublogic . sentence) sens of

senLog ->

if isSubElem senLog sub

then res

else Result

[ Diag Hint thDoc nullRange

, Diag Error

("for '" ++ language_name cid ++

"' expected sublogic '" ++

sublogicName sub ++

"'\n but found sublogic '" ++

sublogicName senLog ++

"' with signature sublogic '" ++

sublogicName sigLog ++ "'") nullRange] Nothing

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) . unmark) sens

return (sign', nameAndDisambiguate

$ map (markSen "SignatureProperty") sens' ++ sens'')

data InclComorphism lid sublogics = InclComorphism

{ inclusion_logic :: lid

, inclusion_source_sublogic :: sublogics

, inclusion_target_sublogic :: sublogics }

deriving (Show, Typeable, Data)

-- | 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, Typeable, Data)

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

mapSublogic cid2 .

forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2)

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 return $ Comorphism (CompComorphism cid1 cid2)

else fail $ "Subl" ++ msg ++ " (Expected sublogic "

++ sublogicName (sourceSublogic cid2)

++ " but found sublogic "

++ sublogicName (targetSublogic cid1) ++ ")"

else fail $ 'L' : msg ++ " (Expected logic "

++ language_name l2

++ " but found logic "

++ language_name l1 ++ ")"