Comorphism.hs revision a9183ce3b997bf3539e427b3cd22d70c3565446e
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann{-# LANGUAGE UndecidableInstances #-}
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannModule : $Header$
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannDescription : interface and class for logic translations
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannMaintainer : till@informatik.uni-bremen.de
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannStability : provisional
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannPortability : non-portable (via Logic)
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannCentral interface (type class) for logic translations (comorphisms) in Hets
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann These are just collections of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann functions between (some of) the types of logics.
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann References: see Logic.hs
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann ( CompComorphism (..)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , InclComorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , inclusion_logic
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , inclusion_source_sublogic
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , inclusion_target_sublogic
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , mkInclComorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , mkIdComorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , Comorphism (..)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , targetSublogic
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , ext_map_sign
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , mapDefaultMorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , wrapMapTheory
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , simpleTheoryMapping
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , mkTheoryMapping
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , AnyComorphism (..)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , idComorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , isIdComorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , isModelTransportable
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , hasModelExpansion
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , isWeaklyAmalgamable
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , compComorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannimport qualified Data.Set as Set
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannclass (Language cid,
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann Logic lid1 sublogics1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann basic_spec1 sentence1 symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann Logic lid2 sublogics2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann basic_spec2 sentence2 symb_items2 symb_map_items2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann Comorphism cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann | cid -> lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- source and target logic and sublogic
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- the source sublogic is the maximal one for which the comorphism works
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sourceLogic :: cid -> lid1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sourceSublogic :: cid -> sublogics1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann targetLogic :: cid -> lid2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- finer information of target sublogics corresponding to source sublogics
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- this function must be partial because mapTheory is partial
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann mapSublogic :: cid -> sublogics1 -> Maybe sublogics2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- the translation functions are partial
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- because the target may be a sublanguage
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- cover theoroidal comorphisms as well
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_theory :: cid -> (sign1,[Named sentence1])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -> Result (sign2,[Named sentence2])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_morphism :: cid -> morphism1 -> Result morphism2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- also covers semi-comorphisms
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- with no sentence translation
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- - but these are spans!
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_sentence = failMapSentence
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_symbol :: cid -> symbol1 -> Set.Set symbol2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_symbol = errMapSymbol
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann extractModel :: cid -> sign1 -> proof_tree2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -> Result (sign1, [Named sentence1])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann extractModel cid _ _ = fail
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann $ "extractModel not implemented for comorphism "
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann ++ language_name cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann --properties of comorphisms
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann is_model_transportable :: cid -> Bool
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- a comorphism (\phi, \alpha, \beta) is model-transportable
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- if for any signature \Sigma,
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- any \Sigma-model M and any \phi(\Sigma)-model N
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- for any isomorphism h : \beta_\Sigma(N) -> M
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- there exists an isomorphism h': N -> M' such that \beta_\Sigma(h') = h
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann is_model_transportable _ = False
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann has_model_expansion :: cid -> Bool
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann has_model_expansion _ = False
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann is_weakly_amalgamable :: cid -> Bool
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann is_weakly_amalgamable _ = False
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann constituents :: cid -> [String]
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann constituents cid = [language_name cid]
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann isInclusionComorphism :: cid -> Bool
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann isInclusionComorphism _ = False
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanntargetSublogic :: Comorphism cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann => cid -> sublogics2
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanntargetSublogic cid = maybe (error ("Logic.Comorphism: " ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann language_name cid ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann " does not provide a mapping for it's " ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "source sublogic"))
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann id $ mapSublogic cid $ sourceSublogic cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | this function is base on 'map_theory' using no sentences as input
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannmap_sign :: Comorphism cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann => cid -> sign1 -> Result (sign2,[Named sentence2])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannmap_sign cid sign = wrapMapTheory cid (sign,[])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannext_map_sign :: Comorphism cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann => cid -> ExtSign sign1 symbol1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -> Result (ExtSign sign2 symbol2, [Named sentence2])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmannext_map_sign cid (ExtSign sign _) = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (sign2, sens2) <- map_sign cid sign
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann return (makeExtSign (targetLogic cid) sign2, sens2)
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannmapDefaultMorphism :: Comorphism cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann => cid -> morphism1 -> Result morphism2
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannmapDefaultMorphism cid mor = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (sig1, _) <- map_sign cid $ dom mor
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (sig2, _) <- map_sign cid $ cod mor
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann inclusion (targetLogic cid) sig1 sig2
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannfailMapSentence :: Comorphism cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann => cid -> sign1 -> sentence1 -> Result sentence2
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannfailMapSentence cid _ _ =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann fail $ "Unsupported sentence translation " ++ show cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannerrMapSymbol :: Comorphism cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann => cid -> symbol1 -> Set.Set symbol2
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannerrMapSymbol cid _ = error $ "no symbol mapping for " ++ show cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | use this function instead of 'map_theory'
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannwrapMapTheory :: Comorphism cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann => cid -> (sign1, [Named sentence1])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -> Result (sign2, [Named sentence2])
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannwrapMapTheory cid (sign, sens) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann case sourceSublogic cid of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sub -> case minSublogic sign of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sigLog -> case foldl join sigLog
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann $ map (minSublogic . sentence) sens of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann if isSubElem senLog sub
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann then map_theory cid (sign, sens)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann else fail $ "for '" ++ language_name cid ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "' expected sublogic '" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sublogicName sub ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "'\n but found sublogic '" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sublogicName senLog ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "' with signature sublogic '" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sublogicName sigLog ++ "'\n" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann show (vcat $ pretty sign : map
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (print_named $ sourceLogic cid) sens)
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannsimpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -> (sign1, [Named sentence1])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -> (sign2, [Named sentence2])
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannsimpleTheoryMapping mapSig mapSen (sign,sens) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (mapSig sign, map (mapNamed mapSen) sens)
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannmkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -> (sign1 -> sentence1 -> m sentence2)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -> (sign1, [Named sentence1])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -> m (sign2, [Named sentence2])
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannmkTheoryMapping mapSig mapSen (sign,sens) = do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (sign',sens') <- mapSig sign
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sens'' <- mapM (mapNamedM $ mapSen sign) sens
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann return (sign', nameAndDisambiguate $ sens' ++ sens'')
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanndata InclComorphism lid sublogics = InclComorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann { inclusion_logic :: lid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , inclusion_source_sublogic :: sublogics
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , inclusion_target_sublogic :: sublogics }
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | construction of an identity comorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannmkIdComorphism :: (Logic lid sublogics
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann basic_spec sentence symb_items symb_map_items
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign morphism symbol raw_symbol proof_tree) =>
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid -> sublogics -> InclComorphism lid sublogics
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannmkIdComorphism lid sub = InclComorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann { inclusion_logic = lid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , inclusion_source_sublogic = sub
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , inclusion_target_sublogic = sub }
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | construction of an inclusion comorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannmkInclComorphism :: (Logic lid sublogics
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann basic_spec sentence symb_items symb_map_items
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign morphism symbol raw_symbol proof_tree,
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid -> sublogics -> sublogics
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -> m (InclComorphism lid sublogics)
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannmkInclComorphism lid srcSub trgSub =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann if isSubElem srcSub trgSub
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann then return $ InclComorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann { inclusion_logic = lid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , inclusion_source_sublogic = srcSub
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann , inclusion_target_sublogic = trgSub }
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann else fail ("mkInclComorphism: first sublogic must be a "++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "subElem of the second sublogic")
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanninstance Logic lid sublogics
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann basic_spec sentence symb_items symb_map_items
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign morphism symbol raw_symbol proof_tree =>
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann Show (InclComorphism lid sublogics)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann show = language_name
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanninstance Logic lid sublogics
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann basic_spec sentence symb_items symb_map_items
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign morphism symbol raw_symbol proof_tree =>
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann Language (InclComorphism lid sublogics) where
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann language_name (InclComorphism lid sub_src sub_trg) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let sblName = sublogicName sub_src in
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann if sub_src == sub_trg
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann then "id_" ++ language_name lid ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann if null sblName
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann then "" else "." ++ sblName
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann else "incl_" ++ language_name lid ++ ":" ++
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sblName ++ "->" ++ sublogicName sub_trg
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanninstance Logic lid sublogics
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann basic_spec sentence symb_items symb_map_items
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign morphism symbol raw_symbol proof_tree =>
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann Comorphism (InclComorphism lid sublogics)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid sublogics
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann basic_spec sentence symb_items symb_map_items
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign morphism symbol raw_symbol proof_tree
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid sublogics
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann basic_spec sentence symb_items symb_map_items
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign morphism symbol raw_symbol proof_tree
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sourceLogic = inclusion_logic
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann targetLogic = inclusion_logic
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sourceSublogic = inclusion_source_sublogic
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann mapSublogic cid subl =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann if isSubElem subl $ inclusion_source_sublogic cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann then Just subl
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_theory _ = return
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_morphism _ = return
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_sentence _ = \_ -> return
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann constituents cid =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann if inclusion_source_sublogic cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann == inclusion_target_sublogic cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann else [language_name cid]
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann is_model_transportable _ = True
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann has_model_expansion _ = True
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann is_weakly_amalgamable _ = True
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann isInclusionComorphism _ = True
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanndata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanninstance (Language cid1, Language cid2)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann => Language (CompComorphism cid1 cid2) where
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann language_name (CompComorphism cid1 cid2) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann language_name cid1 ++ ";" ++ language_name cid2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanninstance (Comorphism cid1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann Comorphism cid2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign4 morphism4 symbol4 raw_symbol4 proof_tree4
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann => Comorphism (CompComorphism cid1 cid2)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sourceLogic (CompComorphism cid1 _) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sourceLogic cid1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann targetLogic (CompComorphism _ cid2) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann targetLogic cid2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sourceSublogic (CompComorphism cid1 _) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sourceSublogic cid1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann mapSublogic (CompComorphism cid1 cid2) sl =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann mapSublogic cid1 sl >>=
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (\ y -> mapSublogic cid2 $
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2) y)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_sentence (CompComorphism cid1 cid2) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann do (si2,_) <- map_sign cid1 si1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann se2 <- map_sentence cid1 si1 se1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (si2', se2') <- coerceBasicTheory
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (targetLogic cid1) (sourceLogic cid2)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Mapping sentence along comorphism" (si2, [makeNamed "" se2])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann [x] -> map_sentence cid2 si2' $ sentence x
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_theory (CompComorphism cid1 cid2) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann do ti2 <- map_theory cid1 ti1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann ti2' <- coerceBasicTheory (targetLogic cid1) (sourceLogic cid2)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Mapping theory along comorphism" ti2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann wrapMapTheory cid2 ti2'
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_morphism (CompComorphism cid1 cid2) = \ m1 ->
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann do m2 <- map_morphism cid1 m1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann "Mapping signature morphism along comorphism"m2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_morphism cid2 m3
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann map_symbol (CompComorphism cid1 cid2) = \ s1 ->
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let mycast = coerceSymbol (targetLogic cid1) (sourceLogic cid2)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (map (map_symbol cid2 . mycast)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (Set.toList (map_symbol cid1 s1)))
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann extractModel (CompComorphism cid1 cid2) sign pt3 =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann if isIdComorphism (Comorphism cid1) then do
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let lid1 = sourceLogic cid1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid4 = sourceLogic cid2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (sign', _) <- coerceBasicTheory lid1 lid4 "extractModel1" (sign, [])
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (sign'', sens') <- extractModel cid2 sign' pt3
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann bTh <- coerceBasicTheory lid4 lid1 "extractModel2" (sign'', sens')
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann else fail $ "extractModel not implemented for comorphism composition with"
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann ++ language_name cid1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann constituents (CompComorphism cid1 cid2) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann constituents cid1 ++ constituents cid2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann is_model_transportable (CompComorphism cid1 cid2) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann is_model_transportable cid1 && is_model_transportable cid2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann has_model_expansion (CompComorphism cid1 cid2) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann has_model_expansion cid1 && has_model_expansion cid2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann is_weakly_amalgamable (CompComorphism cid1 cid2) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann is_weakly_amalgamable cid1 && is_weakly_amalgamable cid2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann isInclusionComorphism (CompComorphism cid1 cid2) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann isInclusionComorphism cid1 && isInclusionComorphism cid2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- * Comorphisms and existential types for the logic graph
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Existential type for comorphisms
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanndata AnyComorphism = forall cid lid1 sublogics1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann basic_spec1 sentence1 symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid2 sublogics2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann basic_spec2 sentence2 symb_items2 symb_map_items2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann Comorphism cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid1 sublogics1 basic_spec1 sentence1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann symb_items1 symb_map_items1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann lid2 sublogics2 basic_spec2 sentence2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann symb_items2 symb_map_items2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann Comorphism cid deriving Typeable -- used for GTheory
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanninstance Eq AnyComorphism where
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann a == b = compare a b == EQ
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanninstance Ord AnyComorphism where
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann compare (Comorphism cid1) (Comorphism cid2) = compare
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (language_name cid1, constituents cid1)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (language_name cid2, constituents cid2)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann -- maybe needs to be refined, using comorphism translations?
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanninstance Show AnyComorphism where
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann show (Comorphism cid) = language_name cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann ++ " : " ++ language_name (sourceLogic cid)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann ++ " -> " ++ language_name (targetLogic cid)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmanninstance Pretty AnyComorphism where
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann pretty = text . show
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | compute the identity comorphism for a logic
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannidComorphism :: AnyLogic -> AnyComorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannidComorphism (Logic lid) = Comorphism (mkIdComorphism lid (top_sublogic lid))
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Test whether a comporphism is the identity
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannisIdComorphism :: AnyComorphism -> Bool
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannisIdComorphism (Comorphism cid) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann constituents cid == []
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- * Properties of comorphisms
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Test whether a comorphism is model-transportable
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannisModelTransportable :: AnyComorphism -> Bool
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannisModelTransportable (Comorphism cid) = is_model_transportable cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Test whether a comorphism has model expansion
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannhasModelExpansion :: AnyComorphism -> Bool
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannhasModelExpansion (Comorphism cid) = has_model_expansion cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Test whether a comorphism is weakly amalgamable
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannisWeaklyAmalgamable :: AnyComorphism -> Bool
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmannisWeaklyAmalgamable (Comorphism cid) = is_weakly_amalgamable cid
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann-- | Compose comorphisms
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanncompComorphism :: Monad m => AnyComorphism -> AnyComorphism -> m AnyComorphism
304d15b2ffa9376d78bddcfc63569824381714abDaniel HausmanncompComorphism (Comorphism cid1) (Comorphism cid2) =
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann let l1 = targetLogic cid1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann l2 = sourceLogic cid2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann msg = "ogic mismatch in composition of " ++ language_name cid1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann ++ " and " ++ language_name cid2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann if language_name l1 == language_name l2 then
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann if isSubElem (forceCoerceSublogic l1 l2 $ targetSublogic cid1)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann $ sourceSublogic cid2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann then {- case (isIdComorphism cm1,isIdComorphism cm2) of
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (True,_) -> return cm2
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann (_,True) -> return cm1
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann _ -> -} return $ Comorphism (CompComorphism cid1 cid2)
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann else fail $ "Subl" ++ msg
304d15b2ffa9376d78bddcfc63569824381714abDaniel Hausmann else fail $ "L" ++ msg