如何生成Coq源码AST？coq-lsp解析合法代码失败问题排查

问题背景 #

我正在开发一款Coq源码格式化工具，核心需求是获取Coq源码的抽象语法树（AST）。最初尝试通过Coq官方API生成AST，但因上手难度过高放弃。后来发现coq-lsp具备生成解析级AST的能力，于是基于它编写了代码。

成功实现的代码示例 #

OCaml核心代码 #

let opts =
  {
    Coq.Init.load_module = (fun _ -> ());
    Coq.Init.load_plugin = (fun _ -> ());
    Coq.Init.fb_handler = (fun _ -> ());
    Coq.Init.debug = false;
  }

let code =
  {|Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.
|}

let code_stream = Gramlib.Stream.of_string code
let init_state = Coq.Init.coq_init opts
let parser = Coq.Parsing.Parsable.make code_stream
let result = Coq.Parsing.parse ~st:init_state parser
let (Coq.Protect.R.Completed (Stdlib.Ok (Some ast))) = result.r

Dune配置文件 #

(executable
 (public_name foo)
 (name main)
 (libraries foo coq-lsp.coq coq-core.gramlib)
 (flags
  (:standard -rectypes)))

运行结果 #

utop # #rectypes;;
utop # #use "bin/main.ml";;
val opts : Coq.Init.coq_opts =
  {Coq.Init.fb_handler = <fun>; load_module = <fun>; 
   load_plugin = <fun>; debug = false}
val code : string =
  "Inductive day : Type :=\n     | monday\n     | tuesday\n     | wednesday\n     | thursday\n     | friday\n     | saturday\n     | sunday.\n   "
val code_stream : char Gramlib.Stream.t = <abstr>
val init_state : Coq.State.t = <abstr>
val parser : Coq.Parsing.Parsable.t = <abstr>
val result : (Coq.Ast.t option, Loc.t) Coq.Protect.E.t =
  {Coq.Protect.E.r = Coq.Protect.R.Completed (Stdlib.Ok (Some <abstr>));
   feedback = []}
File "bin/main.ml", line 28, characters 4-52:
28 | let (Coq.Protect.R.Completed (Stdlib.Ok (Some ast))) = result.r
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Completed (Ok None)
val ast : Coq.Ast.t = <abstr>

遇到的问题 #

当把code替换为以下合法Coq代码时：

let code = {|Example foo: 1 = 1.
Proof.
Abort.|}

result返回错误：

val result : (Coq.Ast.t option, Loc.t) Coq.Protect.E.t =
  {Coq.Protect.E.r =
    Coq.Protect.R.Completed
     (Stdlib.Error
       (Coq.Protect.Error.User
         (Some
           {Loc.fname = Loc.ToplevelInput; line_nb = 1; 
            bol_pos = 0; line_nb_last = 1; bol_pos_last = 0; 
            bp = 15; ep = 16},
          <abstr>)));

开启Coq.Init.debug = true也未得到有效调试信息。

核心疑问 #

1. 为什么Coq.Parsing.parse会拒绝这段合法的Coq代码？
2. 如何获取任意合法Coq源码的AST？不局限于coq-lsp，但需要从.v文件原始内容生成。

版本信息 #

• OCaml: 4.14.1
• coq-lsp: 0.1.6.1+8.17
• coq-core: 8.17.1
• utop: 2.13.0

问题原因分析 #

Coq.Parsing.parse默认仅处理顶层定义类代码，而Proof.和Abort.属于证明脚本，这类代码的解析要求Coq解释器切换到特定的证明模式上下文。当前代码的初始化状态仅支持顶层定义解析，无法处理证明脚本的状态切换，因此解析失败。

解决方案 #

方案1：使用coq-lsp完整文档解析流程

coq-lsp设计为处理完整Coq文档，包括证明脚本。需使用其文档管理API替代单一parse函数：

let doc = Coq.Document.create ~uri:(Uri.of_string "file://test.v") ~text:code
let _ = Coq.Document.parse doc
let ast_nodes = Coq.Document.ast doc

该流程会自动处理顶层定义与证明脚本的状态切换，完整生成所有节点的AST。

方案2：直接使用Coq官方API

Coq官方coq-core库提供了完整AST生成能力，正确入口为Coqtop模块：

let coqtop = Coqtop.init ()
let _ = Coqtop.interp coqtop "Example foo: 1 = 1."
let _ = Coqtop.interp coqtop "Proof."
let _ = Coqtop.interp coqtop "Abort."
let ast = Coqtop.get_ast coqtop

注：不同Coq版本的CoqtopAPI细节可能有差异，需参考对应版本的coqtop.mli文档。

方案3：使用coqc命令行导出AST

无需编写OCaml代码，直接通过coqc命令行工具从.v文件导出AST：

coqc -dump-ast test.v > test.ast

适合批量处理场景，直接从源码文件生成AST。

内容的提问来源于stack exchange，提问作者toku-sa-n