tests/test_foreach.mlw

   1 use int.Int
   2
   3 scope Constant
   4   let create () : unit = ()
   5   exception Done
   6   let next () : (r:int)
   7     ensures { r = 42 } =
   8     42
   9 end
  10
  11 let test_Constant () =
  12   for x in () with Constant do
  13     variant { 0 }
  14     assert { x =  42 };
  15     if x = 42 then break
  16   done
  17
  18 use array.Array
  19
  20 scope A
  21   type t 'a = private {
  22     a: array 'a;
  23     mutable index: int; (* next index *)
  24   }
  25   invariant { 0 <= index <= Array.length a }
  26   by { a = Array.make 0 (any 'a); index = 0 }
  27
  28   val create (a: array 'a) : t 'a
  29     ensures { result.a = a }
  30     ensures { result.index = 0 }
  31
  32   exception Done
  33
  34   val next (t: t 'a) : (int, 'a)
  35     writes  { t.index }
  36     raises  { Done -> t.index = old t.index = Array.length t.a }
  37     ensures { old t.index < Array.length t.a }
  38     returns { i, x -> i = old t.index && t.index = i + 1 && x = t.a[i] }
  39 end
  40
  41 let test_A ()
  42 = let a = Array.make 10 1 in
  43   let ref s = 0 in
  44   for _, x in a with A do
  45     invariant { s = it.A.index < 5 }
  46     variant   { 10 - it.A.index }
  47     s <- s + x;
  48     if s = 5 then break
  49   done;
  50   assert { s = 5 }
  51
  52 use list.List
  53 use list.Append
  54 use list.Length
  55
  56 scope L
  57   type t 'a = private {
  58     initial: list 'a;
  59     mutable visited: list 'a;
  60     mutable upcoming: list 'a;
  61   }
  62   invariant { initial = visited ++ upcoming }
  63   by { initial = Nil; visited = Nil; upcoming = Nil }
  64
  65   val create (l: list 'a) : t 'a
  66     ensures { result.initial = result.upcoming = l }
  67
  68   exception Done
  69
  70   val next (t: t 'a) : 'a
  71     writes  { t }
  72     raises  { Done -> t.upcoming = old t.upcoming = Nil }
  73     ensures { match old t.upcoming with
  74               | Nil -> false
  75               | Cons x a -> result = x && t.upcoming = a end }
  76 end
  77
  78 let test_L () =
  79   let l = Cons 1 (Cons 2 (Cons 3 Nil)) in
  80   let ref s = 0 in
  81   for x in l with L do
  82     variant { length it.L.upcoming }
  83     invariant { s = 0 && it.L.upcoming = Cons 1 (Cons 2 (Cons 3 Nil))
  84              || s = 1 && it.L.upcoming =         Cons 2 (Cons 3 Nil)
  85              || s = 3 && it.L.upcoming =                 Cons 3 Nil
  86              || s = 6 && it.L.upcoming =                        Nil }
  87     s <- s + x
  88   done;
  89   assert { s = 6 }