@@ -1,5 +1,14 @@
11module Data.String
22
3+private
4+parseNumWithoutSign : List Char -> Integer -> Maybe Integer
5+parseNumWithoutSign [] acc = Just acc
6+parseNumWithoutSign (c :: cs) acc =
7+ if (c >= '0' && c <= '9')
8+ then parseNumWithoutSign cs ((acc * 10) + (cast ((ord c) - (ord '0'))))
9+ else Nothing
10+
11+
312||| Convert a positive number string to a Num.
413|||
514||| ```idris example
@@ -15,15 +24,8 @@ parsePositive s = parsePosTrimmed (trim s)
1524 parsePosTrimmed "" | StrNil = Nothing
1625 parsePosTrimmed (strCons x xs) | (StrCons x xs) =
1726 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
27+ then map fromInteger (parseNumWithoutSign (unpack xs) 0)
28+ else map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0')))
2729
2830
2931||| Convert a number string to a Num.
@@ -41,14 +43,68 @@ parseInteger s = parseIntTrimmed (trim s)
4143 parseIntTrimmed "" | StrNil = Nothing
4244 parseIntTrimmed (strCons x xs) | (StrCons x xs) =
4345 if (x == '-')
44− then map (\y => negate (fromInteger y)) (parseIntegerAux (unpack xs) 0)
46+ then map (\y => negate (fromInteger y)) (parseNumWithoutSign (unpack xs) 0)
4547 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
48+ then map fromInteger (parseNumWithoutSign (unpack xs) (cast {from=Int} 0))
49+ else map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0')))
50+
51+
52+||| Convert a number string to a Double.
53+|||
54+||| ```idris example
55+||| parseDouble "+123.123e-2"
56+||| ```
57+||| ```idris example
58+||| parseDouble {a=Int} " -123.123E+2"
59+||| ```
60+||| ```idris example
61+||| parseDouble {a=Int} " +123.123"
62+||| ```
63+parseDouble : String -> Maybe Double
64+parseDouble = mkDouble . wfe . trim
65+ where
66+ mkDouble (Just (w, f, e)) = let ex = intPow 10 e in
67+ Just $ (w * ex + f * ex)
68+ mkDouble Nothing = Nothing
69+
70+ %assert_total
71+ intPow : Integer -> Integer -> Double
72+ intPow base exp = if exp > 0 then (num base exp) else 1 / (num base exp)
73+ where
74+ num base 0 = 1
75+ num base e = if e < 0
76+ then cast base * num base (e + 1)
77+ else cast base * num base (e - 1)
78+
79+ wfe : String -> Maybe (Double, Double, Integer)
80+ wfe cs = case split (== '.') cs of
81+ (wholeAndExp :: []) =>
82+ case split (\c => c == 'e' || c == 'E') wholeAndExp of
83+ (whole::exp::[]) =>
84+ do
85+ w <- cast <$> parseInteger whole
86+ e <- parseInteger exp
87+ return (w, 0, e)
88+ (whole::[]) =>
89+ do
90+ w <- cast <$> parseInteger whole
91+ return (w, 0, 0)
92+ _ => Nothing
93+ (whole::fracAndExp::[]) =>
94+ case split (\c => c == 'e' || c == 'E') fracAndExp of
95+ (""::exp::[]) => Nothing
96+ (frac::exp::[]) =>
97+ do
98+ w <- cast <$> parseInteger whole
99+ f <- (/ (pow 10 (length frac))) <$>
100+ (cast <$> parseNumWithoutSign (unpack frac) 0)
101+ e <- parseInteger exp
102+ return (w, if w < 0 then (-f) else f, e)
103+ (frac::[]) =>
104+ do
105+ w <- cast <$> parseInteger whole
106+ f <- (/ (pow 10 (length frac))) <$>
107+ (cast <$> parseNumWithoutSign (unpack frac) 0)
108+ return (w, if w < 0 then (-f) else f, 0)
109+ _ => Nothing
110+ _ => Nothing