tests/test_exec.mlw

   1
   2
   3 module M
   4
   5   use int.Int
   6
   7   let x0 () : int = 13 * 3 + 7 - 4
   8
   9   let x1 () : bool = 2 + 2 = 4
  10
  11   use ref.Ref
  12
  13   let x2 () : int =
  14     let x = ref 13 in
  15     if !x <> 3 then 7 else 4
  16
  17   use list.List
  18   use list.Append
  19
  20   let y () : list int =
  21     Cons 12 (Cons 34 (Cons 56 Nil)) ++ Cons 78 (Cons 90 Nil)
  22
  23 end
  24
  25 module Map
  26
  27   use int.Int
  28   use map.Map
  29   use map.Const
  30
  31   exception Found int
  32
  33   let search (t:map int int) (len:int) (v:int) : int =
  34     try
  35       for i=0 to len-1 do
  36         if t[i] = v then raise (Found i)
  37       done;
  38       -1
  39     with Found i -> i
  40     end
  41
  42   constant t : map int int = (const 0)[0 <- 12][1 <- 42][2 <- 67]
  43
  44   let ghost test12 () = search t 3 12
  45   let ghost test42 () = search t 3 42
  46   let ghost test67 () = search t 3 67
  47   let ghost test0 () = search t 3 0
  48
  49 end
  50
  51 module Mut
  52
  53   use int.Int
  54
  55   type t = { mutable a : int; c: int ; mutable b : int }
  56
  57   let e0 () =
  58     let y = { a = 1; c = 43; b = 2 } in
  59     y
  60
  61   let e1 () =
  62     let y = { a = 1; c = 43; b = 2 } in
  63     y.a <- 3;
  64     y.b <- 7;
  65     y
  66
  67   let t0 () =
  68     let y = { a = 1; c = 43; b = 2 } in
  69     y.a + y.b (* should be 3 *)
  70
  71   let t1 () =
  72     let y = { a = 1; c = 43; b = 2 } in
  73     let z = y in
  74     y.a + z.b (* should be 3 *)
  75
  76   let t2 () =
  77     let y = { a = 1; c = 43; b = 2 } in
  78     y.a <- 3;
  79     y.a + y.b (* should be 5 *)
  80
  81   let t3 () =
  82     let y = { a = 1; c = 43; b = 2 } in
  83     let z = y in
  84     z.a <- 3;
  85     y.a (* should be 3 *)
  86
  87   type refint = { mutable i : int }
  88
  89   let y () : refint = { i = 0 }
  90
  91   let z () : int =
  92     let r = { i = 0 } in r.i <- 42; r.i
  93
  94
  95   let test () =
  96     let x = { i = 0 } in
  97     let s = { i = 0 } in
  98     while x.i <= 10 do
  99       variant { 10 - x.i }
 100       s.i <- s.i + x.i;
 101       x.i <- x.i + 1
 102     done;
 103     s.i (* should be 55 *)
 104
 105
 106   let f m : int
 107   = let x = { i = 2 } in
 108     let y = { i = 8 } in
 109     let sum = { i = 0 } in
 110     while x.i <= m do
 111       variant { m - x.i }
 112       let tmp = x.i in
 113       x.i <- y.i;
 114       y.i <- 4 * y.i + tmp;
 115       sum.i <- sum.i + tmp
 116     done;
 117     sum.i
 118
 119   let run1 () = f 10 (* should be 10 *)
 120
 121   let run2 () = f 4000000 (* should be 4613732 *)
 122
 123   (* use of a global mutable variable *)
 124
 125   val x : refint
 126
 127   let j0 () = x.i
 128
 129   let j () = x.i <- 42; x.i
 130
 131 end
 132
 133 module Ref
 134
 135   use ref.Ref
 136
 137   let y () : ref int = { contents = 0 }
 138
 139   let z () : int =
 140     let r = ref 0 in r := 42; !r
 141
 142   use int.Int
 143
 144   let f m : int
 145   = let x = ref 2 in
 146     let y = ref 8 in
 147     let sum = ref 0 in
 148     while !x <= m do
 149       variant { m - !x }
 150       let tmp = !x in
 151       x := !y;
 152       y := 4 * !y + tmp;
 153       sum := !sum + tmp
 154     done;
 155     !sum
 156
 157   let run1 () = f 10 (* should be 10 *)
 158
 159   let run2 () = f 4000000 (* should be 4613732 *)
 160
 161
 162   let g () : int =
 163     for i=1 to 10 do
 164        let x = ref i in
 165        x := !x + 1
 166     done;
 167     42
 168
 169   let rec h n : int
 170     variant { n }
 171   =
 172     let x = ref 0 in
 173     x := !x + 1;
 174     if n = 0 then 0 else h (n-1) + !x
 175
 176   let hh () = h 10
 177
 178   (* use of a global ref *)
 179
 180   val x : ref int
 181
 182   let j () =
 183     x := 42;
 184     !x
 185
 186 end
 187
 188
 189 module Pair
 190
 191   use ref.Ref
 192
 193   type t = { left : ref int ; middle : int; right : ref int }
 194
 195   let a () = { left = ref 13 ; middle = 5; right = ref 42 }
 196
 197   let b () =
 198     let x = a () in
 199     x.left := 57;
 200     x.right := 98;
 201     x
 202
 203   type u = { u1 : t ; u2 : t }
 204
 205   let c () =
 206     let x = { left = ref 1; middle = 2; right = ref 3} in
 207     let y = { left = ref 4; middle = 5; right = ref 6} in
 208     let u = { u1 = x ; u2 = y } in
 209     u.u2.left := 7;
 210     u
 211
 212 end
 213
 214 module Array
 215
 216   use int.Int
 217   use array.Array
 218
 219   exception Found int
 220
 221   let search (t:array int) (v:int) : int =
 222     try
 223       for i=0 to t.length - 1 do
 224         if t[i] = v then raise (Found i)
 225       done;
 226       -1
 227     with Found i -> i
 228     end
 229
 230   let incr (t:array int) : unit =
 231     for i=0 to t.length - 1 do
 232       t[i] <- t[i]+1
 233     done
 234
 235   let test0 () =
 236     let t = Array.make 2 21 in
 237     t[0]+t[1]
 238     (* should be 42 *)
 239
 240   let test1 () =
 241     let t = Array.make 2 21 in
 242     t[1] <- 17;
 243     t[0]+t[1]
 244     (* should be 38 *)
 245
 246   let test2 () =
 247     let t = Array.make 2 21 in
 248     t[1] <- 17;
 249     t[0] <- 7;
 250     t[0]+t[1]
 251     (* should be 24 *)
 252
 253   let t () : array int =
 254      let t = Array.make 3 0 in
 255      t[0] <- 12;
 256      t[1] <- 42;
 257      t[2] <- 67;
 258      t
 259
 260   let t1 () =
 261     let t = t () in
 262     t[0] + t[1] + t[2] (* 121 *)
 263
 264   let i () = incr (t ())
 265
 266   let test12 () = search (t ()) 12
 267   let test42 () = search (t ()) 42
 268   let test67 () = search (t ()) 67
 269   let test7 () = search (t ()) 7
 270
 271
 272   use array.ArraySwap
 273
 274   let test_swap () =
 275      let t = Array.make 3 0 in
 276      t[0] <- 12;
 277      t[1] <- 42;
 278      t[2] <- 67;
 279      swap t 1 2;
 280      t[1] (* 67 *)
 281
 282
 283   let test_loop () =
 284      let t = Array.make 3 0 in
 285      for i=0 to 2 do t[i] <- i done;
 286      t[0] + t[1] + t[2] (* 3 *)
 287
 288   (* global arrays *)
 289
 290   val g : array int
 291
 292   let j () = g[0] <- 42
 293
 294 end