1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./DFOL/Morphism.hs

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovaDescription : Definition of signature morphisms for

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakova first-order logic with dependent types (DFOL)

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaCopyright : (c) Kristina Sojakova, DFKI Bremen 2009

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaMaintainer : k.sojakova@jacobs-university.de

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaStability : experimental

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaPortability : portable

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-}

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovamodule DFOL.Morphism

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ( Morphism (..)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , idMorph

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , compMorph

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , isValidMorph

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova , canForm

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , applyMorph

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , mapSymbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , inclusionMorph

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , morphUnion

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , inducedFromMorphism

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , inducedFromToMorphism

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova , coGenSig

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova , toTermMap

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ) where

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport DFOL.AS_DFOL

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport DFOL.Sign

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport DFOL.Symbol

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Common.Result

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Common.Doc

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport Common.DocUtils

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.Id

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport Common.ExtSign

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport qualified Common.Result as Result

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport qualified Data.Map as Map

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport qualified Data.Set as Set

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport Data.Data

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- morphisms for DFOL - maps of symbol names

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakovadata Morphism = Morphism

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova { source :: Sign

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova , target :: Sign

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova , symMap :: Map.Map NAME NAME

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Ord, Show, Typeable)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- constructs an identity morphism

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaidMorph :: Sign -> Morphism

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovaidMorph sig = Morphism sig sig Map.empty

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova-- composes two morphisms

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovacompMorph :: Morphism -> Morphism -> Result Morphism

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovacompMorph m1 m2 =

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova if target m1 /= source m2

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova then Result.Result [incompatibleMorphsError m1 m2] Nothing

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova else return $ Morphism (source m1) (target m2) $

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova Set.fold (\ sym1 -> let sym2 = mapSymbol m2

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova $ mapSymbol m1 sym1

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova in Map.insert sym1 sym2)

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova Map.empty $

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova getSymbols $ source m1

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova-- determines whether a morphism is valid

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaisValidMorph :: Morphism -> Bool

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovaisValidMorph m@(Morphism sig1 sig2 map1) =

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova let sym1 = getSymbols sig1

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova sym2 = getSymbols sig2

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova checkDom = Set.isSubsetOf (Map.keysSet map1) sym1

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova checkCod = Set.isSubsetOf (Set.map (mapSymbol m) sym1) sym2

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova checkTypes = map (checkTypePres m) $ Set.toList sym1

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder in and $ [checkDom, checkCod] ++ checkTypes

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedercheckTypePres :: Morphism -> NAME -> Bool

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovacheckTypePres m n =

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova let Just type1 = getSymbolType n $ source m

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova Just type2 = getSymbolType (mapSymbol m n) $ target m

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in applyMorph m type1 == type2

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova{- converts the morphism into its canonical form where the symbol map contains

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova no key/value pairs of the form (k,k) -}

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovacanForm :: Morphism -> Morphism

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovacanForm (Morphism sig1 sig2 map1) =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let map2 = Map.fromList $ filter (uncurry (/=)) $ Map.toList map1

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova in Morphism sig1 sig2 map2

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- constructs the inclusion morphism between signatures

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovainclusionMorph :: Sign -> Sign -> Result.Result Morphism

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovainclusionMorph sig1 sig2 =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let m = Morphism sig1 sig2 Map.empty

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if isValidMorph m

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then Result.Result [] $ Just m

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else Result.Result [noSubsigError sig1 sig2] Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder{- generated and cogenerated signatures

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaederAlgorithm description:

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaFOR GENERATED SIGNATURES

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaInput : a signature "sig" and a set of symbols "syms"

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaOutput : an inclusion morphism

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova1 : Check if all symbols in syms occur in sig; if not, output Nothing

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova2 : Initialize the set of symbols "incl" which necessarily must be included

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova in the generated signature to syms

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova Initialize the set "done" of analyzed symbols to empty

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova Initialize the set "todo" of symbols to be analyzed to syms

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova3 : Check if todo is empty

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova 3.1 : If yes, go to 5

12d9bff7c82145a8b68bfb8553688172655c926eKristina Sojakova 3.2 : If not, go to 4

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova4 : Pick a symbol "s" from todo

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova 4.1 : Get the type "t" of s in sig

12d9bff7c82145a8b68bfb8553688172655c926eKristina Sojakova 4.2 : Get the set "vars" of free variables in t, i.e. the symbols of sig

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova that t depends on

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova 4.3 : For each "v" in vars :

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova 4.3.1 : Add v to incl

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova 4.3.2 : If v does not occur in done, add it to todo

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova 4.4 : Remove v from todo and add it to done

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova 4.5 : Go to 3

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova5 : Let "sig1" be the subsignature of sig containing only the symbols in incl

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova and output the inclusion morphism m : sig1 -> sig

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaFOR COGENERATED SIGNATURES

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaInput : a signature "sig" and a set of symbols "syms"

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovaOutput : an inclusion morphism

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova1 : Check if all symbols in syms occur in sig; if not, output Nothing

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova2 : Initialize the set of symbols "excl" which necessarily must be excluded

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova from the cogenerated signature to syms

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova3 : For each symbol "s" in sig (keeping the order in which they are defined) :

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova 3.1 : If s does not occur in excl :

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova 4.1 : Get the type "t" of s in sig

12d9bff7c82145a8b68bfb8553688172655c926eKristina Sojakova 4.2 : Get the set "vars" of free variables in t, i.e. the symbols

12d9bff7c82145a8b68bfb8553688172655c926eKristina Sojakova of sig that t depends on

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova 4.3 : If any of the symbols in vars occurs in excl, add s to excl

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova4 : Let "sig1" be the subsignature of sig containing all the symbols not

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova occurring in excl and output the inclusion morphism m : sig1 -> sig

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova-}

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovacoGenSig :: Bool -> Set.Set Symbol -> Sign -> Result Morphism

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovacoGenSig flag syms sig@(Sign ds) =

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova let names = Set.map name syms

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova ds1 = expandDecls ds

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if Set.isSubsetOf names (getSymbols sig)

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova then let incl = if flag

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova then cogSig names ds1 sig

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else genSig names Set.empty names sig

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder ds2 = map (\ (n, t) -> ([n], t))

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder $ filter (\ (n, _) -> Set.member n incl) ds1

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova in inclusionMorph (Sign ds2) sig

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova else Result.Result [symsNotInSigError names sig] Nothing

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovagenSig :: Set.Set NAME -> Set.Set NAME -> Set.Set NAME -> Sign -> Set.Set NAME

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovagenSig incl done todo sig =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if Set.null todo

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova then incl

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova else let n = Set.findMin todo

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova Just t = getSymbolType n sig

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova ns = getFreeVars t

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova incl1 = Set.union incl ns

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ns1 = Set.filter (`Set.member` done) ns

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova done1 = Set.insert n done

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova todo1 = Set.union ns1 $ Set.delete n todo

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova in genSig incl1 done1 todo1 sig

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedercogSig :: Set.Set NAME -> [SDECL] -> Sign -> Set.Set NAME

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina SojakovacogSig excl [] sig = Set.difference (getSymbols sig) excl

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedercogSig excl ((n, t) : ds) sig =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if Set.member n excl

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova then cogSig excl ds sig

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova else let ns = Set.toList $ getFreeVars t

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder depen = any (`Set.member` excl) ns

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova in if depen

