Luna Flow
日本語

cmd API

cmd パッケージ(Luna-Flow/QED/cmd)は、コマンドラインツール qed-cmd である。定理スクリプトファイルを 1 つ読み込み、その中のすべての定理を prover パッケージで検査し、定理ごとにレポートを 1 つ出力して、ステータスコードで終了する。実行可能パッケージ(moon.pkg の pkgtype(kind: "executable"))であるため、他のパッケージからインポートすることはできない。公開関数はツールのテスト対象となる表面であり、保守者向けにここに列挙する。

cmd チュートリアルではツールを順に解説し、cmd 設計ノートでは出力契約を説明する。出力契約の全体はユーザーマニュアルにもある。

コマンドライン

qed-cmd

qed-cmd は定理スクリプトファイルを検査する。

qed-cmd [-d] [--no-warn] <file>
引数意味
<file>定理スクリプトファイル。定理は qed だけの行で区切られる。定理が 1 つだけのファイルでは省略してよい。
-d証明された各定理の名前の後に結論を出力する。
--no-warn未完了の証明があってもエラーがなければ 0 で終了する。警告は引き続き出力される。

リポジトリからは moon run で実行する。ツールへの引数は -- の後に置く。

moon run src/cmd examples/truth_file.qed
moon run src/cmd -- -d --no-warn examples/multi_with_hole.qed

未知のオプション、ファイル引数の欠落、2 つ目のファイル引数がある場合は、使用法の行を出力して 1 で終了する。

出力

各定理につき、ファイルの順に 1 ブロックが出力される。

結果出力
証明済みok <name>。-d を付けた場合は ok <name>: <conclusion>
失敗error[<kind>] <file> (<name>): <detail>。失敗に証明の文脈がある場合は、続けて step:、branch:、goal:、locals: の行が出力される
未完了warning[unfinished] <file> (<name>): <detail>。続けて theorem:、step:、branch:、goal:、locals:、hole:、message: の行が出力される

<kind> は usage、io、parse、bridge、tactic、sig、logic のいずれかである。分岐パスは 1.1 のように出力され、空のパスは <root>、存在しない値は <none> と出力される。ゴールとローカルは、カーネルの構造的な項プリンタで出力される。

終了ステータス

ステータス条件
0すべての定理が証明された、または未完了の証明のみがあり --no-warn が指定された。
1使用法または I/O のエラー、構文解析できないファイル、失敗した定理、あるいは --no-warn なしの未完了の証明。

オプション

CmdOptions

CmdOptions は実行の設定を保持する。命題論理のプレリュードをインストールするか、結論を出力するか、警告だけの場合に 0 で終了するかである。

pub struct CmdOptions {
  auto_install_prelude : Bool
  detailed_success : Bool
  no_warn : Bool
}

default_cmd_options、cmd_options、cmd_options_with_detail、cmd_options_full

これらの関数はオプションを構築する。default_cmd_options() はプレリュードをインストールし、2 つのフラグをオフにする。それ以外の関数は 1 つ、2 つ、または 3 つのフィールドを設定する。

pub fn default_cmd_options() -> CmdOptions
pub fn cmd_options(Bool) -> CmdOptions
pub fn cmd_options_with_detail(Bool, Bool) -> CmdOptions
pub fn cmd_options_full(Bool, Bool, Bool) -> CmdOptions

実行

cmd_run_argv

cmd_run_argv(args, opts) はコマンドライン(args[0] はプログラム名)を解析し、ファイルを読み込んで検査する。コマンドライン上のフラグは、opts の対応するフィールドを上書きする。

pub fn cmd_run_argv(Array[String], CmdOptions) -> CmdRunResult

cmd_run_script

cmd_run_script(path, src, opts) は、ソーステキスト src が path から読み込まれたかのように、空のカーネル状態から検査する。

pub fn cmd_run_script(String, String, CmdOptions) -> CmdRunResult

cmd_render_result と cmd_exit_code

cmd_render_result はツールが出力するテキストを、cmd_exit_code は終了ステータスを、上述のとおりに生成する。

pub fn cmd_render_result(CmdRunResult) -> String
pub fn cmd_exit_code(CmdRunResult) -> Int

結果

CmdRunResult

CmdRunResult は、検査できたファイルについては定理ごとのレポートであり、そうでない場合は実行全体に対する単一の失敗(使用法、I/O、構文解析)または未完了の結果である。

pub enum CmdRunResult {
  FileReport(CmdFileReport)
  Failure(CmdFailure)
  Unfinished(CmdUnfinished)
}

CmdFileReport と CmdFileItem

ファイルレポートは定理ごとに 1 項目を列挙し、2 つの出力フラグを保持する。

pub struct CmdFileReport {
  path : String
  items : Array[CmdFileItem]
  detailed_success : Bool
  no_warn : Bool
}

pub enum CmdFileItem {
  CmdItemSuccess(CmdSuccess)
  CmdItemFailure(CmdFailure)
  CmdItemWarning(CmdUnfinished)
}

CmdSuccess

CmdSuccess は証明された定理であり、その名前、結論、および整形された結論を持つ。

pub struct CmdSuccess {
  path : String
  theorem_name : String
  conclusion : @kernel.Term
  conclusion_summary : String
}

CmdFailure と CmdFailureKind

CmdFailure は、位置と文脈を文字列として整形した失敗である。CmdFailureKind はその発生元を表す。

pub struct CmdFailure {
  path : String
  theorem_name : String?
  kind : CmdFailureKind
  step_index : Int?
  branch_path : Array[Int]
  current_goal_summary : String?
  local_hyps : Array[CmdLocalHypSummary]
  detail : String
}

pub enum CmdFailureKind {
  Usage
  Io
  Parse
  Bridge
  Tactic
  Sig
  Logic
}

cmd_failure_kind_to_string

cmd_failure_kind_to_string は、error[...] の中に出力される小文字の種別を返す。

pub fn cmd_failure_kind_to_string(CmdFailureKind) -> String

CmdUnfinished、cmd_unfinished、cmd_unfinished_from_prover

CmdUnfinished は、文脈を文字列として整形した未完了の証明である。cmd_unfinished はそれを実行結果として構築し、cmd_unfinished_from_prover は prover のレポートを変換する。

pub struct CmdUnfinished {
  path : String
  theorem_name : String
  step_index : Int?
  branch_path : Array[Int]
  current_goal_summary : String
  local_hyps : Array[CmdLocalHypSummary]
  hole_name : String?
  detail : String
}

pub fn cmd_unfinished(String, String, Int?, Array[Int], String, Array[CmdLocalHypSummary], String?, String) -> CmdRunResult
pub fn cmd_unfinished_from_prover(String, @prover.ProverUnfinished) -> CmdRunResult

CmdLocalHypSummary

CmdLocalHypSummary は出力用に整形されたローカルな仮定であり、name: term の形で出力される。

pub struct CmdLocalHypSummary {
  name : String
  term_summary : String
}