Optimize DafnySequence<Character> to String

[robin-aws]

(Re-cutting #819 on olivergillespie's behalf)

Optimize performance of ToNative$Simple.String. I saw in an allocation profile of my application that this code is creating a lot of garbage, principally from calling Character.toString on every element, which creates a whole String object and backing byte[]. The Stream is wasteful too.

Move to a StringBuilder and for loop. A very rough benchmark shows about 80% reduction in allocations and total time taken.

Small string (4 chars):

	Time	Allocation
Baseline	159 ns/op	608 bytes/op
Optimized	37 ns/op	96 bytes/op

Larger string (88 chars):

	Time	Allocation
Baseline	2079 ns/op	5360 bytes/op
Optimized	419 ns/op	816 bytes/op

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.