{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveDataTypeable

, FlexibleInstances, UndecidableInstances, ExistentialQuantification #-}

{- |

Module : $Header$

Description : interface and class for logic translations

Copyright : (c) Till Mossakowski, Uni Bremen 2002-2006

License : GPLv2 or higher, see LICENSE.txt

Maintainer : till@informatik.uni-bremen.de

Stability : provisional

Portability : non-portable (via Logic)

Central interface (type class) for logic translations (comorphisms) in Hets

These are just collections of

functions between (some of) the types of logics.

References: see Logic.hs

-}

module Logic.Comorphism

( CompComorphism (..)

, InclComorphism

, inclusion_logic

, inclusion_source_sublogic

, inclusion_target_sublogic

, mkInclComorphism

, mkIdComorphism

, Comorphism (..)

, targetSublogic

, map_sign

, wrapMapTheory

, mkTheoryMapping

, AnyComorphism (..)

, idComorphism

, isIdComorphism

, isModelTransportable

, hasModelExpansion

, isWeaklyAmalgamable

, compComorphism

) where

import Logic.Logic

import Logic.Coerce

import Common.AS_Annotation

import Common.Doc

import Common.DocUtils

import Common.Id

import Common.LibName

import Common.ProofUtils

import Common.Result

import Data.Data

import Data.Maybe

import qualified Data.Set as Set

class (Language cid,

Logic lid1 sublogics1

basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

Logic lid2 sublogics2

basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>

Comorphism 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

| 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

where

{- source and target logic and sublogic

the source sublogic is the maximal one for which the comorphism works -}

sourceLogic :: cid -> lid1

sourceSublogic :: cid -> sublogics1

sourceSublogic cid = top_sublogic $ sourceLogic cid

minSourceTheory :: cid -> Maybe (LibName, String)

minSourceTheory _ = Nothing

targetLogic :: cid -> lid2

{- finer information of target sublogics corresponding to source sublogics

this function must be partial because mapTheory is partial -}

mapSublogic :: cid -> sublogics1 -> Maybe sublogics2

mapSublogic cid _ = Just $ top_sublogic $ targetLogic cid

{- the translation functions are partial

because the target may be a sublanguage

map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2

cover theoroidal comorphisms as well -}

map_theory :: cid -> (sign1, [Named sentence1])

-> Result (sign2, [Named sentence2])

-- map_theory but also consider sentence marks

mapMarkedTheory :: cid -> (sign1, [Named sentence1])

-> Result (sign2, [Named sentence2])

mapMarkedTheory cid (sig, sens) = do

(sig2, sens2) <- map_theory cid (sig, map unmark sens)

return (sig2, map (markSen $ language_name cid) sens2)

map_morphism :: cid -> morphism1 -> Result morphism2

map_morphism = mapDefaultMorphism

map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2

{- also covers semi-comorphisms

with no sentence translation

- but these are spans! -}

map_sentence = failMapSentence

map_symbol :: cid -> sign1 -> symbol1 -> Set.Set symbol2

map_symbol = errMapSymbol

extractModel :: cid -> sign1 -> proof_tree2

-> Result (sign1, [Named sentence1])

extractModel cid _ _ = fail

$ "extractModel not implemented for comorphism "

++ language_name cid

-- properties of comorphisms

is_model_transportable :: cid -> Bool

{- a comorphism (\phi, \alpha, \beta) is model-transportable

if for any signature \Sigma,

any \Sigma-model M and any \phi(\Sigma)-model N

for any isomorphism h : \beta_\Sigma(N) -> M

there exists an isomorphism h': N -> M' such that \beta_\Sigma(h') = h -}

is_model_transportable _ = False

has_model_expansion :: cid -> Bool

has_model_expansion _ = False

is_weakly_amalgamable :: cid -> Bool

is_weakly_amalgamable _ = False

constituents :: cid -> [String]

constituents cid = [language_name cid]

isInclusionComorphism :: cid -> Bool

isInclusionComorphism _ = False

targetSublogic :: Comorphism 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

=> cid -> sublogics2

targetSublogic cid = fromMaybe (top_sublogic $ targetLogic cid)

$ mapSublogic cid $ sourceSublogic cid

-- | this function is based on 'map_theory' using no sentences as input

map_sign :: Comorphism 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

=> cid -> sign1 -> Result (sign2, [Named sentence2])

map_sign cid sign = wrapMapTheory cid (sign, [])

mapDefaultMorphism :: Comorphism 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

=> cid -> morphism1 -> Result morphism2

mapDefaultMorphism cid mor = do

(sig1, _) <- map_sign cid $ dom mor

(sig2, _) <- map_sign cid $ cod mor

inclusion (targetLogic cid) sig1 sig2

failMapSentence :: Comorphism 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

=> cid -> sign1 -> sentence1 -> Result sentence2

failMapSentence cid _ _ =

fail $ "Unsupported sentence translation " ++ show cid

errMapSymbol :: Comorphism 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

=> cid -> sign1 -> symbol1 -> Set.Set symbol2

errMapSymbol cid _ _ = error $ "no symbol mapping for " ++ show cid

-- | use this function instead of 'mapMarkedTheory'

wrapMapTheory :: Comorphism 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

=> cid -> (sign1, [Named sentence1])

-> Result (sign2, [Named sentence2])

wrapMapTheory cid (sign, sens) =

let res = mapMarkedTheory cid (sign, sens)

lid1 = sourceLogic cid

thDoc = show (vcat $ pretty sign : map (print_named lid1) sens)

in

if isIdComorphism $ Comorphism cid then res else case sourceSublogic cid of

sub -> case minSublogic sign of

sigLog -> case foldl lub sigLog

$ map (minSublogic . sentence) sens of

senLog ->

if isSubElem senLog sub

then res

else Result

[ Diag Hint thDoc nullRange

, Diag Error

("for '" ++ language_name cid ++

"' expected sublogic '" ++

sublogicName sub ++

"'\n but found sublogic '" ++

sublogicName senLog ++

"' with signature sublogic '" ++

sublogicName sigLog ++ "'") nullRange] Nothing

mkTheoryMapping :: Monad m => (sign1 -> m (sign2, [Named sentence2]))

-> (sign1 -> sentence1 -> m sentence2)

-> (sign1, [Named sentence1])

-> m (sign2, [Named sentence2])

mkTheoryMapping mapSig mapSen (sign, sens) = do

(sign', sens') <- mapSig sign

sens'' <- mapM (mapNamedM (mapSen sign) . unmark) sens

return (sign', nameAndDisambiguate

$ map (markSen "SignatureProperty") sens' ++ sens'')

data InclComorphism lid sublogics = InclComorphism

{ inclusion_logic :: lid

, inclusion_source_sublogic :: sublogics

, inclusion_target_sublogic :: sublogics }

deriving (Show, Typeable, Data)

-- | construction of an identity comorphism

mkIdComorphism :: (Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree) =>

lid -> sublogics -> InclComorphism lid sublogics

mkIdComorphism lid sub = InclComorphism

{ inclusion_logic = lid

, inclusion_source_sublogic = sub

, inclusion_target_sublogic = sub }

-- | construction of an inclusion comorphism

mkInclComorphism :: (Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree,

Monad m) =>

lid -> sublogics -> sublogics

-> m (InclComorphism lid sublogics)

mkInclComorphism lid srcSub trgSub =

if isSubElem srcSub trgSub

then return InclComorphism

{ inclusion_logic = lid

, inclusion_source_sublogic = srcSub

, inclusion_target_sublogic = trgSub }

else fail ("mkInclComorphism: first sublogic must be a " ++

"subElem of the second sublogic")

instance (Language lid, Eq sublogics, Show sublogics, SublogicName sublogics)

=> Language (InclComorphism lid sublogics) where

language_name (InclComorphism lid sub_src sub_trg) =

let sblName = sublogicName sub_src

lname = language_name lid

in if sub_src == sub_trg

then "id_" ++ lname ++

if null sblName then "" else '.' : sblName

else "incl_" ++ lname ++ ':'

: sblName ++ "->" ++ sublogicName sub_trg

instance Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

Comorphism (InclComorphism lid sublogics)

lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

where

sourceLogic = inclusion_logic

targetLogic = inclusion_logic

sourceSublogic = inclusion_source_sublogic

mapSublogic cid subl =

if isSubElem subl $ inclusion_source_sublogic cid

then Just subl

else Nothing

map_theory _ = return

map_morphism _ = return

map_sentence _ _ = return

map_symbol _ _ = Set.singleton

constituents cid =

if inclusion_source_sublogic cid

== inclusion_target_sublogic cid

then []

else [language_name cid]

is_model_transportable _ = True

has_model_expansion _ = True

is_weakly_amalgamable _ = True

isInclusionComorphism _ = True

data CompComorphism cid1 cid2 = CompComorphism cid1 cid2

deriving (Show, Typeable, Data)

instance (Language cid1, Language cid2)

=> Language (CompComorphism cid1 cid2) where

language_name (CompComorphism cid1 cid2) =

language_name cid1 ++ ";" ++ language_name cid2

instance (Comorphism cid1

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,

Comorphism cid2

lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4

sign4 morphism4 symbol4 raw_symbol4 proof_tree4

lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

sign3 morphism3 symbol3 raw_symbol3 proof_tree3)

=> Comorphism (CompComorphism cid1 cid2)

lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where

sourceLogic (CompComorphism cid1 _) =

sourceLogic cid1

targetLogic (CompComorphism _ cid2) =

targetLogic cid2

sourceSublogic (CompComorphism cid1 _) =

sourceSublogic cid1

mapSublogic (CompComorphism cid1 cid2) sl =

mapSublogic cid1 sl >>=

mapSublogic cid2 .

forceCoerceSublogic (targetLogic cid1) (sourceLogic cid2)

map_sentence (CompComorphism cid1 cid2) si1 se1 =

do (si2, _) <- map_sign cid1 si1

se2 <- map_sentence cid1 si1 se1

(si2', se2') <- coerceBasicTheory

(targetLogic cid1) (sourceLogic cid2)

"Mapping sentence along comorphism" (si2, [makeNamed "" se2])

case se2' of

[x] -> map_sentence cid2 si2' $ sentence x

_ -> error "CompComorphism.map_sentence"

map_theory (CompComorphism cid1 cid2) ti1 =

do ti2 <- map_theory cid1 ti1

ti2' <- coerceBasicTheory (targetLogic cid1) (sourceLogic cid2)

"Mapping theory along comorphism" ti2

wrapMapTheory cid2 ti2'

map_morphism (CompComorphism cid1 cid2) m1 =

do m2 <- map_morphism cid1 m1

m3 <- coerceMorphism (targetLogic cid1) (sourceLogic cid2)

"Mapping signature morphism along comorphism" m2

map_morphism cid2 m3

map_symbol (CompComorphism cid1 cid2) sig1 = let

th = map_sign cid1 sig1 in

case maybeResult th of

Nothing -> error "failed translating signature"

Just (sig2', _) -> let

th2 = coerceBasicTheory

(targetLogic cid1) (sourceLogic cid2)

"Mapping symbol along comorphism" (sig2', [])

in case maybeResult th2 of

Nothing -> error "failed coercing"

Just (sig2, _) ->

\ s1 ->

let mycast = coerceSymbol (targetLogic cid1) (sourceLogic cid2)

in Set.unions

(map (map_symbol cid2 sig2 . mycast)

(Set.toList (map_symbol cid1 sig1 s1)))

extractModel (CompComorphism cid1 cid2) sign pt3 =

let lid1 = sourceLogic cid1

lid3 = sourceLogic cid2

in if language_name lid1 == language_name lid3 then do

bTh1 <- map_sign cid1 sign

(sign1, _) <-

coerceBasicTheory (targetLogic cid1) lid3 "extractModel1" bTh1

bTh2 <- extractModel cid2 sign1 pt3

coerceBasicTheory lid3 lid1 "extractModel2" bTh2

else fail $ "extractModel not implemented for comorphism composition with "

++ language_name cid1

constituents (CompComorphism cid1 cid2) =

constituents cid1 ++ constituents cid2

is_model_transportable (CompComorphism cid1 cid2) =

is_model_transportable cid1 && is_model_transportable cid2

has_model_expansion (CompComorphism cid1 cid2) =

has_model_expansion cid1 && has_model_expansion cid2

is_weakly_amalgamable (CompComorphism cid1 cid2) =

is_weakly_amalgamable cid1 && is_weakly_amalgamable cid2

isInclusionComorphism (CompComorphism cid1 cid2) =

isInclusionComorphism cid1 && isInclusionComorphism cid2

-- * Comorphisms and existential types for the logic graph

-- | Existential type for comorphisms

data AnyComorphism = 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 .

Comorphism 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 =>

Comorphism cid deriving Typeable -- used for GTheory

instance Eq AnyComorphism where

a == b = compare a b == EQ

instance Ord AnyComorphism where

compare (Comorphism cid1) (Comorphism cid2) = compare

(language_name cid1, constituents cid1)

(language_name cid2, constituents cid2)

-- maybe needs to be refined, using comorphism translations?

instance Show AnyComorphism where

show (Comorphism cid) = language_name cid

++ " : " ++ language_name (sourceLogic cid)

++ " -> " ++ language_name (targetLogic cid)

instance Pretty AnyComorphism where

pretty = text . show

-- | compute the identity comorphism for a logic

idComorphism :: AnyLogic -> AnyComorphism

idComorphism (Logic lid) = Comorphism (mkIdComorphism lid (top_sublogic lid))

-- | Test whether a comporphism is the identity

isIdComorphism :: AnyComorphism -> Bool

isIdComorphism (Comorphism cid) = null $ constituents cid

-- * Properties of comorphisms

-- | Test whether a comorphism is model-transportable

isModelTransportable :: AnyComorphism -> Bool

isModelTransportable (Comorphism cid) = is_model_transportable cid

-- | Test whether a comorphism has model expansion

hasModelExpansion :: AnyComorphism -> Bool

hasModelExpansion (Comorphism cid) = has_model_expansion cid

-- | Test whether a comorphism is weakly amalgamable

isWeaklyAmalgamable :: AnyComorphism -> Bool

isWeaklyAmalgamable (Comorphism cid) = is_weakly_amalgamable cid

-- | Compose comorphisms

compComorphism :: Monad m => AnyComorphism -> AnyComorphism -> m AnyComorphism

compComorphism (Comorphism cid1) (Comorphism cid2) =

let l1 = targetLogic cid1

l2 = sourceLogic cid2

msg = "ogic mismatch in composition of " ++ language_name cid1

++ " and " ++ language_name cid2

in

if language_name l1 == language_name l2 then

if isSubElem (forceCoerceSublogic l1 l2 $ targetSublogic cid1)

$ sourceSublogic cid2

then return $ Comorphism (CompComorphism cid1 cid2)

else fail $ "Subl" ++ msg ++ " (Expected sublogic "

++ sublogicName (sourceSublogic cid2)

++ " but found sublogic "

++ sublogicName (targetSublogic cid1) ++ ")"

else fail $ 'L' : msg ++ " (Expected logic "

++ language_name l2

++ " but found logic "

++ language_name l1 ++ ")"