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