306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder{-|

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederModule : $Header$

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederMaintainer : till@tzi.de

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : non-portable (via Logic)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

44fb55f639914f4f531641f32dd4904f15c510a4Till MossakowskiProvides data structures for institution comorphisms.

44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski These are just collections of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski functions between (some of) the types of logics.

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder-}

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder{- References: see Logic.hs

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Todo:

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Flag for model expansion property

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski Weak amalgamability, also for comorphisms

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski comorphism modifications

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski comorphisms out of sublogic relationships

ae7058143db9e9993b5eff70bd6b7aede7cec658Till Mossakowski restrictions of comorphisms to sublogics

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski morphisms and other translations via spans

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskimodule Logic.Comorphism where

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Logic.Logic

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederimport Logic.Coerce

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Common.Lib.Set as Set

9e2e744c6b967c3f5f581acf01c13769b6769285Till Mossakowskiimport Common.Result

38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowskiimport Common.ProofUtils

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Common.AS_Annotation

59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiclass (Language cid,

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid1 sublogics1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid2 sublogics2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec2 sentence2 symb_items2 symb_map_items2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism cid

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder | cid -> lid1, cid -> lid2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski where

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- source and target logic and sublogic

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- the source sublogic is the maximal one for which the comorphism works

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski -- the target sublogic is the resulting one

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceLogic :: cid -> lid1

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski sourceSublogic :: cid -> sublogics1

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski targetLogic :: cid -> lid2

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski targetSublogic :: cid -> sublogics2

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- finer information of target sublogics corresponding to source sublogics

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski mapSublogic :: cid -> sublogics1 -> sublogics2

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski -- default implementation

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski mapSublogic cid _ = targetSublogic cid

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- the translation functions are partial

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- because the target may be a sublanguage

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2

38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowski -- cover theoroidal comorphisms as well

5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski map_theory :: cid -> (sign1,[Named sentence1])

5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski -> Result (sign2,[Named sentence2])

9a36df4f63e0214bc0b4aef9b388c8d4e48632bbTill Mossakowski map_morphism :: cid -> morphism1 -> Result morphism2

9a36df4f63e0214bc0b4aef9b388c8d4e48632bbTill Mossakowski map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2

5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski -- also covers semi-comorphisms

5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski -- with no sentence translation

62867c8459918ce0a96960093eb43d758b97a603Till Mossakowski -- - but these are spans!

5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski map_symbol :: cid -> symbol1 -> Set.Set symbol2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski constituents :: cid -> [String]

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- default implementation

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski constituents cid = [language_name cid]

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskimap_sign :: Comorphism cid

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2

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

586af0e9490a14dd3075095692b584c652584875Till Mossakowskimap_sign cid sign = map_theory cid (sign,[])

586af0e9490a14dd3075095692b584c652584875Till Mossakowski

933baca0720dae81434de384b32a93b47e754d09Christian MaedersimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski -> (sign1, [Named sentence1])

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski -> (sign2, [Named sentence2])

933baca0720dae81434de384b32a93b47e754d09Christian MaedersimpleTheoryMapping mapSig mapSen (sign,sens) =

586af0e9490a14dd3075095692b584c652584875Till Mossakowski (mapSig sign, map (mapNamed mapSen) sens)

59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder

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

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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -> (sign1, [Named sentence1])

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -> m (sign2, [Named sentence2])

586af0e9490a14dd3075095692b584c652584875Till MossakowskimkTheoryMapping mapSig mapSen (sign,sens) = do

586af0e9490a14dd3075095692b584c652584875Till Mossakowski (sign',sens') <- mapSig sign

933baca0720dae81434de384b32a93b47e754d09Christian Maeder sens'' <- mapM (mapNamedM $ mapSen sign) sens

933baca0720dae81434de384b32a93b47e754d09Christian Maeder return (sign', disambiguateSens Set.empty . nameSens $ sens' ++ sens'')

933baca0720dae81434de384b32a93b47e754d09Christian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata IdComorphism lid sublogics =

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski IdComorphism lid sublogics

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics

586af0e9490a14dd3075095692b584c652584875Till Mossakowski basic_spec sentence symb_items symb_map_items

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree =>

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Show (IdComorphism lid sublogics)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski where

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski show = language_name

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items

933baca0720dae81434de384b32a93b47e754d09Christian Maeder sign morphism symbol raw_symbol proof_tree =>

933baca0720dae81434de384b32a93b47e754d09Christian Maeder Language (IdComorphism lid sublogics) where

933baca0720dae81434de384b32a93b47e754d09Christian Maeder language_name (IdComorphism lid sub) =

933baca0720dae81434de384b32a93b47e754d09Christian Maeder case sublogic_names lid sub of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski [] -> error "language_name IdComorphism"

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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski basic_spec sentence symb_items symb_map_items

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree =>

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder Comorphism (IdComorphism lid sublogics)

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder lid sublogics

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items

8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski sign morphism symbol raw_symbol proof_tree

933baca0720dae81434de384b32a93b47e754d09Christian Maeder lid sublogics

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder basic_spec sentence symb_items symb_map_items

59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder sign morphism symbol raw_symbol proof_tree

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski where

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sourceLogic (IdComorphism lid _sub) = lid

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski targetLogic (IdComorphism lid _sub) = lid

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sourceSublogic (IdComorphism _lid sub) = sub

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski targetSublogic (IdComorphism _lid sub) = sub

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski mapSublogic _ = id

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_theory _ = return

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder map_morphism _ = return

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder map_sentence _ = \_ -> return

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_symbol _ = Set.singleton

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski constituents _ = []

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance (Language cid1, Language cid2)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski => Language (CompComorphism cid1 cid2) where

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder language_name (CompComorphism cid1 cid2) =

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski language_name cid1++ ";" ++language_name cid2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance (Comorphism cid1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism cid2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder sign4 morphism4 symbol4 raw_symbol4 proof_tree4

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski => Comorphism (CompComorphism cid1 cid2)

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski sourceLogic (CompComorphism cid1 _) =

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceLogic cid1

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski targetLogic (CompComorphism _ cid2) =

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski targetLogic cid2

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic (CompComorphism cid1 _) =

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sourceSublogic cid1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski targetSublogic (CompComorphism cid1 cid2) =

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski mapSublogic cid2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (coerceSublogic (targetLogic cid1) (sourceLogic cid2)

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski (targetSublogic cid1))

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski mapSublogic (CompComorphism cid1 cid2) =

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder mapSublogic cid2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski . coerceSublogic (targetLogic cid1) (sourceLogic cid2)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski . mapSublogic cid1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence (CompComorphism cid1 cid2) =

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski \si1 se1 ->

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski do (si2,_) <- map_sign cid1 si1

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder se2 <- map_sentence cid1 si1 se1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (si2', se2') <- coerceBasicTheory

38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowski (targetLogic cid1) (sourceLogic cid2)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski "Mapping sentence along comorphism" (si2, [emptyName se2])

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder case se2' of

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder [x] -> map_sentence cid2 si2' $ sentence x

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder _ -> error "CompComorphism.map_sentence"

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski map_theory (CompComorphism cid1 cid2) =

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder \ti1 ->

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder do ti2 <- map_theory cid1 ti1

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

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder "Mapping theory along comorphism" ti2

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski map_theory cid2 ti2'

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder map_morphism (CompComorphism cid1 cid2) = \ m1 ->

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do m2 <- map_morphism cid1 m1

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

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski "Mapping signature morphism along comorphism"m2

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski map_morphism cid2 m3

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder map_symbol (CompComorphism cid1 cid2) = \ s1 ->

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

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski in Set.unions

933baca0720dae81434de384b32a93b47e754d09Christian Maeder (map (map_symbol cid2 . mycast)

(Set.toList (map_symbol cid1 s1)))

constituents (CompComorphism cid1 cid2) =

constituents cid1 ++ constituents cid2