git.iko.soy/Idris-dev
on master help sign in
parsing negative and non negative numbers
01a11c7Saurabh Rawat
libs/base/Data/String.idrnew file+38
compare with master
unifiedsplit
@@ -0,0 +1,38 @@
1+module Data.String
2+
3+||| Convert a positive number string to a Num.
4+|||
5+||| ```idris example
6+||| parsePositive "123"
7+||| parsePositive {a=Int} " +123"
8+||| ```
9+parsePositive : Num a => String -> Maybe a
10+parsePositive s = parsePosTrimmed (trim s) where
11+ parsePosTrimmed s with (strM s)
12+ parsePosTrimmed "" | StrNil = Nothing
13+ parsePosTrimmed (strCons x xs) | (StrCons x xs) = if (x == '+') then map fromInteger (parsePosAux (unpack xs) 0)
14+ else map fromInteger (parsePosAux (unpack xs) (ord x - ord '0')) where
15+ parsePosAux : (List Char) -> Int -> Maybe Integer
16+ parsePosAux [] acc = Just (cast acc)
17+ parsePosAux (c :: cs) acc = if (c >= '0' && c <= '9') then parsePosAux cs ((acc * 10) + (ord c) - (ord '0'))
18+ else Nothing
19+
20+
21+||| Convert a number string to a Num.
22+|||
23+||| ```idris example
24+||| parseInteger " 123"
25+||| parseInteger {a=Int} " -123"
26+||| ```
27+parseInteger : (Num a, Neg a) => String -> Maybe a
28+parseInteger s = parseIntTrimmed (trim s) where
29+ parseIntTrimmed s with (strM s)
30+ parseIntTrimmed "" | StrNil = Nothing
31+ parseIntTrimmed (strCons x xs) | (StrCons x xs) = if (x == '-') then map (\y => negate (fromInteger y)) (parseIntegerAux (unpack xs) 0)
32+ else if (x == '+') then map fromInteger (parseIntegerAux (unpack xs) 0)
33+ else map fromInteger (parseIntegerAux (unpack xs) (ord x - ord '0')) where
34+ parseIntegerAux : (List Char) -> Int -> Maybe Integer
35+ parseIntegerAux [] acc = Just (cast acc)
36+ parseIntegerAux (c :: cs) acc = if (c >= '0' && c <= '9') then parseIntegerAux cs ((acc * 10) + (ord c) - (ord '0'))
37+ else Nothing
38+
libs/base/base.ipkg+1−1
@@ -17,7 +17,7 @@ modules = System,
17 Data.HVect, Data.Vect.Quantifiers,
17 Data.HVect, Data.Vect.Quantifiers,
18 Data.Complex,
18 Data.Complex,
19 Data.Erased, Data.List,
19 Data.Erased, Data.List,
20− Data.So,
20+ Data.So, Data.String,
21
21
22 Control.Isomorphism,
22 Control.Isomorphism,
23 Control.Monad.Identity,
23 Control.Monad.Identity,
libs/prelude/Prelude/Strings.idr−14
@@ -340,20 +340,6 @@ toUpper x with (strM x)
340 strToLower (strCons c cs) | (StrCons c cs) =
340 strToLower (strCons c cs) | (StrCons c cs) =
341 strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))
341 strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))
342
342
343−||| Convert a number string to int.
344−|||
345−||| ```idris example
346−||| parseInt "123"
347−||| ```
348−parseInt : String -> Maybe Int
349−parseInt s with (strM s)
350− parseInt "" | StrNil = Nothing
351− parseInt (strCons x xs) | (StrCons x xs) = parseIntAux (unpack xs) (ord x - ord '0') where
352− parseIntAux : (List Char) -> Int -> Maybe Int
353− parseIntAux [] acc = Just acc
354− parseIntAux (c :: cs) acc = if (c >= '0' && c <= '9') then parseIntAux cs ((acc * 10) + (ord c) - (ord '0'))
355− else Nothing
356−
357--------------------------------------------------------------------------------
343--------------------------------------------------------------------------------
358-- Predicates
344-- Predicates
359--------------------------------------------------------------------------------
345--------------------------------------------------------------------------------