## Stream: Elpi users & devs

### Topic: Print context

#### 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?

#### 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) ... )).

#### 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»))]]


#### Enzo Crance (Jul 07 2021 at 09:06):

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

#### Enrico Tassi (Jul 07 2021 at 09:22):

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

#### 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.

#### 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).

#### 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