{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./CSL/Morphism.hs
Description :  Abstract syntax for reduce
Copyright   :  (c) Dominik Dietrich, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  dominik.dietrich@dfki.de
Stability   :  experimental
Portability :  portable

this file defines morhpisms for the reduce logic. A morphism is a mapping of operator symbols
-}


module CSL.Morphism
  ( Morphism (..)               -- datatype for Morphisms
  , pretty                      -- pretty printing
  , idMor                       -- identity morphism
  , composeMor                  -- composition
  , inclusionMap                -- inclusion map
  , mapSentence                 -- map of sentences
  , mapSentenceH                -- map of sentences, without Result type
  , applyMap                    -- application function for maps
  , applyMorphism               -- application function for morphism
  , morphismUnion
  ) where

import Data.Data
import qualified Data.Map as Map
import qualified Data.Set as Set

import CSL.Sign as Sign
import CSL.AS_BASIC_CSL

import Common.Id as Id
import Common.Result
import Common.Doc
import Common.DocUtils
import qualified Common.Result as Result

-- | The datatype for morphisms in reduce logic as maps of sets
data Morphism = Morphism
  { Morphism -> Sign
source :: Sign
  , Morphism -> Sign
target :: Sign
  , Morphism -> Map Id Id
operatorMap :: Map.Map Id Id
  } deriving (Int -> Morphism -> ShowS
[Morphism] -> ShowS
Morphism -> String
(Int -> Morphism -> ShowS)
-> (Morphism -> String) -> ([Morphism] -> ShowS) -> Show Morphism
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Morphism] -> ShowS
$cshowList :: [Morphism] -> ShowS
show :: Morphism -> String
$cshow :: Morphism -> String
showsPrec :: Int -> Morphism -> ShowS
$cshowsPrec :: Int -> Morphism -> ShowS
Show, Morphism -> Morphism -> Bool
(Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool) -> Eq Morphism
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Morphism -> Morphism -> Bool
$c/= :: Morphism -> Morphism -> Bool
== :: Morphism -> Morphism -> Bool
$c== :: Morphism -> Morphism -> Bool
Eq, Eq Morphism
Eq Morphism =>
(Morphism -> Morphism -> Ordering)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Morphism)
-> (Morphism -> Morphism -> Morphism)
-> Ord Morphism
Morphism -> Morphism -> Bool
Morphism -> Morphism -> Ordering
Morphism -> Morphism -> Morphism
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Morphism -> Morphism -> Morphism
$cmin :: Morphism -> Morphism -> Morphism
max :: Morphism -> Morphism -> Morphism
$cmax :: Morphism -> Morphism -> Morphism
>= :: Morphism -> Morphism -> Bool
$c>= :: Morphism -> Morphism -> Bool
> :: Morphism -> Morphism -> Bool
$c> :: Morphism -> Morphism -> Bool
<= :: Morphism -> Morphism -> Bool
$c<= :: Morphism -> Morphism -> Bool
< :: Morphism -> Morphism -> Bool
$c< :: Morphism -> Morphism -> Bool
compare :: Morphism -> Morphism -> Ordering
$ccompare :: Morphism -> Morphism -> Ordering
$cp1Ord :: Eq Morphism
Ord, Typeable, Typeable Morphism
Constr
DataType
Typeable Morphism =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Morphism -> c Morphism)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Morphism)
-> (Morphism -> Constr)
-> (Morphism -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Morphism))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism))
-> ((forall b. Data b => b -> b) -> Morphism -> Morphism)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Morphism -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Morphism -> r)
-> (forall u. (forall d. Data d => d -> u) -> Morphism -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Morphism -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Morphism -> m Morphism)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Morphism -> m Morphism)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Morphism -> m Morphism)
-> Data Morphism
Morphism -> Constr
Morphism -> DataType
(forall b. Data b => b -> b) -> Morphism -> Morphism
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Morphism -> c Morphism
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Morphism
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Morphism -> u
forall u. (forall d. Data d => d -> u) -> Morphism -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Morphism -> m Morphism
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Morphism -> m Morphism
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Morphism
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Morphism -> c Morphism
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Morphism)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism)
$cMorphism :: Constr
$tMorphism :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Morphism -> m Morphism
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Morphism -> m Morphism
gmapMp :: (forall d. Data d => d -> m d) -> Morphism -> m Morphism
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Morphism -> m Morphism
gmapM :: (forall d. Data d => d -> m d) -> Morphism -> m Morphism
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Morphism -> m Morphism
gmapQi :: Int -> (forall d. Data d => d -> u) -> Morphism -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Morphism -> u
gmapQ :: (forall d. Data d => d -> u) -> Morphism -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Morphism -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism -> r
gmapT :: (forall b. Data b => b -> b) -> Morphism -> Morphism
$cgmapT :: (forall b. Data b => b -> b) -> Morphism -> Morphism
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Morphism)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Morphism)
dataTypeOf :: Morphism -> DataType
$cdataTypeOf :: Morphism -> DataType
toConstr :: Morphism -> Constr
$ctoConstr :: Morphism -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Morphism
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Morphism
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Morphism -> c Morphism
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Morphism -> c Morphism
$cp1Data :: Typeable Morphism
Data)

