✔ Outputting a list of variables · Elpi users & devs

Hi,
I would like to output a list of the form [ X1 , .... , Xn ] where n is a parameter and the Xi are supposed to be placeholders for terms.
What is wrong with this? (I get an unspecified error)

Elpi Program listX lp:{{
  pred listX i : int, o : list term.
    listX (1 + k ) [X | L]:-  listX k L.
    listX 0 [].
}}.

Elpi Query lp:{{
    listX 3 L.   % ---> ERROR
}}.

PS: two very loosely related questions:
1) is there a way to print the elpi type of an expression?
2) is there native pairs in elpi or should we use list for that?

Enrico Tassi (Sep 11 2022 at 19:24):

Enrico Tassi (Sep 11 2022 at 20:25):

Arithmetic evaluation happens via is, you can write N is M - 1, but you can't expect N = 1 + M to compute. 1 + M is just syntax, is gives it the meaning.

Pierre Vial (Sep 12 2022 at 09:44):

Pierre Vial (Sep 12 2022 at 11:25):

As a follow-up question, I would like to substitue these k variables in a function which takes k parameters, so do something like this:

Elpi Accumulate lp:{{
pred appk i : list term, i : term, o : term.
    appk [ X0 | L ] (fun _ Ty Fu) (Fu' X0) :- appk L (Fu X0) (Fu' X0) .
    appk [] T T.
}}.

Elpi Query lp:{{
  appk [X0 , X1 ] {{fun (a b : nat) => a + b}} T.
}}.

However, I obtain this error:

Non deterministic pruning, delay to be implemented: t=
A4 ≪.X0≫_0, delta=0

Enzo Crance (Sep 12 2022 at 11:41):

I am not a master in Elpi internals but it seems to detect that T depends on X0 after the call, yet the code does not reflect this.

First, I would suggest not to try to unify the output of appk with a function applied to a unification variable. Instead of:

appk [X0|L] (fun _ Ty Fu) (Fu' X0) :-
  appk L (Fu X0) (Fu' X0).

appk [X0|L] (fun _ Ty Fu) (Fu' X0) :-
  pi x\ appk L (Fu x) (Fu' x).

You create a universal constant x that Elpi can easily abstract in Fu', whereas a unification variable can depend on other unification variables, etc. It usually works better. In my experience working with unification variables is tricky.

Then, I think the error would still be there, but it would come from the fact that X0 and X1 are unification variables in your query. For example, provided that you use the formulation with the universal constant, if you replace X0 and X1 with {{ O }}, the code works.

Elpi Query lp:{{
  appk [{{ 0 }}, {{ 0 }}] {{ fun (a b : nat) => a }} T.
}}.

Query assignments:
  T = global (indc «O»)

Pierre Vial (Sep 12 2022 at 11:53):

OK, so if I take your line for appk, I still have the exact same error with my initial query. But with your code and query, it works.

However, this solution won't work for what I'm endeavouring to do: I need some generic variables (which will have two occurrences in a proof term) and that I can bind afterwards.
Basically, I would like to be able to output something like: F X1 X2 ... Xn + G X1 ... Xn to be able to then build pi x1\decl _ _ _ => .... pi xn\decl _ _ _ _ => F x1 ... xn (in fact, as you can expect, what I'm doing to do is more complicated than that and I need to tinker with the syntax of terms)

Enzo Crance (Sep 12 2022 at 12:10):

so from terms f, g and a number n of arguments you want to create the binder fun x1 ... xn => f x1 ... xn + g x1 ... xn?

Pierre Vial (Sep 12 2022 at 12:16):

something which is more complex than that, which plays with equalities, implication etc, but what I'm trying to understand how to manipulate variables (which will be bound) in a term that I build

Enzo Crance (Sep 12 2022 at 12:21):

I think there are a few idiomatic patterns to make code work, but I cannot really list them from memory, it's better with an example. idk how I could help more at this point. You can still ask other more experienced users. Good luck!

Pierre Vial (Sep 12 2022 at 13:26):

Enrico Tassi (Sep 12 2022 at 13:29):

You can also look for hd-beta in reducion.elpi (loaded by default) or coq.reduction.*

Stream: Elpi users & devs

Topic: ✔ Outputting a list of variables

Pierre Vial (Sep 11 2022 at 15:51):