git.iko.soy/Idris-dev
on master help sign in
Remove some of the more easily avoided %assert_totals
a17d8d5Stephen Drodge
libs/base/Data/BoundedList.idr−1
compare with master
unifiedsplit
@@ -77,7 +77,6 @@ map f (x :: xs) = f x :: map f xs
77-- Misc
77-- Misc
78--------------------------------------------------------------------------------
78--------------------------------------------------------------------------------
79
79
80−%assert_total -- not sure why this isn't accepted - clearly decreasing on n
81pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n
80pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n
82pad {n=Z} [] _ = []
81pad {n=Z} [] _ = []
83pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)
82pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)
libs/prelude/Prelude/List.idr+20−30
@@ -35,28 +35,26 @@ isCons (x::xs) = True
35-- Indexing into lists
35-- Indexing into lists
36--------------------------------------------------------------------------------
36--------------------------------------------------------------------------------
37
37
38−%assert_total
39head : (l : List a) -> (isCons l = True) -> a
38head : (l : List a) -> (isCons l = True) -> a
39+head [] refl impossible
40−head (x::xs) p = x
40+head (x::xs) p = x
41
41
42head' : (l : List a) -> Maybe a
42head' : (l : List a) -> Maybe a
43head' [] = Nothing
43head' [] = Nothing
44head' (x::xs) = Just x
44head' (x::xs) = Just x
45
45
46−%assert_total
47tail : (l : List a) -> (isCons l = True) -> List a
46tail : (l : List a) -> (isCons l = True) -> List a
47+tail [] refl impossible
48−tail (x::xs) p = xs
48+tail (x::xs) p = xs
49
49
50tail' : (l : List a) -> Maybe (List a)
50tail' : (l : List a) -> Maybe (List a)
51tail' [] = Nothing
51tail' [] = Nothing
52tail' (x::xs) = Just xs
52tail' (x::xs) = Just xs
53
53
54−%assert_total
55last : (l : List a) -> (isCons l = True) -> a
54last : (l : List a) -> (isCons l = True) -> a
56−last (x::xs) p =
55+last [] refl impossible
57− case xs of
56+last [x] p = x
58− [] => x
59− y::ys => last (y::ys) ?lastProof
57+last (x::y::ys) p = last (y::ys) refl
60
58
61last' : (l : List a) -> Maybe a
59last' : (l : List a) -> Maybe a
62last' [] = Nothing
60last' [] = Nothing
@@ -65,12 +63,10 @@ last' (x::xs) =
65 [] => Just x
63 [] => Just x
66 y::ys => last' xs
64 y::ys => last' xs
67
65
68−%assert_total
69init : (l : List a) -> (isCons l = True) -> List a
66init : (l : List a) -> (isCons l = True) -> List a
70−init (x::xs) p =
67+init [] refl impossible
71− case xs of
72− [] => []
68+init [x] p = []
73− y::ys => x :: init (y::ys) ?initProof
69+init (x::y::ys) p = x :: init (y::ys) refl
74
70
75init' : (l : List a) -> Maybe (List a)
71init' : (l : List a) -> Maybe (List a)
76init' [] = Nothing
72init' [] = Nothing
@@ -175,17 +171,21 @@ instance Functor List where
175-- Zips and unzips
171-- Zips and unzips
176--------------------------------------------------------------------------------
172--------------------------------------------------------------------------------
177
173
178−%assert_total
179zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->
174zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->
180 (length l = length r) -> List c
175 (length l = length r) -> List c
181−zipWith f [] [] p = []
176+zipWith f [] (y::ys) refl impossible
177+zipWith f (x::xs) [] refl impossible
178+zipWith f [] [] p = []
182−zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)
179+zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)
183
180
184−%assert_total
185zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
181zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
186 (z : List c) -> (length x = length y) -> (length y = length z) -> List d
182 (z : List c) -> (length x = length y) -> (length y = length z) -> List d
187−zipWith3 f [] [] [] refl refl = []
183+zipWith3 f _ [] (z::zs) p refl impossible
184+zipWith3 f _ (y::ys) [] p refl impossible
185+zipWith3 f [] (y::ys) _ refl q impossible
186+zipWith3 f (x::xs) [] _ refl q impossible
187+zipWith3 f [] [] [] p q = []
188−zipWith3 f (x::xs) (y::ys) (z::zs) p q =
188+zipWith3 f (x::xs) (y::ys) (z::zs) p q =
189 f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')
189 f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')
190
190
191zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
191zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
@@ -562,16 +562,6 @@ hasAnyByNilFalseStepCase = proof {
562 trivial;
562 trivial;
563}
563}
564
564
565−initProof = proof {
566− intros;
567− trivial;
568−}
569−
570−lastProof = proof {
571− intros;
572− trivial;
573−}
574−
575appendNilRightNeutralStepCase = proof {
565appendNilRightNeutralStepCase = proof {
576 intros;
566 intros;
577 rewrite inductiveHypothesis;
567 rewrite inductiveHypothesis;