SATySFi の導出木描画ライブラリ satysfi-derive

最近 [satysfi-derive](https://github.com/yabaitechtokyo/satysfi-derive) というライブラリを Satyrographos で公開しました。もともと [satysfi-base](https://github.com/nyuichi/satysfi-base) の一部だったものを独立したライブラリとして切り分けたものになります。機能としてはsatysfi-baseの一部だった頃([当時の記事](https://qiita.com/zptmtr/items/6bbbacb18000e9be4889))からあまり変わっていないのですが、細かい部分がアップデートされているため新しく紹介記事を書いています。

# これは何？
satysfi-derive は[組版処理システム SATySFi](https://github.com/gfngfn/SATySFi/blob/master/README-ja.md) で導出木を書くためのコマンドとDSLを提供するライブラリです。SATySFi 及び LaTeX の既存のライブラリと比較して以下の点を特徴とします。

* 可読性の高いDSLで導出木を書ける
* 組版の設定を柔軟に変更できる
* 回帰テストでコードの品質を担保している

例えば以下のコードをコンパイルすると

```ml
@require: math
@require: base/typeset/satysfi-it
@require: derive/derive

open Derive in
satysfi-it ${
  \proven!(
    open DeriveDSL in
    derive ${ \vdash A \wedge \paren {B \vee C} }
    |> by { ${\wedge} I }
    |> from [
        assume ${ \vdash A };
        derive ${ \vdash B \vee C }
        |> by { ${\vee} I }
        |> from [
          assume ${ \vdash B };
        ];
    ]
  )
}
```

以下のような導出木が描画されます。

![tldr.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/d0ec6537-a634-f690-8537-1e68d60a2164.png)


# インストール方法
Satyrographos でインストールできます。

```
$ opam install satysfi-derive
$ satyrogaraphos install -l derive
```

# 使い方
## 導出木を書く
satysfi-derive 関連のモジュールを使用するためには `@require derive/derive` をファイルの先頭に書いてください。

導出木を描画するためには数式モード中で `\Derive.proven` コマンドを使います。コードの最初の方で`Derive`モジュールをopenしておくと単に`\proven`と書くことができます。

```
% 数式モード
\proven!(derivation)
```
(`!(...)`は数式モードからプログラムモードへ切り替えるための構文です。)

ここで引数の `derivation` は導出木の内容を表す`DeriveAst.t`型の値です。`DeriveAst.t`の値を構築するためのDSLを`DeriveDSL`モジュールが提供しているのでこれを使いましょう。`DeriveDSL`が提供している関数は以下の通りです。

* `derive`
* `from`
* `assume`
* `by`
* `byOp`
* `withLine`

### 導出木をつくる
`derive` が一番基本的な関数で、`derive ${math}`で前提部が空で結論部が`${math}`の導出木を構築します。基本的に導出木を構築する際には`derive`から始めることになると思います。

```ml:deriveの使用例
derive ${A \wedge B}
```

![derive の描画結果](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/4dc67cbe-cb35-7daa-ab06-9f4f40b953cd.png)

### 前提を設定する
`derivation |> from [derivation1; derivation2; ...]`は`derivation`の前提部を`derivation1`, `derivation2`...それぞれに対応する導出木に設定します。

```ml:fromの使用例
derive ${A \wedge B}
|> from [
  derive ${A};
  derive ${B};
]
```
![fromを使った描画結果](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/a38ac996-81ce-67b9-dadc-6de7d111769b.png)

### 仮定をつくる
`assume` は `derive` の亜種で、`derive`が実線を描画していたのに対して`assume`は線を描画しません。ある導出木が仮定である場合は`assume`を使った方が適切でしょう。

```ml:assumeの使用例
derive ${A \wedge B}
|> from [
  assume ${A};
  assume ${B};
]
```
![assumeの描画結果](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/dfd95d2b-1c07-d87c-2a31-a362939febd2.png)

### ラベルの設定
`derivation |> by {label}` は導出木のラベルを設定します。

```ml:byの使用例
derive ${A \wedge B}
|> by {${\wedge}-intro}
|> from [
  assume ${A};
  assume ${B};
]
```
![byの描画結果](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/939cd4e9-d13d-aadf-c019-6ad99c572df9.png)


`derivation |> byOp {label}` も導出木のラベルを設定しますが、ラベルの表示場所が`by`と反対側になります。

```ml:byOpの使用例
derive ${A \wedge B}
|> by {${\wedge}-intro}
|> byOp {(1)}
|> from [
  assume ${A};
  assume ${B};
]
```
![byOpの描画結果](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/f425fc19-7398-f57c-738c-1156a01522d3.png)

### 線の変更
`derivation |> withLine line` は導出の線がどのように描画されるかを明示的に設定します。`line`には`DeriveLine.t`型の値が使えますが、`DeriveDSL`で用意されているものは以下の三つです。

* `standard-line`: 実線
* `no-line`: 線なし
* `dotted-line dot-len spacing`: 点線(点の長さが`dot-len`、空白の長さが`spacing`)

`standard-line`と`no-line`は`derive`と`assume`でそれぞれデフォルトで使われているので、`withLine`を使うのは`dotted-line`を使いたい場合になるでしょう。他の線を自前で定義したい場合には `DeriveLine.make` ([ドキュメント](https://github.com/yabaitechtokyo/satysfi-derive/blob/main/src/line.satyh#L8-L11)) を使うことを検討してください。

```ml:withLineの使用例
derive ${A \wedge B}
|> withLine (dotted-line 2pt 1pt)
```
![dotted-lineの描画結果](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/92fb29fd-a5ca-bbab-b305-f979b252b8e1.png)

## レイアウトを調整する
`DeriveConfig` モジュール([ソースコード](https://github.com/yabaitechtokyo/satysfi-derive/blob/main/src/config.satyh))を使うことで細かいレイアウトを調整することができます。具体的には以下のプロパティを調整することが可能です。

* main-label-position: `by`でラベルがどちら側に配置されるか 
* default-line: `derive`で使われる線
* line-vertical-margin: 下図の1。線と結論・前提との間。
* line-horizontal-margin: 下図の2。線と左右のラベルとの間。
* assumption-spacing: 下図の3。前提同士の間。
* line-thickness: 下図の4。線の厚さ。
* content-padding: 下図の5。結論部と前提部のパディング(線の長さに影響します)

![レイアウトのプロパティ](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/6655854f-a7e9-d578-c905-70e5b6f1e9b1.png)

特に設定をしなければ `DeriveConfig.default`がデフォルトの設定として使われます。自前の設定を使いたい際には`\proven`のオプショナル引数を用いてください。

```ml:DeriveConfigの使用例
open Derive in
let my-derive-config = open DeriveConfig in
    default
    |> set-main-label-position LabelRight
    |> set-default-line (DeriveLine.dotted-line 5pt 5pt)
    |> set-line-vertical-margin 10pt
    |> set-line-horizontal-margin 10pt
    |> set-bar-thickness 10pt
    |> set-assumption-spacing 30pt
in
...
${
  \proven ?:!(my-derive-config) !(
    open DeriveDSL in
    derive ${ \Gamma \vdash \Delta }
    |> by {Cut}
    |> from [
      assume ${\Gamma \vdash \Delta, A};
      assume ${\Gamma, A \vdash \Delta}
    ]
  )
}
```

# まとめと宣伝
以上がsatysfi-deriveの紹介です。我ながら便利なものを作れたと思っているので、ドシドシ使ってフィードバックをもらえると嬉しいです。要望等があれば [Issue を立ててください](https://github.com/yabaitechtokyo/satysfi-derive/issues)。

ところで私の所属している同人誌サークル yabaitech.tokyo が技術書典10で新刊 [yabaitech.tokyo vol.6](https://techbookfest.org/product/5260858349322240?productVariantID=4971089992089600) を販売中です。興味があれば買っていただけると嬉しいです！既刊の[yabaitech.tokyo vol.3](https://techbookfest.org/product/5191254740566016)の「真矛盾主義入門」では実際に導出木を satysfi-derive (の前身のコード) を用いて導出木を組版しています。こちらも興味があれば是非🙇

それでは皆さん、快適なSATySFiライフを楽しんでください👋