elab API

elab パッケージ(Luna-Flow/QED/elab)は、名前とカーネルの間の解決の境界である。項の各名前をローカル文脈とカーネル状態に対して一度だけ解決し、定数がカーネル上の同一性を持つ解決済み項 RTerm にする。解決済み項を状態に対して型検査し、カーネル項へローワリングする。また、型検査付きでカーネル項を構築する薄いビルダーも提供する。kernel のみに依存し、定理は生成しない。

凍結された同一性の背後にある設計は elab 設計ノートにあり、elab チュートリアルでは解決とスコープの変更を順に解説する。

文脈

`ElabCtx`

ElabCtx はローカル文脈であり、変数名とその型の順序付きリストで、最も内側が末尾に来る。

pub struct ElabCtx {
  locals : Array[(String, @kernel.HolType)]
}

`empty_elab_ctx`、`elab_ctx_from_locals`、`elab_ctx_extend`

これらの関数は文脈を構築する。elab_ctx_extend はローカルを 1 つ追加した新しい文脈を返し、引数は変更されない。

pub fn empty_elab_ctx() -> ElabCtx
pub fn elab_ctx_from_locals(Array[(String, @kernel.HolType)]) -> ElabCtx
pub fn elab_ctx_extend(ElabCtx, String, @kernel.HolType) -> ElabCtx

同じ名前を持つ後のローカルは、先のローカルをシャドーイングする。

解決済み項

`ResolvedConst`

ResolvedConst は、解決時に凍結された定数の出現である。

pub struct ResolvedConst {
  name : String
  const_id : Int
  inst_ty : @kernel.HolType
  schema_ty : @kernel.HolType
}

const_id は名前が解決された先のカーネル上の同一性、schema_ty はその時点で宣言されていたスキーマ、inst_ty はこの出現の型であり schema_ty のインスタンスである。組み込みの等号は const_id == -1 で、スキーマは $\alpha \to \alpha \to \mathit{bool}$ である。

`RTerm`

RTerm は解決済み項であり、すべての定数が ResolvedConst である名前付きの項である。

pub enum RTerm {
  RVar(String, @kernel.HolType)
  RConst(ResolvedConst)
  RComb(RTerm, RTerm)
  RAbs(String, @kernel.HolType, RTerm)
}

`rterm_var`、`rterm_const`、`rterm_comb`、`rterm_abs`

これらの関数は、検査なしで解決済み項を構築する。

pub fn rterm_var(String, @kernel.HolType) -> RTerm
pub fn rterm_const(ResolvedConst) -> RTerm
pub fn rterm_comb(RTerm, RTerm) -> RTerm
pub fn rterm_abs(String, @kernel.HolType, RTerm) -> RTerm

`rconst_name`、`rconst_id`、`rconst_inst_ty`、`rconst_schema_ty`

これらの関数は ResolvedConst のフィールドを読み出す。

pub fn rconst_name(ResolvedConst) -> String
pub fn rconst_id(ResolvedConst) -> Int
pub fn rconst_inst_ty(ResolvedConst) -> @kernel.HolType
pub fn rconst_schema_ty(ResolvedConst) -> @kernel.HolType

`rterm_eq`

rterm_eq は解決済み項の構造的等価性であり、束縛名と定数の同一性を含む。α 同値ではない。

pub fn rterm_eq(RTerm, RTerm) -> Bool

`rterm_collect_free_vars` と `rterm_collect_consts`

rterm_collect_free_vars は解決済み項の自由変数を、出現順に重複を含めて列挙する。rterm_collect_consts はすべての定数の出現を列挙する。

pub fn rterm_collect_free_vars(RTerm) -> Array[(String, @kernel.HolType)]
pub fn rterm_collect_consts(RTerm) -> Array[ResolvedConst]

`rterm_to_string`

