test_exec.mlw 4.72 KB
Newer Older
1 2 3 4


module M

5
  use int.Int
6

7 8 9
  let x0 () : int = 13 * 3 + 7 - 4

  let x1 () : bool = 2 + 2 = 4
10

11
  use ref.Ref
MARCHE Claude's avatar
MARCHE Claude committed
12

13
  let x2 () : int =
MARCHE Claude's avatar
MARCHE Claude committed
14 15 16
    let x = ref 13 in
    if !x <> 3 then 7 else 4

17 18
  use list.List
  use list.Append
19

20
  let y () : list int =
21 22
    Cons 12 (Cons 34 (Cons 56 Nil)) ++ Cons 78 (Cons 90 Nil)

23 24 25 26
end

module Map

27 28 29
  use int.Int
  use map.Map
  use map.Const
30 31 32 33 34 35 36 37 38 39 40 41 42 43

  exception Found int

  let search (t:map int int) (len:int) (v:int) : int =
    try
      for i=0 to len-1 do
        if t[i] = v then raise (Found i)
      done;
      -1
    with Found i -> i
    end

  constant t : map int int = (const 0)[0 <- 12][1 <- 42][2 <- 67]

44 45 46 47
  let ghost test12 () = search t 3 12
  let ghost test42 () = search t 3 42
  let ghost test67 () = search t 3 67
  let ghost test0 () = search t 3 0
48 49 50

end

51 52
module Mut

53
  use int.Int
54 55 56 57 58 59 60 61 62 63

  type t = { mutable a : int; c: int ; mutable b : int }

  let e0 () =
    let y = { a = 1; c = 43; b = 2 } in
    y

  let e1 () =
    let y = { a = 1; c = 43; b = 2 } in
    y.a <- 3;
64
    y.b <- 7;
65 66 67 68
    y

  let t0 () =
    let y = { a = 1; c = 43; b = 2 } in
69
    y.a + y.b (* should be 3 *)
70 71 72 73

  let t1 () =
    let y = { a = 1; c = 43; b = 2 } in
    let z = y in
74
    y.a + z.b (* should be 3 *)
75 76 77 78

  let t2 () =
    let y = { a = 1; c = 43; b = 2 } in
    y.a <- 3;
79
    y.a + y.b (* should be 5 *)
80

81 82
  let t3 () =
    let y = { a = 1; c = 43; b = 2 } in
83 84
    let z = y in
    z.a <- 3;
85
    y.a (* should be 3 *)
86

87 88
  type refint = { mutable i : int }

89 90 91 92 93 94
  let y () : refint = { i = 0 }

  let z () : int =
    let r = { i = 0 } in r.i <- 42; r.i


95 96 97 98
  let test () =
    let x = { i = 0 } in
    let s = { i = 0 } in
    while x.i <= 10 do
99
      variant { 10 - x.i }
100 101 102
      s.i <- s.i + x.i;
      x.i <- x.i + 1
    done;
103
    s.i (* should be 55 *)
104 105 106 107 108 109 110


  let f m : int
  = let x = { i = 2 } in
    let y = { i = 8 } in
    let sum = { i = 0 } in
    while x.i <= m do
111
      variant { m - x.i }
112 113 114 115
      let tmp = x.i in
      x.i <- y.i;
      y.i <- 4 * y.i + tmp;
      sum.i <- sum.i + tmp
116
    done;
117 118 119 120 121 122
    sum.i

  let run1 () = f 10 (* should be 10 *)

  let run2 () = f 4000000 (* should be 4613732 *)

123
  (* use of a global mutable variable *)
124 125 126

  val x : refint

127 128 129
  let j0 () = x.i

  let j () = x.i <- 42; x.i
130

131 132
end

133 134
module Ref

135
  use ref.Ref
136

137
  let y () : ref int = { contents = 0 }
138 139 140 141

  let z () : int =
    let r = ref 0 in r := 42; !r

142
  use int.Int
