0

当出现以下代码时：

module TotalityOrWhat

%default total

data Instruction = Jump Nat | Return Char | Error

parse : List Char -> Instruction
parse ('j' :: '1' :: _) = Jump 1
parse ('j' :: '2' :: _) = Jump 2
parse ('j' :: '3' :: _) = Jump 3
parse ('r' :: x :: _) = Return x
parse _ = Error

parseDriver : String -> Maybe Char
parseDriver = parseDriver' . unpack where
  parseDriver' : List Char -> Maybe Char
  parseDriver' xs =
    case parse xs of
      (Jump j) => parseDriver' $ drop j xs
      (Return x) => Just x
      Error => Nothing

伊德里斯给出了一个错误：

TotalityOrWhat.idr:17:3:
TotalityOrWhat.parseDriver, parseDriver' is possibly not total due to recursive path
TotalityOrWhat.parseDriver, parseDriver' --> TotalityOrWhat.parseDriver, parseDriver'

TotalityOrWhat.idr:15:1:
TotalityOrWhat.parseDriver is possibly not total due to:
TotalityOrWhat.parseDriver, parseDriver'

我已经用其他几种方式重写了这段代码，但无法让 Idris 将其识别为全部。我错了它是完全的，还是伊德里斯无法确定它是完全的？如果它本质上是完全的，我该如何重写它以便 Idris 将其识别为完全？

4

2 回答 2

3

这不是对“为什么不将其识别为全部”的答案，甚至不是对“我如何将其更改为被识别为全部”的真正答案，但是既然您提到了

我已经用其他几种方式重写了这段代码，但无法让 Idris 将其识别为全部，

我认为您可能对解决方法感兴趣。如果您手动内联parse到parseDriver'，您可以通过整体检查器获取它：

total parseDriver : String -> Maybe Char
parseDriver = parseDriver' . unpack where
  parseDriver' : List Char -> Maybe Char
  parseDriver' ('j' :: '1' :: xs) = parseDriver' ('1' :: xs)
  parseDriver' ('j' :: '2' :: xs) = parseDriver' xs
  parseDriver' ('j' :: '3' :: _ :: xs) = parseDriver' xs
  parseDriver' ('r' :: x :: _) = Just x
  parseDriver' _ = Nothing

这是有效的，因为我们总是在结构上递归xs.

于 2016-08-21T13:16:57.583 回答
3

这里的问题是 Idris 无法知道它drop j xs会从其输入中生成一个严格较小的列表，因为drop' 的类型没有足够的表现力。

因此，另一种特别的方法是使用一个虚拟参数，通过在递归xs'调用时使用结构上更小的列表，使整体检查器接受该函数。parseDriver'

parseDriver : String -> Maybe Char
parseDriver s = parseDriver' chars chars where
  chars : List Char
  chars = unpack s

  -- 2nd parameter is a dummy one (to make totality checker happy)
  parseDriver' : List Char -> List Char -> Maybe Char
  parseDriver' _  [] = Nothing
  parseDriver' xs (_::xs') =
    case parse xs of
      Jump j => parseDriver' (drop j xs) xs'
      Return x => Just x
      Error => Nothing

我们也可以使用一些自然参数n，我们可以在每一步递减，确保我们停在0。的初始值n自然可以是输入列表的长度。

于 2016-08-21T15:40:52.200 回答