-- the source sublogic is the maximal one for which the comorphism works
-- the target sublogic is the resulting one
morSourceLogic :: cid -> lid1
morSourceSublogic :: cid -> sublogics1
morTargetLogic :: cid -> lid2
morTargetSublogic :: cid -> sublogics2
-- finer information of target sublogics corresponding to source sublogics
morMapSublogicSign :: cid -> sublogics1 -> sublogics2
-- information about the source sublogics corresponding to target sublogics
morMapSublogicSen :: cid -> sublogics2 -> sublogics1
-- the translation functions are partial
-- because the target may be a sublanguage
-- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
-- we do not cover theoroidal morphisms,
-- since there are no relevant examples and they do not compose nicely
-- no mapping of theories, since signatures and sentences are mapped
morMap_sign :: cid -> sign1 -> Maybe sign2
morMap_morphism :: cid -> morphism1 -> Maybe morphism2
morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
-- also covers semi-morphisms ??
-- with no sentence translation
-- - but these are spans!
morMap_sign_symbol :: cid -> sign_symbol1 ->
Set.Set sign_symbol2
-- morConstituents not needed, because composition only via lax triangles
data IdMorphism lid sublogics =
IdMorphism lid sublogics deriving (Typeable, Show)
instance Logic lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism sign_symbol symbol proof_tree =>
Language (IdMorphism lid sublogics) where
language_name (IdMorphism lid sub) = "id_" ++ language_name lid
++ case sublogicName sub of
instance Logic lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism sign_symbol symbol proof_tree =>
Morphism (IdMorphism lid sublogics)
basic_spec sentence symb_items symb_map_items
sign morphism sign_symbol symbol proof_tree
basic_spec sentence symb_items symb_map_items
sign morphism sign_symbol symbol proof_tree
morSourceLogic (IdMorphism lid _sub) = lid
morTargetLogic (IdMorphism lid _sub) = lid
morSourceSublogic (IdMorphism _lid sub) = sub
morTargetSublogic (IdMorphism _lid sub) = sub
morMapSublogicSign _ x = x
morMapSublogicSen _ x = x
morMap_sentence _ _ = Just
-- composition not needed, use lax triangles instead
-- | comorphisms inducing morphisms
lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 sign_symbol1 symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 sign_symbol2 symbol2 proof_tree2 =>
lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 sign_symbol1 symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 sign_symbol2 symbol2 proof_tree2
indMorMap_sign :: cid -> sign2 -> Maybe sign1
indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
epsilon :: cid -> sign2 -> Maybe morphism2
--------------------------------------------------------------------------
-- Morphisms as spans of comorphisms
-- if the morphism is (psi, alpha, beta) : I -> J
-- it is replaced with the following span
-- SignI id -> SignI psi -> SignJ
-- SenI alpha <- psi;SenJ id -> psi;SenJ
-- ModI beta -> psi^op;ModJ id <- psi^op;ModJ
-- 1. introduce a new logic for the domain of the span
-- * the name (SpanDomain cid) where cid is the name of the morphism
-- * sublogics - pairs (s1, s2) with s1 being a sublogic of I and s2
-- being a sublogic of J; the lattice is the product lattice of the two
-- * basic_spec will be () - the unit type, because we mix signatures
-- with sentences in specifications
-- * sentence - sentences of J, wrapped
-- * sign - signatures of I
-- * morphism - morphisms of I
-- * sign_symbol - sign_symbols of I
-- * symbol - symbols of I
-- * proof_tree - proof_tree of J
data SpanDomain cid = SpanDomain cid deriving (Eq, Show)
data SublogicsPair a b = SublogicsPair a b deriving (Eq, Ord, Show, Typeable)
instance Language cid => Language (SpanDomain cid) where
language_name (SpanDomain cid) = "SpanDomain" ++ language_name cid
{- the category of signatures is exactly the category of signatures of
the sublogic on which the morphism is defined, but with another name -}
lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 sign_symbol1 symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 sign_symbol2 symbol2 proof_tree2
=> Syntax (SpanDomain cid) () () ()
newtype S2 s = S2 { sentence2 :: s }
deriving (Eq, Ord, Show, Typeable, ShATermConvertible, Pretty)
lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 sign_symbol1 symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 sign_symbol2 symbol2 proof_tree2
=> Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1
--one has to take care about signature and morphisms
--and translate them to targetLogic
map_sen (SpanDomain cid) mor1 (S2 sen) =
case morMap_morphism cid mor1 of
map_sen (morTargetLogic cid) mor2 sen
Nothing -> statFail (SpanDomain cid) "map_sen"
simplify_sen (SpanDomain cid) sigma (S2 sen) =
case morMap_sign cid sigma of
simplify_sen (morTargetLogic cid) sigma2 sen
Nothing -> error "simplify_sen"
parse_sentence (SpanDomain cid) = fmap (fmap S2) $
parse_sentence (morTargetLogic cid)
print_named (SpanDomain cid) = print_named (morTargetLogic cid)
sym_of (SpanDomain cid) = sym_of (morSourceLogic cid)
symmap_of (SpanDomain cid) = symmap_of (morSourceLogic cid)
sym_name (SpanDomain cid) = sym_name (morSourceLogic cid)
lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 sign_symbol1 symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 sign_symbol2 symbol2 proof_tree2)
=> StaticAnalysis (SpanDomain cid) () (S2 sentence2) () ()
sign1 morphism1 sign_symbol1 symbol1 where
ensures_amalgamability l _ = statFail l "ensures_amalgamability"
symbol_to_raw (SpanDomain cid) = symbol_to_raw (morSourceLogic cid)
id_to_raw (SpanDomain cid) = id_to_raw (morSourceLogic cid)
matches (SpanDomain cid) = matches (morSourceLogic cid)
empty_signature (SpanDomain cid) = empty_signature (morSourceLogic cid)
signature_union (SpanDomain cid) = signature_union (morSourceLogic cid)
final_union (SpanDomain cid) = final_union (morSourceLogic cid)
morphism_union (SpanDomain cid) = morphism_union (morSourceLogic cid)
is_subsig (SpanDomain cid) = is_subsig (morSourceLogic cid)
subsig_inclusion (SpanDomain cid) = subsig_inclusion (morSourceLogic cid)
generated_sign (SpanDomain cid) = generated_sign (morSourceLogic cid)
cogenerated_sign (SpanDomain cid) = cogenerated_sign (morSourceLogic cid)
is_transportable (SpanDomain cid) = is_transportable (morSourceLogic cid)
is_injective (SpanDomain cid) = is_injective (morSourceLogic cid)
instance (SemiLatticeWithTop sublogics1, SemiLatticeWithTop sublogics2)
=> SemiLatticeWithTop (SublogicsPair sublogics1 sublogics2) where
top = SublogicsPair top top
join (SublogicsPair x1 y1) (SublogicsPair x2 y2) =
SublogicsPair (join x1 x2) (join y1 y2)
instance (SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2)
=> MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) where
minSublogic (S2 sen2) = SublogicsPair top (minSublogic sen2)
{- just a dummy implementation, it should be the sublogic of sen2 in J
paired with its image through morMapSublogicSen? -}
instance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
=> MinSublogic (SublogicsPair sublogics1 sublogics2) alpha where
minSublogic x = SublogicsPair (minSublogic x) top
{- also should have instances of MinSublogic class for Sublogics-pair
and morphism1, sign_symbol1, sign1 this is why the wrapping is needed -}
-- instance SemiLatticeWithTop sublogics => MinSublogic sublogics () where
instance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
=> ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha where
-- it should be used for (), morphism1, sign_symbol1, sign1
instance (MinSublogic sublogics1 sign1, SemiLatticeWithTop sublogics2)
=> ProjectSublogicM (SublogicsPair sublogics1 sublogics2) sign1 where
projectSublogicM _ = Just
instance (ShATermConvertible a, ShATermConvertible b)
=> ShATermConvertible (SublogicsPair a b) where
toShATermAux att0 (SublogicsPair a b) = do
(att1, a') <- toShATerm' att0 a
(att2, b') <- toShATerm' att1 b
return $ addATerm (ShAAppl "SublogicsPair" [a',b'] []) att2
fromShATermAux ix att0 = case getShATerm ix att0 of
ShAAppl "SublogicsPair" [a,b] _ ->
case fromShATerm' a att0 of { (att1, a') ->
case fromShATerm' b att1 of { (att2, b') ->
(att2, SublogicsPair a' b') }}
u -> fromShATermError "SublogicsPair" u
instance (SublogicName sublogics1, SublogicName sublogics2)
=> SublogicName (SublogicsPair sublogics1 sublogics2) where
sublogicName (SublogicsPair sub1 sub2) =
let s1 = sublogicName sub1
in if null s1 then s2 else if null s2 then s1 else
instance ( MinSublogic sublogics1 ()
lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 sign_symbol1 symbol1 proof_tree1
lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 sign_symbol2 symbol2 proof_tree2
) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) ()
(S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2
stability (SpanDomain _) = Experimental
data_logic (SpanDomain _) = Nothing
top_sublogic (SpanDomain cid) = SublogicsPair
(top_sublogic $ morSourceLogic cid) $ top_sublogic $ morTargetLogic cid
all_sublogics (SpanDomain cid) =
| x <- all_sublogics (morSourceLogic cid)
, y <- all_sublogics (morTargetLogic cid) ]
-- project_sublogic_epsilon - default implementation for now
conservativityCheck _ = []
empty_proof_tree (SpanDomain cid) = empty_proof_tree (morTargetLogic cid)
-- | Existential type for morphisms
data AnyMorphism = forall cid lid1 sublogics1
basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
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 =>
instance Eq AnyMorphism where
Morphism cid1 == Morphism cid2 =
constituents cid1 == constituents cid2
-- need to be refined, using morphism translations !!!
instance Show AnyMorphism where
show (Morphism cid) = language_name cid
++ " : " ++ language_name (morSourceLogic cid)
++ " -> " ++ language_name (morTargetLogic cid)