Morphism.hs revision a7be28e157e9ceeec73a8fd0e642c36ea29d4218
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{-# LANGUAGE UndecidableInstances #-}
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder{-# LANGUAGE IncoherentInstances #-}
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiModule : $Header$
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederDescription : interface (type class) for logic projections (morphisms) in Hets
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederMaintainer : till@informatik.uni-bremen.de
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederStability : provisional
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaederPortability : non-portable (via Logic)
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederInterface (type class) for logic projections (morphisms) in Hets
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederProvides data structures for institution morphisms.
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder These are just collections of
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder functions between (some of) the types of logics.
f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian Maeder{- References: see Logic.hs
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder morphism modifications / representation maps
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport qualified Data.Set as Set
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport Common.ATerm.Lib -- (ShATermConvertible)
64f7c2188d578b920d8e5513a423449af633e9bcChristian Maederclass (Language cid,
64f7c2188d578b920d8e5513a423449af633e9bcChristian Maeder Logic lid1 sublogics1
64f7c2188d578b920d8e5513a423449af633e9bcChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1,
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder Logic lid2 sublogics2
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2) =>
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder | cid -> lid1, cid -> lid2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , lid1 -> sublogics1 basic_spec1 sentence1 symb_items1
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , lid2 -> sublogics2 basic_spec2 sentence2 symb_items2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -- source and target logic and sublogic
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder -- the source sublogic is the maximal one for which the comorphism works
e289294500ad68fa0706b09521af340bbb356a69Christian Maeder -- the target sublogic is the resulting one
e289294500ad68fa0706b09521af340bbb356a69Christian Maeder morSourceLogic :: cid -> lid1
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morSourceSublogic :: cid -> sublogics1
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morTargetLogic :: cid -> lid2
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morTargetSublogic :: cid -> sublogics2
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -- finer information of target sublogics corresponding to source sublogics
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder morMapSublogicSign :: cid -> sublogics1 -> sublogics2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -- information about the source sublogics corresponding to target sublogics
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morMapSublogicSen :: cid -> sublogics2 -> sublogics1
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -- the translation functions are partial
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -- because the target may be a sublanguage
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -- we do not cover theoroidal morphisms,
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -- since there are no relevant examples and they do not compose nicely
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -- no mapping of theories, since signatures and sentences are mapped
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -- contravariantly
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morMap_sign :: cid -> sign1 -> Maybe sign2
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morMap_morphism :: cid -> morphism1 -> Maybe morphism2
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -- also covers semi-morphisms ??
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -- with no sentence translation
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -- - but these are spans!
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder morMap_sign_symbol :: cid -> sign_symbol1 -> Set.Set sign_symbol2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -- morConstituents not needed, because composition only via lax triangles
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- | identity morphisms
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederdata IdMorphism lid sublogics =
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder IdMorphism lid sublogics deriving (Typeable, Show)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederinstance Logic lid sublogics
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder basic_spec sentence symb_items symb_map_items
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sign morphism sign_symbol symbol proof_tree =>
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder Language (IdMorphism lid sublogics) where
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder language_name (IdMorphism lid sub) = "id_" ++ language_name lid
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder ++ case sublogicName sub of
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder h -> "." ++ h
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederinstance Logic lid sublogics
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder basic_spec sentence symb_items symb_map_items
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder sign morphism sign_symbol symbol proof_tree =>
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder Morphism (IdMorphism lid sublogics)
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder lid sublogics
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder basic_spec sentence symb_items symb_map_items
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder sign morphism sign_symbol symbol proof_tree
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder lid sublogics
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder basic_spec sentence symb_items symb_map_items
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder sign morphism sign_symbol symbol proof_tree
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morSourceLogic (IdMorphism lid _sub) = lid
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morTargetLogic (IdMorphism lid _sub) = lid
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morSourceSublogic (IdMorphism _lid sub) = sub
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morTargetSublogic (IdMorphism _lid sub) = sub
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder --changed to identities!
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morMapSublogicSign _ x = x
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morMapSublogicSen _ x = x
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morMap_sign _ = Just
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morMap_morphism _ = Just
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder morMap_sentence _ = \_ -> Just
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder morMap_sign_symbol _ = Set.singleton
9b3bf7c6cf82dc11478bbac3414fe657b9bca327Christian Maeder-- composition not needed, use lax triangles instead
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- | comorphisms inducing morphisms
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederclass Comorphism cid
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2 =>
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder InducingComorphism cid
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder indMorMap_sign :: cid -> sign2 -> Maybe sign1
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder epsilon :: cid -> sign2 -> Maybe morphism2
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder--------------------------------------------------------------------------
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- Morphisms as spans of comorphisms
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- if the morphism is (psi, alpha, beta) : I -> J
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- it is replaced with the following span
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- SignI id -> SignI psi -> SignJ
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- SenI alpha <- psi;SenJ id -> psi;SenJ
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- ModI beta -> psi^op;ModJ id <- psi^op;ModJ
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- 1. introduce a new logic for the domain of the span
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- this logic will have
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- * the name (SpanDomain cid) where cid is the name of the morphism
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- * sublogics - pairs (s1, s2) with s1 being a sublogic of I and s2
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- being a sublogic of J; the lattice is the product lattice of the two
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- existing lattices
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- * basic_spec will be () - the unit type, because we mix signatures
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- with sentences in specifications
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- * sentence - sentences of J, wrapped
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- * symb_items - ()
9b3bf7c6cf82dc11478bbac3414fe657b9bca327Christian Maeder-- * symb_map_items - ()
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder-- * sign - signatures of I
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder-- * morphism - morphisms of I
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder-- * sign_symbol - sign_symbols of I
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder-- * symbol - symbols of I
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder-- * proof_tree - proof_tree of J
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maederdata SpanDomain cid = SpanDomain cid deriving (Eq, Show)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maederdata SublogicsPair a b = SublogicsPair a b deriving (Eq, Ord, Show)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederinstance Language cid => Language (SpanDomain cid) where
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder language_name (SpanDomain cid) = "SpanDomain" ++ language_name cid
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder{- the category of signatures is exactly the category of signatures of
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maederthe sublogic on which the morphism is defined, but with another name -}
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maederinstance Morphism cid
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder => Syntax (SpanDomain cid) () () ()
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- default is ok
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maedernewtype S2 s = S2 { sentence2 :: s } deriving (Eq, Ord, Show, Typeable)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederinstance Pretty s => Pretty (S2 s) where
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder pretty (S2 x) = pretty x
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maederinstance ShATermConvertible s => ShATermConvertible (S2 s) where
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder toShATermAux att (S2 s) = do
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (att1, i) <- toShATerm' att s
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return $ addATerm (ShAAppl "S2" [i] []) att1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder fromShATermAux ix att =
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder case getShATerm ix att of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ShAAppl "S2" [i] _ -> case fromShATerm' i att of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (att1, i1) -> (att1, S2 i1)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder u -> fromShATermError "S2" u
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederinstance Morphism cid
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder sign_symbol1 where
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder--one has to take care about signature and morphisms
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder--and translate them to targetLogic
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder map_sen (SpanDomain cid) mor1 (S2 sen) =
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder case morMap_morphism cid mor1 of
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder Just mor2 -> fmap S2 $
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder map_sen (morTargetLogic cid) mor2 sen
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder Nothing -> statErr (SpanDomain cid) "map_sen"
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder simplify_sen (SpanDomain cid) sigma (S2 sen) =
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder case morMap_sign cid sigma of
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder Just sigma2 -> S2 $
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder simplify_sen (morTargetLogic cid) sigma2 sen
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder Nothing -> error "simplify_sen"
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder parse_sentence (SpanDomain cid) = fmap (fmap S2) $
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder parse_sentence (morTargetLogic cid)
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder print_named (SpanDomain cid) = print_named (morTargetLogic cid)
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder . mapNamed sentence2
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder sym_of (SpanDomain cid) = sym_of (morSourceLogic cid)
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder symmap_of (SpanDomain cid) = symmap_of (morSourceLogic cid)
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder sym_name (SpanDomain cid) = sym_name (morSourceLogic cid)
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maederinstance (Morphism cid
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () ()
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder sign1 morphism1 sign_symbol1 symbol1 where
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder ensures_amalgamability l _ = statErr l "ensures_amalgamability"
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder symbol_to_raw (SpanDomain cid) = symbol_to_raw (morSourceLogic cid)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder id_to_raw (SpanDomain cid) = id_to_raw (morSourceLogic cid)
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder matches (SpanDomain cid) = matches (morSourceLogic cid)
3a9dafc31d54a6bdac1acda72bb15aceffb0240fChristian Maeder empty_signature (SpanDomain cid) = empty_signature (morSourceLogic cid)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder signature_union (SpanDomain cid) = signature_union (morSourceLogic cid)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder final_union (SpanDomain cid) = final_union (morSourceLogic cid)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder morphism_union (SpanDomain cid) = morphism_union (morSourceLogic cid)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder is_subsig (SpanDomain cid) = is_subsig (morSourceLogic cid)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder subsig_inclusion (SpanDomain cid) = subsig_inclusion (morSourceLogic cid)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder generated_sign (SpanDomain cid) = generated_sign (morSourceLogic cid)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder cogenerated_sign (SpanDomain cid) = cogenerated_sign (morSourceLogic cid)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder is_transportable (SpanDomain cid) = is_transportable (morSourceLogic cid)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder is_injective (SpanDomain cid) = is_injective (morSourceLogic cid)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maederinstance (SemiLatticeWithTop sublogics1, SemiLatticeWithTop sublogics2)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder => SemiLatticeWithTop (SublogicsPair sublogics1 sublogics2) where
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder top = SublogicsPair top top
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder join (SublogicsPair x1 y1) (SublogicsPair x2 y2) =
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder SublogicsPair (join x1 x2) (join y1 y2)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maederinstance (SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) where
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder minSublogic (S2 sen2) = SublogicsPair top (minSublogic sen2)
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder{- just a dummy implementation, it should be the sublogic of sen2 in J
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederpaired with its image through morMapSublogicSen? -}
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maederinstance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder => MinSublogic (SublogicsPair sublogics1 sublogics2) alpha where
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder minSublogic x = SublogicsPair (minSublogic x) top
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder{- also should have instances of MinSublogic class for Sublogics-pair
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maederand morphism1, sign_symbol1, sign1 this is why the wrapping is needed -}
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder-- instance SemiLatticeWithTop sublogics => MinSublogic sublogics () where
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- minSublogic _ = top
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maederinstance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder => ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha where
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder projectSublogic _ x = x
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder-- it should be used for (), morphism1, sign_symbol1, sign1
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maederinstance (MinSublogic sublogics1 sign1, SemiLatticeWithTop sublogics2)
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder => ProjectSublogicM (SublogicsPair sublogics1 sublogics2) sign1 where
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder projectSublogicM _ x = Just x
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederinstance (Typeable sublogics1, Typeable sublogics2)
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder => Typeable (SublogicsPair sublogics1 sublogics2) where
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder typeOf _ = mkTyConApp (mkTyCon "Logic.Morphism.SpanDomain") []
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederinstance (ShATermConvertible sublogics1, ShATermConvertible sublogics2)
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder => ShATermConvertible (SublogicsPair sublogics1 sublogics2) where
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder toShATermAux att0 (SublogicsPair sub1 sub2) = do
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder (att1,i1) <- toShATerm' att0 sub1
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder (att2,i2) <- toShATerm' att1 sub2
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder return $ addATerm (ShAAppl "SublogicsPair" [i1,i2] []) att2
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder fromShATermAux ix att =
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder case getShATerm ix att of
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder ShAAppl "SublogicsPair" [i1, i2] _ ->
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder case fromShATerm' i2 att of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (att2, i2') -> case fromShATerm' i1 att2 of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (att1, i1') -> (att1, SublogicsPair i1' i2')
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder u -> fromShATermError "SublogicsPair" u
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maederinstance (SublogicName sublogics1, SublogicName sublogics2)
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder => SublogicName (SublogicsPair sublogics1 sublogics2) where
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sublogicName (SublogicsPair sub1 sub2) =
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let s1 = sublogicName sub1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder s2 = sublogicName sub2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder in if null s1 then s2 else if null s2 then s1 else
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder s1 ++ "|" ++ s2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederinstance ( MinSublogic sublogics1 ()
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , Morphism cid
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder ) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) ()
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder stability (SpanDomain _) = Experimental
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder data_logic (SpanDomain _) = Nothing
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder top_sublogic (SpanDomain cid) = SublogicsPair
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder (top_sublogic $ morSourceLogic cid) $ top_sublogic $ morTargetLogic cid
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder all_sublogics (SpanDomain cid) =
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder [ SublogicsPair x y
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder | x <- all_sublogics (morSourceLogic cid)
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder , y <- all_sublogics (morTargetLogic cid) ]
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -- project_sublogic_epsilon - default implementation for now
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder provers _ = []
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder cons_checkers _ = []
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder conservativityCheck _ = []
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder empty_proof_tree (SpanDomain cid) = empty_proof_tree (morTargetLogic cid)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- * Morphisms
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder-- | Existential type for morphisms
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maederdata AnyMorphism = forall cid lid1 sublogics1
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian Maeder lid2 sublogics2
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder lid1 sublogics1 basic_spec1 sentence1
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder symb_items1 symb_map_items1
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder lid2 sublogics2 basic_spec2 sentence2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder symb_items2 symb_map_items2
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maederinstance Eq AnyMorphism where
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder Morphism cid1 == Morphism cid2 =
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder constituents cid1 == constituents cid2
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder -- need to be refined, using morphism translations !!!
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederinstance Show AnyMorphism where
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder show (Morphism cid) = language_name cid
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder ++ " : " ++ language_name (morSourceLogic cid)
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder ++ " -> " ++ language_name (morTargetLogic cid)