fix: Add missing type characteristics (#154)

* Add missing (!new) for type parameters
* chore: Improve whitespace
* chore: Remove unnecessary parentheses
* chore: Remove deprecated semi-colons
* chore: Remove explicit triggers that do the same as the default triggers
* chore: Show reads clause between requires and ensures
* Make reads clauses more specific
* Remove {:opaque} attribute from lemmas

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 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)
@@ -688,7 +688,7 @@ module {:options "-functionSyntax:4"} Seq {
   /* Filtering a sequence is distributive over concatenation. That is, concatenating two sequences 
      and then using "Filter" is the same as using "Filter" on each sequence separately, and then 
      concatenating the two resulting sequences. */
-  lemma {:opaque} LemmaFilterDistributesOverConcat<T>(f: (T ~> bool), xs: seq<T>, ys: seq<T>)
+  lemma LemmaFilterDistributesOverConcat<T>(f: (T ~> bool), 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 Filter(f, xs + ys) == Filter(f, xs) + Filter(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 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 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);