Morphism.hs revision 98890889ffb2e8f6f722b00e265a211f13b5a861
a78048ccbdb6256da15e6b0e7e95355e480c2301nd{- |
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
a78048ccbdb6256da15e6b0e7e95355e480c2301nd
a78048ccbdb6256da15e6b0e7e95355e480c2301ndMaintainer : k.sojakova@jacobs-university.de
a78048ccbdb6256da15e6b0e7e95355e480c2301ndStability : experimental
96ad5d81ee4a2cc66a4ae19893efc8aa6d06fae7jailletcPortability : portable
a78048ccbdb6256da15e6b0e7e95355e480c2301nd-}
a78048ccbdb6256da15e6b0e7e95355e480c2301nd
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenmodule LF.Morphism where
2e545ce2450a9953665f701bb05350f0d3f26275nd
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenimport LF.Sign
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen
a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.Result
a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport Common.Doc
af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowenimport Common.DocUtils
3f08db06526d6901aa08c110b5bc7dde6bc39905nd
a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport qualified Data.Map as Map
a78048ccbdb6256da15e6b0e7e95355e480c2301ndimport qualified Data.Set as Set
a78048ccbdb6256da15e6b0e7e95355e480c2301nd
3f08db06526d6901aa08c110b5bc7dde6bc39905nddata MorphType = Definitional | Postulated | Unknown deriving (Ord,Eq,Show)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd
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)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd
4aa603e6448b99f9371397d439795c91a93637eand-- constructs an identity morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndidMorph :: Sign -> Morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndidMorph sig = Morphism "" "" "" sig sig Unknown Map.empty
a78048ccbdb6256da15e6b0e7e95355e480c2301nd
a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- composes two morphisms
a78048ccbdb6256da15e6b0e7e95355e480c2301ndcompMorph :: Morphism -> Morphism -> Result Morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndcompMorph m1 m2 = do
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let newmap =
a78048ccbdb6256da15e6b0e7e95355e480c2301nd Set.fold (\ s ->
a78048ccbdb6256da15e6b0e7e95355e480c2301nd let Just e1 = mapSymbol s m1
a78048ccbdb6256da15e6b0e7e95355e480c2301nd Just e2 = translate m2 e1
a78048ccbdb6256da15e6b0e7e95355e480c2301nd in Map.insert s e2
a78048ccbdb6256da15e6b0e7e95355e480c2301nd )
a78048ccbdb6256da15e6b0e7e95355e480c2301nd Map.empty $
a78048ccbdb6256da15e6b0e7e95355e480c2301nd getDeclaredSyms $ source m1
a78048ccbdb6256da15e6b0e7e95355e480c2301nd return $ Morphism "" "" "" (source m1) (target m2) Unknown newmap
a78048ccbdb6256da15e6b0e7e95355e480c2301nd
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
a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- translates a well-formed expression along the given morphism
a78048ccbdb6256da15e6b0e7e95355e480c2301ndtranslate :: Morphism -> EXP -> Maybe EXP
a78048ccbdb6256da15e6b0e7e95355e480c2301ndtranslate m e = translateH m (recForm e)
a78048ccbdb6256da15e6b0e7e95355e480c2301nd
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
a78048ccbdb6256da15e6b0e7e95355e480c2301nd return e
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
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
a78048ccbdb6256da15e6b0e7e95355e480c2301nd-- equality
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjunginstance Eq Morphism where
727872d18412fc021f03969b8641810d8896820bhumbedooh m1 == m2 = eqMorph (canForm m1) (canForm m2)
0d0ba3a410038e179b695446bb149cce6264e0abnd
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)
cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh
727872d18412fc021f03969b8641810d8896820bhumbedooh-- pretty printing
0d0ba3a410038e179b695446bb149cce6264e0abndinstance Pretty Morphism where
0d0ba3a410038e179b695446bb149cce6264e0abnd pretty m = printSymMap $ symMap $ canForm m
0d0ba3a410038e179b695446bb149cce6264e0abnd
ac082aefa89416cbdc9a1836eaf3bed9698201c8humbedoohprintSymMap :: Map.Map Symbol EXP -> Doc
0d0ba3a410038e179b695446bb149cce6264e0abndprintSymMap m =
0d0ba3a410038e179b695446bb149cce6264e0abnd vcat $ map (\ (s,e) -> pretty s <+> text "|->" <+> pretty e) $ Map.toList m
0d0ba3a410038e179b695446bb149cce6264e0abnd