git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2100 from david-christiansen/maybe-monoid
8a3d348David Christiansen
CHANGELOG+3
compare with master
unifiedsplit
@@ -21,6 +21,9 @@ New in 0.9.18:
21 requiring a separate lemma.
21 requiring a separate lemma.
22* Case alternatives are allowed to be impossible:
22* Case alternatives are allowed to be impossible:
23 case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }
23 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.
24
27
25New in 0.9.17:
28New in 0.9.17:
26--------------
29--------------
libs/prelude/Prelude/Maybe.idr+18−10
@@ -78,17 +78,25 @@ instance (Eq a) => Eq (Maybe a) where
78 (Just _) == Nothing = False
78 (Just _) == Nothing = False
79 (Just a) == (Just b) = a == b
79 (Just a) == (Just b) = a == b
80
80
81−-- Lift a semigroup into 'Maybe' forming a 'Monoid' according to
81+||| Prioritised choice. Just like the `Alternative` instance, the
82−-- <http://en.wikipedia.org/wiki/Monoid>: "Any semigroup S may be
82+||| `Semigroup` for `Maybe a` keeps the first succeeding computation.
83−-- turned into a monoid simply by adjoining an element i not in S
83+|||
84−-- and defining i+i = i and i+s = s = s+i for all s in S."
84+||| **NB**: This is a different choice than in the Haskell libraries.
85−
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.
86−instance (Semigroup a) => Semigroup (Maybe a) where
94+instance [collectJust] Semigroup a => Semigroup (Maybe a) where
87− Nothing <+> m = m
95+ Nothing <+> m = m
88− m <+> Nothing = m
96+ m <+> Nothing = m
89 (Just m1) <+> (Just m2) = Just (m1 <+> m2)
97 (Just m1) <+> (Just m2) = Just (m1 <+> m2)
90
98
91−instance (Semigroup a) => Monoid (Maybe a) where
99+instance Monoid (Maybe a) where
92 neutral = Nothing
100 neutral = Nothing
93
101
94instance (Monoid a, Eq a) => Cast a (Maybe a) where
102instance (Monoid a, Eq a) => Cast a (Maybe a) where
@@ -98,5 +106,5 @@ instance (Monoid a) => Cast (Maybe a) a where
98 cast = lowerMaybe
106 cast = lowerMaybe
99
107
100instance Foldable Maybe where
108instance Foldable Maybe where
101− foldr _ z Nothing = z
109+ foldr _ z Nothing = z
102 foldr f z (Just x) = f x z
110 foldr f z (Just x) = f x z
src/Idris/IdrisDoc.hs+7−2
@@ -1,5 +1,6 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
2{-# LANGUAGE OverloadedStrings #-}
2{-# LANGUAGE OverloadedStrings #-}
3+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3
4
4-- | Generation of HTML documentation for Idris code
5-- | Generation of HTML documentation for Idris code
5module Idris.IdrisDoc (generateDocs) where
6module Idris.IdrisDoc (generateDocs) where
@@ -217,9 +218,11 @@ referredNss (n, Just d, _) =
217 names = concatMap (extractPTermNames) ts
218 names = concatMap (extractPTermNames) ts
218 in S.map getNs $ S.fromList names
219 in S.map getNs $ S.fromList names
219
220
220− where getFunDocs (FunDoc f) = [f]
221+ where getFunDocs (FunDoc f) = [f]
221− getFunDocs (DataDoc f fs) = f:fs
222+ getFunDocs (DataDoc f fs) = f:fs
222 getFunDocs (ClassDoc _ _ fs _ _ _ _) = fs
223 getFunDocs (ClassDoc _ _ fs _ _ _ _) = fs
224+ getFunDocs (NamedInstanceDoc _ fd) = [fd]
225+ getFunDocs (ModDoc _ _) = []
223 types (FD _ _ args t _) = t:(map second args)
226 types (FD _ _ args t _) = t:(map second args)
224 second (_, x, _, _) = x
227 second (_, x, _, _) = x
225
228
@@ -609,6 +612,8 @@ createOtherDoc ist (DataDoc fd@(FD n docstring args _ _) fds) = do
609 H.dt $ toHtml $ show name
612 H.dt $ toHtml $ show name
610 H.dd $ Docstrings.renderHtml docstring
613 H.dd $ Docstrings.renderHtml docstring
611
614
615+createOtherDoc ist (NamedInstanceDoc _ fd) = createFunDoc ist fd
616+
612createOtherDoc ist (ModDoc _ docstring) = do
617createOtherDoc ist (ModDoc _ docstring) = do
613 Docstrings.renderHtml docstring
618 Docstrings.renderHtml docstring
614
619