git.iko.soy/Idris-dev
on 181dddb help sign in
Idris-dev/libs/base/Data/String.idr
112 lines 4.0 kB history raw
1module Data.String
2%access public export
4private
5parseNumWithoutSign : List Char -> Integer -> Maybe Integer
6parseNumWithoutSign [] acc = Just acc
7parseNumWithoutSign (c :: cs) acc =
8 if (c >= '0' && c <= '9')
9 then parseNumWithoutSign cs ((acc * 10) + (cast ((ord c) - (ord '0'))))
10 else Nothing
13||| Convert a positive number string to a Num.
14|||
15||| ```idris example
16||| parsePositive "123"
17||| ```
18||| ```idris example
19||| parsePositive {a=Int} " +123"
20||| ```
21parsePositive : Num a => String -> Maybe a
22parsePositive s = parsePosTrimmed (trim s)
23 where
24 parsePosTrimmed s with (strM s)
25 parsePosTrimmed "" | StrNil = Nothing
26 parsePosTrimmed (strCons '+' xs) | (StrCons '+' xs) =
27 map fromInteger (parseNumWithoutSign (unpack xs) 0)
28 parsePosTrimmed (strCons x xs) | (StrCons x xs) =
29 if (x >= '0' && x <= '9')
30 then map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0')))
31 else Nothing
34||| Convert a number string to a Num.
35|||
36||| ```idris example
37||| parseInteger " 123"
38||| ```
39||| ```idris example
40||| parseInteger {a=Int} " -123"
41||| ```
42parseInteger : (Num a, Neg a) => String -> Maybe a
43parseInteger s = parseIntTrimmed (trim s)
44 where
45 parseIntTrimmed s with (strM s)
46 parseIntTrimmed "" | StrNil = Nothing
47 parseIntTrimmed (strCons x xs) | (StrCons x xs) =
48 if (x == '-')
49 then map (\y => negate (fromInteger y)) (parseNumWithoutSign (unpack xs) 0)
50 else if (x == '+')
51 then map fromInteger (parseNumWithoutSign (unpack xs) (cast {from=Int} 0))
52 else map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0')))
55||| Convert a number string to a Double.
56|||
57||| ```idris example
58||| parseDouble "+123.123e-2"
59||| ```
60||| ```idris example
61||| parseDouble {a=Int} " -123.123E+2"
62||| ```
63||| ```idris example
64||| parseDouble {a=Int} " +123.123"
65||| ```
66parseDouble : String -> Maybe Double
67parseDouble = mkDouble . wfe . trim
68 where
69 mkDouble (Just (w, f, e)) = let ex = intPow 10 e in
70 Just $ (w * ex + f * ex)
71 mkDouble Nothing = Nothing
73 intPow : Integer -> Integer -> Double
74 intPow base exp = assert_total $ if exp > 0 then (num base exp) else 1 / (num base exp)
75 where
76 num base 0 = 1
77 num base e = if e < 0
78 then cast base * num base (e + 1)
79 else cast base * num base (e - 1)
81 wfe : String -> Maybe (Double, Double, Integer)
82 wfe cs = case split (== '.') cs of
83 (wholeAndExp :: []) =>
84 case split (\c => c == 'e' || c == 'E') wholeAndExp of
85 (whole::exp::[]) =>
86 do
87 w <- cast <$> parseInteger whole
88 e <- parseInteger exp
89 return (w, 0, e)
90 (whole::[]) =>
91 do
92 w <- cast <$> parseInteger whole
93 return (w, 0, 0)
94 _ => Nothing
95 (whole::fracAndExp::[]) =>
96 case split (\c => c == 'e' || c == 'E') fracAndExp of
97 (""::exp::[]) => Nothing
98 (frac::exp::[]) =>
99 do
100 w <- cast <$> parseInteger whole
101 f <- (/ (pow 10 (length frac))) <$>
102 (cast <$> parseNumWithoutSign (unpack frac) 0)
103 e <- parseInteger exp
104 return (w, if w < 0 then (-f) else f, e)
105 (frac::[]) =>
106 do
107 w <- cast <$> parseInteger whole
108 f <- (/ (pow 10 (length frac))) <$>
109 (cast <$> parseNumWithoutSign (unpack frac) 0)
110 return (w, if w < 0 then (-f) else f, 0)
111 _ => Nothing
112 _ => Nothing