-
Notifications
You must be signed in to change notification settings - Fork 0
/
test-state.timl
62 lines (51 loc) · 2 KB
/
test-state.timl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
val TestState_m : map int int
val TestState_mm : map int (map int int)
val TestState_v : vector int
val TestState_r : cell int
val TestState_i : icell
structure TestState = struct
fun waste_time () = 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0 + 0
fun assert p = if p then waste_time (); () else __&halt 0x11111111
fun iassert (p : ibool {true}) = ifi p then waste_time (); () else __&halt 0x11111111
fun inc n = n + 1
fun addBy b a = a + b
fun foo (a : int, b : int) using _ =
(* TestState_m[[a]] *)
(* set TestState_m[[a]] b *)
(* set TestState_m[[a]] ((((addBy b) using _, _) a) using _, _) (* TestState_m[[a]] *) *)
(modify TestState_m[[a]] += b);
TestState_m[[a]]
val a = foo (10, 20)
val () = assert (a = 20)
fun foo {len : Nat} () pre {TestState_v : len} post {TestState_v : len+1} =
let
val a = 0
val len = vector_len TestState_v
val () = push_back (TestState_v, 2)
val a = a + TestState_v[[len]]
val () = set TestState_v[[#0]] 10
val () = modify TestState_v[[#0]] inc (* == let val x = TestState_v[[0]] in set TestState_v[[0]] (inc x) end == set TestState_v[[0]] (inc TestState_v[[0]]) *)
val () = modify TestState_v[[#0]] addBy 20
val a = a + TestState_v[[#0]]
val () = set TestState_m[[1]] 100
val () = modify TestState_m[[1]] inc
val a = a + TestState_m[[1]]
val () = set TestState_mm[[1]][[2]] 200
val () = modify TestState_mm[[1]][[2]] ++
val () = modify TestState_mm[[1]][[2]] += 3
val a = a + TestState_mm[[1]][[2]]
val () = set TestState_r 44
val () = modify TestState_r += 5
val a = a + !TestState_r
in
a
end
val a = %foo ()
val () = assert (a = 2+10+1+20+100+1+200+1+3+44+5)
val a = vector_len TestState_v
val () = vector_clear TestState_v
val a = vector_len TestState_v
val () = set TestState_i #12
val () = iassert (!TestState_i #= #12)
val a = new_array (#5, 0x123) using _, _
end