Morphism.hs revision 98890889ffb2e8f6f722b00e265a211f13b5a861
a78048ccbdb6256da15e6b0e7e95355e480c2301ndModule : $Header$
fd9abdda70912b99b24e3bf1a38f26fde908a74cndDescription : Definition of signature morphisms for the Edinburgh
fd9abdda70912b99b24e3bf1a38f26fde908a74cnd Logical Framework
fd9abdda70912b99b24e3bf1a38f26fde908a74cndCopyright : (c) Kristina Sojakova, DFKI Bremen 2009
a78048ccbdb6256da15e6b0e7e95355e480c2301ndLicense : GPLv2 or higher, see LICENSE.txt
a78048ccbdb6256da15e6b0e7e95355e480c2301ndMaintainer : k.sojakova@jacobs-university.de
a78048ccbdb6256da15e6b0e7e95355e480c2301ndStability : experimental
96ad5d81ee4a2cc66a4ae19893efc8aa6d06fae7jailletcPortability : portable
a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport qualified Data.Map as Map
a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport qualified Data.Set as Set
3f08db06526d6901aa08c110b5bc7dde6bc39905nddata MorphType = Definitional | Postulated | Unknown deriving (Ord,Eq,Show)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- LF morphism cannot map defined symbols, only declared ones
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjungdata Morphism = Morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301nd { morphBase :: BASE
4b575a6b6704b516f22d65a3ad35696d7b9ba372rpluem , morphModule :: MODULE
4b575a6b6704b516f22d65a3ad35696d7b9ba372rpluem , morphName :: NAME
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , source :: Sign
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , target :: Sign
4aa603e6448b99f9371397d439795c91a93637eand , morphType :: MorphType
a78048ccbdb6256da15e6b0e7e95355e480c2301nd , symMap :: Map.Map Symbol EXP
a78048ccbdb6256da15e6b0e7e95355e480c2301nd } deriving (Ord, Show)
4aa603e6448b99f9371397d439795c91a93637eand-- constructs an identity morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndidMorph :: Sign -> Morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndidMorph sig = Morphism "" "" "" sig sig Unknown Map.empty
a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- composes two morphisms
a78048ccbdb6256da15e6b0e7e95355e480c2301ndcompMorph :: Morphism -> Morphism -> Result Morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndcompMorph m1 m2 = do
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let newmap =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let Just e1 = mapSymbol s m1
a78048ccbdb6256da15e6b0e7e95355e480c2301nd Just e2 = translate m2 e1
a78048ccbdb6256da15e6b0e7e95355e480c2301nd getDeclaredSyms $ source m1
a78048ccbdb6256da15e6b0e7e95355e480c2301nd return $ Morphism "" "" "" (source m1) (target m2) Unknown newmap
a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- applies a morphism to a symbol in the source signature
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapSymbol :: Symbol -> Morphism -> Maybe EXP
a78048ccbdb6256da15e6b0e7e95355e480c2301ndmapSymbol s m =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let sig = source m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd in if (isDeclaredSym s sig)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd then Just $ Map.findWithDefault (Const s) s $ symMap m
a78048ccbdb6256da15e6b0e7e95355e480c2301nd else if (isDefinedSym s sig)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd then do val <- getSymValue s sig
a78048ccbdb6256da15e6b0e7e95355e480c2301nd translate m val
a78048ccbdb6256da15e6b0e7e95355e480c2301nd else Nothing
a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- translates a well-formed expression along the given morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndtranslate :: Morphism -> EXP -> Maybe EXP
a78048ccbdb6256da15e6b0e7e95355e480c2301ndtranslate m e = translateH m (recForm e)
a78048ccbdb6256da15e6b0e7e95355e480c2301ndtranslateH :: Morphism -> EXP -> Maybe EXP
a78048ccbdb6256da15e6b0e7e95355e480c2301ndtranslateH _ Type = Just Type
a78048ccbdb6256da15e6b0e7e95355e480c2301ndtranslateH _ (Var n) = Just $ Var n
a78048ccbdb6256da15e6b0e7e95355e480c2301ndtranslateH m (Const s) =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd do e <- mapSymbol s m
a78048ccbdb6256da15e6b0e7e95355e480c2301ndtranslateH m (Appl f [a]) =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd do f1 <- translateH m f
a78048ccbdb6256da15e6b0e7e95355e480c2301nd a1 <- translateH m a
a78048ccbdb6256da15e6b0e7e95355e480c2301nd return $ Appl f1 [a1]
a78048ccbdb6256da15e6b0e7e95355e480c2301ndtranslateH m (Func [t] s) =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd do t1 <- translateH m t
a78048ccbdb6256da15e6b0e7e95355e480c2301nd s1 <- translateH m s
a78048ccbdb6256da15e6b0e7e95355e480c2301nd return $ Func [t1] s1
a78048ccbdb6256da15e6b0e7e95355e480c2301ndtranslateH m (Pi [(x,t)] a) =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd do t1 <- translateH m t
a78048ccbdb6256da15e6b0e7e95355e480c2301nd a1 <- translateH m a
a78048ccbdb6256da15e6b0e7e95355e480c2301nd return $ Pi [(x,t1)] a1
a78048ccbdb6256da15e6b0e7e95355e480c2301ndtranslateH m (Lamb [(x,t)] a) =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd do t1 <- translateH m t
a78048ccbdb6256da15e6b0e7e95355e480c2301nd a1 <- translateH m a
a78048ccbdb6256da15e6b0e7e95355e480c2301nd return $ Lamb [(x,t1)] a1
a78048ccbdb6256da15e6b0e7e95355e480c2301ndtranslateH _ _ = Nothing
a78048ccbdb6256da15e6b0e7e95355e480c2301nd{- converts the morphism into its canonical form where the symbol map contains
a78048ccbdb6256da15e6b0e7e95355e480c2301nd no key/value pairs of the form (s, Const s) -}
a78048ccbdb6256da15e6b0e7e95355e480c2301ndcanForm :: Morphism -> Morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndcanForm (Morphism b m n sig1 sig2 k map1) =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let map2 = Map.fromList $ filter (\ (s,e) -> Const s /= e) $ Map.toList map1
a78048ccbdb6256da15e6b0e7e95355e480c2301nd in Morphism b m n sig1 sig2 k map2
a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- equality
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjunginstance Eq Morphism where
727872d18412fc021f03969b8641810d8896820bhumbedooh m1 == m2 = eqMorph (canForm m1) (canForm m2)
727872d18412fc021f03969b8641810d8896820bhumbedooheqMorph :: Morphism -> Morphism -> Bool
cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooheqMorph (Morphism _ m1 n1 s1 t1 k1 map1) (Morphism _ m2 n2 s2 t2 k2 map2) =
0d0ba3a410038e179b695446bb149cce6264e0abnd (m1,n1,s1,t1,k1,map1) == (m2,n2,s2,t2,k2,map2)
727872d18412fc021f03969b8641810d8896820bhumbedooh-- pretty printing
0d0ba3a410038e179b695446bb149cce6264e0abndinstance Pretty Morphism where
0d0ba3a410038e179b695446bb149cce6264e0abnd pretty m = printSymMap $ symMap $ canForm m
ac082aefa89416cbdc9a1836eaf3bed9698201c8humbedoohprintSymMap :: Map.Map Symbol EXP -> Doc
0d0ba3a410038e179b695446bb149cce6264e0abndprintSymMap m =
0d0ba3a410038e179b695446bb149cce6264e0abnd vcat $ map (\ (s,e) -> pretty s <+> text "|->" <+> pretty e) $ Map.toList m