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 · 設計 · 適合性 · 性能

合成と共通語彙

パッケージ目的ページ
defSign、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_exprGDA の .decTest ファイルをパースして実行するチュートリアル · API · 設計
frontend/itl_exprITF1788 の区間テストの行をパースして実行するチュートリアル · API · 設計
frontend/mpfr_expr固定された MPFR の証拠データ(witness)をパースして実行するチュートリアル · API · 設計
frontend/testfloat_exprBerkeley TestFloat のベクタをパースして実行するチュートリアル · API · 設計

適合性検証のコマンドライン

パッケージ目的ページ
cli四つの適合性検証バックエンドのためのネイティブディスパッチャチュートリアル · API · 設計
cli/gda_expr_cli.decTest 実行のためのファイルおよび出力アダプタチュートリアル · API · 設計
cli/itl_expr_cliITF1788 実行のためのファイルおよび JSON アダプタチュートリアル · API · 設計
cli/mpfr_expr_cliMPFR 証拠データ実行のためのコマンドアダプタチュートリアル · API · 設計
cli/testfloat_expr_cliTestFloat 実行のためのコマンドアダプタチュートリアル · API · 設計

基盤と証拠

パッケージ目的ページ
internal共有の厳密有理数、多倍長整数、パース、正規化、丸めのヘルパーチュートリアル · API · 設計
internal/conformanceソース位置、決定的なシャード、ケースの処理区分、サマリーチュートリアル · API · 設計
internal/runner_cli共有の CLI オプション、ファイル、診断、JSONチュートリアル · API · 設計
consistencyホワイトボックスによるパッケージ横断の法則と API 監査チュートリアル · API · 設計
doc_examplesjust docs で実行される実行可能なドキュメントの例チュートリアル · API · 設計
bench共有の Maremark ベンチマーク基盤チュートリアル · API · 設計
bench/bin_float二進算術と初等関数のベンチマークチュートリアル · API · 設計
bench/decimalIEEE 十進ベンチマークチュートリアル · API · 設計
bench/decimal_gdaGDA 十進ベンチマークチュートリアル · 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 が定義し、振る舞いはソースとテストが定義します。ページと生成されたインターフェースが食い違う場合は、インターフェースが優先されます。