15524a8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #13 from dpmulligan/master

15524a8Edwin Brady15 years ago

lib/prelude/list.idr+114−43

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

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

107(++) [] right = right

108(++) [] right = right

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

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

109

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+

145+--------------------------------------------------------------------------------

146+-- Zips and unzips

147+--------------------------------------------------------------------------------

148+

149+zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->

150+ (length l = length r) -> List c

151+zipWith f [] [] p = []

152+zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)

153+

154+zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->

155+ (z : List c) -> (length x = length y) -> (length y = length z) -> List d

156+zipWith3 f [] [] [] p q = []

157+zipWith3 f (x::xs) (y::ys) (z::zs) p q =

158+ f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')

159+

160+zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)

161+zip = zipWith (\x => \y => (x, y))

162+

163+zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->

164+ (length y = length z) -> List (a, b, c)

165+zip3 = zipWith3 (\x => \y => \z => (x, y, z))

166+

167+unzip : List (a, b) -> (List a, List b)

168+unzip [] = ([], [])

169+unzip ((l, r)::xs) with (unzip xs)

170+ | (lefts, rights) = (l::lefts, r::rights)

171+

172+unzip3 : List (a, b, c) -> (List a, List b, List c)

173+unzip3 [] = ([], [], [])

174+unzip3 ((l, c, r)::xs) with (unzip3 xs)

175+ | (lefts, centres, rights) = (l::lefts, c::centres, r::rights)

176+

110--------------------------------------------------------------------------------

177--------------------------------------------------------------------------------

111-- Maps

178-- Maps

112--------------------------------------------------------------------------------

179--------------------------------------------------------------------------------

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

138-- Special folds

205-- Special folds

139--------------------------------------------------------------------------------

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

140

207

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

209+mconcat = foldr (<+>) neutral

210+

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

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

142−concat = foldr (++) []

212+concat [] = []

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

143

214

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

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

145concatMap f [] = []

216concatMap f [] = []

@@ -403,31 +474,33 @@ catMaybes (x::xs) =

403 Just j => j :: catMaybes xs

474 Just j => j :: catMaybes xs

404

475

405--------------------------------------------------------------------------------

476--------------------------------------------------------------------------------

406−-- Instances

477+-- Properties

407--------------------------------------------------------------------------------

478--------------------------------------------------------------------------------

408

479

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

480+-- append

410− (==) [] [] = True

481+appendNilRightNeutral : (l : List a) ->

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

482+ l ++ [] = l

412− if a == b

483+appendNilRightNeutral [] = refl

413− then restA == restB

484+appendNilRightNeutral (x::xs) =

414− else False

485+ let inductiveHypothesis = appendNilRightNeutral xs in

415− (==) _ _ = False

486+ ?appendNilRightNeutralStepCase

416−

417

487

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

488+appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->

419− compare [] [] = EQ

489+ l ++ (c ++ r) = (l ++ c) ++ r

420− compare [] _ = LT

490+appendAssociative [] c r = refl

421− compare _ [] = GT

491+appendAssociative (x::xs) c r =

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

492+ let inductiveHypothesis = appendAssociative xs c r in

423− if a /= b

493+ ?appendAssociativeStepCase

424− then compare a b

425− else compare restA restB

426

494

427−--------------------------------------------------------------------------------

495+-- length

428−-- Properties

496+lengthAppend : (left : List a) -> (right : List a) ->

429−--------------------------------------------------------------------------------

497+ length (left ++ right) = length left + length right

498+lengthAppend [] right = refl

499+lengthAppend (x::xs) right =

500+ let inductiveHypothesis = lengthAppend xs right in

501+ ?lengthAppendStepCase

430

502

503+-- map

431mapPreservesLength : (f : a -> b) -> (l : List a) ->

504mapPreservesLength : (f : a -> b) -> (l : List a) ->

432 length (map f l) = length l

505 length (map f l) = length l

433mapPreservesLength f [] = refl

506mapPreservesLength f [] = refl

@@ -449,20 +522,7 @@ mapFusion f g (x::xs) =

449 let inductiveHypothesis = mapFusion f g xs in

522 let inductiveHypothesis = mapFusion f g xs in

450 ?mapFusionStepCase

523 ?mapFusionStepCase

451

524

452−appendNilRightNeutral : (l : List a) ->

525+-- hasAny

453− l ++ [] = l

454−appendNilRightNeutral [] = refl

455−appendNilRightNeutral (x::xs) =

456− let inductiveHypothesis = appendNilRightNeutral xs in

