(***********************************************************************)
(*                                                                     *)
(*                       ATS/contrib/libats-hwxi                       *)
(*                                                                     *)
(***********************************************************************)
(*
** Copyright (C) 2015-2017 Hongwei Xi, ATS Trustful Software, Inc.
**
** Permission is hereby granted, free of charge, to any person obtaining a
** copy of this software and associated documentation files (the "Software"),
** to deal in the Software without restriction, including without limitation
** the rights to use, copy, modify, merge, publish, distribute, sublicense,
** and/or sell copies of the Software, and to permit persons to whom the
** Software is furnished to do so, subject to the following stated conditions:
** 
** The above copyright notice and this permission notice shall be included in
** all copies or substantial portions of the Software.
** 
** THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
** OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
** FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL
** THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
** LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
** FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
** IN THE SOFTWARE.
*)
(* ****** ****** *)
// HX-2015-01:
// An array-based linear channel
(* ****** ****** *)
staload UN = "prelude/SATS/unsafe.sats"

(* ****** ****** *)
staload "libats/SATS/athread.sats"
staload "libats/SATS/deqarray.sats"

(* ****** ****** *)
staload "./../SATS/channel_vt.sats"

(* ****** ****** *)
absvtype queue_vtype(a : vt@ype+, int) = ptr

vtypedef queue(a : vt0p, id : int) = queue_vtype(a, id)
vtypedef queue(a : vt0p) = [id:int] queue(a, id)

(* ****** ****** *)
extern
fun {a:vt0p} queue_make  (cap : sizeGt(0)) : queue(a)

extern
fun {a:t@ype} queue_free_type  (que : queue(a)) : void

(* ****** ****** *)
absprop ISNIL (id : int, b : bool)

absprop ISFUL (id : int, b : bool)

(* ****** ****** *)
extern
fun {a:vt0p} queue_isnil {id:int} (que : !queue(a, id)) :
  [b:bool] (ISNIL(id, b) | bool(b))

extern
fun {a:vt0p} queue_isful {id:int} (que : !queue(a, id)) :
  [b:bool] (ISFUL(id, b) | bool(b))

(* ****** ****** *)
extern
fun {a:vt0p} queue_insert {id:int}
(pf : ISFUL(id, false) | xs : !queue(a, id) >> queue(a, id2), x0 : a) :
  #[id2:int] void

extern
fun {a:vt0p} queue_takeout {id:int}
(pf : ISNIL(id, false) | xs : !queue(a, id) >> queue(a, id2)) :
  #[id2:int] a

(* ****** ****** *)
local
  assume ISFUL(id : int, b : bool) = unit_p
  
  assume ISNIL(id : int, b : bool) = unit_p
  
  assume queue_vtype(a : vt0p, id : int) = deqarray(a)
  
  staload "libats/SATS/deqarray.sats"
in
  implement {a} queue_takeout (pf | xs) =
    let
      prval () = __assert(pf) where
      { extern
        praxi __assert {id:int} (pf : ISNIL(id, false)) : [ false ] void }
    in
      deqarray_takeout_atbeg<a>(xs)
    end
  
  (* ****** ****** *)
  implement {a} queue_insert (pf | xs, x0) =
    {
      prval () = __assert(pf) where
      { extern
        praxi __assert {id:int} (pf : ISFUL(id, false)) : [ false ] void }
      val () = deqarray_insert_atend<a>(xs, x0)
    }
  
  implement {a} queue_isful (xs) =
    (unit_p() | deqarray_is_full<a>(xs))
  
  implement {a} queue_isnil (xs) =
    (unit_p() | deqarray_is_nil{a}(xs))
  
  implement {a} queue_free_type (q0) =
    deqarray_free_nil{a}($UN.castvwtp0{deqarray(a, 1, 0)}(q0))
  
  implement {a} queue_make (cap) =
    deqarray_make_cap(cap)
end

(* ****** ****** *)
datavtype channel_ =
  | { l0, l1, l2, l3 : agz } CHANNEL of @{ cap = sizeGt(0)
                                         , spin = spin_vt(l0)
                                         , rfcnt = intGt(0)
                                         , mutex = mutex_vt(l1)
                                         , CVisnil = condvar_vt(l2)
                                         , CVisful = condvar_vt(l3)
                                         , queue = ptr
                                         }

(* ****** ****** *)
assume channel_vtype(a : vt0p) = channel_

(* ****** ****** *)
implement {a} channel_create_exn (cap) =
  let
    extern
    praxi __assert() : [l:agz] void
    
    prval [l0:addr]() = __assert()
    prval [l1:addr]() = __assert()
    prval [l2:addr]() = __assert()
    prval [l3:addr]() = __assert()
    val chan = CHANNEL{l0,l1,l2,l3}(_)
    val+ CHANNEL (ch) = chan
    val () = ch.cap := cap
    val () = ch.rfcnt := 1
    
    local
      val x = spin_create_exn()
    in
      val () = ch.spin := unsafe_spin_t2vt(x)
    end
    
    local
      val x = mutex_create_exn()
    in
      val () = ch.mutex := unsafe_mutex_t2vt(x)
    end
    
    local
      val x = condvar_create_exn()
    in
      val () = ch.CVisnil := unsafe_condvar_t2vt(x)
    end
    
    local
      val x = condvar_create_exn()
    in
      val () = ch.CVisful := unsafe_condvar_t2vt(x)
    end
    
    val () = ch.queue := $UN.castvwtp0{ptr}(queue_make<a>(cap))
  in
    (fold@(chan) ; chan)
  end

(* ****** ****** *)
implement {a} channel_ref (chan) =
  let
    val @CHANNEL (ch) = chan
    val spin = unsafe_spin_vt2t(ch.spin)
    val (pf | ()) = spin_lock(spin)
    val () = ch.rfcnt := ch.rfcnt + 1
    val () = spin_unlock(pf | spin)
    prval () = fold@(chan)
  in
    $UN.castvwtp1{channel(a)}(chan)
  end

(* ****** ****** *)
implement {a} channel_unref (chan) =
  let
    val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan
    val spin = unsafe_spin_vt2t(ch.spin)
    val (pf | ()) = spin_lock(spin)
    val rfcnt = ch.rfcnt
    val () = spin_unlock(pf | spin)
  in
    if (rfcnt >= 2) then
      let
        val () = ch.rfcnt := rfcnt - 1
        prval () = fold@(chan)
        prval () = $UN.cast2void(chan)
      in
        $UN.castvwtp0{queueopt(a)}(0)
      end
    else
      let
        val que = $UN.castvwtp0{queue(a)}(ch.queue)
        val () = spin_vt_destroy(ch.spin)
        val () = mutex_vt_destroy(ch.mutex)
        val () = condvar_vt_destroy(ch.CVisnil)
        val () = condvar_vt_destroy(ch.CVisful)
        val () = free@{l0,l1,l2,l3}(chan)
      in
        $UN.castvwtp0{queueopt(a)}(que)
      end
  end

(* ****** ****** *)
implement channel_get_refcount {a} (chan) =
  let
    val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan
    val rfcnt = ch.rfcnt
  in
    (fold@(chan) ; rfcnt)
  end

(* ****** ****** *)
local
  extern
  fun {a:vt0p} channel_insert_buf  (!channel(a), !queue(a) >> _, a) : void
