Stream: Elpi users & devs

Topic: ✔ Non closed Term


view this post on Zulip Gregory Malecha (Dec 21 2022 at 13:14):

I'm getting Error: Evaluation of a non closed term (maybe delay). I'm guessing this has to do with a higher-order predicate that I am trying to define.

    pred tele-until i:(term -> term -> term -> prop) i:term i:term o:term.
    tele-until K Ty Trm Res :- std.do! [
      Ty is (prod _ {{nat}} _),
      coq.say "going to run K",
      K Ty Trm Res ].
    tele-until K (prod X Ty Bo) Trm (prod X Ty Re) :-
      not (Ty is {{nat}}),
      pi x\ tele-untilf K (Bo x) {{ lp:Trm lp:x }} (Re x).
    tele-until _ T _ {{ False }} :-
      coq.say "tele-until not-found" {coq.term->string T}.

Can Elpi support this sort of thing? Do I need to change the type of the K argument?

view this post on Zulip Enrico Tassi (Dec 21 2022 at 13:30):

Hum, it is a runtime error, so I can't really guess here.
Maybe use coq.say "going to run K=" K, in line 4 to see what K is. If it is a variable, e.g. (X22) then that is the problem.
Unfortunately I never tried to code a static mode analysis, and the "bug" is that K is an input, but you did not pass it.

view this post on Zulip Enrico Tassi (Dec 21 2022 at 13:31):

Ah no, wait, now I see it

view this post on Zulip Enrico Tassi (Dec 21 2022 at 13:31):

Ty = (prod _ {{nat}} _), should be it

view this post on Zulip Enrico Tassi (Dec 21 2022 at 13:32):

the point is that is tries to evaluate, and there is nothing to evaluate. I guess that if you fill the holes, e.g. Ty is {{ forall x : nat, nat }} then the error would become more clear (like "dunno how to evaluate 'prod'").

view this post on Zulip Enrico Tassi (Dec 21 2022 at 13:33):

Ditto for not (Ty is {{nat}})

view this post on Zulip Enrico Tassi (Dec 21 2022 at 13:33):

You want = there.

view this post on Zulip Enrico Tassi (Dec 21 2022 at 13:34):

I think you could open an issue to improve the error message for calc (well, is), since it is quite cryptic.

view this post on Zulip Enrico Tassi (Dec 21 2022 at 13:42):

Actually, if the RHS of is is a closed term, then it behaves like =, making this error even more subtle. It could just work, maybe warn that the term is already 'normal'.

The code is already okis for applicative terms, it just complains on variables for no good reason:
https://github.com/LPCIC/elpi/blob/4d64e2207cad529d17e696ad268179035428db25/src/builtin.ml#L58-L81

view this post on Zulip Enrico Tassi (Dec 21 2022 at 13:45):

Done (opening the issue): https://github.com/LPCIC/elpi/issues/170

view this post on Zulip Gregory Malecha (Dec 21 2022 at 15:35):

Thanks! I didn't realize that is was very different from =. It makes sense.

view this post on Zulip Notification Bot (Dec 21 2022 at 15:38):

Gregory Malecha has marked this topic as resolved.


Last updated: May 24 2024 at 22:02 UTC