b470a3e54a4289b4189906e41f0c04578c85619dKristina Sojakova then let excl1 = Set.insert n excl

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova in cogSig excl1 ds sig

5b84285ea066187061fc123a3b86b1b6433e06b5Kristina Sojakova else cogSig excl ds sig

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- morphism union

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovamorphUnion :: Morphism -> Morphism -> Result.Result Morphism

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovamorphUnion m1@(Morphism sig1D sig1C map1) m2@(Morphism sig2D sig2C map2) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let Result.Result diag1 sigDM = sigUnion sig1D sig2D

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Result diag2 sigCM = sigUnion sig1C sig2C

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova Result.Result diag3 map3M = combineMaps map1 map2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in case sigDM of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> Result.Result diag1 Nothing

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova Just sigD ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case sigCM of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> Result.Result diag2 Nothing

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova Just sigC ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova case map3M of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> Result.Result diag3 Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just map3 ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let m = Morphism sigD sigC map3

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if isValidMorph m

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then Result.Result [] $ Just m

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova else Result.Result

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova [invalidMorphError m1 m2] Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovacombineMaps :: Map.Map NAME NAME -> Map.Map NAME NAME ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Result (Map.Map NAME NAME)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovacombineMaps map1 map2 = combineMapsH map1 $ Map.toList map2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedercombineMapsH :: Map.Map NAME NAME -> [(NAME, NAME)] ->

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova Result.Result (Map.Map NAME NAME)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovacombineMapsH map1 [] = Result.Result [] $ Just map1

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedercombineMapsH map1 ((k, v) : ds) =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if Map.member k map1

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then let Just v1 = Map.lookup k map1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if v == v1

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then combineMapsH map1 ds

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova else Result.Result [incompatibleMapError k v v1] Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else let map2 = Map.insert k v map1

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova in combineMapsH map2 ds

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova-- applies a morphism to a symbol

