Luna Flow
简体中文

parser 教程

本教程使用 parser 包从文本中读取公式、目标和定理脚本。你将学习在没有内核状态时解析以检查结构，把文本降级为内核项，在原始输入中定位错误，以及读取证明脚本的步骤结构。这里使用的定理脚本来自回归语料 (corpus)。

快速开始

在 moon.pkg 中导入这些包：

import {
  "Luna-Flow/QED/kernel",
  "Luna-Flow/QED/logic",
  "Luna-Flow/QED/parser",
}

解析一个目标并将其降级为内核项：

test "quick start" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let goal = @parser.parse_goal(st, "⊢ T").unwrap()
  inspect(@kernel.term_to_string(@parser.parsed_goal_concl(goal)), content="Const(T#1 : bool)")
  inspect(@parser.parsed_goal_hyps(goal).length(), content="0")
}

T 是命题序言中的常量，所以状态需要先执行 install_prop_prelude。

日常任务

检查公式如何分组

parse_term_raw 不需要状态，并展示优先级规则生成的树：

test "grouping" {
  // ∧ binds tighter than ∨, which binds tighter than ->
  let t = @parser.parse_term_raw("a ∧ b ∨ c -> d").unwrap()
  inspect(t is @parser.Infix("->", @parser.Infix("∨", @parser.Infix("∧", _, _), _), _), content="true")
  // -> associates to the right
  let r = @parser.parse_term_raw("a -> b -> c").unwrap()
  inspect(r is @parser.Infix("->", @parser.Name("a"), @parser.Infix("->", _, _)), content="true")
  // application is juxtaposition and binds tightest
  let app = @parser.parse_term_raw("f x ∧ y").unwrap()
  inspect(app is @parser.Infix("∧", @parser.App(_, _), @parser.Name("y")), content="true")
}

使用 ASCII 输入

你可以键入 \and、\or、\not、\imp 和 |-；解析前它们会被规范化为 ∧、∨、¬、-> 和 ⊢：

test "ascii" {
  let a = @parser.parse_goal_raw("p \\and q |- \\not r").unwrap()
  let b = @parser.parse_goal_raw("p ∧ q ⊢ ¬r").unwrap()
  inspect(a.concl is @parser.Prefix("¬", _) && b.concl is @parser.Prefix("¬", _), content="true")
  inspect(@parser.normalize_parser_input("p \\imp q").unwrap().text, content="p -> q")
}

声明局部变量并降级项

自由名称必须是局部变量或已声明的常量。用 parse_let 或 parse_env_push_local 声明局部变量：

test "locals" {
  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 t = @parser.parse_term_with_env(st, env, "p ∧ q -> p").unwrap()
  let (lhs, rhs) = @logic.prop_dest_imp(st, pre, t).unwrap()
  inspect(@logic.prop_dest_and(st, pre, lhs) is Some(_), content="true")
  inspect(@kernel.term_to_string(rhs), content="Var(p : bool)")
  // without the declaration, `r` is unknown
  inspect(@parser.parse_term_with_env(st, env, "p ∧ r") is Err(@parser.Sig(@kernel.UnknownConst)), content="true")
}

找到错误的位置

错误偏移指向你传入的文本，即使规范化改变了其长度：

test "error position" {
  let src = "p \\and"
  match @parser.parse_term_raw(src) {
    Err(e) => {
      inspect(e.code is @parser.UnexpectedEof, content="true")
      inspect(e.offset, content="6")
      inspect(e.detail, content="unexpected end while parsing atom")
    }
    Ok(_) => fail("expected a parse error")
  }
}

输入长六个字符，并在 \and 之后结束，所以偏移 6 是用户键入内容的末尾，而不是规范化后的 p ∧ 的末尾。

读取定理脚本

定理脚本解析为头部、目标，以及带位置的步骤列表。这是 examples/demo_and.qed 中的 demo_and 脚本：

test "script structure" {
  let src = "theorem demo_and (x : bool) : ⊢ x -> x ∧ x := by\n  intro h\n  split { exact h } { exact h }"
  let s = @parser.parse_theorem_script_raw(src).unwrap()
  inspect(s.name, content="demo_and")
  inspect(s.binders[0].src, content="(x : bool)")
  let steps = s.body.steps
  inspect(steps[0].step is @parser.Intro("h"), content="true")
  inspect(steps[1].src, content="split") // the step itself; its blocks are branches
  // the two branch blocks of split, each with one step
  let second = steps[1].branches[1]
  inspect(second.body.steps[0].step_index, content="4")
  assert_eq(second.body.steps[0].branch_path, [2])
}

步骤索引按阅读顺序对每个步骤计数，包括分支内部的步骤：intro 为 1，split 为 2，第一个 exact 为 3，第二个为 4。prover 用这些编号报告失败。

进一步使用

降级量化目标。 目标开头接受 forall，并将其降级为定理头部绑定子：绑定名成为目标的自由变量。

test "forall goal" {
  let st = @logic.install_prop_prelude(@kernel.empty_kernel_state()).unwrap()
  let g = @parser.parse_goal(st, "⊢ forall (x : bool), x -> x").unwrap()
  let free = @kernel.free_vars(@parser.parsed_goal_concl(g))
  inspect(free.length() == 1 && free[0].0 == "x", content="true")
}

保留标识。 parse_resolved_term 和 parse_resolved_goal_with_env 返回常量标识已冻结的 elab 项；当项被存储并在稍后检查时使用它们，如 elab 教程所述。

从文本定义函数。 parse_def_function(state, env, "def id(x : bool) : bool { x }") 通过内核接纳一个定义并返回其定理；见 parser API。

运行脚本。 解析脚本并不证明它。请把源文本传给 prover，它会降级目标，用 tactics 包运行每一步，并用你在上面看到的跨度 (span) 报告失败。

常见陷阱

  • 旧的联结词写法。 /\ 和 \/ 不被接受；请使用 ∧、∨ 或 \and、\or。
  • 链式等式。 a = b = c 是 NonAssocChain 错误；请加括号。
  • 项中的量词。 forall 只允许出现在目标开头。parse_term 会以 Parse 错误拒绝它。
  • 缺少转门符。 目标需要 ⊢ 或 |-，即使没有假设：写 ⊢ T，而不是 T。
  • 没有序言时的 T 和 F。 它们是常量，不是关键字；没有 install_prop_prelude 时它们是未知名称。
  • 对非命题使用联结词。 当 f : bool -> bool 时，f ∧ p 在降级时以 Logic(NotBoolTerm) 失败。

后续步骤