在agda中，我们有一个简单的方法来看详细的核心术语吗？

Question

我正在研究agda中依赖模式匹配的工作原理。如果我能看到.agda文件的任意源代码的详细核心术语(.agda)，这将对我很有帮助。

但是，agda cli似乎没有为这种使用提供任何选项。有吗？

Answer 1

根据你想要多少细节，你可以尝试三种选择，尽管没有一种是完美的：

1. 如果您只想查看Agda插入了什么隐式参数，您可以启用标志--show-implicit和--show-irrelevant，通过在文件底部添加_ = {! yourTerm !}创建一个新的空洞，在文件底部添加_ = {! yourTerm !}，用C-c C-l重新加载文件，然后在洞内按下光标的C-u C-c C-m。写出来让我意识到应该有一个更简单的方法来做这件事。
2. 如果要检查并可能操作Agda术语的完整AST，可以使用反射API (https://agda.readthedocs.io/en/v2.6.2.1/language/reflection.html)进行操作。特别是，您可以使用quoteTerm原语获得任意Agda术语的反射语法。
3. 最后，如果您需要更多信息，您可以查看Agda本身的源代码，并启用调试标志来打印您想要的信息。请注意，不能保证此调试信息是有用的，甚至是可读的，因为它是为开发人员使用的。可以这样说，例如，您可以通过在文件顶部添加{-# OPTIONS -v tc.cc:12 #-}，通过模式匹配打印从定义中生成的案例树。在Emacs中，这个调试信息将在一个名为*Agda debug*的单独缓冲区中结束(在加载.agda文件之后，您必须手动打开该缓冲区)。