Comorphism.hs revision 4184cb191a9081cb2a9cf3ef5f060f56f0ca5922
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- needs ghc -fglasgow-exts -package data
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Till Mossakowski, Christian Maeder
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Provides data structures logic (co)morphisms.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic (co)morphisms are just collections of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski functions between (some of) the types of logics.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski References: see Logic.hs
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Weak amalgamability, also for comorphisms
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski comorphism maps
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski comorphisms out of sublogic relationships
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Data.Maybe(catMaybes)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- Logic comorphisms (possibly also morphisms via adjointness)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiclass (Language cid,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid1 sublogics1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid2 sublogics2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism cid
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | cid -> lid1, cid -> lid2
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski sourceLogic :: cid -> lid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski source_sublogic :: cid -> sublogics1
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski targetLogic :: cid -> lid2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski target_sublogic :: cid -> sublogics2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- the translation functions are partial
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- because the target may be a sublanguage
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- cover theoroidal comorphisms as well
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sign :: cid -> sign1 -> Maybe (sign2,[sentence2])
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_morphism :: cid -> morphism1 -> Maybe morphism2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence :: cid -> sign1 -> sentence1 -> Maybe sentence2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- also covers semi-comorphisms
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- with no sentence translation
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- - but these are spans!
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_symbol :: cid -> symbol1 -> Set symbol2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata IdComorphism lid =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski IdComorphism lid deriving Show
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Language (IdComorphism lid) where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski language_name _ = "id_"++language_name (undefined::lid)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism (IdComorphism lid) --sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski --basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski --sign morphism symbol raw_symbol proof_tree)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski source_sublogic _ = top
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski target_sublogic _ = top
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sign _ = \sigma -> Just(sigma,[])
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_morphism _ = Just
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence _ = \_ -> Just
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_symbol _ = single
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata (Comorphism cid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism cid2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski CompComorphism cid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3 =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski CompComorphism cid1 cid2 deriving (Show)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskityconCompComorphism :: TyCon
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskityconCompComorphism = mkTyCon "CompComorphism"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Typeable (CompComorphism cid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3) where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski typeOf _ = mkAppTy tyconCompComorphism []
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance (Comorphism cid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism cid2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski => Language (CompComorphism cid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3) where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski language_name (CompComorphism cid1 cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski language_name cid1++";"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ++language_name cid2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance (Comorphism cid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism cid2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski => Comorphism (CompComorphism cid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski source_sublogic (CompComorphism cid1 _) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski source_sublogic cid1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski target_sublogic (CompComorphism _ cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski target_sublogic cid2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence (CompComorphism cid1 cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do (si2,_) <- map_sign cid1 si1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski se2 <- map_sentence cid1 si1 se1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence cid2 si2 se2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sign (CompComorphism cid1 cid2) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do (si2, se2s) <- map_sign cid1 si1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (si3, se3s) <- map_sign cid2 si2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return (si3, se3s ++ catMaybes
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (map (map_sentence cid2 si2) se2s))
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_morphism (CompComorphism cid1 cid2) = \ m1 -> map_morphism cid1 m1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski >>= map_morphism cid2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_symbol (CompComorphism cid1 cid2) = \ s1 -> unions
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (map (map_symbol cid2)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (toList (map_symbol cid1 s1)))
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiidComorphism l = IdComorphism l (empty_as l)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance (Logic lid1 sublogics1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid2 sublogics2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Typeable (Comorphism lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance (Logic lid1 sublogics1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid2 sublogics2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Eq (Comorphism lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski r1==r2 = language_name r1 == language_name r2 &&
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski language_name (source r1) == language_name (source r2) &&
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski language_name (target r1) == language_name (target r2) &&
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski coerce (source r1) (source r2) (source_sublogic r1) ==
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Just (source_sublogic r2) &&
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski coerce (target r1) (target r2) (target_sublogic r1) ==
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Just (target_sublogic r2)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance (Logic lid1 sublogics1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid2 sublogics2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Show (Comorphism lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski show r = show (source r) ++ " -> " ++ show (target r)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiid_comorphism ::
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree =>
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism lid sublogics basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid sublogics basic_spec sentence symb_items symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign morphism symbol raw_symbol proof_tree
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiid_comorphism lid =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- composition of logic comorphisms (diagrammatic order)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskicomp_comorphism ::
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (Logic lid1 sublogics1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid2 sublogics2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Logic lid3 sublogics3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_spec3 sentence3 symb_items3 symb_map_items3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -> Comorphism lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Comorphism lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign1 morphism1 symbol1 raw_symbol1 proof_tree1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign3 morphism3 symbol3 raw_symbol3 proof_tree3 )
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskicomp_comorphism r1 r2 = if target_sublogic r1 <<= source_sublogic r2 then
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Just(Comorphism{
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski language_name = language_name r1++";"++language_name r2,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski source = source r1, target = target r2,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski source_sublogic = source_sublogic r1,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski target_sublogic = target_sublogic r2,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do (si2,_) <- map_sign r1 si1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski se2 <- map_sentence r1 si1 se1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_sentence r2 si2 se2 ,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do (si2, se2s) <- map_sign r1 si1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (si3, se3s) <- map_sign r2 si2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return (si3, se3s ++ catMaybes
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (map (map_sentence r2 si2) se2s)) ,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski projection = undefined ,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_morphism = \ m1 -> map_morphism r1 m1 >>= map_morphism r2 ,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map_symbol = \ s1 -> unions
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (map (map_symbol r2) (toList (map_symbol r1 s1)))
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski }) else Nothing