da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw{- |

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwModule : $Header$

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwDescription : interface and class for logic translations

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwLicense : GPLv2 or higher, see LICENSE.txt

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwMaintainer : till@informatik.uni-bremen.de

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwStability : provisional

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwPortability : non-portable (via Logic)

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwCentral interface (type class) for logic translations (comorphisms) in Hets

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw These are just collections of

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw functions between (some of) the types of logics.

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw References: see Logic.hs

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw-}

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwmodule Logic.Comorphism

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw ( CompComorphism (..)

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , InclComorphism

416953930b8cfea779e8a7dfdefafc1c6479926cGordon Ross , inclusion_logic

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright , inclusion_source_sublogic

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , inclusion_target_sublogic

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , mkInclComorphism

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , mkIdComorphism

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , Comorphism (..)

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , targetSublogic

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , map_sign

08344b293eab865a57e4629b178f2003dced397eGordon Ross , wrapMapTheory

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , mkTheoryMapping

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , AnyComorphism (..)

94fff7907278e4540aa7abee2b1b0ea71d36f7faAlan Wright , idComorphism

bbf6f00c25b6a2bed23c35eac6d62998ecdb338cJordan Brown , isIdComorphism

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , isModelTransportable

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb , hasModelExpansion

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , isWeaklyAmalgamable

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , compComorphism

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw ) where

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb

faa1795a28a5c712eed6d0a3f84d98c368a316c6jbimport Logic.Logic

faa1795a28a5c712eed6d0a3f84d98c368a316c6jbimport Logic.Coerce

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwimport Common.AS_Annotation

faa1795a28a5c712eed6d0a3f84d98c368a316c6jbimport Common.Doc

faa1795a28a5c712eed6d0a3f84d98c368a316c6jbimport Common.DocUtils

faa1795a28a5c712eed6d0a3f84d98c368a316c6jbimport Common.Id

faa1795a28a5c712eed6d0a3f84d98c368a316c6jbimport Common.LibName

faa1795a28a5c712eed6d0a3f84d98c368a316c6jbimport Common.ProofUtils

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwimport Common.Result

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb

faa1795a28a5c712eed6d0a3f84d98c368a316c6jbimport Data.Maybe

faa1795a28a5c712eed6d0a3f84d98c368a316c6jbimport qualified Data.Set as Set

faa1795a28a5c712eed6d0a3f84d98c368a316c6jbimport Data.Typeable

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb

