この再帰関数は合計ではありませんか、コンパイラはそれを証明できませんか？それを合計で書き直すには？

Question

次のコードを提示：私は他のいくつかの方法でこのコードを再書かれているが、イドリスは合計としてそれを認識することができません

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' 

：

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 

イドリスはエラーになります。私はそれが完全であることについて間違っているのですか、それともIdrisだけがそれを判断できませんか？本質的に合計であれば、どのように書き直してIdrisがそれを合計として認識するのですか？

Answer 1

これは、「なぜそれが全体として認識されていない」ともない、本当に「どのように私はそれがトータルとして認識されるように変更できますか」に対する答えを、しかし、あなたは

I have re-written this code in several other ways but cannot get Idris to recognize it as total,

を述べたので、への答えではありません

あなたは回避策に興味があると思っていました。手動parseDriver'にparseをインライン化した場合、あなたは全体チェッカーを通してそれを得ることができます：

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のいくつかのサフィックスに構造的に再帰されているので、これは動作します。

Answer 2

ここでの問題は、dropの型が十分に表現力がないため、Idreamはdrop j xsが入力から厳密に小さいリストを生成することを知ることができないということです。

ので、別のアドホックアプローチは、再帰的にparseDriver'の呼び出し中に構造的に小さいリストxs'を使用することによって、機能を受け入れる全体チェッカーを作るダミーパラメータを使用することであろう。

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 

我々はまた、我々は0で停止を確認しながら、私たちは各ステップでデクリメントができ、いくつかの自然なパラメータnを、使用していたかもしれません。当然、nの初期値は、入力リストの長さになります。