parser API リファレンス

parser パッケージ (Luna-Flow/QED/parser) はテキストのフロントエンドである。入力を正規化し、項、ゴール、定理スクリプトを元のテキスト中の位置を保持した構文木にパースし、elab と logic パッケージを通じて項とゴールをカーネルの項へローワリングする。タクティクのオブジェクトは持たない。パースされたゴールはパーサが所有する ParsedGoal であり、prover がこれをタクティク層へ橋渡しする。

_raw で終わる関数はパースのみを行う。それ以外は、名前の解決と KernelState に対するカーネル項の構築も行う。表層構文は構文ガイドにまとめられている。その背後にある選択はパーサの設計にあり、パーサチュートリアルではパースとローワリングを段階的に行う。

入力の正規化

NormalizedInput

NormalizedInput は、正規化されたテキストと、生の入力への対応表の組である。

pub struct NormalizedInput {
  text : String
  raw_offsets : Array[Int]
  raw_length : Int
}

raw_offsets[i] は text の i 番目の文字の生の入力におけるオフセットであり、raw_length は生の入力の長さである。

normalize_parser_input

normalize_parser_input は、互換用の綴りを正準の綴りに書き換え、連続する空白をまとめる。

pub fn normalize_parser_input(String) -> Result[NormalizedInput, ParseError]

\not、\and、\or、\imp はそれぞれ ¬、∧、∨、-> になり、|- は ⊢ になる。旧来の綴り /\ と \/ は受理されない。すべてのパース関数が最初にこれを呼び出す。

normalized_input_raw_offset_at

normalized_input_raw_offset_at(input, i) は、正規化されたテキスト中のオフセットを生の入力へ対応づける。

pub fn normalized_input_raw_offset_at(NormalizedInput, Int) -> Int

ParseError とソーススパンのオフセットはすでに元に戻されているため、エラー位置は常にユーザが入力したものを指す。

SourceSpan と source_span

SourceSpan は生のオフセットの半開区間である。source_span(start, end) はそれを構築し、負の start は 0 に、start より前の end は start に丸める。

pub struct SourceSpan {
  start_offset : Int
  end_offset : Int
}

pub fn source_span(Int, Int) -> SourceSpan

test "normalise" {
  let n = @parser.normalize_parser_input("p  \\and  q |- r").unwrap()
  inspect(n.text, content="p ∧ q ⊢ r")
  // `∧` (offset 2 in the normalised text) came from `\and` at offset 3
  inspect(@parser.normalized_input_raw_offset_at(n, 2), content="3")
  let sp = @parser.source_span(5, 2)
  assert_eq((sp.start_offset, sp.end_offset), (5, 5))
}

エラー

ParseError と ParseErrorCode

ParseError は、生のオフセットにおける構文エラーであり、人間が読める詳細を伴う。

pub struct ParseError {
  code : ParseErrorCode
  offset : Int
  detail : String
}

pub enum ParseErrorCode {
  UnexpectedToken
  UnexpectedEof
  MissingTurnstile
  NonAssocChain
  UnknownOperator
  EmptyConclusion
  EmptyHypothesis
}

コード	意味
UnexpectedToken	ここに現れ得ないトークン。項中の生の forall や未知のステップキーワードを含む。
UnexpectedEof	入力が構文の途中で終わった。
MissingTurnstile	ゴールに ⊢ がない。
NonAssocChain	非結合的な演算子 = による a = b = c のような連鎖。
UnknownOperator	結合優先度表にない演算子。
EmptyConclusion	ゴールの ⊢ の後に何もない。
EmptyHypothesis	ゴールのコンマの間に空の仮定がある。

ParseBridgeError

ParseBridgeError は、パースとローワリングを行う関数のエラーであり、構文エラー、またはカーネルもしくはリゾルバからのエラーである。

pub enum ParseBridgeError {
  Parse(ParseError)
  Sig(@kernel.SigError)
  Logic(@kernel.LogicError)
  Elab(@elab.ElabError)
}

ローカルでも宣言済みの定数でもない名前は Sig(UnknownConst) を報告し、命題でないものに適用された結合子は Logic(NotBoolTerm) を報告する。

ローカル環境

ParseEnv

ParseEnv は、パーサから見えるローカル変数のリストであり、最も内側が最後に来る。

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

