(* Demonstrates Pottier's (2007) version of adoption/focus
   (Faehnrich and DeLine, 2002). *)

(* Some affine list operations. *)

(*
  type variables:
    `a                 stored value
    't                  region name

  variables:
    x, y: `a           stored value
    xs: `a list        region representation

  T[[ { p |→ t } ]]     = (p, T[[ t ]]) region1
  T[[ { p |→^w t } ]]   = (p, T[[ t ]]) region
  T[[ Ptr t ]]           = T[[ t ]] ptr

*)

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))

module type REGION = sig
  type ('t, `a) region  : A
  type ('t, `a) region1 : A
  type 't ptr

  val newRgn    : unit → ∃ 't. ('t,`a) region
  val mallocIn  : ('t,`a) region → `a -A> 't ptr * ('t,`a) region
  val swap      : ('t,`a) region → 't ptr -A> `a -A> `a * ('t,`a) region
  val malloc    : unit → ∃ 't. ('t,unit) region1 * 't ptr
  val free      : ('t,`a) region1 → unit
  val adopt     : ('t1,`a) region → ('t2,`a) region1 -A> 't2 ptr -A>
                  't1 ptr * ('t1,`a) region
  val focus     : ('t,`a) region → 't ptr -A>
                  ∃ 't1. ('t1,`a) region1 * 't1 ptr *
                          (('t1,`a) region1 -A> ('t,`a) region)
end

module Region : REGION = struct
  type ('t, `a) region = `a list
  type ('t, `a) region1 = `a
  type 't ptr = int

  let newRgn () = [] : ∃ 't. ('t,`a) region

  let freeRgn _ = ()

  let mallocIn (xs: `a list) (a: `a) =
    let (ix, xs) = lengthA xs in
      (ix, snoc a xs)

  let swap (xs: `a list) (ix: 't ptr) (x: `a) =
    let (y, xs) = swapN ix x xs in
      (y, xs)

  let malloc () = ((), 0) : ∃ 't. ('t,unit) region1 * 't ptr

  let swap1 (x: `a) _ (y: `b) = (x, y)

  let free _ = ()

  let adopt (rgn: `a list) (x: `a) _ =
    mallocIn rgn x

  let focus xs ix
        : ∃ 't1. ('t1,`a) region1 * 't1 ptr *
                 (('t1,`a) region1 -A> ('t,`a) region)
        =
     let (x ∷ xs, acc) = revAppN ix xs [] in
       (x, 0, λ y → revApp acc (y ∷ xs))
end