fix: Add missing type characteristics

examples/BinaryOperations.dfy

@@ -161,15 +161,15 @@ module {:options "-functionSyntax:4"} HomomorphismExamples {
   import IntegersExample
   import RealsExample
 
-  lemma IdentityIsHomomorphism<T>(bop: (T, T) -> T)
+  lemma IdentityIsHomomorphism<T(!new)>(bop: (T, T) -> T)
     ensures IsHomomorphism(bop, bop, x => x)
   {}
 
   lemma IntRealEmbeddingIsHomomorphism()
     ensures IsHomomorphism(IntegersExample.add, RealsExample.add, (x: int) => x as real)
   {}
 
-  lemma ConstUnitIsHomomorphism<S,T>(bop1: (S, S) -> S, bop2: (T, T) -> T, unit: T)
+  lemma ConstUnitIsHomomorphism<S(!new), T(!new)>(bop1: (S, S) -> S, bop2: (T, T) -> T, unit: T)
     requires IsUnital(bop2, unit)
     ensures IsHomomorphism(bop1, bop2, x => unit)
   {}

examples/RelationsExamples.dfy

@@ -23,19 +23,19 @@ module {:options "-functionSyntax:4"} RelationsExamples {
     requires n >= 1
     ensures EquivalenceRelation(R)
   {
-    (x, y) => (x % n ==  y % n)
+    (x, y) => x % n ==  y % n
   }
 
   lemma BuiltInIntEqIsEquivalenceRelation()
-    ensures EquivalenceRelation((x: int, y: int) => (x == y))
+    ensures EquivalenceRelation((x: int, y: int) => x == y)
   {}
 
   lemma BuiltInIntGeIsAntiSymmetricRelation()
-    ensures AntiSymmetric((x: int, y: int) => (x >= y))
+    ensures AntiSymmetric((x: int, y: int) => x >= y)
   {}
 
   lemma BuiltInIntLtIsAsymmetricRelation()
-    ensures Asymmetric((x: int, y: int) => (x < y))
+    ensures Asymmetric((x: int, y: int) => x < y)
   {
   }
 
@@ -48,31 +48,31 @@ module {:options "-functionSyntax:4"} RelationsExamples {
   }
 
   lemma BuiltInIntLtIsNotReflexiveRelation()
-    ensures !Reflexive((x: int, y: int) => (x < y))
+    ensures !Reflexive((x: int, y: int) => x < y)
   {
-    var f := (x: int, y: int) => (x < y);
-    assert !f(0,0);
-    assert !forall x: int :: f(x,x);
+    var f := (x: int, y: int) => x < y;
+    assert !f(0, 0);
+    assert !forall x: int :: f(x, x);
     assert !Reflexive(f);
   }
 
   lemma BuiltInIntLtIsIrreflexiveRelation()
-    ensures Irreflexive((x: int, y: int) => (x < y))
+    ensures Irreflexive((x: int, y: int) => x < y)
   {}
 
   lemma BuiltInIntEqIsNotIrreflexiveRelation()
-    ensures !Irreflexive((x: int, y: int) => (x == y))
+    ensures !Irreflexive((x: int, y: int) => x == y)
   {
-    var f := (x: int, y: int) => (x == y);
-    assert f(0,0);
+    var f := (x: int, y: int) => x == y;
+    assert f(0, 0);
     assert !Irreflexive(f);
   }
 
-  lemma AsymmetricIsAntiSymmetric<T>(f: (T,T)->bool)
+  lemma AsymmetricIsAntiSymmetric<T(!new)>(f: (T, T) -> bool)
     ensures Asymmetric(f) ==> AntiSymmetric(f)
   {}
 
-  lemma AsymmetricIsIrreflexive<T>(f: (T,T)->bool)
+  lemma AsymmetricIsIrreflexive<T(!new)>(f: (T, T) -> bool)
     ensures Asymmetric(f) ==> Irreflexive(f)
   {}
 }

src/Collections/Arrays/BinarySearch.dfy

@@ -12,7 +12,7 @@ module BinarySearch {
   import opened Wrappers
   import opened Relations
 
-  method BinarySearch<T>(a: array<T>, key: T, less: (T, T) -> bool) returns (r: Option<nat>)
+  method BinarySearch<T(!new)>(a: array<T>, key: T, less: (T, T) -> bool) returns (r: Option<nat>)
     requires SortedBy(a[..], (x, y) => less(x, y) || x == y)
     requires StrictTotalOrdering(less)
     ensures r.Some? ==> r.value < a.Length && a[r.value] == key

src/Collections/Sequences/MergeSort.dfy

@@ -12,7 +12,7 @@ module {:options "-functionSyntax:4"} Seq.MergeSort {
   import opened Relations
 
   //Splits a sequence in two, sorts the two subsequences using itself, and merge the two sorted sequences using `MergeSortedWith`
-  function MergeSortBy<T>(a: seq<T>, lessThanOrEq: (T, T) -> bool): (result :seq<T>)
+  function MergeSortBy<T(!new)>(a: seq<T>, lessThanOrEq: (T, T) -> bool): (result :seq<T>)
     requires TotalOrdering(lessThanOrEq)
     ensures multiset(a) == multiset(result)
     ensures SortedBy(result, lessThanOrEq)
@@ -31,7 +31,7 @@ module {:options "-functionSyntax:4"} Seq.MergeSort {
       MergeSortedWith(leftSorted, rightSorted, lessThanOrEq)
   }
 
-  function {:tailrecursion} MergeSortedWith<T>(left: seq<T>, right: seq<T>, lessThanOrEq: (T, T) -> bool) : (result :seq<T>)
+  function {:tailrecursion} MergeSortedWith<T(!new)>(left: seq<T>, right: seq<T>, lessThanOrEq: (T, T) -> bool) : (result :seq<T>)
     requires SortedBy(left, lessThanOrEq)
     requires SortedBy(right, lessThanOrEq)
     requires TotalOrdering(lessThanOrEq)

src/Collections/Sequences/Seq.dfy

@@ -385,7 +385,7 @@ module {:options "-functionSyntax:4"} Seq {
   }
 
   /* Unzips a sequence that contains pairs into two separate sequences. */
-  function {:opaque} Unzip<A,B>(xs: seq<(A, B)>): (seq<A>, seq<B>)
+  function {:opaque} Unzip<A, B>(xs: seq<(A, B)>): (seq<A>, seq<B>)
     ensures |Unzip(xs).0| == |Unzip(xs).1| == |xs|
     ensures forall i {:trigger Unzip(xs).0[i]} {:trigger Unzip(xs).1[i]}
               :: 0 <= i < |xs| ==> (Unzip(xs).0[i], Unzip(xs).1[i]) == xs[i]
@@ -397,7 +397,7 @@ module {:options "-functionSyntax:4"} Seq {
   }
 
   /* Zips two sequences of equal length into one sequence that consists of pairs. */
-  function {:opaque} Zip<A,B>(xs: seq<A>, ys: seq<B>): seq<(A, B)>
+  function {:opaque} Zip<A, B>(xs: seq<A>, ys: seq<B>): seq<(A, B)>
     requires |xs| == |ys|
     ensures |Zip(xs, ys)| == |xs|
     ensures forall i {:trigger Zip(xs, ys)[i]} :: 0 <= i < |Zip(xs, ys)| ==> Zip(xs, ys)[i] == (xs[i], ys[i])
@@ -409,7 +409,7 @@ module {:options "-functionSyntax:4"} Seq {
   }
 
   /* Unzipping and zipping a sequence results in the original sequence */
-  lemma LemmaZipOfUnzip<A,B>(xs: seq<(A,B)>)
+  lemma LemmaZipOfUnzip<A, B>(xs: seq<(A, B)>)
     ensures Zip(Unzip(xs).0, Unzip(xs).1) == xs
   {
   }
@@ -617,7 +617,7 @@ module {:options "-functionSyntax:4"} Seq {
 
   /* Returns the sequence one obtains by applying a function to every element 
      of a sequence. */
-  function {:opaque} Map<T,R>(f: (T ~> R), xs: seq<T>): (result: seq<R>)
+  function {:opaque} 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])
@@ -627,14 +627,14 @@ module {:options "-functionSyntax:4"} Seq {
     // more efficient when compiled, allocating the storage for |xs| elements
     // once instead of creating a chain of |xs| single element concatenations.
     seq(|xs|, i requires 0 <= i < |xs| && f.requires(xs[i])
-                reads set i,o | 0 <= i < |xs| && o in f.reads(xs[i]) :: o
+                reads set i, o | 0 <= i < |xs| && o in f.reads(xs[i]) :: o
     => f(xs[i]))
   }
 
   /* 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.  */
-  function {:opaque} MapWithResult<T, R, E>(f: (T ~> Result<R,E>), xs: seq<T>): (result: Result<seq<R>, E>)
+  function {:opaque} MapWithResult<T, R, E>(f: (T ~> Result<R, E>), xs: seq<T>): (result: Result<seq<R>, E>)
     requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i])
     ensures result.Success? ==>
               && |result.value| == |xs|
