diff --git a/.github/workflows/library_interop_keyring_test_vectors.yml b/.github/workflows/library_interop_keyring_test_vectors.yml index ce41dedd1..fa4fe8096 100644 --- a/.github/workflows/library_interop_keyring_test_vectors.yml +++ b/.github/workflows/library_interop_keyring_test_vectors.yml @@ -65,7 +65,9 @@ jobs: - name: Install LibCurl if: matrix.os == 'ubuntu-22.04' && matrix.language == 'c' - run: sudo apt-get install libcurl4-openssl-dev + run: | + sudo apt-get update + sudo apt-get install -y libcurl4-openssl-dev - name: Checkout C-ESDK if: matrix.language == 'c' @@ -338,7 +340,9 @@ jobs: - name: Install LibCurl if: matrix.os == 'ubuntu-22.04' && matrix.decrypting_language == 'c' - run: sudo apt-get install libcurl4-openssl-dev + run: | + sudo apt-get update + sudo apt-get install -y libcurl4-openssl-dev - name: Checkout C-ESDK if: matrix.decrypting_language == 'c' diff --git a/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod index 2cab70f42..e368192b0 100644 --- a/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod +++ b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod @@ -45,3 +45,5 @@ require ( github.com/google/uuid v1.6.0 // indirect github.com/jmespath/go-jmespath v0.4.0 // indirect ) + +replace github.com/dafny-lang/DafnyRuntimeGo/v4 => ../../../../esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4 diff --git a/TestVectors/runtimes/go/ImplementationFromDafny-go/go.sum b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.sum index 7391db490..25a116da7 100644 --- a/TestVectors/runtimes/go/ImplementationFromDafny-go/go.sum +++ b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.sum @@ -30,8 +30,6 @@ github.com/aws/aws-sdk-go-v2/service/sts v1.33.8 h1:pqEJQtlKWvnv3B6VRt60ZmsHy3So github.com/aws/aws-sdk-go-v2/service/sts v1.33.8/go.mod h1:f6vjfZER1M17Fokn0IzssOTMT2N8ZSq+7jnNF0tArvw= github.com/aws/smithy-go v1.22.1 h1:/HPHZQ0g7f4eUeK6HKglFz8uwVfZKgoI25rb/J+dnro= github.com/aws/smithy-go v1.22.1/go.mod h1:irrKGvNn1InZwb2d7fkIRNucdfwR8R+Ts3wxYa/cJHg= -github.com/dafny-lang/DafnyRuntimeGo/v4 v4.11.1 h1:tTQ9M9HCUaf2SXqutj2vmMqJKJpefWMSqx1niqTqi8M= -github.com/dafny-lang/DafnyRuntimeGo/v4 v4.11.1/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto= github.com/davecgh/go-spew v1.1.0 h1:ZDRjVQ15GmhC3fiQ8ni8+OwkZQO4DARzQgrnXU1Liz8= github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38= github.com/google/uuid v1.6.0 h1:NIvaJDMOsjHA8n1jAhLSgzrAzy1Hgr+hNrb57e+94F0= diff --git a/TestVectors/runtimes/go/TestsFromDafny-go/go.mod b/TestVectors/runtimes/go/TestsFromDafny-go/go.mod index d7349b733..578a804d9 100644 --- a/TestVectors/runtimes/go/TestsFromDafny-go/go.mod +++ b/TestVectors/runtimes/go/TestsFromDafny-go/go.mod @@ -47,3 +47,5 @@ require ( github.com/google/uuid v1.6.0 // indirect github.com/jmespath/go-jmespath v0.4.0 // indirect ) + +replace github.com/dafny-lang/DafnyRuntimeGo/v4 => ../../../../esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4 diff --git a/TestVectors/runtimes/go/TestsFromDafny-go/go.sum b/TestVectors/runtimes/go/TestsFromDafny-go/go.sum index 7391db490..25a116da7 100644 --- a/TestVectors/runtimes/go/TestsFromDafny-go/go.sum +++ b/TestVectors/runtimes/go/TestsFromDafny-go/go.sum @@ -30,8 +30,6 @@ github.com/aws/aws-sdk-go-v2/service/sts v1.33.8 h1:pqEJQtlKWvnv3B6VRt60ZmsHy3So github.com/aws/aws-sdk-go-v2/service/sts v1.33.8/go.mod h1:f6vjfZER1M17Fokn0IzssOTMT2N8ZSq+7jnNF0tArvw= github.com/aws/smithy-go v1.22.1 h1:/HPHZQ0g7f4eUeK6HKglFz8uwVfZKgoI25rb/J+dnro= github.com/aws/smithy-go v1.22.1/go.mod h1:irrKGvNn1InZwb2d7fkIRNucdfwR8R+Ts3wxYa/cJHg= -github.com/dafny-lang/DafnyRuntimeGo/v4 v4.11.1 h1:tTQ9M9HCUaf2SXqutj2vmMqJKJpefWMSqx1niqTqi8M= -github.com/dafny-lang/DafnyRuntimeGo/v4 v4.11.1/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto= github.com/davecgh/go-spew v1.1.0 h1:ZDRjVQ15GmhC3fiQ8ni8+OwkZQO4DARzQgrnXU1Liz8= github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38= github.com/google/uuid v1.6.0 h1:NIvaJDMOsjHA8n1jAhLSgzrAzy1Hgr+hNrb57e+94F0= diff --git a/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/.gitignore b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/.gitignore new file mode 100644 index 000000000..6f6f5e6ad --- /dev/null +++ b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/.gitignore @@ -0,0 +1,22 @@ +# If you prefer the allow list template instead of the deny list, see community template: +# https://github.com/github/gitignore/blob/main/community/Golang/Go.AllowList.gitignore +# +# Binaries for programs and plugins +*.exe +*.exe~ +*.dll +*.so +*.dylib + +# Test binary, built with `go test -c` +*.test + +# Output of the go coverage tool, specifically when used with LiteIDE +*.out + +# Dependency directories (remove the comment below to include it) +# vendor/ + +# Go workspace file +go.work +go.work.sum diff --git a/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/LICENSE b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/LICENSE new file mode 100644 index 000000000..19030ac32 --- /dev/null +++ b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2024 Dafny + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/README.md b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/README.md new file mode 100644 index 000000000..4881ed7a8 --- /dev/null +++ b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/README.md @@ -0,0 +1,3 @@ +# DafnyRuntimeGo + +The Go version of the Dafny runtime library diff --git a/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/go.mod b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/go.mod new file mode 100644 index 000000000..5aa34e4cd --- /dev/null +++ b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/go.mod @@ -0,0 +1,3 @@ +module github.com/dafny-lang/DafnyRuntimeGo + +go 1.21 diff --git a/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/System_/System_.go b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/System_/System_.go new file mode 100644 index 000000000..26534ed77 --- /dev/null +++ b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/System_/System_.go @@ -0,0 +1,56 @@ +// Package _System +// Dafny module _System compiled into Go + +package _System + +import ( + os "os" + + _dafny "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" +) + +var _ = os.Args +var _ _dafny.Dummy__ + +type Dummy__ struct{} + +// Definition of class Nat +type Nat struct { +} + +func New_Nat_() *Nat { + _this := Nat{} + + return &_this +} + +type CompanionStruct_Nat_ struct { +} + +var Companion_Nat_ = CompanionStruct_Nat_{} + +func (*Nat) String() string { + return "_System.Nat" +} + +// End of class Nat + +func Type_Nat_() _dafny.TypeDescriptor { + return type_Nat_{} +} + +type type_Nat_ struct { +} + +func (_this type_Nat_) Default() interface{} { + return _dafny.Zero +} + +func (_this type_Nat_) String() string { + return "_System.Nat" +} +func (_this *CompanionStruct_Nat_) Is_(__source _dafny.Int) bool { + var _0_x _dafny.Int = (__source) + _ = _0_x + return (_0_x).Sign() != -1 +} diff --git a/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/dafny/dafny.go b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/dafny/dafny.go new file mode 100644 index 000000000..a000fabdd --- /dev/null +++ b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/dafny/dafny.go @@ -0,0 +1,3522 @@ +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT + +package dafny + +import ( + "fmt" + big "math/big" + "os" + refl "reflect" + "runtime" + "slices" + "unicode/utf8" +) + +func FromMainArguments(args []string) Sequence { + var size = len(args) + var dafnyArgs []interface{} = make([]interface{}, size) + for i, item := range args { + dafnyArgs[i] = SeqOfString(item) + } + return SeqOf(dafnyArgs...) +} + +func UnicodeFromMainArguments(args []string) Sequence { + var size = len(args) + var dafnyArgs []interface{} = make([]interface{}, size) + for i, item := range args { + dafnyArgs[i] = UnicodeSeqOfUtf8Bytes(item) + } + return SeqOf(dafnyArgs...) +} + +/****************************************************************************** + * Generic values + ******************************************************************************/ + +// An EqualsGeneric can be compared to any other object. This method should +// *only* return true when the other value is of the same type. +type EqualsGeneric interface { + EqualsGeneric(other interface{}) bool +} + +// AreEqual compares two values for equality in a generic way. Besides the +// refl.DeepEqual logic (to which this method defers as a last resort), the +// values are handled intelligently if their type is refl.Value or any type that +// implements the EqualsGeneric interface. +func AreEqual(x, y interface{}) bool { + if IsDafnyNull(x) { + return IsDafnyNull(y) + } + if IsDafnyNull(y) { + return false + } + switch x := x.(type) { + case refl.Value: + { + y, ok := y.(refl.Value) + return ok && x.CanInterface() && y.CanInterface() && + AreEqual(x.Interface(), y.Interface()) + } + case EqualsGeneric: + return x.EqualsGeneric(y) + default: + return refl.DeepEqual(x, y) + } +} + +// Checking for `Comparable` doesn't work, because it matches things for which == fails. +// This is a non-exhaustive list of types, but should include the things that are most performance critical +func IsEqualityComparable(i interface{}) bool { + switch i.(type) { + case uint8, Char, CodePoint: + return true + default: + return false + } +} + +func (_static *CompanionStruct_Sequence_) EqualUpTo(left Sequence, right Sequence, index uint32) bool { + if index == 0 { + return true + } + + leftArr, rightArr := left.ToArray(), right.ToArray() + return leftArr.(GoNativeArray).underlying.arrayEqualUpTo(rightArr.(GoNativeArray).underlying, int(index)) +} + +func IsDafnyNull(x interface{}) bool { + if x == nil { + return true + } + v := refl.ValueOf(x) + if v.Kind() == refl.Ptr { + return v.IsNil() + } + return false +} + +func isNil(v refl.Value) bool { + switch v.Kind() { + case refl.Chan, refl.Func, refl.Map, refl.Ptr, refl.Slice: + return v.IsNil() + case refl.Interface: + return v.IsNil() || v.Elem().IsNil() + default: + return false + } +} + +// String formats the given value using fmt.Sprint, unless it's nil, in which +// case it formats it as "null" to conform to other languages' output. +func String(x interface{}) string { + if x == nil { + return "null" + } + v := refl.ValueOf(x) + if isNil(v) { + return "null" + } + if v.Kind() == refl.Func { + return v.Type().String() + } + return fmt.Sprint(x) +} + +// Print prints the given value using fmt.Print, formatted using String. +func Print(x interface{}) { + fmt.Print(String(x)) +} + +// SetFinalizer is a re-export of runtime.SetFinalizer. Included here so that +// only this module needs to be imported by every Dafny module. +func SetFinalizer(x interface{}, f interface{}) { + runtime.SetFinalizer(x, f) +} + +/****************************************************************************** + * Run-time type descriptors (RTDs) + ******************************************************************************/ + +// A TypeDescriptor has the ability to produce a default value for an associated type. +type TypeDescriptor interface { + Default() interface{} +} + +func CreateStandardTypeDescriptor(value interface{}) TypeDescriptor { + return standardTypeDescriptor{value} +} + +type standardTypeDescriptor struct { + defaultValue interface{} +} + +func (rtd standardTypeDescriptor) Default() interface{} { + return rtd.defaultValue +} + +// IntType is the RTD for int +var IntType = CreateStandardTypeDescriptor(Zero) + +// BoolType is the RTD of bool +var BoolType = CreateStandardTypeDescriptor(false) + +// CharType is the RTD of char +var CharType = CreateStandardTypeDescriptor(Char('D')) // See CharType.DefaultValue in Dafny source code + +// CodePointType is the RTD of char +var CodePointType = CreateStandardTypeDescriptor(CodePoint('D')) // See CharType.DefaultValue in Dafny source code + +// RealType is the RTD for real +var RealType = CreateStandardTypeDescriptor(ZeroReal) + +// Int64Type is the RTD of int64. +var Int64Type = CreateStandardTypeDescriptor(int64(0)) + +// PossiblyNullType is the RTD of any possibly null reference type +var PossiblyNullType = CreateStandardTypeDescriptor((*interface{})(nil)) + +// Uint8Type is the RTD of uint8 +var Uint8Type = CreateStandardTypeDescriptor(uint8(0)) + +// Uint16Type is the RTD of uint16 +var Uint16Type = CreateStandardTypeDescriptor(uint16(0)) + +// Uint32Type is the RTD of uint32 +var Uint32Type = CreateStandardTypeDescriptor(uint32(0)) + +// Uint64Type is the RTD of uint64 +var Uint64Type = CreateStandardTypeDescriptor(uint64(0)) + +// SetType is the RTD for sets +var SetType = CreateStandardTypeDescriptor(EmptySet) + +// MultiSetType is the RTD for multisets +var MultiSetType = CreateStandardTypeDescriptor(EmptyMultiSet) + +// SeqType is the RTD for sequences +var SeqType = CreateStandardTypeDescriptor(EmptySeq) + +// MapType is the RTD for maps +var MapType = CreateStandardTypeDescriptor(EmptyMap) + +/****************************************************************************** + * Trait parent information + ******************************************************************************/ + +// Every class gets compiled to have a ParentTraits_ method, which returns the +// list of Dafny parent traits (including transitive parent traits). This is +// used to determine, at run time, if a given object satisfies a particular trait. +// While it is unusual that this information is needed, it is needed in a situation +// like +// var s: set := ... +// // the following line requires run-time check that t (of type UberTrait) is a Trait +// var ts := set t: Trait | t in s; +// A more straightforward situation is the expression +// x is Trait + +type TraitID struct { + dummy byte +} + +type TraitOffspring interface { + ParentTraits_() []*TraitID +} + +func InstanceOfTrait(obj TraitOffspring, trait *TraitID) bool { + for _, parent := range obj.ParentTraits_() { + if parent == trait { + return true + } + } + return false +} + +// Use this method to test if an object "p" has a given class type (denoted by the +// type of "q"). More generally, this method returns true if p and q are of the +// same type. It is assumed that neither "p" nor "q" denotes a Dafny "null" value. + +func InstanceOf(p interface{}, q interface{}) bool { + return refl.TypeOf(p) == refl.TypeOf(q) +} + +/****************************************************************************** + * Object + ******************************************************************************/ + +type Object struct { + dummy byte +} + +func New_Object() *Object { + _this := Object{} + return &_this +} + +func (_this *Object) Equals(other *Object) bool { + return _this == other +} + +func (_this *Object) EqualsGeneric(x interface{}) bool { + other, ok := x.(*Object) + return ok && _this.Equals(other) +} + +func (*Object) String() string { + return "object" +} + +func (_this *Object) ParentTraits_() []*TraitID { + return [](*TraitID){} +} + +var _ TraitOffspring = &Object{} + +/****************************************************************************** + * Characters + ******************************************************************************/ + +// A Char is a rune in a wrapper so that we can detect it and treat it +// distinctly from int32. +type Char rune + +func (char Char) String() string { + return fmt.Sprintf("%c", rune(char)) +} + +// AllChars returns an iterator that returns all 16-bit characters. +func AllChars() Iterator { + c := int32(0) + return func() (interface{}, bool) { + if c >= 0x10000 { + return -1, false + } else { + ans := Char(c) + c++ + return ans, true + } + } +} + +type CodePoint rune + +func (cp CodePoint) Escape() string { + switch rune(cp) { + case '\n': + return "\\n" + case '\r': + return "\\r" + case '\t': + return "\\t" + case '\x00': + return "\\0" + case '\'': + return "\\'" + case '"': + return "\\\"" + case '\\': + return "\\\\" + default: + return fmt.Sprintf("%c", rune(cp)) + } +} + +func (cp CodePoint) String() string { + return fmt.Sprintf("'%s'", cp.Escape()) +} + +func IsCodePoint(i Int) bool { + return ((i.Sign() != -1 && i.Cmp(IntOfInt32(0xD800)) < 0) || + (IntOfInt32(0xE000).Cmp(i) <= 0 && i.Cmp(IntOfInt32(0x11_0000)) < 0)) +} + +// AllUnicodeChars returns an iterator that returns all Unicode scalar values. +func AllUnicodeChars() Iterator { + c := int32(0) + return func() (interface{}, bool) { + if c >= 0x11_0000 { + return -1, false + } else { + if c == 0xD800 { + // Skip over the surrogates + c = 0xE000 + } + ans := CodePoint(c) + c++ + return ans, true + } + } +} + +/****************************************************************************** + * Slices + ******************************************************************************/ + +func sliceEquals(s1, s2 []interface{}) bool { + return len(s1) == len(s2) && sliceIsPrefixAfterLengthCheck(s1, s2) +} + +func sliceIsPrefixOf(s1, s2 []interface{}) bool { + return len(s1) <= len(s2) && sliceIsPrefixAfterLengthCheck(s1, s2) +} + +func sliceIsProperPrefixOf(s1, s2 []interface{}) bool { + return len(s1) < len(s2) && sliceIsPrefixAfterLengthCheck(s1, s2) +} + +func sliceIsPrefixAfterLengthCheck(s1, s2 []interface{}) bool { + for i, v := range s1 { + if !(AreEqual(v, s2[i])) { + return false + } + } + return true +} + +func sliceContains(s []interface{}, value interface{}) bool { + for _, v := range s { + if AreEqual(v, value) { + return true + } + } + return false +} + +// Iterator returns an iterator over the sequence. +func sliceIterator(s []interface{}) Iterator { + i := 0 + n := len(s) + return func() (interface{}, bool) { + if i >= n { + return nil, false + } + ans := s[i] + i++ + return ans, true + } +} + +func stringOfElements(iter interface{}) string { + str := "" + sep := "" + for i := Iterate(iter); ; { + v, ok := i() + if !ok { + break + } + + str += sep + str += String(v) + sep = ", " + } + return str +} + +/****************************************************************************** + * Iteration + ******************************************************************************/ + +// An Iterator is a function that can be called multiple times to get successive +// values, until the second value returned is false. +type Iterator = func() (interface{}, bool) + +// An Iterable can produce an iterator, which we represent as a function which +// can be called to get successive values. +type Iterable interface { + Iterator() Iterator +} + +// Iterate gets an iterator from a value that is either an iterator or an +// iterable. +func Iterate(over interface{}) Iterator { + switch over := over.(type) { + case Iterator: + return over + case Iterable: + return over.Iterator() + default: + if refl.TypeOf(over).Kind() != refl.Slice { + panic(fmt.Errorf("Not iterable: %v", over)) + } else { + return anySliceIterator(over) + } + } +} + +func anySliceIterator(slice interface{}) Iterator { + val := refl.ValueOf(slice) + n := val.Len() + i := 0 + return func() (interface{}, bool) { + if i >= n { + return nil, false + } else { + ans := val.Index(i).Interface() + i++ + return ans, true + } + } +} + +// Quantifier calculates whether a predicate holds either for all values yielded +// by an iterator or for at least one. +func Quantifier(iter interface{}, isForAll bool, pred interface{}) bool { + predVal := refl.ValueOf(pred) + + for i := Iterate(iter); ; { + v, ok := i() + if !ok { + return isForAll + } + if predVal.Call([]refl.Value{refl.ValueOf(v)})[0].Interface() != isForAll { + return !isForAll + } + } +} + +// SingleValue produces an iterator that yields only a single value. +func SingleValue(value interface{}) Iterator { + done := false + return func() (interface{}, bool) { + if done { + return nil, false + } else { + done = true + return value, true + } + } +} + +// AllBooleans returns an iterator that returns false, then returns true. +func AllBooleans() Iterator { + phase := 0 + return func() (interface{}, bool) { + switch phase { + case 0: + phase = 1 + return false, true + case 1: + phase = 2 + return true, true + default: + return false, false + } + } +} + +/****************************************************************************** + * Sequences + ******************************************************************************/ + +// The sequence type is now defined in dafnyRuntime.dfy instead. +// These declarations are just filling in the gaps to make sure +// Dafny.Sequence is a well-behaved Dafny value in this runtime. + +// EmptySeq is the empty sequence. +var EmptySeq = SeqOf() + +// Create a sequence from a length and an element initializer +// This still exists because it's technically difficult +// for the compiler to coerce the init function to a +// func (uint32) interface{}. +func SeqCreate(n uint32, init func(Int) interface{}) Sequence { + return Companion_Sequence_.Create(n, func(index uint32) interface{} { + return init(IntOfUint32(index)) + }) +} + +// WARNING: This function uses the given array directly without making a defensive copy. +// This is only safe if the array never changes afterward. +func SeqFromArray(contents []interface{}, isString bool) Sequence { + return unsafeSeqWrappingDafnyArray(unsafeWrapArray(contents), isString) +} + +// SeqOf returns a sequence containing the given values. +func SeqOf(values ...interface{}) Sequence { + return unsafeSeqWrappingDafnyArray(newArrayWithValues(values...), false) +} + +// SeqOfChars returns a sequence containing the given character values. +func SeqOfChars(values ...Char) Sequence { + return unsafeSeqWrappingDafnyArray(newArrayFromCharArray(values), true) +} + +func SeqOfBytes(values []byte) Sequence { + return unsafeSeqWrappingDafnyArray(newArrayFromByteArray(values), false) +} + +func unsafeSeqWrappingDafnyArray(array Array, isString bool) Sequence { + result := New_ArraySequence_() + result.Ctor__(GoNativeArray{underlying: array}, isString) + return result +} + +// SeqOfString converts the given string into a sequence of characters. +// The given string must contain only ASCII characters! +func SeqOfString(str string) Sequence { + // Need to make sure the elements of the array are Chars + arr := make([]interface{}, len(str)) + for i, v := range str { + arr[i] = Char(v) + } + return SeqFromArray(arr, true) +} + +func UnicodeSeqOfUtf8Bytes(str string) Sequence { + // Need to make sure the elements of the array are CodePoints + arr := make([]interface{}, utf8.RuneCountInString(str)) + i := 0 + for _, v := range str { + arr[i] = CodePoint(v) + i++ + } + return SeqFromArray(arr, false) +} + +// Iterator returns an iterator over the sequence. +// This could be implemented more efficiently +// in the source Dafny code in the future, +// by traversing the Sequence node structure rather than +// forcing the lazy evaluation, +// but will involve defining an Iterator trait of some kind. +func SequenceIterator(seq Sequence) Iterator { + var i uint32 = 0 + n := seq.Cardinality() + return func() (interface{}, bool) { + if i >= n { + return nil, false + } + ans := seq.Select(i) + i++ + return ans, true + } +} + +// Unfortunately when we want to provide a single common definition +// for a trait function, we have to take care of the indirection +// from the concrete structs to the trait implementation ourselves. +// Ideally there would be a way of telling Dafny +// an {:extern} trait method will be specifically implemented at the trait level +// so the compiler could do this for us. +func (seq *ArraySequence) Iterator() Iterator { + return SequenceIterator(seq) +} +func (seq *ConcatSequence) Iterator() Iterator { + return SequenceIterator(seq) +} +func (seq *LazySequence) Iterator() Iterator { + return SequenceIterator(seq) +} + +// UniqueElements returns the set of elements in the sequence. +// This should be in Dafny eventually but for now it's much more efficient +// and convenient here. +func (seq *ArraySequence) UniqueElements() Set { + return NewBuilderOf(seq).ToSet() +} +func (seq *ConcatSequence) UniqueElements() Set { + return NewBuilderOf(seq).ToSet() +} +func (seq *LazySequence) UniqueElements() Set { + return NewBuilderOf(seq).ToSet() +} + +func SequenceString(seq Sequence) string { + if seq.IsString() { + s := "" + // FIXME: Note this doesn't produce the right string in UTF-8, + // since it converts surrogates independently. + for i := Iterate(seq); ; { + c, ok := i() + if !ok { + break + } + s += c.(Char).String() + } + return s + } else { + return "[" + stringOfElements(seq) + "]" + } +} +func (seq *ArraySequence) String() string { + return SequenceString(seq) +} +func (seq *ConcatSequence) String() string { + return SequenceString(seq) +} +func (seq *LazySequence) String() string { + return SequenceString(seq) +} + +func SequenceVerbatimString(seq Sequence, asLiteral bool) string { + s := "" + if asLiteral { + s += "\"" + } + for i := Iterate(seq); ; { + c, ok := i() + if !ok { + break + } + + if asLiteral { + s += c.(CodePoint).Escape() + } else { + s += fmt.Sprintf("%c", c.(CodePoint)) + } + } + if asLiteral { + s += "\"" + } + return s +} +func (seq *ArraySequence) VerbatimString(asLiteral bool) string { + return SequenceVerbatimString(seq, asLiteral) +} +func (seq *ConcatSequence) VerbatimString(asLiteral bool) string { + return SequenceVerbatimString(seq, asLiteral) +} +func (seq *LazySequence) VerbatimString(asLiteral bool) string { + return SequenceVerbatimString(seq, asLiteral) +} + +func (seq *ArraySequence) Equals(other Sequence) bool { + return Companion_Sequence_.Equal(seq, other) +} +func (seq *ConcatSequence) Equals(other Sequence) bool { + return Companion_Sequence_.Equal(seq, other) +} +func (seq *LazySequence) Equals(other Sequence) bool { + return Companion_Sequence_.Equal(seq, other) +} + +func (seq *ArraySequence) EqualsGeneric(x interface{}) bool { + other, ok := x.(Sequence) + return ok && Companion_Sequence_.Equal(seq, other) +} +func (seq *ConcatSequence) EqualsGeneric(x interface{}) bool { + other, ok := x.(Sequence) + return ok && Companion_Sequence_.Equal(seq, other) +} +func (seq *LazySequence) EqualsGeneric(x interface{}) bool { + other, ok := x.(Sequence) + return ok && Companion_Sequence_.Equal(seq, other) +} + +func (seq *ArraySequence) ToByteArray() []byte { + return ToByteArray(seq) +} +func (seq *ConcatSequence) ToByteArray() []byte { + return ToByteArray(seq) +} +func (seq *LazySequence) ToByteArray() []byte { + return ToByteArray(seq) +} + +func ToByteArray(x Sequence) []byte { + switch x := x.(type) { + + case *LazySequence: + return ToByteArray(x.Box().Get().(Sequence)) + case *ConcatSequence: + leftByteArray := ToByteArray(x._left) + rightByteArray := ToByteArray(x._right) + return append(leftByteArray, rightByteArray...) + + default: + arr := x.ToArray() + length := arr.Length() + result := make([]byte, length) + // Optimize for the same kind of content array + if arrayByte, ok := arr.(GoNativeArray).underlying.(*arrayForByte); ok { + copy(result, arrayByte.contents) + } else { + for i := uint32(0); i < length; i++ { + result[i] = arr.Select(i).(byte) + } + } + return result + } +} + +/****************************************************************************** + * Arrays + ******************************************************************************/ + +// A GoNativeArray is a single dimensional Array, +// wrapped up for the benefit of dafnyRuntime.dfy. +// GoNativeArray wraps the Array interface for external compatibility +// while allowing optimized implementations internally. +type GoNativeArray struct { + underlying Array +} + +func (CompanionStruct_NativeArray_) Make(length uint32) NativeArray { + underlying := &arrayStruct{ + contents: make([]interface{}, length), + dims: []int{int(length)}, + } + 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} +} + +func (CompanionStruct_NativeArray_) Copy(other ImmutableArray) NativeArray { + return GoNativeArray{underlying: other.(GoNativeArray).underlying.arrayCopy()} +} + +func (g GoNativeArray) Length() uint32 { + return uint32(g.underlying.dimensionLength(0)) +} + +func (g GoNativeArray) Select(i uint32) interface{} { + return g.underlying.ArrayGet1(int(i)) +} + +func (g GoNativeArray) Update(i uint32, t interface{}) { + g.underlying.ArraySet1(t, int(i)) +} + +func (g GoNativeArray) UpdateSubarray(i uint32, other ImmutableArray) { + g.underlying.arraySetRange1(int(i), other.(GoNativeArray).underlying) +} + +func (g GoNativeArray) Freeze(size uint32) ImmutableArray { + return g.Subarray(0, size) +} + +func (g GoNativeArray) Subarray(lo, hi uint32) ImmutableArray { + return GoNativeArray{underlying: g.underlying.arrayGetRange1(IntOfUint32(lo), IntOfUint32(hi))} +} + +func (g GoNativeArray) String() string { + return "dafny.GoNativeArray" +} + +// Array is the general interface for arrays. Conceptually, it contains some +// underlying storage (a slice) of elements, together with a record of the length +// of each dimension. Thus, this general interface supports 1- and multi-dimensional +// Dafny arrays. +// +// All array indices are given as the Go type "int". This is what the Dafny implementation +// refers to as "target-language array-index type". However, the dimension lengths +// are given as "big.Int". + +type Array interface { + dimensionCount() int + dimensionLength(dim int) int + ArrayGet1(index int) interface{} + ArraySet1(value interface{}, index int) + arrayGetRange1(lo, hi Int) Array + arraySetRange1(index int, other Array) + 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) + ArrayGet1Char(index int) Char + ArraySet1Char(value Char, index int) + ArrayGet1CodePoint(index int) CodePoint + ArraySet1CodePoint(value CodePoint, index int) +} + +func defaultArrayEqualUpTo(left Array, right Array, index uint32) bool { + lSlice := left.anySlice(Zero, IntOfUint32(index)) + rSlice := right.anySlice(Zero, IntOfUint32(index)) + if len(lSlice) > 0 && IsEqualityComparable(lSlice[0]) { + return slices.Equal(lSlice, rSlice) + } + for i := uint32(0); i < index; i++ { + if !AreEqual(lSlice[i], rSlice[i]) { + return false + } + } + return true +} + +func defaultArraySetRange1(left Array, right Array, index int) { + rightLength := right.dimensionLength(0) + for j := 0; j < rightLength; j++ { + left.ArraySet1(right.ArrayGet1(j), int(index+j)) + } +} + +/***** newArray *****/ + +// Multiply the numbers in "dims" and return the product as an "int". +// If the product doesn't fit in an "int", panic with the message that the +// array-size limit has been exceeded. +// It is expected that len(dims) is at least 1 and that each number in +// dims is non-negative. +func computeTotalArrayLength(dims ...Int) int { + product := dims[0] + for i := 1; i < len(dims); i++ { + product = product.Times(dims[i]) + } + if IntOf(0x8000_0000).Cmp(product) <= 0 { + panic(fmt.Sprintf("array size exceeds memory limit: %v", String(product))) + } + totalLength := product.Int() + return totalLength +} + +func newArrayFromCharArray(values []Char) Array { + contents := make([]Char, len(values)) + copy(contents, values) + return &arrayForChar{ + contents: contents, + dims: []int{len(values)}, + } +} + +func newArrayFromByteArray(values []byte) Array { + contents := make([]byte, len(values)) + copy(contents, values) + return &arrayForByte{ + contents: contents, + dims: []int{len(values)}, + } +} + +// Uses the given array directly. +// Only safe if this array is not used anywhere else afterwards! +// Currently only used to support the existing publish SeqFromArray. +func unsafeWrapArray(values []interface{}) Array { + return &arrayStruct{ + contents: values, + dims: []int{len(values)}, + } +} + +// NewArrayFromExample returns a new Array. +// If "init" is non-nil, it is used to initialize all elements of the array. +// "example" is used only to figure out the right kind of Array to return. +// If "init" is non-nil, the types of "example" and "init" must agree. +// All numbers in "dims" are expected to be non-negative and "len(dims)" is +// expected to be at least 1 (this is not checked). The function checks that +// the product of the numbers in "dims" lies within the limit of what array +// lengths are supported; the code will panic if the limit is exceeded. +func NewArrayFromExample(example interface{}, init interface{}, dims ...Int) Array { + numberOfDimensions := len(dims) + intDims := make([]int, len(dims)) + totalLength := computeTotalArrayLength(dims...) + // If the previous line does not panic, then the .Int() conversions in + // the following loop will succeed. + for d := 0; d < numberOfDimensions; d++ { + intDims[d] = dims[d].Int() + } + + if totalLength == 0 { + return newZeroLengthArray(intDims) + } + + // Inspect the type of "example" to consider Array specialization + if _, ok := example.(byte); ok { + arr := make([]byte, totalLength) + if init != nil { + x := init.(byte) + for i := range arr { + arr[i] = x + } + } + return &arrayForByte{ + contents: arr, + dims: intDims, + } + } + if _, ok := example.(Char); ok { + arr := make([]Char, totalLength) + if init != nil { + x := init.(Char) + for i := range arr { + arr[i] = x + } + } + return &arrayForChar{ + contents: arr, + dims: intDims, + } + } + if _, ok := example.(CodePoint); ok { + arr := make([]CodePoint, totalLength) + if init != nil { + x := init.(CodePoint) + for i := range arr { + arr[i] = x + } + } + return &arrayForCodePoint{ + contents: arr, + dims: intDims, + } + } + + // Use the default representation + arr := make([]interface{}, totalLength) + if init != nil { + for i := range arr { + arr[i] = init + } + } + + return &arrayStruct{ + contents: arr, + dims: intDims, + } +} + +func newZeroLengthArray(intDims []int) Array { + // Use the default representation + return &arrayStruct{ + contents: nil, + dims: intDims, + } +} + +// newArrayWithValues returns a new one-dimensional Array with the given initial +// values. It is only used internally, by *Builder.ToArray(). +func newArrayWithValues(values ...interface{}) Array { + totalLength := len(values) + intDims := []int{totalLength} + if totalLength == 0 { + return newZeroLengthArray(intDims) + } + + // Inspect the type of "values[0]" to consider Array specialization + if _, ok := values[0].(byte); ok { + arr := make([]byte, totalLength) + for i := range arr { + arr[i] = values[i].(byte) + } + return &arrayForByte{ + contents: arr, + dims: intDims, + } + } + if _, ok := values[0].(Char); ok { + arr := make([]Char, totalLength) + for i := range arr { + arr[i] = values[i].(Char) + } + return &arrayForChar{ + contents: arr, + dims: intDims, + } + } + + // Use the default representation + arr := make([]interface{}, totalLength) + copy(arr, values) + return &arrayStruct{ + contents: arr, + dims: intDims, + } +} + +// 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. +func newArrayWithInitFn(init func(uint32) interface{}, length int) Array { + intDims := []int{length} + if length == 0 { + return newZeroLengthArray(intDims) + } + + // Inspect the type of the first initial value to consider Array specialization + value0 := init(0) + if _, ok := value0.(byte); ok { + arr := make([]byte, length) + arr[0] = value0.(byte) + for i := 1; i < length; i++ { + arr[i] = init(uint32(i)).(byte) + } + return &arrayForByte{ + contents: arr, + dims: intDims, + } + } + if _, ok := value0.(Char); ok { + arr := make([]Char, length) + arr[0] = value0.(Char) + for i := 1; i < length; i++ { + arr[i] = init(uint32(i)).(Char) + } + return &arrayForChar{ + contents: arr, + dims: intDims, + } + } + + // Use the default representation + arr := make([]interface{}, length) + arr[0] = value0 + for i := 1; i < length; i++ { + arr[i] = init(uint32(i)) + } + return &arrayStruct{ + contents: arr, + dims: intDims, + } +} + +// NewArrayWithValue returns a new Array full of the given initial value. +func NewArrayWithValue(init interface{}, dims ...Int) Array { + return NewArrayFromExample(init, init, dims...) +} + +// NewArray returns a new Array full of the default value of the given type. +func NewArray(dims ...Int) Array { + return NewArrayFromExample(nil, nil, dims...) +} + +/***** arrayStruct is default implementation of the Array interface. *****/ + +type arrayStruct struct { + contents []interface{} // stored as a flat one-dimensional slice + dims []int +} + +func (_this arrayStruct) dimensionCount() int { + return len(_this.dims) +} + +func (_this arrayStruct) dimensionLength(dim int) int { + return _this.dims[dim] +} + +func (_this arrayStruct) ArrayGet1(index int) interface{} { + return _this.contents[index] +} + +func (_this arrayStruct) ArraySet1(value interface{}, index int) { + _this.contents[index] = value +} + +func (_this arrayStruct) arrayGetRange1(lo, hi Int) Array { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + newContents := _this.contents[iLo:iHi] + return &arrayStruct{ + contents: newContents, + dims: []int{int(iHi - iLo)}, + } +} + +func (_this arrayStruct) arraySetRange1(index int, other Array) { + // Optimize for the same type of content array + if otherStruct, ok := other.(arrayStruct); ok { + copy(_this.contents[index:], otherStruct.contents) + } else { + defaultArraySetRange1(_this, other, index) + } +} + +func (_this arrayStruct) arrayCopy() Array { + newContents := make([]interface{}, len(_this.contents)) + copy(newContents, _this.contents) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) + return &arrayStruct{ + contents: newContents, + dims: newDims, + } +} + +func (_this arrayStruct) arrayEqualUpTo(other Array, index int) bool { + // Not much point in optimizing for the same type of content array + // since anySlice is cheap on arrayStructs. + 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{}") +} + +func (_this arrayStruct) ArraySet1Byte(value byte, index int) { + panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") +} + +func (_this arrayStruct) ArrayGet1Char(index int) Char { + panic("Expected specialized array type that contains characters, but found general-purpose array of interface{}") +} + +func (_this arrayStruct) ArraySet1Char(value Char, index int) { + panic("Expected specialized array type that contains characters, but found general-purpose array of interface{}") +} + +func (_this arrayStruct) ArrayGet1CodePoint(index int) CodePoint { + panic("Expected specialized array type that contains code points, but found general-purpose array of interface{}") +} + +func (_this arrayStruct) ArraySet1CodePoint(value CodePoint, index int) { + panic("Expected specialized array type that contains code points, but found general-purpose array of interface{}") +} + +func (_this arrayStruct) anySlice(lo, hi Int) []interface{} { + if lo.IsNilInt() && hi.IsNilInt() { + return _this.contents + } + if lo.IsNilInt() { + return _this.contents[:hi.Int()] + } + if hi.IsNilInt() { + return _this.contents[lo.Int():] + } + return _this.contents[lo.Int():hi.Int()] +} + +// arrayStruct implements the EqualsGeneric interface. +func (_this arrayStruct) EqualsGeneric(other interface{}) bool { + otherArray, ok := other.(*arrayStruct) + if !ok { + return false + } + // In the next line, we're sure to compare the references, not the addresses of the arrayStruct's. + return &_this.dims[0] == &otherArray.dims[0] +} + +/***** arrayForByte is the Array interface specialized for byte. *****/ + +type arrayForByte struct { + contents []byte // stored as a flat one-dimensional slice + dims []int +} + +func (_this arrayForByte) dimensionCount() int { + return len(_this.dims) +} + +func (_this arrayForByte) dimensionLength(dim int) int { + return _this.dims[dim] +} + +func (_this arrayForByte) ArrayGet1(index int) interface{} { + return _this.contents[index] +} + +func (_this arrayForByte) ArraySet1(value interface{}, index int) { + _this.contents[index] = value.(byte) +} + +func (_this arrayForByte) arrayGetRange1(lo, hi Int) Array { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + newContents := _this.contents[iLo:iHi] + return &arrayForByte{ + contents: newContents, + dims: []int{int(iHi - iLo)}, + } +} + +func (_this arrayForByte) arraySetRange1(index int, other Array) { + // Optimize for the same type of content array + if otherByte, ok := other.(arrayForByte); ok { + copy(_this.contents[index:], otherByte.contents) + } else { + defaultArraySetRange1(_this, other, index) + } +} + +func (_this arrayForByte) arrayCopy() Array { + newContents := make([]byte, len(_this.contents)) + copy(newContents, _this.contents) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) + return &arrayForByte{ + contents: newContents, + dims: newDims, + } +} + +func (_this arrayForByte) arrayEqualUpTo(other Array, index int) bool { + // Optimize for the same type of content array + if otherByte, ok := other.(arrayForByte); ok { + return slices.Equal(_this.contents[:index], otherByte.contents[:index]) + } else { + return defaultArrayEqualUpTo(_this, other, uint32(index)) + } +} + +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] +} + +func (_this arrayForByte) ArraySet1Byte(value byte, index int) { + _this.contents[index] = value +} + +func (_this arrayForByte) ArrayGet1Char(index int) Char { + panic("Expected specialized array type that contains characters, but found general-purpose array of interface{}") +} + +func (_this arrayForByte) ArraySet1Char(value Char, index int) { + panic("Expected specialized array type that contains characters, but found general-purpose array of interface{}") +} + +func (_this arrayForByte) ArrayGet1CodePoint(index int) CodePoint { + panic("Expected specialized array type that contains code points, but found general-purpose array of interface{}") +} + +func (_this arrayForByte) ArraySet1CodePoint(value CodePoint, index int) { + panic("Expected specialized array type that contains code points, but found general-purpose array of interface{}") +} + +func (_this arrayForByte) anySlice(lo, hi Int) []interface{} { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + anyArray := make([]interface{}, iHi-iLo) + for i := iLo; i < iHi; i++ { + anyArray[i] = _this.contents[i] + } + return anyArray +} + +// arrayForByte implements the EqualsGeneric interface. +func (_this arrayForByte) EqualsGeneric(other interface{}) bool { + otherArray, ok := other.(*arrayForByte) + if !ok { + return false + } + return &_this.dims[0] == &otherArray.dims[0] +} + +/***** arrayForChar is the Array interface specialized for Char. *****/ + +type arrayForChar struct { + contents []Char // stored as a flat one-dimensional slice + dims []int +} + +func (_this arrayForChar) dimensionCount() int { + return len(_this.dims) +} + +func (_this arrayForChar) dimensionLength(dim int) int { + return _this.dims[dim] +} + +func (_this arrayForChar) ArrayGet1(index int) interface{} { + return _this.contents[index] +} + +func (_this arrayForChar) ArraySet1(value interface{}, index int) { + _this.contents[index] = value.(Char) +} + +func (_this arrayForChar) arrayGetRange1(lo, hi Int) Array { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + newContents := _this.contents[iLo:iHi] + return &arrayForChar{ + contents: newContents, + dims: []int{int(iHi - iLo)}, + } +} + +func (_this arrayForChar) arraySetRange1(index int, other Array) { + // Optimize for the same type of content array + if otherByte, ok := other.(arrayForChar); ok { + copy(_this.contents[index:], otherByte.contents) + } else { + defaultArraySetRange1(_this, other, index) + } +} + +func (_this arrayForChar) arrayCopy() Array { + newContents := make([]Char, len(_this.contents)) + copy(newContents, _this.contents) + newDims := make([]int, len(_this.dims)) + copy(newDims, _this.dims) + return &arrayForChar{ + contents: newContents, + dims: newDims, + } +} + +func (_this arrayForChar) arrayEqualUpTo(other Array, index int) bool { + // Optimize for the same type of content array + if otherChar, ok := other.(arrayForChar); ok { + return slices.Equal(_this.contents[:index], otherChar.contents[:index]) + } else { + return defaultArrayEqualUpTo(_this, other, uint32(index)) + } +} + +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{}") +} + +func (_this arrayForChar) ArraySet1Byte(value byte, index int) { + panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") +} + +func (_this arrayForChar) ArrayGet1Char(index int) Char { + return _this.contents[index] +} + +func (_this arrayForChar) ArraySet1Char(value Char, index int) { + _this.contents[index] = value +} + +func (_this arrayForChar) ArrayGet1CodePoint(index int) CodePoint { + panic("Expected specialized array type that contains code points, but found general-purpose array of interface{}") +} + +func (_this arrayForChar) ArraySet1CodePoint(value CodePoint, index int) { + panic("Expected specialized array type that contains code points, but found general-purpose array of interface{}") +} + +func (_this arrayForChar) anySlice(lo, hi Int) []interface{} { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + anyArray := make([]interface{}, iHi-iLo) + for i := iLo; i < iHi; i++ { + anyArray[i] = _this.contents[i] + } + return anyArray +} + +// arrayForChar implements the EqualsGeneric interface. +func (_this arrayForChar) EqualsGeneric(other interface{}) bool { + otherArray, ok := other.(*arrayForChar) + if !ok { + return false + } + return &_this.dims[0] == &otherArray.dims[0] +} + +/***** arrayForCodePoint is the Array interface specialized for CodePoint. *****/ + +type arrayForCodePoint struct { + contents []CodePoint // stored as a flat one-dimensional slice + dims []int +} + +func (_this arrayForCodePoint) dimensionCount() int { + return len(_this.dims) +} + +func (_this arrayForCodePoint) dimensionLength(dim int) int { + return _this.dims[dim] +} + +func (_this arrayForCodePoint) ArrayGet1(index int) interface{} { + return _this.contents[index] +} + +func (_this arrayForCodePoint) ArraySet1(value interface{}, index int) { + _this.contents[index] = value.(CodePoint) +} + +func (_this arrayForCodePoint) arrayGetRange1(lo, hi Int) Array { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + newContents := _this.contents[iLo:iHi] + return &arrayForCodePoint{ + contents: newContents, + dims: []int{int(iHi - iLo)}, + } +} + +func (_this arrayForCodePoint) arraySetRange1(index int, other Array) { + // Optimize for the same type of content array + if otherCodePoint, ok := other.(arrayForCodePoint); ok { + copy(_this.contents[index:], otherCodePoint.contents) + } else { + defaultArraySetRange1(_this, other, index) + } +} + +func (_this arrayForCodePoint) arrayCopy() Array { + newContents := make([]CodePoint, len(_this.contents)) + copy(newContents, _this.contents) + return &arrayForCodePoint{ + contents: newContents, + // TODO: Does dims have to be copied as well? + dims: _this.dims, + } +} + +func (_this arrayForCodePoint) arrayEqualUpTo(other Array, index int) bool { + // Optimize for the same type of content array + if otherCodePoint, ok := other.(arrayForCodePoint); ok { + return slices.Equal(_this.contents[:index], otherCodePoint.contents[:index]) + } else { + return defaultArrayEqualUpTo(_this, other, uint32(index)) + } +} + +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{}") +} + +func (_this arrayForCodePoint) ArraySet1Byte(value byte, index int) { + panic("Expected specialized array type that contains bytes, but found general-purpose array of interface{}") +} + +func (_this arrayForCodePoint) ArrayGet1Char(index int) Char { + panic("Expected specialized array type that contains characters, but found general-purpose array of interface{}") +} + +func (_this arrayForCodePoint) ArraySet1Char(value Char, index int) { + panic("Expected specialized array type that contains characters, but found general-purpose array of interface{}") +} + +func (_this arrayForCodePoint) ArrayGet1CodePoint(index int) CodePoint { + return _this.contents[index] +} + +func (_this arrayForCodePoint) ArraySet1CodePoint(value CodePoint, index int) { + _this.contents[index] = value +} + +func (_this arrayForCodePoint) anySlice(lo, hi Int) []interface{} { + if lo.IsNilInt() { + lo = Zero + } + if hi.IsNilInt() { + hi = IntOf(len(_this.contents)) + } + iLo := lo.Int() + iHi := hi.Int() + anyArray := make([]interface{}, iHi-iLo) + for i := iLo; i < iHi; i++ { + anyArray[i] = _this.contents[i] + } + return anyArray +} + +// arrayForCodePoint implements the EqualsGeneric interface. +func (_this arrayForCodePoint) EqualsGeneric(other interface{}) bool { + otherArray, ok := other.(*arrayForCodePoint) + if !ok { + return false + } + return &_this.dims[0] == &otherArray.dims[0] +} + +/***** other Array methods *****/ + +// EmptyArray is an empty one-dimensional array. +var EmptyArray = NewArray(Zero) + +func ArrayCastTo(x interface{}) Array { + var t Array + t, _ = x.(Array) + return t +} + +// ArrayLen returns the length of the array in the given dimension. +func ArrayLen(array Array, dim int) Int { + return IntOf(ArrayLenInt(array, dim)) +} + +// ArrayLenInt returns the length of the array in the given dimension, as an int. +func ArrayLenInt(array Array, dim int) int { + return array.dimensionLength(dim) +} + +func computeArrayIndex(array Array, ixs ...int) int { + dimensionCount := array.dimensionCount() + if len(ixs) != dimensionCount { + panic(fmt.Sprintf("Expected %d indices but got %d", dimensionCount, len(ixs))) + } + i := 0 + size := 1 + for d := dimensionCount - 1; d >= 0; d-- { + i += size * ixs[d] + size *= array.dimensionLength(d) + } + return i +} + +func ArrayGet(array Array, ixs ...int) interface{} { + index := computeArrayIndex(array, ixs...) + return array.ArrayGet1(index) +} + +func ArraySet(array Array, value interface{}, ixs ...int) { + index := computeArrayIndex(array, ixs...) + array.ArraySet1(value, index) +} + +// RangeToSeq converts the selected portion of the array to a sequence. +func ArrayRangeToSeq(array Array, lo, hi Int) Sequence { + if array.dimensionCount() != 1 { + panic("Can't take a slice of a multidimensional array") + } + isString := false + if array.dimensionLength(0) > 0 { + _, isString = array.ArrayGet1(0).(Char) + } + + seq := New_ArraySequence_() + underlying := array.arrayGetRange1(lo, hi).arrayCopy() + seq.Ctor__(GoNativeArray{underlying: underlying}, false) + seq.IsString_set_(isString) + return seq +} + +/****************************************************************************** + * Tuples + ******************************************************************************/ + +// A Tuple is a one-dimensional heterogeneous array. +type Tuple struct { + contents []interface{} +} + +// TupleOf creates a tuple with the given values. +func TupleOf(values ...interface{}) Tuple { + arr := make([]interface{}, len(values)) + copy(arr, values) + return Tuple{arr} +} + +// Equals returns whether two tuples have the same values. +func (tuple Tuple) Equals(other Tuple) bool { + return sliceEquals(tuple.contents, other.contents) +} + +// Tuple implements the EqualsGeneric interface. +func (tuple Tuple) EqualsGeneric(other interface{}) bool { + tuple2, ok := other.(Tuple) + return ok && tuple.Equals(tuple2) +} + +func (tuple Tuple) String() string { + return "(" + stringOfElements(tuple.contents) + ")" +} + +// Index looks up the address of the ith element of the tuple. +func (tuple Tuple) Index(i Int) *interface{} { + return tuple.IndexInt(i.Int()) +} + +// IndexInt looks up the address of the ith element of the tuple. +func (tuple Tuple) IndexInt(i int) *interface{} { + return &tuple.contents[i] +} + +// TupleType returns the type of a tuple with given element types. +func TupleType(tys ...TypeDescriptor) TypeDescriptor { + arr := make([]TypeDescriptor, len(tys)) + copy(arr, tys) + return tupleType{arr} +} + +type tupleType struct { + eltTys []TypeDescriptor +} + +func (tt tupleType) Default() interface{} { + values := make([]interface{}, len(tt.eltTys)) + for i, ty := range tt.eltTys { + values[i] = ty.Default() + } + return TupleOf(values...) +} + +func (tt tupleType) String() string { + s := "(" + sep := "" + for _, ty := range tt.eltTys { + s += sep + String(ty) + sep = ", " + } + s += ")" + return s +} + +/****************************************************************************** + * Collection building + ******************************************************************************/ + +// A Builder holds values as they're imperatively accumulated in order to build +// an Array, Set, or MultiSet. +type Builder []interface{} + +// NewBuilder creates a new Builder. +func NewBuilder() *Builder { + return new(Builder) +} + +// NewBuilder creates a new Builder. +func NewBuilderOf(iter interface{}) *Builder { + b := NewBuilder() + for i := Iterate(iter); ; { + v, ok := i() + if !ok { + break + } + b.Add(v) + } + return b +} + +// Add adds a new value to a Builder. +func (builder *Builder) Add(value interface{}) { + *builder = append(*builder, value) +} + +// ToArray creates an Array with the accumulated values. +func (builder *Builder) ToArray() Array { + return newArrayWithValues(*builder...) +} + +// ToSet creates a Set with the accumulated values. +func (builder *Builder) ToSet() Set { + return SetOf(*builder...) +} + +// ToMultiset creates a MultiSet with the accumulated values. +func (builder *Builder) ToMultiSet() MultiSet { + return MultiSetOf(*builder...) +} + +// Iterator iterates over the accumulated values. +func (builder *Builder) Iterator() Iterator { + return sliceIterator(*builder) +} + +/****************************************************************************** + * Sets + ******************************************************************************/ + +// A Set is a sequence without duplicates. +type Set struct { + contents []interface{} +} + +// EmptySet is the empty set. +var EmptySet = SetOf() + +// SetOf creates a set with the given values. +func SetOf(values ...interface{}) Set { + uniq := make([]interface{}, 0, len(values)) +NEXT_INPUT: + for _, v := range values { + for _, u := range uniq { + if AreEqual(u, v) { + continue NEXT_INPUT + } + } + uniq = append(uniq, v) + } + return Set{uniq} +} + +// Cardinality returns the cardinality (size) of the set. +func (set Set) Cardinality() Int { + return IntOf(set.CardinalityInt()) +} + +// CardinalityInt returns the cardinality (size) of the set as an int. +func (set Set) CardinalityInt() int { + return len(set.contents) +} + +// Contains returns whether the given value is an element of the set. +func (set Set) Contains(value interface{}) bool { + return sliceContains(set.contents, value) +} + +// Iterator returns an iterator over the elements of the set. +func (set Set) Iterator() Iterator { + return sliceIterator(set.contents) +} + +// Union makes a set containing each element contained by either input set. +func (set Set) Union(set2 Set) Set { + if set.CardinalityInt() == 0 { + return set2 + } + if set2.CardinalityInt() == 0 { + return set + } + + n := set.CardinalityInt() + uniq := make([]interface{}, n) + copy(uniq, set.contents) +NEXT_INPUT: + for _, v := range set2.contents { + for _, u := range uniq { + if AreEqual(u, v) { + continue NEXT_INPUT + } + } + uniq = append(uniq, v) + } + + return Set{uniq} +} + +// Intersection makes a set containing each element contained by both input +// sets. +func (set Set) Intersection(set2 Set) Set { + if set.CardinalityInt() == 0 || set2.CardinalityInt() == 0 { + return EmptySet + } + + uniq := make([]interface{}, 0) + for _, v := range set.contents { + if set2.Contains(v) { + uniq = append(uniq, v) + } + } + + return Set{uniq} +} + +// Difference makes a set containing each element contained by set but not +// by set2. +func (set Set) Difference(set2 Set) Set { + if set.CardinalityInt() == 0 || set2.CardinalityInt() == 0 { + return set + } + + elts := make([]interface{}, 0, max(0, set.CardinalityInt()-set2.CardinalityInt())) + for _, v := range set.contents { + if !set2.Contains(v) { + elts = append(elts, v) + } + } + + return Set{elts} +} + +// IsDisjointFrom returns true if the sets have no elements in common. +func (set Set) IsDisjointFrom(set2 Set) bool { + if set.CardinalityInt() == 0 || set2.CardinalityInt() == 0 { + return true + } + + for _, v := range set.contents { + if sliceContains(set2.contents, v) { + return false + } + } + + return true +} + +// Equals tests whether the sets contain the same elements. +func (set Set) Equals(set2 Set) bool { + return set.CardinalityInt() == set2.CardinalityInt() && + set.isSubsetAfterCardinalityCheck(set2) +} + +// Set implements the EqualsGeneric interface. +func (set Set) EqualsGeneric(other interface{}) bool { + set2, ok := other.(Set) + return ok && set.Equals(set2) +} + +// IsSubsetOf returns true if each element in this set is also in the other. +func (set Set) IsSubsetOf(set2 Set) bool { + return set.CardinalityInt() <= set2.CardinalityInt() && + set.isSubsetAfterCardinalityCheck(set2) +} + +// IsProperSubsetOf returns true if each element in this set is also in the +// other, and moreover the sets aren't equal. +func (set Set) IsProperSubsetOf(set2 Set) bool { + return set.CardinalityInt() < set2.CardinalityInt() && + set.isSubsetAfterCardinalityCheck(set2) +} + +func (set Set) isSubsetAfterCardinalityCheck(set2 Set) bool { + for _, v := range set.contents { + if !sliceContains(set2.contents, v) { + return false + } + } + return true +} + +// Elements returns the set of elements (i.e. the set itself). +func (set Set) Elements() Set { + return set +} + +// AllSubsets returns an iterator over all subsets of the given set. +func (set Set) AllSubsets() Iterator { + // Use a big integer to range from 0 to 2^n + r := new(big.Int) + limit := new(big.Int).Lsh(One.impl, uint(set.CardinalityInt())) + return func() (interface{}, bool) { + if r.Cmp(limit) == 0 { + return Set{}, false + } else { + values := make([]interface{}, 0, len(set.contents)) + i := 0 + s := new(big.Int).Set(r) + mod := new(big.Int) + for s.Cmp(Zero.impl) > 0 { + if mod.Mod(s, Two.impl).Cmp(Zero.impl) != 0 { + values = append(values, set.contents[i]) + } + s.Div(s, Two.impl) + i++ + } + r.Add(r, One.impl) + + // Annoyingly, the other implementations reverse the order of the + // elements, so we have to as well + return Set{reverse(values)}, true + } + } +} + +func reverse(values []interface{}) []interface{} { + ans := make([]interface{}, len(values)) + n := len(values) + for i, v := range values { + ans[n-1-i] = v + } + return ans +} + +func (set Set) String() string { + return "{" + stringOfElements(set.contents) + "}" +} + +/****************************************************************************** + * Multisets + ******************************************************************************/ + +// A MultiSet is an unordered sequence of elements with possible duplication. +type MultiSet struct { + elts []msetElt +} + +type msetElt struct { + value interface{} + count Int +} + +// EmptyMultiSet is the empty multiset. +var EmptyMultiSet = MultiSetOf() + +// MultiSetOf creates a MultiSet with the given elements. +func MultiSetOf(values ...interface{}) MultiSet { + elts := make([]msetElt, 0, len(values)) +NEXT_INPUT: + for _, v := range values { + for i, u := range elts { + if AreEqual(u.value, v) { + elts[i] = msetElt{value: u.value, count: u.count.Plus(One)} + continue NEXT_INPUT + } + } + elts = append(elts, msetElt{value: v, count: One}) + } + return MultiSet{elts} +} + +// MultiSetFromSeq creates a MultiSet from the elements in the given sequence. +func MultiSetFromSeq(seq Sequence) MultiSet { + return NewBuilderOf(seq).ToMultiSet() +} + +// MultiSetFromSet creates a MultiSet from the elements in the given set. +func MultiSetFromSet(set Set) MultiSet { + elts := make([]msetElt, len(set.contents)) + for i, v := range set.contents { + // No need to check whether it's already there because Set elements are + // assumed to be unique + elts[i] = msetElt{v, One} + } + return MultiSet{elts} +} + +func (mset MultiSet) clone() MultiSet { + elts := make([]msetElt, len(mset.elts)) + copy(elts, mset.elts) + return MultiSet{elts} +} + +func (mset MultiSet) findIndex(value interface{}) (int, bool) { + for i, e := range mset.elts { + if AreEqual(e.value, value) { + return i, true + } + } + return -1, false +} + +// Update changes the cardinality of the given value in the multiset, returning +// a new multiset unless the cardinality did not actually change. +func (mset MultiSet) Update(value interface{}, n Int) MultiSet { + i, found := mset.findIndex(value) + if found { + if mset.elts[i].count == n { + return mset + } else { + ans := mset.clone() + ans.elts[i] = msetElt{value, n} + return ans + } + } else if n.Cmp(Zero) == 0 { + return mset + } else { + return MultiSet{append(mset.clone().elts, msetElt{value, n})} + } +} + +// Cardinality returns the number of elements in the multiset (counting +// repetitions). +func (mset MultiSet) Cardinality() Int { + n := new(big.Int) + for _, e := range mset.elts { + n.Add(n, e.count.impl) + } + return intOf(n) +} + +// CardinalityInt returns the number of elements in the multiset (counting +// repetitions) as an int. +func (mset MultiSet) CardinalityInt() int { + n := 0 + for _, e := range mset.elts { + n += e.count.Int() + } + return n +} + +// Index returns the ith element of the multiset, which is arbitrary except that +// it is different from the jth element when i /= j. (Repetitions are ignored.) +func (mset MultiSet) Index(i Int) interface{} { + return mset.elts[i.Int()] +} + +// Iterator returns an iterator over the multiset (including repetitions). +func (mset MultiSet) Iterator() Iterator { + i := 0 + n := new(big.Int) + return func() (interface{}, bool) { + for { + if i >= len(mset.elts) { + return nil, false + } + if n.Cmp(mset.elts[i].count.impl) >= 0 { + n.SetInt64(0) + i++ + } else { + break + } + } + + ans := mset.elts[i].value + n.Add(n, One.impl) + return ans, true + } +} + +// Contains returns whether the multiset contains the given element (at least +// once). +func (mset MultiSet) Contains(value interface{}) bool { + return mset.Multiplicity(value).Cmp(Zero) > 0 +} + +// Multiplicity returns the number of times a given element occurs in the +// multiset. +func (mset MultiSet) Multiplicity(value interface{}) Int { + i, found := mset.findIndex(value) + if found { + return mset.elts[i].count + } else { + return Zero + } +} + +// Elements returns an iterator that yields each element in the multiset, as +// many times as it appears. +func (mset MultiSet) Elements() func() (interface{}, bool) { + i := 0 + n := new(big.Int) + return func() (interface{}, bool) { + for { + if i >= len(mset.elts) { + return nil, false + } + if n.Cmp(mset.elts[i].count.impl) == 0 { + i++ + n.SetInt64(0) + } else { + break + } + } + n.Add(n, One.impl) + return mset.elts[i].value, true + } +} + +// UniqueElements returns an iterator that yields each element in the multiset +// once. +func (mset MultiSet) UniqueElements() func() (interface{}, bool) { + i := 0 + return func() (interface{}, bool) { + if i >= len(mset.elts) { + return nil, false + } else { + i++ + return mset.elts[i-1].value, true + } + } +} + +// Union returns a multiset including each element of either set. Each value's +// multiplicity will be the sum of its multiplicities in the original multisets. +func (mset MultiSet) Union(mset2 MultiSet) MultiSet { + if len(mset.elts) == 0 { + return mset2 + } + if len(mset2.elts) == 0 { + return mset + } + + elts := make([]msetElt, 0, len(mset.elts)+len(mset2.elts)) + for _, e := range mset.elts { + if e.count.Cmp(Zero) == 0 { + // e.value in mset2 will be added in the next separate for loop + continue + } + m := mset2.Multiplicity(e.value) + elts = append(elts, msetElt{e.value, e.count.Plus(m)}) + } + for _, e := range mset2.elts { + if !mset.Contains(e.value) { + elts = append(elts, e) + } + } + + return MultiSet{elts} +} + +// Intersection returns a multiset including those elements which occur in both +// sets. Each value's multiplicity will be the minimum of its multiplicities +// in the original multisets. +func (mset MultiSet) Intersection(mset2 MultiSet) MultiSet { + if len(mset.elts) == 0 || len(mset2.elts) == 0 { + return EmptyMultiSet + } + + elts := make([]msetElt, 0) + for _, e := range mset.elts { + m := mset2.Multiplicity(e.value) + if m.Cmp(Zero) != 0 { + elts = append(elts, msetElt{e.value, e.count.Min(m)}) + } + } + + return MultiSet{elts} +} + +// Difference returns a multiset including those elements which occur in the +// first argument but not the second. Each value's multiplicity will be its +// multiplicity in mset minus its multiplicity in mset2. +func (mset MultiSet) Difference(mset2 MultiSet) MultiSet { + if len(mset.elts) == 0 || len(mset2.elts) == 0 { + return mset + } + + elts := make([]msetElt, 0, max(0, len(mset.elts)-len(mset2.elts))) + for _, e := range mset.elts { + d := e.count.Minus(mset2.Multiplicity(e.value)) + if d.Cmp(Zero) > 0 { + elts = append(elts, msetElt{e.value, d}) + } + } + + return MultiSet{elts} +} + +// IsDisjointFrom returns whether two multisets contain no elements in common. +func (mset MultiSet) IsDisjointFrom(mset2 MultiSet) bool { + if len(mset.elts) == 0 || len(mset2.elts) == 0 { + return true + } + + for _, e := range mset.elts { + if (e.count.Cmp(Zero) != 0) && mset2.Contains(e.value) { + return false + } + } + + return true +} + +// Equals returns whether two multisets have the same values with the same +// multiplicities. +func (mset MultiSet) Equals(mset2 MultiSet) bool { + for _, e := range mset.elts { + m := mset2.Multiplicity(e.value) + if e.count.Cmp(m) != 0 { + return false + } + } + return mset.CardinalityInt() == mset2.CardinalityInt() +} + +// MultiSet implements the EqualsGeneric interface. +func (mset MultiSet) EqualsGeneric(other interface{}) bool { + mset2, ok := other.(MultiSet) + return ok && mset.Equals(mset2) +} + +// IsSubsetOf returns whether one multiset has a subset of the elements of the +// other, with lesser or equal multiplicities. +func (mset MultiSet) IsSubsetOf(mset2 MultiSet) bool { + for _, e := range mset.elts { + m := mset2.Multiplicity(e.value) + if e.count.Cmp(m) > 0 { + return false + } + } + return true +} + +// IsProperSubsetOf returns whether one multiset has a proper subset of the +// elements of the other, with strictly lesser multiplicities. +func (mset MultiSet) IsProperSubsetOf(mset2 MultiSet) bool { + return mset.IsSubsetOf(mset2) && mset.CardinalityInt() < mset2.CardinalityInt() +} + +func (mset MultiSet) String() string { + s := "multiset{" + sep := "" + i := new(big.Int) + for _, e := range mset.elts { + for i.SetInt64(0); i.Cmp(e.count.impl) < 0; i.Add(i, One.impl) { + s += sep + String(e.value) + sep = ", " + } + } + s += "}" + return s +} + +/****************************************************************************** + * Maps + ******************************************************************************/ + +// A Map is an association between keys and values. +type Map struct { + elts []mapElt +} + +type mapElt struct { + key, value interface{} +} + +// A MapBuilder creates a new Map by accumulating elements imperatively. +type MapBuilder []mapElt + +// NewMapBuilder creates a new map builder. +func NewMapBuilder() *MapBuilder { + return new(MapBuilder) +} + +// Add adds a key and value to the map being built, used by map comprehension +func (mb *MapBuilder) Add(k, v interface{}) *MapBuilder { + *mb = append(*mb, mapElt{k, v}) + return mb +} + +// ToMap gets the map out of the map builder. +func (mb *MapBuilder) ToMap() Map { + return Map{*mb} +} + +// EmptyMap is the empty map. +var EmptyMap = NewMapBuilder().ToMap() + +func (m Map) clone() Map { + elts := make([]mapElt, len(m.elts)) + copy(elts, m.elts) + return Map{elts} +} + +func (m Map) findIndex(key interface{}) (int, bool) { + for i, e := range m.elts { + if AreEqual(e.key, key) { + return i, true + } + } + return -1, false +} + +// Cardinality finds the number of elements in the map. +func (m Map) Cardinality() Int { + return IntOf(m.CardinalityInt()) +} + +// CardinalityInt finds the number of elements in the map as an int. +func (m Map) CardinalityInt() int { + return len(m.elts) +} + +// Find finds the given key in the map, returning it and a success flag. +func (m Map) Find(key interface{}) (interface{}, bool) { + i, found := m.findIndex(key) + if found { + return m.elts[i].value, true + } else { + return nil, false + } +} + +// Get finds the given key in the map, returning it or nil. +func (m Map) Get(key interface{}) interface{} { + v, _ := m.Find(key) + return v +} + +// Contains returns whether the given key is in the map. +func (m Map) Contains(key interface{}) bool { + _, found := m.findIndex(key) + return found +} + +// Update returns a new Map which associates the given key and value. +func (m Map) Update(key, value interface{}) Map { + ans := m.clone() + i, found := ans.findIndex(key) + if found { + ans.elts[i] = mapElt{key, value} + } else { + ans.elts = append(ans.elts, mapElt{key, value}) + } + return ans +} + +// Similar to Update, but make the modification in-place. +// Meant to be used in the map constructor. +func (m Map) UpdateUnsafe(key, value interface{}) Map { + ans := m + i, found := ans.findIndex(key) + if found { + ans.elts[i] = mapElt{key, value} + } else { + ans.elts = append(ans.elts, mapElt{key, value}) + } + return ans +} + +func (a Map) Merge(b Map) Map { + if a.CardinalityInt() == 0 { + return b + } + if b.CardinalityInt() == 0 { + return a + } + + m := make([]mapElt, len(b.elts), len(a.elts)+len(b.elts)) + copy(m, b.elts) + for _, e := range a.elts { + _, found := b.findIndex(e.key) + if !found { + m = append(m, e) + } + } + return Map{m} +} + +func (a Map) Subtract(keys Set) Map { + if a.CardinalityInt() == 0 || keys.CardinalityInt() == 0 { + return a + } + + mb := NewMapBuilder() + for _, e := range a.elts { + if !keys.Contains(e.key) { + *mb = append(*mb, e) + } + } + return mb.ToMap() +} + +// Equals returns whether each map associates the same keys to the same values. +func (m Map) Equals(m2 Map) bool { + if len(m.elts) != len(m2.elts) { + return false + } + for _, e := range m.elts { + i, found := m2.findIndex(e.key) + if !found || !AreEqual(e.value, m2.elts[i].value) { + return false + } + } + return true +} + +// Map implements the EqualsGeneric interface. +func (m Map) EqualsGeneric(other interface{}) bool { + m2, ok := other.(Map) + return ok && m.Equals(m2) +} + +// Keys returns the set of keys in the map. +func (m Map) Keys() Set { + b := NewBuilder() + for _, e := range m.elts { + b.Add(e.key) + } + return b.ToSet() +} + +// Values returns the set of values in the map. +func (m Map) Values() Set { + b := NewBuilder() + for _, e := range m.elts { + b.Add(e.value) + } + return b.ToSet() +} + +// Items returns the set of items in the map as a Set of Tuples. +func (m Map) Items() Set { + b := NewBuilder() + for _, e := range m.elts { + b.Add(TupleOf(e.key, e.value)) + } + return b.ToSet() +} + +func (m Map) String() string { + s := "map[" + for i, e := range m.elts { + if i > 0 { + s += ", " + } + s += fmt.Sprintf("%s := %s", String(e.key), String(e.value)) + } + s += "]" + return s +} + +/****************************************************************************** + * Integers + ******************************************************************************/ + +// An Int is an immutable big integer. +type Int struct { + impl *big.Int + // debug string +} // Careful not to mutate! + +// A BV is an immutable big bitvector (presumed to be non-negative). +type BV = Int + +func intOf(i *big.Int) Int { + return Int{ + impl: i, + // debug: i.String(), + } +} + +// IntOf turns the given int into an Int. Common values are cached. This is +// simply a shorter form of IntOfInt. +func IntOf(i int) Int { + return IntOfInt(i) +} + +// IntOfInt turns the given int into an Int. Common values are cached. +func IntOfInt(i int) Int { + return IntOfInt64(int64(i)) +} + +// IntOfInt8 turns the given int8 into an Int. Common values are cached. +func IntOfInt8(i int8) Int { + return IntOfInt64(int64(i)) +} + +// IntOfInt16 turns the given int16 into an Int. Common values are cached. +func IntOfInt16(i int16) Int { + return IntOfInt64(int64(i)) +} + +// IntOfInt32 turns the given int32 into an Int. Common values are cached. +func IntOfInt32(i int32) Int { + return IntOfInt64(int64(i)) +} + +// IntOfInt64 turns the given int64 into an Int. Common values are cached. +func IntOfInt64(i int64) Int { + switch i { + case -1: + return NegativeOne + case 0: + return Zero + case 1: + return One + case 2: + return Two + case 5: + return Five + case 10: + return Ten + default: + return intOf(big.NewInt(i)) + } +} + +// IntOfUint turns the given uint into an Int. Common values are cached. +func IntOfUint(i uint) Int { + return IntOfUint64(uint64(i)) +} + +// IntOfUint8 turns the given uint8 into an Int. Common values are cached. +func IntOfUint8(i uint8) Int { + return IntOfUint64(uint64(i)) +} + +// IntOfUint16 turns the given uint16 into an Int. Common values are cached. +func IntOfUint16(i uint16) Int { + return IntOfUint64(uint64(i)) +} + +// IntOfUint32 turns the given uint32 into an Int. Common values are cached. +func IntOfUint32(i uint32) Int { + return IntOfUint64(uint64(i)) +} + +// IntOfUint64 turns the given uint64 into an Int. Common values are cached. +func IntOfUint64(i uint64) Int { + switch i { + case 0: + return Zero + case 1: + return One + case 2: + return Two + case 5: + return Five + case 10: + return Ten + default: + return intOf(new(big.Int).SetUint64(i)) + } +} + +// IntOfString parses the given string as an Int, panicking on failure. +func IntOfString(s string) Int { + switch s { + case "-1": + return NegativeOne + case "0": + return Zero + case "1": + return One + case "2": + return Two + case "5": + return Five + case "10": + return Ten + default: + i, ok := new(big.Int).SetString(s, 0) + if !ok { + panic("Unable to parse string as int: " + s) + } else { + return intOf(i) + } + } +} + +// IntOfAny converts from many different things to Int. Note that +// switch-on-type does a linear search, so this can be slow for less common +// cases. +func IntOfAny(x interface{}) Int { + switch x := x.(type) { + // Try and put the most common cases earliest. + case Int: + return x + case int: + return IntOfInt(x) + case string: + return IntOfString(x) + case uint: + return IntOfUint(x) + case Char: + return IntOfInt32(rune(x)) + case int32: + return IntOfInt32(x) + case int64: + return IntOfInt64(x) + case uint32: + return IntOfUint32(x) + case uint64: + return IntOfUint64(x) + case int8: + return IntOfInt8(x) + case uint8: + return IntOfUint8(x) + case int16: + return IntOfInt16(x) + case uint16: + return IntOfUint16(x) + default: + panic(fmt.Errorf("unexpected type for IntToAny: %v", refl.TypeOf(x))) + } +} + +// Int converts back into an int. If the result is not within int range, +// the value is undefined. +func (i Int) Int() int { + return int(i.impl.Int64()) +} + +// Int8 converts back into an int8. If the result is not within int8 range, +// the value is undefined. +func (i Int) Int8() int8 { + return int8(i.impl.Int64()) +} + +// Int16 converts back into an int16. If the result is not within int16 range, +// the value is undefined. +func (i Int) Int16() int16 { + return int16(i.impl.Int64()) +} + +// Int32 converts back into an int32. If the result is not within int32 range, +// the value is undefined. +func (i Int) Int32() int32 { + return int32(i.impl.Int64()) +} + +// Int64 converts back to an int64. If the result is not within int64 range, +// the value is undefined. +func (i Int) Int64() int64 { + return i.impl.Int64() +} + +// Uint converts back to a uint. If the result is not within uint range, the +// value is undefined. +func (i Int) Uint() uint { + return uint(i.impl.Uint64()) +} + +// Uint8 converts back to a uint8. If the result is not within uint8 range, the +// value is undefined. +func (i Int) Uint8() uint8 { + return uint8(i.impl.Uint64()) +} + +// Uint16 converts back to a uint16. If the result is not within uint16 range, +// the value is undefined. +func (i Int) Uint16() uint16 { + return uint16(i.impl.Uint64()) +} + +// Uint32 converts back to a uint32. If the result is not within uint32 range, +// the value is undefined. +func (i Int) Uint32() uint32 { + return uint32(i.impl.Uint64()) +} + +// Uint64 converts back to a uint64. If the result is not within uint64 range, +// the value is undefined. +func (i Int) Uint64() uint64 { + return i.impl.Uint64() +} + +func (i Int) String() string { + return i.impl.String() +} + +// NegativeOne is the constant -1. +var NegativeOne = intOf(big.NewInt(-1)) + +// Zero is the constant 0. +var Zero = intOf(big.NewInt(0)) + +// One is the constant 1. +var One = intOf(big.NewInt(1)) + +// Two is the constant 2. +var Two = intOf(big.NewInt(2)) + +// Five is the constant 5. +var Five = intOf(big.NewInt(5)) + +// Ten is the constant 10. +var Ten = intOf(big.NewInt(10)) + +// NilInt is a missing int value. +var NilInt = intOf(nil) + +// IsNilInt returns whether this Int is actually a missing value. +func (i Int) IsNilInt() bool { + return i.impl == nil +} + +func (i Int) binOp(j Int, f func(*big.Int, *big.Int, *big.Int) *big.Int) Int { + return intOf(f(new(big.Int), i.impl, j.impl)) +} + +// Plus adds two Ints. +func (i Int) Plus(j Int) Int { + return i.binOp(j, (*big.Int).Add) +} + +// Minus subtracts one Int from another. +func (i Int) Minus(j Int) Int { + return i.binOp(j, (*big.Int).Sub) +} + +// Times multiplies two Ints. +func (i Int) Times(j Int) Int { + return i.binOp(j, (*big.Int).Mul) +} + +// DivBy divides one Int by another. (So named to distinguish from +// big.Int.Div(), which is an in-place operation.) +func (i Int) DivBy(j Int) Int { + return i.binOp(j, (*big.Int).Div) +} + +// Modulo takes the remainder when dividing one Int by another. (So named to +// distinguish from big.Int.Mod(), which performs the operation in place.) +func (i Int) Modulo(j Int) Int { + return i.binOp(j, (*big.Int).Mod) +} + +// Negated negates an Int. +func (i Int) Negated() Int { + return intOf(new(big.Int).Neg(i.impl)) +} + +// Lsh performs a left shift. +func (i Int) Lsh(j Int) Int { + return intOf(new(big.Int).Lsh(i.impl, uint(j.Uint64()))) +} + +// Rsh performs a right shift. +func (i Int) Rsh(j Int) Int { + return intOf(new(big.Int).Rsh(i.impl, uint(j.Uint64()))) +} + +// Lrot performs a left rotate on a BV with width w. +func (i BV) Lrot(j Int, w uint) BV { + // (i <<< j) == ((i << j) % 2^w) | (i >> (w-j)) + + ju := uint(j.Uint64()) + l := new(big.Int).Lsh(i.impl, ju) + modulus := new(big.Int).Lsh(One.impl, w) + l.Mod(l, modulus) + r := modulus.Rsh(i.impl, w-ju) // reuse memory from modulus + return intOf(l.Or(l, r)) +} + +// Rrot performs a right rotate on a BV with width w. +func (i BV) Rrot(j BV, w uint) BV { + // (i >>> j) == ((i << (w-j)) % 2^w) | (i >> j) + + ju := uint(j.Uint64()) + l := new(big.Int).Lsh(i.impl, w-ju) + modulus := new(big.Int).Lsh(One.impl, w) + l.Mod(l, modulus) + r := modulus.Rsh(i.impl, ju) // reuse memory from modulus + return intOf(l.Or(l, r)) +} + +// Cmp compares two Ints, returning -1 for less, 0 for equal, or 1 for greater. +func (i Int) Cmp(j Int) int { + return i.impl.Cmp(j.impl) +} + +// Sign returns the sign of an Int, returning -1 for negative, 0 for zero, or +// 1 for positive. +func (i Int) Sign() int { + return i.impl.Sign() +} + +// EqualsGeneric compares an int to another value. +func (i Int) EqualsGeneric(other interface{}) bool { + j, ok := other.(Int) + return ok && i.Cmp(j) == 0 +} + +// Min returns the minimum of two integers. +func (i Int) Min(j Int) Int { + if i.Cmp(j) <= 0 { + return i + } else { + return j + } +} + +// Max returns the maximum of two integers. +func (i Int) Max(j Int) Int { + if i.Cmp(j) >= 0 { + return i + } else { + return j + } +} + +// And performs bitwise AND. +func (i Int) And(j Int) Int { + return i.binOp(j, (*big.Int).And) +} + +// Or performs bitwise OR. +func (i Int) Or(j Int) Int { + return i.binOp(j, (*big.Int).Or) +} + +// Xor performs bitwise XOR. +func (i Int) Xor(j Int) Int { + return i.binOp(j, (*big.Int).Xor) +} + +// Not performs bitwise NOT. +func (i Int) Not() Int { + return intOf(new(big.Int).Not(i.impl)) +} + +func (i Int) isPowerOf10() (bool, int) { + if i.Cmp(Zero) != 1 { + return false, -1 + } + n := 0 + j := i + for { + if j.Cmp(One) == 0 { + return true, n + } else if j.Modulo(Ten).Cmp(Zero) != 0 { + return false, -1 + } else { + j = j.DivBy(Ten) + n++ + } + } +} + +func (i Int) dividesAPowerOf10() (yes bool, factor Int, log10 int) { + if i.Cmp(Zero) != 1 { + return false, Zero, -1 + // okay, so technically you could multiply by a + // negative number, but that's not useful to + // Real.String(). + } + n := 0 + j := i + fact := One + for { + if j.Cmp(One) == 0 { + return true, One, n + } else if j.Modulo(Ten).Cmp(Zero) != 0 { + if j.Modulo(Five).Cmp(Zero) == 0 { + for { + fact = fact.Times(Two) + j = j.DivBy(Five) + n++ + if j.Cmp(One) == 0 { + return true, fact, n + } else if j.Modulo(Five).Cmp(Zero) != 0 { + return false, NegativeOne, -1 + } + } + } else if j.Modulo(Two).Cmp(Zero) == 0 { + for { + fact = fact.Times(Five) + j = j.DivBy(Two) + n++ + if j.Cmp(One) == 0 { + return true, fact, n + } else if j.Modulo(Two).Cmp(Zero) != 0 { + return false, NegativeOne, -1 + } + } + } else { + return false, NegativeOne, -1 + } + } else { + j = j.DivBy(Ten) + n++ + } + } +} + +// IntegerRange returns an iterator over the integers from lo up to (but not +// including) hi. +func IntegerRange(lo, hi Int) Iterator { + if lo.impl != nil { + i := lo + return func() (interface{}, bool) { + if hi.impl != nil && i.Cmp(hi) >= 0 { + return nil, false + } else { + ans := i + i = i.Plus(One) + return ans, true + } + } + } else if hi.impl != nil { + i := hi + return func() (interface{}, bool) { + ans := i + i = i.Minus(One) + return ans, true + } + } else { + return AllIntegers() + } +} + +// AllIntegers returns an iterator over all integers, starting at zero and +// alternating between positive and negative. +func AllIntegers() Iterator { + type phase int + const ( + zeroPhase int = iota + posPhase + negPhase + ) + + i := Zero + p := zeroPhase + + return func() (interface{}, bool) { + switch p { + case zeroPhase: + i = One + p = posPhase + return Zero, true + case posPhase: + p = negPhase + return i, true + case negPhase: + ans := i.Negated() + i = i.Plus(One) + p = posPhase + return ans, true + default: + panic("unknown phase") + } + } +} + +/****************************************************************************** + * Ordinals + ******************************************************************************/ + +// An Ord is an immutable big integer (presumed to be non-negative). +type Ord = Int + +// IsLimitOrd returns true for a limit ordinal. +func (ord Ord) IsLimitOrd() bool { + return ord.Cmp(Zero) == 0 +} + +// IsSuccOrd returns true for a successor ordinal. +func (ord Ord) IsSuccOrd() bool { + return ord.Cmp(Zero) > 0 +} + +// OrdOffset returns the ordinal as an Int. +func (ord Ord) OrdOffset() Int { + return ord +} + +// IsNatOrd returns true if the ordinal represents a natural number. +func (Ord) IsNatOrd() bool { + return true // at run time, every ORDINAL is a natural number +} + +/****************************************************************************** + * Reals + ******************************************************************************/ + +// A Real is an arbitrary-precision real number, represented as a ratio of +// arbitrary-precision integers. +type Real struct { + impl *big.Rat + // debug string +} + +func realOf(r *big.Rat) Real { + return Real{ + impl: r, + // debug: r.String() + } +} + +// RealOf converts a float64 into a Real. Common values are cached. +func RealOf(f float64) Real { + if f == 0.0 { + return ZeroReal + } + return realOf(new(big.Rat).SetFloat64(f)) +} + +// RealOfFrac makes a Real of the ratio of two Ints. +func RealOfFrac(num, denom Int) Real { + if num.Cmp(Zero) == 0 { + return ZeroReal + } + return realOf(new(big.Rat).SetFrac(num.impl, denom.impl)) +} + +// ZeroReal is the Real value zero. +var ZeroReal = realOf(new(big.Rat)) + +// NilReal is a missing Real value. +var NilReal = realOf(nil) + +// IsNilReal returns whether this is actually a missing value. +func (x Real) IsNilReal() bool { + return x.impl == nil +} + +// RealOfString parses the given string in base 10 and panics if this is not +// possible. +func RealOfString(s string) Real { + x, ok := new(big.Rat).SetString(s) + if !ok { + panic("Can't parse generated string as ratio: \"" + s + "\"") + } + if x.Cmp(ZeroReal.impl) == 0 { + return ZeroReal + } + return realOf(x) +} + +// Int converts the given real to an integer, rounding toward negative numbers. +// (That is, returns floor(x).) +func (x Real) Int() Int { + if x.Cmp(ZeroReal) == 0 || x.Denom().Cmp(One) == 0 { + return x.Num() + } else if x.Num().Cmp(Zero) > 0 { + return intOf(new(big.Int).Div(x.impl.Num(), x.impl.Denom())) + } else { + a := new(big.Int).Sub(x.impl.Num(), x.impl.Denom()) + a.Add(a, One.impl) + return intOf(a.Quo(a, x.impl.Denom())) // note: *truncated* division + } +} + +func (x Real) IsInteger() bool { + return RealOfFrac(x.Int(), One).Cmp(x) == 0 +} + +// Num returns the given Real's numerator as an Int +func (x Real) Num() Int { + return intOf(x.impl.Num()) +} + +// Denom returns the given Real's denominator as an Int +func (x Real) Denom() Int { + return intOf(x.impl.Denom()) +} + +func (x Real) String() string { + if x.Num().Cmp(Zero) == 0 || x.Denom().Cmp(One) == 0 { + return x.Num().String() + ".0" + } + divsPow10, fact, log10 := x.Denom().dividesAPowerOf10() + if divsPow10 { + num := x.Num().Times(fact) + var sign, digits string + if x.Cmp(ZeroReal) < 0 { + sign, digits = "-", num.Negated().String() + } else { + sign, digits = "", num.String() + } + if log10 < len(digits) { + n := len(digits) - log10 + return sign + digits[0:n] + "." + digits[n:] + } else { + s := sign + "0." + for i := 0; i < log10-len(digits); i++ { + s = s + "0" + } + return s + digits + } + } else { + return "(" + x.Num().String() + ".0 / " + x.Denom().String() + ".0)" + } +} + +func (x Real) isPowerOf10() (bool, int) { + if x.Num().Cmp(Zero) != 1 { + return false, -1 + } else if x.Num().Cmp(One) == 1 { + b, i := x.Denom().isPowerOf10() + return b, -i + } else if x.Denom().Cmp(One) != 1 { + return false, -1 + } else { + return x.Num().isPowerOf10() + } +} + +// binOp lifts a binary operation on *big.Rat to one on Reals. The second +// argument is intended to be of the form (*big.Rat).Op. +func (x Real) binOp(y Real, f func(*big.Rat, *big.Rat, *big.Rat) *big.Rat) Real { + return realOf(f(new(big.Rat), x.impl, y.impl)) +} + +// Plus adds two Reals. +func (x Real) Plus(y Real) Real { + return x.binOp(y, (*big.Rat).Add) +} + +// Minus subtracts one Real from another. +func (x Real) Minus(y Real) Real { + return x.binOp(y, (*big.Rat).Sub) +} + +// Times multiplies two Reals. +func (x Real) Times(y Real) Real { + return x.binOp(y, (*big.Rat).Mul) +} + +// DivBy divides one Real by another. +func (x Real) DivBy(y Real) Real { + return x.binOp(y, (*big.Rat).Quo) +} + +// Cmp compares one Real to another, returning -1 for less, 0 for equal, or 1 +// for greater. +func (x Real) Cmp(y Real) int { + return x.impl.Cmp(y.impl) +} + +// Sign returns the sign of a Real, returning -1 for negative, 0 for zero, or +// 1 for positive. +func (x Real) Sign() int { + return x.impl.Sign() +} + +// EqualsGeneric compares an int to another value. +func (x Real) EqualsGeneric(other interface{}) bool { + y, ok := other.(Real) + return ok && x.Cmp(y) == 0 +} + +// Min returns the minimum of two reals. +func (x Real) Min(y Real) Real { + if x.Cmp(y) <= 0 { + return x + } else { + return y + } +} + +// Max returns the maximum of two reals. +func (x Real) Max(y Real) Real { + if x.Cmp(y) >= 0 { + return x + } else { + return y + } +} + +/****************************************************************************** + * Native math + ******************************************************************************/ + +// DivInt does Euclidean division on the given ints +func DivInt(x int, y int) int { + if x >= 0 { + if y >= 0 { + return x / y + } else { + return -(x / -y) + } + } else { + if y >= 0 { + return -((-x - 1) / y) - 1 + } else { + return ((-x - 1) / (-y)) + 1 + } + } +} + +// DivInt8 does Euclidean divison on the given int8s +func DivInt8(x int8, y int8) int8 { + if x >= 0 { + if y >= 0 { + return x / y + } else { + return -(x / -y) + } + } else { + if y >= 0 { + return -((-x - 1) / y) - 1 + } else { + return ((-x - 1) / (-y)) + 1 + } + } +} + +// DivInt16 does Euclidean divison on the given int16s +func DivInt16(x int16, y int16) int16 { + if x >= 0 { + if y >= 0 { + return x / y + } else { + return -(x / -y) + } + } else { + if y >= 0 { + return -((-x - 1) / y) - 1 + } else { + return ((-x - 1) / (-y)) + 1 + } + } +} + +// DivInt32 does Euclidean divison on the given int32s +func DivInt32(x int32, y int32) int32 { + if x >= 0 { + if y >= 0 { + return x / y + } else { + return -(x / -y) + } + } else { + if y >= 0 { + return -((-x - 1) / y) - 1 + } else { + return ((-x - 1) / (-y)) + 1 + } + } +} + +// DivInt64 does Euclidean divison on the given int64s +func DivInt64(x int64, y int64) int64 { + if x >= 0 { + if y >= 0 { + return x / y + } else { + return -(x / -y) + } + } else { + if y >= 0 { + return -((-x - 1) / y) - 1 + } else { + return ((-x - 1) / (-y)) + 1 + } + } +} + +// DivFloat32 does Euclidean division on the given float32s +func DivFloat32(x float32, y float32) float32 { + if x >= 0 { + if y >= 0 { + return x / y + } else { + return -(x / -y) + } + } else { + if y >= 0 { + return -((-x - 1) / y) - 1 + } else { + return ((-x - 1) / (-y)) + 1 + } + } +} + +// DivFloat64 does Euclidean division on the given float64s +func DivFloat64(x float64, y float64) float64 { + if x >= 0 { + if y >= 0 { + return x / y + } else { + return -(x / -y) + } + } else { + if y >= 0 { + return -((-x - 1) / y) - 1 + } else { + return ((-x - 1) / (-y)) + 1 + } + } +} + +// LrotUint performs left rotation on the low w bits of an int +func LrotUint(x uint, n Int, w uint) uint { + y := n.Uint() + return ((x << y) % (1 << w)) | (x >> (w - y)) +} + +// LrotUint8 performs left rotation on the low w bits of an int8 +func LrotUint8(x uint8, n Int, w uint) uint8 { + y := n.Uint() + return ((x << y) % (1 << w)) | (x >> (w - y)) +} + +// LrotUint16 performs left rotation on the low w bits of an int16 +func LrotUint16(x uint16, n Int, w uint) uint16 { + y := n.Uint() + return ((x << y) % (1 << w)) | (x >> (w - y)) +} + +// LrotUint32 performs left rotation on the low w bits of an int32 +func LrotUint32(x uint32, n Int, w uint) uint32 { + y := n.Uint() + return ((x << y) % (1 << w)) | (x >> (w - y)) +} + +// LrotUint64 performs left rotation on the low w bits of an int64 +func LrotUint64(x uint64, n Int, w uint) uint64 { + y := n.Uint() + return ((x << y) % (1 << w)) | (x >> (w - y)) +} + +// ModInt finds Euclidean remainder of the given ints +func ModInt(x int, y int) int { + if y < 0 { + y = -y + } + if x >= 0 { + return x % y + } else { + z := (-x) % y + if z == 0 { + return 0 + } else { + return y - z + } + } +} + +// ModInt8 finds Euclidean remainder of the given int8s +func ModInt8(x int8, y int8) int8 { + if y < 0 { + y = -y + } + if x >= 0 { + return x % y + } else { + z := (-x) % y + if z == 0 { + return 0 + } else { + return y - z + } + } +} + +// ModInt16 finds Euclidean remainder of the given int16s +func ModInt16(x int16, y int16) int16 { + if y < 0 { + y = -y + } + if x >= 0 { + return x % y + } else { + z := (-x) % y + if z == 0 { + return 0 + } else { + return y - z + } + } +} + +// ModInt32 finds Euclidean remainder of the given int32s +func ModInt32(x int32, y int32) int32 { + if y < 0 { + y = -y + } + if x >= 0 { + return x % y + } else { + z := (-x) % y + if z == 0 { + return 0 + } else { + return y - z + } + } +} + +// ModInt64 finds Euclidean remainder of the given int64s +func ModInt64(x int64, y int64) int64 { + if y < 0 { + y = -y + } + if x >= 0 { + return x % y + } else { + z := (-x) % y + if z == 0 { + return 0 + } else { + return y - z + } + } +} + +// RrotUint performs right rotation on the low w bits of an int +func RrotUint(x uint, n Int, w uint) uint { + y := n.Uint() + return (x >> y) | ((x << (w - y)) % (1 << w)) +} + +// RrotUint8 performs right rotation on the low w bits of an int8 +func RrotUint8(x uint8, n Int, w uint) uint8 { + y := n.Uint() + return (x >> y) | ((x << (w - y)) % (1 << w)) +} + +// RrotUint16 performs right rotation on the low w bits of an int16 +func RrotUint16(x uint16, n Int, w uint) uint16 { + y := n.Uint() + return (x >> y) | ((x << (w - y)) % (1 << w)) +} + +// RrotUint32 performs right rotation on the low w bits of an int32 +func RrotUint32(x uint32, n Int, w uint) uint32 { + y := n.Uint() + return (x >> y) | ((x << (w - y)) % (1 << w)) +} + +// RrotUint64 performs right rotation on the low w bits of an int64 +func RrotUint64(x uint64, n Int, w uint) uint64 { + y := n.Uint() + return (x >> y) | ((x << (w - y)) % (1 << w)) +} + +/****************************************************************************** + * Utility functions + ******************************************************************************/ + +func min(n, m int) int { + if n <= m { + return n + } else { + return m + } +} + +func max(n, m int) int { + if n >= m { + return n + } else { + return m + } +} + +func CatchHalt() { + if r := recover(); r != nil { + fmt.Println("[Program halted]", r) + os.Exit(1) + } +} + +type GoAtomicBox struct { + value interface{} +} + +func (box *GoAtomicBox) Get() interface{} { + return box.value +} + +func (box *GoAtomicBox) Put(value interface{}) { + box.value = value +} + +func (box *GoAtomicBox) String() string { + return "dafny.GoAtomicBox" +} + +func (CompanionStruct_AtomicBox_) Make(value interface{}) AtomicBox { + return &GoAtomicBox{ + value: value, + } +} + +func (CompanionStruct_Helpers_) DafnyValueToDafnyString(value interface{}) Sequence { + return SeqOfString(String(value)) +} diff --git a/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/dafny/dafnyFromDafny.go b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/dafny/dafnyFromDafny.go new file mode 100644 index 000000000..463fb517b --- /dev/null +++ b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/dafny/dafnyFromDafny.go @@ -0,0 +1,1334 @@ +// Package dafny +// Dafny module dafny compiled into Go + +package dafny + +type Dummy__ struct{} + +// Definition of class Default__ +type Default__ struct { + dummy byte +} + +func New_Default___() *Default__ { + _this := Default__{} + + return &_this +} + +type CompanionStruct_Default___ struct { +} + +var Companion_Default___ = CompanionStruct_Default___{} + +func (_this *Default__) Equals(other *Default__) bool { + return _this == other +} + +func (_this *Default__) EqualsGeneric(x interface{}) bool { + other, ok := x.(*Default__) + return ok && _this.Equals(other) +} + +func (*Default__) String() string { + return "dafny.Default__" +} +func (_this *Default__) ParentTraits_() []*TraitID { + return [](*TraitID){} +} + +var _ TraitOffspring = &Default__{} + +func (_static *CompanionStruct_Default___) SizeAdditionInRange(a uint32, b uint32) bool { + var _hresult bool = false + _ = _hresult + _hresult = (a) <= ((Companion_Default___.SIZE__T__MAX()) - (func() uint32 { return (b) })()) + return _hresult + return _hresult +} +func (_static *CompanionStruct_Default___) AppendRecursive(builder *Vector, e Sequence) { + if func(_is_0 Sequence) bool { + return InstanceOf(_is_0, (*ConcatSequence)(nil)) + }(e) { + var _0_concat *ConcatSequence + _ = _0_concat + _0_concat = e.(*ConcatSequence) + Companion_Default___.AppendRecursive(builder, (_0_concat).Left()) + Companion_Default___.AppendRecursive(builder, (_0_concat).Right()) + } else if func(_is_1 Sequence) bool { + return InstanceOf(_is_1, (*LazySequence)(nil)) + }(e) { + var _1_lazy *LazySequence + _ = _1_lazy + _1_lazy = e.(*LazySequence) + var _2_boxed Sequence + _ = _2_boxed + var _out0 interface{} + _ = _out0 + _out0 = ((_1_lazy).Box()).Get() + _2_boxed = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out0)) + Companion_Default___.AppendRecursive(builder, _2_boxed) + } else { + var _3_a ImmutableArray + _ = _3_a + var _out1 ImmutableArray + _ = _out1 + _out1 = Companion_ImmutableArray_.CastTo_((e).ToArray()) + _3_a = Companion_ImmutableArray_.CastTo_(_out1) + (builder).Append(_3_a) + } +} +func (_static *CompanionStruct_Default___) AppendOptimized(builder *Vector, e Sequence, stack *Vector) { + goto TAIL_CALL_START +TAIL_CALL_START: + if func(_is_2 Sequence) bool { + return InstanceOf(_is_2, (*ConcatSequence)(nil)) + }(e) { + var _0_concat *ConcatSequence + _ = _0_concat + _0_concat = e.(*ConcatSequence) + if !(Companion_Default___.SizeAdditionInRange(stack.Size, Companion_Default___.ONE__SIZE())) { + panic("dafnyRuntime.dfy(805,6): " + (SeqOfString("expectation violation")).String()) + } + (stack).AddLast((_0_concat).Right()) + var _in0 *Vector = builder + _ = _in0 + var _in1 Sequence = (_0_concat).Left() + _ = _in1 + var _in2 *Vector = stack + _ = _in2 + builder = _in0 + e = _in1 + stack = _in2 + goto TAIL_CALL_START + } else if func(_is_3 Sequence) bool { + return InstanceOf(_is_3, (*LazySequence)(nil)) + }(e) { + var _1_lazy *LazySequence + _ = _1_lazy + _1_lazy = e.(*LazySequence) + var _2_boxed Sequence + _ = _2_boxed + var _out0 interface{} + _ = _out0 + _out0 = ((_1_lazy).Box()).Get() + _2_boxed = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out0)) + var _in3 *Vector = builder + _ = _in3 + var _in4 Sequence = _2_boxed + _ = _in4 + var _in5 *Vector = stack + _ = _in5 + builder = _in3 + e = _in4 + stack = _in5 + goto TAIL_CALL_START + } else if func(_is_4 Sequence) bool { + return InstanceOf(_is_4, (*ArraySequence)(nil)) + }(e) { + var _3_a *ArraySequence + _ = _3_a + _3_a = e.(*ArraySequence) + (builder).Append((_3_a).Values()) + if (uint32(0)) < (stack.Size) { + var _4_next Sequence + _ = _4_next + var _out1 interface{} + _ = _out1 + _out1 = (stack).RemoveLast() + _4_next = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out1)) + var _in6 *Vector = builder + _ = _in6 + var _in7 Sequence = _4_next + _ = _in7 + var _in8 *Vector = stack + _ = _in8 + builder = _in6 + e = _in7 + stack = _in8 + goto TAIL_CALL_START + } + } else { + if !(false) { + panic("dafnyRuntime.dfy(828,6): " + (SeqOfString("Unsupported Sequence implementation")).String()) + } + } +} +func (_static *CompanionStruct_Default___) SIZE__T__LIMIT() Int { + return IntOfInt64(2147483648) +} +func (_static *CompanionStruct_Default___) SIZE__T__MAX() uint32 { + return ((Companion_Default___.SIZE__T__LIMIT()).Minus(One)).Uint32() +} +func (_static *CompanionStruct_Default___) ZERO__SIZE() uint32 { + return uint32(0) +} +func (_static *CompanionStruct_Default___) ONE__SIZE() uint32 { + return uint32(1) +} +func (_static *CompanionStruct_Default___) TWO__SIZE() uint32 { + return uint32(2) +} +func (_static *CompanionStruct_Default___) TEN__SIZE() uint32 { + return uint32(10) +} + +// End of class Default__ + +// Definition of trait Sequence +type Sequence interface { + String() string + Equals(other Sequence) bool + EqualsGeneric(x interface{}) bool + VerbatimString(isLiteral bool) string + SetString() Sequence + IsString() bool + IsString_set_(value bool) + Cardinality() uint32 + PrototypeArray() ImmutableArray + Select(index uint32) interface{} + Drop(lo uint32) Sequence + Take(hi uint32) Sequence + Subsequence(lo uint32, hi uint32) Sequence + ToArray() ImmutableArray + Elements() Sequence + UniqueElements() Set +} + +func (_static *CompanionStruct_Sequence_) SetString(_this Sequence) Sequence { + { + var ret Sequence = (Sequence)(nil) + _ = ret + (_this).IsString_set_(true) + ret = _this + return ret + return ret + } +} +func (_static *CompanionStruct_Sequence_) Select(_this Sequence, index uint32) interface{} { + { + var ret interface{} = (interface{})(nil) + _ = ret + var _0_a ImmutableArray + _ = _0_a + var _out0 ImmutableArray + _ = _out0 + _out0 = (_this).ToArray() + _0_a = _out0 + ret = (_0_a).Select(index) + return ret + return ret + } +} +func (_static *CompanionStruct_Sequence_) Drop(_this Sequence, lo uint32) Sequence { + { + var ret Sequence = (Sequence)(nil) + _ = ret + var _out0 Sequence + _ = _out0 + _out0 = (_this).Subsequence(lo, (_this).Cardinality()) + ret = _out0 + return ret + } +} +func (_static *CompanionStruct_Sequence_) Take(_this Sequence, hi uint32) Sequence { + { + var ret Sequence = (Sequence)(nil) + _ = ret + var _out0 Sequence + _ = _out0 + _out0 = (_this).Subsequence(uint32(0), hi) + ret = _out0 + return ret + } +} +func (_static *CompanionStruct_Sequence_) Subsequence(_this Sequence, lo uint32, hi uint32) Sequence { + { + var ret Sequence = (Sequence)(nil) + _ = ret + var _0_a ImmutableArray + _ = _0_a + var _out0 ImmutableArray + _ = _out0 + _out0 = (_this).ToArray() + _0_a = _out0 + var _1_subarray ImmutableArray + _ = _1_subarray + var _out1 ImmutableArray + _ = _out1 + _out1 = Companion_ImmutableArray_.CastTo_((_0_a).Subarray(lo, hi)) + _1_subarray = Companion_ImmutableArray_.CastTo_(_out1) + var _nw0 *ArraySequence = New_ArraySequence_() + _ = _nw0 + _nw0.Ctor__(_1_subarray, false) + ret = _nw0 + return ret + } +} +func (_static *CompanionStruct_Sequence_) Elements(_this Sequence) Sequence { + { + return _this + } +} +func (_static *CompanionStruct_Sequence_) Create(cardinality uint32, initFn func(uint32) interface{}) Sequence { + var ret Sequence = (Sequence)(nil) + _ = ret + var _0_a NativeArray + _ = _0_a + var _out0 NativeArray + _ = _out0 + _out0 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.MakeWithInit(cardinality, func(coer0 func(uint32) interface{}) func(uint32) interface{} { + return func(arg0 uint32) interface{} { + return coer0(arg0) + } + }(initFn))) + _0_a = Companion_NativeArray_.CastTo_(_out0) + var _1_frozen ImmutableArray + _ = _1_frozen + var _out1 ImmutableArray + _ = _out1 + _out1 = Companion_ImmutableArray_.CastTo_((_0_a).Freeze(cardinality)) + _1_frozen = Companion_ImmutableArray_.CastTo_(_out1) + var _nw0 *ArraySequence = New_ArraySequence_() + _ = _nw0 + _nw0.Ctor__(_1_frozen, false) + ret = _nw0 + return ret +} +func (_static *CompanionStruct_Sequence_) Equal(left Sequence, right Sequence) bool { + var ret bool = false + _ = ret + if ((left).Cardinality()) != ((right).Cardinality()) /* dircomp */ { + ret = false + return ret + } + var _out0 bool + _ = _out0 + _out0 = Companion_Sequence_.EqualUpTo(left, right, (left).Cardinality()) + ret = _out0 + return ret +} +func (_static *CompanionStruct_Sequence_) IsPrefixOf(left Sequence, right Sequence) bool { + var ret bool = false + _ = ret + if ((right).Cardinality()) < ((left).Cardinality()) { + ret = false + return ret + } + var _out0 bool + _ = _out0 + _out0 = Companion_Sequence_.EqualUpTo(left, right, (left).Cardinality()) + ret = _out0 + return ret +} +func (_static *CompanionStruct_Sequence_) IsProperPrefixOf(left Sequence, right Sequence) bool { + var ret bool = false + _ = ret + if ((right).Cardinality()) <= ((left).Cardinality()) { + ret = false + return ret + } + var _out0 bool + _ = _out0 + _out0 = Companion_Sequence_.EqualUpTo(left, right, (left).Cardinality()) + ret = _out0 + return ret +} +func (_static *CompanionStruct_Sequence_) Contains(s Sequence, t interface{}) bool { + var _hresult bool = false + _ = _hresult + var _hi0 uint32 = (s).Cardinality() + _ = _hi0 + for _0_i := Companion_Default___.ZERO__SIZE(); _0_i < _hi0; _0_i++ { + var _1_element interface{} + _ = _1_element + var _out0 interface{} + _ = _out0 + _out0 = (s).Select(_0_i) + _1_element = _out0 + if AreEqual(_1_element, t) { + _hresult = true + return _hresult + } + } + _hresult = false + return _hresult + return _hresult +} +func (_static *CompanionStruct_Sequence_) Update(s Sequence, i uint32, t interface{}) Sequence { + var ret Sequence = (Sequence)(nil) + _ = ret + var _0_a ImmutableArray + _ = _0_a + var _out0 ImmutableArray + _ = _out0 + _out0 = Companion_ImmutableArray_.CastTo_((s).ToArray()) + _0_a = Companion_ImmutableArray_.CastTo_(_out0) + var _1_newValue NativeArray + _ = _1_newValue + var _out1 NativeArray + _ = _out1 + _out1 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.Copy(_0_a)) + _1_newValue = Companion_NativeArray_.CastTo_(_out1) + (_1_newValue).Update(i, t) + var _2_newValueFrozen ImmutableArray + _ = _2_newValueFrozen + var _out2 ImmutableArray + _ = _out2 + _out2 = Companion_ImmutableArray_.CastTo_((_1_newValue).Freeze((_1_newValue).Length())) + _2_newValueFrozen = Companion_ImmutableArray_.CastTo_(_out2) + var _nw0 *ArraySequence = New_ArraySequence_() + _ = _nw0 + _nw0.Ctor__(_2_newValueFrozen, false) + ret = _nw0 + return ret +} +func (_static *CompanionStruct_Sequence_) Concatenate(left Sequence, right Sequence) Sequence { + var ret Sequence = (Sequence)(nil) + _ = ret + if !(Companion_Default___.SizeAdditionInRange((left).Cardinality(), (right).Cardinality())) { + panic("dafnyRuntime.dfy(616,6): " + (Companion_Sequence_.Concatenate(Companion_Sequence_.Concatenate(SeqOfString("Concatenation result cardinality would be larger than the maximum ("), Companion_Helpers_.DafnyValueToDafnyString(Companion_Default___.SIZE__T__MAX())), SeqOfString(")"))).String()) + } + var _0_left_k Sequence + _ = _0_left_k + _0_left_k = left + if func(_is_5 Sequence) bool { + return InstanceOf(_is_5, (*LazySequence)(nil)) + }(left) { + var _1_lazyLeft *LazySequence + _ = _1_lazyLeft + _1_lazyLeft = left.(*LazySequence) + var _out0 interface{} + _ = _out0 + _out0 = ((_1_lazyLeft).Box()).Get() + _0_left_k = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out0)) + } + var _2_right_k Sequence + _ = _2_right_k + _2_right_k = right + if func(_is_6 Sequence) bool { + return InstanceOf(_is_6, (*LazySequence)(nil)) + }(right) { + var _3_lazyRight *LazySequence + _ = _3_lazyRight + _3_lazyRight = right.(*LazySequence) + var _out1 interface{} + _ = _out1 + _out1 = ((_3_lazyRight).Box()).Get() + _2_right_k = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out1)) + } + var _4_c *ConcatSequence + _ = _4_c + var _nw0 *ConcatSequence = New_ConcatSequence_() + _ = _nw0 + _nw0.Ctor__(_0_left_k, _2_right_k) + _4_c = _nw0 + var _nw1 *LazySequence = New_LazySequence_() + _ = _nw1 + _nw1.Ctor__(_4_c) + ret = _nw1 + return ret +} + +type CompanionStruct_Sequence_ struct { + TraitID_ *TraitID +} + +var Companion_Sequence_ = CompanionStruct_Sequence_{ + TraitID_: &TraitID{}, +} + +func (CompanionStruct_Sequence_) CastTo_(x interface{}) Sequence { + var t Sequence + t, _ = x.(Sequence) + return t +} + +// End of trait Sequence + +// Definition of trait Validatable +type Validatable interface { + String() string +} +type CompanionStruct_Validatable_ struct { + TraitID_ *TraitID +} + +var Companion_Validatable_ = CompanionStruct_Validatable_{ + TraitID_: &TraitID{}, +} + +func (CompanionStruct_Validatable_) CastTo_(x interface{}) Validatable { + var t Validatable + t, _ = x.(Validatable) + return t +} + +// End of trait Validatable + +// Definition of class Size__t +type Size__t struct { +} + +func New_Size__t_() *Size__t { + _this := Size__t{} + + return &_this +} + +type CompanionStruct_Size__t_ struct { +} + +var Companion_Size__t_ = CompanionStruct_Size__t_{} + +func (*Size__t) String() string { + return "dafny.Size__t" +} +func (_this *Size__t) ParentTraits_() []*TraitID { + return [](*TraitID){} +} + +var _ TraitOffspring = &Size__t{} + +func (_this *CompanionStruct_Size__t_) IntegerRange(lo Int, hi Int) Iterator { + iter := IntegerRange(lo, hi) + return func() (interface{}, bool) { + next, ok := iter() + if !ok { + return uint32(0), false + } + return next.(Int).Uint32(), true + } +} +func (_this *CompanionStruct_Size__t_) Witness() uint32 { + return (Zero).Uint32() +} + +// End of class Size__t + +func Type_Size__t_() TypeDescriptor { + return type_Size__t_{} +} + +type type_Size__t_ struct { +} + +func (_this type_Size__t_) Default() interface{} { + return Companion_Size__t_.Witness() +} + +func (_this type_Size__t_) String() string { + return "dafny.Size__t" +} +func (_this *CompanionStruct_Size__t_) Is_(__source uint32) bool { + var _0_x Int = IntOfUint32(__source) + _ = _0_x + return ((_0_x).Sign() != -1) && ((_0_x).Cmp(Companion_Default___.SIZE__T__LIMIT()) < 0) +} + +// Definition of trait NativeArray +type NativeArray interface { + String() string + Length() uint32 + Select(i uint32) interface{} + Update(i uint32, t interface{}) + UpdateSubarray(start uint32, other ImmutableArray) + Freeze(size uint32) ImmutableArray +} +type CompanionStruct_NativeArray_ struct { + TraitID_ *TraitID +} + +var Companion_NativeArray_ = CompanionStruct_NativeArray_{ + TraitID_: &TraitID{}, +} + +func (CompanionStruct_NativeArray_) CastTo_(x interface{}) NativeArray { + var t NativeArray + t, _ = x.(NativeArray) + return t +} + +// End of trait NativeArray + +// Definition of datatype ArrayCell +type ArrayCell struct { + Data_ArrayCell_ +} + +func (_this ArrayCell) Get_() Data_ArrayCell_ { + return _this.Data_ArrayCell_ +} + +type Data_ArrayCell_ interface { + isArrayCell() +} + +type CompanionStruct_ArrayCell_ struct { +} + +var Companion_ArrayCell_ = CompanionStruct_ArrayCell_{} + +type ArrayCell_Set struct { + Value interface{} +} + +func (ArrayCell_Set) isArrayCell() {} + +func (CompanionStruct_ArrayCell_) Create_Set_(Value interface{}) ArrayCell { + return ArrayCell{ArrayCell_Set{Value}} +} + +func (_this ArrayCell) Is_Set() bool { + _, ok := _this.Get_().(ArrayCell_Set) + return ok +} + +type ArrayCell_Unset struct { +} + +func (ArrayCell_Unset) isArrayCell() {} + +func (CompanionStruct_ArrayCell_) Create_Unset_() ArrayCell { + return ArrayCell{ArrayCell_Unset{}} +} + +func (_this ArrayCell) Is_Unset() bool { + _, ok := _this.Get_().(ArrayCell_Unset) + return ok +} + +func (CompanionStruct_ArrayCell_) Default() ArrayCell { + return Companion_ArrayCell_.Create_Unset_() +} + +func (_this ArrayCell) Dtor_value() interface{} { + return _this.Get_().(ArrayCell_Set).Value +} + +func (_this ArrayCell) String() string { + switch data := _this.Get_().(type) { + case nil: + return "null" + case ArrayCell_Set: + { + return "DafnyGo.ArrayCell.Set" + "(" + String(data.Value) + ")" + } + case ArrayCell_Unset: + { + return "DafnyGo.ArrayCell.Unset" + } + default: + { + return "" + } + } +} + +func (_this ArrayCell) Equals(other ArrayCell) bool { + switch data1 := _this.Get_().(type) { + case ArrayCell_Set: + { + data2, ok := other.Get_().(ArrayCell_Set) + return ok && AreEqual(data1.Value, data2.Value) + } + case ArrayCell_Unset: + { + _, ok := other.Get_().(ArrayCell_Unset) + return ok + } + default: + { + return false // unexpected + } + } +} + +func (_this ArrayCell) EqualsGeneric(other interface{}) bool { + typed, ok := other.(ArrayCell) + return ok && _this.Equals(typed) +} + +func Type_ArrayCell_() TypeDescriptor { + return type_ArrayCell_{} +} + +type type_ArrayCell_ struct { +} + +func (_this type_ArrayCell_) Default() interface{} { + return Companion_ArrayCell_.Default() +} + +func (_this type_ArrayCell_) String() string { + return "dafny.ArrayCell" +} +func (_this ArrayCell) ParentTraits_() []*TraitID { + return [](*TraitID){} +} + +var _ TraitOffspring = ArrayCell{} + +// End of datatype ArrayCell + +// Definition of trait ImmutableArray +type ImmutableArray interface { + String() string + Length() uint32 + Select(index uint32) interface{} + Subarray(lo uint32, hi uint32) ImmutableArray +} +type CompanionStruct_ImmutableArray_ struct { + TraitID_ *TraitID +} + +var Companion_ImmutableArray_ = CompanionStruct_ImmutableArray_{ + TraitID_: &TraitID{}, +} + +func (CompanionStruct_ImmutableArray_) CastTo_(x interface{}) ImmutableArray { + var t ImmutableArray + t, _ = x.(ImmutableArray) + return t +} + +// End of trait ImmutableArray + +// Definition of class Vector +type Vector struct { + Storage NativeArray + Size uint32 +} + +func New_Vector_() *Vector { + _this := Vector{} + + _this.Storage = (NativeArray)(nil) + _this.Size = Companion_Size__t_.Witness() + return &_this +} + +type CompanionStruct_Vector_ struct { +} + +var Companion_Vector_ = CompanionStruct_Vector_{} + +func (_this *Vector) Equals(other *Vector) bool { + return _this == other +} + +func (_this *Vector) EqualsGeneric(x interface{}) bool { + other, ok := x.(*Vector) + return ok && _this.Equals(other) +} + +func (*Vector) String() string { + return "dafny.Vector" +} + +func Type_Vector_(Type_T_ TypeDescriptor) TypeDescriptor { + return type_Vector_{Type_T_} +} + +type type_Vector_ struct { + Type_T_ TypeDescriptor +} + +func (_this type_Vector_) Default() interface{} { + return (*Vector)(nil) +} + +func (_this type_Vector_) String() string { + return "dafny.Vector" +} +func (_this *Vector) ParentTraits_() []*TraitID { + return [](*TraitID){Companion_Validatable_.TraitID_} +} + +var _ Validatable = &Vector{} +var _ TraitOffspring = &Vector{} + +func (_this *Vector) Ctor__(length uint32) { + { + var _0_storage NativeArray + _ = _0_storage + var _out0 NativeArray + _ = _out0 + _out0 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.Make(length)) + _0_storage = Companion_NativeArray_.CastTo_(_out0) + (_this).Storage = _0_storage + (_this).Size = uint32(0) + } +} +func (_this *Vector) WithPrototype(length uint32, prototype ImmutableArray) { + { + var _0_storage NativeArray + _ = _0_storage + var _out0 NativeArray + _ = _out0 + _out0 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.MakeWithPrototype(length, prototype)) + _0_storage = Companion_NativeArray_.CastTo_(_out0) + (_this).Storage = _0_storage + (_this).Size = uint32(0) + } +} +func (_this *Vector) Select(index uint32) interface{} { + { + return (_this.Storage).Select(index) + } +} +func (_this *Vector) Last() interface{} { + { + return (_this.Storage).Select((_this.Size) - (func() uint32 { return (uint32(1)) })()) + } +} +func (_this *Vector) AddLast(t interface{}) { + { + (_this).EnsureCapacity((_this.Size) + (Companion_Default___.ONE__SIZE())) + (_this.Storage).Update(_this.Size, t) + (_this).Size = (_this.Size) + (uint32(1)) + } +} +func (_this *Vector) Max(a uint32, b uint32) uint32 { + { + if (a) < (b) { + return b + } else { + return a + } + } +} +func (_this *Vector) EnsureCapacity(newMinCapacity uint32) { + { + if ((_this.Storage).Length()) >= (newMinCapacity) { + return + } + var _0_newCapacity uint32 + _ = _0_newCapacity + _0_newCapacity = newMinCapacity + if ((_this.Storage).Length()) <= ((Companion_Default___.SIZE__T__MAX()) / (Companion_Default___.TWO__SIZE())) { + _0_newCapacity = (_this).Max(_0_newCapacity, ((_this.Storage).Length())*(Companion_Default___.TWO__SIZE())) + } + var _1_values ImmutableArray + _ = _1_values + var _out0 ImmutableArray + _ = _out0 + _out0 = Companion_ImmutableArray_.CastTo_((_this.Storage).Freeze(_this.Size)) + _1_values = Companion_ImmutableArray_.CastTo_(_out0) + var _2_newStorage NativeArray + _ = _2_newStorage + var _out1 NativeArray + _ = _out1 + _out1 = Companion_NativeArray_.CastTo_(Companion_NativeArray_.MakeWithPrototype(_0_newCapacity, _1_values)) + _2_newStorage = Companion_NativeArray_.CastTo_(_out1) + (_2_newStorage).UpdateSubarray(uint32(0), _1_values) + (_this).Storage = _2_newStorage + } +} +func (_this *Vector) RemoveLast() interface{} { + { + var t interface{} = (interface{})(nil) + _ = t + t = (_this.Storage).Select((_this.Size) - (func() uint32 { return (uint32(1)) })()) + (_this).Size = (_this.Size) - (func() uint32 { return (uint32(1)) })() + return t + } +} +func (_this *Vector) Append(other ImmutableArray) { + { + var _0_newSize uint32 + _ = _0_newSize + _0_newSize = (_this.Size) + ((other).Length()) + (_this).EnsureCapacity(_0_newSize) + (_this.Storage).UpdateSubarray(_this.Size, other) + (_this).Size = (_this.Size) + ((other).Length()) + } +} +func (_this *Vector) Freeze() ImmutableArray { + { + var ret ImmutableArray = (ImmutableArray)(nil) + _ = ret + var _out0 ImmutableArray + _ = _out0 + _out0 = Companion_ImmutableArray_.CastTo_((_this.Storage).Freeze(_this.Size)) + ret = Companion_ImmutableArray_.CastTo_(_out0) + return ret + } +} + +// End of class Vector + +// Definition of trait AtomicBox +type AtomicBox interface { + String() string + Get() interface{} + Put(t interface{}) +} +type CompanionStruct_AtomicBox_ struct { + TraitID_ *TraitID +} + +var Companion_AtomicBox_ = CompanionStruct_AtomicBox_{ + TraitID_: &TraitID{}, +} + +func (CompanionStruct_AtomicBox_) CastTo_(x interface{}) AtomicBox { + var t AtomicBox + t, _ = x.(AtomicBox) + return t +} + +// End of trait AtomicBox + +// Definition of class ArraySequence +type ArraySequence struct { + _isString bool + _values ImmutableArray +} + +func New_ArraySequence_() *ArraySequence { + _this := ArraySequence{} + + _this._isString = false + _this._values = (ImmutableArray)(nil) + return &_this +} + +type CompanionStruct_ArraySequence_ struct { +} + +var Companion_ArraySequence_ = CompanionStruct_ArraySequence_{} + +func Type_ArraySequence_(Type_T_ TypeDescriptor) TypeDescriptor { + return type_ArraySequence_{Type_T_} +} + +type type_ArraySequence_ struct { + Type_T_ TypeDescriptor +} + +func (_this type_ArraySequence_) Default() interface{} { + return (*ArraySequence)(nil) +} + +func (_this type_ArraySequence_) String() string { + return "dafny.ArraySequence" +} +func (_this *ArraySequence) ParentTraits_() []*TraitID { + return [](*TraitID){Companion_Sequence_.TraitID_} +} + +var _ Sequence = &ArraySequence{} +var _ TraitOffspring = &ArraySequence{} + +func (_this *ArraySequence) Drop(lo uint32) Sequence { + var _out1 Sequence + _ = _out1 + _out1 = Companion_Sequence_.Drop(_this, lo) + return _out1 +} +func (_this *ArraySequence) Elements() Sequence { + return Companion_Sequence_.Elements(_this) +} +func (_this *ArraySequence) IsString() bool { + return _this._isString +} +func (_this *ArraySequence) IsString_set_(value bool) { + _this._isString = value +} +func (_this *ArraySequence) Select(index uint32) interface{} { + var _out1 interface{} + _ = _out1 + _out1 = Companion_Sequence_.Select(_this, index) + return _out1 +} +func (_this *ArraySequence) SetString() Sequence { + var _out0 Sequence + _ = _out0 + _out0 = Companion_Sequence_.SetString(_this) + return _out0 +} +func (_this *ArraySequence) Subsequence(lo uint32, hi uint32) Sequence { + var _out2 Sequence + _ = _out2 + _out2 = Companion_Sequence_.Subsequence(_this, lo, hi) + return _out2 +} +func (_this *ArraySequence) Take(hi uint32) Sequence { + var _out1 Sequence + _ = _out1 + _out1 = Companion_Sequence_.Take(_this, hi) + return _out1 +} +func (_this *ArraySequence) PrototypeArray() ImmutableArray { + { + var ret ImmutableArray = (ImmutableArray)(nil) + _ = ret + ret = (_this).Values() + return ret + return ret + } +} +func (_this *ArraySequence) Ctor__(value ImmutableArray, isString bool) { + { + (_this)._values = value + (_this)._isString = isString + } +} +func (_this *ArraySequence) Cardinality() uint32 { + { + return ((_this).Values()).Length() + } +} +func (_this *ArraySequence) ToArray() ImmutableArray { + { + var ret ImmutableArray = (ImmutableArray)(nil) + _ = ret + ret = (_this).Values() + return ret + return ret + } +} +func (_this *ArraySequence) Values() ImmutableArray { + { + return _this._values + } +} + +// End of class ArraySequence + +// Definition of class ConcatSequence +type ConcatSequence struct { + _isString bool + _left Sequence + _right Sequence + _length uint32 +} + +func New_ConcatSequence_() *ConcatSequence { + _this := ConcatSequence{} + + _this._isString = false + _this._left = (Sequence)(nil) + _this._right = (Sequence)(nil) + _this._length = Companion_Size__t_.Witness() + return &_this +} + +type CompanionStruct_ConcatSequence_ struct { +} + +var Companion_ConcatSequence_ = CompanionStruct_ConcatSequence_{} + +func Type_ConcatSequence_(Type_T_ TypeDescriptor) TypeDescriptor { + return type_ConcatSequence_{Type_T_} +} + +type type_ConcatSequence_ struct { + Type_T_ TypeDescriptor +} + +func (_this type_ConcatSequence_) Default() interface{} { + return (*ConcatSequence)(nil) +} + +func (_this type_ConcatSequence_) String() string { + return "dafny.ConcatSequence" +} +func (_this *ConcatSequence) ParentTraits_() []*TraitID { + return [](*TraitID){Companion_Sequence_.TraitID_} +} + +var _ Sequence = &ConcatSequence{} +var _ TraitOffspring = &ConcatSequence{} + +func (_this *ConcatSequence) Drop(lo uint32) Sequence { + var _out2 Sequence + _ = _out2 + _out2 = Companion_Sequence_.Drop(_this, lo) + return _out2 +} +func (_this *ConcatSequence) Elements() Sequence { + return Companion_Sequence_.Elements(_this) +} +func (_this *ConcatSequence) IsString() bool { + return _this._isString +} +func (_this *ConcatSequence) IsString_set_(value bool) { + _this._isString = value +} +func (_this *ConcatSequence) Select(index uint32) interface{} { + var _out2 interface{} + _ = _out2 + _out2 = Companion_Sequence_.Select(_this, index) + return _out2 +} +func (_this *ConcatSequence) SetString() Sequence { + var _out1 Sequence + _ = _out1 + _out1 = Companion_Sequence_.SetString(_this) + return _out1 +} +func (_this *ConcatSequence) Subsequence(lo uint32, hi uint32) Sequence { + var _out3 Sequence + _ = _out3 + _out3 = Companion_Sequence_.Subsequence(_this, lo, hi) + return _out3 +} +func (_this *ConcatSequence) Take(hi uint32) Sequence { + var _out2 Sequence + _ = _out2 + _out2 = Companion_Sequence_.Take(_this, hi) + return _out2 +} +func (_this *ConcatSequence) PrototypeArray() ImmutableArray { + { + var ret ImmutableArray = (ImmutableArray)(nil) + _ = ret + var _out0 ImmutableArray + _ = _out0 + _out0 = Companion_ImmutableArray_.CastTo_(((_this).Left()).PrototypeArray()) + ret = Companion_ImmutableArray_.CastTo_(_out0) + return ret + } +} +func (_this *ConcatSequence) Ctor__(left Sequence, right Sequence) { + { + (_this)._left = left + (_this)._right = right + (_this)._length = ((left).Cardinality()) + ((right).Cardinality()) + (_this)._isString = (left.IsString()) || (right.IsString()) + } +} +func (_this *ConcatSequence) Cardinality() uint32 { + { + return (_this).Length() + } +} +func (_this *ConcatSequence) ToArray() ImmutableArray { + { + var ret ImmutableArray = (ImmutableArray)(nil) + _ = ret + var _0_prototype ImmutableArray + _ = _0_prototype + var _out0 ImmutableArray + _ = _out0 + _out0 = Companion_ImmutableArray_.CastTo_((_this).PrototypeArray()) + _0_prototype = Companion_ImmutableArray_.CastTo_(_out0) + var _1_builder *Vector + _ = _1_builder + var _nw0 *Vector = New_Vector_() + _ = _nw0 + _nw0.WithPrototype((_this).Length(), _0_prototype) + _1_builder = _nw0 + var _2_stack *Vector + _ = _2_stack + var _nw1 *Vector = New_Vector_() + _ = _nw1 + _nw1.Ctor__(Companion_Default___.TEN__SIZE()) + _2_stack = _nw1 + Companion_Default___.AppendOptimized(_1_builder, _this, _2_stack) + var _out1 ImmutableArray + _ = _out1 + _out1 = Companion_ImmutableArray_.CastTo_((_1_builder).Freeze()) + ret = Companion_ImmutableArray_.CastTo_(_out1) + return ret + } +} +func (_this *ConcatSequence) Left() Sequence { + { + return _this._left + } +} +func (_this *ConcatSequence) Right() Sequence { + { + return _this._right + } +} +func (_this *ConcatSequence) Length() uint32 { + { + return _this._length + } +} + +// End of class ConcatSequence + +// Definition of class LazySequence +type LazySequence struct { + _isString bool + _length uint32 + _box AtomicBox +} + +func New_LazySequence_() *LazySequence { + _this := LazySequence{} + + _this._isString = false + _this._length = Companion_Size__t_.Witness() + _this._box = (AtomicBox)(nil) + return &_this +} + +type CompanionStruct_LazySequence_ struct { +} + +var Companion_LazySequence_ = CompanionStruct_LazySequence_{} + +func Type_LazySequence_(Type_T_ TypeDescriptor) TypeDescriptor { + return type_LazySequence_{Type_T_} +} + +type type_LazySequence_ struct { + Type_T_ TypeDescriptor +} + +func (_this type_LazySequence_) Default() interface{} { + return (*LazySequence)(nil) +} + +func (_this type_LazySequence_) String() string { + return "dafny.LazySequence" +} +func (_this *LazySequence) ParentTraits_() []*TraitID { + return [](*TraitID){Companion_Sequence_.TraitID_} +} + +var _ Sequence = &LazySequence{} +var _ TraitOffspring = &LazySequence{} + +func (_this *LazySequence) Drop(lo uint32) Sequence { + var _out3 Sequence + _ = _out3 + _out3 = Companion_Sequence_.Drop(_this, lo) + return _out3 +} +func (_this *LazySequence) Elements() Sequence { + return Companion_Sequence_.Elements(_this) +} +func (_this *LazySequence) IsString() bool { + return _this._isString +} +func (_this *LazySequence) IsString_set_(value bool) { + _this._isString = value +} +func (_this *LazySequence) Select(index uint32) interface{} { + var _out3 interface{} + _ = _out3 + _out3 = Companion_Sequence_.Select(_this, index) + return _out3 +} +func (_this *LazySequence) SetString() Sequence { + var _out2 Sequence + _ = _out2 + _out2 = Companion_Sequence_.SetString(_this) + return _out2 +} +func (_this *LazySequence) Subsequence(lo uint32, hi uint32) Sequence { + var _out4 Sequence + _ = _out4 + _out4 = Companion_Sequence_.Subsequence(_this, lo, hi) + return _out4 +} +func (_this *LazySequence) Take(hi uint32) Sequence { + var _out3 Sequence + _ = _out3 + _out3 = Companion_Sequence_.Take(_this, hi) + return _out3 +} +func (_this *LazySequence) PrototypeArray() ImmutableArray { + { + var ret ImmutableArray = (ImmutableArray)(nil) + _ = ret + var _0_expr Sequence + _ = _0_expr + var _out0 interface{} + _ = _out0 + _out0 = ((_this).Box()).Get() + _0_expr = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out0)) + var _out1 ImmutableArray + _ = _out1 + _out1 = Companion_ImmutableArray_.CastTo_((_0_expr).PrototypeArray()) + ret = Companion_ImmutableArray_.CastTo_(_out1) + return ret + } +} +func (_this *LazySequence) Ctor__(wrapped Sequence) { + { + var _0_box AtomicBox + _ = _0_box + var _out0 AtomicBox + _ = _out0 + _out0 = Companion_AtomicBox_.CastTo_(Companion_AtomicBox_.Make(wrapped)) + _0_box = Companion_AtomicBox_.CastTo_(_out0) + (_this)._box = _0_box + (_this)._length = (wrapped).Cardinality() + (_this)._isString = wrapped.IsString() + } +} +func (_this *LazySequence) Cardinality() uint32 { + { + return (_this).Length() + } +} +func (_this *LazySequence) ToArray() ImmutableArray { + { + var ret ImmutableArray = (ImmutableArray)(nil) + _ = ret + var _0_expr Sequence + _ = _0_expr + var _out0 interface{} + _ = _out0 + _out0 = ((_this).Box()).Get() + _0_expr = Companion_Sequence_.CastTo_(Companion_Sequence_.CastTo_(_out0)) + if func(_is_7 Sequence) bool { + return InstanceOf(_is_7, (*ArraySequence)(nil)) + }(_0_expr) { + ret = (_0_expr.(*ArraySequence)).Values() + return ret + } + var _out1 ImmutableArray + _ = _out1 + _out1 = Companion_ImmutableArray_.CastTo_((_0_expr).ToArray()) + ret = Companion_ImmutableArray_.CastTo_(_out1) + var _1_arraySeq *ArraySequence + _ = _1_arraySeq + var _nw0 *ArraySequence = New_ArraySequence_() + _ = _nw0 + _nw0.Ctor__(ret, false) + _1_arraySeq = _nw0 + ((_this).Box()).Put(_1_arraySeq) + return ret + } +} +func (_this *LazySequence) Length() uint32 { + { + return _this._length + } +} +func (_this *LazySequence) Box() AtomicBox { + { + return _this._box + } +} + +// End of class LazySequence + +// Definition of trait Helpers +type Helpers interface { + String() string +} +type CompanionStruct_Helpers_ struct { + TraitID_ *TraitID +} + +var Companion_Helpers_ = CompanionStruct_Helpers_{ + TraitID_: &TraitID{}, +} + +func (CompanionStruct_Helpers_) CastTo_(x interface{}) Helpers { + var t Helpers + t, _ = x.(Helpers) + return t +} + +// End of trait Helpers diff --git a/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/dafny/dafny_test.go b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/dafny/dafny_test.go new file mode 100644 index 000000000..8569886d8 --- /dev/null +++ b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/dafny/dafny_test.go @@ -0,0 +1,186 @@ +package dafny + +import "testing" + +func TestArraySequence(t *testing.T) { + arrSeq := MakeArraySequence() + AssertImplementsSequence(arrSeq, t) +} + +func MakeArraySequence() Sequence { + underlying := &arrayStruct{ + contents: []interface{}{}, + dims: []int{0}, + } + arr := GoNativeArray{underlying: underlying} + arrSeq := New_ArraySequence_() + arrSeq.Ctor__(arr, false) + return arrSeq +} + +func TestConcatSequence(t *testing.T) { + left := MakeArraySequence() + right := MakeArraySequence() + + concatSeq := New_ConcatSequence_() + concatSeq.Ctor__(left, right) + + AssertImplementsSequence(concatSeq, t) +} + +func TestLazySequence(t *testing.T) { + arrSeq := MakeArraySequence() + + lazySeq := New_LazySequence_() + lazySeq.Ctor__(arrSeq) + + AssertImplementsSequence(lazySeq, t) +} + +// Test byte sequence optimization using arrayForByte wrapper +func TestByteSequenceOptimization(t *testing.T) { + // Test creating byte sequence from slice + data := []byte{1, 2, 3, 4, 5} + seq := SeqOfBytes(data) + + // Verify it implements Sequence interface + AssertImplementsSequence(seq, t) + + // Verify ToArray returns GoNativeArray + arr := seq.ToArray() + if byteArr, ok := arr.(GoNativeArray); ok { + if byteArr.Length() != 5 { + t.Errorf("Expected length 5, got %d", byteArr.Length()) + } + if byteArr.Select(0).(uint8) != 1 { + t.Errorf("Expected first element 1, got %v", byteArr.Select(0)) + } + } else { + t.Errorf("Expected GoNativeArray, got %T", arr) + } +} + +// Test optimization detection for uint8 vs non-uint8 +func TestSeqOf(t *testing.T) { + // Test uint8 slice - should optimize + uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} + seq := SeqOf(uint8Contents...) + if !SequenceIsBackedByByteArray(seq) { + t.Error("Expected optimization for uint8 slice") + } + + // Verify it returns GoNativeArray + arr := seq.ToArray() + if _, ok := arr.(GoNativeArray); !ok { + t.Errorf("Expected GoNativeArray, got %T", arr) + } + + // Test non-uint8 slice - should not optimize + intContents := []interface{}{1, 2, 3} + seq2 := SeqOf(intContents...) + if SequenceIsBackedByByteArray(seq2) { + t.Error("Expected no optimization for int slice") + } + + // Test empty slice - should not optimize + emptyContents := []interface{}{} + seq3 := SeqOf(emptyContents...) + if SequenceIsBackedByByteArray(seq3) { + t.Error("Expected no optimization for empty slice") + } +} + +func TestSeqFromArray(t *testing.T) { + // Test uint8 slice - should not optimize + // (in fact it should use the array without copying) + uint8Contents := []interface{}{uint8(1), uint8(2), uint8(3)} + seq := SeqFromArray(uint8Contents, false) + if SequenceIsBackedByByteArray(seq) { + t.Error("Expected no optimization for int slice") + } + + // Mutate the array (exactly as you're not supposed to :) + // and check the sequence changes. + uint8Contents[1] = uint8(42) + if seq.Select(1) != uint8(42) { + t.Errorf("Expected element at index 1 to be 42, got %v", seq.Select(1)) + } +} + +// Test refactored CompanionStruct_NativeArray_ functions +func TestNativeArrayFunctions(t *testing.T) { + // Test Make function + arr := Companion_NativeArray_.Make(3) + if goArr, ok := arr.(GoNativeArray); ok { + if goArr.Length() != 3 { + t.Errorf("Expected length 3, got %d", goArr.Length()) + } + } else { + t.Errorf("Expected GoNativeArray, got %T", arr) + } + + // Test MakeWithInit function + initFunc := func(i uint32) interface{} { return int(i * 2) } + arr2 := Companion_NativeArray_.MakeWithInit(3, initFunc) + if goArr2, ok := arr2.(GoNativeArray); ok { + if goArr2.Length() != 3 { + t.Errorf("Expected length 3, got %d", goArr2.Length()) + } + if goArr2.Select(1) != 2 { + t.Errorf("Expected element at index 1 to be 2, got %v", goArr2.Select(1)) + } + } else { + t.Errorf("Expected GoNativeArray, got %T", arr2) + } + + // Test Copy function with GoNativeArray + arr3 := Companion_NativeArray_.Copy(arr2.(GoNativeArray)) + if goArr3, ok := arr3.(GoNativeArray); ok { + if goArr3.Length() != 3 { + t.Errorf("Expected length 3, got %d", goArr3.Length()) + } + if goArr3.Select(1) != 2 { + t.Errorf("Expected element at index 1 to be 2, got %v", goArr3.Select(1)) + } + } else { + t.Errorf("Expected GoNativeArray, got %T", arr3) + } + + // Test Copy function with GoNativeArray + data := []byte{10, 20, 30} + byteSeq := SeqOfBytes(data) + byteArr := byteSeq.ToArray() + arr4 := Companion_NativeArray_.Copy(byteArr) + if byteArr4, ok := arr4.(GoNativeArray); ok { + if byteArr4.Length() != 3 { + t.Errorf("Expected length 3, got %d", byteArr4.Length()) + } + if byteArr4.Select(1).(uint8) != 20 { + t.Errorf("Expected element at index 1 to be 20, got %v", byteArr4.Select(1)) + } + } else { + t.Errorf("Expected GoNativeArray, got %T", arr4) + } +} + +func TestArrayCopy(t *testing.T) { + arr := NewArray(Five) + copy := arr.arrayCopy() + if arr.(EqualsGeneric).EqualsGeneric(copy) { + t.Errorf("Expected array to not compare EqualsGeneric to its copy") + } +} + +func AssertImplementsSequence(s interface{}, t *testing.T) { + _, ok := s.(Sequence) + if !ok { + t.Errorf("Expected %v to implement the Sequence interface", s) + } +} + +func SequenceIsBackedByByteArray(seq Sequence) bool { + _, ok := seq.(*ArraySequence)._values.(GoNativeArray).underlying.(*arrayForByte) + return ok +} + + diff --git a/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/go.mod b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/go.mod new file mode 100644 index 000000000..113f3e903 --- /dev/null +++ b/esdk-performance-testing/benchmarks/go/DafnyRuntimeGo/v4/go.mod @@ -0,0 +1,3 @@ +module github.com/dafny-lang/DafnyRuntimeGo/v4 + +go 1.21 diff --git a/esdk-performance-testing/benchmarks/go/go.mod b/esdk-performance-testing/benchmarks/go/go.mod index 0d27d8fe6..330f552fe 100644 --- a/esdk-performance-testing/benchmarks/go/go.mod +++ b/esdk-performance-testing/benchmarks/go/go.mod @@ -56,3 +56,5 @@ require ( golang.org/x/sys v0.15.0 // indirect golang.org/x/term v0.14.0 // indirect ) + +replace github.com/dafny-lang/DafnyRuntimeGo/v4 => ./DafnyRuntimeGo/v4 diff --git a/esdk-performance-testing/benchmarks/go/go.sum b/esdk-performance-testing/benchmarks/go/go.sum index 4ecd94240..4a61ff9bb 100644 --- a/esdk-performance-testing/benchmarks/go/go.sum +++ b/esdk-performance-testing/benchmarks/go/go.sum @@ -30,8 +30,6 @@ github.com/aws/aws-sdk-go-v2/service/sts v1.38.0 h1:iV1Ko4Em/lkJIsoKyGfc0nQySi+v github.com/aws/aws-sdk-go-v2/service/sts v1.38.0/go.mod h1:bEPcjW7IbolPfK67G1nilqWyoxYMSPrDiIQ3RdIdKgo= github.com/aws/smithy-go v1.22.5 h1:P9ATCXPMb2mPjYBgueqJNCA5S9UfktsW0tTxi+a7eqw= github.com/aws/smithy-go v1.22.5/go.mod h1:t1ufH5HMublsJYulve2RKmHDC15xu1f26kHCp/HgceI= -github.com/dafny-lang/DafnyRuntimeGo/v4 v4.11.1 h1:tTQ9M9HCUaf2SXqutj2vmMqJKJpefWMSqx1niqTqi8M= -github.com/dafny-lang/DafnyRuntimeGo/v4 v4.11.1/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto= github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38= github.com/davecgh/go-spew v1.1.1 h1:vj9j/u1bqnvCEfJOwUhtlOARqs3+rkHYY13jYWTU97c= github.com/davecgh/go-spew v1.1.1/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38=