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