Stream: Ltac2

Topic: How to count goals?

Emilio Jesús Gallego Arias (Jun 09 2022 at 08:25):

Hi folks, is there a way to count the number of goals in scope Ltac2?

Michael Soegtrop (Jun 09 2022 at 08:56):

The only way I know of is to search over j - first expanding in powers of two until it fails and then do a binary intersection search on:

Control.focus j j (fun _ => ())

This fails if there are not at least j goals. I am not aware of a direct way to ask for the number of goals.

Janno (Jun 09 2022 at 09:19):

Why not use a mutable integer field to count?

From Ltac2 Require Import Ltac2 Printf.
Ltac2 Type count := { mutable count : int }.
Goal True /\ True.
  split;
    (let c := { count := 0 } in
     Control.enter (fun _ =>
                      c.(count) := Int.add 1 (c.(count))
       );
     printf "number of goals: %i" (c.(count))
    ).

Enrico Tassi (Jun 09 2022 at 09:30):

With the premise that I dislike this API (and that this task is trivial in elpi) I think you want to expose, in the Control module I guess, this OCaml API https://github.com/coq/coq/blob/master/engine/proofview.mli#L310 which "maps" the goal list and provides a list of results. You can then compute the length of the list (in OCaml the type has a monad, but is implicit in Ltac2).

Enrico Tassi (Jun 09 2022 at 09:31):

I mean tclINDEPENDENTL (tclUNIT ()) >>= List.length does what you want (in OCaml).

Paolo Giarrusso (Jun 09 2022 at 10:37):

Since Ltac1 has numgoals, some answer probably belongs in the Ltac2 stdlib?

Emilio Jesús Gallego Arias (Jun 09 2022 at 19:26):

Thanks, indeed we should expose a primitive function and not do a hack, as @Enrico Tassi says goals are just stored in a list (+ the shelf)

Last updated: Oct 12 2024 at 12:01 UTC