[CakeML-dev] Partial applications in CF

[Armaël Guéneau]

Hi Ramana,

Short answer: yes, partial application of CF specs is possible and is
supposed to be handled, but not everything is implemented at the moment.

Long answer: cfAppScript defines a [curried] predicate. [curried n f]
means that [f] is curried [n] times. At the moment nothing is really
proved about [curried]; the intention is to have lemmas that given a
[app f [x1..xn] ...] and a [curried n f], produce a specification [app f
[x1..xi] ...] for i <> n; i.e. allow to apply less or more arguments
than defined in the spec.

So, to do what you need, the following needs to be done:
- prove the required lemmas about [curried]
- have [xapp] use a [curried] ... theorem when needed
- produce a [curried ...] theorem from translator specifications, to go
with the [app ...] theorem.

I'm putting these items on top of my todo-list.

— Armaël

On 09/03/2017 03:52, Ramana Kumar wrote:
> Hi Armaël, Magnus, developers,
> 
> Do you know how to use CF for partial applications of
> translator-verified functions? It seems that app_of_Arrow_rule always
> produces an app spec with the maximum number of arguments applied. Is
> it possible to use this app spec (with xapp) in a situation where
> only, say, the first out of two arguments has been applied?
> 
> If that is not possible, what is a good workaround? Do I need to
> define a new function for every partial application?
> 
> Cheers,
> Ramana
> 
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>