git.iko.soy/Idris-dev
on master help sign in
removed unnecessary casts, style fixes
c2a473aSaurabh Rawat
libs/base/Data/String.idr+35−31
compare with master
unifiedsplit
@@ -4,46 +4,50 @@ module Data.String
4|||
4|||
5||| ```idris example
5||| ```idris example
6||| parsePositive "123"
6||| parsePositive "123"
7+||| ```idris example
7||| parsePositive {a=Int} " +123"
8||| parsePositive {a=Int} " +123"
8||| ```
9||| ```
9parsePositive : Num a => String -> Maybe a
10parsePositive : Num a => String -> Maybe a
10−parsePositive s = parsePosTrimmed (trim s) where
11+parsePositive s = parsePosTrimmed (trim s)
12+ where
11− parsePosTrimmed s with (strM s)
13+ parsePosTrimmed s with (strM s)
12− parsePosTrimmed "" | StrNil = Nothing
14+ parsePosTrimmed "" | StrNil = Nothing
13− parsePosTrimmed (strCons x xs) | (StrCons x xs) =
15+ parsePosTrimmed (strCons x xs) | (StrCons x xs) =
14− if (x == '+')
16+ if (x == '+')
15− then map fromInteger (parsePosAux (unpack xs) (cast {from=Int} 0))
17+ then map fromInteger (parsePosAux (unpack xs) 0)
16− else map fromInteger (parsePosAux (unpack xs) (cast (ord x - ord '0')))
18+ else map fromInteger (parsePosAux (unpack xs) (cast (ord x - ord '0')))
17− where
19+ where
18− parsePosAux : (List Char) -> Integer -> Maybe Integer
20+ parsePosAux : List Char -> Integer -> Maybe Integer
19− parsePosAux [] acc = Just acc
21+ parsePosAux [] acc = Just acc
20− parsePosAux (c :: cs) acc =
22+ parsePosAux (c :: cs) acc =
21− if (c >= '0' && c <= '9')
23+ if (c >= '0' && c <= '9')
22− then parsePosAux cs ((acc * (cast {from=Int} 10)) + (cast ((ord c) - (ord '0'))))
24+ then parsePosAux cs ((acc * 10) + (cast ((ord c) - (ord '0'))))
23− else Nothing
25+ else Nothing
24
26
25
27
26||| Convert a number string to a Num.
28||| Convert a number string to a Num.
27|||
29|||
28||| ```idris example
30||| ```idris example
29||| parseInteger " 123"
31||| parseInteger " 123"
32+||| ```
33+||| ```idris example
30||| parseInteger {a=Int} " -123"
34||| parseInteger {a=Int} " -123"
31||| ```
35||| ```
32parseInteger : (Num a, Neg a) => String -> Maybe a
36parseInteger : (Num a, Neg a) => String -> Maybe a
33−parseInteger s = parseIntTrimmed (trim s) where
37+parseInteger s = parseIntTrimmed (trim s)
38+ where
34− parseIntTrimmed s with (strM s)
39+ parseIntTrimmed s with (strM s)
35− parseIntTrimmed "" | StrNil = Nothing
40+ parseIntTrimmed "" | StrNil = Nothing
36− parseIntTrimmed (strCons x xs) | (StrCons x xs) =
41+ parseIntTrimmed (strCons x xs) | (StrCons x xs) =
37− if (x == '-')
42+ if (x == '-')
38− then map (\y => negate (fromInteger y)) (parseIntegerAux (unpack xs) (cast {from=Int} 0))
43+ then map (\y => negate (fromInteger y)) (parseIntegerAux (unpack xs) 0)
39− else if (x == '+')
44+ else if (x == '+')
40− then map fromInteger (parseIntegerAux (unpack xs) (cast {from=Int} 0))
45+ then map fromInteger (parseIntegerAux (unpack xs) (cast {from=Int} 0))
41− else map fromInteger (parseIntegerAux (unpack xs) (cast (ord x - ord '0')))
46+ else map fromInteger (parseIntegerAux (unpack xs) (cast (ord x - ord '0')))
42− where
47+ where
43− parseIntegerAux : (List Char) -> Integer -> Maybe Integer
48+ parseIntegerAux : List Char -> Integer -> Maybe Integer
44− parseIntegerAux [] acc = Just acc
49+ parseIntegerAux [] acc = Just acc
45− parseIntegerAux (c :: cs) acc =
50+ parseIntegerAux (c :: cs) acc =
46− if (c >= '0' && c <= '9')
51+ if (c >= '0' && c <= '9')
47− then parseIntegerAux cs ((acc * (cast {from=Int} 10)) + (cast ((ord c) - (ord '0'))))
52+ then parseIntegerAux cs ((acc * 10) + (cast ((ord c) - (ord '0'))))
48− else Nothing
53+ else Nothing
49−