elab チュートリアル

このチュートリアルでは、elab パッケージで名前をカーネル項へ解決し、解決後にシグネチャが変わると何が起こるかを示す。カーネルの上に独自のフロントエンドを構築するとき、あるいはパーサが報告しうるエラー ScopeResolutionMismatch を理解したいときに使ってほしい。

クイックスタート

moon.pkg でカーネルと elab をインポートする。

import {
  "Luna-Flow/QED/kernel",
  "Luna-Flow/QED/elab",
}

x をローカル、c を宣言済みの定数として等式 $x = c$ を解決し、カーネル項へローワリングする。

test "quick start" {
  let a = @kernel.mk_tyvar("A")
  let st = @kernel.ks_add_const(@kernel.empty_kernel_state(), "c", a).unwrap()
  let ctx = @elab.elab_ctx_from_locals([("x", a)])
  let x = @elab.elab_resolve_name(st, ctx, "x").unwrap()
  let c = @elab.elab_resolve_name(st, ctx, "c").unwrap()
  let eq = @elab.elab_resolve_eq(st, ctx, x, c).unwrap()
  let t = @elab.elab_lower_to_term(eq).unwrap()
  inspect(
    @kernel.term_to_string(t),
    content="Comb(Comb(Const(= : fun(A, fun(A, bool))), Var(x : A)), Const(c#1 : A))",
  )
}

定数は c#1 として現れる。その同一性は解決時に確定している。

日常的な作業

項をボトムアップに構築する

elab_resolve_app と elab_resolve_abs は、構築しながら型を検査する。

test "bottom up" {
  let bool = @kernel.bool_ty()
  let st = @kernel.ks_add_const(@kernel.empty_kernel_state(), "neg", @kernel.fun_ty(bool, bool)).unwrap()
  let ctx = @elab.empty_elab_ctx()
  let neg = @elab.elab_resolve_name(st, ctx, "neg").unwrap()
  // λp. neg p  — the body is checked with p in scope
  let inner = @elab.elab_ctx_extend(ctx, "p", bool)
  let body = @elab.elab_resolve_app(st, inner, neg, @elab.elab_resolve_name(st, inner, "p").unwrap()).unwrap()
  let lam = @elab.elab_resolve_abs(st, ctx, "p", bool, body).unwrap()
  inspect(@elab.elab_check_core_type(st, ctx, lam, @kernel.fun_ty(bool, bool)), content="true")
  // neg applied to itself is rejected
  inspect(@elab.elab_resolve_app(st, ctx, neg, neg) is Err(@elab.CoreTypingFailure), content="true")
}

多相定数をインスタンスで使う

型変数を含む型で宣言された定数は、そのスキーマの任意のインスタンスで解決できる。

test "instances" {
  let a = @kernel.mk_tyvar("A")
  let st = @kernel.ks_add_const(@kernel.empty_kernel_state(), "default", a).unwrap()
  let rc = @elab.elab_resolve_const(st, "default", @kernel.bool_ty()).unwrap()
  inspect(@kernel.hol_type_to_string(@elab.rconst_inst_ty(rc)), content="bool")
  inspect(@kernel.hol_type_to_string(@elab.rconst_schema_ty(rc)), content="A")
  // fun(A, A) is not an instance of the schema bool -> bool of `flip`
  let bool = @kernel.bool_ty()
  let st2 = @kernel.ks_add_const(st, "flip", @kernel.fun_ty(bool, bool)).unwrap()
  let bad = @elab.elab_resolve_const(st2, "flip", @kernel.fun_ty(a, a))
  inspect(bad is Err(@elab.InvalidConstInstance("flip")), content="true")
}

スコープのずれを検出する

解決済みの項は、各定数がどの宣言を指していたかを覚えている。シャドーイングする宣言の後でもう一度検査すると、新しい定数に切り替わるのではなく失敗する。

test "scope drift" {
  let bool = @kernel.bool_ty()
  let st1 = @kernel.ks_add_const(@kernel.empty_kernel_state(), "flag", bool).unwrap()
  let ctx = @elab.empty_elab_ctx()
  let flag = @elab.elab_resolve_name(st1, ctx, "flag").unwrap()
  let st2 = @kernel.ks_add_const(@kernel.ks_push_scope(st1), "flag", bool).unwrap()
  inspect(@elab.rterm_well_formed(st2, ctx, flag), content="false")
  // resolving the name again in st2 gives the new constant
  let flag2 = @elab.elab_resolve_name(st2, ctx, "flag").unwrap()
  inspect(@elab.rterm_to_string(flag2), content="RConst(flag#2 : bool <= bool)")
  // back in the outer scope the old term is fine again
  let st3 = @kernel.ks_pop_scope(st2).unwrap()
  inspect(@elab.rterm_well_formed(st3, ctx, flag), content="true")
}

さらに進む

外部から来た項を検査する。 elab_roundtrip_term(state, ctx, t) はカーネル項を再解決し、何も変わっていないことを検査する。別の状態で構築された項が自分のコードに入ってくる境界で使う。

項を調べる。 rterm_collect_consts はすべての定数の出現をその同一性とともに列挙し、rterm_collect_free_vars はすべての自由変数を列挙する。どちらも診断に役立つ。

カーネルに渡す。 elab_lower_to_term でローワリングし、その結果をカーネル規則に渡す。解決した同一性はそのまま引き継がれ、カーネルの許容性検査がそれを改めて強制する。

代わりにパーサを使う。 テキスト入力に対しては、@parser.parse_term と @parser.parse_resolved_term がこのパッケージを代わりに実行してくれる。parser チュートリアルを参照。

よくある落とし穴

型推論を期待する。 束縛子の型は決して推論されない。elab_resolve_abs に渡すか、型付きでローカルを文脈に宣言すること。
rterm_eq で比較する。 これは束縛名も比較するため、α 同値な項でも異なりうる。両方をローワリングして @kernel.term_alpha_eq を使うこと。
拡張後に文脈を再利用する。 elab_ctx_extend は新しい文脈を返し、古い文脈は変わらない。束縛子を抜けるときにはまさにこれが望ましい。
状態の中に = を探す。 等号は組み込みであり、宣言なしで解決される。宣言することもシャドーイングすることもできない。

次のステップ

elab API には、すべての関数とエラーが列挙されている。
elab 設計は凍結の性質と、それが成り立つ理由を述べる。
parser チュートリアルは、このパッケージの上に構築されたテキストフロントエンドを示す。