020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett , FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowski{- |

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettModule : $Header$

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettDescription : interface and class for logic translations

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettMaintainer : till@informatik.uni-bremen.de

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettStability : provisional

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettPortability : non-portable (via Logic)

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettCentral interface (type class) for logic translations (comorphisms) in Hets

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett These are just collections of

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett functions between (some of) the types of logics.

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett References: see Logic.hs

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett-}

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettmodule Logic.Comorphism

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett ( CompComorphism (..)

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett , InclComorphism

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett , inclusion_logic

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett , inclusion_source_sublogic

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett , inclusion_target_sublogic

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett , mkInclComorphism

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , mkIdComorphism

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , Comorphism (..)

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , targetSublogic

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , map_sign

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , ext_map_sign

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , mapDefaultMorphism

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , wrapMapTheory

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , simpleTheoryMapping

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , mkTheoryMapping

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , AnyComorphism (..)

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , idComorphism

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , isIdComorphism

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , isModelTransportable

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , hasModelExpansion

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , isWeaklyAmalgamable

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , compComorphism

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett ) where

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Logic.Logic

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Logic.Coerce

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Logic.ExtSign

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.AS_Annotation

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.Doc

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.DocUtils

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.ExtSign

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.Id

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.ProofUtils

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.Result

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Data.Maybe

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport qualified Data.Set as Set

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Data.Typeable

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettclass (Language cid,

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett Logic lid1 sublogics1

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett basic_spec1 sentence1 symb_items1 symb_map_items1

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett Logic lid2 sublogics2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett basic_spec2 sentence2 symb_items2 symb_map_items2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett Comorphism cid

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett where

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -- source and target logic and sublogic

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -- the source sublogic is the maximal one for which the comorphism works

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett sourceLogic :: cid -> lid1

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett sourceSublogic :: cid -> sublogics1

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett targetLogic :: cid -> lid2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -- finer information of target sublogics corresponding to source sublogics

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -- this function must be partial because mapTheory is partial

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett mapSublogic :: cid -> sublogics1 -> Maybe sublogics2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -- the translation functions are partial

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -- because the target may be a sublanguage

29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy Gimblett -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -- cover theoroidal comorphisms as well

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett map_theory :: cid -> (sign1,[Named sentence1])

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -> Result (sign2,[Named sentence2])

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett map_morphism :: cid -> morphism1 -> Result morphism2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -- also covers semi-comorphisms

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -- with no sentence translation

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -- - but these are spans!

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett map_sentence = failMapSentence

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett map_symbol :: cid -> sign1 -> symbol1 -> Set.Set symbol2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett map_symbol = errMapSymbol

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett extractModel :: cid -> sign1 -> proof_tree2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -> Result (sign1, [Named sentence1])

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett extractModel cid _ _ = fail

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett $ "extractModel not implemented for comorphism "

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett ++ language_name cid

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett --properties of comorphisms

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett is_model_transportable :: cid -> Bool

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

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -- if for any signature \Sigma,

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -- any \Sigma-model M and any \phi(\Sigma)-model N

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

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

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett is_model_transportable _ = False

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett has_model_expansion :: cid -> Bool

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett has_model_expansion _ = False

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett is_weakly_amalgamable :: cid -> Bool

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett is_weakly_amalgamable _ = False

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett constituents :: cid -> [String]

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett constituents cid = [language_name cid]

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett isInclusionComorphism :: cid -> Bool

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett isInclusionComorphism _ = False

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy GimbletttargetSublogic :: Comorphism cid

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett => cid -> sublogics2

f909337bf7012aca169c0b56b89efbd4a310f8daAndy GimbletttargetSublogic cid = fromMaybe (top_sublogic $ targetLogic cid)

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett $ mapSublogic cid $ sourceSublogic cid

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett

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

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettmap_sign :: Comorphism cid

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2

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

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettmap_sign cid sign = wrapMapTheory cid (sign,[])

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettext_map_sign :: Comorphism cid

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett => cid -> ExtSign sign1 symbol1

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

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettext_map_sign cid (ExtSign sign _) = do

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett (sign2, sens2) <- map_sign cid sign

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett return (makeExtSign (targetLogic cid) sign2, sens2)

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett

2f06b54890375b6cac90394b80b07bd451d728fcAndy GimblettmapDefaultMorphism :: Comorphism cid

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett sign2 morphism2 symbol2 raw_symbol2 proof_tree2

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett => cid -> morphism1 -> Result morphism2

mapDefaultMorphism cid mor = do

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

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

inclusion (targetLogic cid) sig1 sig2

failMapSentence :: Comorphism cid

lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2

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

failMapSentence cid _ _ =

fail $ "Unsupported sentence translation " ++ show cid

errMapSymbol :: Comorphism cid

lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2

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

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

-- | use this function instead of 'map_theory'

wrapMapTheory :: Comorphism cid

lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2

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

-> Result (sign2, [Named sentence2])

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

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

sub -> case minSublogic sign of

sigLog -> case foldl join sigLog

$ map (minSublogic . sentence) sens of

senLog ->

if isSubElem senLog sub

then res

else Result

[ Diag Hint

(show (vcat $ pretty sign : map

(print_named $ sourceLogic cid) sens))

nullRange

, Diag Error

("for '" ++ language_name cid ++

"' expected sublogic '" ++

sublogicName sub ++

"'\n but found sublogic '" ++

sublogicName senLog ++

"' with signature sublogic '" ++

sublogicName sigLog ++ "'") nullRange] Nothing

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

-> (sign1, [Named sentence1])

-> (sign2, [Named sentence2])

simpleTheoryMapping mapSig mapSen (sign,sens) =

(mapSig sign, map (mapNamed mapSen) sens)

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

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

-> (sign1, [Named sentence1])

-> m (sign2, [Named sentence2])

mkTheoryMapping mapSig mapSen (sign,sens) = do

(sign',sens') <- mapSig sign

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

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

data InclComorphism lid sublogics = InclComorphism

{ inclusion_logic :: lid

, inclusion_source_sublogic :: sublogics

, inclusion_target_sublogic :: sublogics }

deriving Show

-- | construction of an identity comorphism

mkIdComorphism :: (Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree) =>

lid -> sublogics -> InclComorphism lid sublogics

mkIdComorphism lid sub = InclComorphism

{ inclusion_logic = lid

, inclusion_source_sublogic = sub

, inclusion_target_sublogic = sub }

-- | construction of an inclusion comorphism

mkInclComorphism :: (Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree,

Monad m) =>

lid -> sublogics -> sublogics

-> m (InclComorphism lid sublogics)

mkInclComorphism lid srcSub trgSub =

if isSubElem srcSub trgSub

then return InclComorphism

{ inclusion_logic = lid

, inclusion_source_sublogic = srcSub

, inclusion_target_sublogic = trgSub }

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

"subElem of the second sublogic")

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

