訪問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是實驗軟件。