rterm_to_string は解決済み項を整形する。定数は RConst(name#id : inst <= schema) の形で出力される。

pub fn rterm_to_string(RTerm) -> String

解決

`elab_resolve_name`

elab_resolve_name(state, ctx, name) は名前を解決する。ctx にローカルがあればそれに、なければ state で可視な定数をそのスキーマ型で解決する。ローカルは定数より優先される。

pub fn elab_resolve_name(@kernel.KernelState, ElabCtx, String) -> Result[RTerm, ElabError]

名前がどちらでもない場合は UnknownName(name) で失敗する。

`elab_resolve_const`、`elab_resolve_const_by_name`、`elab_resolve_const_instance`

これらの関数は定数を解決する。elab_resolve_const(state, name, ty) は型 ty での出現を解決し、elab_resolve_const_by_name はスキーマ型を用い、elab_resolve_const_instance は結果を RConst で包む。

pub fn elab_resolve_const(@kernel.KernelState, String, @kernel.HolType) -> Result[ResolvedConst, ElabError]
pub fn elab_resolve_const_by_name(@kernel.KernelState, String) -> Result[ResolvedConst, ElabError]
pub fn elab_resolve_const_instance(@kernel.KernelState, String, @kernel.HolType) -> Result[RTerm, ElabError]

名前 = は常に組み込みの等号に解決される。失敗は次のとおり。何も宣言されていなければ UnknownConst(name)、型がスキーマのインスタンスでなければ InvalidConstInstance(name)、状態の同一性テーブルとスキーマテーブルが食い違っていれば ScopeResolutionMismatch。

`elab_resolve_var`

elab_resolve_var は文脈を参照せずに解決済みの変数を構築する。

pub fn elab_resolve_var(String, @kernel.HolType) -> RTerm

`elab_resolve_app`、`elab_resolve_abs`、`elab_resolve_eq`

これらの関数は、解決済みの部品から適用、抽象、等式を構築し、結果を状態と文脈に対して型検査する。

pub fn elab_resolve_app(@kernel.KernelState, ElabCtx, RTerm, RTerm) -> Result[RTerm, ElabError]
pub fn elab_resolve_abs(@kernel.KernelState, ElabCtx, String, @kernel.HolType, RTerm) -> Result[RTerm, ElabError]
pub fn elab_resolve_eq(@kernel.KernelState, ElabCtx, RTerm, RTerm) -> Result[RTerm, ElabError]

結果が型付けできない場合は CoreTypingFailure で失敗する。elab_resolve_abs では、本体は束縛子で拡張した ctx で検査される。

`elab_resolve_named_term` と `elab_roundtrip_term`

elab_resolve_named_term(state, ctx, t) は既存のカーネル項を解決する。自由変数は同じ型の ctx のローカルでなければならず、定数は state で名前により改めて検索される。elab_roundtrip_term はさらに結果をローワリングし、定数の同一性を含めて t と α 同値であることを検査する。

pub fn elab_resolve_named_term(@kernel.KernelState, ElabCtx, @kernel.Term) -> Result[RTerm, ElabError]
pub fn elab_roundtrip_term(@kernel.KernelState, ElabCtx, @kernel.Term) -> Result[RTerm, ElabError]

t の定数が別の同一性に解決されるようになった場合、elab_roundtrip_term は ScopeResolutionMismatch で失敗する。これは、あるスコープで構築された項が、シャドーイングする宣言の後で検出される仕組みである。

test "resolve" {
  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()
  inspect(@elab.rterm_to_string(c), content="RConst(c#1 : A <= A)")
  let eq = @elab.elab_resolve_eq(st, ctx, x, c).unwrap()
  inspect(@elab.elab_check_core_type(st, ctx, eq, @kernel.bool_ty()), content="true")
  inspect(@elab.elab_resolve_name(st, ctx, "nope") is Err(@elab.UnknownName("nope")), content="true")
  // a local named like a constant wins
  let ctx2 = @elab.elab_ctx_extend(ctx, "c", @kernel.bool_ty())
  inspect(@elab.elab_resolve_name(st, ctx2, "c") is Ok(@elab.RVar("c", _)), content="true")
}

コア型付け

`elab_core_type_of`、`elab_check_core_type`、`rterm_well_formed`

elab_core_type_of(state, ctx, t) は解決済み項の型を計算する。変数は同じ型の ctx のローカルでなければならず、定数は state で同じ同一性とスキーマを持ち続けていて、その型がスキーマのインスタンスでなければならない。elab_check_core_type は結果を期待される型と比較し、rterm_well_formed は型が存在するかを検査する。

pub fn elab_core_type_of(@kernel.KernelState, ElabCtx, RTerm) -> @kernel.HolType?
pub fn elab_check_core_type(@kernel.KernelState, ElabCtx, RTerm, @kernel.HolType) -> Bool
pub fn rterm_well_formed(@kernel.KernelState, ElabCtx, RTerm) -> Bool

コア型付けは名前を再検索しない。凍結された同一性がもはや有効なものでなければ、新しい定数を拾うのではなく型付けが失敗する。

ローワリング

`elab_lower_to_term` と `elab_lower_to_db`

elab_lower_to_term は解決済み項を、すべての定数の同一性を保ったままカーネル項に変換する。elab_lower_to_db はさらにカーネルの de Bruijn 形式まで進める。

pub fn elab_lower_to_term(RTerm) -> Result[@kernel.Term, ElabError]
pub fn elab_lower_to_db(RTerm) -> Result[@kernel.DbTerm, ElabError]

どちらも、ローワリングされた項が型付けできない場合や変換できない場合に CoreTypingFailure で失敗する。

test "freeze" {
  let bool = @kernel.bool_ty()
  let st1 = @kernel.ks_add_const(@kernel.empty_kernel_state(), "c", bool).unwrap()
  let ctx = @elab.empty_elab_ctx()
  let c1 = @elab.elab_resolve_name(st1, ctx, "c").unwrap()
  // a shadowing declaration in an inner scope
  let st2 = @kernel.ks_add_const(@kernel.ks_push_scope(st1), "c", bool).unwrap()
  inspect(@elab.rterm_well_formed(st1, ctx, c1), content="true")
  inspect(@elab.rterm_well_formed(st2, ctx, c1), content="false")
  // the lowered term keeps the identity resolved in st1
  let t = @elab.elab_lower_to_term(c1).unwrap()
  inspect(@kernel.term_to_string(t), content="Const(c#1 : bool)")
  inspect(@elab.elab_roundtrip_term(st2, ctx, t) is Err(@elab.ScopeResolutionMismatch), content="true")
}

カーネル項ビルダー

これらの関数は、解決済み項を必要としない呼び出し側のために、型検査付きでカーネルの Term 値を直接構築する。

`elab_var`、`elab_const`、`elab_const_instance`

elab_var は mk_var である。elab_const と elab_const_instance は、それぞれ ks_mk_const と ks_mk_const_instance である。

pub fn elab_var(String, @kernel.HolType) -> @kernel.Term
pub fn elab_const(@kernel.KernelState, String) -> Result[@kernel.Term, @kernel.SigError]
pub fn elab_const_instance(@kernel.KernelState, String, @kernel.HolType) -> Result[@kernel.Term, @kernel.SigError]

`elab_app`、`elab_app2`、`elab_abs`、`elab_eq`

これらの関数は適用(引数 1 つまたは 2 つ)、抽象、等式を構築し、結果が型付けできない場合は TypeMismatch で失敗する。

pub fn elab_app(@kernel.Term, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]
pub fn elab_app2(@kernel.Term, @kernel.Term, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]
pub fn elab_abs(String, @kernel.HolType, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]
pub fn elab_eq(@kernel.Term, @kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]

`elab_is_prop` と `elab_require_prop`

elab_is_prop は項が型付けされた命題かどうかを検査する。elab_require_prop は項を返すか、NotBoolTerm で失敗する(型付けできない場合は TypeMismatch)。

pub fn elab_is_prop(@kernel.Term) -> Bool
pub fn elab_require_prop(@kernel.Term) -> Result[@kernel.Term, @kernel.LogicError]

test "builders" {
  let a = @kernel.mk_tyvar("A")
  let f = @elab.elab_var("f", @kernel.fun_ty(a, @kernel.bool_ty()))
  let x = @elab.elab_var("x", a)
  let fx = @elab.elab_app(f, x).unwrap()
  inspect(@elab.elab_is_prop(fx), content="true")
  inspect(@elab.elab_app(x, f) is Err(@kernel.TypeMismatch), content="true")
  inspect(@elab.elab_require_prop(x) is Err(@kernel.NotBoolTerm), content="true")
}

エラー

`ElabError`

ElabError は解決とローワリングのエラーである。

pub enum ElabError {
  UnknownName(String)
  UnknownConst(String)
  InvalidConstInstance(String)
  ScopeResolutionMismatch
  CoreTypingFailure
}

コンストラクタ	意味
`UnknownName(name)`	名前がローカルでも可視な定数でもない。
`UnknownConst(name)`	この名前の定数は宣言されていない。
`InvalidConstInstance(name)`	要求された型が定数のスキーマのインスタンスではない。
`ScopeResolutionMismatch`	凍結された同一性が状態と一致しなくなった、または状態のテーブルが食い違っている。
`CoreTypingFailure`	解決済み項が、現在の状態と文脈で型付けできない。

`elab_err_unknown_name`、`elab_err_unknown_const`、`elab_err_invalid_const_instance`、`elab_err_scope_resolution_mismatch`、`elab_err_core_typing_failure`

これらの述語は、ElabError がどのコンストラクタであるかを検査する。パターンよりも関数を好む呼び出し側向けである。

pub fn elab_err_unknown_name(ElabError) -> Bool
pub fn elab_err_unknown_const(ElabError) -> Bool
pub fn elab_err_invalid_const_instance(ElabError) -> Bool
pub fn elab_err_scope_resolution_mismatch(ElabError) -> Bool
pub fn elab_err_core_typing_failure(ElabError) -> Bool

elab API

文脈

ElabCtx

empty_elab_ctx、elab_ctx_from_locals、elab_ctx_extend

解決済み項

ResolvedConst

RTerm

rterm_var、rterm_const、rterm_comb、rterm_abs

rconst_name、rconst_id、rconst_inst_ty、rconst_schema_ty

rterm_eq

rterm_collect_free_vars と rterm_collect_consts

rterm_to_string

解決

elab_resolve_name

elab_resolve_const、elab_resolve_const_by_name、elab_resolve_const_instance

elab_resolve_var

elab_resolve_app、elab_resolve_abs、elab_resolve_eq

elab_resolve_named_term と elab_roundtrip_term