in
  implement {a} channel_insert_buf (chan, xs, x0) =
    let
      val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan
      val (pf | isful) = queue_isful<a>(xs)
    in
      if isful then
        let
          prval (pfmut, fpf) = __assert() where
          { extern
            praxi __assert() : vtakeout0(locked_v(l1)) }
          val mutex = unsafe_mutex_vt2t(ch.mutex)
          val CVisful = unsafe_condvar_vt2t(ch.CVisful)
          val () = condvar_wait(pfmut | CVisful, mutex)
          prval () = fpf(pfmut)
        in
          channel_insert_buf<a>(chan, xs, x0)
        end
      else
        let
          val isnil = queue_isnil<a>(xs)
          val () = queue_insert<a>(pf | xs, x0)
          val () = if isnil.1 then
            condvar_broadcast(unsafe_condvar_vt2t(ch.CVisnil))
        in end
    end
  
  (* ****** ****** *)
  implement {a} channel_insert_opt (chan, x0) =
    opt where
    { val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan
      val mutex = unsafe_mutex_vt2t(ch.mutex)
      val (pfmut | ()) = mutex_lock(mutex)
      val xs = $UN.castvwtp0{queue(a)}((pfmut | ch.queue))
      val (pf | isful) = queue_isful<a>(xs)
      val opt = (if isful then
        Some_vt(x0)
      else
        None_vt where
        { val isnil = queue_isnil<a>(xs)
          val () = queue_insert<a>(pf | xs, x0)
          val () = if isnil.1 then
            condvar_broadcast(unsafe_condvar_vt2t(ch.CVisnil)) }) : Option_vt(a)
      prval pfmut = $UN.castview0{locked_v(l1)}(xs)
      val () = mutex_unlock(pfmut | mutex) }
  
  (* ****** ****** *)
  implement {a} channel_insert (chan, x0) =
    let
      val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan
      val mutex = unsafe_mutex_vt2t(ch.mutex)
      val (pfmut | ()) = mutex_lock(mutex)
      val xs = $UN.castvwtp0{queue(a)}((pfmut | ch.queue))
      val () = channel_insert_buf<a>(chan, xs, x0)
      prval pfmut = $UN.castview0{locked_v(l1)}(xs)
      val () = mutex_unlock(pfmut | mutex)
    in end
  
  (* ****** ****** *)
end

(* ****** ****** *)
local
  extern
  fun {a:vt0p} channel_takeout_buf  (chan : !channel(a), !queue(a) >> _) :
    a
in
  implement {a} channel_takeout_buf (chan, xs) =
    let
      val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan
      val (pf | isnil) = queue_isnil<a>(xs)
    in
      if isnil then
        let
          prval (pfmut, fpf) = __assert() where
          { extern
            praxi __assert() : vtakeout0(locked_v(l1)) }
          val mutex = unsafe_mutex_vt2t(ch.mutex)
          val CVisnil = unsafe_condvar_vt2t(ch.CVisnil)
          val () = condvar_wait(pfmut | CVisnil, mutex)
          prval () = fpf(pfmut)
        in
          channel_takeout_buf<a>(chan, xs)
        end
      else
        let
          val isful = queue_isful<a>(xs)
          val x0_out = queue_takeout<a>(pf | xs)
          val () = if isful.1 then
            condvar_broadcast(unsafe_condvar_vt2t(ch.CVisful))
        in
          x0_out
        end
    end
  
  (* ****** ****** *)
  implement {a} channel_takeout_opt (chan) =
    opt where
    { val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan
      val mutex = unsafe_mutex_vt2t(ch.mutex)
      val (pfmut | ()) = mutex_lock(mutex)
      val xs = $UN.castvwtp0{queue(a)}((pfmut | ch.queue))
      val (pf | isnil) = queue_isnil<a>(xs)
      val opt = (if isnil then
        None_vt()
      else
        Some_vt(x0_out) where
        { val isful = queue_isful<a>(xs)
          val x0_out = queue_takeout<a>(pf | xs)
          val () = if isful.1 then
            condvar_broadcast(unsafe_condvar_vt2t(ch.CVisful)) }) : Option_vt(a)
      prval pfmut = $UN.castview0{locked_v(l1)}(xs)
      val () = mutex_unlock(pfmut | mutex) }
  
  (* ****** ****** *)
  implement {a} channel_takeout (chan) =
    x0_out where
    { val+ CHANNEL{ l0, l1, l2, l3 }(ch) = chan
      val mutex = unsafe_mutex_vt2t(ch.mutex)
      val (pfmut | ()) = mutex_lock(mutex)
      val xs = $UN.castvwtp0{queue(a)}((pfmut | ch.queue))
      val x0_out = channel_takeout_buf<a>(chan, xs)
      prval pfmut = $UN.castview0{locked_v(l1)}(xs)
      val () = mutex_unlock(pfmut | mutex) }
  
  (* ****** ****** *)
end

(* ****** ****** *)
(* end of [channel_vt.dats] *)