git.iko.soy/Idris-dev
on master help sign in
Use toNat to avoid %assert_total when negative Int is treated the same as 0.
0ea9704Stephen Drodge
libs/base/Network/Cgi.idr+7−8
compare with master
unifiedsplit
@@ -2,6 +2,8 @@ module Network.Cgi
2
2
3import System
3import System
4
4
5+%default total
6+
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