Comorphism.hs revision 5d6e7ea3bd14fc987436cff0f542393ea9ba34bb
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{-|
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannModule : $Header$
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannMaintainer : hets@tzi.de
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannStability : provisional
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannPortability : non-portable (via Logic)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Provides data structures logic (co)morphisms.
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Logic (co)morphisms are just collections of
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann functions between (some of) the types of logics.
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-}
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{- References: see Logic.hs
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Todo:
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Weak amalgamability, also for comorphisms
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann comorphism maps
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann comorphisms out of sublogic relationships
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-}
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannmodule Logic.Comorphism where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Logic.Logic
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Lib.Set
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Data.Maybe
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Data.Dynamic
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.AS_Annotation (Named, mapNamedM)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.ATerm.Lib
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann--import Logic.Grothendieck
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- Logic comorphisms (possibly also morphisms via adjointness)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannclass (Language cid,
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Logic lid1 sublogics1
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann basic_spec1 sentence1 symb_items1 symb_map_items1
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Logic lid2 sublogics2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann basic_spec2 sentence2 symb_items2 symb_map_items2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Comorphism cid
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sign1 morphism1 symbol1 raw_symbol1 proof_tree1
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sign2 morphism2 symbol2 raw_symbol2 proof_tree2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann | cid -> lid1, cid -> lid2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sourceLogic :: cid -> lid1
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sourceSublogic :: cid -> sublogics1
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann targetLogic :: cid -> lid2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann targetSublogic :: cid -> sublogics2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -- the translation functions are partial
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -- because the target may be a sublanguage
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -- cover theoroidal comorphisms as well
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map_sign :: cid -> sign1 -> Maybe (sign2,[Named sentence2])
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map_theory :: cid -> (sign1,[Named sentence1])
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -> Maybe (sign2,[Named sentence2])
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann --default implementation
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map_theory cid (sign,sens) = do
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (sign',sens') <- map_sign cid sign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sens'' <- mapM (mapNamedM (map_sentence cid sign)) sens
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann return (sign',sens'++sens'')
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map_morphism :: cid -> morphism1 -> Maybe morphism2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map_sentence :: cid -> sign1 -> sentence1 -> Maybe sentence2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -- also covers semi-comorphisms
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -- with no sentence translation
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann -- - but these are spans!
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map_symbol :: cid -> symbol1 -> Set symbol2
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann fromShATerm_sign1 :: (ATermConvertible sign) => cid -> ATermTable -> sign
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann fromShATerm_sign1 _ att = fromShATerm att
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann fromShATerm_morphism2 :: (ATermConvertible morphism) => cid -> ATermTable -> morphism
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann fromShATerm_morphism2 _ att = fromShATerm att
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanndata IdComorphism lid =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann IdComorphism lid deriving Show
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannidComorphismTc :: TyCon
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannidComorphismTc = mkTyCon "Logic.Comorphism.IdComorphism"
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Typeable (IdComorphism lid) where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann typeOf _ = mkTyConApp idComorphismTc []
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Logic lid sublogics
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann basic_spec sentence symb_items symb_map_items
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sign morphism symbol raw_symbol proof_tree =>
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Language (IdComorphism lid) where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann language_name (IdComorphism lid) =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann "id_"++language_name lid
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Logic lid sublogics
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann basic_spec sentence symb_items symb_map_items
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sign morphism symbol raw_symbol proof_tree =>
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Comorphism (IdComorphism lid) --sublogics
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann --basic_spec sentence symb_items symb_map_items
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann --sign morphism symbol raw_symbol proof_tree)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann lid sublogics
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann basic_spec sentence symb_items symb_map_items
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sign morphism symbol raw_symbol proof_tree
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann lid sublogics
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann basic_spec sentence symb_items symb_map_items
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sign morphism symbol raw_symbol proof_tree
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sourceLogic (IdComorphism lid) = lid
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann targetLogic (IdComorphism lid) = lid
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sourceSublogic _ = top
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann targetSublogic _ = top
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map_sign _ = \sigma -> Just(sigma,[])
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map_morphism _ = Just
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map_sentence _ = \_ -> Just
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map_symbol _ = single
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanndata CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanntyconCompComorphism :: TyCon
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanntyconCompComorphism = mkTyCon "Logic.Comorphism.CompComorphism"
instance Typeable (CompComorphism cid1 cid2) where
typeOf _ = mkTyConApp tyconCompComorphism []
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)
=> 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
targetSublogic (CompComorphism _ cid2) =
targetSublogic cid2
map_sentence (CompComorphism cid1 cid2) =
\si1 se1 ->
do (si2,_) <- map_sign cid1 si1
se2 <- map_sentence cid1 si1 se1
(si2', se2') <- coerce (targetLogic cid1) (sourceLogic cid2)
(si2, se2)
map_sentence cid2 si2' se2'
map_sign (CompComorphism cid1 cid2) =
\si1 ->
do (si2, se2s) <- map_sign cid1 si1
(si2', se2s') <- coerce (targetLogic cid1) (sourceLogic cid2)
(si2, se2s)
(si3, se3s) <- map_sign cid2 si2'
return (si3, se3s ++ catMaybes
(map (mapNamedM (map_sentence cid2 si2')) se2s'))
map_morphism (CompComorphism cid1 cid2) = \ m1 ->
do m2 <- map_morphism cid1 m1
m3 <- coerce (targetLogic cid1) (sourceLogic cid2) m2
map_morphism cid2 m3
map_symbol (CompComorphism cid1 cid2) = \ s1 ->
let mycast = fromJust . coerce (targetLogic cid1) (sourceLogic cid2)
in unions
(map (map_symbol cid2 . mycast)
(toList (map_symbol cid1 s1)))