instance Pretty Morphism where
    pretty :: Morphism -> Doc
pretty = Morphism -> Doc
printMorphism

-- | pretty printer for morphisms
printMorphism :: Morphism -> Doc
printMorphism :: Morphism -> Doc
printMorphism m :: Morphism
m = Sign -> Doc
forall a. Pretty a => a -> Doc
pretty (Morphism -> Sign
source Morphism
m) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text "-->" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Sign -> Doc
forall a. Pretty a => a -> Doc
pretty (Morphism -> Sign
target Morphism
m)
  Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
vcat (((Id, Id) -> Doc) -> [(Id, Id)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (x :: Id
x, y :: Id
y) -> Doc
lparen Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
x Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text ","
  Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
y Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
rparen) ([(Id, Id)] -> [Doc]) -> [(Id, Id)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Map Id Id -> [(Id, Id)]
forall k a. Map k a -> [(k, a)]
Map.assocs (Map Id Id -> [(Id, Id)]) -> Map Id Id -> [(Id, Id)]
forall a b. (a -> b) -> a -> b
$ Morphism -> Map Id Id
operatorMap Morphism
m)


-- | Constructs an id-morphism
idMor :: Sign -> Morphism
idMor :: Sign -> Morphism
idMor a :: Sign
a = Sign -> Sign -> Morphism
inclusionMap Sign
a Sign
a

-- | calculates the composition of two morhpisms f:X->Y, g:Y->Z
composeMor :: Morphism -> Morphism -> Result Morphism
composeMor :: Morphism -> Morphism -> Result Morphism
composeMor f :: Morphism
f g :: Morphism
g =
  let fSource :: Sign
fSource = Morphism -> Sign
source Morphism
f
      gTarget :: Sign
gTarget = Morphism -> Sign
target Morphism
g
      fMap :: Map Id Id
fMap = Morphism -> Map Id Id
operatorMap Morphism
f
      gMap :: Map Id Id
gMap = Morphism -> Map Id Id
operatorMap Morphism
g
  in Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism :: Sign -> Sign -> Map Id Id -> Morphism
Morphism
  { source :: Sign
source = Sign
fSource
  , target :: Sign
target = Sign
gTarget
  , operatorMap :: Map Id Id
operatorMap = if Map Id Id -> Bool
forall k a. Map k a -> Bool
Map.null Map Id Id
gMap then Map Id Id
fMap else
      (Id -> Map Id Id -> Map Id Id) -> Map Id Id -> Set Id -> Map Id Id
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ( \ i :: Id
i -> let j :: Id
j = Map Id Id -> Id -> Id
applyMap Map Id Id
gMap (Map Id Id -> Id -> Id
applyMap Map Id Id
fMap Id
i) in
                        if Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
j then Map Id Id -> Map Id Id
forall a. a -> a
id else Id -> Id -> Map Id Id -> Map Id Id
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i Id
j)
                                  Map Id Id
forall k a. Map k a
Map.empty (Set Id -> Map Id Id) -> Set Id -> Map Id Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
opIds Sign
fSource }

-- | constructs the inclusion map for a given signature
inclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
inclusionMap :: Sign -> Sign -> Morphism
inclusionMap s1 :: Sign
s1 s2 :: Sign
s2 = Morphism :: Sign -> Sign -> Map Id Id -> Morphism
Morphism
  { source :: Sign
source = Sign
s1
  , target :: Sign
target = Sign
s2
  , operatorMap :: Map Id Id
operatorMap = Map Id Id
forall k a. Map k a
Map.empty }


-- | Application function for propMaps
applyMap :: Map.Map Id Id -> Id -> Id
applyMap :: Map Id Id -> Id -> Id
applyMap operatormap :: Map Id Id
operatormap idt :: Id
idt = Id -> Id -> Map Id Id -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
idt Id
idt Map Id Id
operatormap


-- | Application funtion for morphisms
applyMorphism :: Morphism -> Id -> Id
applyMorphism :: Morphism -> Id -> Id
applyMorphism mor :: Morphism
mor idt :: Id
idt = Id -> Id -> Map Id Id -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
idt Id
idt (Map Id Id -> Id) -> Map Id Id -> Id
forall a b. (a -> b) -> a -> b
$ Morphism -> Map Id Id
operatorMap Morphism
mor


{- | sentence translation along signature morphism
here just the renaming of formulae -}
mapSentence :: Morphism -> CMD -> Result.Result CMD
mapSentence :: Morphism -> CMD -> Result CMD
mapSentence mor :: Morphism
mor = CMD -> Result CMD
forall (m :: * -> *) a. Monad m => a -> m a
return (CMD -> Result CMD) -> (CMD -> CMD) -> CMD -> Result CMD
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> CMD -> CMD
mapSentenceH Morphism
mor

mapSentenceH :: Morphism -> CMD -> CMD
mapSentenceH :: Morphism -> CMD -> CMD
mapSentenceH _ frm :: CMD
frm = CMD
frm

morphismUnion :: Morphism -> Morphism -> Result.Result Morphism
morphismUnion :: Morphism -> Morphism -> Result Morphism
morphismUnion mor1 :: Morphism
mor1 mor2 :: Morphism
mor2 =
  let pmap1 :: Map Id Id
pmap1 = Morphism -> Map Id Id
operatorMap Morphism
mor1
      pmap2 :: Map Id Id
pmap2 = Morphism -> Map Id Id
operatorMap Morphism
mor2
      p1 :: Sign
p1 = Morphism -> Sign
source Morphism
mor1
      p2 :: Sign
p2 = Morphism -> Sign
source Morphism
mor2
      up1 :: Set Id
up1 = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set Id
opIds Sign
p1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Map Id Id -> Set Id
forall k a. Map k a -> Set k
Map.keysSet Map Id Id
pmap1
      up2 :: Set Id
up2 = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set Id
opIds Sign
p2) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Map Id Id -> Set Id
forall k a. Map k a -> Set k
Map.keysSet Map Id Id
pmap2
      (pds :: [Diagnosis]
pds, pmap :: Map Id Id
pmap) = ((Id, Id) -> ([Diagnosis], Map Id Id) -> ([Diagnosis], Map Id Id))
-> ([Diagnosis], Map Id Id)
-> [(Id, Id)]
-> ([Diagnosis], Map Id Id)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ (i :: Id
i, j :: Id
j) (ds :: [Diagnosis]
ds, m :: Map Id Id
m) -> case Id -> Map Id Id -> Maybe Id
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i Map Id Id
m of
          Nothing -> ([Diagnosis]
ds, Id -> Id -> Map Id Id -> Map Id Id
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i Id
j Map Id Id
m)
          Just k :: Id
