ocaml - 从 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对于插件开发人员来说也是非常有用的设备。