parser API 参考

parser 包（Luna-Flow/QED/parser）是文本前端。它规范化输入，把项、目标和定理脚本解析为保留原文位置的语法树，并通过 elab 与 logic 包把项和目标降级（lowering）为内核项。它不拥有任何策略对象：解析出的目标是解析器自有的 ParsedGoal，由 prover 桥接到 tactics 层。

以 _raw 结尾的函数只做解析。其余函数还会针对 KernelState 解析名字并构造内核项。表层语法概述见语法指南；其背后的取舍见 parser 设计，parser 教程则逐步演示解析与降级。

输入规范化

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 是解析并降级的函数所返回的错误：语法错误，或来自内核或解析器（resolver）的错误。

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

这些函数早一步停止，返回已解析的项，其中常量标识已冻结。

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 是已降级的目标：假设和结论都是内核项。两个访问函数读取它们。

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；parser 不依赖 tactics 包。

parse_goal、parse_goal_with_env 与 lower_syn_goal_with_env

这些函数解析并降级目标：不带局部量、带环境，或从已解析的 SynGoal 出发。

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]；left { ... } 与 right { ... } 各有一个。嵌套块会延长路径。

SynTacticStep

SynTacticStep 是一个证明步骤。

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

Hole 仅存在于 parser 中：tactics 层没有 hole 步骤，prover 把 hole 转换为未完成结果。

parse_theorem_script_raw 与 parse_theorem_file_raw

parse_theorem_script_raw 解析一个定理脚本。步骤可以在同一行以 ; 分隔，也可每行一个。parse_theorem_file_raw 解析以含 qed 的行分隔的脚本文件；只有单个定理的文件可以省略它。

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")
}