71a3efa · Idris-dev · git.iko.soy

lib/Network/Cgi.idr+5−2

compare with master

unifiedsplit

@@ -98,10 +98,13 @@ getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)

98

99getContent : Int -> IO String

100getContent x = getC x "" where

101+ %assert_total

101 getC : Int -> String -> IO String

102 getC : Int -> String -> IO String

102 getC 0 acc = return $ reverse acc

103 getC 0 acc = return $ reverse acc

104+ getC n acc = if (n > 0)

103− getC n acc = do x <- getChar

105+ then do x' <- getChar

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

106+ getC (n-1) (strCons x' acc)

107+ else (return "")

105

108

106abstract

109abstract

107runCGI : CGI a -> IO a

110runCGI : CGI a -> IO a

lib/Prelude/Strings.idr+6−3

@@ -11,14 +11,17 @@ data StrM : String -> Set where

11 StrNil : StrM ""

12 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)

13

14+%assert_total

14strHead' : (x : String) -> so (not (x == "")) -> Char

15strHead' : (x : String) -> so (not (x == "")) -> Char

15strHead' x p = prim__strHead x

16strHead' x p = prim__strHead x

16

17

18+%assert_total

17strTail' : (x : String) -> so (not (x == "")) -> String

19strTail' : (x : String) -> so (not (x == "")) -> String

18strTail' x p = prim__strTail x

20strTail' x p = prim__strTail x

19

21

20-- we need the 'believe_me' because the operations are primitives

22-- we need the 'believe_me' because the operations are primitives

21

23

24+%assert_total

22strM : (x : String) -> StrM x

25strM : (x : String) -> StrM x

23strM x with (choose (not (x == "")))

26strM x with (choose (not (x == "")))

24 strM x | (Left p) = believe_me $ StrCons (strHead' x p) (strTail' x p)

27 strM x | (Left p) = believe_me $ StrCons (strHead' x p) (strTail' x p)

@@ -71,11 +74,12 @@ words' s = case dropWhile isSpace s of

71words : String -> List String

74words : String -> List String

72words s = map pack $ words' $ unpack s

75words s = map pack $ words' $ unpack s

73

76

77+partial

74foldr1 : (a -> a -> a) -> List a -> a

78foldr1 : (a -> a -> a) -> List a -> a

75foldr1 f [x] = x

79foldr1 f [x] = x

76foldr1 f (x::xs) = f x (foldr1 f xs)

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

77

81

78−

82+%assert_total -- due to foldr1, but used safely

79unwords' : List (List Char) -> List Char

83unwords' : List (List Char) -> List Char

80unwords' [] = []

84unwords' [] = []

81unwords' ws = (foldr1 addSpace ws)

85unwords' ws = (foldr1 addSpace ws)

@@ -83,7 +87,6 @@ unwords' ws = (foldr1 addSpace ws)

83 addSpace : List Char -> List Char -> List Char

87 addSpace : List Char -> List Char -> List Char

84 addSpace w s = w ++ (' ' :: s)

88 addSpace w s = w ++ (' ' :: s)

85

89

86−

87−unwords : List String -> String

90+unwords : List String -> String

88unwords = pack . unwords' . map unpack

91unwords = pack . unwords' . map unpack

89

92

lib/System.idr+1

@@ -2,6 +2,7 @@ module System

2

3import Prelude

4

5+%default partial

5%access public

6%access public

6

7

7getArgs : IO (List String)

8getArgs : IO (List String)

lib/base.ipkg+1−1

@@ -1,6 +1,6 @@

1package base

2

3−opts = "--noprelude"

3+opts = "--noprelude --total"

4modules = Builtins, Prelude, IO, System,

5

6 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,

src/Idris/Coverage.hs+1−1

@@ -512,7 +512,7 @@ mkMultiPaths ist path [] = [reverse path]

512mkMultiPaths ist path cg

513 = concat (map extend cg)

514 where extend (nextf, args)

515− | (nextf, args) `elem` path = [ (nextf, args) : path ]

515+ | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]

516 | otherwise

517 = case lookupCtxt Nothing nextf (idris_callgraph ist) of

518 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)