Morphism.hs revision af0cbe339851fc558d2b18cde3666981325e667c
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlModule : $Header$
8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlDescription : interface (type class) for logic projections (morphisms) in Hets
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlMaintainer : till@tzi.de
8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlStability : provisional
8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlPortability : non-portable (via Logic)
8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlInterface (type class) for logic projections (morphisms) in Hets
8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlProvides data structures for institution morphisms.
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl These are just collections of
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl functions between (some of) the types of logics.
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl References: see Logic.hs
425f67c9c94605777800c1307ac38cc3965be571Martin Kühlimport qualified Data.Set as Set
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühlclass (Language cid,
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl Logic lid1 sublogics1
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl basic_spec1 sentence1 symb_items1 symb_map_items1
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl Logic lid2 sublogics2
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl basic_spec2 sentence2 symb_items2 symb_map_items2
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl Morphism cid
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl sign1 morphism1 symbol1 raw_symbol1 proof_tree1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl | cid -> lid1, cid -> lid2
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl -- source and target logic and sublogic
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl -- the source sublogic is the maximal one for which the comorphism works
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl -- the target sublogic is the resulting one
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl morSourceLogic :: cid -> lid1
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl morSourceSublogic :: cid -> sublogics1
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl morTargetLogic :: cid -> lid2
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl morTargetSublogic :: cid -> sublogics2
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl -- finer information of target sublogics corresponding to source sublogics
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl morMapSublogic :: cid -> sublogics1 -> sublogics2
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl -- default implementation
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl-- morMapSublogic cid _ = targetSublogic cid
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl -- the translation functions are partial
425f67c9c94605777800c1307ac38cc3965be571Martin Kühl -- because the target may be a sublanguage
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl -- we do not cover theoroidal morphisms,
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl -- since there are no relevant examples and they do not compose nicely
425f67c9c94605777800c1307ac38cc3965be571Martin Kühl -- no mapping of theories, since signatrures and sentences are mapped
425f67c9c94605777800c1307ac38cc3965be571Martin Kühl -- contravariantly
425f67c9c94605777800c1307ac38cc3965be571Martin Kühl morMap_sign :: cid -> sign1 -> Maybe sign2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder morMap_morphism :: cid -> morphism1 -> Maybe morphism2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
425f67c9c94605777800c1307ac38cc3965be571Martin Kühl -- also covers semi-morphisms ??
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco -- with no sentence translation
425f67c9c94605777800c1307ac38cc3965be571Martin Kühl -- - but these are spans!
425f67c9c94605777800c1307ac38cc3965be571Martin Kühl morMap_symbol :: cid -> symbol1 -> Set.Set symbol2
8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl -- morConstituents not needed, because composition only via lax triangles
425f67c9c94605777800c1307ac38cc3965be571Martin Kühl-- identity morphisms
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühldata IdMorphism lid sublogics =
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl IdMorphism lid sublogics deriving Show
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin KühlidMorphismTc :: TyCon
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin KühlidMorphismTc = mkTyCon "Logic.Morphism.IdMorphism"
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühlinstance Typeable (IdMorphism lid sub) where
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl typeOf _ = mkTyConApp idMorphismTc []
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühlinstance Logic lid sublogics
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl basic_spec sentence symb_items symb_map_items
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl sign morphism symbol raw_symbol proof_tree =>
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl Language (IdMorphism lid sublogics) where
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl language_name (IdMorphism lid sub) =
4533f0100d33e9a579b8caf73d1c28b11c8a6e26Martin Kühl case sublogic_names sub of
4533f0100d33e9a579b8caf73d1c28b11c8a6e26Martin Kühl [] -> error "language_name IdMorphism"
4533f0100d33e9a579b8caf73d1c28b11c8a6e26Martin Kühl h : _ -> "id_" ++ language_name lid ++ "." ++ h
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühlinstance Logic lid sublogics
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl basic_spec sentence symb_items symb_map_items
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign morphism symbol raw_symbol proof_tree =>
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl Morphism (IdMorphism lid sublogics)
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl lid sublogics
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl basic_spec sentence symb_items symb_map_items
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sign morphism symbol raw_symbol proof_tree
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl lid sublogics
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl basic_spec sentence symb_items symb_map_items
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl sign morphism symbol raw_symbol proof_tree
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl morSourceLogic (IdMorphism lid _sub) = lid
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl morTargetLogic (IdMorphism lid _sub) = lid
ecf79f3ba9d0ae326915831eab64b1deb1f0e672Martin Kühl morSourceSublogic (IdMorphism _lid sub) = sub
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder morTargetSublogic (IdMorphism _lid sub) = sub
62710dbd25738bda353362e457e42a4fa072332aMartin Kühl morMapSublogic _ _ =
9c3072fb010b501fc8ac94a5b66086d49b7756c2Martin Kühl error "Logic.Morphism.IdMorphism.morMapSublogic"
62710dbd25738bda353362e457e42a4fa072332aMartin Kühl morMap_sign _ = Just
62710dbd25738bda353362e457e42a4fa072332aMartin Kühl morMap_morphism _ = Just
morMap_symbol _ = Set.singleton