从 OCaml 检查感应类型的元素

Question

我想编写一个 Coq 插件，它将采用归纳类型的元素并在元素上递归地进行模式匹配，并在每次迭代中执行一些计算。这听起来很简单，但我真的不知道从哪里开始。

我设法找到了一些 Coq 插件，编译并运行它们。但是我还没有找到任何关于 Coq API 的概述来了解基本概念。

到目前为止我发现的有用资源：

• A small tutorial for Ocaml plugins to extend the Coq system
• Emancipate yourself from LTac: Your first Coq plugin

---

简单例子：

让我们有一个简单的归纳类型，用一个二元运算来表示表达式

Inductive expr : Type :=
| var : nat  -> expr
| op  : expr -> expr -> expr

我想定义一个新的白话命令InspectExpression，它将递归地遍历表达式并执行一些计算。

InspectExpression (op (op (var 0) (var 1)) (var 2)). (* expression: "(x+y)+z" *)

我的最终目标是根据这些表达式生成一些 C++ 代码，但我认为这对于问题/答案并不重要。

Answer 1

这些天的规范来源是官方的Coq Plugin Tutorial，虽然它是最新的，但在 Google fu [因此它首先出现在搜索中] 和格式/演示方面都需要一些帮助。

我会说从那里开始，如果您想获得其他类型的示例，请不要犹豫在 Coq issue tracker 中打开错误。

Coq's discourse 和Gitter channel 对于插件开发者来说也是非常有用的设备。