faa1795a28a5c712eed6d0a3f84d98c368a316c6jbclass (Language cid,

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb Logic lid1 sublogics1

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb basic_spec1 sentence1 symb_items1 symb_map_items1

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh Logic lid2 sublogics2

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb basic_spec2 sentence2 symb_items2 symb_map_items2

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh Comorphism cid

2c2961f8403049d948b9f3e6c35d6488b6b7e1aajose borrego lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh sign1 morphism1 symbol1 raw_symbol1 proof_tree1

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb sign2 morphism2 symbol2 raw_symbol2 proof_tree2

c8ec8eea9849cac239663c46be8a7f5d2ba7ca00jose borrego | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

416953930b8cfea779e8a7dfdefafc1c6479926cGordon Ross sign1 morphism1 symbol1 raw_symbol1 proof_tree1

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

2c2961f8403049d948b9f3e6c35d6488b6b7e1aajose borrego sign2 morphism2 symbol2 raw_symbol2 proof_tree2

2c2961f8403049d948b9f3e6c35d6488b6b7e1aajose borrego where

2c2961f8403049d948b9f3e6c35d6488b6b7e1aajose borrego {- source and target logic and sublogic

2c2961f8403049d948b9f3e6c35d6488b6b7e1aajose borrego the source sublogic is the maximal one for which the comorphism works -}

2c2961f8403049d948b9f3e6c35d6488b6b7e1aajose borrego sourceLogic :: cid -> lid1

2c2961f8403049d948b9f3e6c35d6488b6b7e1aajose borrego sourceSublogic :: cid -> sublogics1

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb sourceSublogic cid = top_sublogic $ sourceLogic cid

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh minSourceTheory :: cid -> Maybe (LibName, String)

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh minSourceTheory _ = Nothing

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh targetLogic :: cid -> lid2

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh {- finer information of target sublogics corresponding to source sublogics

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh this function must be partial because mapTheory is partial -}

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh mapSublogic :: cid -> sublogics1 -> Maybe sublogics2

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh mapSublogic cid _ = Just $ top_sublogic $ targetLogic cid

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh {- the translation functions are partial

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh because the target may be a sublanguage

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh cover theoroidal comorphisms as well -}

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh map_theory :: cid -> (sign1, [Named sentence1])

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh -> Result (sign2, [Named sentence2])

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh map_morphism :: cid -> morphism1 -> Result morphism2

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh map_morphism = mapDefaultMorphism

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

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh {- also covers semi-comorphisms

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh with no sentence translation

08344b293eab865a57e4629b178f2003dced397eGordon Ross - but these are spans! -}

08344b293eab865a57e4629b178f2003dced397eGordon Ross map_sentence = failMapSentence

08344b293eab865a57e4629b178f2003dced397eGordon Ross map_symbol :: cid -> sign1 -> symbol1 -> Set.Set symbol2

08344b293eab865a57e4629b178f2003dced397eGordon Ross map_symbol = errMapSymbol

08344b293eab865a57e4629b178f2003dced397eGordon Ross extractModel :: cid -> sign1 -> proof_tree2

08344b293eab865a57e4629b178f2003dced397eGordon Ross -> Result (sign1, [Named sentence1])

08344b293eab865a57e4629b178f2003dced397eGordon Ross extractModel cid _ _ = fail

08344b293eab865a57e4629b178f2003dced397eGordon Ross $ "extractModel not implemented for comorphism "

08344b293eab865a57e4629b178f2003dced397eGordon Ross ++ language_name cid

08344b293eab865a57e4629b178f2003dced397eGordon Ross -- properties of comorphisms

08344b293eab865a57e4629b178f2003dced397eGordon Ross is_model_transportable :: cid -> Bool

08344b293eab865a57e4629b178f2003dced397eGordon Ross {- a comorphism (\phi, \alpha, \beta) is model-transportable

08344b293eab865a57e4629b178f2003dced397eGordon Ross if for any signature \Sigma,

08344b293eab865a57e4629b178f2003dced397eGordon Ross any \Sigma-model M and any \phi(\Sigma)-model N

08344b293eab865a57e4629b178f2003dced397eGordon Ross for any isomorphism h : \beta_\Sigma(N) -> M

08344b293eab865a57e4629b178f2003dced397eGordon Ross there exists an isomorphism h': N -> M' such that \beta_\Sigma(h') = h -}

08344b293eab865a57e4629b178f2003dced397eGordon Ross is_model_transportable _ = False

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh has_model_expansion :: cid -> Bool

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb has_model_expansion _ = False

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb is_weakly_amalgamable :: cid -> Bool

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb is_weakly_amalgamable _ = False

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb constituents :: cid -> [String]

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb constituents cid = [language_name cid]

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb isInclusionComorphism :: cid -> Bool

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw isInclusionComorphism _ = False

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwtargetSublogic :: Comorphism cid

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign1 morphism1 symbol1 raw_symbol1 proof_tree1

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign2 morphism2 symbol2 raw_symbol2 proof_tree2

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw => cid -> sublogics2

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwtargetSublogic cid = fromMaybe (top_sublogic $ targetLogic cid)

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw $ mapSublogic cid $ sourceSublogic cid

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw-- | this function is base on 'map_theory' using no sentences as input

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwmap_sign :: Comorphism cid

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign1 morphism1 symbol1 raw_symbol1 proof_tree1

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign2 morphism2 symbol2 raw_symbol2 proof_tree2

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

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwmap_sign cid sign = wrapMapTheory cid (sign, [])

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwmapDefaultMorphism :: Comorphism cid

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign1 morphism1 symbol1 raw_symbol1 proof_tree1

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign2 morphism2 symbol2 raw_symbol2 proof_tree2

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw => cid -> morphism1 -> Result morphism2

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwmapDefaultMorphism cid mor = do

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

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

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw inclusion (targetLogic cid) sig1 sig2

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwfailMapSentence :: Comorphism cid

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

193974072f41a843678abf5f61979c748687e66bSherry Moore sign1 morphism1 symbol1 raw_symbol1 proof_tree1

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign2 morphism2 symbol2 raw_symbol2 proof_tree2

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

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwfailMapSentence cid _ _ =

193974072f41a843678abf5f61979c748687e66bSherry Moore fail $ "Unsupported sentence translation " ++ show cid

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwerrMapSymbol :: Comorphism cid

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign1 morphism1 symbol1 raw_symbol1 proof_tree1

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign2 morphism2 symbol2 raw_symbol2 proof_tree2

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

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

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw-- | use this function instead of 'map_theory'

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwwrapMapTheory :: Comorphism cid

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb sign1 morphism1 symbol1 raw_symbol1 proof_tree1

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb sign2 morphism2 symbol2 raw_symbol2 proof_tree2

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

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw -> Result (sign2, [Named sentence2])

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwwrapMapTheory cid (sign, sens) =

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw let res = map_theory cid (sign, sens)

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid1 = sourceLogic cid

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

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright in

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright if isIdComorphism $ Comorphism cid then res else case sourceSublogic cid of

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright sub -> case minSublogic sign of

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright sigLog -> case foldl join sigLog

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright $ map (minSublogic . sentence) sens of

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright senLog ->

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright if isSubElem senLog sub

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright then res

f9a15d2c042edba37d61b071eb7ea274eb2754d1jose borrego else Result

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright [ Diag Hint thDoc nullRange

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright , Diag Error

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright ("for '" ++ language_name cid ++

f9a15d2c042edba37d61b071eb7ea274eb2754d1jose borrego "' expected sublogic '" ++

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright sublogicName sub ++

f9a15d2c042edba37d61b071eb7ea274eb2754d1jose borrego "'\n but found sublogic '" ++

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sublogicName senLog ++

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw "' with signature sublogic '" ++

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sublogicName sigLog ++ "'") nullRange] Nothing

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

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

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

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw -> (sign1, [Named sentence1])

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw -> m (sign2, [Named sentence2])

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwmkTheoryMapping mapSig mapSen (sign, sens) = do

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw (sign', sens') <- mapSig sign

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

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

f9a15d2c042edba37d61b071eb7ea274eb2754d1jose borrego

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wrightdata InclComorphism lid sublogics = InclComorphism

f9a15d2c042edba37d61b071eb7ea274eb2754d1jose borrego { inclusion_logic :: lid

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright , inclusion_source_sublogic :: sublogics

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright , inclusion_target_sublogic :: sublogics }

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright deriving Show

f9a15d2c042edba37d61b071eb7ea274eb2754d1jose borrego

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw-- | construction of an identity comorphism

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwmkIdComorphism :: (Logic lid sublogics

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw basic_spec sentence symb_items symb_map_items

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb sign morphism symbol raw_symbol proof_tree) =>

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb lid -> sublogics -> InclComorphism lid sublogics

faa1795a28a5c712eed6d0a3f84d98c368a316c6jbmkIdComorphism lid sub = InclComorphism

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw { inclusion_logic = lid

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , inclusion_source_sublogic = sub

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , inclusion_target_sublogic = sub }

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw-- | construction of an inclusion comorphism

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwmkInclComorphism :: (Logic lid sublogics

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw basic_spec sentence symb_items symb_map_items

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign morphism symbol raw_symbol proof_tree,

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb Monad m) =>

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid -> sublogics -> sublogics

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw -> m (InclComorphism lid sublogics)

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwmkInclComorphism lid srcSub trgSub =

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw if isSubElem srcSub trgSub

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw then return InclComorphism

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb { inclusion_logic = lid

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , inclusion_source_sublogic = srcSub

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw , inclusion_target_sublogic = trgSub }

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

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw "subElem of the second sublogic")

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

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

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb => Language (InclComorphism lid sublogics) where

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw language_name (InclComorphism lid sub_src sub_trg) =

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw let sblName = sublogicName sub_src

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb lname = language_name lid

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw in if sub_src == sub_trg

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright then "id_" ++ lname ++

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

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

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright : sblName ++ "->" ++ sublogicName sub_trg

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wrightinstance Logic lid sublogics

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright basic_spec sentence symb_items symb_map_items

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb sign morphism symbol raw_symbol proof_tree =>

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw Comorphism (InclComorphism lid sublogics)

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright lid sublogics

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright basic_spec sentence symb_items symb_map_items

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb sign morphism symbol raw_symbol proof_tree

94fff7907278e4540aa7abee2b1b0ea71d36f7faAlan Wright lid sublogics

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright basic_spec sentence symb_items symb_map_items

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright sign morphism symbol raw_symbol proof_tree

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright where

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright sourceLogic = inclusion_logic

94fff7907278e4540aa7abee2b1b0ea71d36f7faAlan Wright targetLogic = inclusion_logic

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright sourceSublogic = inclusion_source_sublogic

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright mapSublogic cid subl =

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright if isSubElem subl $ inclusion_source_sublogic cid

94fff7907278e4540aa7abee2b1b0ea71d36f7faAlan Wright then Just subl

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright else Nothing

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw map_theory _ = return

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb map_morphism _ = return

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb map_sentence _ _ = return

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright map_symbol _ _ = Set.singleton

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb constituents cid =

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb if inclusion_source_sublogic cid

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright == inclusion_target_sublogic cid

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb then []

9fb67ea305c66b6a297583b9b0db6796b0dfe497afshin salek ardakani - Sun Microsystems - Irvine United States else [language_name cid]

9fb67ea305c66b6a297583b9b0db6796b0dfe497afshin salek ardakani - Sun Microsystems - Irvine United States is_model_transportable _ = True

9fb67ea305c66b6a297583b9b0db6796b0dfe497afshin salek ardakani - Sun Microsystems - Irvine United States has_model_expansion _ = True

9fb67ea305c66b6a297583b9b0db6796b0dfe497afshin salek ardakani - Sun Microsystems - Irvine United States is_weakly_amalgamable _ = True

9fb67ea305c66b6a297583b9b0db6796b0dfe497afshin salek ardakani - Sun Microsystems - Irvine United States isInclusionComorphism _ = True

9fb67ea305c66b6a297583b9b0db6796b0dfe497afshin salek ardakani - Sun Microsystems - Irvine United States

faa1795a28a5c712eed6d0a3f84d98c368a316c6jbdata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wrightinstance (Language cid1, Language cid2)

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright => Language (CompComorphism cid1 cid2) where

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wright language_name (CompComorphism cid1 cid2) =

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright language_name cid1 ++ ";" ++ language_name cid2

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright

148c5f43199ca0b43fc8e3b643aab11cd66ea327Alan Wrightinstance (Comorphism cid1

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh sign1 morphism1 symbol1 raw_symbol1 proof_tree1

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh Comorphism cid2

1fcced4c370617db71610fecffd5451a5894ca5eJordan Brown lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4

1fcced4c370617db71610fecffd5451a5894ca5eJordan Brown sign4 morphism4 symbol4 raw_symbol4 proof_tree4

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright sign3 morphism3 symbol3 raw_symbol3 proof_tree3)

1fcced4c370617db71610fecffd5451a5894ca5eJordan Brown => Comorphism (CompComorphism cid1 cid2)

1fcced4c370617db71610fecffd5451a5894ca5eJordan Brown lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright sign1 morphism1 symbol1 raw_symbol1 proof_tree1

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

1fcced4c370617db71610fecffd5451a5894ca5eJordan Brown sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where

1fcced4c370617db71610fecffd5451a5894ca5eJordan Brown sourceLogic (CompComorphism cid1 _) =

1fcced4c370617db71610fecffd5451a5894ca5eJordan Brown sourceLogic cid1

1fcced4c370617db71610fecffd5451a5894ca5eJordan Brown targetLogic (CompComorphism _ cid2) =

1fcced4c370617db71610fecffd5451a5894ca5eJordan Brown targetLogic cid2

1fcced4c370617db71610fecffd5451a5894ca5eJordan Brown sourceSublogic (CompComorphism cid1 _) =

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh sourceSublogic cid1

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh mapSublogic (CompComorphism cid1 cid2) sl =

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh mapSublogic cid1 sl >>=

cb174861876aea6950a7ab4ce944aff84b1914cdjoyce mcintosh mapSublogic cid2 .

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2)

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb map_sentence (CompComorphism cid1 cid2) si1 se1 =

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb do (si2, _) <- map_sign cid1 si1

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw se2 <- map_sentence cid1 si1 se1

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright (si2', se2') <- coerceBasicTheory

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright (targetLogic cid1) (sourceLogic cid2)

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright "Mapping sentence along comorphism" (si2, [makeNamed "" se2])

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright case se2' of

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright [x] -> map_sentence cid2 si2' $ sentence x

29bd28862cfb8abbd3a0f0a4b17e08bbc3652836Alan Wright _ -> error "CompComorphism.map_sentence"

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw map_theory (CompComorphism cid1 cid2) ti1 =

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw do ti2 <- map_theory cid1 ti1

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw ti2' <- coerceBasicTheory (targetLogic cid1) (sourceLogic cid2)

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb "Mapping theory along comorphism" ti2

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb wrapMapTheory cid2 ti2'

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw map_morphism (CompComorphism cid1 cid2) m1 =

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb do m2 <- map_morphism cid1 m1

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2)

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw "Mapping signature morphism along comorphism" m2

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb map_morphism cid2 m3

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb map_symbol (CompComorphism cid1 cid2) sig1 = let

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb th = map_sign cid1 sig1 in

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb case maybeResult th of

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb Nothing -> error "failed translating signature"

