8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova{- |

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaModule : $Header$

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovaDescription : Definition of signature morphisms for

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

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaCopyright : (c) Kristina Sojakova, Jacobs University 2009

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaMaintainer : k.sojakova@ijacobs-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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , morphCanForm

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , applyMorph

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , mapSymbol

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , inclusionMorph

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , morphUnion

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , inducedFromMorphism

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , inducedFromToMorphism

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova , toTermMap

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ) where

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport DFOL.AS_DFOL

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaimport DFOL.Sign

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport DFOL.Symbol

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

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport qualified Data.Map as Map

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakovaimport qualified Data.Set as Set

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

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova } deriving (Eq, Ord, Show)

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

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova then fail $ "Codomain of the first morphism "

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova ++ "must equal the domain of the second."

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

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

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina Sojakova $ mapSymbol m1 sym1

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova in if (sym1 == sym2)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova then id

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova else 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

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina Sojakova in and $ [checkDom,checkCod] ++ checkTypes

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova

81d28e8372831ae5e6054d8d2212f0114b09b79aKristina SojakovacheckTypePres:: 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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova 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) -}

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina SojakovamorphCanForm :: Morphism -> Morphism

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina SojakovamorphCanForm (Morphism sig1 sig2 map1) =

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova let map2 = Map.fromList $ filter (\ (k,a) -> k /= a) $ 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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in if (isValidMorph m)

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

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina 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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova 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

887a1999374d1fb3a534e602a8d322de6ef4c8e8Kristina SojakovacombineMapsH :: Map.Map NAME NAME -> [(NAME,NAME)] ->

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

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovacombineMapsH map1 ((k,v):ds) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova if (Map.member k map1)

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova 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

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina 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

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina SojakovatoTermMap m = Map.fromList $ map (\ (k,a) -> (k, Identifier a))

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova $ Map.toList m

45caf47cd6ed07be0637f6c51e4735512ce9d83aKristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova-- pretty printing

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovainstance Pretty Morphism where

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova pretty = printMorph

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina SojakovaprintMorph :: Morphism -> Doc

cb5d588c4c3b286cc1e7210335d6ef7f584d79bcKristina SojakovaprintMorph m =

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova if m == (idMorph $ source m)

51bbd37b3957f301b2628422e161aac2cbd46f1cKristina Sojakova then vcat [text "Identity morphism on:", pretty $ source m]

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova else vcat [text "Source signature:", pretty $ source m,

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova text "Target signature:", pretty $ target m,

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina Sojakova text "Mapping:", printSymMap $ symMap m]

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova

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

f2f62e61c66f678b0042d1a772ff89849d8b2113Kristina SojakovaprintSymMap 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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovabuildSig (Sign ds) map1 = buildSigH (expandDecls ds) emptySig map1

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovabuildSigH :: [DECL] -> Sign -> Map.Map NAME NAME -> Result.Result Sign

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovabuildSigH (([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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova 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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else buildSigH ds (addSymbolDecl ([n2],t2) sig) map1

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovabuildSigH _ _ _ = Result.Result [] Nothing

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in if (isValidMorph m)

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else buildMorph (expandDecls ds) m

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovabuildMorph :: [DECL] -> Morphism -> Result.Result Morphism

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovabuildMorph (([n1],t1):ds) m@(Morphism _ sig2 map1) =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova if (Map.member n1 map1)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then let n2 = mapSymbol m n1

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova t2 = applyMorph m t1

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Just t3 = getSymbolType n2 sig2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in if t2 == t3

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then buildMorph ds m

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else Result.Result [incompatibleViewError2 n2 t2 t3] Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else let t2 = applyMorph m t1

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ss = getSymsOfType sig2 t2

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova in case ss of

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova [s] -> buildMorph ds $

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova [] -> Result.Result [noSymToMapError n1 t2] Nothing

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovabuildMorph _ _ = Result.Result [] Nothing

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetSymsOfType :: Sign -> TYPE -> [NAME]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetSymsOfType (Sign ds) t = getSymsOfTypeH ds t

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetSymsOfTypeH :: [DECL] -> TYPE -> [NAME]

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetSymsOfTypeH [] _ = []

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovagetSymsOfTypeH ((ns,t1):ds) t =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova if (t1 == t)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova then ns ++ (getSymsOfTypeH ds t)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova else getSymsOfTypeH ds t

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- ERROR MESSAGES

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaincompatibleViewError1 n t1 t2 =

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova Result.Diag

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova { Result.diagKind = Result.Error

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , Result.diagString = "Symbol\n" ++ (show $ pretty n)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\nmust have both type\n" ++ (show $ pretty t1)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , Result.diagString = "Symbol\n" ++ (show $ pretty n)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\nmust have type\n" ++ (show $ pretty t1)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , 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"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ (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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , 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"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ (show $ pretty t) ++ "\n namely\n"

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ (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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , Result.diagString = "Signature\n" ++ (show $ pretty sig1)

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ (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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , Result.diagString = "Symbol\n" ++ (show $ pretty n)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\nis mapped both to\n" ++ (show $ pretty n1)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova , Result.diagString = "The combination of morphisms\n" ++ (show $ pretty m1)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova ++ "\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 }