Stream: Coq users

Topic: How to get comments from a Coq source code?


view this post on Zulip Hiroki Tokunaga (Oct 12 2023 at 13:46):

Hi. I'm having difficulty retrieving comments from a Coq source code using Coq's compiler API.
I thought Pcoq.Parsable.coments provided comments from a code, but it returned an empty list.

let _ =
  Coqinit.init_ocaml ();
  Coqinit.parse_arguments
    ~parse_extra:(fun _ -> ((), []))
    ~usage:
      Boot.Usage.
        { executable_name = "coqfmt"; extra_args = ""; extra_options = "" }
    ()
  |> fst |> Coqinit.init_runtime
in
Stm.init_core ();
Stm.init_process Stm.AsyncOpts.default_opts
;;

let parsable = Gramlib.Stream.of_string "(* foo *)" |> Pcoq.Parsable.make in

Pcoq.Parsable.comments parsable |> List.length |> print_int (* prints 0 *)

In gramlib/plexing.mli there is a comment that seems to be a TODO one (reported by BridgeTheMasterBuilder here).

  (* State for the comments, at some point we should make it functional *)
  module State : sig
    type t
    val init : unit -> t
    val set : t -> unit
    val get : unit -> t
    val drop : unit -> unit
    val get_comments : t -> ((int * int) * string) list
  end

Is Pcoq.Parsable.comments not implemented, or am I missing something and is there a way to retrieve comments?

Coq version: 8.18.0

view this post on Zulip Enrico Tassi (Oct 12 2023 at 13:48):

I think you need to first parse (some non empty sentence) and then you can retrieve the comments that were skipped by the lexer.

view this post on Zulip Hiroki Tokunaga (Oct 12 2023 at 14:01):

Do you mean something like this?

let _ =
  Coqinit.init_ocaml ();
  Coqinit.parse_arguments
    ~parse_extra:(fun _ -> ((), []))
    ~usage:
      Boot.Usage.
        { executable_name = "coqfmt"; extra_args = ""; extra_options = "" }
    ()
  |> fst |> Coqinit.init_runtime
in
Stm.init_core ();
Stm.init_process Stm.AsyncOpts.default_opts
;;

let parsable =
  Gramlib.Stream.of_string "(* foo *) Theorem foo: 1=1. Abort. "
  |> Pcoq.Parsable.make
in

let stm_init_options =
  Stm.
    {
      doc_type = Interactive (TopLogical Coqargs.default_toplevel);
      injections =
        [
          Coqargs.RequireInjection
            { lib = "Prelude"; prefix = Some "Coq"; export = Some Import };
        ];
    }
in

let doc, state = Stm.new_doc stm_init_options in

let rec loop doc state =
  match Stm.parse_sentence ~doc ~entry:Pvernac.main_entry state parsable with
  | None -> ()
  | Some ast ->
      let doc', state', _ = Stm.add ~doc ~ontop:state false ast in
      loop doc' state'
in
loop doc state;

Pcoq.Parsable.comments parsable |> List.length |> print_int

This also prints 0. Note that parsable seems a mutable variable, and it doesn't need to be a parameter of loop.


Last updated: Jun 23 2024 at 05:02 UTC