0246f66 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #664 from sjdrodge/assert_total_cleanup

Some %assert_total cleanup

commit0246f667d33f7ecb37756feceded5d7157b9576e authorEdwin Brady <edwin.brady@gmail.com> dateMon 25 Nov 2013, 06:38 (13 years ago) parentc459480 5d71e52

4 files changed+32−59

compare with master

unifiedsplit

libs/base/Data/BoundedList.idr−1 libs/base/Data/Heap.idr+5−20 libs/base/Network/Cgi.idr+7−8 libs/prelude/Prelude/List.idr+20−30

libs/base/Data/BoundedList.idr−1

@@ -77,7 +77,6 @@ map f (x :: xs) = f x :: map f xs

7777-- Misc

7878--------------------------------------------------------------------------------

7979

80−%assert_total -- not sure why this isn't accepted - clearly decreasing on n

8180pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n

8281pad {n=Z} [] _ = []

8382pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)

libs/base/Data/Heap.idr+5−20

@@ -5,6 +5,7 @@

66module Data.Heap

8+%default total

89%access public

910

1011abstract data MaxiphobicHeap : Type -> Type where

@@ -82,12 +83,12 @@ insert e = merge $ singleton e

8283--------------------------------------------------------------------------------

8384

8485findMinimum : (h : MaxiphobicHeap a) -> (isEmpty h = False) -> a

85−findMinimum Empty p = ?findMinimumEmptyAbsurd

86−findMinimum (Node s l e r) p = e

86+findMinimum Empty refl impossible

87+findMinimum (Node s l e r) p = e

8788

8889deleteMinimum : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> MaxiphobicHeap a

89−deleteMinimum Empty p = ?deleteMinimumEmptyAbsurd

90−deleteMinimum (Node s l e r) p = merge l r

90+deleteMinimum Empty refl impossible

91+deleteMinimum (Node s l e r) p = merge l r

9192

9293--------------------------------------------------------------------------------

9394-- Conversions to and from lists (and a derived heap sorting algorithm)

@@ -173,22 +174,6 @@ isEmptySizeZeroNodeAbsurd = proof {

173174 exact p;

174175}

175176

176−findMinimumEmptyAbsurd = proof {

177− intros;

178− refine FalseElim;

179− refine absurdBoolDischarge;

180− rewrite p;

181− trivial;

182−}

183−

184−deleteMinimumEmptyAbsurd = proof {

185− intros;

186− refine FalseElim;

187− refine absurdBoolDischarge;

188− rewrite p;

189− trivial;

190−}

191−

192177--------------------------------------------------------------------------------

193178-- Debug

194179--------------------------------------------------------------------------------

libs/base/Network/Cgi.idr+7−8

@@ -2,6 +2,8 @@ module Network.Cgi

33import System

5+%default total

57public

68Vars : Type

79Vars = List (String, String)

@@ -106,14 +108,11 @@ getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)

106108 | _ = Nothing

107109

108110getContent : Int -> IO String

109−getContent x = getC x "" where

110− %assert_total

111− getC : Int -> String -> IO String

112− getC 0 acc = return $ reverse acc

113− getC n acc = if (n > 0)

114− then do x <- getChar

115− getC (n-1) (strCons x acc)

116− else (return "")

111+getContent x = getC (toNat x) "" where

112+ getC : Nat -> String -> IO String

113+ getC Z acc = return $ reverse acc

114+ getC (S k) acc = do x <- getChar

115+ getC k (strCons x acc)

117116

118117getCgiEnv : String -> IO String

119118getCgiEnv key = do

libs/prelude/Prelude/List.idr+20−30

@@ -35,28 +35,26 @@ isCons (x::xs) = True

3535-- Indexing into lists

3636--------------------------------------------------------------------------------

3737

38−%assert_total

3938head : (l : List a) -> (isCons l = True) -> a

40−head (x::xs) p = x

39+head [] refl impossible

40+head (x::xs) p = x

4141

4242head' : (l : List a) -> Maybe a

4343head' [] = Nothing

4444head' (x::xs) = Just x

4545

46−%assert_total

4746tail : (l : List a) -> (isCons l = True) -> List a

48−tail (x::xs) p = xs

47+tail [] refl impossible

48+tail (x::xs) p = xs

4949

5050tail' : (l : List a) -> Maybe (List a)

5151tail' [] = Nothing

5252tail' (x::xs) = Just xs

5353

54−%assert_total

5554last : (l : List a) -> (isCons l = True) -> a

56−last (x::xs) p =

57− case xs of

58− [] => x

59− y::ys => last (y::ys) ?lastProof

55+last [] refl impossible

56+last [x] p = x

57+last (x::y::ys) p = last (y::ys) refl

6058

6159last' : (l : List a) -> Maybe a

6260last' [] = Nothing

@@ -65,12 +63,10 @@ last' (x::xs) =

6563 [] => Just x

6664 y::ys => last' xs

6765

68−%assert_total

6966init : (l : List a) -> (isCons l = True) -> List a

70−init (x::xs) p =

71− case xs of

72− [] => []

73− y::ys => x :: init (y::ys) ?initProof

67+init [] refl impossible

68+init [x] p = []

69+init (x::y::ys) p = x :: init (y::ys) refl

7470

7571init' : (l : List a) -> Maybe (List a)

7672init' [] = Nothing

@@ -175,17 +171,21 @@ instance Functor List where

175171-- Zips and unzips

176172--------------------------------------------------------------------------------

177173

178−%assert_total

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

180175 (length l = length r) -> List c

181−zipWith f [] [] p = []

182−zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)

176+zipWith f [] (y::ys) refl impossible

177+zipWith f (x::xs) [] refl impossible

178+zipWith f [] [] p = []

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

183180

184−%assert_total

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

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

187−zipWith3 f [] [] [] refl refl = []

188−zipWith3 f (x::xs) (y::ys) (z::zs) p q =

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 =

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

190190

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

@@ -562,16 +562,6 @@ hasAnyByNilFalseStepCase = proof {

562562 trivial;

563563}

564564

565−initProof = proof {

566− intros;

567− trivial;

568−}

569−

570−lastProof = proof {

571− intros;

572− trivial;

573−}

574−

575565appendNilRightNeutralStepCase = proof {

576566 intros;

577567 rewrite inductiveHypothesis;