git.iko.soy/Idris-dev
on master help sign in
Library now builds with "--total"
commit71a3efae2bd8815bc399839dec9d84e43a7d4c9b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 28 Oct 2012, 23:50 (14 years ago) parent9affb75
5 files changed+14−7
compare with master
unifiedsplit
lib/Network/Cgi.idr+5−2 lib/Prelude/Strings.idr+6−3 lib/System.idr+1 lib/base.ipkg+1−1 src/Idris/Coverage.hs+1−1
lib/Network/Cgi.idr+5−2
@@ -98,10 +98,13 @@ getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)
9898
9999getContent : Int -> IO String
100100getContent x = getC x "" where
101+ %assert_total
101102 getC : Int -> String -> IO String
102103 getC 0 acc = return $ reverse acc
103− getC n acc = do x <- getChar
104− getC (n-1) (strCons x acc)
104+ getC n acc = if (n > 0)
105+ then do x' <- getChar
106+ getC (n-1) (strCons x' acc)
107+ else (return "")
105108
106109abstract
107110runCGI : CGI a -> IO a
lib/Prelude/Strings.idr+6−3
@@ -11,14 +11,17 @@ data StrM : String -> Set where
1111 StrNil : StrM ""
1212 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)
1313
14+%assert_total
1415strHead' : (x : String) -> so (not (x == "")) -> Char
1516strHead' x p = prim__strHead x
1617
18+%assert_total
1719strTail' : (x : String) -> so (not (x == "")) -> String
1820strTail' x p = prim__strTail x
1921
2022-- we need the 'believe_me' because the operations are primitives
2123
24+%assert_total
2225strM : (x : String) -> StrM x
2326strM x with (choose (not (x == "")))
2427 strM x | (Left p) = believe_me $ StrCons (strHead' x p) (strTail' x p)
@@ -71,11 +74,12 @@ words' s = case dropWhile isSpace s of
7174words : String -> List String
7275words s = map pack $ words' $ unpack s
7376
77+partial
7478foldr1 : (a -> a -> a) -> List a -> a
7579foldr1 f [x] = x
7680foldr1 f (x::xs) = f x (foldr1 f xs)
7781
78−
82+%assert_total -- due to foldr1, but used safely
7983unwords' : List (List Char) -> List Char
8084unwords' [] = []
8185unwords' ws = (foldr1 addSpace ws)
@@ -83,7 +87,6 @@ unwords' ws = (foldr1 addSpace ws)
8387 addSpace : List Char -> List Char -> List Char
8488 addSpace w s = w ++ (' ' :: s)
8589
86−
87−unwords : List String -> String
90+unwords : List String -> String
8891unwords = pack . unwords' . map unpack
8992
lib/System.idr+1
@@ -2,6 +2,7 @@ module System
22
33import Prelude
44
5+%default partial
56%access public
67
78getArgs : IO (List String)
lib/base.ipkg+1−1
@@ -1,6 +1,6 @@
11package base
22
3−opts = "--noprelude"
3+opts = "--noprelude --total"
44modules = Builtins, Prelude, IO, System,
55
66 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
src/Idris/Coverage.hs+1−1
@@ -512,7 +512,7 @@ mkMultiPaths ist path [] = [reverse path]
512512mkMultiPaths ist path cg
513513 = concat (map extend cg)
514514 where extend (nextf, args)
515− | (nextf, args) `elem` path = [ (nextf, args) : path ]
515+ | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
516516 | otherwise
517517 = case lookupCtxt Nothing nextf (idris_callgraph ist) of
518518 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)