Add Seq.MapPartialFunction and restore proofs

dafny-lang · Dec 25, 2024 · 64374b3 · 64374b3
1 parent 8cf5e3a
commit 64374b3
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 8 deletions.
diff --git a/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy b/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy
@@ -717,7 +717,7 @@ module Std.Collections.Seq {
 
   /* Returns the sequence one obtains by applying a function to every element
      of a sequence. */
-  opaque function Map<T, R>(f: (T ~> R), xs: seq<T>): (result: seq<R>)
+  opaque function Map<T, R>(f: T ~> R, xs: seq<T>): (result: seq<R>)
     requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i])
     ensures |result| == |xs|
     ensures forall i {:trigger result[i]} :: 0 <= i < |xs| ==> result[i] == f(xs[i])
@@ -727,6 +727,12 @@ module Std.Collections.Seq {
     else [f(xs[0])] + Map(f, xs[1..])
   }
 
+  function MapPartialFunction<T, R>(f: T --> R, xs: seq<T>): (result: seq<R>)
+    requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i])
+  {
+    Map(f, xs)
+  }
+
   /* Applies a function to every element of a sequence, returning a Result value (which is a
      failure-compatible type). Returns either a failure, or, if successful at every element,
      the transformed sequence.  */

diff --git a/Source/DafnyStandardLibraries/src/Std/Unicode/UnicodeEncodingForm.dfy b/Source/DafnyStandardLibraries/src/Std/Unicode/UnicodeEncodingForm.dfy
@@ -275,7 +275,7 @@ abstract module Std.Unicode.UnicodeEncodingForm {
     s := [];
     ghost var unflattened: seq<MinimalWellFormedCodeUnitSeq> := [];
     for i := |vs| downto 0
-      invariant unflattened == Seq.Map(EncodeScalarValue, vs[i..])
+      invariant unflattened == Seq.MapPartialFunction(EncodeScalarValue, vs[i..])
       invariant s == Seq.Flatten(unflattened)
     {
       var next: MinimalWellFormedCodeUnitSeq := EncodeScalarValue(vs[i]);
@@ -292,12 +292,12 @@ abstract module Std.Unicode.UnicodeEncodingForm {
     ensures EncodeScalarSequence(vs) == s
   {
     var parts := PartitionCodeUnitSequence(s);
-    var vs := Seq.Map(DecodeMinimalWellFormedCodeUnitSubsequence, parts);
+    var vs := Seq.MapPartialFunction(DecodeMinimalWellFormedCodeUnitSubsequence, parts);
     calc == {
       s;
       Seq.Flatten(parts);
-      { assert parts == Seq.Map(EncodeScalarValue, vs); }
-      Seq.Flatten(Seq.Map(EncodeScalarValue, vs));
+      { assert parts == Seq.MapPartialFunction(EncodeScalarValue, vs); }
+      Seq.Flatten(Seq.MapPartialFunction(EncodeScalarValue, vs));
       EncodeScalarSequence(vs);
     }
     vs
@@ -324,12 +324,12 @@ abstract module Std.Unicode.UnicodeEncodingForm {
       return None;
     }
     var parts := maybeParts.value;
-    var vs := Seq.Map(DecodeMinimalWellFormedCodeUnitSubsequence, parts);
+    var vs := Seq.MapPartialFunction(DecodeMinimalWellFormedCodeUnitSubsequence, parts);
     calc == {
       s;
       Seq.Flatten(parts);
-      { assert parts == Seq.Map(EncodeScalarValue, vs); }
-      Seq.Flatten(Seq.Map(EncodeScalarValue, vs));
+      { assert parts == Seq.MapPartialFunction(EncodeScalarValue, vs); }
+      Seq.Flatten(Seq.MapPartialFunction(EncodeScalarValue, vs));
       EncodeScalarSequence(vs);
     }
     return Some(vs);