Gregory Malecha (Dec 21 2022 at 13:14): 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?
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.
Enrico Tassi (Dec 21 2022 at 13:31):Ah no, wait, now I see it
Enrico Tassi (Dec 21 2022 at 13:31):Ty = (prod _ {{nat}} _), should be it
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'").
Enrico Tassi (Dec 21 2022 at 13:33):Ditto for not (Ty is {{nat}})
Enrico Tassi (Dec 21 2022 at 13:33):You want = there.
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.
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
Enrico Tassi (Dec 21 2022 at 13:45):Done (opening the issue): https://github.com/LPCIC/elpi/issues/170
Gregory Malecha (Dec 21 2022 at 15:35):Thanks! I didn't realize that is was very different from =. It makes sense.
Notification Bot (Dec 21 2022 at 15:38):Gregory Malecha has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC