Implement pragma for declaring nat optimizations

[fabianhjr]

No description provided.

[fabianhjr]

Helped me improve the performance of an alternative idris2 prelude I am playing with, tested with mock of ProjectEuler problem #1:

module NaiveSolution

import Prelude

import Data.Integral
import Data.Nat.Integral

main : LinkedList Nat
main = filter (`divBy` (the Nat 3)) [(the Nat 1)..100]

[fabianhjr]

Marceline discovered that this PR causes an explosion of memory usage while compiling Idris2 in Core/Binary (Extra ~ 5GB or so of memory usage)

[edwinb]

This does make the nat hack a bit less hacky, thanks! Is the compile time performance still an issue? Sometimes that can be due to ambiguity resolution going a bit out of control.

[fabianhjr]

Yes, there is still an issue with Idris1 compilation of Idris2.

Idris2 runs fine though.

[gallais]

Could we refactor this as something like:

do c <- builtinPragma
   n <- name
   atEnd indents
   pure (c n)

where builtinPragma is a big choice of parsers of the form
PrimNatSucc <$ pragma "builtinNatSucc"