@@ -653,7 +653,7 @@ module {:options "-functionSyntax:4"} Seq {
   /* Applying a function to a sequence  is distributive over concatenation. That is, concatenating 
      two sequences and then applying Map is the same as applying Map to each sequence separately, 
      and then concatenating the two resulting sequences. */
-  lemma {:opaque} LemmaMapDistributesOverConcat<T,R>(f: (T ~> R), xs: seq<T>, ys: seq<T>)
+  lemma {:opaque} LemmaMapDistributesOverConcat<T, R>(f: (T ~> R), xs: seq<T>, ys: seq<T>)
     requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i])
     requires forall j :: 0 <= j < |ys| ==> f.requires(ys[j])
     ensures Map(f, xs + ys) == Map(f, xs) + Map(f, ys)
@@ -711,7 +711,7 @@ module {:options "-functionSyntax:4"} Seq {
 
   /* Folds a sequence xs from the left (the beginning), by repeatedly acting on the accumulator
      init via the function f. */
-  function {:opaque} FoldLeft<A,T>(f: (A, T) -> A, init: A, xs: seq<T>): A
+  function {:opaque} FoldLeft<A, T>(f: (A, T) -> A, init: A, xs: seq<T>): A
   {
     if |xs| == 0 then init
     else FoldLeft(f, f(init, xs[0]), xs[1..])
@@ -720,7 +720,7 @@ module {:options "-functionSyntax:4"} Seq {
   /* Folding to the left is distributive over concatenation. That is, concatenating two 
      sequences and then folding them to the left, is the same as folding to the left the 
      first sequence and using the result to fold to the left the second sequence. */
-  lemma {:opaque} LemmaFoldLeftDistributesOverConcat<A,T>(f: (A, T) -> A, init: A, xs: seq<T>, ys: seq<T>)
+  lemma {:opaque} LemmaFoldLeftDistributesOverConcat<A, T>(f: (A, T) -> A, init: A, xs: seq<T>, ys: seq<T>)
     requires 0 <= |xs + ys|
     ensures FoldLeft(f, init, xs + ys) == FoldLeft(f, FoldLeft(f, init, xs), ys)
   {
@@ -744,19 +744,19 @@ module {:options "-functionSyntax:4"} Seq {
 
   /* Is true, if inv is an invariant under stp, which is a relational 
      version of the function f passed to fold. */
-  ghost predicate InvFoldLeft<A(!new),B(!new)>(inv: (B, seq<A>) -> bool,
-                                               stp: (B, A, B) -> bool)
+  ghost predicate InvFoldLeft<A(!new), B(!new)>(inv: (B, seq<A>) -> bool,
+                                                stp: (B, A, B) -> bool)
   {
     forall x: A, xs: seq<A>, b: B, b': B ::
       inv(b, [x] + xs) && stp(b, x, b') ==> inv(b', xs)
   }
 
   /* inv(b, xs) ==> inv(FoldLeft(f, b, xs), []). */
-  lemma LemmaInvFoldLeft<A,B>(inv: (B, seq<A>) -> bool,
-                              stp: (B, A, B) -> bool,
-                              f: (B, A) -> B,
-                              b: B,
-                              xs: seq<A>)
+  lemma LemmaInvFoldLeft<A(!new), B(!new)>(inv: (B, seq<A>) -> bool,
+                                           stp: (B, A, B) -> bool,
+                                           f: (B, A) -> B,
+                                           b: B,
+                                           xs: seq<A>)
     requires InvFoldLeft(inv, stp)
     requires forall b, a :: stp(b, a, f(b, a))
     requires inv(b, xs)
@@ -772,7 +772,7 @@ module {:options "-functionSyntax:4"} Seq {
 
   /* Folds a sequence xs from the right (the end), by acting on the accumulator init via the 
      function f. */
-  function {:opaque} FoldRight<A,T>(f: (T, A) -> A, xs: seq<T>, init: A): A
+  function {:opaque} FoldRight<A, T>(f: (T, A) -> A, xs: seq<T>, init: A): A
   {
     if |xs| == 0 then init
     else f(xs[0], FoldRight(f, xs[1..], init))
@@ -781,7 +781,7 @@ module {:options "-functionSyntax:4"} Seq {
   /* Folding to the right is (contravariantly) distributive over concatenation. That is, concatenating
      two sequences and then folding them to the right, is the same as folding to the right 
      the second sequence and using the result to fold to the right the first sequence. */
-  lemma {:opaque} LemmaFoldRightDistributesOverConcat<A,T>(f: (T, A) -> A, init: A, xs: seq<T>, ys: seq<T>)
+  lemma {:opaque} LemmaFoldRightDistributesOverConcat<A, T>(f: (T, A) -> A, init: A, xs: seq<T>, ys: seq<T>)
     requires 0 <= |xs + ys|
     ensures FoldRight(f, xs + ys, init) == FoldRight(f, xs, FoldRight(f, ys, init))
   {
@@ -802,19 +802,19 @@ module {:options "-functionSyntax:4"} Seq {
 
   /* Is true, if inv is an invariant under stp, which is a relational version
      of the function f passed to fold. */
-  ghost predicate InvFoldRight<A(!new),B(!new)>(inv: (seq<A>, B) -> bool,
-                                                stp: (A, B, B) -> bool)
+  ghost predicate InvFoldRight<A(!new), B(!new)>(inv: (seq<A>, B) -> bool,
+                                                 stp: (A, B, B) -> bool)
   {
     forall x: A, xs: seq<A>, b: B, b': B ::
       inv(xs, b) && stp(x, b, b') ==> inv(([x] + xs), b')
   }
 
   /* inv([], b) ==> inv(xs, FoldRight(f, xs, b)) */
-  lemma LemmaInvFoldRight<A,B>(inv: (seq<A>, B) -> bool,
-                               stp: (A, B, B) -> bool,
-                               f: (A, B) -> B,
-                               b: B,
-                               xs: seq<A>)
+  lemma LemmaInvFoldRight<A(!new), B(!new)>(inv: (seq<A>, B) -> bool,
+                                            stp: (A, B, B) -> bool,
+                                            f: (A, B) -> B,
+                                            b: B,
+                                            xs: seq<A>)
     requires InvFoldRight(inv, stp)
     requires forall a, b :: stp(a, b, f(a, b))
     requires inv([], b)
@@ -828,7 +828,7 @@ module {:options "-functionSyntax:4"} Seq {
   }
 
   /* Optimized implementation of Flatten(Map(f, xs)). */
-  function FlatMap<T,R>(f: (T ~> seq<R>), xs: seq<T>): (result: seq<R>)
+  function FlatMap<T, R>(f: (T ~> seq<R>), xs: seq<T>): (result: seq<R>)
     requires forall i :: 0 <= i < |xs| ==> f.requires(xs[i])
     reads set i, o | 0 <= i < |xs| && o in f.reads(xs[i]) :: o
   {
@@ -876,7 +876,7 @@ module {:options "-functionSyntax:4"} Seq {
   }
 
   /* Proves that any two sequences that are sorted by a total order and that have the same elements are equal. */
-  lemma SortedUnique<T>(xs: seq<T>, ys: seq<T>, R: (T, T) -> bool)
+  lemma SortedUnique<T(!new)>(xs: seq<T>, ys: seq<T>, R: (T, T) -> bool)
     requires SortedBy(xs, R)
     requires SortedBy(ys, R)
     requires TotalOrdering(R)
@@ -896,7 +896,7 @@ module {:options "-functionSyntax:4"} Seq {
   }
 
   /* Converts a set to a sequence that is ordered w.r.t. a given total order. */
-  function SetToSortedSeq<T>(s: set<T>, R: (T, T) -> bool): (xs: seq<T>)
+  function SetToSortedSeq<T(!new)>(s: set<T>, R: (T, T) -> bool): (xs: seq<T>)
     requires TotalOrdering(R)
     ensures multiset(s) == multiset(xs)
     ensures SortedBy(xs, R)

src/Collections/Sets/Isets.dfy

@@ -27,10 +27,10 @@ module {:options "-functionSyntax:4"} Isets {
   }
 
   /* Map an injective function to each element of an iset. */
-  ghost function {:opaque} Map<X(!new), Y>(xs: iset<X>, f: X-->Y): (ys: iset<Y>)
-    reads f.reads
-    requires forall x {:trigger f.requires(x)} :: f.requires(x)
+  ghost function {:opaque} Map<X(!new), Y>(xs: iset<X>, f: X --> Y): (ys: iset<Y>)
+    requires forall x :: f.requires(x)
     requires Injective(f)
+    reads f.reads
     ensures forall x {:trigger f(x)} :: x in xs <==> f(x) in ys
   {
     var ys := iset x | x in xs :: f(x);
@@ -39,9 +39,9 @@ module {:options "-functionSyntax:4"} Isets {
 
   /* Construct an iset using elements of another set for which a function
   returns true. */
-  ghost function {:opaque} Filter<X(!new)>(xs: iset<X>, f: X~>bool): (ys: iset<X>)
-    reads f.reads
-    requires forall x {:trigger f.requires(x)} {:trigger x in xs} :: x in xs ==> f.requires(x)
+  ghost function {:opaque} Filter<X(!new)>(xs: iset<X>, f: X ~> bool): (ys: iset<X>)
+    requires forall x :: x in xs ==> f.requires(x)
+    reads set x, o | x in xs && o in f.reads(x) :: o
     ensures forall y {:trigger f(y)}{:trigger y in xs} :: y in ys <==> y in xs && f(y)
   {
     var ys := iset x | x in xs && f(x);

src/Collections/Sets/Sets.dfy

@@ -123,8 +123,8 @@ module {:options "-functionSyntax:4"} Sets {
 
   /* If an injective function is applied to each element of a set to construct
   another set, the two sets have the same size. */
-  lemma LemmaMapSize<X(!new), Y>(xs: set<X>, ys: set<Y>, f: X-->Y)
-    requires forall x {:trigger f.requires(x)} :: f.requires(x)
+  lemma LemmaMapSize<X(!new), Y>(xs: set<X>, ys: set<Y>, f: X --> Y)
+    requires forall x :: f.requires(x)
     requires Injective(f)
     requires forall x {:trigger f(x)} :: x in xs <==> f(x) in ys
     requires forall y {:trigger y in ys} :: y in ys ==> exists x :: x in xs && y == f(x)
@@ -139,10 +139,10 @@ module {:options "-functionSyntax:4"} Sets {
   }
 
   /* Map an injective function to each element of a set. */
-  function {:opaque} Map<X(!new), Y>(xs: set<X>, f: X-->Y): (ys: set<Y>)
-    reads f.reads
-    requires forall x {:trigger f.requires(x)} :: f.requires(x)
+  function {:opaque} Map<X(!new), Y>(xs: set<X>, f: X --> Y): (ys: set<Y>)
+    requires forall x :: f.requires(x)
     requires Injective(f)
+    reads f.reads
     ensures forall x {:trigger f(x)} :: x in xs <==> f(x) in ys
     ensures |xs| == |ys|
   {
@@ -154,8 +154,8 @@ module {:options "-functionSyntax:4"} Sets {
   /* If a set ys is constructed using elements of another set xs for which a
   function returns true, the size of ys is less than or equal to the size of
   xs. */
-  lemma LemmaFilterSize<X>(xs: set<X>, ys: set<X>, f: X~>bool)
-    requires forall x {:trigger f.requires(x)}{:trigger x in xs} :: x in xs ==> f.requires(x)
+  lemma LemmaFilterSize<X>(xs: set<X>, ys: set<X>, f: X ~> bool)
+    requires forall x :: x in xs ==> f.requires(x)
     requires forall y {:trigger f(y)}{:trigger y in xs} :: y in ys ==> y in xs && f(y)
     ensures |ys| <= |xs|
     decreases xs, ys
@@ -170,9 +170,9 @@ module {:options "-functionSyntax:4"} Sets {
 
   /* Construct a set using elements of another set for which a function returns
   true. */
-  function {:opaque} Filter<X(!new)>(xs: set<X>, f: X~>bool): (ys: set<X>)
-    reads f.reads
-    requires forall x {:trigger f.requires(x)} {:trigger x in xs} :: x in xs ==> f.requires(x)
+  function {:opaque} Filter<X(!new)>(xs: set<X>, f: X ~> bool): (ys: set<X>)
+    requires forall x :: x in xs ==> f.requires(x)
+    reads set x, o | x in xs && o in f.reads(x) :: o
     ensures forall y {:trigger f(y)}{:trigger y in xs} :: y in ys <==> y in xs && f(y)
     ensures |ys| <= |xs|
   {
@@ -206,7 +206,7 @@ module {:options "-functionSyntax:4"} Sets {
   /* Construct a set with all integers in the range [a, b). */
   function {:opaque} SetRange(a: int, b: int): (s: set<int>)
     requires a <= b
-    ensures forall i {:trigger i in s} :: a <= i < b <==> i in s
+    ensures forall i :: a <= i < b <==> i in s
     ensures |s| == b - a
     decreases b - a
   {
@@ -216,7 +216,7 @@ module {:options "-functionSyntax:4"} Sets {
   /* Construct a set with all integers in the range [0, n). */
   function {:opaque} SetRangeZeroBound(n: int): (s: set<int>)
     requires n >= 0
-    ensures forall i {:trigger i in s} :: 0 <= i < n <==> i in s
+    ensures forall i :: 0 <= i < n <==> i in s
     ensures |s| == n
   {
     SetRange(0, n)
@@ -225,7 +225,7 @@ module {:options "-functionSyntax:4"} Sets {
   /* If a set solely contains integers in the range [a, b), then its size is
   bounded by b - a. */
   lemma LemmaBoundedSetSize(x: set<int>, a: int, b: int)
-    requires forall i {:trigger i in x} :: i in x ==> a <= i < b
+    requires forall i :: i in x ==> a <= i < b
     requires a <= b
     ensures |x| <= b - a
   {