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?

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.

Ah no, wait, now I see it

`Ty = (prod _ {{nat}} _),`

should be it

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'").

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

You want `=`

there.

I think you could open an issue to improve the error message for `calc`

(well, `is`

), since it is quite cryptic.

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

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

Thanks! I didn't realize that `is`

was very different from `=`

. It makes sense.

Gregory Malecha has marked this topic as resolved.

Last updated: May 24 2024 at 22:02 UTC