8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable

8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder , FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder{- |

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederModule : $Header$

3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederDescription : interface and class for logic translations

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : provisional

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : non-portable (via Logic)

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederCentral interface (type class) for logic translations (comorphisms) in Hets

44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski These are just collections of

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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

af0cbe339851fc558d2b18cde3666981325e667cTill Mossakowski References: see Logic.hs

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maedermodule Logic.Comorphism

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ( CompComorphism (..)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , InclComorphism

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , inclusion_logic

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , inclusion_source_sublogic

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , inclusion_target_sublogic

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , mkInclComorphism

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , mkIdComorphism

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , Comorphism (..)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , targetSublogic

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , map_sign

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , ext_map_sign

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , mapDefaultMorphism

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , wrapMapTheory

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , simpleTheoryMapping

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder , mkTheoryMapping

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , AnyComorphism (..)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , idComorphism

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , isIdComorphism

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , isModelTransportable

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , hasModelExpansion

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , isWeaklyAmalgamable

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , compComorphism

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder ) where

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Logic.Logic

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maederimport Logic.Coerce

63324a97283728a30932828a612c7b0b0f687624Christian Maederimport Logic.ExtSign

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maederimport Common.AS_Annotation

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederimport Common.Doc

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederimport Common.DocUtils

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maederimport Common.ExtSign

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maederimport Common.Id

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maederimport Common.ProofUtils

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maederimport Common.Result

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maederimport Data.Maybe

63324a97283728a30932828a612c7b0b0f687624Christian Maederimport qualified Data.Set as Set

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport Data.Typeable

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maederclass (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

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder 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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2

3a87487c048b275c56e502c4a933273788e8d0bbChristian Maeder | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu sign1 morphism1 symbol1 raw_symbol1 proof_tree1

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu sign2 morphism2 symbol2 raw_symbol2 proof_tree2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till 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 sourceLogic :: cid -> lid1

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic :: cid -> sublogics1

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski targetLogic :: cid -> lid2

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

bba825b39570777866d560bfde3807731131097eKlaus Luettich -- this function must be partial because mapTheory is partial

bba825b39570777866d560bfde3807731131097eKlaus Luettich mapSublogic :: cid -> sublogics1 -> Maybe sublogics2

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -- the translation functions are partial

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- because the target may be a sublanguage

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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- cover theoroidal comorphisms as well

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

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

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder map_morphism :: cid -> morphism1 -> Result morphism2

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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- also covers semi-comorphisms

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- with no sentence translation

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- - but these are spans!

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder map_sentence = failMapSentence

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu map_symbol :: cid -> sign1 -> symbol1 -> Set.Set symbol2

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder map_symbol = errMapSymbol

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

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

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder extractModel cid _ _ = fail

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder $ "extractModel not implemented for comorphism "

63324a97283728a30932828a612c7b0b0f687624Christian Maeder ++ language_name cid

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu --properties of comorphisms

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu is_model_transportable :: cid -> Bool

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

b4e202184f6977662c439c82866fe93f06cebe41Christian Maeder -- if for any signature \Sigma,

830e14495f9cac8e154dd4813dae010166f33d09Mihai Codescu -- any \Sigma-model M and any \phi(\Sigma)-model N

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

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

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu is_model_transportable _ = False

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder has_model_expansion :: cid -> Bool

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu has_model_expansion _ = False

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder is_weakly_amalgamable :: cid -> Bool

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu is_weakly_amalgamable _ = False

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski constituents :: cid -> [String]

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski constituents cid = [language_name cid]

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder isInclusionComorphism :: cid -> Bool

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder isInclusionComorphism _ = False

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedertargetSublogic :: Comorphism cid

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder => cid -> sublogics2

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaedertargetSublogic cid = fromMaybe (top_sublogic $ targetLogic cid)

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder $ mapSublogic cid $ sourceSublogic cid

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

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

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maedermap_sign :: Comorphism cid

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

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

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maedermap_sign cid sign = wrapMapTheory cid (sign,[])

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_map_sign :: Comorphism cid

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder => cid -> ExtSign sign1 symbol1

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

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederext_map_sign cid (ExtSign sign _) = do

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder (sign2, sens2) <- map_sign cid sign

64e1905404e5135e98a26d2ab4150b6764956576Christian Maeder return (makeExtSign (targetLogic cid) sign2, sens2)

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapDefaultMorphism :: Comorphism cid

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder => cid -> morphism1 -> Result morphism2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapDefaultMorphism cid mor = do

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

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

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder inclusion (targetLogic cid) sig1 sig2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederfailMapSentence :: Comorphism cid

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder => cid -> sign1 -> sentence1 -> Result sentence2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederfailMapSentence cid _ _ =

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder fail $ "Unsupported sentence translation " ++ show cid

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedererrMapSymbol :: Comorphism cid

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu => cid -> sign1 -> symbol1 -> Set.Set symbol2

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai CodescuerrMapSymbol cid _ _ = error $ "no symbol mapping for " ++ show cid

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder-- | use this function instead of 'map_theory'

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian MaederwrapMapTheory :: Comorphism cid

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

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

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

255f43c567972176c2078e3de2fb7a2798bcfde0Christian MaederwrapMapTheory cid (sign, sens) = let res = map_theory cid (sign, sens) in

255f43c567972176c2078e3de2fb7a2798bcfde0Christian Maeder if isIdComorphism $ Comorphism cid then res else case sourceSublogic cid of

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder sub -> case minSublogic sign of

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder sigLog -> case foldl join sigLog

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder $ map (minSublogic . sentence) sens of

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder senLog ->

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder if isSubElem senLog sub

255f43c567972176c2078e3de2fb7a2798bcfde0Christian Maeder then res

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder else Result

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder [ Diag Hint

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder (show (vcat $ pretty sign : map

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder (print_named $ sourceLogic cid) sens))

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder nullRange

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder , Diag Error

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder ("for '" ++ language_name cid ++

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder "' expected sublogic '" ++

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder sublogicName sub ++

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder "'\n but found sublogic '" ++

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder sublogicName senLog ++

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder "' with signature sublogic '" ++

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder sublogicName sigLog ++ "'") nullRange] Nothing

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder

53310804002cd9e3c9c5844db3b984abcf001788Christian MaedersimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -> (sign1, [Named sentence1])

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -> (sign2, [Named sentence2])

53310804002cd9e3c9c5844db3b984abcf001788Christian MaedersimpleTheoryMapping mapSig mapSen (sign,sens) =

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (mapSig sign, map (mapNamed mapSen) sens)

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder

19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -> (sign1 -> sentence1 -> m sentence2)

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -> (sign1, [Named sentence1])

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder -> m (sign2, [Named sentence2])

19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermkTheoryMapping mapSig mapSen (sign,sens) = do

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (sign',sens') <- mapSig sign

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder sens'' <- mapM (mapNamedM $ mapSen sign) sens

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

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederdata InclComorphism lid sublogics = InclComorphism

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder { inclusion_logic :: lid

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , inclusion_source_sublogic :: sublogics

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , inclusion_target_sublogic :: sublogics }

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder deriving Show

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich-- | construction of an identity comorphism

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichmkIdComorphism :: (Logic lid sublogics

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich basic_spec sentence symb_items symb_map_items

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich sign morphism symbol raw_symbol proof_tree) =>

6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu lid -> sublogics -> InclComorphism lid sublogics

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedermkIdComorphism lid sub = InclComorphism

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder { inclusion_logic = lid

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , inclusion_source_sublogic = sub

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , inclusion_target_sublogic = sub }

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich-- | construction of an inclusion comorphism

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichmkInclComorphism :: (Logic lid sublogics

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich basic_spec sentence symb_items symb_map_items

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich sign morphism symbol raw_symbol proof_tree,

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich Monad m) =>

da955132262baab309a50fdffe228c9efe68251dCui Jian lid -> sublogics -> sublogics

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich -> m (InclComorphism lid sublogics)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichmkInclComorphism lid srcSub trgSub =

da955132262baab309a50fdffe228c9efe68251dCui Jian if isSubElem srcSub trgSub

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder then return InclComorphism

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder { inclusion_logic = lid

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , inclusion_source_sublogic = srcSub

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , inclusion_target_sublogic = trgSub }

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

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich "subElem of the second sublogic")

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich

3946c010d94321f14139e12061dd4261a3cc7295Christian Maederinstance (Language lid, Eq sublogics, Show sublogics, SublogicName sublogics)

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder => Language (InclComorphism lid sublogics) where

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder language_name (InclComorphism lid sub_src sub_trg) =

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder let sblName = sublogicName sub_src

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder lname = language_name lid

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder in if sub_src == sub_trg

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder then "id_" ++ lname ++

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder if null sblName then "" else '.' : sblName

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder else "incl_" ++ lname ++ ':'

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder : sblName ++ "->" ++ sublogicName sub_trg

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree =>

6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu Comorphism (InclComorphism lid sublogics)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid sublogics

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid sublogics

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sign morphism symbol raw_symbol proof_tree

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski where

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich sourceLogic = inclusion_logic

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich targetLogic = inclusion_logic

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich sourceSublogic = inclusion_source_sublogic

3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder mapSublogic cid subl =

3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder if isSubElem subl $ inclusion_source_sublogic cid

3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder then Just subl

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich else Nothing

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder map_theory _ = return

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder map_morphism _ = return

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder map_sentence _ _ = return

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu map_symbol _ _ = Set.singleton

da955132262baab309a50fdffe228c9efe68251dCui Jian constituents cid =

da955132262baab309a50fdffe228c9efe68251dCui Jian if inclusion_source_sublogic cid

da955132262baab309a50fdffe228c9efe68251dCui Jian == inclusion_target_sublogic cid

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich then []

da955132262baab309a50fdffe228c9efe68251dCui Jian else [language_name cid]

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu is_model_transportable _ = True

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu has_model_expansion _ = True

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu is_weakly_amalgamable _ = True

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder isInclusionComorphism _ = True

da955132262baab309a50fdffe228c9efe68251dCui Jian

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederdata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder

ca8550c6d47234042130bdc10a152806ecbc9832Christian Maederinstance (Language cid1, Language cid2)

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder => Language (CompComorphism cid1 cid2) where

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder language_name (CompComorphism cid1 cid2) =

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder language_name cid1 ++ ";" ++ language_name cid2

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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism cid2

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder 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)

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder => Comorphism (CompComorphism cid1 cid2)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sourceLogic (CompComorphism cid1 _) =

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski sourceLogic cid1

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder targetLogic (CompComorphism _ cid2) =

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski targetLogic cid2

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder sourceSublogic (CompComorphism cid1 _) =

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic cid1

