問題タブ [zipper]

APIで取得したPDFからzipファイルを作成するためにZipperパッケージを使用しています。圧縮は正常に機能しますが、圧縮された PDF ファイルを削除したいと考えています。

私はこのコードを使用していますがcleanDirectory()、圧縮が完了する前に呼び出され、zip が生成されていないと思います。最後の行をコメントアウトすると、zip ファイルと PDF の両方が/user_downloads.

ジッパーが完全に閉じるのを待つにはどうすればよいですか?

私は次のものを持っています：

Idris が一致できないため、これは型チェックを行いません私の質問は、式に具象型の子がある場合に、ツリー内の 1 レベルを再構築できるようにするにはどうすればよいですかAnd? なんらかの方法で型を改良する必要があると思いますが、新しい従属型 (または GADT) を作成することがこれにどのように役立つか実際にはわかりません (そして、型を改良する他の方法を知りません!)upZipper f gZipper Bool g

私は意見と証明を調べましたが、数週間最善を尽くした後、問題を次のように書く方法を見つけることができないようですThe focus of the zipper has the same type as the right child of the context's parent expression, if the context was constructed with R. The same is true for the focus and the context's left child, if the context was constructed with L.

各式がその子の型を保持するように型パラメーターを増やしてみましたが、この関係をキャプチャするExpr a l m rために新しいバージョンを作成できても、同じエラーが発生します。最後に、いくつかのパラメトリックが実際に特定のパターン マッチの下にあるR : Expr r t u v -> Expr a l m r -> Expr m h i j -> Expr r x y z -> Context -> Contextことを Idris に伝える方法が必要です!aBool

私は非常に立ち往生しているので、アドバイスをいただければ幸いです！

よろしく、ドノバン