git.iko.soy/Idris-dev
on bbefa33 help sign in
Idris-dev/libs/base/Data/String.idr
114 lines 4.1 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 if (x >= '0' && x <= '9')
53 then map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0')))
54 else Nothing
57||| Convert a number string to a Double.
58|||
59||| ```idris example
60||| parseDouble "+123.123e-2"
61||| ```
62||| ```idris example
63||| parseDouble {a=Int} " -123.123E+2"
64||| ```
65||| ```idris example
66||| parseDouble {a=Int} " +123.123"
67||| ```
68parseDouble : String -> Maybe Double
69parseDouble = mkDouble . wfe . trim
70 where
71 mkDouble (Just (w, f, e)) = let ex = intPow 10 e in
72 Just $ (w * ex + f * ex)
73 mkDouble Nothing = Nothing
75 intPow : Integer -> Integer -> Double
76 intPow base exp = assert_total $ if exp > 0 then (num base exp) else 1 / (num base exp)
77 where
78 num base 0 = 1
79 num base e = if e < 0
80 then cast base * num base (e + 1)
81 else cast base * num base (e - 1)
83 wfe : String -> Maybe (Double, Double, Integer)
84 wfe cs = case split (== '.') cs of
85 (wholeAndExp :: []) =>
86 case split (\c => c == 'e' || c == 'E') wholeAndExp of
87 (whole::exp::[]) =>
88 do
89 w <- cast <$> parseInteger whole
90 e <- parseInteger exp
91 pure (w, 0, e)
92 (whole::[]) =>
93 do
94 w <- cast <$> parseInteger whole
95 pure (w, 0, 0)
96 _ => Nothing
97 (whole::fracAndExp::[]) =>
98 case split (\c => c == 'e' || c == 'E') fracAndExp of
99 (""::exp::[]) => Nothing
100 (frac::exp::[]) =>
101 do
102 w <- cast <$> parseInteger whole
103 f <- (/ (pow 10 (length frac))) <$>
104 (cast <$> parseNumWithoutSign (unpack frac) 0)
105 e <- parseInteger exp
106 pure (w, if w < 0 then (-f) else f, e)
107 (frac::[]) =>
108 do
109 w <- cast <$> parseInteger whole
110 f <- (/ (pow 10 (length frac))) <$>
111 (cast <$> parseNumWithoutSign (unpack frac) 0)
112 pure (w, if w < 0 then (-f) else f, 0)
113 _ => Nothing
114 _ => Nothing