{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./CommonLogic/Morphism.hs
Description :  Morphism of Common Logic
Copyright   :  (c) Uni Bremen DFKI 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  eugenk@informatik.uni-bremen.de
Stability   :  experimental
Portability :  non-portable (via Logic.Logic)

Morphism of Common Logic

-}

module CommonLogic.Morphism
  ( Morphism (..)
  , pretty                      -- pretty printing
  , idMor                       -- identity morphism
  , isLegalMorphism             -- check if morhpism is ok
  , composeMor                  -- composition
  , inclusionMap                -- inclusion map
  , mkMorphism                  -- create Morphism
  , mapSentence                 -- map of sentences
  , applyMap                    -- application function for maps
  , applyMorphism               -- application function for morphism
  , morphismUnion
  ) where

import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Common.Result as Result
import Common.Id as Id
import Common.Result
import Common.Doc
import Common.DocUtils

import CommonLogic.AS_CommonLogic as AS
import CommonLogic.Sign as Sign

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

import Data.Data

-- 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
allItems (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
allItems (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 CommonLogic 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 propositional 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
allItems 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 }

-- | creates a Morphism
mkMorphism :: Sign.Sign -> Sign.Sign -> Map.Map Id Id -> Morphism
mkMorphism :: Sign -> Sign -> Map Id Id -> Morphism
mkMorphism s :: Sign
s t :: Sign
t p :: Map Id Id
p =
  Morphism :: Sign -> Sign -> Map Id Id -> Morphism
Morphism { source :: Sign
source = Sign
s
           , target :: Sign
target = Sign
t
           , propMap :: Map Id Id
propMap = Map Id Id
p }

{- | sentence (text) translation along signature morphism
here just the renaming of formulae -}
mapSentence :: Morphism -> AS.TEXT_META -> Result.Result AS.TEXT_META
mapSentence :: Morphism -> TEXT_META -> Result TEXT_META
mapSentence mor :: Morphism
mor tm :: TEXT_META
tm =
  TEXT_META -> Result TEXT_META
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT_META -> Result TEXT_META) -> TEXT_META -> Result TEXT_META
forall a b. (a -> b) -> a -> b
$ TEXT_META
tm { getText :: TEXT
getText = Morphism -> TEXT -> TEXT
mapSen_txt Morphism
mor (TEXT -> TEXT) -> TEXT -> TEXT
forall a b. (a -> b) -> a -> b
$ TEXT_META -> TEXT
getText TEXT_META
tm }

-- propagates the translation to sentences
mapSen_txt :: Morphism -> AS.TEXT -> AS.TEXT
mapSen_txt :: Morphism -> TEXT -> TEXT
mapSen_txt mor :: Morphism
mor txt :: TEXT
txt = case TEXT
txt of
  AS.Text phrs :: [PHRASE]
phrs r :: Range
r -> [PHRASE] -> Range -> TEXT
AS.Text ((PHRASE -> PHRASE) -> [PHRASE] -> [PHRASE]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism -> PHRASE -> PHRASE
mapSen_phr Morphism
mor) [PHRASE]
phrs) Range
r
  AS.Named_text n :: NAME
n t :: TEXT
t r :: Range
r -> NAME -> TEXT -> Range -> TEXT
AS.Named_text NAME
n (Morphism -> TEXT -> TEXT
mapSen_txt Morphism
mor TEXT
t) Range
r

-- propagates the translation to sentences
mapSen_phr :: Morphism -> AS.PHRASE -> AS.PHRASE
mapSen_phr :: Morphism -> PHRASE -> PHRASE
mapSen_phr mor :: Morphism
mor phr :: PHRASE
phr = case PHRASE
phr of
  AS.Module m :: MODULE
m -> MODULE -> PHRASE
AS.Module (MODULE -> PHRASE) -> MODULE -> PHRASE
forall a b. (a -> b) -> a -> b
$ Morphism -> MODULE -> MODULE
mapSen_mod Morphism
mor MODULE
m
  AS.Sentence s :: SENTENCE
s -> SENTENCE -> PHRASE
AS.Sentence (SENTENCE -> PHRASE) -> SENTENCE -> PHRASE
forall a b. (a -> b) -> a -> b
$ Morphism -> SENTENCE -> SENTENCE
mapSen_sen Morphism
mor SENTENCE
s
  AS.Comment_text c :: COMMENT
