From b9ceb8d3d48ae7c8beb8070db134294ba8bd964f Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Tue, 9 Aug 2022 10:44:22 -0700
Subject: [PATCH] Changes from
 https://github.com/dafny-lang/libraries-without-variance/pull/1

---
 src/Unicode/Utf16EncodingForm.dfy |  9 +++++++--
 src/Unicode/Utf8EncodingForm.dfy  | 15 +++++++++++----
 src/Wrappers.dfy                  | 14 ++++++++++++++
 3 files changed, 32 insertions(+), 6 deletions(-)

diff --git a/src/Unicode/Utf16EncodingForm.dfy b/src/Unicode/Utf16EncodingForm.dfy
index a8bccd0f..13466693 100644
--- a/src/Unicode/Utf16EncodingForm.dfy
+++ b/src/Unicode/Utf16EncodingForm.dfy
@@ -58,8 +58,13 @@ module Utf16EncodingForm refines UnicodeEncodingForm {
       && prefix == s[..|prefix|]
       && IsMinimalWellFormedCodeUnitSubsequence(prefix)
   {
-    if |s| >= 1 && IsWellFormedSingleCodeUnitSequence(s[..1]) then Some(s[..1])
-    else if |s| >= 2 && IsWellFormedDoubleCodeUnitSequence(s[..2]) then Some(s[..2])
+    // Attaching the subset types explicitly to work around
+    // type inference not picking them (unless Option<T> is declared as Option<+T>).
+    // BUG(https://github.com/dafny-lang/dafny/issues/2551)
+    if |s| >= 1 && IsWellFormedSingleCodeUnitSequence(s[..1]) then
+      var r: MinimalWellFormedCodeUnitSeq := s[..1]; Some(r)
+    else if |s| >= 2 && IsWellFormedDoubleCodeUnitSequence(s[..2]) then
+      var r: MinimalWellFormedCodeUnitSeq := s[..2]; Some(r)
     else None
   }
 
diff --git a/src/Unicode/Utf8EncodingForm.dfy b/src/Unicode/Utf8EncodingForm.dfy
index f6409ac7..5a72ca53 100644
--- a/src/Unicode/Utf8EncodingForm.dfy
+++ b/src/Unicode/Utf8EncodingForm.dfy
@@ -106,10 +106,17 @@ module Utf8EncodingForm refines UnicodeEncodingForm {
   function method SplitPrefixMinimalWellFormedCodeUnitSubsequence(s: CodeUnitSeq):
     (maybePrefix: Option<MinimalWellFormedCodeUnitSeq>)
   {
-    if |s| >= 1 && IsWellFormedSingleCodeUnitSequence(s[..1]) then Some(s[..1])
-    else if |s| >= 2 && IsWellFormedDoubleCodeUnitSequence(s[..2]) then Some(s[..2])
-    else if |s| >= 3 && IsWellFormedTripleCodeUnitSequence(s[..3]) then Some(s[..3])
-    else if |s| >= 4 && IsWellFormedQuadrupleCodeUnitSequence(s[..4]) then Some(s[..4])
+    // Attaching the subset types explicitly to work around
+    // type inference not picking it (unless Option<T> is declared as Option<+T>).
+    // BUG(https://github.com/dafny-lang/dafny/issues/2551)
+    if |s| >= 1 && IsWellFormedSingleCodeUnitSequence(s[..1]) then 
+      var r: MinimalWellFormedCodeUnitSeq := s[..1]; Some(r)
+    else if |s| >= 2 && IsWellFormedDoubleCodeUnitSequence(s[..2]) then
+      var r: MinimalWellFormedCodeUnitSeq := s[..2]; Some(r)
+    else if |s| >= 3 && IsWellFormedTripleCodeUnitSequence(s[..3]) then
+      var r: MinimalWellFormedCodeUnitSeq := s[..3]; Some(r)
+    else if |s| >= 4 && IsWellFormedQuadrupleCodeUnitSequence(s[..4]) then
+      var r: MinimalWellFormedCodeUnitSeq := s[..4]; Some(r)
     else None
   }
 
diff --git a/src/Wrappers.dfy b/src/Wrappers.dfy
index ddb9b7f3..a889fe3b 100644
--- a/src/Wrappers.dfy
+++ b/src/Wrappers.dfy
@@ -35,6 +35,13 @@ module Wrappers {
     {
       value
     }
+
+    function method Map<NewT>(reWrap: T -> NewT): Option<NewT>
+    {
+      match this
+      case Some(v) => Some(reWrap(v))
+      case None => None
+    }
   }
 
   datatype Result<+T, +R> = | Success(value: T) | Failure(error: R) {
@@ -62,6 +69,13 @@ module Wrappers {
       Failure(this.error)
     }
 
+    function method MapSuccess<NewT>(reWrap: T -> NewT): Result<NewT, R>
+    {
+      match this
+      case Success(s) => Success(reWrap(s))
+      case Failure(e) => Failure(e)
+    }
+
     function method MapFailure<NewR>(reWrap: R -> NewR): Result<T, NewR>
     {
       match this