Morphism.hs revision da955132262baab309a50fdffe228c9efe68251d
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder{-# OPTIONS -fallow-incoherent-instances #-}
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiModule : $Header$
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederDescription : interface (type class) for logic projections (morphisms) in Hets
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiStability : provisional
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiPortability : non-portable (via Logic)
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederInterface (type class) for logic projections (morphisms) in Hets
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian MaederProvides data structures for institution morphisms.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski These are just collections of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski functions between (some of) the types of logics.
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- References: see Logic.hs
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morphism modifications / representation maps
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederimport Common.ATerm.Lib -- (ShATermConvertible)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiclass (Language cid,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Logic lid1 sublogics1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Logic lid2 sublogics2
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2) =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski | cid -> lid1, cid -> lid2
df476f3bf7038997303a1760a9c1ce09be40a05eChristian Maeder , lid1 -> sublogics1 basic_spec1 sentence1 symb_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , lid2 -> sublogics2 basic_spec2 sentence2 symb_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- source and target logic and sublogic
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- the source sublogic is the maximal one for which the comorphism works
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- the target sublogic is the resulting one
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceLogic :: cid -> lid1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceSublogic :: cid -> sublogics1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetLogic :: cid -> lid2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetSublogic :: cid -> sublogics2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- finer information of target sublogics corresponding to source sublogics
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morMapSublogicSign :: cid -> sublogics1 -> sublogics2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- information about the source sublogics corresponding to target sublogics
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morMapSublogicSen :: cid -> sublogics2 -> sublogics1
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder -- the translation functions are partial
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- because the target may be a sublanguage
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder -- we do not cover theoroidal morphisms,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- since there are no relevant examples and they do not compose nicely
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- no mapping of theories, since signatures and sentences are mapped
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- contravariantly
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sign :: cid -> sign1 -> Maybe sign2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_morphism :: cid -> morphism1 -> Maybe morphism2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- also covers semi-morphisms ??
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- with no sentence translation
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- - but these are spans!
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morMap_sign_symbol :: cid -> sign_symbol1 -> Set.Set sign_symbol2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- morConstituents not needed, because composition only via lax triangles
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder-- identity morphisms
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maederdata IdMorphism lid sublogics =
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski IdMorphism lid sublogics deriving Show
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiidMorphismTc :: TyCon
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiidMorphismTc = mkTyCon "Logic.Morphism.IdMorphism"
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maederinstance Typeable (IdMorphism lid sub) where
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski typeOf _ = mkTyConApp idMorphismTc []
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Logic lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign morphism sign_symbol symbol proof_tree =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Language (IdMorphism lid sublogics) where
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder language_name (IdMorphism lid sub) =
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder case sublogic_names sub of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski [] -> error "language_name IdMorphism"
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski h : _ -> "id_" ++ language_name lid ++ "." ++ h
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Logic lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign morphism sign_symbol symbol proof_tree =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Morphism (IdMorphism lid sublogics)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign morphism sign_symbol symbol proof_tree
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign morphism sign_symbol symbol proof_tree
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceLogic (IdMorphism lid _sub) = lid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetLogic (IdMorphism lid _sub) = lid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceSublogic (IdMorphism _lid sub) = sub
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetSublogic (IdMorphism _lid sub) = sub
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu --changed to identities!
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu morMapSublogicSign _ x = x
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu morMapSublogicSen _ x = x
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sign _ = Just
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_morphism _ = Just
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sentence _ = \_ -> Just
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morMap_sign_symbol _ = Set.singleton
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- composition not needed, use lax triangles instead
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- comorphisms inducing morphisms
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiclass Comorphism cid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2 =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski InducingComorphism cid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski indMorMap_sign :: cid -> sign2 -> Maybe sign1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski epsilon :: cid -> sign2 -> Maybe morphism2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder--------------------------------------------------------------------------
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- Morphisms as spans of comorphisms
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- if the morphism is (psi, alpha, beta) : I -> J
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- it is replaced with the following span
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- SignI id -> SignI psi -> SignJ
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- SenI alpha <- psi;SenJ id -> psi;SenJ
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- ModI beta -> psi^op;ModJ id <- psi^op;ModJ
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- 1. introduce a new logic for the domain of the span
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- this logic will have
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * the name (SpanDomain cid) where cid is the name of the morphism
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * sublogics - pairs (s1, s2) with s1 being a sublogic of I and s2 being a sublogic of J; the lattice is the product lattice of the two existing lattices
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * basic_spec will be () - the unit type, because we mix signatures with sentences in specifications
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu-- * sentence - sentences of J, wrapped
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * symb_items - ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * symb_map_items - ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * sign - signatures of I
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * morphism - morphisms of I
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * sign_symbol - sign_symbols of I
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * symbol - symbols of I
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- * proof_tree - proof_tree of J
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederdata SpanDomain cid = SpanDomain cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder deriving (Eq, Show)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederdata SublogicsPair a b = SublogicsPair a b
23e0b003dd27c804487db4d3a9fc8ff2f452cb77Christian Maeder deriving (Eq, Ord, Show)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Language cid =>
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Language (SpanDomain cid) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder language_name (SpanDomain cid) = "SpanDomain" ++ language_name cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Morphism cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2=>
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Category (SpanDomain cid) sign1 morphism1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ide (SpanDomain cid) = ide (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- ok in Haskell, because cid is a variable of type cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder comp (SpanDomain cid) = comp (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder cod (SpanDomain cid) = cod (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder dom (SpanDomain cid) = dom (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder legal_obj (SpanDomain cid) = legal_obj (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder legal_mor (SpanDomain cid) = legal_mor (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- the category of signatures is exactly the category of signatures of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederthe sublogic on which the morphism is defined, but with another name -}
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Morphism cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Syntax (SpanDomain cid) () () () where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder parse_basic_spec _ = Nothing
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder parse_symb_items _ = Nothing
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder parse_symb_map_items _ = Nothing
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maedernewtype S2 s = S2 { sentence2 :: s } deriving (Eq, Ord, Show, Typeable)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescuinstance Pretty s => Pretty (S2 s) where
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu pretty (S2 x) = pretty x
c18a07fe36512679e66faa59274bb273e735738aMihai Codescuinstance ShATermConvertible s => ShATermConvertible (S2 s) where
da955132262baab309a50fdffe228c9efe68251dCui Jian toShATermAux att (S2 s) = do
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu (att1, i) <- toShATerm' att s
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu return $ addATerm (ShAAppl "S2" [i] []) att1
da955132262baab309a50fdffe228c9efe68251dCui Jian fromShATermAux ix att =
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu case getShATerm ix att of
da955132262baab309a50fdffe228c9efe68251dCui Jian ShAAppl "S2" [i] _ -> case fromShATerm' i att of
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu (att1, i1) -> (att1, S2 i1)
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu u -> fromShATermError "S2" u
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance Morphism cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign_symbol1 where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder--one has to take care about signature and morphisms
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder--and translate them to targetLogic
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder map_sen (SpanDomain cid) mor1 (S2 sen) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder case morMap_morphism cid mor1 of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Just mor2 -> fmap S2 $
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder map_sen (morTargetLogic cid) mor2 sen
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Nothing -> statErr (SpanDomain cid) "map_sen"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder simplify_sen (SpanDomain cid) sigma (S2 sen) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder case morMap_sign cid sigma of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Just sigma2 -> S2 $
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder simplify_sen (morTargetLogic cid) sigma2 sen
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Nothing -> error "simplify_sen"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder parse_sentence (SpanDomain cid) = fmap (fmap S2) $
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder parse_sentence (morTargetLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder print_named (SpanDomain cid) = print_named (morTargetLogic cid)
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder . mapNamed sentence2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sym_of (SpanDomain cid) = sym_of (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder symmap_of (SpanDomain cid) = symmap_of (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sym_name (SpanDomain cid) = sym_name (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (Morphism cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2)
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign_to_basic_spec _ _ _ = ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ensures_amalgamability l _ = statErr l "ensures_amalgamability"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder symbol_to_raw (SpanDomain cid) = symbol_to_raw (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder id_to_raw (SpanDomain cid) = id_to_raw (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder matches (SpanDomain cid) = matches (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder empty_signature (SpanDomain cid) = empty_signature (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder signature_union (SpanDomain cid) = signature_union (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder signature_difference (SpanDomain cid) = signature_difference (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder is_subsig (SpanDomain cid) = is_subsig (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder final_union (SpanDomain cid) = final_union (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morphism_union (SpanDomain cid) = morphism_union (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder inclusion (SpanDomain cid)= inclusion (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder generated_sign (SpanDomain cid) = generated_sign (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder cogenerated_sign (SpanDomain cid) = cogenerated_sign (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder is_transportable (SpanDomain cid) = is_transportable (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder is_injective (SpanDomain cid) = is_injective (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (SemiLatticeWithTop sublogics1, SemiLatticeWithTop sublogics2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => SemiLatticeWithTop (SublogicsPair sublogics1 sublogics2) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder top = SublogicsPair top top
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder join (SublogicsPair x1 y1) (SublogicsPair x2 y2) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder SublogicsPair (join x1 x2) (join y1 y2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder minSublogic (S2 sen2) = SublogicsPair top (minSublogic sen2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- just a dummy implementation, it should be the sublogic of sen2 in J
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederpaired with its image through morMapSublogicSen? -}
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescuinstance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu => MinSublogic (SublogicsPair sublogics1 sublogics2) alpha where
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu minSublogic x = SublogicsPair (minSublogic x) top
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- also should have instances of MinSublogic class for Sublogics-pair
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederand morphism1, sign_symbol1, sign1 this is why the wrapping is needed -}
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- instance SemiLatticeWithTop sublogics => MinSublogic sublogics () where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- minSublogic _ = top
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescuinstance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu => ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder projectSublogic _ x = x
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu-- it should be used for (), morphism1, sign_symbol1, sign1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (MinSublogic sublogics1 sign1, SemiLatticeWithTop sublogics2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => ProjectSublogicM (SublogicsPair sublogics1 sublogics2) sign1 where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder projectSublogicM _ x = Just x
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (Typeable sublogics1, Typeable sublogics2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => Typeable (SublogicsPair sublogics1 sublogics2) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder typeOf _ = mkTyConApp (mkTyCon "Logic.Morphism.SpanDomain") []
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (ShATermConvertible sublogics1, ShATermConvertible sublogics2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => ShATermConvertible (SublogicsPair sublogics1 sublogics2) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder toShATermAux att0 (SublogicsPair sub1 sub2) = do
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (att1,i1) <- toShATerm' att0 sub1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (att2,i2) <- toShATerm' att1 sub2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder return $ addATerm (ShAAppl "SublogicsPair" [i1,i2] []) att2
da955132262baab309a50fdffe228c9efe68251dCui Jian fromShATermAux ix att =
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu case getShATerm ix att of
da955132262baab309a50fdffe228c9efe68251dCui Jian ShAAppl "SublogicsPair" [i1, i2] _ ->
da955132262baab309a50fdffe228c9efe68251dCui Jian case fromShATerm' i2 att of
da955132262baab309a50fdffe228c9efe68251dCui Jian (att2, i2') -> case fromShATerm' i1 att2 of
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu (att1, i1') -> (att1, SublogicsPair i1' i2')
c18a07fe36512679e66faa59274bb273e735738aMihai Codescu u -> fromShATermError "SublogicsPair" u
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (Sublogics sublogics1, Sublogics sublogics2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => Sublogics (SublogicsPair sublogics1 sublogics2) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sublogic_names (SublogicsPair sub1 sub2) =
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu [ x1 ++ " " ++ x2
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu | x1 <- sublogic_names sub1
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu , x2 <- sublogic_names sub2 ]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance ( MinSublogic sublogics1 ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , Morphism cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder ) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder stability (SpanDomain _) = Experimental
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder data_logic (SpanDomain _) = Nothing
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder top_sublogic (SpanDomain cid) = SublogicsPair
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder (top_sublogic $ morSourceLogic cid) $ top_sublogic $ morTargetLogic cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder all_sublogics (SpanDomain cid) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder [ SublogicsPair x y
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder | x <- all_sublogics (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , y <- all_sublogics (morTargetLogic cid) ]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- project_sublogic_epsilon - default implementation for now
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich provers _ = []
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich cons_checkers _ = []
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich conservativityCheck l _ _ _ = statErr l "conservativityCheck"
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich empty_proof_tree (SpanDomain cid) = empty_proof_tree (morTargetLogic cid)