ac05da7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added Semigroup and Monoid instances (non-verified) to list module.

ac05da7Dominic Mulligan15 years ago

lib/prelude/list.idr+36−24

compare with master

unifiedsplit

@@ -2,6 +2,7 @@ module prelude.list

3import builtins

5+import prelude.algebra

5import prelude.maybe

6import prelude.maybe

6import prelude.nat

7import prelude.nat

@@ -434,28 +435,6 @@ catMaybes (x::xs) =

434 Nothing => catMaybes xs

435 Nothing => catMaybes xs

435 Just j => j :: catMaybes xs

436 Just j => j :: catMaybes xs

436

437

437−--------------------------------------------------------------------------------

438−-- Instances

439−--------------------------------------------------------------------------------

440−

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

442− (==) [] [] = True

443− (==) (a::restA) (b::restB) =

444− if a == b

445− then restA == restB

446− else False

447− (==) _ _ = False

448−

449−

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

451− compare [] [] = EQ

452− compare [] _ = LT

453− compare _ [] = GT

454− compare (a::restA) (b::restB) =

455− if a /= b

456− then compare a b

457− else compare restA restB

458−

459--------------------------------------------------------------------------------

438--------------------------------------------------------------------------------

460-- Properties

439-- Properties

461--------------------------------------------------------------------------------

440--------------------------------------------------------------------------------

@@ -469,7 +448,7 @@ appendNilRightNeutral (x::xs) =

469 ?appendNilRightNeutralStepCase

448 ?appendNilRightNeutralStepCase

470

449

471appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->

450appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->

472− (l ++ c) ++ r = l ++ (c ++ r)

451+ l ++ (c ++ r) = (l ++ c) ++ r

473appendAssociative [] c r = refl

452appendAssociative [] c r = refl

474appendAssociative (x::xs) c r =

453appendAssociative (x::xs) c r =

475 let inductiveHypothesis = appendAssociative xs c r in

454 let inductiveHypothesis = appendAssociative xs c r in

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

515

494

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

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

517hasAnyNilFalse l = ?hasAnyNilFalseBody

496hasAnyNilFalse 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

518

531

519--------------------------------------------------------------------------------

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

520-- Proofs

533-- Proofs

@@ -595,4 +608,3 @@ prelude.list.zipWith3TailProof' = proof {

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

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

596 trivial;

609 trivial;

597}

610}

598−