feat: Avoid boxing primitives in Go in sequence concatenations as well

Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy

@@ -159,6 +159,11 @@ abstract module {:options "/functionSyntax:4"} Dafny {
       ensures fresh(ret.Repr)
       ensures ret.Length() == length
 
+    static method {:axiom} {:extern} MakeWithPrototype<T>(length: size_t, prototype: ImmutableArray<T>) returns (ret: NativeArray<T>)
+      ensures ret.Valid()
+      ensures fresh(ret.Repr)
+      ensures ret.Length() == length
+
     static method {:axiom} {:extern} MakeWithInit<T>(length: size_t, initFn: size_t -> T) returns (ret: NativeArray<T>)
       ensures ret.Valid()
       ensures fresh(ret.Repr)
@@ -240,6 +245,20 @@ abstract module {:options "/functionSyntax:4"} Dafny {
       Repr := {this} + storage.Repr;
     }
 
+    // Note it is important to use this constructor
+    // if T may be compiled to a primitive type we want to avoid boxing,
+    // such as bytes or characters!
+    constructor WithPrototype(length: size_t, prototype: ImmutableArray<T>)
+      ensures Valid()
+      ensures Value() == []
+      ensures fresh(Repr)
+    {
+      var storage := NativeArray<T>.MakeWithPrototype(length, prototype);
+      this.storage := storage;
+      size := 0;
+      Repr := {this} + storage.Repr;
+    }
+
     ghost function Value(): seq<T>
       requires Valid()
       reads this, Repr
@@ -297,8 +316,8 @@ abstract module {:options "/functionSyntax:4"} Dafny {
         newCapacity := Max(newCapacity, storage.Length() * TWO_SIZE);
       }
 
-      var newStorage := NativeArray<T>.Make(newCapacity);
       var values := storage.Freeze(size);
+      var newStorage := NativeArray<T>.MakeWithPrototype(newCapacity, values);
       newStorage.UpdateSubarray(0, values);
       storage := newStorage;
 
@@ -404,6 +423,21 @@ abstract module {:options "/functionSyntax:4"} Dafny {
       decreases NodeCount, 2
       ensures |Value()| < SIZE_T_LIMIT && |Value()| as size_t == Cardinality()
 
+    // Returns an array of the same element type as this sequence.
+    // Used to ensure when we create more arrays of T elements
+    // that we optimize for common types like bytes and characters,
+    // even though in several Dafny backends we don't have enough type information
+    // at runtime from Dafny itself.
+    // TypeDescriptors would be the more general solution,
+    // but they are not present where we need them
+    // in most backends.
+    //
+    // Note this is very similar to the DafnySequence.newCopier(int length)
+    // method in the Java runtime.
+    method PrototypeArray() returns (ret: ImmutableArray<T>)
+      requires Valid()
+      decreases NodeCount, 1
+
     method Select(index: size_t) returns (ret: T)
       requires Valid()
       requires index < Cardinality()
@@ -604,6 +638,13 @@ abstract module {:options "/functionSyntax:4"} Dafny {
   class ArraySequence<T> extends Sequence<T> {
     const values: ImmutableArray<T>
 
+    method PrototypeArray() returns (ret: ImmutableArray<T>)
+      requires Valid()
+      decreases NodeCount, 1
+    {
+      return values;
+    }
+
     ghost predicate Valid()
       decreases NodeCount, 0
       ensures Valid() ==> 0 < NodeCount
@@ -653,6 +694,15 @@ abstract module {:options "/functionSyntax:4"} Dafny {
     const right: Sequence<T>
     const length: size_t
 
+    method PrototypeArray() returns (ret: ImmutableArray<T>)
+      requires Valid()
+      decreases NodeCount, 1
+    {
+      // This is arbitrary but should work well for the majority of cases,
+      // and is consistent with how the Java runtime currently handles the same problem.
+      ret := left.PrototypeArray();
+    }
+
     ghost predicate Valid()
       decreases NodeCount, 0
       ensures Valid() ==> 0 < NodeCount
@@ -702,7 +752,8 @@ abstract module {:options "/functionSyntax:4"} Dafny {
       ensures ret.Length() == Cardinality()
       ensures ret.values == Value()
     {
-      var builder := new Vector<T>(length);
+      var prototype := PrototypeArray();
+      var builder := new Vector<T>.WithPrototype(length, prototype);
       var stack := new Vector<Sequence<T>>(TEN_SIZE);
       AppendOptimized(builder, this, stack);
       ret := builder.Freeze();
@@ -814,6 +865,14 @@ abstract module {:options "/functionSyntax:4"} Dafny {
     const box: AtomicBox<Sequence<T>>
     const length: size_t
 
+    method PrototypeArray() returns (ret: ImmutableArray<T>)
+      requires Valid()
+      decreases NodeCount, 1
+    {
+      var expr : Sequence<T> := box.Get();
+      ret := expr.PrototypeArray();
+    }
+
     ghost predicate Valid()
       decreases NodeCount, 0
       ensures Valid() ==> 0 < NodeCount

Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go

@@ -750,6 +750,11 @@ func (CompanionStruct_NativeArray_) Make(length uint32) NativeArray {
 	return GoNativeArray{underlying: underlying}
 }
 
+func (CompanionStruct_NativeArray_) MakeWithPrototype(length uint32, prototype ImmutableArray) NativeArray {
+	underlying := prototype.(GoNativeArray).underlying.arrayNewOfSameType(int(length))
+	return GoNativeArray{underlying: underlying}
+}
+
 func (CompanionStruct_NativeArray_) MakeWithInit(length uint32, init func(uint32) interface{}) NativeArray {
 	underlying := newArrayWithInitFn(init, int(length))
 	return GoNativeArray{underlying: underlying}
@@ -806,6 +811,7 @@ type Array interface {
 	anySlice(lo, hi Int) []interface{}
 	arrayCopy() Array
 	arrayEqualUpTo(other Array, index int) bool
+	arrayNewOfSameType(length int) Array
 	// specializations
 	ArrayGet1Byte(index int) byte
 	ArraySet1Byte(value byte, index int)
@@ -953,6 +959,7 @@ func NewArrayFromExample(example interface{}, init interface{}, dims ...Int) Arr
 			arr[i] = init
 		}
 	}
+
 	return &arrayStruct{
 		contents: arr,
 		dims:     intDims,
@@ -1007,7 +1014,7 @@ func newArrayWithValues(values ...interface{}) Array {
 	}
 }
 
-// newArrayWithInitFn returns a new one-dimensional Array with the given initial values. 
+// newArrayWithInitFn returns a new one-dimensional Array with the given initial values.
 // It is currently only used internally, by CompanionStruct_NativeArray_.MakeWithInit.
 // It could potentially be used in the translation of Dafny array instantiations with initializing lambdas,
 // but that is currently rewritten by the single-pass compiler instead.
@@ -1119,7 +1126,7 @@ func (_this arrayStruct) arrayCopy() Array {
 	copy(newDims, _this.dims)
 	return &arrayStruct{
 		contents: newContents,
-		dims:    newDims,
+		dims:     newDims,
 	}
 }
 
@@ -1129,6 +1136,15 @@ func (_this arrayStruct) arrayEqualUpTo(other Array, index int) bool {
 	return defaultArrayEqualUpTo(_this, other, uint32(index))
 }
 
+func (_this arrayStruct) arrayNewOfSameType(length int) Array {
+	conents := make([]interface{}, length)
+	dims := []int{length}
+	return &arrayStruct{
+		contents: conents,
+		dims:     dims,
+	}
+}
+
 func (_this arrayStruct) ArrayGet1Byte(index int) byte {
 	panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}")
 }
@@ -1244,6 +1260,15 @@ func (_this arrayForByte) arrayEqualUpTo(other Array, index int) bool {
 	}
 }
 
+func (_this arrayForByte) arrayNewOfSameType(length int) Array {
+	conents := make([]byte, length)
+	dims := []int{length}
+	return &arrayForByte{
+		contents: conents,
+		dims:     dims,
+	}
+}
+
 func (_this arrayForByte) ArrayGet1Byte(index int) byte {
 	return _this.contents[index]
 }
@@ -1361,6 +1386,15 @@ func (_this arrayForChar) arrayEqualUpTo(other Array, index int) bool {
 	}
 }
 
+func (_this arrayForChar) arrayNewOfSameType(length int) Array {
+	conents := make([]Char, length)
+	dims := []int{length}
+	return &arrayForChar{
+		contents: conents,
+		dims:     dims,
+	}
+}
+
 func (_this arrayForChar) ArrayGet1Byte(index int) byte {
 	panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}")
 }
@@ -1464,7 +1498,7 @@ func (_this arrayForCodePoint) arrayCopy() Array {
 	return &arrayForCodePoint{
 		contents: newContents,
 		// TODO: Does dims have to be copied as well?
-		dims:     _this.dims,
+		dims: _this.dims,
 	}
 }
 
@@ -1477,6 +1511,15 @@ func (_this arrayForCodePoint) arrayEqualUpTo(other Array, index int) bool {
 	}
 }
 
+func (_this arrayForCodePoint) arrayNewOfSameType(length int) Array {
+	conents := make([]CodePoint, length)
+	dims := []int{length}
+	return &arrayForCodePoint{
+		contents: conents,
+		dims:     dims,
+	}
+}
+
 func (_this arrayForCodePoint) ArrayGet1Byte(index int) byte {
 	panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}")
 }