bba825b39570777866d560bfde3807731131097eKlaus Luettich mapSublogic (CompComorphism cid1 cid2) sl =

da955132262baab309a50fdffe228c9efe68251dCui Jian mapSublogic cid1 sl >>=

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder mapSublogic cid2 .

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2)

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder map_sentence (CompComorphism cid1 cid2) si1 se1 =

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

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder se2 <- map_sentence cid1 si1 se1

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (si2', se2') <- coerceBasicTheory

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (targetLogic cid1) (sourceLogic cid2)

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

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder case se2' of

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder [x] -> map_sentence cid2 si2' $ sentence x

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder _ -> error "CompComorphism.map_sentence"

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder map_theory (CompComorphism cid1 cid2) ti1 =

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder do ti2 <- map_theory cid1 ti1

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

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder "Mapping theory along comorphism" ti2

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder wrapMapTheory cid2 ti2'

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder map_morphism (CompComorphism cid1 cid2) m1 =

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder do m2 <- map_morphism cid1 m1

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2)

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski "Mapping signature morphism along comorphism"m2

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder map_morphism cid2 m3

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu map_symbol (CompComorphism cid1 cid2) sig1 = let

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu th = map_sign cid1 sig1 in

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu case maybeResult th of

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu Nothing -> error "failed translating signature"

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu Just (sig2', _) -> let

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu th2 = coerceBasicTheory

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu (targetLogic cid1) (sourceLogic cid2)

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

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu in case maybeResult th2 of

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu Nothing -> error "failed coercing"

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu Just (sig2, _) ->

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu \ s1 ->

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu let mycast = coerceSymbol (targetLogic cid1) (sourceLogic cid2)

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu in Set.unions

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu (map (map_symbol cid2 sig2 . mycast)

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu (Set.toList (map_symbol cid1 sig1 s1)))

63324a97283728a30932828a612c7b0b0f687624Christian Maeder

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder extractModel (CompComorphism cid1 cid2) sign pt3 =

53f347ab16f992d909f47a50bf2059f57f3c7ad0Christian Maeder let lid1 = sourceLogic cid1

0cd4575fe679a26de63d9a75a4d66d8366f79ab8Christian Maeder lid3 = sourceLogic cid2

0cd4575fe679a26de63d9a75a4d66d8366f79ab8Christian Maeder in if language_name lid1 == language_name lid3 then do

0cd4575fe679a26de63d9a75a4d66d8366f79ab8Christian Maeder bTh1 <- map_sign cid1 sign

0cd4575fe679a26de63d9a75a4d66d8366f79ab8Christian Maeder (sign1, _) <-

0cd4575fe679a26de63d9a75a4d66d8366f79ab8Christian Maeder coerceBasicTheory (targetLogic cid1) lid3 "extractModel1" bTh1

0cd4575fe679a26de63d9a75a4d66d8366f79ab8Christian Maeder bTh2 <- extractModel cid2 sign1 pt3

0cd4575fe679a26de63d9a75a4d66d8366f79ab8Christian Maeder coerceBasicTheory lid3 lid1 "extractModel2" bTh2

53f347ab16f992d909f47a50bf2059f57f3c7ad0Christian Maeder else fail $ "extractModel not implemented for comorphism composition with "

63324a97283728a30932828a612c7b0b0f687624Christian Maeder ++ language_name cid1

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder constituents (CompComorphism cid1 cid2) =

933baca0720dae81434de384b32a93b47e754d09Christian Maeder constituents cid1 ++ constituents cid2

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu

da955132262baab309a50fdffe228c9efe68251dCui Jian is_model_transportable (CompComorphism cid1 cid2) =

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu is_model_transportable cid1 && is_model_transportable cid2

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu

da955132262baab309a50fdffe228c9efe68251dCui Jian has_model_expansion (CompComorphism cid1 cid2) =

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu has_model_expansion cid1 && has_model_expansion cid2

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu

da955132262baab309a50fdffe228c9efe68251dCui Jian is_weakly_amalgamable (CompComorphism cid1 cid2) =

da955132262baab309a50fdffe228c9efe68251dCui Jian is_weakly_amalgamable cid1 && is_weakly_amalgamable cid2

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder isInclusionComorphism (CompComorphism cid1 cid2) =

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder isInclusionComorphism cid1 && isInclusionComorphism cid2

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- * Comorphisms and existential types for the logic graph

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | Existential type for comorphisms

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederdata AnyComorphism = forall cid lid1 sublogics1

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid2 sublogics2

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Comorphism cid

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid1 sublogics1 basic_spec1 sentence1

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder symb_items1 symb_map_items1

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid2 sublogics2 basic_spec2 sentence2

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder symb_items2 symb_map_items2

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Comorphism cid deriving Typeable -- used for GTheory

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Eq AnyComorphism where

a9183ce3b997bf3539e427b3cd22d70c3565446eChristian Maeder a == b = compare a b == EQ

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Ord AnyComorphism where

a9183ce3b997bf3539e427b3cd22d70c3565446eChristian Maeder compare (Comorphism cid1) (Comorphism cid2) = compare

a9183ce3b997bf3539e427b3cd22d70c3565446eChristian Maeder (language_name cid1, constituents cid1)

a9183ce3b997bf3539e427b3cd22d70c3565446eChristian Maeder (language_name cid2, constituents cid2)

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

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Show AnyComorphism where

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder show (Comorphism cid) = language_name cid

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ++ " : " ++ language_name (sourceLogic cid)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ++ " -> " ++ language_name (targetLogic cid)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Pretty AnyComorphism where

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder pretty = text . show

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | compute the identity comorphism for a logic

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederidComorphism :: AnyLogic -> AnyComorphism

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederidComorphism (Logic lid) = Comorphism (mkIdComorphism lid (top_sublogic lid))

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | Test whether a comporphism is the identity

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederisIdComorphism :: AnyComorphism -> Bool

3946c010d94321f14139e12061dd4261a3cc7295Christian MaederisIdComorphism (Comorphism cid) = null $ constituents cid

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- * Properties of comorphisms

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | Test whether a comorphism is model-transportable

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederisModelTransportable :: AnyComorphism -> Bool

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederisModelTransportable (Comorphism cid) = is_model_transportable cid

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | Test whether a comorphism has model expansion

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederhasModelExpansion :: AnyComorphism -> Bool

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederhasModelExpansion (Comorphism cid) = has_model_expansion cid

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | Test whether a comorphism is weakly amalgamable

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederisWeaklyAmalgamable :: AnyComorphism -> Bool

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederisWeaklyAmalgamable (Comorphism cid) = is_weakly_amalgamable cid

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | Compose comorphisms

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedercompComorphism :: Monad m => AnyComorphism -> AnyComorphism -> m AnyComorphism

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedercompComorphism (Comorphism cid1) (Comorphism cid2) =

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder let l1 = targetLogic cid1

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder l2 = sourceLogic cid2

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder msg = "ogic mismatch in composition of " ++ language_name cid1

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder ++ " and " ++ language_name cid2

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder in

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder if language_name l1 == language_name l2 then

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder if isSubElem (forceCoerceSublogic l1 l2 $ targetSublogic cid1)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder $ sourceSublogic cid2

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder then {- case (isIdComorphism cm1,isIdComorphism cm2) of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (True,_) -> return cm2

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (_,True) -> return cm1

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

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder else fail $ "Subl" ++ msg

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder else fail $ 'L' : msg