問題タブ [idris]

型シグネチャを持つ関数があります(x, y : SomeType) -> (cond x y) = True -> SomeType。if-then-else/case/with ステートメントで条件を確認するとき、対応するブランチの関数にその条件が true であるという事実を渡すにはどうすればよいですか?

を使用して実行可能ファイルの代わりにライブラリを生成する方法はありidrisますか? なしでコンパイルしようとするとmain、次のようなエラーが発生します。

ライブラリを生成できる場合、C コードから呼び出す方法はありますか? 生成された C コードを見ましたが、外部から呼び出されることを意図していたようには見えません。

私は C の他の言語との相互運用性と妥当なパフォーマンスを必要とするライブラリ プロジェクトを持っていますが、文芸的なプログラミングのように非常に明確に文書化する必要があり、その文書化は Haskell やIdrisの証明機能の ような関数型アプローチの恩恵を受ける可能性があります。

したがって、私はこのライブラリを読み書き可能なプログラムとして構築することに興味があります。最初にドキュメンテーションを作成し、Idris プロトタイプ コードを動作させます。次に、パフォーマンスの問題に対処し、他の言語から簡単にリンクできるように Idris コードと密接に類似する C コードを作成します。

どの文芸プログラミング ツールが必要ですか?

NuWebは多言語の読み書き可能なプログラミング用に設計されていますが、@ 記号や実際のエスケープ文字の使用は、Idris、Haskell などの関数型言語では問題があります。

Idrisは、私が貢献できる読み書きのできるプログラミング ツールを求めています。ブロックで区切られたファイルを使用するという彼らの好ましいアプローチが気に入っています。.tex\begin{code} .. \end{code}

Idris、Haskell などは、C のようにもつれを必要としないため、複雑さが増すため、ここで使用しているツールはそのまま使用することをお勧めします。

ライブラリ コンシューマー向けのツールを最小限に抑えるアプローチは、次のような単純な Perl スクリプトを使用して C および Idris コードを抽出することですcat_latex_env。

その時点で、Idris は正常にコンパイルされるはずです。そして、CWEB や NuWeb のような C 用の文芸的なプログラミング ツールに必要なタングル命令を埋め込むことができました。

考え？

IdrisNet2ライブラリを使用して、いくつかのバイナリ データ構造を定義しようとしています。Idris 0.9.17.1 を使用しており、IdrisNet2 の 262b746c9a2405e43d1de6a48de44cac2fd19932 をコミットしています。1 つの 16 ビット フィールドでパケットを定義しています。

コンパイラ エラーが発生します。

正確には何が問題で、どうすれば修正できますか? 16 が 0 より大きいことをコンパイラに証明する必要があると推測していますが、Idris でこれを行う方法や、なぜこれが必要なのかがわかりません。

Vect値を表示するための単純な型をいくつか書きました。

ベクトルの最後の要素を分離している場合、それSplitを に変換できるはずですSnocVect。

残念ながら、これを実装する方法が見つからないようです。特に、引数のパターン マッチを可能にする方法がまったく見つかりませんでした。それがなけれSplit n xsば、明らかにどこにもたどり着けません。基本的な問題は、私がタイプの何かを持っていることだと思います

単射ではないので++、何らかの魔法をかけて、型チェッカーに意味があることを納得させる必要があります。しかし、私はこれを確実に言うには十分に理解していません。