Agda User Manual v2.5.4.2

• 语言: 英语
• 格式: .pdf
• 来源: agda.readthedocs.io

摘要

文档详细介绍了Agda编程语言的使用指南，包括库管理系统、编译工具链和文档生成功能。库管理系统允许用户管理多个库的位置和依赖关系，通过配置library文件和defaults文件实现默认库的使用。文档还涵盖了Agda的编辑和编译工具，如字体高亮功能、代码示例的处理以及类型检查功能。另外，文档介绍了Agda的编译工具链，包括GHC和JavaScript后端，并提供了外部函数接口（FFI）的使用示例。

AI总结

### 《Agda User Manual v2.5.4.2》内容总结

Agda用户手册主要介绍了Agda编程语言及其工具的使用方法，以下是核心内容的总结：

---

#### 1. **生成LaTeX**
- Agda支持通过 `.lagda` 文件生成LaTeX文档。
- 码块需使用 `\begin{code}` 和 `\end{code}` 包裹，示例：

  \begin{document}
  Introduction
  \begin{code}
  module MyPaper where
  open import Prelude
  five : Nat
  five = 2 + 3
  \end{code}
  \end{document}

- 支持生成HTML文档，并可通过 `make user-manual-test` 检查代码示例的正确性。

---

#### 2. **库管理**
- Agda有一个简单的包管理系统，支持多个库的管理。
- 使用标准库时需：
1. 创建 `AGDA_DIR/libraries` 文件，内容为 `AGDA_STDLIB/standard-library.agda-lib`。
2. 创建 `AGDA_DIR/defaults` 文件，内容为 `standard-library`。
- 默认库路径：
- Unix-like系统：`~/.agda`。
- Windows：`C:\Users\USERNAME\AppData\Roaming\agda`。

---

#### 3. **代码编辑与类型检查**
- 支持批处理模式命令行工具 `agda`，可通过 `agda --help` 查看帮助。
- Agda文件可以包含代码示例，需通过 `agda2-mode` 和 `rst-mode` 提供的交互模式类型检查。
- 在 `.lagda.rst` 文件中嵌入代码示例时，需确保代码正确，避免尾随空格。

---

#### 4. **外部函数接口 (FFI)**
- 支持将Haskell类型映射到Agda类型，使用 `FOREIGN` 和 `COMPILE` pragmas。
- 非透明类型：

    postulate FileHandle : Set
    {-# COMPILE GHC FileHandle = type System.IO.Handle #-}

- 透明数据类型：

    data Maybe (A : Set) : Set where nothing | just
    {-# COMPILE GHC Maybe = data Maybe (Nothing | Just) #-}

- 内置类型映射：
- `NAT` → `Integer`。
- `STRING` → `Data.Text.Text`。
- `FLOAT` → `Double`。

---

#### 5. **编译器**
- **GHC后端**：将Agda代码编译为Haskell代码，使用 `agda --compile` 命令。
- 示例：

    module HelloWorld where
    postulate putStrLn : String → IO
    {-# COMPILE GHC putStrLn = Text.putStrLn #-}
    main : IO
    main = putStrLn "Hello, World!"

- 需要额外库支持：
- `primFloatEquality` 需要 `ieee754` 库。
- **JavaScript后端**：将Agda代码编译为JavaScript代码。

---

#### 6. **其他**
- Agda是布局敏感语言，使用与Haskell类似的缩进规则，但不允许使用 `{}` 和 `;`。
- 支持逐字编程（Literate Programming），文件扩展名为 `.lagda`。
- 手册为工作版本，欢迎通过GitHub提出修改和补充。

---

以上为手册的核心内容，涵盖了Agda的库管理、文档生成、类型检查、外部函数接口及编译器的主要功能。