=> Language (InclComorphism lid sublogics) where

language_name (InclComorphism lid sub_src sub_trg) =

let sblName = sublogicName sub_src

lname = language_name lid

in if sub_src == sub_trg

then "id_" ++ lname ++

if null sblName then "" else '.' : sblName

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

: sblName ++ "->" ++ sublogicName sub_trg

instance Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

Comorphism (InclComorphism lid sublogics)

lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

where

sourceLogic = inclusion_logic

targetLogic = inclusion_logic

sourceSublogic = inclusion_source_sublogic

mapSublogic cid subl =

if isSubElem subl $ inclusion_source_sublogic cid

then Just subl

else Nothing

map_theory _ = return

map_morphism _ = return

map_sentence _ _ = return

map_symbol _ _ = Set.singleton

constituents cid =

if inclusion_source_sublogic cid

== inclusion_target_sublogic cid

then []

else [language_name cid]

is_model_transportable _ = True

has_model_expansion _ = True

is_weakly_amalgamable _ = True

isInclusionComorphism _ = True

data CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show

instance (Language cid1, Language cid2)

=> Language (CompComorphism cid1 cid2) where

language_name (CompComorphism cid1 cid2) =

language_name cid1 ++ ";" ++ language_name cid2

instance (Comorphism cid1

lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

Comorphism cid2

lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4

sign4 morphism4 symbol4 raw_symbol4 proof_tree4

lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

sign3 morphism3 symbol3 raw_symbol3 proof_tree3)

=> Comorphism (CompComorphism cid1 cid2)

lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where

sourceLogic (CompComorphism cid1 _) =

sourceLogic cid1

targetLogic (CompComorphism _ cid2) =

targetLogic cid2

sourceSublogic (CompComorphism cid1 _) =

sourceSublogic cid1

mapSublogic (CompComorphism cid1 cid2) sl =

mapSublogic cid1 sl >>=

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 {- case (isIdComorphism cm1,isIdComorphism cm2) of

(True,_) -> return cm2

(_,True) -> return cm1

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

else fail $ "Subl" ++ msg

else fail $ 'L' : msg