floating
Luna-Flow/floating は MoonBit のための任意精度浮動小数点算術ライブラリです。任意精度で IEEE 754 の意味論に従う二進値、IEEE 754 および General Decimal Arithmetic の十進数、そして IEEE 1788 に従う認証付き区間(ボール)算術を提供します。精度、丸め、指数範囲、特殊値、ステータスフラグ、トラップ、包含区間は、隠れたグローバル状態ではなく、すべての API で明示的な値として扱われます。このマニュアルは現在のブランチを説明しており、現在のリリースは 0.8.0 です。
インストール
moon add Luna-Flow/floating@0.8.0
次に、moon.pkg で必要なパッケージをインポートします。たとえば "Luna-Flow/floating/bin_float" です。このモジュールには MoonBit ツールチェーン 0.10 以降(moonc ≥ 0.10)が必要です。Luna-Flow/arithmetic(丸めモード、コンテキスト、checked およびコンテキスト付きトレイト)と Luna-Flow/luna-generic(代数的トレイト)に依存しています。Luna-Flow/arithmetic の型を名指しする場合は、自分でそれを追加してください。はじめにでは最初のプログラムを順を追って説明しています。
ガイド
| ガイド | 読むべき場面 |
|---|---|
| はじめに | パッケージの選択、インストール、最初の値、コンテキストと失敗モデル |
| 数値意味論 | 共通の語彙: 厳密値と丸められた結果、丸め関数、ulp と単位丸め誤差、フラグ、量子、符号付きゼロ、NaN、包含区間 |
| アーキテクチャ | パッケージのレイヤー、数値コアのパイプライン、認証付き初等関数、不変条件 |
| 検証 | ゲート、公開されている適合性の主張、およびその再現方法 |
| 性能監査 | 最適化された算術経路に対する証明と証拠 |
| リポジトリの規約 | ドキュメントの規則とレビューのチェックリスト |
パッケージマップ
各パッケージには、チュートリアル(使い方)、API リファレンス(呼び出せるもの)、設計ページ(なぜそのように動作するのか)があります。四つの数値コアには、さらに適合性と性能のページがあります。
数値コア
| パッケージ | 目的 | ページ |
|---|---|---|
bin_float | 任意精度の二進浮動小数点、IEEE 754 二進演算、binary16/32/64/128 交換形式 | チュートリアル · API · 設計 · 適合性 · 性能 |
decimal | 演算ごとのフラグと DPD/BID 交換形式を備えた IEEE 754 任意精度十進数 | チュートリアル · API · 設計 · 適合性 · 性能 |
decimal_gda | スティッキーなステータスとトラップを備えた General Decimal Arithmetic | チュートリアル · API · 設計 · 適合性 · 性能 |
ball_float | 外向き丸めによる bare 区間と decorated 区間(IEEE 1788) | チュートリアル · API · 設計 · 適合性 · 性能 |
合成と共通語彙
| パッケージ | 目的 | ページ |
|---|---|---|
def | Sign、PartialOrder、Floating トレイト、述語、再エクスポートされた arithmetic の型 | チュートリアル · API · 設計 |
bin_float_checked | 最初のエラーで停止する二進パイプライン | チュートリアル · API · 設計 |
decimal_checked | フラグを蓄積する IEEE 十進パイプライン | チュートリアル · API · 設計 |
decimal_gda_checked | ステータスを受け渡し、トラップで停止する GDA パイプライン | チュートリアル · API · 設計 |
ball_float_checked | 最初のエラーで停止する区間パイプライン | チュートリアル · API · 設計 |
semantic | パッケージ間の比較のための、表現に依存しない厳密な射影 | チュートリアル · API · 設計 |
式とコーパスのフロントエンド
| パッケージ | 目的 | ページ |
|---|---|---|
numeric_expr | ホストに依存しない数値式の構文と評価 | チュートリアル · API · 設計 |
frontend/gda_expr | GDA の .decTest ファイルをパースして実行する | チュートリアル · API · 設計 |
frontend/itl_expr | ITF1788 の区間テストの行をパースして実行する | チュートリアル · API · 設計 |
frontend/mpfr_expr | 固定された MPFR の証拠データ(witness)をパースして実行する | チュートリアル · API · 設計 |
frontend/testfloat_expr | Berkeley TestFloat のベクタをパースして実行する | チュートリアル · API · 設計 |
適合性検証のコマンドライン
| パッケージ | 目的 | ページ |
|---|---|---|
cli | 四つの適合性検証バックエンドのためのネイティブディスパッチャ | チュートリアル · API · 設計 |
cli/gda_expr_cli | .decTest 実行のためのファイルおよび出力アダプタ | チュートリアル · API · 設計 |
cli/itl_expr_cli | ITF1788 実行のためのファイルおよび JSON アダプタ | チュートリアル · API · 設計 |
cli/mpfr_expr_cli | MPFR 証拠データ実行のためのコマンドアダプタ | チュートリアル · API · 設計 |
cli/testfloat_expr_cli | TestFloat 実行のためのコマンドアダプタ | チュートリアル · API · 設計 |
基盤と証拠
| パッケージ | 目的 | ページ |
|---|---|---|
internal | 共有の厳密有理数、多倍長整数、パース、正規化、丸めのヘルパー | チュートリアル · API · 設計 |
internal/conformance | ソース位置、決定的なシャード、ケースの処理区分、サマリー | チュートリアル · API · 設計 |
internal/runner_cli | 共有の CLI オプション、ファイル、診断、JSON | チュートリアル · API · 設計 |
consistency | ホワイトボックスによるパッケージ横断の法則と API 監査 | チュートリアル · API · 設計 |
doc_examples | just docs で実行される実行可能なドキュメントの例 | チュートリアル · API · 設計 |
bench | 共有の Maremark ベンチマーク基盤 | チュートリアル · API · 設計 |
bench/bin_float | 二進算術と初等関数のベンチマーク | チュートリアル · API · 設計 |
bench/decimal | IEEE 十進ベンチマーク | チュートリアル · API · 設計 |
bench/decimal_gda | GDA 十進ベンチマーク | チュートリアル · API · 設計 |
bench/ball_float | 区間算術ベンチマーク | チュートリアル · API · 設計 |
アプリケーション向けの公開面は、数値コア、def、checked ラッパーです。semantic と numeric_expr は暫定的な統合用の公開面です。その他のパッケージは、リポジトリのツールがそれらを合成するためにインターフェースを公開しており、その設計ページではより限定的な安定性の約束を述べています。
読み進め方
- ライブラリを初めて使う場合。 はじめにを読み、次に選んだパッケージのチュートリアル、たとえば
bin_floatチュートリアルやdecimalチュートリアルを読んでください。用語については数値意味論を手元に開いておいてください。 - アプリケーションやライブラリで使う場合。 数値意味論を一度読み、その後は使用するパッケージの API ページを参照して作業してください。標準の振る舞いに依拠する前に、対応する適合性ページを確認してください。パイプラインについては、checked ラッパーのチュートリアルを読んでください。
- コントリビュートする場合。 アーキテクチャ、検証、リポジトリの規約を読み、次に変更するパッケージの設計ページを読んでください。最適化された経路を変更する場合は、性能監査とそのパッケージの性能ページも必要です。
証拠の概要
- 固定された GDA の
officialコーパスは 64,986/64,986 件の正当な実行可能スカラー行 をパスし、official0は 16,124/16,124 件をパスします。残る 141 件の#プレースホルダ行または非スカラー行は診断上の除外対象です。 - 二進の TestFloat レベル 1 マトリクスは、binary16/32/64/128 にわたる 254,227,872 個のベクタをパスします。これには融合積和、剰余、整数値への丸め、整数変換、比較述語が含まれ、さらに固定された MPFR の平方根および初等関数の証拠データもパスします。
- 厳密な ITF1788 の集計は、選択された 4,656/4,656 件の区間ケースをパスします。
- IEEE 十進のゲートは、四つのターゲット上で decimal32/64/128 の DPD および BID エンコーディング、フラグ、算術をカバーします。
これらの有限の結果は、あらゆる演算、将来のあらゆるコーパス改訂、あらゆる実数入力に対するサポートを意味するものではありません。結果を互換性の主張とする前に、そのパッケージの適合性ページを読んでください。
典拠
何が公開されているかは pkg.generated.mbti が定義し、振る舞いはソースとテストが定義します。ページと生成されたインターフェースが食い違う場合は、インターフェースが優先されます。