Open robin-aws opened 1 year ago
Follow-up from #49, which will close #39 but uses my quick-and-dirty-but-correct MergeSort from https://github.com/dafny-lang/dafny-reportgenerator/blob/main/src/StandardLibrary.dfy#L38. That code is actually very inefficient at runtime because it relies on s[..1] slices which currently impose a full copy.
s[..1]
I'd personally be happy with anything based on arrays instead of sequences, but as per #39 https://en.wikipedia.org/wiki/Timsort may be an even better option.
See also: https://github.com/dafny-lang/compiler-bootstrap/blob/28299a21101342e5384664c71103c562ad707a80/src/Utils/Lib.Sort.dfy#L357
robin-aws
commented
1 year ago
Follow-up from #49, which will close #39 but uses my quick-and-dirty-but-correct MergeSort from https://github.com/dafny-lang/dafny-reportgenerator/blob/main/src/StandardLibrary.dfy#L38. That code is actually very inefficient at runtime because it relies on
s[..1]slices which currently impose a full copy.I'd personally be happy with anything based on arrays instead of sequences, but as per #39 https://en.wikipedia.org/wiki/Timsort may be an even better option.