Speculative normalisation (#1902)

* Split Normalise into three files

Evaluation, Quoting, and Conversion checking are distinct steps, and I'm
about to add some variations to quoting so better to reorganise a bit.

* Add a Quote mode that limits size of result

Sometimes normalising an expression is a good idea because it makes
things smaler, and sometimes it isnt, because it doesn't. We can't tell
in advance which situation we're in, but we can try speculatively
normalising something. This is good for case types and hole types - we
generally want the normal form, but if that's expensive, we should stop.

So, quote is now able to give up if it passes a certain size threshold
for stuck applications. By experimentation, it seems that up to 10
doesn't hurt too much, but beyond that it's better not to normalise at
all.

* Add the new normalise files

Author: edwinb

idris2api.ipkg

@@ -61,6 +61,9 @@ modules =
     Core.Name,
     Core.Name.Namespace,
     Core.Normalise,
+    Core.Normalise.Convert,
+    Core.Normalise.Eval,
+    Core.Normalise.Quote,
     Core.Options,
     Core.Options.Log,
     Core.Ord,