git.iko.soy/Idris-dev
on 4e4b7df help sign in
Idris-dev/libs/base/Data/String.idr
111 lines 3.9 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 x xs) | (StrCons x xs) =
27 if (x == '+')
28 then map fromInteger (parseNumWithoutSign (unpack xs) 0)
29 else map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0')))
32||| Convert a number string to a Num.
33|||
34||| ```idris example
35||| parseInteger " 123"
36||| ```
37||| ```idris example
38||| parseInteger {a=Int} " -123"
39||| ```
40parseInteger : (Num a, Neg a) => String -> Maybe a
41parseInteger s = parseIntTrimmed (trim s)
42 where
43 parseIntTrimmed s with (strM s)
44 parseIntTrimmed "" | StrNil = Nothing
45 parseIntTrimmed (strCons x xs) | (StrCons x xs) =
46 if (x == '-')
47 then map (\y => negate (fromInteger y)) (parseNumWithoutSign (unpack xs) 0)
48 else if (x == '+')
49 then map fromInteger (parseNumWithoutSign (unpack xs) (cast {from=Int} 0))
50 else map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0')))
53||| Convert a number string to a Double.
54|||
55||| ```idris example
56||| parseDouble "+123.123e-2"
57||| ```
58||| ```idris example
59||| parseDouble {a=Int} " -123.123E+2"
60||| ```
61||| ```idris example
62||| parseDouble {a=Int} " +123.123"
63||| ```
64parseDouble : String -> Maybe Double
65parseDouble = mkDouble . wfe . trim
66 where
67 mkDouble (Just (w, f, e)) = let ex = intPow 10 e in
68 Just $ (w * ex + f * ex)
69 mkDouble Nothing = Nothing
71 %assert_total
72 intPow : Integer -> Integer -> Double
73 intPow base exp = if exp > 0 then (num base exp) else 1 / (num base exp)
74 where
75 num base 0 = 1
76 num base e = if e < 0
77 then cast base * num base (e + 1)
78 else cast base * num base (e - 1)
80 wfe : String -> Maybe (Double, Double, Integer)
81 wfe cs = case split (== '.') cs of
82 (wholeAndExp :: []) =>
83 case split (\c => c == 'e' || c == 'E') wholeAndExp of
84 (whole::exp::[]) =>
85 do
86 w <- cast <$> parseInteger whole
87 e <- parseInteger exp
88 return (w, 0, e)
89 (whole::[]) =>
90 do
91 w <- cast <$> parseInteger whole
92 return (w, 0, 0)
93 _ => Nothing
94 (whole::fracAndExp::[]) =>
95 case split (\c => c == 'e' || c == 'E') fracAndExp of
96 (""::exp::[]) => Nothing
97 (frac::exp::[]) =>
98 do
99 w <- cast <$> parseInteger whole
100 f <- (/ (pow 10 (length frac))) <$>
101 (cast <$> parseNumWithoutSign (unpack frac) 0)
102 e <- parseInteger exp
103 return (w, if w < 0 then (-f) else f, e)
104 (frac::[]) =>
105 do
106 w <- cast <$> parseInteger whole
107 f <- (/ (pow 10 (length frac))) <$>
108 (cast <$> parseNumWithoutSign (unpack frac) 0)
109 return (w, if w < 0 then (-f) else f, 0)
110 _ => Nothing
111 _ => Nothing