k -> if Id
j Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
k then ([Diagnosis]
ds, Map Id Id
m) else
              (DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error
               ("incompatible mapping of prop " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
i " to "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
j " and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
k "")
               Range
nullRange Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
ds, Map Id Id
m)) ([], Map Id Id
pmap1)
          (Map Id Id -> [(Id, Id)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Id Id
pmap2 [(Id, Id)] -> [(Id, Id)] -> [(Id, Id)]
forall a. [a] -> [a] -> [a]
++ (Id -> (Id, Id)) -> [Id] -> [(Id, Id)]
forall a b. (a -> b) -> [a] -> [b]
map (\ a :: Id
a -> (Id
a, Id
a))
                      (Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Set Id -> [Id]) -> Set Id -> [Id]
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Id
up1 Set Id
up2))
   in if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
pds then Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism :: Sign -> Sign -> Map Id Id -> Morphism
Morphism
      { source :: Sign
source = Sign -> Sign -> Sign
unite Sign
p1 Sign
p2
      , target :: Sign
target = Sign -> Sign -> Sign
unite (Morphism -> Sign
target Morphism
mor1) (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
target Morphism
mor2
      , operatorMap :: Map Id Id
operatorMap = Map Id Id
pmap } else [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
pds Maybe Morphism
forall a. Maybe a
Nothing