名前はローカルが先、次に定数の順で解決される。

empty_parse_env、parse_env_push_local、parse_env_local_count と parse_env_local_at

これらの関数は環境を構築および読み出す。parse_env_push_local は新しい環境を返す。

pub fn empty_parse_env() -> ParseEnv
pub fn parse_env_push_local(ParseEnv, String, @kernel.HolType) -> ParseEnv
pub fn parse_env_local_count(ParseEnv) -> Int
pub fn parse_env_local_at(ParseEnv, Int) -> (String, @kernel.HolType)?

parse_let

parse_let(env, src) は宣言 let <name> : <type> をパースし、そのローカルを追加した環境を返す。

pub fn parse_let(ParseEnv, String) -> Result[ParseEnv, ParseBridgeError]

型は型名(bool、ind、または A のような型変数)とそれらの間の矢印である。例: let f : A -> bool。

項

SynTerm

SynTerm は項の構文木である。

pub enum SynTerm {
  Name(String)
  Prefix(String, SynTerm)
  App(SynTerm, SynTerm)
  Infix(String, SynTerm, SynTerm)
  Forall(String, @kernel.HolType, SynTerm)
}

Prefix は ¬ であり、Infix は =、∧、∨、-> のいずれかであり、App は並置である。Forall はゴールの構文からのみ生じる。

parse_term_raw

parse_term_raw は名前を解決せずに項をパースする。

pub fn parse_term_raw(String) -> Result[SynTerm, ParseError]

適用が最も強く結合し、次に ¬、その次に中置演算子が次の表の順で結合する。

演算子	優先順位	結合性
=	40	なし
∧	30	左
∨	20	左
->	15	右

したがって p ∧ q ∨ ¬p -> q は $((p \wedge q) \vee \neg p) \Rightarrow q$ と読まれ、a = b = c はエラーである。

parse_term、parse_term_with_env と lower_syn_term_with_env

これらの関数はカーネルの項を生成する。parse_term(state, src) はローカルなしでパースし、parse_term_with_env は環境を用いる。lower_syn_term_with_env はすでにパースされた SynTerm をローワリングする。

pub fn parse_term(@kernel.KernelState, String) -> Result[@kernel.Term, ParseBridgeError]
pub fn parse_term_with_env(@kernel.KernelState, ParseEnv, String) -> Result[@kernel.Term, ParseBridgeError]
pub fn lower_syn_term_with_env(@kernel.KernelState, ParseEnv, SynTerm) -> Result[@kernel.Term, ParseBridgeError]

名前は elab を通じて解決される。結合子は logic のビルダで構築されるため、p ∧ q は prop_mk_and の基底項になり、これらのためにプレリュードをインストールする必要はない。定数 T と F は通常の名前であり、プレリュードが必要である。

parse_resolved_term と parse_resolved_term_with_env

これらの関数は 1 ステップ手前で止まり、定数の同一性を固定した解決済みの項を返す。

pub fn parse_resolved_term(@kernel.KernelState, String) -> Result[@elab.RTerm, ParseBridgeError]
pub fn parse_resolved_term_with_env(@kernel.KernelState, ParseEnv, String) -> Result[@elab.RTerm, ParseBridgeError]

test "terms" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let pre = @logic.default_prop_prelude()
  let env = @parser.parse_let(@parser.empty_parse_env(), "let p : bool").unwrap()
  let env = @parser.parse_let(env, "let q : bool").unwrap()
  let syn = @parser.parse_term_raw("p ∧ q ∨ ¬p -> q").unwrap()
  inspect(syn is @parser.Infix("->", @parser.Infix("∨", _, _), _), content="true")
  let t = @parser.parse_term_with_env(st, env, "p ∧ q").unwrap()
  inspect(@logic.prop_dest_and(st, pre, t) is Some(_), content="true")
  inspect(@kernel.term_to_string(@parser.parse_term(st, "T").unwrap()), content="Const(T#1 : bool)")
  // errors
  inspect(@parser.parse_term(st, "x") is Err(@parser.Sig(@kernel.UnknownConst)), content="true")
  inspect(@parser.parse_term_raw("p = q = p") is Err({ code: @parser.NonAssocChain, .. }), content="true")
  let env_f = @parser.parse_let(env, "let f : bool -> bool").unwrap()
  inspect(@parser.parse_term_with_env(st, env_f, "f ∧ p") is Err(@parser.Logic(@kernel.NotBoolTerm)), content="true")
}

