alms-0.6.0: examples/ex28-focusing-and-adoption.alms

(* Demonstrates adoption/focus (Faehnrich and DeLine, 2002). *)

(*
  type variables:
    `a `b             stored value
    't 's               capability name
*)

let snoc x xs = append xs [x]

let rec revAppN n xs acc =
    match n with
    | 0 → (acc, xs)
    | _ → match xs with
           | x ∷ xs → revAppN (n - 1) xs (x ∷ acc)
           | xs     → (acc, xs)

let swapN ix y xs =
  let (x ∷ xs, acc) = revAppN ix xs [] in
    (x, revApp acc (y ∷ xs))

abstype 't tr            = Tr
    and ('t, `a) cap : A = Cap of `a * (unit -A> unit) list
    and ('t, `a) guarded =
                    Guarded of (`a * (unit -A> unit) list) option ref
with
  let new (x: `a) : ∃ 't. ('t, `a) cap * 't tr =
    (Cap (x, []), Tr)

  let swap ((Cap (x, fs), _) : ('t, `a) cap * 't tr) (y : `b)
    : ('t, `b) cap * `a =
    (Cap (y, fs), x)

  let free (Cap (_, fs)) = map (λ f → f ()) fs; ()

  let adoptByThen
      ((Cap adoptee, _)                : ('ta, `a) cap * 'ta tr)
      ((Cap (adoptor, destructors), _) : ('tb, `b) cap * 'tb tr)
      (destroy                         : ('ta, `a) cap -A> unit)
      : ('tb, `b) cap * ('tb, `a) guarded =
    let r    = ref (Some adoptee) in
    let g () = match r <- None with
               | None   → failwith "Can't happen"
               | Some c → destroy (Cap c) in
      (Cap (adoptor, g ∷ destructors), Guarded r)
  let adoptBy
      (adoptee : ('ta, `a) cap * 'ta tr)
      (adoptor : ('tb, `b) cap * 'tb tr)
      : ('tb, `b) cap * ('tb, `a) guarded
      = adoptByThen adoptee adoptor (λ (_: ('ta, `a) cap) → ())

  let focusIn
      ((guard, Guarded r) : ('t, `a) cap * ('t, `b) guarded)
      (body               : (∀ 's. ('s, `b) cap * 's tr -A>
                                   ('s, `b) cap * `r))
      : ('t, `a) cap * `r =
      match r <- None with
      | None   → failwith "Can't happen"
      | Some c →
          let (Cap c, result) = body (Cap c, Tr)
           in r <- Some c;
              (guard, result)
end