Lean语法扩展

Lean语法扩展

介绍

Lean语法扩展是Lean元编程的核心功能之一，允许用户通过宏系统或自定义解析规则扩展Lean语言的语法。这种机制使得开发者能够根据需求引入新的语法糖、领域特定语言（DSL）或简化现有语法结构。语法扩展在数学证明、自动化工具开发和库设计中尤为常见。

在Lean中，语法扩展主要通过以下两种方式实现：

• 宏（Macros）：在解析阶段对语法树进行转换。
• 自定义语法解析器：通过`notation`、`syntax`和`macro_rules`等命令定义新的语法规则。

基础语法扩展

使用`notation`定义中缀运算符

`notation`命令是最简单的语法扩展方式，常用于定义中缀运算符或简化已有符号：

-- 定义一个新的中缀运算符
notation:50 a " ⊕ " b => a + b * 2

-- 使用示例
#eval 1 ⊕ 3  -- 输出: 7 (因为 1 + 3*2 = 7)

参数说明：

• `:50`表示运算符优先级（数值越大优先级越高）
• `a`和`b`是占位符
• `⊕`是新定义的运算符符号

使用`syntax`和`macro_rules`

更复杂的语法扩展需要结合`syntax`和`macro_rules`：

-- 定义新的语法结构
syntax "greet" ident : command

-- 实现语法扩展的逻辑
macro_rules
| `(greet $name) => `(println! "Hello, " $(Lean.quote name))

-- 使用示例
greet Alice  -- 输出: Hello, Alice

高级语法扩展

递归宏

宏可以递归调用自身，实现复杂语法结构：

syntax "repeat" num "times" "{" command "}" : command

macro_rules
| `(repeat $n times { $cmd }) => do
  let n ← n.getNat
  let cmds ← (List.range n).mapM fun _ => `($cmd)
  `(do $cmds*)

-- 使用示例
repeat 3 times { println! "Looping" }
-- 输出:
-- Looping
-- Looping
-- Looping

带参数的语法扩展

可以通过`$`符号接收参数：

syntax "vector[" sepBy(term, ", ") "]" : term

macro_rules
| `(vector[ $[$elems],* ]) => `(#[ $[$elems],* ])

-- 使用示例
#eval vector[1, 2, 3]  -- 输出: #[1, 2, 3]

实际应用案例

数学符号扩展

在数学库中扩展集合论符号：

-- 定义集合包含语法
syntax lhs:term " ⊆ " rhs:term : term

macro_rules
| `($a ⊆ $b) => `(∀ x, x ∈ $a → x ∈ $b)

-- 使用示例
example : {1, 2} ⊆ {1, 2, 3} := by
  intro x h
  cases h <;> simp

DSL实现

创建小型领域特定语言：

syntax "query" "from" term "where" term : term

macro_rules
| `(query from $table where $cond) => 
  `(filter (fun row => $cond) $table)

-- 使用示例
def students := [{name := "Alice", age := 20}, {name := "Bob", age := 22}]
#eval query from students where row.age > 21  -- 输出: [{name := "Bob", age := 22}]

语法扩展处理流程

graph TD A[源代码文本] --> B[词法分析] B --> C[基础语法解析] C --> D{是否有语法扩展?} D -->|是| E[应用语法扩展规则] E --> F[生成抽象语法树] D -->|否| F F --> G[进一步处理]

注意事项

1. 语法扩展可能影响代码可读性，应谨慎使用 2. 注意运算符优先级和结合性 3. 复杂的语法扩展可能增加编译时间 4. 保持与现有语法的兼容性

数学公式支持

语法扩展可以用于简化数学表达式，例如定义微分符号： 解析失败 (未知函数“\diff”): {\displaystyle \frac{d}{dx}f(x) \rightarrow \diff x f(x) }

实现代码：

syntax "diff" term term : term
macro_rules | `(diff $x $f) => `(derivative $x $f)

总结

Lean语法扩展提供了强大的元编程能力，使得语言可以适应各种特定需求。从简单的运算符定义到完整的DSL实现，语法扩展都是Lean灵活性的关键所在。初学者应从简单的`notation`开始，逐步掌握更复杂的`syntax`和`macro_rules`组合。