345d3dcc9f809776009851c446916fc770aa428dKristina SojakovamapSymbol :: Morphism -> NAME -> NAME

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovamapSymbol m sym = Map.findWithDefault sym sym $ symMap m

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova

345d3dcc9f809776009851c446916fc770aa428dKristina Sojakova-- translates a term, type or formula along the given morphism

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaapplyMorph :: Translatable a => Morphism -> a -> a

a3a6b6ebe9c2d1dc3554e44779dc7361a90e7617Kristina SojakovaapplyMorph m t =

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova let syms = getSymbols (target m)

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova map1 = toTermMap $ symMap m

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova in translate map1 syms t

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina SojakovatoTermMap :: Map.Map NAME NAME -> Map.Map NAME TERM

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaedertoTermMap m = Map.fromList $ map (\ (k, a) -> (k, Identifier a))

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova $ Map.toList m

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova-- equality

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovainstance Eq Morphism where

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova m1 == m2 = eqMorph (canForm m1) (canForm m2)

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina SojakovaeqMorph :: Morphism -> Morphism -> Bool

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina SojakovaeqMorph (Morphism s1 t1 map1) (Morphism s2 t2 map2) =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (s1, t1, map1) == (s2, t2, map2)

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-- pretty printing

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovainstance Pretty Morphism where

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova pretty = printMorph

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaprintMorph :: Morphism -> Doc

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovaprintMorph m =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder vcat $ if m == idMorph (source m)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then [text "Identity morphism on:", pretty $ source m]

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else [text "Source signature:", pretty $ source m,

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder text "Target signature:", pretty $ target m,

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder text "Mapping:", printSymMap $ symMap m]

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina SojakovaprintSymMap :: Map.Map NAME NAME -> Doc

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaederprintSymMap m = vcat $ map (\ (k, a) -> pretty k <+> text "|->" <+> pretty a)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova $ Map.toList m

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- induces a signature morphism from the source signature and a symbol map

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovainducedFromMorphism :: Map.Map Symbol Symbol -> Sign -> Result.Result Morphism

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovainducedFromMorphism map1 sig1 =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let map2 = toNameMap map1

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Result dgs sig2M = buildSig sig1 map2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in case sig2M of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing -> Result.Result dgs Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just sig2 -> Result.Result [] $ Just $ Morphism sig1 sig2 map2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovabuildSig :: Sign -> Map.Map NAME NAME -> Result.Result Sign

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederbuildSig (Sign ds) = buildSigH (expandDecls ds) emptySig

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaederbuildSigH :: [SDECL] -> Sign -> Map.Map NAME NAME -> Result.Result Sign

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovabuildSigH [] sig _ = Result.Result [] $ Just sig

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaederbuildSigH ((n1, t1) : ds) sig map1 =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let n2 = Map.findWithDefault n1 n1 map1

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova map2 = toTermMap map1

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova syms = Set.map (\ n -> Map.findWithDefault n n map1)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova $ getSymbols sig

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova t2 = translate map2 syms t1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if isConstant n2 sig

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then let Just t3 = getSymbolType n2 sig

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in if t2 == t3

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then buildSigH ds sig map1

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else Result.Result [incompatibleViewError1 n2 t2 t3]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Nothing

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian Maeder else buildSigH ds (addSymbolDecl ([n2], t2) sig) map1

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- induces a signature morphism from the source and target sigs and a symbol map

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovainducedFromToMorphism :: Map.Map Symbol Symbol -> ExtSign Sign Symbol ->

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ExtSign Sign Symbol -> Result.Result Morphism

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovainducedFromToMorphism map1 (ExtSign sig1 _) (ExtSign sig2 _) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova let map2 = toNameMap map1

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova m = Morphism sig1 sig2 map2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Sign ds = sig1

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova in buildMorph (expandDecls ds) m

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

fc08da86ea2ef76a631faca30ca30b8ed112d864Christian MaederbuildMorph :: [SDECL] -> Morphism -> Result.Result Morphism

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovabuildMorph [] m = Result.Result [] $ Just m

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina SojakovabuildMorph ((n1, t1) : ds) m@(Morphism _ sig2 map1) = do

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let t2 = applyMorph m t1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if Map.member n1 map1

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova then do

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let n2 = mapSymbol m n1

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let Just t3 = getSymbolType n2 sig2

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if t2 == t3 then buildMorph ds m else

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova Result.Result [incompatibleViewError2 n2 t2 t3] Nothing

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova else do

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let t3 = getSymbolType n1 sig2

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if Just t2 == t3 then buildMorph ds m else do

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let ss = getSymsOfType sig2 t2

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova case ss of

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova [s] -> buildMorph ds $

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova m {symMap = Map.insert n1 s $ symMap m}

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova [] -> Result.Result [noSymToMapError n1 t2] Nothing

