Print context · Elpi users & devs

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 _ _ _)},
  % ...
)

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.

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):

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):

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.

Stream: Elpi users & devs

Topic: Print context