f9a15d2c042edba37d61b071eb7ea274eb2754d1jose borrego Just (sig2', _) -> let

f9a15d2c042edba37d61b071eb7ea274eb2754d1jose borrego th2 = coerceBasicTheory

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb (targetLogic cid1) (sourceLogic cid2)

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb "Mapping symbol along comorphism" (sig2', [])

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb in case maybeResult th2 of

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb Nothing -> error "failed coercing"

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw Just (sig2, _) ->

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw \ s1 ->

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

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw in Set.unions

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw (map (map_symbol cid2 sig2 . mycast)

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw (Set.toList (map_symbol cid1 sig1 s1)))

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw extractModel (CompComorphism cid1 cid2) sign pt3 =

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb let lid1 = sourceLogic cid1

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb lid3 = sourceLogic cid2

f9a15d2c042edba37d61b071eb7ea274eb2754d1jose borrego in if language_name lid1 == language_name lid3 then do

f9a15d2c042edba37d61b071eb7ea274eb2754d1jose borrego bTh1 <- map_sign cid1 sign

f9a15d2c042edba37d61b071eb7ea274eb2754d1jose borrego (sign1, _) <-

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw coerceBasicTheory (targetLogic cid1) lid3 "extractModel1" bTh1

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb bTh2 <- extractModel cid2 sign1 pt3

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw coerceBasicTheory lid3 lid1 "extractModel2" bTh2

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw else fail $ "extractModel not implemented for comorphism composition with "

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb ++ language_name cid1

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw constituents (CompComorphism cid1 cid2) =

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb constituents cid1 ++ constituents cid2

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb is_model_transportable (CompComorphism cid1 cid2) =

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw is_model_transportable cid1 && is_model_transportable cid2

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb has_model_expansion (CompComorphism cid1 cid2) =

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb has_model_expansion cid1 && has_model_expansion cid2

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw is_weakly_amalgamable (CompComorphism cid1 cid2) =

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb is_weakly_amalgamable cid1 && is_weakly_amalgamable cid2

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb isInclusionComorphism (CompComorphism cid1 cid2) =

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb isInclusionComorphism cid1 && isInclusionComorphism cid2

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb-- * Comorphisms and existential types for the logic graph

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw-- | Existential type for comorphisms

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwdata AnyComorphism = forall cid lid1 sublogics1

faa1795a28a5c712eed6d0a3f84d98c368a316c6jb basic_spec1 sentence1 symb_items1 symb_map_items1

da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2

basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .

Comorphism cid

lid1 sublogics1 basic_spec1 sentence1

symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2 basic_spec2 sentence2

symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>

Comorphism cid deriving Typeable -- used for GTheory

instance Eq AnyComorphism where

a == b = compare a b == EQ

instance Ord AnyComorphism where

compare (Comorphism cid1) (Comorphism cid2) = compare

(language_name cid1, constituents cid1)

(language_name cid2, constituents cid2)

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

instance Show AnyComorphism where

show (Comorphism cid) = language_name cid

++ " : " ++ language_name (sourceLogic cid)

++ " -> " ++ language_name (targetLogic cid)

instance Pretty AnyComorphism where

pretty = text . show

-- | compute the identity comorphism for a logic

idComorphism :: AnyLogic -> AnyComorphism

idComorphism (Logic lid) = Comorphism (mkIdComorphism lid (top_sublogic lid))

-- | Test whether a comporphism is the identity

isIdComorphism :: AnyComorphism -> Bool

isIdComorphism (Comorphism cid) = null $ constituents cid

-- * Properties of comorphisms

-- | Test whether a comorphism is model-transportable

isModelTransportable :: AnyComorphism -> Bool

isModelTransportable (Comorphism cid) = is_model_transportable cid

-- | Test whether a comorphism has model expansion

hasModelExpansion :: AnyComorphism -> Bool

hasModelExpansion (Comorphism cid) = has_model_expansion cid

-- | Test whether a comorphism is weakly amalgamable

isWeaklyAmalgamable :: AnyComorphism -> Bool

isWeaklyAmalgamable (Comorphism cid) = is_weakly_amalgamable cid

-- | Compose comorphisms

compComorphism :: Monad m => AnyComorphism -> AnyComorphism -> m AnyComorphism

compComorphism (Comorphism cid1) (Comorphism cid2) =

let l1 = targetLogic cid1

l2 = sourceLogic cid2

msg = "ogic mismatch in composition of " ++ language_name cid1

++ " and " ++ language_name cid2

in

if language_name l1 == language_name l2 then

if isSubElem (forceCoerceSublogic l1 l2 $ targetSublogic cid1)

$ sourceSublogic cid2

then return $ Comorphism (CompComorphism cid1 cid2)

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

++ sublogicName (sourceSublogic cid2)

++ " but found sublogic "

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

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

++ language_name l2

++ " but found logic "

++ language_name l1 ++ ")"