Idris - ベクトルキューと書き換えルール

Question

私はIdrisに機能キューのようなものを実装しようとしていますが、Queue ty n m (n+m)のような要素の数を持っています。nは1の要素の数ですVect n ty、m第2の要素Vect m tyであり、(n+m)が要素です。

問題は、私は暗黙の引数としてこれらのサイズを操作する際に書き換えルールを適用することの問題に実行している、次のとおりです。

module Queue 

import Data.Vect as V 

data Queue : Type -> Nat -> Nat -> Nat -> Type where 
    mkQueue : (front : V.Vect n ty) 
      -> (back : V.Vect m ty) 
      -> Queue ty n m (n + m) 

%name Queue queue 

top : Queue ty n m (S k) -> ty 
top {n = S j} {m} {k = j + m} (mkQueue front back) = 
    V.head front 
top {n = Z} {m = S j} {k = j} (mkQueue front back) = 
    V.head $ V.reverse back 

bottom : Queue ty n m (S k) -> ty 
bottom {m = S j} {n} {k = n + j} (mkQueue front back) = 
    ?some_rewrite_1 (V.head back) 
bottom {m = Z} {n = S j} {k = j} (mkQueue front back) = 
    ?some_rewrite_2 (V.head $ V.reverse front) 

top作品が、bottomません。私は何とかplusZeroRightNeutralとplusRightSuccRightの書き換えを提供する必要があるようですが、どこに書き換えるか、別のオプションがあるかどうかはわかりません。ここではエラーメッセージは以下のとおりです。bottomの最初の行に

エラー：bottomの2行目に

  Type mismatch between 
       Queue ty n (S j) (n + S j) (Type of mkQueue front back) 
     and 
       Queue ty n (S j) (S (n + j)) (Expected type) 

     Specifically: 
       Type mismatch between 
         plus n (S j) 
       and 
         S (n + j) 

エラー：私は2を回転させる必要がある場合

  Type mismatch between 
       Queue ty (S j) 0 (S j + 0) (Type of mkQueue front back) 
     and 
       Queue ty (S j) 0 (S j) (Expected type) 

     Specifically: 
       Type mismatch between 
         plus (S j) 0 
       and 
         S j 

個々のサイズを教えてくださいVectsであり、空の場合と空でない場合は全体のサイズがわかりますQueueですので、可能であればすべての情報を追跡したいと考えています。

Answer 1

この問題を解決する1つの方法は、nも破壊することです。

側の注意点として

total 
bottom : Queue ty n m (S k) -> ty 
bottom {m = S m} {n = S n} (MkQueue _ back) = V.head back 
bottom {m = S m} {n = Z} (MkQueue _ back) = V.head back 
bottom {m = Z} {n = S n} (MkQueue front _) = V.head $ V.reverse front 
bottom {m = Z} {n = Z} (MkQueue _ _) impossible 

、私はtop機能の合計を作成することをお勧めしたい：イドリスは最後の引数が、それは基本的に文句され、ゼロではないことを理解しているこの時間として

total 
top : Queue ty n m (S k) -> ty 
top {n = S n}   (MkQueue front _) = V.head front 
top {n = Z} {m = S m} (MkQueue _ back) = V.head $ V.reverse back 
top {n = Z} {m = Z} (MkQueue _ _) impossible