24d95b0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added mconcat for concatenating over an arbitrary monoid (replace concat on lists with the generalized version later?)

24d95b0Dominic Mulligan15 years ago

lib/prelude/list.idr+43−38

compare with master

unifiedsplit

@@ -108,6 +108,40 @@ length (x::xs) = 1 + length xs

108(++) [] right = right

109(++) (x::xs) right = x :: (xs ++ right)

110

111+--------------------------------------------------------------------------------

112+-- Instances

113+--------------------------------------------------------------------------------

114+

115+instance (Eq a) => Eq (List a) where

116+ (==) [] [] = True

117+ (==) (x::xs) (y::ys) =

118+ if x == y then

119+ xs == ys

120+ else

121+ False

122+ (==) _ _ = False

123+

124+

125+instance Ord a => Ord (List a) where

126+ compare [] [] = EQ

127+ compare [] _ = LT

128+ compare _ [] = GT

129+ compare (x::xs) (y::ys) =

130+ if x /= y then

131+ compare x y

132+ else

133+ compare xs ys

134+

135+instance Semigroup (List a) where

136+ (<+>) = (++)

137+

138+instance Monoid (List a) where

139+ neutral = []

140+

141+-- XXX: unification failure

142+-- instance VerifiedSemigroup (List a) where

143+-- semigroupOpIsAssociative = appendAssociative

144+

111--------------------------------------------------------------------------------

145--------------------------------------------------------------------------------

112-- Zips and unzips

146-- Zips and unzips

113--------------------------------------------------------------------------------

147--------------------------------------------------------------------------------

@@ -171,8 +205,12 @@ foldr f e (x::xs) = f x (foldr f e xs)

171-- Special folds

205-- Special folds

172--------------------------------------------------------------------------------

206--------------------------------------------------------------------------------

173

207

208+mconcat : Monoid a => List a -> a

209+mconcat = foldr (<+>) neutral

210+

174concat : List (List a) -> List a

211concat : List (List a) -> List a

175−concat = foldr (++) []

212+concat [] = []

213+concat (x::xs) = x ++ concat xs

176

214

177concatMap : (a -> List b) -> List a -> List b

215concatMap : (a -> List b) -> List a -> List b

178concatMap f [] = []

216concatMap f [] = []

@@ -494,40 +532,6 @@ hasAnyByNilFalse p (x::xs) =

494

532

495hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False

533hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False

496hasAnyNilFalse l = ?hasAnyNilFalseBody

534hasAnyNilFalse l = ?hasAnyNilFalseBody

497−

498−--------------------------------------------------------------------------------

499−-- Instances

500−--------------------------------------------------------------------------------

501−

502−instance (Eq a) => Eq (List a) where

503− (==) [] [] = True

504− (==) (x::xs) (y::ys) =

505− if x == y then

506− xs == ys

507− else

508− False

509− (==) _ _ = False

510−

511−

512−instance Ord a => Ord (List a) where

513− compare [] [] = EQ

514− compare [] _ = LT

515− compare _ [] = GT

516− compare (x::xs) (y::ys) =

517− if x /= y then

518− compare x y

519− else

520− compare xs ys

521−

522−instance Semigroup (List a) where

523− (<+>) = (++)

524−

525−instance Monoid (List a) where

526− neutral = []

527−

528−-- XXX: unification failure

529−-- instance VerifiedSemigroup (List a) where

530−-- semigroupOpIsAssociative = appendAssociative

531

535

532--------------------------------------------------------------------------------

536--------------------------------------------------------------------------------

533-- Proofs

537-- Proofs

@@ -591,20 +595,21 @@ mapPreservesLengthStepCase = proof {

591 trivial;

595 trivial;

592}

596}

593

597

594−prelude.list.zipWithTailProof = proof {

598+zipWithTailProof = proof {

595 intros;

599 intros;

596 rewrite (succInjective (length xs) (length ys) p);

600 rewrite (succInjective (length xs) (length ys) p);

597 trivial;

601 trivial;

598}

602}

599

603

600−prelude.list.zipWith3TailProof = proof {

604+zipWith3TailProof = proof {

601 intros;

605 intros;

602 rewrite (succInjective (length xs) (length ys) p);

606 rewrite (succInjective (length xs) (length ys) p);

603 trivial;

607 trivial;

604}

608}

605

609

606−prelude.list.zipWith3TailProof' = proof {

610+zipWith3TailProof' = proof {

607 intros;

611 intros;

608 rewrite (succInjective (length ys) (length zs) q);

612 rewrite (succInjective (length ys) (length zs) q);

609 trivial;

613 trivial;

610}

614}

615+