Morphism.hs revision d9a45a35cd696085be1a038b2cc67bee6819c574
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett , FlexibleInstances, UndecidableInstances, OverlappingInstances
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett , ExistentialQuantification, GeneralizedNewtypeDeriving #-}
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyModule : $Header$
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuDescription : interface (type class) for logic projections (morphisms) in Hets
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettLicense : GPLv2 or higher, see LICENSE.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : till@informatik.uni-bremen.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : non-portable (via Logic)
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettInterface (type class) for logic projections (morphisms) in Hets
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachProvides data structures for institution morphisms.
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach These are just collections of
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach functions between (some of) the types of logics.
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett{- References: see Logic.hs
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder morphism modifications / representation maps
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maederimport qualified Data.Set as Set
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblettclass (Language cid,
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett Logic lid1 sublogics1
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett sign1 morphism1 sign_symbol1 symbol1 proof_tree1,
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly Logic lid2 sublogics2
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly basic_spec2 sentence2 symb_items2 symb_map_items2
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly sign2 morphism2 sign_symbol2 symbol2 proof_tree2) =>
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett sign1 morphism1 sign_symbol1 symbol1 proof_tree1
765e55b764e0fd32c09d33709d6e2770c4766799Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign2 morphism2 sign_symbol2 symbol2 proof_tree2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly | cid -> lid1, cid -> lid2
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder , lid1 -> sublogics1 basic_spec1 sentence1 symb_items1
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder , lid2 -> sublogics2 basic_spec2 sentence2 symb_items2
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly {- source and target logic and sublogic
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly the source sublogic is the maximal one for which the comorphism works
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly the target sublogic is the resulting one -}
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly morSourceLogic :: cid -> lid1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly morSourceSublogic :: cid -> sublogics1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly morTargetLogic :: cid -> lid2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly morTargetSublogic :: cid -> sublogics2
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder -- finer information of target sublogics corresponding to source sublogics
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett morMapSublogicSign :: cid -> sublogics1 -> sublogics2
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett -- information about the source sublogics corresponding to target sublogics
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett morMapSublogicSen :: cid -> sublogics2 -> sublogics1
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett {- the translation functions are partial
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett because the target may be a sublanguage
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett we do not cover theoroidal morphisms,
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett since there are no relevant examples and they do not compose nicely
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett no mapping of theories, since signatures and sentences are mapped
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett contravariantly -}
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett morMap_sign :: cid -> sign1 -> Maybe sign2
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett morMap_morphism :: cid -> morphism1 -> Maybe morphism2
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett {- also covers semi-morphisms ??
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett with no sentence translation
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett - but these are spans! -}
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett morMap_sign_symbol :: cid -> sign_symbol1 -> Set.Set sign_symbol2
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett -- morConstituents not needed, because composition only via lax triangles
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | identity morphisms
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettdata IdMorphism lid sublogics =
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett IdMorphism lid sublogics deriving (Typeable, Show)
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettinstance Logic lid sublogics
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett basic_spec sentence symb_items symb_map_items
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett sign morphism sign_symbol symbol proof_tree =>
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett Language (IdMorphism lid sublogics) where
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett language_name (IdMorphism lid sub) = "id_" ++ language_name lid
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ++ case sublogicName sub of
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettinstance Logic lid sublogics
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett basic_spec sentence symb_items symb_map_items
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett sign morphism sign_symbol symbol proof_tree =>
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Morphism (IdMorphism lid sublogics)
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder lid sublogics
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder basic_spec sentence symb_items symb_map_items
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett sign morphism sign_symbol symbol proof_tree
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett lid sublogics
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett basic_spec sentence symb_items symb_map_items
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett sign morphism sign_symbol symbol proof_tree
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett morSourceLogic (IdMorphism lid _sub) = lid
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett morTargetLogic (IdMorphism lid _sub) = lid
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett morSourceSublogic (IdMorphism _lid sub) = sub
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett morTargetSublogic (IdMorphism _lid sub) = sub
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -- changed to identities!
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett morMapSublogicSign _ x = x
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly morMapSublogicSen _ x = x
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly morMap_sign _ = Just
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly morMap_morphism _ = Just
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly morMap_sentence _ _ = Just
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly morMap_sign_symbol _ = Set.singleton
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- composition not needed, use lax triangles instead
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- | comorphisms inducing morphisms
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettclass Comorphism cid
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sign1 morphism1 sign_symbol1 symbol1 proof_tree1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sign2 morphism2 sign_symbol2 symbol2 proof_tree2 =>
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett InducingComorphism cid
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach sign1 morphism1 sign_symbol1 symbol1 proof_tree1
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett sign2 morphism2 sign_symbol2 symbol2 proof_tree2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett indMorMap_sign :: cid -> sign2 -> Maybe sign1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett epsilon :: cid -> sign2 -> Maybe morphism2
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- ------------------------------------------------------------------------
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- Morphisms as spans of comorphisms
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett{- if the morphism is (psi, alpha, beta) : I -> J
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettit is replaced with the following span
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettSignI id -> SignI psi -> SignJ
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettSenI alpha <- psi;SenJ id -> psi;SenJ
31f039ffdb33d78cb31d24b71d3155b11a323975Andy GimblettModI beta -> psi^op;ModJ id <- psi^op;ModJ -}
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett{- 1. introduce a new logic for the domain of the span
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettthis logic will have
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettthe name (SpanDomain cid) where cid is the name of the morphism
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettsublogics - pairs (s1, s2) with s1 being a sublogic of I and s2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettbeing a sublogic of J; the lattice is the product lattice of the two
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblettexisting lattices
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillybasic_spec will be () - the unit type, because we mix signatures
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillywith sentences in specifications
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillysentence - sentences of J, wrapped
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillysymb_items - ()
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillysymb_map_items - ()
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettsign - signatures of I
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reillymorphism - morphisms of I
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reillysign_symbol - sign_symbols of I
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reillysymbol - symbols of I
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reillyproof_tree - proof_tree of J -}
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maederdata SpanDomain cid = SpanDomain cid deriving (Eq, Show)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettdata SublogicsPair a b = SublogicsPair a b deriving (Eq, Ord, Show, Typeable)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance Language cid => Language (SpanDomain cid) where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett language_name (SpanDomain cid) = "SpanDomain" ++ language_name cid
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett{- the category of signatures is exactly the category of signatures of
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettthe sublogic on which the morphism is defined, but with another name -}
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyinstance Morphism cid
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett sign1 morphism1 sign_symbol1 symbol1 proof_tree1
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign2 morphism2 sign_symbol2 symbol2 proof_tree2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly => Syntax (SpanDomain cid) () sign_symbol1 () ()
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly-- default is ok
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillynewtype S2 s = S2 { sentence2 :: s }
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly deriving (Eq, Ord, Show, Typeable, Data, ShATermConvertible, Pretty
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly , GetRange, ToJson)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance (Morphism cid
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sign1 morphism1 sign_symbol1 symbol1 proof_tree1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign2 morphism2 sign_symbol2 symbol2 proof_tree2)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign_symbol1 where
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly{- one has to take care about signature and morphisms
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyand translate them to targetLogic
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillywe get a Maybe sign/morphism -}
c60c643bbac58809100f35f187493b6f170314f0Liam O'Reilly map_sen (SpanDomain cid) mor1 (S2 sen) =
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly case morMap_morphism cid mor1 of
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Just mor2 -> fmap S2 $
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly map_sen (morTargetLogic cid) mor2 sen
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Nothing -> statFail (SpanDomain cid) "map_sen"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly simplify_sen (SpanDomain cid) sigma (S2 sen) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly case morMap_sign cid sigma of
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Just sigma2 -> S2 $
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly simplify_sen (morTargetLogic cid) sigma2 sen
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly Nothing -> error "simplify_sen"
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly print_named (SpanDomain cid) = print_named (morTargetLogic cid)
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett . mapNamed sentence2
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett sym_of (SpanDomain cid) = sym_of (morSourceLogic cid)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett symmap_of (SpanDomain cid) = symmap_of (morSourceLogic cid)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett sym_name (SpanDomain cid) = sym_name (morSourceLogic cid)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance (Morphism cid
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sign1 morphism1 sign_symbol1 symbol1 proof_tree1
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sign2 morphism2 sign_symbol2 symbol2 proof_tree2)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () ()
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sign1 morphism1 sign_symbol1 symbol1 where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly ensures_amalgamability l _ = statFail l "ensures_amalgamability"
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly symbol_to_raw (SpanDomain cid) = symbol_to_raw (morSourceLogic cid)
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett id_to_raw (SpanDomain cid) = id_to_raw (morSourceLogic cid)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett matches (SpanDomain cid) = matches (morSourceLogic cid)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly empty_signature (SpanDomain cid) = empty_signature (morSourceLogic cid)
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett signature_union (SpanDomain cid) = signature_union (morSourceLogic cid)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly final_union (SpanDomain cid) = final_union (morSourceLogic cid)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly morphism_union (SpanDomain cid) = morphism_union (morSourceLogic cid)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly is_subsig (SpanDomain cid) = is_subsig (morSourceLogic cid)
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett subsig_inclusion (SpanDomain cid) = subsig_inclusion (morSourceLogic cid)
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly generated_sign (SpanDomain cid) = generated_sign (morSourceLogic cid)
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett cogenerated_sign (SpanDomain cid) = cogenerated_sign (morSourceLogic cid)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett is_transportable (SpanDomain cid) = is_transportable (morSourceLogic cid)
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett is_injective (SpanDomain cid) = is_injective (morSourceLogic cid)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyinstance (SemiLatticeWithTop sublogics1, SemiLatticeWithTop sublogics2)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett => SemiLatticeWithTop (SublogicsPair sublogics1 sublogics2) where
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly top = SublogicsPair top top
5858e6262048894b0e933b547852f04aed009b58Andy Gimblett lub (SublogicsPair x1 y1) (SublogicsPair x2 y2) =
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly SublogicsPair (lub x1 x2) (lub y1 y2)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance (SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) where
c56c0630e0299eca5dd603cdac49aab4463c0671Liam O'Reilly minSublogic (S2 sen2) = SublogicsPair top (minSublogic sen2)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly{- just a dummy implementation, it should be the sublogic of sen2 in J
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillypaired with its image through morMapSublogicSen? -}
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly => MinSublogic (SublogicsPair sublogics1 sublogics2) alpha where
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly minSublogic x = SublogicsPair (minSublogic x) top
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly{- also should have instances of MinSublogic class for Sublogics-pair
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyand morphism1, sign_symbol1, sign1 this is why the wrapping is needed -}
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett{- instance SemiLatticeWithTop sublogics => MinSublogic sublogics () where
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyminSublogic _ = top -}
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett => ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly projectSublogic _ x = x
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- it should be used for (), morphism1, sign_symbol1, sign1
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance (MinSublogic sublogics1 sign1, SemiLatticeWithTop sublogics2)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett => ProjectSublogicM (SublogicsPair sublogics1 sublogics2) sign1 where
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly projectSublogicM _ = Just
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyinstance (ShATermConvertible a, ShATermConvertible b)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly => ShATermConvertible (SublogicsPair a b) where
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett toShATermAux att0 (SublogicsPair a b) = do
7cbbd12f559c5c700f521a52424b098db198f1b4Liam O'Reilly (att1, a') <- toShATerm' att0 a
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (att2, b') <- toShATerm' att1 b
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly return $ addATerm (ShAAppl "SublogicsPair" [a', b'] []) att2
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly fromShATermAux ix att0 = case getShATerm ix att0 of
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly ShAAppl "SublogicsPair" [a, b] _ ->
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly case fromShATerm' a att0 of { (att1, a') ->
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett case fromShATerm' b att1 of { (att2, b') ->
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly (att2, SublogicsPair a' b') }}
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly u -> fromShATermError "SublogicsPair" u
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance (SublogicName sublogics1, SublogicName sublogics2)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly => SublogicName (SublogicsPair sublogics1 sublogics2) where
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly sublogicName (SublogicsPair sub1 sub2) =
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett let s1 = sublogicName sub1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly s2 = sublogicName sub2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly in if null s1 then s2 else if null s2 then s1 else
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly s1 ++ "|" ++ s2
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyinstance ( MinSublogic sublogics1 ()
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , Morphism cid
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign1 morphism1 sign_symbol1 symbol1 proof_tree1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly sign2 morphism2 sign_symbol2 symbol2 proof_tree2
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) ()
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett stability (SpanDomain _) = Experimental
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly data_logic (SpanDomain _) = Nothing
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly top_sublogic (SpanDomain cid) = SublogicsPair
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly (top_sublogic $ morSourceLogic cid) $ top_sublogic $ morTargetLogic cid
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly all_sublogics (SpanDomain cid) =
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly [ SublogicsPair x y
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly | x <- all_sublogics (morSourceLogic cid)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett , y <- all_sublogics (morTargetLogic cid) ]
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly -- project_sublogic_epsilon - default implementation for now
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly provers _ = []
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly cons_checkers _ = []
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly conservativityCheck _ = []
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly empty_proof_tree (SpanDomain cid) = empty_proof_tree (morTargetLogic cid)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- * Morphisms
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | Existential type for morphisms
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillydata AnyMorphism = forall cid lid1 sublogics1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly basic_spec1 sentence1 symb_items1 symb_map_items1
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly lid2 sublogics2
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly basic_spec2 sentence2 symb_items2 symb_map_items2
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett lid1 sublogics1 basic_spec1 sentence1
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly symb_items1 symb_map_items1
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly sign1 morphism1 symbol1 raw_symbol1 proof_tree1
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly lid2 sublogics2 basic_spec2 sentence2
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly symb_items2 symb_map_items2
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance Eq AnyMorphism where
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Morphism cid1 == Morphism cid2 =
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly constituents cid1 == constituents cid2
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -- need to be refined, using morphism translations !!!
fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reillyinstance Show AnyMorphism where
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly show (Morphism cid) = language_name cid
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ++ " : " ++ language_name (morSourceLogic cid)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ++ " -> " ++ language_name (morTargetLogic cid)