ゴール

SynGoal

SynGoal は、シーケントのゴール h1, h2 ⊢ c の構文木である。

pub struct SynGoal {
  hyps : Array[SynTerm]
  concl : SynTerm
}

parse_goal_raw

parse_goal_raw は名前を解決せずにゴールをパースする。仮定はコンマで区切られ、⊢(または |-)が必須である。

pub fn parse_goal_raw(String) -> Result[SynGoal, ParseError]

項と異なり、ゴールは forall (x : A), body または ∀ (x : A), body で始まってもよく、括弧で囲んでもよい。この形はここでのみ、ゴールの糖衣構文として受理される。

ParsedGoal、parsed_goal_hyps と parsed_goal_concl

ParsedGoal はローワリングされたゴールであり、仮定と結論のカーネル項を持つ。2 つのアクセサがそれらを読み出す。

pub struct ParsedGoal {
  hyps : Array[@kernel.Term]
  concl : @kernel.Term
}

pub fn parsed_goal_hyps(ParsedGoal) -> Array[@kernel.Term]
pub fn parsed_goal_concl(ParsedGoal) -> @kernel.Term

prover は ParsedGoal を @tactics.Goal に変換する。パーサは tactics パッケージに依存しない。

parse_goal、parse_goal_with_env と lower_syn_goal_with_env

これらの関数はゴールをパースしてローワリングする。ローカルなし、環境あり、またはパース済みの SynGoal からの 3 通りがある。

pub fn parse_goal(@kernel.KernelState, String) -> Result[ParsedGoal, ParseBridgeError]
pub fn parse_goal_with_env(@kernel.KernelState, ParseEnv, String) -> Result[ParsedGoal, ParseBridgeError]
pub fn lower_syn_goal_with_env(@kernel.KernelState, ParseEnv, SynGoal) -> Result[ParsedGoal, ParseBridgeError]

すべての仮定と結論は命題でなければならない(そうでなければ Logic(NotBoolTerm))。forall (x : A), body のゴールは、x を型 A のローカルとしてローワリングされる。

ResolvedGoal と parse_resolved_goal_with_env

ResolvedGoal は解決済みの項からなるゴールであり、parse_resolved_goal_with_env がそれを生成する。

pub struct ResolvedGoal {
  hyps : Array[@elab.RTerm]
  concl : @elab.RTerm
}

pub fn parse_resolved_goal_with_env(@kernel.KernelState, ParseEnv, String) -> Result[ResolvedGoal, ParseBridgeError]

test "goals" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let env = @parser.parse_env_push_local(@parser.empty_parse_env(), "p", @kernel.bool_ty())
  let g = @parser.parse_goal_with_env(st, env, "p, p ⊢ p ∧ p").unwrap()
  inspect(@parser.parsed_goal_hyps(g).length(), content="2")
  // goal-only quantifier sugar
  inspect(@parser.parse_goal(st, "⊢ forall (x : bool), x -> x") is Ok(_), content="true")
  inspect(@parser.parse_term(st, "forall (x : bool), x") is Err(@parser.Parse(_)), content="true")
  inspect(@parser.parse_goal(st, "T") is Err(@parser.Parse({ code: @parser.MissingTurnstile, .. })), content="true")
}

定理スクリプト

SynTheoremScript

SynTheoremScript は、パースされた定理スクリプト theorem <name> <binders> : <goal> := by <steps> である。

pub struct SynTheoremScript {
  name : String
  binders : Array[SynBinder]
  goal : SynGoal
  goal_src : String
  goal_span : SourceSpan
  body : SynScriptBody
}

goal_src は書かれたままのゴールのテキストであり、goal_span はその生の位置である。

SynBinder

SynBinder は、位置とソーステキストを伴う定理ヘッダの束縛子 (x : bool) である。

pub struct SynBinder {
  name : String
  ty : @kernel.HolType
  span : SourceSpan
  src : String
}

SynScriptBody、SynScriptStep と SynScriptBranch