c t :: TEXT
t r :: Range
r -> COMMENT -> TEXT -> Range -> PHRASE
AS.Comment_text COMMENT
c (Morphism -> TEXT -> TEXT
mapSen_txt Morphism
mor TEXT
t) Range
r
  x :: PHRASE
x -> PHRASE
x

-- propagates the translation to sentences
mapSen_mod :: Morphism -> AS.MODULE -> AS.MODULE
mapSen_mod :: Morphism -> MODULE -> MODULE
mapSen_mod mor :: Morphism
mor m :: MODULE
m = case MODULE
m of
  AS.Mod n :: NAME
n t :: TEXT
t rn :: Range
rn -> NAME -> TEXT -> Range -> MODULE
AS.Mod NAME
n (Morphism -> TEXT -> TEXT
mapSen_txt Morphism
mor TEXT
t) Range
rn
  AS.Mod_ex n :: NAME
n exs :: [NAME]
exs t :: TEXT
t rn :: Range
rn -> NAME -> [NAME] -> TEXT -> Range -> MODULE
AS.Mod_ex NAME
n [NAME]
exs (Morphism -> TEXT -> TEXT
mapSen_txt Morphism
mor TEXT
t) Range
rn

mapSen_sen :: Morphism -> AS.SENTENCE -> AS.SENTENCE
mapSen_sen :: Morphism -> SENTENCE -> SENTENCE
mapSen_sen mor :: Morphism
mor frm :: SENTENCE
frm = case SENTENCE
frm of
  AS.Quant_sent q :: QUANT
q vs :: [NAME_OR_SEQMARK]
vs is :: SENTENCE
is rn :: Range
rn ->
    QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
AS.Quant_sent QUANT
q ((NAME_OR_SEQMARK -> NAME_OR_SEQMARK)
-> [NAME_OR_SEQMARK] -> [NAME_OR_SEQMARK]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism -> NAME_OR_SEQMARK -> NAME_OR_SEQMARK
mapSen_nos Morphism
mor) [NAME_OR_SEQMARK]
vs) (Morphism -> SENTENCE -> SENTENCE
mapSen_sen Morphism
mor SENTENCE
is) Range
rn
  AS.Bool_sent bs :: BOOL_SENT
bs rn :: Range
rn -> BOOL_SENT -> Range -> SENTENCE
AS.Bool_sent (case BOOL_SENT
bs of
      AS.Junction j :: AndOr
j sens :: [SENTENCE]
sens -> AndOr -> [SENTENCE] -> BOOL_SENT
AS.Junction AndOr
j ((SENTENCE -> SENTENCE) -> [SENTENCE] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism -> SENTENCE -> SENTENCE
mapSen_sen Morphism
mor) [SENTENCE]
sens)
      AS.Negation sen :: SENTENCE
sen -> SENTENCE -> BOOL_SENT
AS.Negation (Morphism -> SENTENCE -> SENTENCE
mapSen_sen Morphism
mor SENTENCE
sen)
      AS.BinOp op :: ImplEq
op s1 :: SENTENCE
s1 s2 :: SENTENCE
s2 ->
          ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
AS.BinOp ImplEq
op (Morphism -> SENTENCE -> SENTENCE
mapSen_sen Morphism
mor SENTENCE
s1) (Morphism -> SENTENCE -> SENTENCE
mapSen_sen Morphism
mor SENTENCE
s2)
    ) Range
rn
  AS.Atom_sent atom :: ATOM
atom rn :: Range
rn -> ATOM -> Range -> SENTENCE
AS.Atom_sent (case ATOM
atom of
      AS.Equation t1 :: TERM
t1 t2 :: TERM
t2 -> TERM -> TERM -> ATOM
AS.Equation (Morphism -> TERM -> TERM
mapSen_trm Morphism
mor TERM
t1) (Morphism -> TERM -> TERM
mapSen_trm Morphism
mor TERM
t2)
      AS.Atom t :: TERM
t tss :: [TERM_SEQ]
tss -> TERM -> [TERM_SEQ] -> ATOM
AS.Atom (Morphism -> TERM -> TERM
mapSen_trm Morphism
mor TERM
t) ((TERM_SEQ -> TERM_SEQ) -> [TERM_SEQ] -> [TERM_SEQ]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism -> TERM_SEQ -> TERM_SEQ
mapSen_trmSeq Morphism
mor) [TERM_SEQ]
tss)
    ) Range
rn
  AS.Comment_sent cm :: COMMENT