d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova _ -> Result.Result [manySymToMapError n1 t2 ss] Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- ERROR MESSAGES

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaincompatibleMorphsError :: Morphism -> Morphism -> Result.Diagnosis

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaincompatibleMorphsError m1 m2 =

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova Result.Diag

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova { Result.diagKind = Result.Error

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , Result.diagString = "Codomain of the morphism\n" ++ show (pretty m1)

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova ++ "\nis different from the domain of the morphism\n"

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (pretty m2)

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova ++ "\nhence their composition cannot be constructed."

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova , Result.diagPos = nullRange

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova }

14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaincompatibleViewError1 :: NAME -> TYPE -> TYPE -> Result.Diagnosis

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaincompatibleViewError1 n t1 t2 =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Diag

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova { Result.diagKind = Result.Error

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , Result.diagString = "Symbol\n" ++ show (pretty n)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ "\nmust have both type\n" ++ show (pretty t1)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ "\nand type\n" ++ show (pretty t2)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\nin the target signature and hence "

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "the view is ill-formed."

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , Result.diagPos = nullRange

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaincompatibleViewError2 :: NAME -> TYPE -> TYPE -> Result.Diagnosis

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaincompatibleViewError2 n t1 t2 =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Diag

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova { Result.diagKind = Result.Error

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , Result.diagString = "Symbol\n" ++ show (pretty n)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ "\nmust have type\n" ++ show (pretty t1)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ "\nbut instead has type\n" ++ show (pretty t2)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\nin the target signature and hence "

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "the view is ill-formed."

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , Result.diagPos = nullRange

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovanoSymToMapError :: NAME -> TYPE -> Result.Diagnosis

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovanoSymToMapError n t =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Diag

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova { Result.diagKind = Result.Error

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , Result.diagString = "Symbol\n" ++ show (pretty n)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\ncannot be mapped to anything as the target "

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "signature contains no symbols of type\n"

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (pretty t)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , Result.diagPos = nullRange

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovamanySymToMapError :: NAME -> TYPE -> [NAME] -> Result.Diagnosis

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovamanySymToMapError n t ss =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Diag

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova { Result.diagKind = Result.Error

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , Result.diagString = "Symbol\n" ++ show (pretty n)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\ncannot be uniquely mapped as the target "

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "signature contains multiple symbols of type\n"

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (pretty t) ++ "\n namely\n"

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (printNames ss)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , Result.diagPos = nullRange

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovanoSubsigError :: Sign -> Sign -> Result.Diagnosis

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovanoSubsigError sig1 sig2 =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Diag

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova { Result.diagKind = Result.Error

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , Result.diagString = "Signature\n" ++ show (pretty sig1)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\nis not a subsignature of\n"

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (pretty sig2)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\nand hence the inclusion morphism "

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina Sojakova ++ "cannot be constructed."

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , Result.diagPos = nullRange

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaincompatibleMapError :: NAME -> NAME -> NAME -> Result.Diagnosis

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaincompatibleMapError n n1 n2 =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Diag

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova { Result.diagKind = Result.Error

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , Result.diagString = "Symbol\n" ++ show (pretty n)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ "\nis mapped both to\n" ++ show (pretty n1)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ "\nand\n" ++ show (pretty n2)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\nin the target signature and hence "

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "the morphism union cannot be constructed."

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , Result.diagPos = nullRange

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovainvalidMorphError :: Morphism -> Morphism -> Result.Diagnosis

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovainvalidMorphError m1 m2 =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Diag

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova { Result.diagKind = Result.Error

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , Result.diagString = "The combination of morphisms\n" ++ show (pretty m1)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ "\nand\n" ++ show (pretty m2)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\nis not a valid morphism and hence "

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "their union cannot be constructed."

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , Result.diagPos = nullRange

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova }

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovasymsNotInSigError :: Set.Set NAME -> Sign -> Result.Diagnosis

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina SojakovasymsNotInSigError syms sig =

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova Result.Diag

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova { Result.diagKind = Result.Error

7caaddef0ccffd5528a7cde7cb0b7161250f4e59Kristina Sojakova , Result.diagString = "The symbols\n"

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (printNames $ Set.toList syms)

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova ++ "\nare not in the signature\n"

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ show (pretty sig)

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova ++ "\nand hence the (co)generated signature "

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova ++ "cannot be constructed."

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova , Result.diagPos = nullRange

df31d6f25f90e5112184f4eb60c8d3c7b116ca2dKristina Sojakova }