Strips a
prefix from a
MonoidMap.
If map
m1 is a
prefix of map
m2, then
stripPrefix m1
m2 will produce a
reduced map where prefix
m1 is
stripped from
m2.
Properties
The
stripPrefix function, when applied to maps
m1 and
m2, produces a result if (and
only if)
m1 is a prefix of
m2:
isJust (stripPrefix m1 m2) == m1 `isPrefixOf` m2
The value for any key
k in the result is
identical to the result of stripping the value for
k in map
m1 from the value for
k in map
m2:
all
(\r -> Just (get k r) == stripPrefix (get k m1) (get k m2))
(stripPrefix m1 m2)
If we append prefix
m1 to the
left-hand side of
the result, we can always recover the original map
m2:
all
(\r -> m1 <> r == m2)
(stripPrefix m1 m2)
This function provides the definition of
stripPrefix for the
MonoidMap instance of
LeftReductive.
Examples
With
String values:
>>> m1 = fromList [(1, "" ), (2, "i" ), (3, "pq" ), (4, "xyz")]
>>> m2 = fromList [(1, "abc"), (2, "ijk"), (3, "pqr"), (4, "xyz")]
>>> m3 = fromList [(1, "abc"), (2, "jk"), (3, "r"), (4, "")]
>>> stripPrefix m1 m2 == Just m3
True
>>> stripPrefix m2 m1 == Nothing
True
With
Sum Natural values:
>>> m1 = fromList [("a", 0), ("b", 1), ("c", 2), ("d", 3)]
>>> m2 = fromList [("a", 3), ("b", 3), ("c", 3), ("d", 3)]
>>> m3 = fromList [("a", 3), ("b", 2), ("c", 1), ("d", 0)]
>>> stripPrefix m1 m2 == Just m3
True
>>> stripPrefix m2 m1 == Nothing
True