我如何使用 'getChar' 递归地填充具有依赖对的 Idris 字符结构？

Question

谁能帮我解决这个问题..

这是我想要的数据结构：

example : (n : Nat ** Vect n (n1 : Nat ** Vect n1 Char))
example = (3 ** [(3 ** ['a', 'b', 'c']), (3 ** ['d', 'e', 'f']), (3 ** ['g', 'h', 'i'])])

我想从 STDIN 读取字符，并为每个 \n 创建一个包含该行字符的新向量。空行结束递归。

这将是上述示例的输入：

abc\n
def\n
ghi\n
\n

我想知道是否可以使用一个递归函数。像这样的整个字符串：

read_vect : IO (len ** Vect len String)
read_vect = do x <- getLine
               if (x == "")
                  then pure (_ ** [])
                  else do (_ ** xs) <- read_vect
                          pure (_ ** x :: xs)

非常感谢！杰森.

Answer 1

您在 example 中的类型仅与 List (List Char) 同构，因为您可以做到

listToVect : List a -> (n : Nat ** Vect n a)
listToVect xs = (length xs ** fromList xs)

vectToList : (n : Nat ** Vect n a) -> List a
vectToList (_ ** xs) = toList xs

所以我们可以写成 List:

lines : List Char -> List (List Char)
lines = foldr step []
  where
    step : Char -> List (List Char) -> List (List Char)
    step '\n' ls = [] :: ls
    step c [] = [[c]]
    step c (l::ls) = (c::l) :: ls

lines' : String -> (n : Nat ** Vect n (n' : Nat ** Vect n' Char))
lines' = listToVect . map listToVect . lines . unpack

但是，我不相信这是你想要的。

字符矩阵不是 List (List Char)，对于某些固定的 n 和 m，它是 Vect n (Vect m Char)，因为它是矩阵的全部意义在于所有行的长度都相同。

我们可以将其实现为

Matrix : Nat -> Nat -> Type -> Type
Matrix n m a = Vect n (Vect m a)

然后写一些东西来解析给定大小的矩阵：

parseLine : (m : Nat) -> List Char -> Maybe (Vect m Char, List Char)
parseLine Z ('\n'::cs) = Just ([], cs)
parseLine (S m) (c :: cs) = map (\(l, cs') => (c::l, cs')) $ parseLine m cs
parseLine _ _ = Nothing

parseMatrix' : (n : Nat) -> (m : Nat) -> List Char -> Maybe (Matrix n m Char, List Char)
parseMatrix' Z m ['\n'] = Just ([], [])
parseMatrix' (S n) m cs = case parseLine m cs of
  Nothing => Nothing
  Just (l, cs') => case parseMatrix' n m cs' of
    Nothing => Nothing
    Just (ls, cs'') => Just (l::ls, cs'')
parseMatrix' _ _ _ = Nothing

parseMatrix : (n : Nat) -> (m : Nat) -> String -> Maybe (Matrix n m Char)
parseMatrix n m = map fst . parseMatrix' n m . unpack

这仍然不是您想要的，因为 n 和 m 是预先确定的，而不是查看输入；所以也许我们应该选择

SomeMatrix : Type -> Type
SomeMatrix a = (n ** (m ** Matrix n m a))

导致

parseSomeMatrix : String -> Maybe (SomeMatrix Char)
parseSomeMatrix cs = case map unpack (lines cs) of
    l::ls => parseFrom l ls
    [] => Just (0 ** (0 ** []))
  where
    parseFrom : List Char -> List (List Char) -> Maybe (SomeMatrix Char)
    parseFrom cs ls = map (\vs => (length vs ** (m ** fromList vs))) (parseInto ls)
      where
        m : Nat
        m = length cs

        parseInto : List (List Char) -> Maybe (List (Vect m Char))
        parseInto [] = Just []
        parseInto (l :: ls) with (decEq (length l) m)
          | Yes p = map (\vs => (replace {P = \m => Vect m Char} p (fromList l)) :: vs) (parseInto ls)
          | No _ = Nothing

Answer 2

编辑，getLine：不需要实际的矩阵，这很简单：

read_structure : IO (k : Nat ** Vect k (l : Nat ** Vect l Char))
read_structure = do str <- getLine
                    let chrs = unpack str
                    let x = fromList chrs
                    if length chrs == 0
                       then pure (_ ** [])
                       else do (_ ** xs) <- read_structure
                               pure (_ ** (_ ** x) :: xs)

Idris 可以推断出最多的东西（并且 ** 绑定比 :: 更强），但为了清楚起见，详细版本将是：

                       then pure (0 ** [])
                       else do (n ** xs) <- read_structure
                               pure ((S n) ** ((length chrs ** x) :: xs))

编辑，getChar：如果你真的想用 getChar 进行递归，下面是一个版本，当用 read_list True 包装时，会给你一个 List (List Char)。 break参数就是找出，如果连续出现了两个'\n'。

read_list : Bool -> IO (List (List Char))
read_list break = do chr <- getChar
                     if chr == '\n'
                        then if break
                                then pure []
                                else do rest <- read_list True
                                        pure ([] :: rest)
                        else do rest <- read_list False
                                case rest of
                                     x :: xs => pure ((chr :: x) :: xs)
                                     Nil => pure ([chr] :: Nil)

要使用 k : Nat ** Vect k (l : Nat ** Vect l Char) 完成这项工作，您只需要输入一些 (_ ** xs):

read_vects : Bool -> IO (k : Nat ** Vect k (l : Nat ** Vect l Char))
read_vects break = do chr <- getChar
                      if chr == '\n'
                        then if break
                                then pure (_ ** [])
                                else do (_ ** rest) <- read_vects True
                                        pure (_ ** (_ ** []) :: rest)
                        else do (_ ** rest) <- read_vects False
                                case rest of
                                     (_ ** x) :: xs => pure (_ ** (_ ** (chr :: x)) :: xs)
                                     Nil => pure (_ ** (_ ** [chr]) :: Nil)

List 版本绝对更具可读性，正如 Cactus 指出的那样，List a 几乎等同于 k ** Vect k a。所以你可以先解析它然后转换成 Vects.

我如何使用 'getChar' 递归地填充具有依赖对的 Idris 字符结构？

How can I recursively fill an Idris character structure with dependent pairs using 'getChar'?

recursion

idris