cm sen :: SENTENCE
sen rn :: Range
rn -> COMMENT -> SENTENCE -> Range -> SENTENCE
AS.Comment_sent COMMENT
cm (Morphism -> SENTENCE -> SENTENCE
mapSen_sen Morphism
mor SENTENCE
sen) Range
rn
  AS.Irregular_sent sen :: SENTENCE
sen rn :: Range
rn -> SENTENCE -> Range -> SENTENCE
AS.Irregular_sent (Morphism -> SENTENCE -> SENTENCE
mapSen_sen Morphism
mor SENTENCE
sen) Range
rn

mapSen_trm :: Morphism -> AS.TERM -> AS.TERM
mapSen_trm :: Morphism -> TERM -> TERM
mapSen_trm mor :: Morphism
mor trm :: TERM
trm = case TERM
trm of
  AS.Name_term n :: NAME
n -> NAME -> TERM
AS.Name_term (Morphism -> NAME -> NAME
mapSen_tok Morphism
mor NAME
n)
  AS.Funct_term t :: TERM
t ts :: [TERM_SEQ]
ts rn :: Range
rn ->
      TERM -> [TERM_SEQ] -> Range -> TERM
AS.Funct_term (Morphism -> TERM -> TERM
mapSen_trm Morphism
mor TERM
t) ((TERM_SEQ -> TERM_SEQ) -> [TERM_SEQ] -> [TERM_SEQ]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism -> TERM_SEQ -> TERM_SEQ
mapSen_trmSeq Morphism
mor) [TERM_SEQ]
ts) Range
rn
  AS.Comment_term t :: TERM
t c :: COMMENT
c rn :: Range
rn -> TERM -> COMMENT -> Range -> TERM
AS.Comment_term (Morphism -> TERM -> TERM
mapSen_trm Morphism
mor TERM
t) COMMENT
c Range
rn
  AS.That_term s :: SENTENCE
s rn :: Range
rn -> SENTENCE -> Range -> TERM
AS.That_term (Morphism -> SENTENCE -> SENTENCE
mapSen_sen Morphism
mor SENTENCE
s) Range
rn

mapSen_nos :: Morphism -> AS.NAME_OR_SEQMARK -> AS.NAME_OR_SEQMARK
mapSen_nos :: Morphism -> NAME_OR_SEQMARK -> NAME_OR_SEQMARK
mapSen_nos mor :: Morphism
mor nos :: NAME_OR_SEQMARK
nos = case NAME_OR_SEQMARK
nos of
  AS.Name n :: NAME
n -> NAME -> NAME_OR_SEQMARK
AS.Name (Morphism -> NAME -> NAME
mapSen_tok Morphism
mor NAME
n)
  AS.SeqMark s :: NAME
s -> NAME -> NAME_OR_SEQMARK
AS.SeqMark (Morphism -> NAME -> NAME
mapSen_tok Morphism
mor NAME
s)

mapSen_trmSeq :: Morphism -> AS.TERM_SEQ -> AS.TERM_SEQ
mapSen_trmSeq :: Morphism -> TERM_SEQ -> TERM_SEQ
mapSen_trmSeq mor :: Morphism
mor ts :: TERM_SEQ
ts = case TERM_SEQ
ts of
  AS.Term_seq t :: TERM
t -> TERM -> TERM_SEQ
AS.Term_seq (Morphism -> TERM -> TERM
mapSen_trm Morphism
mor TERM
t)
  AS.Seq_marks s :: NAME
s -> NAME -> TERM_SEQ
AS.Seq_marks (Morphism -> NAME -> NAME
mapSen_tok Morphism
mor NAME
s)

mapSen_tok :: Morphism -> Id.Token -> Id.Token
mapSen_tok :: Morphism -> NAME -> NAME
mapSen_tok mor :: Morphism
mor tok :: NAME
tok = Id -> NAME
Id.idToSimpleId (Id -> NAME) -> Id -> NAME
forall a b. (a -> b) -> a -> b
$ Morphism -> Id -> Id
applyMorphism Morphism
mor (Id -> Id) -> Id -> Id
forall a b. (a -> b) -> a -> b
$ NAME -> Id
Id.simpleIdToId NAME
tok

-- | Union of two morphisms.
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
propMap Morphism
mor1
      pmap2 :: Map Id Id
pmap2 = Morphism -> Map Id Id
propMap 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
allItems 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
allItems 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
      , propMap :: Map Id Id
propMap = 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