Comorphism.hs revision 8731f7b93b26083dc34a2c0937cd6493b42f2c2c
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- needs ghc -fglasgow-exts -package data
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder{- HetCATS/Comorphism.hs
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder $Id$
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Till Mossakowski, Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Provides data structures logic (co)morphisms.
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Logic (co)morphisms are just collections of
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder functions between (some of) the types of logics.
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder References: see Logic.hs
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Todo:
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Weak amalgamability, also for comorphisms
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder comorphism maps
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder comorphisms out of sublogic relationships
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedermodule Logic.Comorphism where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Logic.Logic
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Common.Lib.Set
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Data.Maybe(catMaybes)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Data.Dynamic
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- Logic comorphisms (possibly also morphisms via adjointness)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederclass (Language cid,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Logic lid1 sublogics1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Logic lid2 sublogics2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Comorphism cid
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder | cid -> lid1, cid -> lid2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sourceLogic :: cid -> lid1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sourceSublogic :: cid -> sublogics1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder targetLogic :: cid -> lid2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder targetSublogic :: cid -> sublogics2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder -- the translation functions are partial
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder -- because the target may be a sublanguage
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder -- cover theoroidal comorphisms as well
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder map_sign :: cid -> sign1 -> Maybe (sign2,[sentence2])
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder map_morphism :: cid -> morphism1 -> Maybe morphism2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder map_sentence :: cid -> sign1 -> sentence1 -> Maybe sentence2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder -- also covers semi-comorphisms
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder -- with no sentence translation
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder -- - but these are spans!
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder map_symbol :: cid -> symbol1 -> Set symbol2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederdata IdComorphism lid =
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder IdComorphism lid deriving Show
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Logic lid sublogics
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec sentence symb_items symb_map_items
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign morphism symbol raw_symbol proof_tree =>
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Language (IdComorphism lid) where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder language_name _ = "id_"++language_name (undefined::lid)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maederinstance Logic lid sublogics
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec sentence symb_items symb_map_items
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder sign morphism symbol raw_symbol proof_tree =>
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder Comorphism (IdComorphism lid) --sublogics
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder --basic_spec sentence symb_items symb_map_items
35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maeder --sign morphism symbol raw_symbol proof_tree)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder lid sublogics
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec sentence symb_items symb_map_items
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign morphism symbol raw_symbol proof_tree
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder lid sublogics
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec sentence symb_items symb_map_items
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign morphism symbol raw_symbol proof_tree
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder where
7325bbe03797fd413af504fb3fac109b2c652a7bChristian Maeder sourceLogic (IdComorphism lid) = lid
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder targetLogic (IdComorphism lid) = lid
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sourceSublogic _ = top
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder targetSublogic _ = top
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder map_sign _ = \sigma -> Just(sigma,[])
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder map_morphism _ = Just
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder map_sentence _ = \_ -> Just
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder map_symbol _ = single
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowskidata (Comorphism cid1
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
1865083b72c1307e9040d78c2743abd5a54ee260Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1865083b72c1307e9040d78c2743abd5a54ee260Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
3a3bbc51abf804d91bc9d8e0f2ce745cfae4c9c7Christian Maeder Comorphism cid2
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3) =>
f624c6980131e5b0598e00e7d8b4acb9720f8996Christian Maeder CompComorphism cid1
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
f624c6980131e5b0598e00e7d8b4acb9720f8996Christian Maeder cid2
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
3a3bbc51abf804d91bc9d8e0f2ce745cfae4c9c7Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3 =
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder CompComorphism cid1 cid2 deriving (Show)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedertyconCompComorphism :: TyCon
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till MossakowskityconCompComorphism = mkTyCon "CompComorphism"
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Typeable (CompComorphism cid1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
1865083b72c1307e9040d78c2743abd5a54ee260Christian Maeder cid2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3) where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder typeOf _ = mkAppTy tyconCompComorphism []
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maederinstance (Comorphism cid1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Comorphism cid2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder => Language (CompComorphism cid1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder cid2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1509ea46b471bef1c5e70864fb1cfc0a5280266bChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3) where
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder language_name (CompComorphism cid1 cid2) =
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder language_name cid1++";"
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder ++language_name cid2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maederinstance (Comorphism cid1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder Comorphism cid2
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder => Comorphism (CompComorphism cid1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder cid2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder where
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sourceLogic (CompComorphism cid1 _) =
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sourceLogic cid1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder targetLogic (CompComorphism _ cid2) =
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder targetLogic cid2
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder sourceSublogic (CompComorphism cid1 _) =
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder sourceSublogic cid1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder targetSublogic (CompComorphism _ cid2) =
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder targetSublogic cid2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder map_sentence (CompComorphism cid1 cid2) =
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder \si1 se1 ->
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder do (si2,_) <- map_sign cid1 si1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder se2 <- map_sentence cid1 si1 se1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder map_sentence cid2 si2 se2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder map_sign (CompComorphism cid1 cid2) =
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder \si1 ->
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder do (si2, se2s) <- map_sign cid1 si1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder (si3, se3s) <- map_sign cid2 si2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder return (si3, se3s ++ catMaybes
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder (map (map_sentence cid2 si2) se2s))
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder map_morphism (CompComorphism cid1 cid2) = \ m1 -> map_morphism cid1 m1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder >>= map_morphism cid2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder map_symbol (CompComorphism cid1 cid2) = \ s1 -> unions
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (map (map_symbol cid2)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (toList (map_symbol cid1 s1)))
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder{-
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederidComorphism l = IdComorphism l (empty_as l)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maederinstance (Logic lid1 sublogics1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Logic lid2 sublogics2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Typeable (Comorphism lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance (Logic lid1 sublogics1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Logic lid2 sublogics2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Eq (Comorphism lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
7325bbe03797fd413af504fb3fac109b2c652a7bChristian Maeder where
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder r1==r2 = language_name r1 == language_name r2 &&
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder language_name (source r1) == language_name (source r2) &&
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder language_name (target r1) == language_name (target r2) &&
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder coerce (source r1) (source r2) (sourceSublogic r1) ==
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Just (sourceSublogic r2) &&
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder coerce (target r1) (target r2) (targetSublogic r1) ==
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder Just (targetSublogic r2)
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder
7325bbe03797fd413af504fb3fac109b2c652a7bChristian Maederinstance (Logic lid1 sublogics1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder Logic lid2 sublogics2
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder Show (Comorphism lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder where
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder show r = show (source r) ++ " -> " ++ show (target r)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maederid_comorphism ::
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder Logic lid sublogics
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder basic_spec sentence symb_items symb_map_items
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski sign morphism symbol raw_symbol proof_tree =>
50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder lid ->
90bf4bf40789422552e566b73738ba5efae144c3Christian Maeder Comorphism lid sublogics basic_spec sentence symb_items symb_map_items
3a3bbc51abf804d91bc9d8e0f2ce745cfae4c9c7Christian Maeder sign morphism symbol raw_symbol proof_tree
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski lid sublogics basic_spec sentence symb_items symb_map_items
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign morphism symbol raw_symbol proof_tree
eb483f2216949400bfef8f6deb5320f071445626Christian Maederid_comorphism lid =
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Comorphism {
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- composition of logic comorphisms (diagrammatic order)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedercomp_comorphism ::
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (Logic lid1 sublogics1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Logic lid2 sublogics2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Logic lid3 sublogics3
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder basic_spec3 sentence3 symb_items3 symb_map_items3
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sign3 morphism3 symbol3 raw_symbol3 proof_tree3
3639c2cf7f65e04c883054f4a52c6fa733663304Christian Maeder ) =>
Comorphism lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2
-> Comorphism lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2
lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
sign3 morphism3 symbol3 raw_symbol3 proof_tree3
-> Maybe (
Comorphism lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
sign3 morphism3 symbol3 raw_symbol3 proof_tree3 )
comp_comorphism r1 r2 = if targetSublogic r1 <<= sourceSublogic r2 then
Just(Comorphism{
language_name = language_name r1++";"++language_name r2,
source = source r1, target = target r2,
sourceSublogic = sourceSublogic r1,
targetSublogic = targetSublogic r2,
map_sentence =
\si1 se1 ->
do (si2,_) <- map_sign r1 si1
se2 <- map_sentence r1 si1 se1
map_sentence r2 si2 se2 ,
map_sign =
\si1 ->
do (si2, se2s) <- map_sign r1 si1
(si3, se3s) <- map_sign r2 si2
return (si3, se3s ++ catMaybes
(map (map_sentence r2 si2) se2s)) ,
projection = undefined ,
map_morphism = \ m1 -> map_morphism r1 m1 >>= map_morphism r2 ,
map_symbol = \ s1 -> unions
(map (map_symbol r2) (toList (map_symbol r1 s1)))
}) else Nothing
-}