Add tests

Test/git-issues/git-issue-3883.dfy

@@ -17,6 +17,10 @@ method Main() {
  TestOthers();
 
  DoIt<real>();
+
+ Arrows();
+
+ MoreTests.Placebo();
 }
 
 method TestMyTest<U>(m: MyType<U>, u: U) {
@@ -38,17 +42,53 @@ method TestOthers() {
  print a, " ", b, " ", c, "\n"; // 10 null [false, true, false]
 }
 
-type ST0<T, U(0)> = x: int | x % 5 == 0
+type ST0<T, U(0)> = x: int | x % 5 == 1 witness 16
 type ST1<T, U(0)> = x: int | (if var m: map<T,U> := map[]; m == map[] then 0 else 8) <= x
 
 method DoIt<X(0)>() {
  var t0: ST0<int, X>;
  var t1: ST1<int, X>;
- Print(t0, " "); // 0-0
+ Print(t0, " "); // 16-16
  Print(t1, "\n"); // 0-0
 }
 
 method Print<X(0)>(x: X, suffix: string) {
  var y: X;
  print x, "-", y, suffix;
 }
+
+type pos = x | 1 <= x witness 9
+type Fn<R(0)> = f: int -> R | true witness *
+
+method Arrows() {
+ var f: Fn<int>;
+ var g: Fn<pos>;
+}
+
+module MoreTests {
+ datatype BSingle<X> = BPlop(bool)
+ type BMyTypeWrapper<T> = x: BSingle<T> | true witness *
+ datatype BD = BD(BMyTypeWrapper<int>)
+
+ datatype XSingle<X> = XPlop(X)
+ type XMyTypeWrapper<T> = x: XSingle<T> | true witness *
+ datatype XD = XD(XMyTypeWrapper<int>)
+
+ datatype IntCell = IntCell(int)
+ type ConstrainedIntCell = c: IntCell | true witness *
+ type GurgleInt = ConstrainedIntCell
+ datatype WrappedInt = WrappedInt(GurgleInt)
+ type MyTypeAroundInt<T> = x: WrappedInt | true witness *
+
+ datatype UCell<U> = UCell(U)
+ type ConstrainedUCell<U> = u: UCell<U> | true witness *
+ type GurgleU<U> = ConstrainedUCell<U>
+ datatype WrappedU<U> = WrappedU(GurgleU<U>)
+ type MyTypeAroundU<U> = x: WrappedU<U> | true witness *
+
+ method Placebo() {
+ var a: XSingle<int>;
+ var b: XMyTypeWrapper<int>;
+ var c: XD;
+ }
+}

Test/git-issues/git-issue-3883.dfy.expect

@@ -3,4 +3,4 @@ true false
 13 true
 18 19
 10 null [false, true, false]
-0-0 0-0
+16-16 0-0