Stream: Elpi users & devs

Topic: matching with function application


view this post on Zulip Kazuhiko Sakaguchi (Feb 21 2021 at 13:40):

Hi. It seems that a pattern {{ lp:T1 lp:T2 }} fails to match with a function application with two or more arguments, say f x y, which I expected to succeed with T1 = {{ f x }} and T2 = {{ y }}.

Elpi Command test.
Elpi Accumulate lp:{{
main [trm {{ _ _ }}] :- !, coq.say "clause 1".
main [trm {{ _ _ _ }}] :- !, coq.say "clause 2".
}}.
Elpi Typecheck.

Section S.
Variable (f : nat -> nat -> nat) (x y : nat).
Elpi test (f x y). (* clause 2 *)
End S.

Since the associativities of function applications and their list representation are opposite in Elpi, the best way I could find to write such matching required the list reversal or std.split-at. Is there any easier way to do this?

view this post on Zulip Enrico Tassi (Feb 21 2021 at 15:50):

I would not use quotations but rather app[F,X|More].
Applications are not binary in Coq nor in Elpi

view this post on Zulip Enrico Tassi (Feb 21 2021 at 15:55):

No easier way. Maybe you can lift take-last to coq terms, eg take-last-arg

view this post on Zulip Enrico Tassi (Feb 21 2021 at 21:42):

Now that I have little more time, let me explain. Application is n-ary in bot Coq and Elpi for performance reasons and also because it is usually nice to get the (real) head of an application in one step. Moreover = in Elpi has a meaning: it is syntactic equality. It can't be the case that app[app[a,b],c] = app[a,b,c]; some API may accept the former syntax "to be polite" but there is no real quotient on =.

view this post on Zulip Kazuhiko Sakaguchi (Feb 22 2021 at 11:37):

It makes sense to me. Thanks.


Last updated: Mar 29 2024 at 07:01 UTC