Morphism.hs revision 96a467c395740b3e785a9bc3d6d37a3273fafd03
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettDescription : Definition of signature morphisms for the Edinburgh
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder Logical Framework
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederCopyright : (c) Kristina Sojakova, DFKI Bremen 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederMaintainer : k.sojakova@jacobs-university.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : experimental
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport qualified Common.Result as Result
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport qualified Data.Map as Map
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport qualified Data.Set as Set
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachdata MorphType = Definitional | Postulated | Unknown deriving (Ord,Eq,Show)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder-- LF morphism cannot map defined symbols, only declared ones
842ae753ab848a8508c4832ab64296b929167a97Christian Maederdata Morphism = Morphism
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett { morphBase :: BASE
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , morphModule :: MODULE
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , morphName :: NAME
70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder , source :: Sign
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , target :: Sign
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder , morphType :: MorphType
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder , symMap :: Map.Map Symbol EXP
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblett } deriving (Ord, Show)
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett-- constructs an identity morphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyidMorph :: Sign -> Morphism
9f93b2a8b552789cd939d599504d39732672dc84Christian MaederidMorph sig = Morphism "" "" "" sig sig Unknown Map.empty
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder-- composes two morphisms
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycompMorph :: Morphism -> Morphism -> Result Morphism
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillycompMorph m1 m2 =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder if target m1 /= source m2
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder then Result.Result [incompatibleMorphsError m1 m2] Nothing
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder let Just e1 = mapSymbol s m1
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder Just e2 = translate m2 e1
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder getDeclaredSyms $ source m1
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return $ Morphism "" "" "" (source m1) (target m2) Unknown newmap
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- applies a morphism to a symbol in the source signature
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaedermapSymbol :: Symbol -> Morphism -> Maybe EXP
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaedermapSymbol s m =
a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian Maeder let sig = source m
a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian Maeder in if (isDeclaredSym s sig)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder then Just $ Map.findWithDefault (Const s) s $ symMap m
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder else if (isDefinedSym s sig)
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder then do val <- getSymValue s sig
7e7d791d2f643ffd82843b78e424b6f9f68c24eeChristian Maeder translate m val
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder-- translates a well-formed expression along the given morphism
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maedertranslate :: Morphism -> EXP -> Maybe EXP
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maedertranslate m e = translateH m (recForm e)
bcd914850de931848b86d7728192a149f9c0108bChristian MaedertranslateH :: Morphism -> EXP -> Maybe EXP
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedertranslateH _ Type = Just Type
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedertranslateH _ (Var n) = Just $ Var n
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedertranslateH m (Const s) =
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder do e <- mapSymbol s m
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedertranslateH m (Appl f [a]) =
12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder do f1 <- translateH m f
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett a1 <- translateH m a
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett return $ Appl f1 [a1]
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimbletttranslateH m (Func [t] s) =
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett do t1 <- translateH m t
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly s1 <- translateH m s
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett return $ Func [t1] s1
31f039ffdb33d78cb31d24b71d3155b11a323975Andy GimbletttranslateH m (Pi [(x,t)] a) =
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett do t1 <- translateH m t
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett a1 <- translateH m a
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett return $ Pi [(x,t1)] a1
842ae753ab848a8508c4832ab64296b929167a97Christian MaedertranslateH m (Lamb [(x,t)] a) =
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder do t1 <- translateH m t
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder a1 <- translateH m a
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett return $ Lamb [(x,t1)] a1
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimbletttranslateH _ _ = Nothing
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- converts the morphism into its canonical form where the symbol map contains
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett no key/value pairs of the form (s, Const s) -}
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettcanForm :: Morphism -> Morphism
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian MaedercanForm (Morphism b m n sig1 sig2 k map1) =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let map2 = Map.fromList $ filter (\ (s,e) -> Const s /= e) $ Map.toList map1
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder in Morphism b m n sig1 sig2 k map2
842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance Eq Morphism where
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder m1 == m2 = (canForm m1) == (canForm m2)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder-- pretty printing
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettinstance Pretty Morphism where
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett pretty m = printMorph $ canForm m
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettprintMorph :: Morphism -> Doc
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederprintMorph m = printSymMap (source m) (target m) $ symMap m
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederprintSymMap :: Sign -> Sign -> Map.Map Symbol EXP -> Doc
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian MaederprintSymMap sig1 sig2 m =
dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder vcat $ map (\ (s,e) -> printSymbol sig1 s <+> text "|->" <+> printExp sig2 e)
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly-- ERROR MESSAGES
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillyincompatibleMorphsError :: Morphism -> Morphism -> Result.Diagnosis
05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillyincompatibleMorphsError m1 m2 =
7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder , Result.diagString = "Codomain of the morphism\n" ++ (show $ pretty m1)
ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder ++ "\nis different from the domain of the morphism\n"
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett ++ (show $ pretty m2)
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett ++ "\nhence their composition cannot be constructed."