{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Temporal/Morphism.hs
Description :  Morphisms in Temporal logic
Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

  Definition of morphisms for temporal logic
  copied from "Propositional.Morphism"

  Ref.

    Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
    What is a Logic?.
    In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
    2005.
-}

module Temporal.Morphism
  ( Morphism (..)               -- datatype for Morphisms
  , pretty                      -- pretty printing
  , idMor                       -- identity morphism
  , isLegalMorphism             -- check if morhpism is ok
  , 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
  ) where

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

import Temporal.Sign as Sign
import qualified Temporal.AS_BASIC_Temporal as AS_BASIC

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

import Control.Monad (unless)
import qualified Control.Monad.Fail as Fail

{- | The datatype for morphisms in temporal logic as
maps of sets -}
data Morphism = Morphism
  { Morphism -> Sign
source :: Sign
  , Morphism -> Sign
target :: Sign
  , Morphism -> Map Id Id
propMap :: Map.Map Id Id
  } deriving (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, 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, Typeable)

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

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

-- | Determines whether a morphism is valid
isLegalMorphism :: Morphism -> Result ()
isLegalMorphism :: Morphism -> Result ()
isLegalMorphism pmor :: Morphism
pmor =
    let psource :: Set Id
psource = Sign -> Set Id
items (Sign -> Set Id) -> Sign -> Set Id
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
pmor
        ptarget :: Set Id
ptarget = Sign -> Set Id
items (Sign -> Set Id) -> Sign -> Set Id
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
target Morphism
pmor
        pdom :: Set Id
pdom = Map Id Id -> Set Id
forall k a. Map k a -> Set k
Map.keysSet (Map Id Id -> Set Id) -> Map Id Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Morphism -> Map Id Id
propMap Morphism
pmor
        pcodom :: Set Id
pcodom = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Morphism -> Id -> Id
applyMorphism Morphism
pmor) Set Id
psource
    in Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set Id
pcodom Set Id
ptarget Bool -> Bool -> Bool
&& Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set Id
pdom Set Id
psource) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$
        String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "illegal Temporal morphism"

-- | 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
propMap Morphism
mor

-- | Application function for propMaps
applyMap :: Map.Map Id Id -> Id -> Id
applyMap :: Map Id Id -> Id -> Id
applyMap pmap :: Map Id Id
pmap 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
pmap

-- | Composition of morphisms in temporal Logic
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
propMap Morphism
f
      gMap :: Map Id Id
gMap = Morphism -> Map Id Id
propMap 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
  , propMap :: Map Id Id
propMap = 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
items Sign
fSource }

-- | Pretty printing 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
propMap Morphism
m)

-- | Inclusion map of a subsig into a supersig
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
  , propMap :: Map Id Id
propMap = Map Id Id
forall k a. Map k a
Map.empty }

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

mapSentenceH :: Morphism -> AS_BASIC.FORMULA -> AS_BASIC.FORMULA
mapSentenceH :: Morphism -> FORMULA -> FORMULA
mapSentenceH _ AS_BASIC.Formula = FORMULA
AS_BASIC.Formula