edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

Add noNewtype option to data types #340

Closed chrrasmussen closed 4 years ago

chrrasmussen commented 4 years ago

Since the newtype optimisation was added (471a47255fb2757b0efce52560e30a0aa88bdeaa), code generators are no longer able to add special handling of the generated constructor/deconstructor for data types that are affected by the newtype optimisation.

To restore this functionality, I have added a new option (noNewtype) to disable the newtype optimisation for individual data types.

Motivation

In my Erlang code generator I have added special handling to some data types, like ErlAtom, ErlBinary and ErlCharlist (from the Erlang module). By doing this I can convert values between an Idris-specific representation to an Erlang-specific representation (and back), like so:

These data types fulfil the critera for the newtype optimisation, which means that, without the noNewtype option, the code generator is unable to add its own special handling.

Other comments

edwinb commented 4 years ago

Good idea, thanks!