| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Compiler.Treeless.Builtin
Description
Translates the Agda builtin nat datatype to arbitrary-precision integers.
Philipp, 20150921: At the moment, this optimization is the reason that there is a TAPlus alternative. For Haskell, this can easily be translated to guards. However, in the long term it would be easier for the backends if these things were translated directly to a less-than primitive and if-then-else expressions or similar. This would require us to add some internal Bool-datatype as compiler-internal type and a primitive less-than function, which will be much easier once Treeless is used for whole modules.
Ulf, 2015-09-21: No, actually we need the n+k patterns, or at least guards. Representing them with if-then-else would make it a lot harder to do optimisations that analyse case tree, like impossible case elimination.
Ulf, 2015-10-30: Guards are actually a better primitive. Fixed that.