Compile where clauses

[omelkonian]

• also compiling postulates to undefined

[UlfNorell]

If you try to add an argument to ex and use it in one of the where functions it fails. I don't think it's worth doing this if it only works for definitions without left-hand sides.

Also, do you have a use case in mind for compiling postulates to undefined? I can't think of situation where you would actually want this...

[omelkonian]

If you try to add an argument to ex and use it in one of the where functions it fails. I don't think it's worth doing this if it only works for definitions without left-hand sides.

I see, the problem is that the definitions inside where are 'lifted' and thus require the arguments to ex as input again.
Would it be possible to (partially) apply all of these definitions and then compile?
Or is this approach doomed to fail from your experience?

Also, do you have a use case in mind for compiling postulates to undefined? I can't think of situation where you would actually want this...

Re. postulates, you will never want it in the end result, but it seems useful while prototyping: think of postulate a : A as a shorthand for:

a :: A
a = undefined

(another way to do it is add a postulate in Prelude.undefined and use a full declaration)

[UlfNorell]

Would it be possible to (partially) apply all of these definitions and then compile? Or is this approach doomed to fail from your experience?

This should be possible. There's an Apply instance for Definition so hopefully you can grab the lhs variables of the clauseTel and simply apply them before compiling the where-functions.

[UlfNorell]

another way to do it is add a postulate in Prelude.undefined and use a full declaration

Hm.. since the objective is to prove things about the code, I'd rather not add undefined to the Prelude. Maybe it could be error "postulate: a" rather than undefined though.

[UlfNorell]

Progress! Still doesn't quite work for functions with multiple clauses.

[UlfNorell]

We're getting there! Some cosmetics and a problem with finding local declarations.

[UlfNorell]

Good job!