blob: 630e1e12572a0e8daf4767afd95c7e307ba367f1 (
plain)
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
67
68
|
(** This module implements support for loops.
Throughout the module, we will use the following code as example to
illustrate what the functions do (this function simply returns a mutable
borrow to the nth element of a list):
{[
pub fn list_nth_mut<'a, T>(mut ls: &'a mut List<T>, mut i: u32) -> &'a mut T {
loop {
match ls {
List::Nil => {
panic!()
}
List::Cons(x, tl) => {
if i == 0 {
return x;
} else {
ls = tl;
i -= 1;
}
}
}
}
}
]}
Upon reaching the loop entry, the environment is as follows (ignoring the
dummy variables):
{[
abs@0 { ML l0 }
ls -> MB l0 (s2 : loops::List<T>)
i -> s1 : u32
]}
Upon reaching the [continue] at the end of the first iteration, the environment
is as follows:
{[
abs@0 { ML l0 }
ls -> MB l4 (s@6 : loops::List<T>)
i -> s@7 : u32
_@1 -> MB l0 (loops::List::Cons (ML l1, ML l2))
_@2 -> MB l2 (@Box (ML l4)) // tail
_@3 -> MB l1 (s@3 : T) // hd
]}
The fixed point we compute is:
{[
abs@0 { ML l0 }
ls -> MB l1 (s@3 : loops::List<T>)
i -> s@4 : u32
abs@fp { // fp: fixed-point
MB l0
ML l1
}
]}
From here, we deduce that [abs@fp { MB l0, ML l1}] is the loop abstraction.
*)
open Contexts
open Cps
open Meta
(** Evaluate a loop.
The `stl_cm_fun` required as input must be the function to evaluate the
loop body (i.e., `eval_statement` applied to the loop body).
*)
val eval_loop : config -> meta -> stl_cm_fun -> stl_cm_fun
|
