Comorphism.hs revision 230a51f3c282a3222d1cf40c2040fee19259964e
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)
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowskiclass (Language cid, Typeable 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
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski | cid -> lid1, cid -> lid2,
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski cid -> sublogics1, cid -> basic_spec1, cid -> sentence1,
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski cid -> symb_items1, cid -> symb_map_items1, cid -> sign1,
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski cid -> morphism1, cid -> symbol1, cid -> raw_symbol1,
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski cid -> proof_tree1, cid -> sublogics2, cid -> basic_spec2,
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski cid -> sentence2, cid -> symb_items2,
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski cid -> symb_map_items2, cid -> sign2, cid -> morphism2,
788dd403da4203e895e15892ef7fa48129617d30Till Mossakowski cid -> symbol2, cid -> raw_symbol2, cid -> proof_tree2
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski sourceLogic :: cid -> lid1
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic :: cid -> sublogics1
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski targetLogic :: cid -> lid2
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski targetSublogic :: 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
425b287f28abf82702d46c176a38b668fb017ce4Felix Reckers fromShATerm_sign1 :: (ATermConvertible sign) => cid -> ATermTable -> sign
425b287f28abf82702d46c176a38b668fb017ce4Felix Reckers fromShATerm_sign1 cid att = fromShATerm att
425b287f28abf82702d46c176a38b668fb017ce4Felix Reckers fromShATerm_morphism2 :: (ATermConvertible morphism) => cid -> ATermTable -> morphism
425b287f28abf82702d46c176a38b668fb017ce4Felix Reckers fromShATerm_morphism2 cid att = fromShATerm att
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata IdComorphism lid =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski IdComorphism lid deriving Show
8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiidComorphismTc :: TyCon
8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskiidComorphismTc = mkTyCon "Logic.Comorphism.IdComorphism"
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowskiinstance Typeable (IdComorphism lid) where
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski typeOf s = mkAppTy idComorphismTc []
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski --[typeOf ((undefined :: IdComorphism a -> a) s)]
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
230a51f3c282a3222d1cf40c2040fee19259964eTill Mossakowski language_name (IdComorphism lid) =
230a51f3c282a3222d1cf40c2040fee19259964eTill Mossakowski "id_"++language_name 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
5e21bb46b24f477dafad6fdeff51aed7aaad0a47Till Mossakowski sourceLogic (IdComorphism lid) = lid
5e21bb46b24f477dafad6fdeff51aed7aaad0a47Till Mossakowski targetLogic (IdComorphism lid) = lid
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic _ = top
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski targetSublogic _ = 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
8db2d2c5a8df6dd6d7302bc59577150b87237940Till MossakowskityconCompComorphism = mkTyCon "Logic.Comorphism.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
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski sourceLogic (CompComorphism cid1 _) =
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski sourceLogic cid1
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski targetLogic (CompComorphism _ cid2) =
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski targetLogic cid2
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic (CompComorphism cid1 _) =
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski sourceSublogic cid1
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski targetSublogic (CompComorphism _ cid2) =
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski targetSublogic 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)))