(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)
(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-2017 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
** 
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
** 
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)
(* ****** ****** *)
(* Author: Hongwei Xi *)
(* Start time: February, 2017 *)
(* Authoremail: hwxiATcsDOTbuDOTedu *)
(* ****** ****** *)
#define ATS_PACKNAME"ATSLIB.libats\
.BUCS320.DivideConquerPar"

(* ****** ****** *)
#staload UN = "prelude/SATS/unsafe.sats"

(* ****** ****** *)
#staload "libats/ML/SATS/basis.sats"
#staload "libats/ML/SATS/list0.sats"
#staload "prelude/DATS/list_vt.dats"
#staload "libats/ML/SATS/atspre.sats"

(* ****** ****** *)
#include "./../mydepies.hats"

(* ****** ****** *)
typedef input = $DivideConquer.input
typedef output = $DivideConquer.output

(* ****** ****** *)
vtypedef fwork = () -<lincloptr1> void
vtypedef fworklst = List0_vt_(fwork)

typedef spinref = $SPINREF.spinref(int)

(* ****** ****** *)
extern
fun DivideConquerPar$submit(fwork) : void

extern
fun DivideConquerPar$submit2(x0 : input, fwork) : void

(* ****** ****** *)
datatype fworkshop =
  | FWORKSHOP_chanlst of $FWORKSHOP_chanlst.fworkshop
  | FWORKSHOP_channel of $FWORKSHOP_channel.fworkshop

extern
fun DivideConquerPar$fworkshop() : fworkshop

(* ****** ****** *)
implement DivideConquerPar$submit (fwork) =
  let
    val fworkshop = DivideConquerPar$fworkshop{}(())
  in
    case+ fworkshop of
      | FWORKSHOP_chanlst (fws) => {
        val () = $FWORKSHOP_chanlst.fworkshop_insert_lincloptr( fws
                                                              , llam () =>
                                                                  0 where
                                                                  { val () = fwork()
                                                                    val () = cloptr_free($UN.castvwtp0{cloptr(void)}(fwork)) }
                                                              )
      }
      | FWORKSHOP_channel (fws) => {
        val () = $FWORKSHOP_channel.fworkshop_insert_lincloptr( fws
                                                              , llam () =>
                                                                  0 where
                                                                  { val () = fwork()
                                                                    val () = cloptr_free($UN.castvwtp0{cloptr(void)}(fwork)) }
                                                              )
      }
  end

(* ****** ****** *)
implement DivideConquerPar$submit2 (x0, fwork) =
  (DivideConquerPar$submit{}(fwork))

(* ****** ****** *)
#staload DC = $DivideConquer
#staload DC_cont = $DivideConquer_cont

(* ****** ****** *)
implement $DivideConquer$solve.DC (x0) =
  let
    #staload $NWAITER
    
    val NW = nwaiter_create_exn()
    val NWT = nwaiter_initiate(NW)
    val NWT = $UN.castvwtp0{ptr}(NWT)
    var res: output with 
    val () = $DC_cont.DivideConquer_cont$solve{}( x0
                                                , lam (r0) =>
                                                    nwaiter_ticket_put(NWT) where
                                                    { val () = $UN.ptr0_set<output>(addr@res, r0)
                                                      val NWT = $UN.castvwtp0{nwaiter_ticket}(NWT) }
                                                )
    val () = nwaiter_waitfor(NW)
    val () = nwaiter_destroy(NW)
  in
    $UN.ptr0_get<output>(addr@res)
  end

(* ****** ****** *)
implement $DivideConquer_cont$conquer.DC_cont (_, xs, k0) =
  let
    #staload $SPINREF
    
    fun spinref_decget(spnr : spinref) : int =
      let
        var env: int = 0
        
        typedef tenv = int
        
        implement spinref_process$fwork (x, env) =
          let
            val () = (x := x - 1)
          in
            env := x
          end
      in
        let
          val () = spinref_process_env(spnr, env)
        in
          env
        end
      end
    
    fun loop2 {n:nat} ( x0 : input
                      , xs : list(input, n)
                      , rs : !list_vt(output, n+1)
                      , spnr : spinref
                      , res : list0(output)
                      ) : void =
      let
        val+ @list_vt_cons (r0, rs1) = rs
        val addr_r0 = addr@(r0)
        val () = DivideConquerPar$submit2{}( x0
                                           , llam () =>
                                               ($DC_cont.DivideConquer_cont$solve( x0
                                                                                 , lam (r0) =>
                                                                                     let
                                                                                       val () = $UN.ptr0_set<output>( addr_r0
                                                                                                                    , r0
                                                                                                                    )
                                                                                       val c0 = spinref_decget(spnr)
                                                                                     in
                                                                                       if (c0 > 0) then
                                                                                         ()
                                                                                       else
                                                                                         k0(res) where
                                                                                         { val () = $SPINVAR.spinvar_destroy($UN.castvwtp0(spnr)) }
                                                                                     end
                                                                                 ))
                                           )
      in
        case+ xs of
          | list_nil() => () where
          { prval () = fold@(rs) }
          | list_cons (x1, xs) => () where
          { val () = loop2(x1, xs, rs1, spnr, res)
            prval () = fold@(rs) }
      end
    
    val xs = g1ofg0(xs)
    val n0 = length(xs)
  in
    ifcase
      | n0 = 0 => k0(list0_nil())
      | n0 = 1 => let
        val+ list_sing (x0) = xs
      in
        $DC_cont.DivideConquer_cont$solve(x0, lam (r0) => k0(list0_sing(r0)))
      end
      | _ => let
        val rs = list_map_cloref(xs, lam _ => _)
        val res = $UN.castvwtp1{list0(output)}(rs)
        val+ list_cons (x, xs) = xs
        val () = loop2(x, xs, rs, spinref_create_exn<int>(n0), res)
        prval () = $UN.cast2void(rs)
      in end
  end

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