git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2100 from david-christiansen/maybe-monoid

Replace the Monoid instance on Maybe

commit8a3d3480c0d7233534569dd69b2098ca8f37b220 authorDavid Christiansen <david@davidchristiansen.dk> dateThu 2 Apr 2015, 14:14 (12 years ago) parent7871ecb8b3b6e8
3 files changed+28−12
compare with master
unifiedsplit
CHANGELOG+3 libs/prelude/Prelude/Maybe.idr+18−10 src/Idris/IdrisDoc.hs+7−2
CHANGELOG+3
@@ -21,6 +21,9 @@ New in 0.9.18:
2121 requiring a separate lemma.
2222* Case alternatives are allowed to be impossible:
2323 case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }
24+* The default Semigroup and Monoid instances for Maybe are now prioritised
25+ choice, keeping the first success as Alternative does. The version that
26+ collects successes is now a named instance.
2427
2528New in 0.9.17:
2629--------------
libs/prelude/Prelude/Maybe.idr+18−10
@@ -78,17 +78,25 @@ instance (Eq a) => Eq (Maybe a) where
7878 (Just _) == Nothing = False
7979 (Just a) == (Just b) = a == b
8080
81−-- Lift a semigroup into 'Maybe' forming a 'Monoid' according to
82−-- <http://en.wikipedia.org/wiki/Monoid>: "Any semigroup S may be
83−-- turned into a monoid simply by adjoining an element i not in S
84−-- and defining i+i = i and i+s = s = s+i for all s in S."
85−
86−instance (Semigroup a) => Semigroup (Maybe a) where
87− Nothing <+> m = m
88− m <+> Nothing = m
81+||| Prioritised choice. Just like the `Alternative` instance, the
82+||| `Semigroup` for `Maybe a` keeps the first succeeding computation.
83+|||
84+||| **NB**: This is a different choice than in the Haskell libraries.
85+||| Use `collectJust` to get the Haskell behaviour.
86+instance Semigroup (Maybe a) where
87+ Nothing <+> m = m
88+ (Just x) <+> _ = Just x
89+
90+||| Transform any semigroup into a monoid by using `Nothing` as the
91+||| designated neutral element and collecting the contents of the
92+||| `Just` constructors using a semigroup structure on `a`. This is
93+||| the behaviour in the Haskell libraries.
94+instance [collectJust] Semigroup a => Semigroup (Maybe a) where
95+ Nothing <+> m = m
96+ m <+> Nothing = m
8997 (Just m1) <+> (Just m2) = Just (m1 <+> m2)
9098
91−instance (Semigroup a) => Monoid (Maybe a) where
99+instance Monoid (Maybe a) where
92100 neutral = Nothing
93101
94102instance (Monoid a, Eq a) => Cast a (Maybe a) where
@@ -98,5 +106,5 @@ instance (Monoid a) => Cast (Maybe a) a where
98106 cast = lowerMaybe
99107
100108instance Foldable Maybe where
101− foldr _ z Nothing = z
109+ foldr _ z Nothing = z
102110 foldr f z (Just x) = f x z
src/Idris/IdrisDoc.hs+7−2
@@ -1,5 +1,6 @@
11{-# LANGUAGE PatternGuards #-}
22{-# LANGUAGE OverloadedStrings #-}
3+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
34
45-- | Generation of HTML documentation for Idris code
56module Idris.IdrisDoc (generateDocs) where
@@ -217,9 +218,11 @@ referredNss (n, Just d, _) =
217218 names = concatMap (extractPTermNames) ts
218219 in S.map getNs $ S.fromList names
219220
220− where getFunDocs (FunDoc f) = [f]
221− getFunDocs (DataDoc f fs) = f:fs
221+ where getFunDocs (FunDoc f) = [f]
222+ getFunDocs (DataDoc f fs) = f:fs
222223 getFunDocs (ClassDoc _ _ fs _ _ _ _) = fs
224+ getFunDocs (NamedInstanceDoc _ fd) = [fd]
225+ getFunDocs (ModDoc _ _) = []
223226 types (FD _ _ args t _) = t:(map second args)
224227 second (_, x, _, _) = x
225228
@@ -609,6 +612,8 @@ createOtherDoc ist (DataDoc fd@(FD n docstring args _ _) fds) = do
609612 H.dt $ toHtml $ show name
610613 H.dd $ Docstrings.renderHtml docstring
611614
615+createOtherDoc ist (NamedInstanceDoc _ fd) = createFunDoc ist fd
616+
612617createOtherDoc ist (ModDoc _ docstring) = do
613618 Docstrings.renderHtml docstring
614619