457− ?appendNilRightNeutralStepCase

458−

459−appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->

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

461−appendAssociative [] c r = refl

462−appendAssociative (x::xs) c r =

463− let inductiveHypothesis = appendAssociative xs c r in

464− ?appendAssociativeStepCase

465−

466hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->

526hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->

467 hasAnyBy p [] l = False

527 hasAnyBy p [] l = False

468hasAnyByNilFalse p [] = refl

528hasAnyByNilFalse p [] = refl

@@ -470,16 +530,9 @@ hasAnyByNilFalse p (x::xs) =

470 let inductiveHypothesis = hasAnyByNilFalse p xs in

530 let inductiveHypothesis = hasAnyByNilFalse p xs in

471 ?hasAnyByNilFalseStepCase

531 ?hasAnyByNilFalseStepCase

472

532

473−lengthAppend : (left : List a) -> (right : List a) ->

474− length (left ++ right) = length left + length right

475−lengthAppend [] right = refl

476−lengthAppend (x::xs) right =

477− let inductiveHypothesis = lengthAppend xs right in

478− ?lengthAppendStepCase

479−

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

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

481hasAnyNilFalse l = ?hasAnyNilFalseBody

534hasAnyNilFalse l = ?hasAnyNilFalseBody

482−

535+

483--------------------------------------------------------------------------------

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

484-- Proofs

537-- Proofs

485--------------------------------------------------------------------------------

538--------------------------------------------------------------------------------

@@ -542,3 +595,21 @@ mapPreservesLengthStepCase = proof {

542 trivial;

595 trivial;

543}

596}

544

597

598+zipWithTailProof = proof {

599+ intros;

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

601+ trivial;

602+}

603+

604+zipWith3TailProof = proof {

605+ intros;

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

607+ trivial;

608+}

609+

610+zipWith3TailProof' = proof {

611+ intros;

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

613+ trivial;

614+}

615+

lib/prelude/vect.idr+25−2

@@ -36,6 +36,21 @@ index (fS k) (x::xs) = index k xs

36index fO [] impossible

37index (fS _) [] impossible

39+--------------------------------------------------------------------------------

40+-- Subvectors

41+--------------------------------------------------------------------------------

42+

43+take : Fin n -> Vect a n -> (p ** Vect a p)

44+take fO xs = (_ ** [])

45+take (fS k) [] impossible

46+take (fS k) (x::xs) with (take k xs)

47+ | (_ ** tail) = (_ ** x::tail)

48+

49+drop : Fin n -> Vect a n -> (p ** Vect a p)

50+drop fO xs = (_ ** xs)

51+drop (fS k) [] impossible

52+drop (fS k) (x::xs) = drop k xs

53+

39--------------------------------------------------------------------------------

54--------------------------------------------------------------------------------

40-- Conversions to and from list

55-- Conversions to and from list

41--------------------------------------------------------------------------------

56--------------------------------------------------------------------------------

@@ -64,6 +79,16 @@ total map : (a -> b) -> Vect a n -> Vect b n

64map f [] = []

79map f [] = []

65map f (x::xs) = f x :: map f xs

80map f (x::xs) = f x :: map f xs

82+-- XXX: causes Idris to enter an infinite loop when type checking in the REPL

83+--mapMaybe : (a -> Maybe b) -> Vect a n -> (p ** Vect b p)

84+--mapMaybe f [] = (_ ** [])

85+--mapMaybe f (x::xs) = mapMaybe' (f x)

86+-- XXX: working around the type restrictions on case statements

87+-- where

88+-- mapMaybe' : (Maybe b) -> (n ** Vect b n) -> (p ** Vect b p)

89+-- mapMaybe' Nothing (n ** tail) = (n ** tail)

90+-- mapMaybe' (Just j) (n ** tail) = (S n ** j::tail)

91+

67--------------------------------------------------------------------------------

92--------------------------------------------------------------------------------

68-- Folds

93-- Folds

69--------------------------------------------------------------------------------

94--------------------------------------------------------------------------------

@@ -217,8 +242,6 @@ nub = nubBy (==)

217-- Splitting and breaking lists

242-- Splitting and breaking lists

218--------------------------------------------------------------------------------

243--------------------------------------------------------------------------------

219

244

220−-- XXX: todo

221−

222--------------------------------------------------------------------------------

245--------------------------------------------------------------------------------

223-- Predicates

246-- Predicates

224--------------------------------------------------------------------------------

247--------------------------------------------------------------------------------