编辑“︁Lean元数据访问”︁

= Lean元数据访问 =

== 介绍 ==
'''Lean元数据访问'''是Lean元编程中的核心概念之一，它允许程序在运行时检查和操作Lean表达式、声明和环境中的元数据。元数据包括类型信息、文档字符串、属性（attributes）以及其他与代码结构相关的附加信息。通过元数据访问，开发者可以动态分析代码、生成代码或实现高级反射功能。

在Lean中，元数据主要通过以下方式访问：
* '''环境（Environment）'''：存储当前上下文中所有的声明和定义。
* '''表达式（Expr）'''：表示Lean中的语法结构，可以携带类型和元数据。
* '''属性（Attributes）'''：附加在声明上的标记，用于控制行为或存储信息。

== 基础元数据访问 ==

=== 访问环境中的声明 ===
Lean的`Environment`对象包含所有已注册的声明（如定义、定理、归纳类型等）。以下示例展示如何从环境中获取声明的元数据：

<syntaxhighlight lang="lean">
import Lean

open Lean Meta

#eval show MetaM Unit from do
  let env ← getEnv
  let declName := ``Nat.add
  if let some info := env.find? declName then
    IO.println s!"Declaration {declName} has type: {info.type}"
    IO.println s!"Kind: {info.kind}"
  else
    IO.println s!"Declaration {declName} not found"
</syntaxhighlight>

'''输出示例'''：
```
Declaration Nat.add has type: Nat → Nat → Nat
Kind: def
```

=== 表达式元数据 ===
Lean的表达式（`Expr`）可能包含位置信息、宏展开历史等元数据。使用`Expr`的API可以提取这些信息：

<syntaxhighlight lang="lean">
def inspectExpr : Expr → MetaM Unit
  | Expr.const name _ => do
    let type ← inferType (Expr.const name [])
    IO.println s!"Constant {name} has type: {type}"
  | e => IO.println s!"Other expression: {e}"

#eval show MetaM Unit from do
  let e := mkConst ``Nat.succ
  inspectExpr e
</syntaxhighlight>

'''输出示例'''：
```
Constant Nat.succ has type: Nat → Nat
```

== 高级元数据操作 ==

=== 属性系统 ===
Lean允许通过属性（如`@[simp]`、`@[inline]`）附加元数据到声明上。以下代码检查声明是否具有特定属性：

<syntaxhighlight lang="lean">
#eval show MetaM Unit from do
  let declName := ``List.length
  let hasSimpAttr ← hasSimpAttribute declName
  IO.println s!"List.length has [simp] attribute: {hasSimpAttr}"
</syntaxhighlight>

'''输出示例'''：
```
List.length has [simp] attribute: true
```

=== 自定义属性 ===
开发者可以定义自己的属性并存储额外元数据：

<syntaxhighlight lang="lean">
import Lean.Attributes

register_attribute my_attr : Unit

#eval show MetaM Unit from do
  let declName := ``myFunction
  let attr ← getAttributeImpl `my_attr
  attr.add declName () -- 添加属性
  IO.println "Attribute added successfully"
</syntaxhighlight>

== 实际应用案例 ==

=== 自动文档生成 ===
通过元数据访问，可以提取函数的类型和文档字符串生成文档：

<syntaxhighlight lang="lean">
def generateDoc (declName : Name) : MetaM String := do
  let env ← getEnv
  let some info := env.find? declName | return "Not found"
  let docString ← findDocString? env declName
  return s!"**{declName}** : {info.type}\n\n{document.getD "No documentation"}"
</syntaxhighlight>

=== 反射式代码验证 ===
在宏或代码生成器中检查输入表达式的类型是否正确：

<syntaxhighlight lang="lean">
def validateType (e : Expr) (expectedType : Expr) : MetaM Unit := do
  let actualType ← inferType e
  unless (← isDefEq actualType expectedType) do
    throwError "Type mismatch: expected {expectedType}, got {actualType}"
</syntaxhighlight>

== 图表说明 ==
以下Mermaid图展示了Lean元数据访问的基本流程：

<mermaid>
graph TD
  A[用户代码] --> B[解析为Expr]
  B --> C{是否含元数据?}
  C -->|是| D[提取类型/属性]
  C -->|否| E[基础处理]
  D --> F[元编程操作]
</mermaid>

== 数学表示 ==
元数据访问可形式化为函数：
<math>
\text{getMetadata}(e, \text{env}) = \begin{cases}
(e.\text{type}, e.\text{attrs}) & \text{if } e \in \text{env} \\
\bot & \text{otherwise}
\end{cases}
</math>

== 总结 ==
Lean元数据访问为元编程提供了强大的基础设施，使得代码分析、生成和转换成为可能。通过环境、表达式和属性系统的组合，开发者能够实现从简单文档提取到复杂反射逻辑的各种功能。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean元编程]]