Stream: Elpi users & devs

Topic: Print context


view this post on Zulip Enzo Crance (Jul 06 2021 at 15:00):

Hello. I am trying to write the current context to find a bug but I get an empty list even right after introducing a new variable.

pi x\ decl x _ T => (
  coq.say "Coq ctx" {std.findall (decl _ _ _)},
  % ...
)

I guess the method is not right. Do you have a fix in mind?

view this post on Zulip Enrico Tassi (Jul 06 2021 at 20:11):

I'm not in front of my computer but I'm afraid you were just unlucky. Probably a bug in find all with underscores under a pi. Try (findall (decl (A x) (B x) ... )).

view this post on Zulip Enrico Tassi (Jul 07 2021 at 08:57):

Oops, forge what I did say. The problem is another one. decl is declares with the first argument in input mode, so you can't pass a variable and expect elpi to find a solution for it. The reason was that I did not expect users to do what you are doing ;-)

In particular, if you are writing a tactic, you get the context, so you should not need to reconstruct it.
But maybe I miss a use case?

I could also change the way findall operates and disregard modes, but I need a very strong use case for that.

Finally, if the use case is debugging, then there are other ways to skin the cat. Example:

From elpi Require Import elpi.

Elpi Command print_ctx.
Elpi Accumulate lp:{{

main _ :-
  pi x\ decl x `x` {{ nat }} => main1.
main1 :-
  pi x\ decl x `y` {{ bool }} => main2.

main2 :-
  var X _ L,
  coq.say "names in scope" L,
  std.map L (n\r\ std.findall (decl n _ _) r) Ctx, % you don't really need findall now
  coq.say "Coq ctx" Ctx.

}}.
Elpi print_ctx.

gives you

names in scope [c0, c1]
Coq ctx
[[decl c0 `x` (global (indt «nat»))],
 [decl c1 `y` (global (indt «bool»))]]

view this post on Zulip Enzo Crance (Jul 07 2021 at 09:06):

Thanks. I did not really know about the var predicate. This is a good alternative.

view this post on Zulip Enrico Tassi (Jul 07 2021 at 09:22):

Can you tell me a bit more about your use case? Was it just debugging?

view this post on Zulip Enzo Crance (Jul 07 2021 at 09:25):

Yes it was. I just wanted to print the context, nothing more, but I did not have the list of defined variables at hand, because the logic looks like your main / main1 predicates, recursively calling themselves while going down a term.

view this post on Zulip Enrico Tassi (Jul 07 2021 at 09:46):

There is a another way to print the context, I should really add it to std.
Here: https://github.com/math-comp/hierarchy-builder/blob/master/HB/common/stdpp.elpi#L94-L98

pred print-ctx.
print-ctx :- declare_constraint print-ctx [].
constraint print-ctx decl def {
  rule \ (G ?- print-ctx) | (coq.say "The context is:" G).
}

After this print-ctx is a constraint (it's a predicate with only one clause which declares the constraint). Then a CHR rule "solves" the constraint (removes it) and prints the context in which the constraint was declared. CHR rules live at the meta level, they see the constraints (suspended \lambda-Prolog goals) in their integrity, context included (only the predicates listed after constraint are kept, hence decl and def, if you need more, add them there).

view this post on Zulip Enrico Tassi (Jul 07 2021 at 09:48):

It's a part of the Elpi language users should not need to know, it's only used in a corner of the whole machinery, but can come handy to see one or more goals from the outside.


Last updated: Feb 04 2023 at 02:03 UTC