1 (* Boyland's nesting is available in Mezzo, thanks to the following primitive
 2    types and operations. *)
 3 
 4 (* A nesting witness, [nests x p], is a duplicable permission, which guarantees
 5    that an exclusive permission for [x] implies the permission [p]. Because
 6    nesting is monotonic (it cannot be undone), a nesting witness is duplicable. *)
 7 
 8 abstract nests (x : term) (p : perm) : perm
 9 fact duplicable (nests x p)
10 
11 (* Nesting consumes the permission [p] and produces a nesting witness [nests x p].
12    The instruction [nest [p] x] is somewhat analogous to an adoption instruction,
13    [give p to x]. The permission [p] becomes implicitly associated with the address
14    [x]. *)
15 
16 val nest: [p : perm, a] exclusive a => (x: a | consumes p) -> (| nests x p)
17 
18 (* A punched type [punched a p] is used to keep track of the fact that a nested
19    permission [p] has been temporarily recovered by focusing on [x]. This type
20    is not duplicable. It cannot be considered exclusive either; this prevents
21    double focusing. *)
22 
23 abstract punched (a : type) (p : perm) : type
24 
25 (* Focusing allows temporarily recovering a permission [p] that was nested in [x].
26    It requires an exclusive permission for [x], as well a nesting witness. It
27    produces a punched permission for [x]. The syntax is [focus [p] x], or
28    perhaps just [focus x]. *)
29 
30 val focus: [p : perm, a] exclusive a => (consumes x: a | nests x p) -> (| x @ punched a p * p)
31 
32 (* Defocusing is the reverse operation. The syntax is [defocus x]. *)
33 
34 val defocus: [p : perm, a] (consumes (x: punched a p | p)) -> (| x @ a)
35 
36 (* Nesting is permitted also while a region is punched. *)
37 
38 val nest_punched: [p : perm, a, q : perm] (x: punched a q | consumes p) -> (| nests x p)
39