967e5f3c25249c779575864692935627004d3f9eChristian Maeder{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

967e5f3c25249c779575864692935627004d3f9eChristian Maeder{- |

967e5f3c25249c779575864692935627004d3f9eChristian MaederModule : $Header$

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiDescription : central interface (type class) for logic translations (comorphisms) in Hets

967e5f3c25249c779575864692935627004d3f9eChristian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006

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

967e5f3c25249c779575864692935627004d3f9eChristian MaederMaintainer : till@tzi.de

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederStability : provisional

967e5f3c25249c779575864692935627004d3f9eChristian MaederPortability : non-portable (via Logic)

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian MaederCentral interface (type class) for logic translations (comorphisms) in Hets

967e5f3c25249c779575864692935627004d3f9eChristian Maeder These are just collections of

967e5f3c25249c779575864692935627004d3f9eChristian Maeder functions between (some of) the types of logics.

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian Maeder References: see Logic.hs

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder-}

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maedermodule Logic.Comorphism ( CompComorphism(..)

ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder , IdComorphism

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder , InclComorphism

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder , inclusion_logic

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder , inclusion_source_sublogic

997c56f3bc74a703043010978e5013fdb074d659Christian Maeder , inclusion_target_sublogic

967e5f3c25249c779575864692935627004d3f9eChristian Maeder , mkInclComorphism

9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowski , mkIdComorphism

9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowski , Comorphism(..)

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder , targetSublogic

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder , map_sign

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , mapDefaultMorphism

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder -- , failMapSentence

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder -- , errMapSymbol

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , wrapMapTheory

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , simpleTheoryMapping

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , mkTheoryMapping) where

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maederimport Logic.Logic

967e5f3c25249c779575864692935627004d3f9eChristian Maederimport Logic.Coerce

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maederimport qualified Data.Set as Set

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederimport Common.Result

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederimport Common.ProofUtils

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederimport Common.AS_Annotation

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Common.Doc

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederimport Common.DocUtils

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederclass (Language cid,

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder Logic lid1 sublogics1

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder Logic lid2 sublogics2

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder Comorphism cid

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder where

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder -- source and target logic and sublogic

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

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder sourceLogic :: cid -> lid1

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder sourceSublogic :: cid -> sublogics1

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder targetLogic :: cid -> lid2

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

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder -- this function must be partial because mapTheory is partial

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder mapSublogic :: cid -> sublogics1 -> Maybe sublogics2

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder -- the translation functions are partial

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder -- because the target may be a sublanguage

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2

d17834302eaa101395b4b806cd73670fd864445fChristian Maeder -- cover theoroidal comorphisms as well

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

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

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder map_morphism :: cid -> morphism1 -> Result morphism2

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder -- also covers semi-comorphisms

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder -- with no sentence translation

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder -- - but these are spans!

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder map_symbol :: cid -> symbol1 -> Set.Set symbol2

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder --properties of comorphisms

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder is_model_transportable :: cid -> Bool

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

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder -- if for any signature \Sigma, any \Sigma-model M and any \phi(\Sigma)-model N

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

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

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder has_model_expansion :: cid -> Bool

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder is_weakly_amalgamable :: cid -> Bool

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder --default implementation for properties

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder is_model_transportable _ = False

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder has_model_expansion _ = False

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder is_weakly_amalgamable _ = False

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder constituents :: cid -> [String]

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder -- default implementation

967e5f3c25249c779575864692935627004d3f9eChristian Maeder constituents cid = [language_name cid]

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder map_sentence = failMapSentence

967e5f3c25249c779575864692935627004d3f9eChristian Maeder map_symbol = errMapSymbol

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder

a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder

83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedertargetSublogic :: Comorphism cid

967e5f3c25249c779575864692935627004d3f9eChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder => cid -> sublogics2

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedertargetSublogic cid = maybe (error ("Logic.Comorphism: " ++

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder language_name cid ++

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder " does not provide a mapping for it's " ++

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder "source sublogic"))

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder id $ mapSublogic cid $ sourceSublogic cid

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

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

a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maedermap_sign :: Comorphism cid

a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

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

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maedermap_sign cid sign = wrapMapTheory cid (sign,[])

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedermapDefaultMorphism :: Comorphism cid

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder => cid -> morphism1 -> Result morphism2

7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermapDefaultMorphism cid mor = do

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder let src = sourceLogic cid

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder (sig1, _) <- map_sign cid $ dom src mor

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

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder inclusion (targetLogic cid) sig1 sig2

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder

bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskifailMapSentence :: Comorphism cid

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder => cid -> sign1 -> sentence1 -> Result sentence2

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederfailMapSentence cid _ _ =

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder fail $ "Unsupported sentence translation " ++ show cid

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedererrMapSymbol :: Comorphism cid

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder => cid -> symbol1 -> Set.Set symbol2

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

e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder

e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder-- | use this function instead of 'map_theory'

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederwrapMapTheory :: Comorphism cid

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2

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

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

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederwrapMapTheory cid (sign, sens) =

e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder case sourceSublogic cid of

e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder sub -> case minSublogic sign of

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder sigLog -> case foldl join sigLog

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder $ map (minSublogic . sentence) sens of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder senLog ->

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder if isSubElem senLog sub

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder then map_theory cid (sign, sens)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder else fail $ "for '" ++ language_name cid ++

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder "' expected sublogic '" ++

967e5f3c25249c779575864692935627004d3f9eChristian Maeder concat (sublogic_names sub) ++

967e5f3c25249c779575864692935627004d3f9eChristian Maeder "'\n but found sublogic '" ++

967e5f3c25249c779575864692935627004d3f9eChristian Maeder concat (sublogic_names senLog) ++

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder "' with signature sublogic '" ++

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder concat (sublogic_names sigLog) ++ "'\n" ++

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder show (vcat $ pretty sign : map

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (print_named $ sourceLogic cid) sens)

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedersimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder -> (sign1, [Named sentence1])

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder -> (sign2, [Named sentence2])

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedersimpleTheoryMapping mapSig mapSen (sign,sens) =

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (mapSig sign, map (mapNamed mapSen) sens)

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder

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

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

967e5f3c25249c779575864692935627004d3f9eChristian Maeder -> (sign1, [Named sentence1])

967e5f3c25249c779575864692935627004d3f9eChristian Maeder -> m (sign2, [Named sentence2])

7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermkTheoryMapping mapSig mapSen (sign,sens) = do

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (sign',sens') <- mapSig sign

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

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder return (sign', disambiguateSens Set.empty . nameSens $ sens' ++ sens'')

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maedertype IdComorphism lid sublogics = InclComorphism lid sublogics

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maederdata InclComorphism lid sublogics =

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder InclComorphism { inclusion_logic :: lid

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder , inclusion_source_sublogic :: sublogics

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder , inclusion_target_sublogic :: sublogics

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder }

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder-- | construction of an identity comorphism

83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermkIdComorphism :: (Logic lid sublogics

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder basic_spec sentence symb_items symb_map_items

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder sign morphism symbol raw_symbol proof_tree) =>

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder lid -> sublogics -> IdComorphism lid sublogics

83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermkIdComorphism lid sub =

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder InclComorphism { inclusion_logic = lid

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , inclusion_source_sublogic = sub

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , inclusion_target_sublogic = sub

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder }

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder-- | construction of an inclusion comorphism

83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermkInclComorphism :: (Logic lid sublogics

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder basic_spec sentence symb_items symb_map_items

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder sign morphism symbol raw_symbol proof_tree,

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Monad m) =>

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder lid -> sublogics -> sublogics

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder -> m (InclComorphism lid sublogics)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermkInclComorphism lid srcSub trgSub =

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder if isSubElem srcSub trgSub

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder then return $ InclComorphism { inclusion_logic = lid

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder , inclusion_source_sublogic = srcSub

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder , inclusion_target_sublogic = trgSub

967e5f3c25249c779575864692935627004d3f9eChristian Maeder }

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

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder "subElem of the second sublogic")

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maederinstance Logic lid sublogics

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder basic_spec sentence symb_items symb_map_items

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder sign morphism symbol raw_symbol proof_tree =>

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder Show (InclComorphism lid sublogics)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder where

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder show = language_name

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederinstance Logic lid sublogics

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder basic_spec sentence symb_items symb_map_items

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder sign morphism symbol raw_symbol proof_tree =>

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder Language (InclComorphism lid sublogics) where

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder language_name (InclComorphism lid sub_src sub_trg) =

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder if sub_src == sub_trg

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder then "id_" ++ language_name lid ++

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder if null (sblName sub_src)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder then "" else "." ++ (sblName sub_src)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder else "incl_" ++ language_name lid ++ ": " ++

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder sblName sub_src ++ " -> " ++ sblName sub_trg

where sblName sub = case sublogic_names sub of

[] -> error "language_name IdComorphism"

h : _ -> h

instance Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

Comorphism (IdComorphism 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 incC subl =

if subl == inclusion_source_sublogic incC

then Just $ inclusion_target_sublogic incC

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

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) = \ s1 ->

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

in Set.unions

(map (map_symbol cid2 . mycast)

(Set.toList (map_symbol cid1 s1)))

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