[CakeML-dev] Partial applications in CF
Ramana.Kumar at cl.cam.ac.uk
Fri Mar 10 00:27:40 UTC 2017
Good to hear that CF will support partial applications.
My workaround was to prove a partial application spec manually, using
the definition of app:
I also did an eta transformation on the code to force a cf_fun
When your updates come through, we can go back to writing the
"natural" code and avoid the manually proven partial app spec.
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?
>> Developers mailing list
>> Developers at cakeml.org
More information about the Developers