{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable
, FlexibleInstances, UndecidableInstances, OverlappingInstances
, ExistentialQuantification, GeneralizedNewtypeDeriving #-}
{- |
Module : ./Logic/Morphism.hs
Description : interface (type class) for logic projections (morphisms) in Hets
Copyright : (c) Till Mossakowski, Uni Bremen 2002-2004
License : GPLv2 or higher, see LICENSE.txt
Maintainer : till@informatik.uni-bremen.de
Stability : provisional
Portability : non-portable (via Logic)
Interface (type class) for logic projections (morphisms) in Hets
Provides data structures for institution morphisms.
These are just collections of
functions between (some of) the types of logics.
-}
{- References: see Logic.hs
Todo:
morphism modifications / representation maps
-}
module Logic.Morphism where
import Logic.Logic
import Logic.Comorphism
import Data.Data
import qualified Data.Set as Set
import ATerm.Lib
import Common.DocUtils
import Common.AS_Annotation
import Common.Id
import Common.Json
import Common.ToXml
class (Language cid,
Logic lid1 sublogics1
basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 sign_symbol1 symbol1 proof_tree1,
Logic lid2 sublogics2
basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 sign_symbol2 symbol2 proof_tree2) =>
Morphism 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
| cid -> lid1, cid -> lid2
, 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
where
{- source and target logic and sublogic
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
contravariantly -}
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
-- | identity morphisms
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
[] -> ""
h -> '.' : h
instance Logic lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism sign_symbol symbol proof_tree =>
Morphism (IdMorphism lid sublogics)
lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism sign_symbol symbol proof_tree
lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism sign_symbol symbol proof_tree
where
morSourceLogic (IdMorphism lid _sub) = lid
morTargetLogic (IdMorphism lid _sub) = lid
morSourceSublogic (IdMorphism _lid sub) = sub
morTargetSublogic (IdMorphism _lid sub) = sub
-- changed to identities!
morMapSublogicSign _ x = x
morMapSublogicSen _ x = x
morMap_sign _ = Just
morMap_morphism _ = Just
morMap_sentence _ _ = Just
morMap_sign_symbol _ = Set.singleton
-- composition not needed, use lax triangles instead
-- | comorphisms inducing morphisms
class Comorphism 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 =>
InducingComorphism 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
where
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
this logic will have
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
existing lattices
basic_spec will be () - the unit type, because we mix signatures
with sentences in specifications
sentence - sentences of J, wrapped
symb_items - ()
symb_map_items - ()
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 -}
instance (Morphism 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
, Pretty sign_symbol1)
=> Syntax (SpanDomain cid) () sign_symbol1 () ()
-- default is ok
newtype S2 s = S2 { sentence2 :: s }
deriving (Eq, Ord, Show, Typeable, Data, ShATermConvertible, Pretty
, GetRange, ToJson, ToXml)
instance (Morphism 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
, Category sign1 morphism1, Ord sign_symbol1, GetRange sign_symbol1)
=> Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1
sign_symbol1 where
{- one has to take care about signature and morphisms
and translate them to targetLogic
we get a Maybe sign/morphism -}
map_sen (SpanDomain cid) mor1 (S2 sen) =
case morMap_morphism cid mor1 of
Just mor2 -> fmap S2 $
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
Just sigma2 -> S2 $
simplify_sen (morTargetLogic cid) sigma2 sen
Nothing -> error "simplify_sen"
print_named (SpanDomain cid) = print_named (morTargetLogic cid)
. mapNamed sentence2
sym_of (SpanDomain cid) = sym_of (morSourceLogic cid)
symmap_of (SpanDomain cid) = symmap_of (morSourceLogic cid)
sym_name (SpanDomain cid) = sym_name (morSourceLogic cid)
instance (Morphism 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
, Ord symbol1, GetRange symbol1, Pretty symbol1, Typeable symbol1)
=> 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
lub (SublogicsPair x1 y1) (SublogicsPair x2 y2) =
SublogicsPair (lub x1 x2) (lub 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
minSublogic _ = top -}
instance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
=> ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha where
projectSublogic _ x = x
-- 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
s2 = sublogicName sub2
in if null s1 then s2 else if null s2 then s1 else
s1 ++ "|" ++ s2
instance ( MinSublogic sublogics1 ()
, Morphism 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
, Ord proof_tree2, Show proof_tree2)
=> Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) ()
(S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2
where
stability (SpanDomain _) = Experimental
data_logic (SpanDomain _) = Nothing
top_sublogic (SpanDomain cid) = SublogicsPair
(top_sublogic $ morSourceLogic cid) $ top_sublogic $ morTargetLogic cid
all_sublogics (SpanDomain cid) =
[ SublogicsPair x y
| x <- all_sublogics (morSourceLogic cid)
, y <- all_sublogics (morTargetLogic cid) ]
-- project_sublogic_epsilon - default implementation for now
provers _ = []
cons_checkers _ = []
conservativityCheck _ = []
empty_proof_tree (SpanDomain cid) = empty_proof_tree (morTargetLogic cid)
-- * Morphisms
-- | 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
lid2 sublogics2
basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
Morphism cid
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 =>
Morphism cid
{-
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)