143 144 145 146 147 148

  let f m : int
  = let x = ref 2 in
    let y = ref 8 in
    let sum = ref 0 in
    while !x <= m do
149
      variant { m - !x }
150 151 152 153 154 155 156 157 158 159 160
      let tmp = !x in
      x := !y;
      y := 4 * !y + tmp;
      sum := !sum + tmp
    done;
    !sum

  let run1 () = f 10 (* should be 10 *)

  let run2 () = f 4000000 (* should be 4613732 *)

161

162 163 164 165 166 167 168
  let g () : int =
    for i=1 to 10 do
       let x = ref i in
       x := !x + 1
    done;
    42

169 170 171
  let rec h n : int
    variant { n }
  =
172 173 174 175 176 177
    let x = ref 0 in
    x := !x + 1;
    if n = 0 then 0 else h (n-1) + !x

  let hh () = h 10

MARCHE Claude's avatar
MARCHE Claude committed
178 179 180 181 182 183 184 185
  (* use of a global ref *)

  val x : ref int

  let j () =
    x := 42;
    !x

186 187 188
end


189 190
module Pair

191
  use ref.Ref
192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213

  type t = { left : ref int ; middle : int; right : ref int }

  let a () = { left = ref 13 ; middle = 5; right = ref 42 }

  let b () =
    let x = a () in
    x.left := 57;
    x.right := 98;
    x

  type u = { u1 : t ; u2 : t }

  let c () =
    let x = { left = ref 1; middle = 2; right = ref 3} in
    let y = { left = ref 4; middle = 5; right = ref 6} in
    let u = { u1 = x ; u2 = y } in
    u.u2.left := 7;
    u

end

214 215
module Array

216 217
  use int.Int
  use array.Array
218 219 220 221 222 223 224 225 226 227 228 229

  exception Found int

  let search (t:array int) (v:int) : int =
    try
      for i=0 to t.length - 1 do
        if t[i] = v then raise (Found i)
      done;
      -1
    with Found i -> i
    end

230 231 232 233 234
  let incr (t:array int) : unit =
    for i=0 to t.length - 1 do
      t[i] <- t[i]+1
    done

235 236 237 238
  let test0 () =
    let t = Array.make 2 21 in
    t[0]+t[1]
    (* should be 42 *)
239

240 241
  let test1 () =
    let t = Array.make 2 21 in
242 243
    t[1] <- 17;
    t[0]+t[1]
244
    (* should be 38 *)
245

246 247 248 249 250
  let test2 () =
    let t = Array.make 2 21 in
    t[1] <- 17;
    t[0] <- 7;
    t[0]+t[1]
251
    (* should be 24 *)
252 253

  let t () : array int =
254 255 256 257 258 259
     let t = Array.make 3 0 in
     t[0] <- 12;
     t[1] <- 42;
     t[2] <- 67;
     t

MARCHE Claude's avatar
MARCHE Claude committed
260
  let t1 () =
261 262 263
    let t = t () in
    t[0] + t[1] + t[2] (* 121 *)

264 265
  let i () = incr (t ())

266 267 268
  let test12 () = search (t ()) 12
  let test42 () = search (t ()) 42
  let test67 () = search (t ()) 67
269
  let test7 () = search (t ()) 7
270

MARCHE Claude's avatar
MARCHE Claude committed
271

272
  use array.ArraySwap
MARCHE Claude's avatar
MARCHE Claude committed
273 274 275 276 277 278 279 280 281 282 283 284 285 286 287

  let test_swap () =
     let t = Array.make 3 0 in
     t[0] <- 12;
     t[1] <- 42;
     t[2] <- 67;
     swap t 1 2;
     t[1] (* 67 *)


  let test_loop () =
     let t = Array.make 3 0 in
     for i=0 to 2 do t[i] <- i done;
     t[0] + t[1] + t[2] (* 3 *)

288 289 290 291 292 293
  (* global arrays *)

  val g : array int

  let j () = g[0] <- 42

294
end