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

ここでの問題は、の型が十分に表現力がないdrop j xsため、 がその入力から厳密に小さいリストを生成することを Idris が認識できないことです。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 に答える