Formurae は、Egison のテンソル添字記法で書いた偏微分方程式を Formura の stencil programへ変換し、 MPI・temporal blocking付きC codeを生成するための実験的な言語処理系です。
表層言語の拡張子は .fme です。数式の意味と離散化を分離し、次の4段で処理します。
model.fme
└─ formurae-pre ──> model.egi
└─ Egison ──> model.feir
└─ formurae-post ──> model.fmr
└─ Formura ──> C
formurae-preは構文、scope、宣言、source mapを検査し、Egison normalization unitを生成します。- Egison はuser definition、tensor/index algebra、analytic differentiationを評価し、canonical FEIRを出力します。
formurae-postはplacement、stencil、補助field、storageを決め、Formura programを生成します。- Formura は配列、loop、MPI通信、temporal blockingを含むC codeを生成します。
純粋な数学演算子はEgisonにだけ定義されます。grad、divg、curl、hessian、lap、
d、hodge、δ、Δ_Hの解析的な部分は、callbackやcomponent loopを含まない短いEgison関数です。
具体的な差分係数や格子offsetをEgisonの演算子定義へ混ぜません。
user tensor operatorも同じ経路です。例えば次のwithSymbolsを出た自由な下添字は、Egisonでは
添字を省略したtensor軸になります。省略軸には既存の明示添字とは異なるfreshな下添字が補われ、
formurae-preは関数名や本体からresult varianceのsignatureを推論・付与しません。EgisonがRHSを評価した後、
宣言済みのequation targetまたはindexed localへ値を格納する時点で、targetが要求するshape、logical
variance、dfOrderと実際の値を照合します。degree-zero covariant tensor targetへ代入する場合に限り、
構造的index completionがcompatibleなanonymous down軸をtargetの下添字へ対応付けます。anonymous down軸を
up targetとして読み替えることはできず、form targetではdfOrderを保持します。
def gradLike u = withSymbols [i] (∂_i u)
field q_i
step:
q' = gradLike u
したがって、E_i + gradLike uのanonymous軸が既存のiへ暗黙に統合されることはありません。
この式では両者は別の軸です。同じ軸で合成する意図は、
withSymbols [i] (E_i + (gradLike u)..._i)のようにcall siteで下添字を明示できます。
pure user operatorの本体は1行に限定されません。=の次をindentすると、Egisonのlet、lambda、
match、withSymbols、generateTensorを含む式blockをそのままnormalizationへ渡せます。
1行の本体とこのようなrich bodyは、どちらもEgisonが通常の式として評価します。Formuraeはuser
definitionの式構造や計算履歴を検査してresult signatureを付けません。評価結果がfield equation
またはindexed localへ格納されるときだけ、上記のtarget metadata照合を行います。
def chooseByDimension X =
let apply := \f x -> f x
choose := match dimension = 3 as bool with
| #True -> \Y -> 2 * Y
| #False -> \Y -> Y
in apply choose X
dimension、coordinates、volume、epsilon、metric、inverseMetricはmodelのambient
Egison環境にあり、ユーザ定義とFormurae.*標準演算子はこれらを直接参照します。
そのためユーザがcontext引数を渡す必要はありません。metric gを宣言すると、同じ実計量を
共変なg_i_j（whole viewはg_#_#）と反変なg~i~jから参照できます。宣言名を使わない
canonical viewはmetric_i_j / metric_#_#とinverseMetric~i~jです。反変なviewは、次のように
varianceが見えるindexed equation/localで直接使います。
metric scale [1, 1 + x]
metric g
field A_i
field X~i
step:
X'~i = withSymbols [j] (g~i~j . A_j)
A'_i = withSymbols [j] (g_i_j . X~j)
この明示的な計量縮約を正準な書き方とし、flat / sharpはFormuraeのpublic operatorとして
提供しません。関数headへ結果添字を書く構文もありません。
ambient名とmetric gの宣言名はfield、parameter、user definition、definition parameter、
step-level let / localでは予約されます。Egison expression block内の局所letやlambdaだけは
通常のlexical scopeに従います。
mode collocated
dimension 3
axes x, y, z
param κ = 1.0
param dt = 0.1*dx*dx
field u : scalar
init:
u = gauss(i*dx,j*dy,k*dz)
step:
u' = u + dt * κ * Δ u
Δはmode collocatedのcanonical scalar Laplacianです。精度に依存しないため、
4次精度へ変更するときも別の数学演算子を定義せず、model-level profileを追加します。
discretization collocated derivative 2 centered accuracy 4
EgisonはgeometryのないΔ uを二階のFieldJetへ正規化し、formurae-postが4次精度を満たす最小半径2の
compact 5点stencilをexact rational coefficientで導出します。一階wide stencilを二重適用しません。
通常の∂は解析微分です。
∂_x (u * u) -- Egison: 2 * u * FieldJet(u,{x:1})
未知の解析微分則を0とみなすことはなく、Egisonの∂/∂がerrorにします。
混合偏微分はcanonicalなmulti-indexへまとめられます。
式全体を先に格子上で評価してから差分したい保存形では、微分式をbackquoteします。
`(∂_x (u * u / 2)) -- product ruleを開かないwhole-expression差分
入れ子のbackquoteは、内側からの軸順と重複を保ちます。
`(∂_y (`(∂_x (`(∂_x q)))) -- x, x, yの順に適用
配置変換を意図的に行う場合の明示surfaceはresampleです。
resample(q, 0, 1) -- 2Dの絶対placement (integer, half) へ線形補間
中間storageは型付きlocalで指定します。face fluxを明示する保存形は、
次のように通常のdivgと合成できます。
field u : scalar @ primal
step:
local q_i @ primal = [| -κ * `(∂_x u), -κ * `(∂_y u) |]_i
u' = u - dt * divg q
q_i @ primalは成分ごとに対応軸のfaceへ保存され、divg qはcellへ戻る差分を作ります。
このtelescopingによる保存保証は周期境界、または同じfluxと整合するghost/boundary処理の下でのものです。
現在の.fmeは物理境界条件自体を宣言せず、Formura側のYAML・boundary設定が権威です。
fieldはscalar、vector、rank-1/rank-2 tensor、k-formを宣言できます。
field E_i @ primal
field B_i @ dual
field σ{~i~j} @ primal
field A : 1-form
field F : 2-form
step:
local q_i @ primal = [| 0, 0, 0 |]_i
local ω : 2-form @ primal = d A
配置はCollocated、Primal、Dualのいずれかです。Primal/Dualの具体的な半セル位置は
field policyとcomponent basisのparityからformurae-postが推論します。異なるplacement間の補間は
暗黙に行わず、必要ならresample(value, bit...)を使います。
Maxwellはcollocated vector、Yee vector、DEC formの各形式で記述できます。
mode dec
dimension 3
axes x, y, z
field E : 1-form
field B : 2-form
step:
E' = E + dt * δ B
B' = B - dt * d E'
mode decのcanonical form演算子はd、hodge、δ、Δ_Hです。
δは余微分、Δ_H A = d (δ A) + δ (d A)はHodge--de Rham Laplacianです。
宣言幾何のδはpreludeマクロとしてdFluxWeights/dFluxScale/dFluxDivへ展開され、幾何のみの係数localはformurae-postがinit凍結のstate配列にします。
Δ_Hはconstant geometryでのpureな合成をサポートし、general variable-metric formは現IRで表せないためcompile-time errorにします。
これらのform演算子は宣言済みscalar/k-formだけを受け取り、ordinary tensorを暗黙にformへ変換しません。
quoted derivativeとcollocated scalar Δもscalar-onlyです。型annotationを持たないuser def parameterの
kindは証明できないため、typed operatorはfield、typed local、またはkindが確定したstep式へ直接適用します。
indexed δ~i_jは余微分とは別のKronecker tensorで、ASCII名deltaのuser定義にも捕捉されません。
d(d A) = 0は演算子ライブラリの定理としてcompiler suiteが検査し、離散的な
div B = 0の保存は各exampleのcheck driverが実測します。
直交計量はscale factorまたはembeddingで宣言します。
axes θ, φ, z
embedding [ `(2 + cos θ) * cos φ, `(2 + cos θ) * sin φ, sin θ, z ]
step:
u' = u + dt * Δ u
Egisonはmetric、inverse metric、scale factor、volumeを記号的に作り、embeddingでは直交性を
検査します。geometryを宣言したモデルのΔ uはpreludeマクロとして、実体化した重み・flux
localと符号付きadjoint divergenceへ展開されます。FEIRに残るのはordinaryなMaterialize
actionとwhole-operandなderivative.grid-whole requestだけで、幾何のみの係数local
はformurae-postが凍結してinit一回+恒等carryのpersistent stateにします(mirror/fixed壁の
境界処理もstate配列として宣言どおりに受けます)。
FEIR (Formurae Egison IR) はEgisonとformurae-postのcanonical protocolです。その同一性は 手で振る版番号ではなくfingerprint(内容ハッシュ)が固定します。
.fme のgeometry、:= analytic initializer、step、parse可能なdefに書いた
小数・指数リテラルは、formurae-preが綴りどおりのexact rationalへ変換します。
raw Egison def本体と= raw initializerはEgisonのFloat/生文字列の意味論を保ちます。
有限なdouble backendへ安全に下ろせない指数、または約分後の分子・分母をbinary64へ
正確に渡せない非整数リテラルは、丸めて続行せずcompile-time errorにします。
Unicode π はEgison CASでシンボリックに簡約され、残った値はFEIRの
(named-constant pi)としてformurae-postまで保持されます。FMRをrenderするときだけ、binary64のπと
同値で両operandが2^53未満の(884279719003555 / 281474976710656)へ変換します。
ASCII piはEgisonのFloatと衝突するためaliasではありません。parameter値と= raw initializerは
symbolic FEIRを通らないので、そこではπを使わずbackend数値を明示します。
- exact rationalを保持するcanonical S-expression
- closedなnamed mathematical constant
- stable
AxisId、FieldId、FunctionId、OriginId - scalar/tensor normal formとderivative multi-index付き
FieldJet GeometryNF、discretization profile、opaque discrete request- registry/primitive-manifest/profile fingerprint
.fmeのpath・line・columnとdefinition expansion trace
list nodeの順序はcanonical S-expressionをrenderしたbyte列で決まり、Egison encoderとHaskell validatorが同じ規則を使います。decoderはwire順を保持するため、非canonicalな入力順をparse時の sortで隠さずhard errorにします。
成功したEgison stageのstdoutはFEIR 1個だけです。diagnosticはstderrへ分離され、warning、type error、 evaluation error、余分なstdoutはmachine runnerが拒否します。
Formurae、Egison、検証済みFormuraはすべてCabalでインストールできます。
cabal installの実行ファイルディレクトリ(通常は~/.local/bin)をPATHに加えてください。
cabal install egison-5.1.0
git clone https://github.com/egison/formura.git
cd formura
git checkout 3bc74b5c6f1a24dfffe869839d75fd44b8aa2eb0
cabal install exe:formura --overwrite-policy=always
cd ..
git clone https://github.com/egison/formurae.git
cd formurae
cabal install exe:formurae exe:formurae-pre exe:formurae-post \
--overwrite-policy=always一括CLIは.egi、.feir、.fmrを入力ファイルと同じディレクトリへ書き、
compileでは続けてFormuraを呼び出します。
formurae compile examples/diffusion3d/diffusion3d.fme
formurae lower examples/diffusion3d/diffusion3d.fmecompileには入力と同じbasenameの.yamlが必要です。lowerは.fmr生成で停止します。
EGISON、FORMURA、FORMURAE_PRE、FORMURAE_POST環境変数で各実行ファイルを明示できます。
リポジトリ全体の試験はGHC 9.6系、隣接する../egison開発tree、および検証済みFormuraを使います。
make setupはFormuraを固定commitからCabalでbin/formuraへインストールします。
1-rank用MPI stubを同梱しています。
make setup
cabal build
make diffusion3d
make maxwell3d_yee
make metric_torusmake NAMEは.fme -> .egi -> .feir -> .fmr -> C -> checkを通します。全例は次で検証できます。
make all各stageを直接確認する場合:
cabal run -v0 formurae-pre -- examples/diffusion3d/diffusion3d.fme > /tmp/model.egi
tools/run_formurae_normalization.sh ../egison \
/tmp/model.egi > /tmp/model.feir
cabal run -v0 formurae-post -- /tmp/model.feir > /tmp/model.fmr.fmeが編集対象です。27個のFME例では.egi、.feir、.fmrをreview可能な生成artifactとして
追跡し、Makefileから再生成します。galleryは4段すべてを表示します。mhd_otは19本の保存流束を
typed localとして物質化し、lbm_d3q19は中心1階・2階差分の恒等式で整数1セルpullを構成して、
どちらも通常の.fme -> .egi -> .feir -> .fmr経路で検査します。LBMの19成分宣言と式を速度集合から
自動展開するfield f : family 19構文は、記述量をさらに減らす将来の表層機能です。
| パス | 役割 |
|---|---|
app/formurae/ |
インストール済みtoolchainを駆動する一括CLI |
app/formurae-pre/ |
Formurae frontend CLI |
app/formurae-post/ |
FEIR validation・discretization・Formura backend CLI |
src/Formurae/FEIR/ |
FEIR syntax、codec、validation、fingerprint |
src/Formurae/Pre/ |
parse、registry、effect analysis、Egison emitter |
src/Formurae/Post/ |
placement、stencil、geometry/backend plan、FMR AST/printer |
lib/formurae-operators.egi |
pure continuum operatorとopaque request constructor |
lib/formurae-primitives.egi |
primitive manifestから自動生成するfull-signature binding |
lib/formurae-feir.egi |
MathValue/Tensorからcanonical FEIRへのencoder |
spec/feir-primitives.sexp |
5 primitiveのfull signatureを規定する唯一のmanifest source |
spec/egison-normalization.list |
Egison normalization libraryの規範load順 |
examples/ |
model、生成artifact、C numerical check |
gallery/ |
galleryのasset(画像・動画・データ)と生成スクリプト |
html/ja/・html/en/ |
gallery・usage guideのHTML(日本語/英語) |
galleryの時間場は、初期・最終画像の補間ではなく、数値計算中に等間隔で保存した実データから
H.264動画を生成します。ffmpegを用意し、全exampleのC生成後に次を実行します。
make all
make gallery-assetsgallery/gen.shが静止画用snapshotと動画frame dataを同じrunで生成し、
render.pyが静止画、render_video.pyが全フレーム共通の色スケールで動画を描画・encodeします。
誤差曲線、厳密解比較、時空図は検証情報を同時に読める静止図のまま保持します。
変更は次の層で検査します。
make compiler-tests
make all- FEIR round-trip、malformed input、fingerprint、source diagnostic
- formurae-pre scope/effect/ambient-binding tests
- Egison analytic differentiation、FieldJet、tensor/form operator tests
- formurae-post profile、exact Taylor stencil、placement、quoted derivative、geometry-aware
Δ/δtests - collocated/Yee/DEC/variable-metric exampleのFormura parseとC numerical checks
- Egison math representative samples、mini-test全件、
cabal test
現在の受入れ基準は tests/compiler_suite.sh、個別の tests/*.sh、および Makefile の
検証targetに実行可能な形で保持します。
設計上、旧fec CLI、旧generated .egi schema、callback/marker based loweringとの後方互換性は
提供しません。仕様変更時はexample、document、testを新しい意味へ同時に更新します。
DSL-DESIGN.md: 表層構文と設計履歴html/ja/usage.html/html/en/usage.html: tutorialとusage guidehtml/ja/gallery.html/html/en/gallery.html: 検証済み応用のgalleryAPPLICATIONS.md: 応用例一覧UPSTREAM.md: Formura側の拡張計画
MIT。Formura本体とvendor sourceはそれぞれのlicenseに従います。