访问Coq丰富的类似于XML的AST输出

Question

在较早版本的Coq（< 8.5）中，主要进程将使用字符串与IDE交换数据。

这应该是最近发生了变化 - 如何查询代表AST的更丰富的类似于XML的结构？

使用案例：我想以不同的方式解释任何Coq计算 - 也就是说，我需要在执行操作（例如调用策略）后以不需要解析的字符串的形式得到它的结果。

Answer 1

使用XML协议，您可以使用Annotate stm call，其中stm是您要打印的句子。但是请注意，XML打印机在8.5/8.6版本中功能远远不足，可能会被删除。 你可以看到所有的遗失案例here。另外请注意，它不输出任何级别的术语的结构化表示。

或者，您可以使用SerAPI，专门用于该特定用途的插件。使用SerAPI，您可以获得任何Coq结构的完整表示：

$ rlwrap ./sertop.native --printer=human --prelude=/home/egallego/external/coq-v8.6/ 
(Control (StmAdd() "Lemma u n : n + 0 = n.")) 
> (Answer 0 (StmAdded 2 (...) NewTip)) 
(Query() (Ast 2)) 
> (Answer 1(ObjList 
> ((CoqAst 
> (VernacStartTheoremProof Lemma 
>  ((((((Id u))())) 
>  (((LocalRawAssum 
>   (((Name (Id n)))) 
>   (Default Explicit) 
>   (CHole() IntroAnonymous()))) 
>  (CNotation 
>   "_ = _" 
>   (((CNotation 
>   "_ + _" 
>   (((CRef 
>    (Ident 
>     (Id n))) 
>    ()) 
>    (CPrim 
>    (Numeral (Ser_Bigint 0)))) 
>   ()())) 
>   (CRef 
>   (Ident 
>    (Id n))) 
>   ())) 
>   ()())) 
>  ()))) 
>  false))))) 

请注意，SerAPI是实验软件。