プロジェクト・テスト・ツール

大きなプログラムに育てるときの、基本の作業を見ます。

12.1 ファイルの分割と import

小さなプログラムは、一つの .taut ファイルで十分です。大きくなったら src/ の中で分割します。取り込みは、そのファイルからの相対パスです。

src/math.taut

pub fn add(a: i64, b: i64): i64 {
  a + b
}

✓ 検査を通過

・ add

src/main.taut

import "math.taut" { add }

let x := add(20, 22)
perform show("result", x)

実行結果

result = 42

tauto run --tote .

result = 42

src/ は暗黙のソースルートです。追加のソースルートは、マニフェスト Tauto.eure の additional-sources に指定します。標準ライブラリを読み込むときも、同じ import を使います（第 6 章）。

12.2 普段使うコマンド

コマンド	何をするか
`tauto init PATH`	新しいプロジェクトを作る
`tauto run --tote .`	プロジェクトを評価する
`tauto check FILE`	実行側の型・効果・所有権と、証明宣言を検査する
`tauto check FILE --fresh`	キャッシュを使わずに検査し直す
`tauto fmt FILE`	ソースコードを整形する
`tauto lint FILE`	スタイル上の規則を検査する
`tauto test PATH`	ソースルートと `cases/` のテストを実行する
`tauto doc PATH`	ローカルの HTML ドキュメントを作る

tauto fmt は 2 スペースのインデントに整形します。この本のコードも、それに合わせています。

tauto check は、命題の証明と、実行するプログラムの型・effect・所有権を検査します。 skipped は、その宣言が証明カーネルの対象ではないことを表し、プログラム側の検査まで省略したという意味ではありません。実際の値や副作用は run とテストで確認します。

12.3 テスト

tauto test は、プロジェクトのソースルート（src/ と additional-sources に書いたディレクトリ）にあるテストと、cases/ を実行します。tests/ にテストを置くときは、Tauto.eure の additional-sources に "tests" を加えます。

Tauto.eure

package {
  name = "add"
  version = "0.1.0"
  additional-sources = ["tests"]
}

テストは perform test(名前, () => expect(条件, 失敗時のメッセージ)) と書きます。テストのファイルは、まず証明検査を通り（穴が残っていてはいけません）、次に評価されます。show や stdout（import std::prelude::Os で使える）は表明（アサーション）ではありません。出力の期待値は、Eure の case ファイルに書きます。

tests/add.taut

import "../src/math.taut" { add }

theorem add_ok(): 2 + 2 = 4 {
  Refl
}

perform test("add", () => expect(add(20, 22) == 42, "add(20, 22) should be 42"))

// 証明した等式の定理と、実行して確かめるテストを組み合わせる

実行結果

✓ theorem add_ok : 2 + 2 = 4

test add ... ok

tauto test .

passed tests/add.taut::add
1 passed; 0 failed

expect の条件が偽になると、failed tests/add.taut::add: add(20, 22) should be 42 のように、テスト名とメッセージが表示されます。

12.4 証明を支援するコマンド

証明の途中では、まだ証明されていない命題（ゴール）を確認できます。証明の一部を、名前付きの穴 ?name にしておきます。

ch12-holes.taut

theorem and_comm(A: Prop, B: Prop, p: A ∧ B): B ∧ A {
  AndIntro(?right, ?left)
}

… 残っているゴール

… theorem and_comm : ∀ A: Prop. ∀ B: Prop. (And(A, B)) -> And(B, A)

?right  (2:12)
  A : Prop
  B : Prop
  p : And(A, B)
⊢ B

?left  (2:20)
  A : Prop
  B : Prop
  p : And(A, B)
⊢ A

穴を含む宣言は、受理されません。INCOMPLETE と報告され、終了コードは 3 です（sorry のような抜け道はありません）。

tauto check ch12-holes.taut
tauto goals ch12-holes.taut

INCOMPLETE and_comm (?right, ?left)
?right in and_comm (ch12-holes.taut:2:15)
  A : Prop
  B : Prop
  p : And(A, B)
⊢ B
?left in and_comm (ch12-holes.taut:2:23)
  A : Prop
  B : Prop
  p : And(A, B)
⊢ A

穴に式を入れて検査だけしてみるのが tauto try、実際にファイルへ書き込むのが tauto fill です。

tauto try ch12-holes.taut --hole right --with 'And::right(p)'
tauto fill ch12-holes.taut --hole right --with 'And::right(p)'
tauto fill ch12-holes.taut --hole left --with 'And::left(p)'
tauto check ch12-holes.taut

ok      and_comm

ほかにも、検査結果を JSON で受け取る tauto check FILE --json（各宣言が使った公理も含みます）、使える定理や構成子の一覧を出す tauto library FILE、穴に合う候補を探す tauto suggest FILE --hole NAME があります。

演習 12.1：プロジェクトを一つ作って、fmt・run・test・check を使い分けてみましょう。