73e2e7e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of github.com:idris-lang/Idris-dev

73e2e7eEdwin Brady13 years ago

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

78--------------------------------------------------------------------------------

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/base/Data/Heap.idr+5−20

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

6module Data.Heap

8+%default total

8%access public

9%access public

10abstract data MaxiphobicHeap : Type -> Type where

11abstract data MaxiphobicHeap : Type -> Type where

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

82--------------------------------------------------------------------------------

83--------------------------------------------------------------------------------

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

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

85−findMinimum Empty p = ?findMinimumEmptyAbsurd

86+findMinimum Empty refl impossible

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

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

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

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

89−deleteMinimum Empty p = ?deleteMinimumEmptyAbsurd

90+deleteMinimum Empty refl impossible

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

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

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

93--------------------------------------------------------------------------------

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

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

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

173 exact p;

174 exact p;

174}

175}

175

176

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−

192--------------------------------------------------------------------------------

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

193-- Debug

178-- Debug

194--------------------------------------------------------------------------------

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

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

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

3import System

5+%default total

5public

7public

6Vars : Type

8Vars : Type

7Vars = List (String, String)

9Vars = List (String, String)

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

106 | _ = Nothing

108 | _ = Nothing

107

109

108getContent : Int -> IO String

110getContent : Int -> IO String

109−getContent x = getC x "" where

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

110− %assert_total

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

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

112− getC 0 acc = return $ reverse acc

113+ getC Z acc = return $ reverse acc

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

114− then do x <- getChar

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

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

115+ getC k (strCons x acc)

116− else (return "")

117

116

118getCgiEnv : String -> IO String

117getCgiEnv : String -> IO String

119getCgiEnv key = do

118getCgiEnv key = do

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

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

35-- Indexing into lists

36--------------------------------------------------------------------------------

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

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

43head' [] = Nothing

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

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

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

51tail' [] = Nothing

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

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

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

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

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')

190

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

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

562 trivial;

563}

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;

src/Idris/ParseExpr.hs+1

@@ -1,4 +1,5 @@

1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

2+{-# OPTIONS_GHC -O0 #-}

2module Idris.ParseExpr where

3module Idris.ParseExpr where

4import Prelude hiding (pi)

5import Prelude hiding (pi)

src/Idris/Parser.hs+1

@@ -1,4 +1,5 @@

1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

2+{-# OPTIONS_GHC -O0 #-}

2module Idris.Parser(module Idris.Parser,

3module Idris.Parser(module Idris.Parser,

3 module Idris.ParseExpr,

4 module Idris.ParseExpr,

4 module Idris.ParseData,

5 module Idris.ParseData,