[CakeML-dev] Partial applications in CF

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Fri Mar 10 00:27:40 UTC 2017


Hi Armaël,

Good to hear that CF will support partial applications.

My workaround was to prove a partial application spec manually, using
the definition of app:
https://github.com/CakeML/cakeml/blob/examples/characteristic/examples/grepProgScript.sml#L589
I also did an eta transformation on the code to force a cf_fun
https://github.com/CakeML/cakeml/blob/examples/characteristic/examples/grepProgScript.sml#L617

When your updates come through, we can go back to writing the
"natural" code and avoid the manually proven partial app spec.

Cheers,
Ramana

On 10 March 2017 at 00:47, Armaël Guéneau <armael.gueneau at ens-lyon.fr> wrote:
> 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
>>



More information about the Developers mailing list