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
63
64
65
66
|
From iris.heap_lang Require Import notation.
From iris.unstable.heap_lang Require Import interpreter.
Example test_1 :
exec 1000 ((λ: "x", "x" + #1) #2) = inl #3.
Proof. reflexivity. Qed.
Check "ex1".
Eval vm_compute in
exec 1000 (let: "x" := ref #() in
let: "y" := ref #() in
!"y").
Check "ex3".
(** eval order *)
Eval vm_compute in
exec 1000 (let: "x" := ref #1 in
let: "y" := ref #2 in
("y" <- !"x",
(* this runs first, so the result is 2 *)
"x" <- !"y");;
!"x").
(* print a location *)
Check "ex4".
Eval vm_compute in
exec 1000 (ref #();; ref #()).
Check "ex5".
Eval vm_compute in
exec 1000 (let: "x" := ref #() in
let: "y" := ref #() in
"x" = "y").
(* a bad case where the interpreter runs a program which is actually stuck,
because this program guesses an allocation that happens to be correct in the
interpreter *)
Check "ex6".
Eval vm_compute in
exec 1000 (let: "x" := ref #1 in
#(LitLoc {|loc_car := 1|}) <- #2;;
!"x").
(** * Failing executions *)
Check "fail app non-function".
Eval vm_compute in
exec 1000 (#2 #4).
(* locations can only be compared with other locations *)
Check "fail loc order".
Eval vm_compute in
exec 1000 (let: "x" := ref #() in
let: "y" := #1 in
"x" < "y").
Check "fail compare pairs".
Eval vm_compute in
exec 1000 ((#0, #1) = (#0, #1)).
Check "fail free var".
Eval vm_compute in exec 100 "x".
Check "fail out of fuel".
(** infinite loop *)
Eval vm_compute in exec 100 (rec: "foo" <> := "foo" #()).
|