本体はステップのリストである。各ステップは、(スクリプト全体を通して 1 から数えた)インデックス、属する分岐パス、位置とソーステキスト、およびその後に書かれた分岐ブロックを記録する。

pub struct SynScriptBody {
  steps : Array[SynScriptStep]
}

pub struct SynScriptStep {
  step : SynTacticStep
  step_index : Int
  branch_path : Array[Int]
  span : SourceSpan
  src : String
  branches : Array[SynScriptBranch]
}

pub struct SynScriptBranch {
  branch_path : Array[Int]
  body : SynScriptBody
  span : SourceSpan
  src : String
}

split { ... } { ... } は、外側のパスからの相対で [1] と [2] のパスを持つ 2 つの分岐を持ち、left { ... } と right { ... } は 1 つ持つ。入れ子のブロックはパスを延長する。

SynTacticStep

SynTacticStep は 1 つの証明ステップである。

pub enum SynTacticStep {
  Intro(String)
  Exact(String)
  Apply(String)
  Assumption
  Split
  Left
  Right
  Hole(String?)
}

Hole はパーサ専用である。タクティク層には hole のステップがなく、prover は hole を未完了の結果に変える。

parse_theorem_script_raw と parse_theorem_file_raw

parse_theorem_script_raw は 1 つの定理スクリプトをパースする。ステップは ; で区切って 1 行に並べても、1 行に 1 つずつでもよい。parse_theorem_file_raw は、qed を含む行で区切られたスクリプトのファイルをパースする。定理が 1 つだけのファイルでは省略してもよい。

pub fn parse_theorem_script_raw(String) -> Result[SynTheoremScript, ParseError]
pub fn parse_theorem_file_raw(String) -> Result[Array[SynTheoremScript], ParseError]

束縛子の型とゴールはパースされるが解決されない。ローワリングは prover が行う。

test "scripts" {
  let s = @parser.parse_theorem_script_raw(
    "theorem dup (x : bool) : ⊢ x -> x ∧ x := by\n  intro h\n  split { exact h } { exact h }",
  ).unwrap()
  assert_eq((s.name, s.binders.length(), s.goal_src), ("dup", 1, "⊢ x -> x ∧ x"))
  let split = s.body.steps[1]
  inspect(split.step is @parser.Split, content="true")
  assert_eq(split.branches.map(b => b.branch_path), [[1], [2]])
  let h = @parser.parse_theorem_script_raw("theorem t : ⊢ T := by hole h1").unwrap()
  inspect(h.body.steps[0].step is @parser.Hole(Some("h1")), content="true")
  let file = @parser.parse_theorem_file_raw(
    "theorem a : ⊢ T := by exact truth\nqed\ntheorem b : ⊢ T := by exact truth\nqed\n",
  ).unwrap()
  inspect(file.length(), content="2")
}

定義

parse_def_function

parse_def_function(state, env, src) は定義 def <name>(<x> : <type>, ...) : <type> { <body> } をパースし、カーネルの DefOK ゲートを通じて定数 $\mathit{name} = \lambda x \dots.\,\mathit{body}$ として受理する。

pub fn parse_def_function(@kernel.KernelState, ParseEnv, String) -> Result[(@kernel.KernelState, @kernel.Thm), ParseBridgeError]

拡張された状態と定義定理を返す。カーネルによる拒否(本体中の自由変数、すでに定義済みの名前)は Sig エラーとして返る。このユーティリティは定理スクリプトの構文には含まれない。

test "definition" {
  let st = @kernel.empty_kernel_state()
  let (st2, th) = @parser.parse_def_function(st, @parser.empty_parse_env(), "def id(x : bool) : bool { x }").unwrap()
  inspect(@kernel.ks_has_def_head(st2, "id"), content="true")
  inspect(
    @kernel.term_to_string(@kernel.thm_concl(th).unwrap()),
    content="Comb(Comb(Const(= : fun(fun(bool, bool), fun(fun(bool, bool), bool))), Const(id#1 : fun(bool, bool))), Abs(Var(_b0 : bool), Var(_b0 : bool)))",
  )
  // defining the same name twice is refused by the kernel
  let again = @parser.parse_def_function(st2, @parser.empty_parse_env(), "def id(x : bool) : bool { x }")
  inspect(again is Err(@parser.Sig(@kernel.DefinitionAlreadyExists)), content="true")
}