Kazuhiko Sakaguchi (Feb 21 2021 at 13:40): 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?
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
Enrico Tassi (Feb 21 2021 at 15:55):No easier way. Maybe you can lift take-last to coq terms, eg take-last-arg
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 =.
Kazuhiko Sakaguchi (Feb 22 2021 at 11:37):It makes sense to me. Thanks.
Last updated: Oct 13 2024 at 01:02 UTC