Morphism.hs revision 1ac1d44af1a5d0c4a800b689d2afc68826484b06
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettDescription : Abstract syntax for reduce
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyCopyright : (c) Dominik Dietrich, DFKI Bremen 2010
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyLicense : GPLv2 or higher, see LICENSE.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : dominik.dietrich@dfki.de
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettStability : experimental
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachthis file defines morhpisms for the reduce logic. A morphism is a mapping of operator symbols
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ( Morphism (..) -- datatype for Morphisms
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , pretty -- pretty printing
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , idMor -- identity morphism
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , isLegalMorphism -- check if morhpism is ok
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett , composeMor -- composition
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett , inclusionMap -- inclusion map
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett , mapSentence -- map of sentences
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder , mapSentenceH -- map of sentences, without Result type
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett , applyMap -- application function for maps
5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maeder , applyMorphism -- application function for morphism
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett , morphismUnion
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblettimport qualified Data.Map as Map
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport qualified Data.Set as Set
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maederimport qualified Common.Result as Result
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett-- | The datatype for morphisms in reduce logic as maps of sets
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettdata Morphism = Morphism
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett { source :: Sign
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett , target :: Sign
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder , operatorMap :: Map.Map Id Id
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett } deriving (Eq, Ord, Show)
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyinstance Pretty Morphism where
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly pretty = printMorphism
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reilly-- | pretty printer for morphisms
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettprintMorphism :: Morphism -> Doc
765e55b764e0fd32c09d33709d6e2770c4766799Christian MaederprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly <> pretty y <> rparen) $ Map.assocs $ operatorMap m)
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder-- | Constructs an id-morphism
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian MaederidMor :: Sign -> Morphism
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian MaederidMor a = inclusionMap a a
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | checks whether a given morphism is legal
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisLegalMorphism :: Morphism -> Bool
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyisLegalMorphism _ = True
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | calculates the composition of two morhpisms f:X->Y, g:Y->Z
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillycomposeMor :: Morphism -> Morphism -> Result Morphism
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian MaedercomposeMor f g =
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett let fSource = source f
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett gTarget = target g
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett fMap = operatorMap f
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett gMap = operatorMap g
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett in return Morphism
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett { source = fSource
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , target = gTarget
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , operatorMap = if Map.null gMap then fMap else
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett if i == j then id else Map.insert i j)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | constructs the inclusion map for a given signature
e771539425f4a0abef9f94cf4b63690f3603f682Andy GimblettinclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettinclusionMap s1 s2 = Morphism
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett { source = s1
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , target = s2
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett , operatorMap = Map.empty }
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett-- | Application function for propMaps
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettapplyMap :: Map.Map Id Id -> Id -> Id
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettapplyMap operatormap idt = Map.findWithDefault idt idt operatormap
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett-- | Application funtion for morphisms
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettapplyMorphism :: Morphism -> Id -> Id
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettapplyMorphism mor idt = Map.findWithDefault idt idt $ operatorMap mor
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett-- | sentence translation along signature morphism
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett-- here just the renaming of formulae
e771539425f4a0abef9f94cf4b63690f3603f682Andy GimblettmapSentence :: Morphism -> CMD -> Result.Result CMD
e771539425f4a0abef9f94cf4b63690f3603f682Andy GimblettmapSentence mor = return . mapSentenceH mor
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettmapSentenceH :: Morphism -> CMD -> CMD
f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian MaedermapSentenceH _ frm = frm
90047eafd2de482c67bcd13103c6064e9b0cb254Andy GimblettmorphismUnion :: Morphism -> Morphism -> Result.Result Morphism
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettmorphismUnion mor1 mor2 =
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett let pmap1 = operatorMap mor1
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett pmap2 = operatorMap mor2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett p1 = source mor1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett p2 = source mor2
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett up1 = Set.difference (Map.keysSet $ items p1) $ Map.keysSet pmap1
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett up2 = Set.difference (Map.keysSet $ items p2) $ Map.keysSet pmap2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Nothing -> (ds, Map.insert i j m)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Just k -> if j == k then (ds, m) else
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly ("incompatible mapping of prop " ++ showId i " to "
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly ++ showId j " and " ++ showId k "")
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly nullRange : ds, m)) ([], pmap1)
4770d29adda064baa5dbfcca03f600d7608806f7Liam O'Reilly (Map.toList pmap2 ++ map (\ a -> (a, a))
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett in if null pds then return Morphism
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett { source = unite p1 p2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , target = unite (target mor1) $ target mor2
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , operatorMap = pmap } else Result pds Nothing