Print type of term in ltac2, including implicts · Ltac2

Is there a way to print the type of a term in ltac2 similar to how About does, where it shows which binders are implicit? The reason I'm not just using About, is because About only works for definitions, but I'd like this to work with partially applied functions.

I found how to get the type of a term using type in ltac2. This snippet shows that along with how ltac2 and About show different types for nth.

From Coq Require Import List.
From Ltac2 Require Import Ltac2.
From Ltac2 Require Import Constr.
From Ltac2 Require Import Printf.

About nth.
Ltac2 Eval
  printf "";
  printf "nth type according to ltac2: %t" (type open_constr:(nth)).

nth : forall [A : Type], nat -> list A -> A -> A

nth is not universe polymorphic
Arguments nth [A]%type_scope n%nat_scope l%list_scope default
nth is transparent
Expands to: Constant Coq.Lists.List.nth

nth type according to ltac2: (forall A : Type, nat -> list A -> A -> A)
- : unit = ()

Ike Mulder (Mar 11 2024 at 08:25):

I think implicit arguments can only be set for definitions... so About would show that information, since it can only be given definitions.
The Ltac2 type function takes any kind of term, so it will not do anything special for definitions. It functions more like Check.
So I don't think this is directly possible. What is your end goal here?

Kyle Stemen (Mar 11 2024 at 08:50):

I'm making a mod for a Minecraft-like video game. The player gets items in game that hold Coq terms. They can combine them together using application to get a new term. The mod calls into Coq to get the type information for the new term so that it can be displayed in game.

I'd like some kind of consistent output that works for both definitions and expressions, to make the mod easier to understand. Ltac2 and Check are showing the maximally implicit arguments with existentials, which are honestly easier to understand than than the forall that About prints. However, the Ltac2 I currently have and the Check command are converting the non-maximal implicit arguments into regular arguments, which is confusing unless you know a lot about Coq already.

Gaëtan Gilbert (Mar 11 2024 at 09:20):

Pierre-Marie Pédrot (Mar 11 2024 at 09:45):

I don't think Ltac2 is the right kind of language for this type of query / interaction. @Kyle Stemen depending on the language your mod is implemented in, you should rather use something like serapi or directly the (unstable) OCaml API of Coq

Michael Soegtrop (Mar 11 2024 at 14:32):

% [coq.arguments.implicit GR Imps] reads the implicit arguments declarations
% associated to a global reference. See also the [] and {} flags for the
% Arguments command.

Kyle Stemen (Mar 11 2024 at 20:51):

I took at look at Serapi. It says its in maintenance mode and replaced by coq-lsp, but the query interface for coq-lsp has even worse documentaiton.

Serapi seems to do about what the coqtop protocol can do, but with a more documented interface. I cannot find a way to get Serapi to print the type of an arbitrary expression, aside from asking Serapi to just run the Check command. When Serapi just runs the Check command, the only benefit it has over running Check through coqc is that it breaks up the pretty printed string into pieces.

Serapi has an option to query a definition, but it just shows the AST of the definition. It doesn't even show the type of the definition.

rlwrap sertop --printer=human
(Add () "Definition x:= 0. Definition y:= x.")
(Exec 3)
(Query () (Definition y))
> (Answer 3 Ack)
> (Answer 3
>  (ObjList
>   ((CoqConstr
>     (Const
>      ((Constant (KerName (MPfile (DirPath ((Id SerTop)))) (Id x)) ())
>       (Instance (() ()))))))))
> (Answer 3 Completed)

Kyle Stemen (Mar 11 2024 at 20:59):

One disadvantage to Elpi is that it doesn't come bundled with distro Coq installations. So the directions for my mod would have to explain how to install Coq along with Elpi.

I didn't try it, but I think the function that Michael linked to in Elpi is just the equivalent of the About Vernac command, meaning that it will work when given a definition reference, but not when given a partially applied expression. For example, let's say I have the following definition:

Definition two_implicits [A: Type] (a: A) [B: Type] (b: B) : nat := 0.

I want to query how many additional arguments should be appended to the expression two_implicits 0 to fully apply the function. Check (two_implicits 0) implies that it needs 2 more arguments. However, really it just needs 1 more argument: (two_implicits 0 1).

Kyle Stemen (Mar 11 2024 at 21:06):

It might be solvable in ltac2 by taking (two_implicits 0) as preterm, then repeatedly adding _ to the end until it stops type checking. Then it could repeatedly match on the resulting constr, and find which terms have the same name as the evars from the wildcards it added. The remaining terms that don't match its evars would have come from implicit variables. At that point it would need to print all of that information in some format.

However, that's pretty complex. So maybe Pierre-Marie is right that I should just directly call Coq APIs from Ocaml.

Stream: Ltac2

Topic: Print type of term in ltac2, including implicts

Kyle Stemen (Mar 11 2024 at 01:52):