8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable
d9a45a35cd696085be1a038b2cc67bee6819c574cmaeder , FlexibleInstances, UndecidableInstances, OverlappingInstances
8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder , ExistentialQuantification, GeneralizedNewtypeDeriving #-}
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederDescription : interface (type class) for logic projections (morphisms) in Hets
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : till@informatik.uni-bremen.de
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiStability : provisional
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till MossakowskiPortability : non-portable (via Logic)
09b431a868c79a92ae7c9bd141565f43f9034144Christian MaederInterface (type class) for logic projections (morphisms) in Hets
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian MaederProvides data structures for institution morphisms.
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski These are just collections of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski functions between (some of) the types of logics.
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- References: see Logic.hs
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morphism modifications / representation maps
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiclass (Language cid,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Logic lid1 sublogics1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1,
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Logic lid2 sublogics2
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2) =>
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder | cid -> lid1, cid -> lid2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , lid1 -> sublogics1 basic_spec1 sentence1 symb_items1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , lid2 -> sublogics2 basic_spec2 sentence2 symb_items2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder {- source and target logic and sublogic
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder the source sublogic is the maximal one for which the comorphism works
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder the target sublogic is the resulting one -}
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceLogic :: cid -> lid1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceSublogic :: cid -> sublogics1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetLogic :: cid -> lid2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetSublogic :: cid -> sublogics2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- finer information of target sublogics corresponding to source sublogics
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morMapSublogicSign :: cid -> sublogics1 -> sublogics2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- information about the source sublogics corresponding to target sublogics
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morMapSublogicSen :: cid -> sublogics2 -> sublogics1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder {- the translation functions are partial
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder because the target may be a sublanguage
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder we do not cover theoroidal morphisms,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder since there are no relevant examples and they do not compose nicely
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder no mapping of theories, since signatures and sentences are mapped
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder contravariantly -}
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sign :: cid -> sign1 -> Maybe sign2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_morphism :: cid -> morphism1 -> Maybe morphism2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder {- also covers semi-morphisms ??
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder with no sentence translation
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder - but these are spans! -}
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morMap_sign_symbol :: cid -> sign_symbol1 -> Set.Set sign_symbol2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski -- morConstituents not needed, because composition only via lax triangles
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | identity morphisms
adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maederdata IdMorphism lid sublogics =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder IdMorphism lid sublogics deriving (Typeable, Show)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Logic lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign morphism sign_symbol symbol proof_tree =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Language (IdMorphism lid sublogics) where
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder language_name (IdMorphism lid sub) = "id_" ++ language_name lid
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder ++ case sublogicName sub of
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiinstance Logic lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign morphism sign_symbol symbol proof_tree =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski Morphism (IdMorphism lid sublogics)
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign morphism sign_symbol symbol proof_tree
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid sublogics
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski basic_spec sentence symb_items symb_map_items
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign morphism sign_symbol symbol proof_tree
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceLogic (IdMorphism lid _sub) = lid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetLogic (IdMorphism lid _sub) = lid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morSourceSublogic (IdMorphism _lid sub) = sub
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morTargetSublogic (IdMorphism _lid sub) = sub
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- changed to identities!
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu morMapSublogicSign _ x = x
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu morMapSublogicSen _ x = x
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_sign _ = Just
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski morMap_morphism _ = Just
e7d2b3903c7b44db432538b0d720c21062c24823Christian Maeder morMap_sentence _ _ = Just
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morMap_sign_symbol _ = Set.singleton
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski-- composition not needed, use lax triangles instead
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | comorphisms inducing morphisms
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskiclass Comorphism cid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2 =>
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski InducingComorphism cid
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski indMorMap_sign :: cid -> sign2 -> Maybe sign1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski epsilon :: cid -> sign2 -> Maybe morphism2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------------------------------------------------------------------
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder-- Morphisms as spans of comorphisms
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- if the morphism is (psi, alpha, beta) : I -> J
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederit is replaced with the following span
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederSignI id -> SignI psi -> SignJ
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederSenI alpha <- psi;SenJ id -> psi;SenJ
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederModI beta -> psi^op;ModJ id <- psi^op;ModJ -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- 1. introduce a new logic for the domain of the span
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederthis logic will have
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederthe name (SpanDomain cid) where cid is the name of the morphism
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedersublogics - pairs (s1, s2) with s1 being a sublogic of I and s2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederbeing a sublogic of J; the lattice is the product lattice of the two
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederexisting lattices
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederbasic_spec will be () - the unit type, because we mix signatures
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederwith sentences in specifications
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedersentence - sentences of J, wrapped
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedersymb_map_items - ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedersign - signatures of I
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedermorphism - morphisms of I
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedersign_symbol - sign_symbols of I
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedersymbol - symbols of I
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederproof_tree - proof_tree of J -}
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederdata SpanDomain cid = SpanDomain cid deriving (Eq, Show)
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maederdata SublogicsPair a b = SublogicsPair a b deriving (Eq, Ord, Show, Typeable)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Language cid => Language (SpanDomain cid) where
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder language_name (SpanDomain cid) = "SpanDomain" ++ language_name cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- the category of signatures is exactly the category of signatures of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederthe sublogic on which the morphism is defined, but with another name -}
c8117ae0b6088d835211e494aef229558c814bd3cmaederinstance (Morphism cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
c8117ae0b6088d835211e494aef229558c814bd3cmaeder , Pretty sign_symbol1)
a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowski => Syntax (SpanDomain cid) () sign_symbol1 () ()
4d7d53fec6b551333c79da6ae3b8ca2af0a741abChristian Maeder-- default is ok
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maedernewtype S2 s = S2 { sentence2 :: s }
d9a45a35cd696085be1a038b2cc67bee6819c574cmaeder deriving (Eq, Ord, Show, Typeable, Data, ShATermConvertible, Pretty
f5e43c6208179131e179f075248880a8cae1e111cmaeder , GetRange, ToJson, ToXml)
c8117ae0b6088d835211e494aef229558c814bd3cmaederinstance (Morphism cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
3f5a42972cccb9c4fd0821def1292ec40b7a4871cmaeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
c8117ae0b6088d835211e494aef229558c814bd3cmaeder , Category sign1 morphism1, Ord sign_symbol1, GetRange sign_symbol1)
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign_symbol1 where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- one has to take care about signature and morphisms
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederand translate them to targetLogic
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder map_sen (SpanDomain cid) mor1 (S2 sen) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder case morMap_morphism cid mor1 of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Just mor2 -> fmap S2 $
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder map_sen (morTargetLogic cid) mor2 sen
e7d2b3903c7b44db432538b0d720c21062c24823Christian Maeder Nothing -> statFail (SpanDomain cid) "map_sen"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder simplify_sen (SpanDomain cid) sigma (S2 sen) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder case morMap_sign cid sigma of
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Just sigma2 -> S2 $
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder simplify_sen (morTargetLogic cid) sigma2 sen
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder Nothing -> error "simplify_sen"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder print_named (SpanDomain cid) = print_named (morTargetLogic cid)
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder . mapNamed sentence2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sym_of (SpanDomain cid) = sym_of (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder symmap_of (SpanDomain cid) = symmap_of (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sym_name (SpanDomain cid) = sym_name (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (Morphism cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
c8117ae0b6088d835211e494aef229558c814bd3cmaeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
c8117ae0b6088d835211e494aef229558c814bd3cmaeder , Ord symbol1, GetRange symbol1, Pretty symbol1, Typeable symbol1)
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 where
e7d2b3903c7b44db432538b0d720c21062c24823Christian Maeder ensures_amalgamability l _ = statFail l "ensures_amalgamability"
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder symbol_to_raw (SpanDomain cid) = symbol_to_raw (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder id_to_raw (SpanDomain cid) = id_to_raw (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder matches (SpanDomain cid) = matches (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder empty_signature (SpanDomain cid) = empty_signature (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder signature_union (SpanDomain cid) = signature_union (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder final_union (SpanDomain cid) = final_union (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder morphism_union (SpanDomain cid) = morphism_union (morSourceLogic cid)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder is_subsig (SpanDomain cid) = is_subsig (morSourceLogic cid)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder subsig_inclusion (SpanDomain cid) = subsig_inclusion (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder generated_sign (SpanDomain cid) = generated_sign (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder cogenerated_sign (SpanDomain cid) = cogenerated_sign (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder is_transportable (SpanDomain cid) = is_transportable (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder is_injective (SpanDomain cid) = is_injective (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (SemiLatticeWithTop sublogics1, SemiLatticeWithTop sublogics2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => SemiLatticeWithTop (SublogicsPair sublogics1 sublogics2) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder top = SublogicsPair top top
8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder lub (SublogicsPair x1 y1) (SublogicsPair x2 y2) =
8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder SublogicsPair (lub x1 x2) (lub y1 y2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder minSublogic (S2 sen2) = SublogicsPair top (minSublogic sen2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- just a dummy implementation, it should be the sublogic of sen2 in J
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederpaired with its image through morMapSublogicSen? -}
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescuinstance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu => MinSublogic (SublogicsPair sublogics1 sublogics2) alpha where
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu minSublogic x = SublogicsPair (minSublogic x) top
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder{- also should have instances of MinSublogic class for Sublogics-pair
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederand morphism1, sign_symbol1, sign1 this is why the wrapping is needed -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- instance SemiLatticeWithTop sublogics => MinSublogic sublogics () where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederminSublogic _ = top -}
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescuinstance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu => ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha where
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder projectSublogic _ x = x
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu-- it should be used for (), morphism1, sign_symbol1, sign1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance (MinSublogic sublogics1 sign1, SemiLatticeWithTop sublogics2)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder => ProjectSublogicM (SublogicsPair sublogics1 sublogics2) sign1 where
e7d2b3903c7b44db432538b0d720c21062c24823Christian Maeder projectSublogicM _ = Just
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maederinstance (ShATermConvertible a, ShATermConvertible b)
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder => ShATermConvertible (SublogicsPair a b) where
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder toShATermAux att0 (SublogicsPair a b) = do
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder (att1, a') <- toShATerm' att0 a
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder (att2, b') <- toShATerm' att1 b
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return $ addATerm (ShAAppl "SublogicsPair" [a', b'] []) att2
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder fromShATermAux ix att0 = case getShATerm ix att0 of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ShAAppl "SublogicsPair" [a, b] _ ->
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder case fromShATerm' a att0 of { (att1, a') ->
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder case fromShATerm' b att1 of { (att2, b') ->
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder (att2, SublogicsPair a' b') }}
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder u -> fromShATermError "SublogicsPair" u
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maederinstance (SublogicName sublogics1, SublogicName sublogics2)
c911a0ec80ca4a178399c68f1e28be4e2bf42fceChristian Maeder => SublogicName (SublogicsPair sublogics1 sublogics2) where
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder sublogicName (SublogicsPair sub1 sub2) =
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder let s1 = sublogicName sub1
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder s2 = sublogicName sub2
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder in if null s1 then s2 else if null s2 then s1 else
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder s1 ++ "|" ++ s2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederinstance ( MinSublogic sublogics1 ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , Morphism cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign1 morphism1 sign_symbol1 symbol1 proof_tree1
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder sign2 morphism2 sign_symbol2 symbol2 proof_tree2
c8117ae0b6088d835211e494aef229558c814bd3cmaeder , Ord proof_tree2, Show proof_tree2)
c8117ae0b6088d835211e494aef229558c814bd3cmaeder => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) ()
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder stability (SpanDomain _) = Experimental
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder data_logic (SpanDomain _) = Nothing
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder top_sublogic (SpanDomain cid) = SublogicsPair
e8eb2b9d68adc3024eb1aa9899b902ed5a3fb460Christian Maeder (top_sublogic $ morSourceLogic cid) $ top_sublogic $ morTargetLogic cid
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder all_sublogics (SpanDomain cid) =
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder [ SublogicsPair x y
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder | x <- all_sublogics (morSourceLogic cid)
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder , y <- all_sublogics (morTargetLogic cid) ]
09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder -- project_sublogic_epsilon - default implementation for now
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich provers _ = []
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich cons_checkers _ = []
c40a1fdc8ec6978bd27240d6780d0e0a7b6b0056Dominik Luecke conservativityCheck _ = []
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich empty_proof_tree (SpanDomain cid) = empty_proof_tree (morTargetLogic cid)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- * Morphisms
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | Existential type for morphisms
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederdata AnyMorphism = forall cid lid1 sublogics1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid2 sublogics2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid1 sublogics1 basic_spec1 sentence1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder symb_items1 symb_map_items1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder lid2 sublogics2 basic_spec2 sentence2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder symb_items2 symb_map_items2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Eq AnyMorphism where
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Morphism cid1 == Morphism cid2 =
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder constituents cid1 == constituents cid2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -- need to be refined, using morphism translations !!!
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Show AnyMorphism where
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder show (Morphism cid) = language_name cid
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ++ " : " ++ language_name (morSourceLogic cid)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ++ " -> " ++ language_name (morTargetLogic cid)