10

在 Idris 中将 String 转换为 Integer 或 Natural的最佳方法是什么？

我知道标准库仍在进行中，所以如果答案是我应该将它添加到标准库中，那很好，我会尝试这样做，但在我想我会确认没有办法之前。

如果我想从用户那里读取索引，我能想到的最好的方法是：

indexAsString <- getLine
let indexAsInt : Integer = cast indexAsString
let items: Vect _ _ = ["shoe", "bat", "hat"]
let i = integerToFin indexAsInt $ length items
maybe (print "invalid index") (\ii => print $ index ii items) i

但是这样，我没有从 cast 中得到失败的迹象。不仅 indexAsString 的格式可能不允许将其转换为 Integer，而且最重要的是，它甚至不会在运行时失败，由于 "bad cast" 而产生 0。

请告诉我有更好的方法和/或指出我正确的方向。

附带说明一下，Idris 中没有 Read 类型类是否有特殊原因？还是只是还没有进入？

提前谢谢。

4

2 回答 2

7

Idris在类型签名中有一个parseInteger和parsePositive函数Data.String

Num a => Neg a => String -> Maybe a

和

Num a => String -> Maybe a

http://www.idris-lang.org/docs/current/base_doc/docs/Data.String.html

于 2016-02-27T13:20:28.580 回答
4

我可能会出错，但我会尝试分享我的想法。失败的迹象是关于解析。

在旧的 idris 存储库中，我可以看到readInt哪个是，String -> Maybe Int但我不知道它现在在哪里。

但是我在这里找到了自定义实现：

charToInt : Char -> Maybe Int
charToInt c = let i = cast {to=Int} c in
              let zero = cast {to=Int} '0' in
              let nine = cast {to=Int} '9' in
              if i < zero || i > nine
                then Nothing
                else Just (i - zero)

total
parse' : Int -> List Int -> Maybe Int
parse' _   []      = Nothing
parse' acc [d]     = Just (10 * acc + d)
parse' acc (d::ds) = parse' (10 * acc + d) ds


total parseInt : String -> Maybe Int
parseInt str = (sequence (map charToInt (unpack str))) >>= parse' 0

main : IO ()
main = do let r = parseInt !getLine
          putStrLn "."

很容易阅读它是如何工作的。charToInt（可能我认为它可以更好地编码，但我不知道如何）基于cast，parse正在*10为列表中的每个新整数（例如符号）一个一个地处理整数并进行解parseInt包并将结果传递给. 在 Haskell 中是一样的。StringcharToIntparse!=<<

于 2014-03-18T05:28:01.337 回答