Coqの豊富なXMLのようなAST出力へのアクセス

Question

Coq（< 8.5）の旧バージョンでは、メインのcoqtopプロセスは文字列を使用して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は実験的ソフトウェアです。