(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-2013 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.
*)

(* ****** ****** *)

(*
**
** A list-based queue implementation
**
*)

(* ****** ****** *)

(*
**
** Author: Hongwei Xi
** Authoremail: hwxiATcsDOTbuDOTedu
** Time: July, 2010
** It is based on an earlier version done in October, 2008
**
*)

(* ****** ****** *)
//
// HX-2012-12: ported to ATS/Postitats from ATS/Anairiats
//
(* ****** ****** *)

%{#
#include "libats/CATS/qlist.cats"
%} // end of [%{#]

(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.qlist"
//
(* ****** ****** *)
//
absvtype
qlist_vtype(a:vt@ype+, n:int) = ptr
//
vtypedef
qlist(a:vt0p, n:int) = qlist_vtype(a, n)
//
vtypedef
qlist(a:vt0p) = [n:int] qlist_vtype(a, n)
//
vtypedef
qlist0(a:vt0p) = [n:int | n >= 0] qlist(a, n)
//
(* ****** ****** *)

praxi
lemma_qlist_param
  {a:vt0p}{n:int}
  (q0: !qlist(INV(a), n)): [n >= 0] void
// end of [lemma_qlist_param]

(* ****** ****** *)
//
fun{}
qlist_make_nil{a:vt0p}():<!wrt> qlist(a, 0)
//
fun{}
qlist_free_nil{a:vt0p}(qlist(a, 0)):<!wrt> void
//
(* ****** ****** *)
//
fun
{a:vt0p}
qlist_length
  {n:int}(q0: !qlist(INV(a), n)):<> int(n)
//
(* ****** ****** *)
//
fun{a:vt0p}
qlist_is_nil
  {n:int}(q0: !qlist(a, n)):<> bool(n == 0)
fun{a:vt0p}
qlist_isnot_nil
  {n:int}(q0: !qlist(INV(a), n)):<> bool(n > 0)
//
(* ****** ****** *)
//
fun{}
fprint_qlist$sep
  (out: FILEref): void
//
fun{a:vt0p}
fprint_qlist
(
  out: FILEref, que: !qlist(INV(a))
) : void // end of [fprint_qlist]
fun{a:vt0p}
fprint_qlist_sep
(
  out: FILEref, que: !qlist(INV(a)), sep: string
) : void // end of [fprint_qlist_sep]
//
(* ****** ****** *)

fun{a:vt0p}
qlist_insert{n:int}
(
  que:
  !qlist(INV(a), n) >> qlist(a, n+1)
, elt: a
) :<!wrt> void // end of [qlist_insert]

(* ****** ****** *)
//
fun{a:vt0p}
qlist_takeout{n:pos}
(
  q0: !qlist(INV(a), n) >> qlist(a, n-1)
) :<!wrt> (a) // end-of-function
//
fun{a:vt0p}
qlist_takeout_opt
  (q0: !qlist(INV(a)) >> _):<!wrt> Option_vt(a)
//
(* ****** ****** *)
//
(*
** HX: this operation is O(1)
*)
//
fun{}
qlist_takeout_list{a:vt0p}{n:int}
  (q0: !qlist(INV(a), n) >> qlist(a, 0)):<!wrt> list_vt(a, n)
// end of [qlist_takeout_list]
//
(* ****** ****** *)
//
fun
{a:vt0p}
qlist_foreach(q0: !qlist(INV(a))): void
fun
{a:vt0p}
{env:vt0p}
qlist_foreach_env
  (q0: !qlist(INV(a)), env: &(env) >> _): void
//
fun
{a:vt0p}
{env:vt0p}
qlist_foreach$cont(x0: &a, env: &env): bool
fun
{a:vt0p}
{env:vt0p}
qlist_foreach$fwork(x0: &a >> _, env: &(env) >> _): void
//
(* ****** ****** *)
//
abst@ype
qstruct_tsize =
$extype"atslib_qlist_struct"
absvt@ype
qstruct_vt0ype
  (a:vt@ype+, n:int) = qstruct_tsize
//
stadef
qstruct = qstruct_vt0ype
//
stadef
qstruct = qstruct_tsize // HX: order significant
//
viewtypedef
qstruct(a:vt0p) = [n:int] qstruct(a, n)
viewtypedef
qstruct0(a:vt0p) = [n:nat] qstruct(a, n)
//
(* ****** ****** *)
//
fun{}
qstruct_initize
  {a:vt0p}
  (q0: &qstruct? >> qstruct(a, 0)):<!wrt> void
// end of [qstruct_initize]
//
praxi
qstruct_uninitize
  {a:vt0p}
  ( q0: &qstruct(a, 0) >> qstruct? ):<prf> void
// end of [qstruct_uninitize]
//
(* ****** ****** *)

praxi
qstruct_objfize
  {a:vt0p}
  {l:addr}{n:int}
(
  pf:
  qstruct
  (INV(a), n) @ l | p0: !ptrlin(l) >> qlist(a, n)
) :<prf> mfree_ngc_v(l) // end of [qstruct_objfize]

praxi
qstruct_unobjfize
  {a:vt0p}
  {l:addr}{n:int}
(
  pf: mfree_ngc_v(l) | p0: ptr(l), q0: !qlist(INV(a), n) >> ptrlin(l)
) :<prf> qstruct(a, n) @ l // end of [qstruct_unobjfize]

(* ****** ****** *)
//
fun{a:vt0p}
qstruct_insert{n:int}
(
  q0: &qstruct(INV(a), n) >> qstruct(a, n+1), x0: a
) :<!wrt> void // end of [qstruct_insert]
//
(* ****** ****** *)
//
fun{a:vt0p}
qstruct_takeout{n:pos}
  (q0: &qstruct(INV(a), n) >> qstruct(a, n-1)):<!wrt> (a)
//
(* ****** ****** *)
//
(*
** HX: this operation is O(1)
*)
//
fun{}
qstruct_takeout_list{a:vt0p}{n:int}
  (q0: &qstruct(INV(a), n) >> qstruct(a, 0)):<!wrt> list_vt(a, n)
// end of [qstruct_takeout_list]
//
(* ****** ****** *)
//
// HX: ngc-functions do not make use of malloc/free
//
(* ****** ****** *)

absvtype
qlist_node_vtype(a:vt@ype+, l:addr) = ptr

(* ****** ****** *)
//
stadef
mynode = qlist_node_vtype
//
vtypedef
mynode(a) = [l:addr] mynode(a, l)
vtypedef
mynode0(a) = [l:addr | l >= null] mynode(a, l)
vtypedef
mynode1(a) = [l:addr | l >  null] mynode(a, l)
//
(* ****** ****** *)

castfn
mynode2ptr
  {a:vt0p}
  {l:addr}
  (nx: !mynode(INV(a), l)):<> ptr(l)
// end of [mynode2ptr]

(* ****** ****** *)
//
fun{}
mynode_null{a:vt0p}(): mynode(a, null)
//
praxi
mynode_free_null{a:vt0p}(nx: mynode(a, null)): void
//
(* ****** ****** *)
//
fun{a:vt0p}
mynode_make_elt(x: a):<!wrt> mynode1(a)
//
fun{a:vt0p}
mynode_getref_elt(nx: !mynode1(INV(a))):<> cPtr1(a)
//
fun{a:vt0p}
mynode_free_elt
  (nx: mynode1(INV(a)), res: &(a?) >> a):<!wrt> void
// end of [mynode_free_elt]
//
fun{a:vt0p}
mynode_getfree_elt(node: mynode1(INV(a))):<!wrt> (a)
//
(* ****** ****** *)

fun{a:vt0p}
qlist_insert_ngc (*last*)
  {n:int}
(
  q0: !qlist(INV(a), n) >> qlist(a, n+1), nx: mynode1(a)
) :<!wrt> void // end of [qlist_insert_ngc]

(* ****** ****** *)

fun{a:vt0p}
qlist_takeout_ngc (*first*)
  {n:int | n > 0}
  (q0: !qlist(INV(a), n) >> qlist(a, n-1)):<!wrt> mynode1(a)
// end of [qlist_takeout_ngc]

(* ****** ****** *)
//
// overloading for certain symbols
//
(* ****** ****** *)
//
overload iseqz with qlist_is_nil
overload isneqz with qlist_isnot_nil
//
overload length with qlist_length
//
overload fprint with fprint_qlist
overload fprint with fprint_qlist_sep
//
(* ****** ****** *)

(* end of [qlist.sats] *)

(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-2013 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 *)
(* Authoremail: hwxi AT cs DOT bu DOT edu *)
(* Start time: March, 2013 *)

(* ****** ****** *)

#define ATS_PACKNAME "ATSLIB.libats.sllist"

(* ****** ****** *)

typedef SHR(a:type) = a // for commenting purpose
typedef NSH(a:type) = a // for commenting purpose

(* ****** ****** *)

(*
**
** HX-2013-03:
** sllist (a, n) means that there are n elements in the list.
**
*)
absvtype
sllist_vtype (a:viewt@ype+, n:int) = ptr
stadef sllist = sllist_vtype // HX: shorthand
//
vtypedef Sllist (a:vt0p) = [n:int] sllist (a, n)
vtypedef Sllist0 (a:vt0p) = [n:int | n >= 0] sllist (a, n)
vtypedef Sllist1 (a:vt0p) = [n:int | n >= 1] sllist (a, n)
//
(* ****** ****** *)

castfn
sllist2ptr {a:vt0p} (xs: !Sllist (INV(a))):<> Ptr0
castfn
sllist2ptr1 {a:vt0p} (xs: !Sllist1 (INV(a))):<> Ptr1

(* ****** ****** *)

praxi
lemma_sllist_param {a:vt0p}
  {n:int} (xs: !sllist (INV(a), n)): [n >= 0] void
// end of [lemma_sllist_param]

(* ****** ****** *)

fun{}
sllist_nil {a:vt0p} ():<> sllist (a, 0)

(* ****** ****** *)

praxi
sllist_free_nil
  {a:vt0p} (xs: sllist (INV(a), 0)): void

(* ****** ****** *)

fun{a:vt0p}
sllist_sing (x: a):<!wrt> sllist (a, 1)

(* ****** ****** *)

fun{a:vt0p}
sllist_cons{n:int}
  (x: a, xs: sllist (INV(a), n)):<!wrt> sllist (a, n+1)
// end of [sllist_cons]

fun{a:vt0p}
sllist_uncons{n:int | n > 0}
  (xs: &sllist (INV(a), n) >> sllist (a, n-1)):<!wrt> (a)
// end of [sllist_uncons]

(* ****** ****** *)

fun{a:vt0p}
sllist_snoc{n:int}
  (xs: sllist (INV(a), n), x: a):<!wrt> sllist (a, n+1)
// end of [sllist_snoc]

fun{a:vt0p}
sllist_unsnoc{n:int | n > 0}
  (xs: &sllist (INV(a), n) >> sllist (a, n-1)):<!wrt> (a)
// end of [sllist_unsnoc]

(* ****** ****** *)

fun{a:t0p}
sllist_make_list
  {n:int} (xs: list (INV(a), n)):<!wrt> sllist (a, n)
// end of [sllist_make_list]

(* ****** ****** *)

fun{a:t0p}
sllist_make_list_vt
  {n:int} (xs: list_vt (INV(a), n)):<!wrt> sllist (a, n)
// end of [sllist_make_list_vt]

(* ****** ****** *)

fun{
} sllist_is_nil
  {a:vt0p}{n:int} (xs: !sllist (INV(a), n)):<> bool (n==0)
fun{
} sllist_is_cons
  {a:vt0p}{n:int} (xs: !sllist (INV(a), n)):<> bool (n > 0)
//
overload iseqz with sllist_is_nil
overload isneqz with sllist_is_cons
//
(* ****** ****** *)

fun{a:vt0p}
sllist_length
  {n:int} (xs: !sllist (INV(a), n)):<> int (n)
//
overload length with sllist_length
//
(* ****** ****** *)

fun{a:t0p}
sllist_get_elt (xs: !Sllist1 (INV(a))): (a)
fun{a:t0p}
sllist_set_elt (xs: !Sllist1 (INV(a)), x0: a): void
fun{a:vt0p}
sllist_getref_elt (xs: !Sllist1 (INV(a))):<> cPtr1 (a)

(* ****** ****** *)

fun{a:vt0p}
sllist_getref_next (xs: !Sllist1 (INV(a))):<> Ptr1

(* ****** ****** *)

fun{a:vt0p}
sllist_getref_elt_at {n:int}
  (xs: !sllist (INV(a), n), i: natLt(n)):<> cPtr1 (a)
// end of [sllist_getref_elt_at]

(* ****** ****** *)

fun{a:t0p}
sllist_get_elt_at {n:int}
  (xs: !sllist (INV(a), n), i: natLt(n)):<> (a)
overload [] with sllist_get_elt_at
fun{a:t0p}
sllist_set_elt_at {n:int}
  (xs: !sllist (INV(a), n), i: natLt(n), x0: a):<!wrt> void
overload [] with sllist_set_elt_at

(* ****** ****** *)

fun{a:vt0p}
sllist_getref_at{n:int}
  (xs: &sllist (INV(a), n), i: natLte(n)):<> Ptr1
// end of [sllist_getref_at]

fun{a:vt0p}
sllist_insert_at {n:int}
  (xs: sllist (INV(a), n), i: natLte(n), x0: a):<!wrt> sllist (a, n+1)
// end of [sllist_insert_at]

fun{a:vt0p}
sllist_takeout_at {n:int}
  (xs: &sllist (INV(a), n) >> sllist (a, n-1), i: natLt(n)):<!wrt> (a)
// end of [sllist_takeout_at]

(* ****** ****** *)

fun{a:vt0p}
sllist_append
  {n1,n2:int} (
  xs1: sllist (INV(a), n1), xs2: sllist (a, n2)
) :<!wrt> sllist (a, n1+n2) // end of [sllist_append]

(* ****** ****** *)

fun{a:vt0p}
sllist_reverse
  {n:int} (xs: sllist (INV(a), n)):<!wrt> sllist (a, n)
// end of [sllist_reverse]

(* ****** ****** *)

fun{a:vt0p}
sllist_reverse_append
  {n1,n2:int} (
  xs1: sllist (INV(a), n1), xs2: sllist (a, n2)
) :<!wrt> sllist (a, n1+n2) // end of [sllist_reverse_append]

(* ****** ****** *)

fun{a:t0p}
sllist_free (xs: Sllist (INV(a))):<!wrt> void

fun{a:vt0p}
sllist_freelin$clear (x: &a >> a?):<!wrt> void
fun{a:vt0p}
sllist_freelin (xs: Sllist (INV(a))):<!wrt> void

(* ****** ****** *)

fun{
a:vt0p}{b:vt0p
} sllist_map$fopr (x: &a): b
fun{
a:vt0p}{b:vt0p
} sllist_map {n:int} (xs: !sllist (a, n)): sllist (b, n)

(* ****** ****** *)
//
fun{
a:vt0p}{env:vt0p
} sllist_foreach$cont (x: &a, env: &env): bool
fun{
a:vt0p}{env:vt0p
} sllist_foreach$fwork (x: &a, env: &env >> _): void
//
fun{a:vt0p}
sllist_foreach (xs: !Sllist (INV(a))): void
fun{
a:vt0p}{env:vt0p
} sllist_foreach_env
  (xs: !Sllist (INV(a)), env: &env >> _): void
// end of [sllist_foreach_env]
//
(* ****** ****** *)
//
fun{}
fprint_sllist$sep (out: FILEref): void
//
fun{a:vt0p}
fprint_sllist
  (out: FILEref, xs: !Sllist (INV(a))): void
// end of [fprint_sllist]
//
overload fprint with fprint_sllist
//
(* ****** ****** *)
//
// HX-2013-05: functions of ngc-version
//
(* ****** ****** *)

staload "libats/SATS/gnode.sats"

(* ****** ****** *)

stadef mytkind = $extkind"libats_sllist"

(* ****** ****** *)

typedef g2node0 (a:vt0p) = gnode0 (mytkind, a)
typedef g2node1 (a:vt0p) = gnode1 (mytkind, a)

(* ****** ****** *)

(*
** HX: this is O(1)-time
*)
fun{a:vt0p}
sllist_cons_ngc{n:int}
  (nx: g2node1(a), xs: sllist(INV(a), n)):<!wrt> sllist (a, n+1)
// end of [sllist_cons_ngc]

(*
** HX: this is O(1)-time
*)
fun{a:vt0p}
sllist_uncons_ngc{n:pos}
  (xs: &sllist (INV(a), n) >> sllist (a, n-1)):<!wrt> g2node1 (a)
// end of [sllist_uncons_ngc]

(* ****** ****** *)

(*
** HX: this is O(n)-time
*)
fun{a:vt0p}
sllist_snoc_ngc{n:int}
  (xs: sllist(INV(a), n), nx: g2node1(a)):<!wrt> sllist (a, n+1)
// end of [sllist_snoc_ngc]

(*
** HX: this is O(n)-time
*)
fun{a:vt0p}
sllist_unsnoc_ngc{n:pos}
  (xs: &sllist (INV(a), n) >> sllist (a, n-1)):<!wrt> g2node1 (a)
// end of [sllist_unsnoc_ngc]

(* ****** ****** *)

(* end of [sllist.sats] *)

(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-2013 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.
*)

(* ****** ****** *)

(*
**
** An list-based stack implementation
**
*)

(* ****** ****** *)

(*
**
** Author: Hongwei Xi
** Start time: March, 2017
** Authoremail: gmhwxiATgmailDOTcom
**
*)

(* ****** ****** *)
//
#define
ATS_PACKNAME
"ATSLIB.libats.stklist"
//
// HX-2017-03-28:
#define // prefix for external
ATS_EXTERN_PREFIX "atslib_" // names
//
(* ****** ****** *)
//
absvtype
stklist_vtype
  (a: vt@ype+, n: int) = ptr
//
(* ****** ****** *)
//
stadef
stklist = stklist_vtype
//
vtypedef
stklist
(
  a:vt0p
) = [n:int] stklist_vtype(a, n)
//
(* ****** ****** *)
//
praxi
lemma_stklist_param
  {a:vt0p}{n:int}
  (stk: !stklist(INV(a), n)): [n >= 0] void
// end of [lemma_stklist_param]
//
(* ****** ****** *)
//
fun{}
stklist_make_nil
  {a:vt0p}((*void*)):<!wrt> stklist(a, 0)
//
(* ****** ****** *)
//
fun{}
stklist_getfree
  {a:vt0p}{n:int}
  (stk: stklist(INV(a), n)):<!wrt> list_vt(a, n)
//
(* ****** ****** *)
//
fun{}
stklist_is_nil
  {a:vt0p}{n:int}
  (stk: !stklist(INV(a), n)):<> bool(n==0)
fun{}
stklist_isnot_nil
  {a:vt0p}{n:int}
  (stk: !stklist(INV(a), n)):<> bool(n > 0)
//
(* ****** ****** *)

fun
{a:vt0p}
stklist_insert
  {n:int}
(
  stk: !stklist(INV(a), n) >> stklist(a, n+1), x0: a
) :<!wrt> void // endfun

(* ****** ****** *)
//
fun
{a:vt0p}
stklist_takeout
  {n:int | n > 0}
(
  stk: !stklist(INV(a), n) >> stklist(a, n-1)
) :<!wrt> (a) // endfun
//
fun
{a:vt0p}
stklist_takeout_opt
  (stk: !stklist(INV(a)) >> _):<!wrt> Option_vt(a)
// end of [stklist_takeout_opt]
//
(* ****** ****** *)

(* end of [stklist.sats] *)

(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-2013 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.
*)

(* ****** ****** *)

(*
**
** An array-based stack implementation
**
*)

(* ****** ****** *)

(*
**
** Author: Hongwei Xi
** Start time: September, 2013
** Authoremail: gmhwxiATgmailDOTcom
**
*)

(* ****** ****** *)
//
#define
ATS_PACKNAME
"ATSLIB.libats.stkarray"
//
// HX-2017-03-28:
#define // prefix for external
ATS_EXTERN_PREFIX "atslib_" // names
//
(* ****** ****** *)

%{#
//
#include "libats/CATS/stkarray.cats"
//
%} // end of [%{#]

(* ****** ****** *)
//
absvtype
stkarray_vtype
  (a: vt@ype+, m: int, n: int) = ptr
//
(* ****** ****** *)
//
stadef
stkarray = stkarray_vtype
//
vtypedef
stkarray
(
  a:vt0p
) = [m,n:int] stkarray_vtype (a, m, n)
//
(* ****** ****** *)

abst@ype
stkarray_tsize = $extype"atslib_stkarray_struct"

(* ****** ****** *)

praxi
lemma_stkarray_param
  {a:vt0p}{m,n:int}
  (!stkarray(INV(a), m, n)): [m >= n; n >= 0] void
// end of [lemma_stkarray_param]

(* ****** ****** *)

fun{a:vt0p}
stkarray_make_cap
  {m:int} (cap: size_t(m)):<!wrt> stkarray(a, m, 0)
// end of [stkarray_make_cap]

(* ****** ****** *)

fun
stkarray_make_ngc_tsz
  {a:vt0p}
  {l:addr}{m:int}
(
  stkarray_tsize? @ l
| ptr(l), arrayptr(a?, m), size_t(m), sizeof_t(a)
) :<!wrt> (mfree_ngc_v (l) | stkarray(a, m, 0)) = "mac#%"

(* ****** ****** *)
//
fun
stkarray_free_nil
  {a:vt0p}{m:int}
  (stk: stkarray(a, m, 0)):<!wrt> void = "mac#%"
// end of [stkarray_free_nil]
//
fun
stkarray_getfree_arrayptr
  {a:vt0p}{m,n:int}
  (stkarray(INV(a), m, n)):<!wrt> arrayptr(a, n) = "mac#%"
// end of [stkarray_getfree_arrayptr]
//
(* ****** ****** *)
//
fun{a:vt0p}
stkarray_get_size
  {m,n:int} (stk: !stkarray(INV(a), m, n)):<> size_t(n)
fun{a:vt0p}
stkarray_get_capacity
  {m,n:int} (stk: !stkarray(INV(a), m, n)):<> size_t(m)
//
(* ****** ****** *)

fun
stkarray_get_ptrbeg{a:vt0p}
  {m,n:int} (stk: !stkarray(INV(a), m, n)):<> Ptr1 = "mac#%"
// end of [stkarray_get_ptrbeg]

(* ****** ****** *)
//
fun
stkarray_is_nil
  {a:vt0p}{m,n:int}
  (stk: !stkarray(INV(a), m, n)):<> bool(n==0) = "mac#%"
fun
stkarray_isnot_nil
  {a:vt0p}{m,n:int}
  (stk: !stkarray(INV(a), m, n)):<> bool(n > 0) = "mac#%"
//
(* ****** ****** *)
//
fun
stkarray_is_full
  {a:vt0p}{m,n:int}
  (stk: !stkarray(INV(a), m, n)):<> bool(m==n) = "mac#%"
fun
stkarray_isnot_full
  {a:vt0p}{m,n:int}
  (stk: !stkarray(INV(a), m, n)):<> bool(m > n) = "mac#%"
//
(* ****** ****** *)

fun{}
fprint_stkarray$sep(out: FILEref): void
fun{a:vt0p}
fprint_stkarray
  (out: FILEref, stk: !stkarray(INV(a))): void
fun{a:vt0p}
fprint_stkarray_sep
  (out: FILEref, stk: !stkarray(INV(a)), sep: string): void
overload fprint with fprint_stkarray
overload fprint with fprint_stkarray_sep

(* ****** ****** *)

fun{a:vt0p}
stkarray_insert
  {m,n:int | m > n}
(
  stk:
  !stkarray(INV(a), m, n) >> stkarray(a, m, n+1)
, elt: a
) :<!wrt> void // stkarray_insert

(* ****** ****** *)

fun{a:vt0p}
stkarray_insert_opt
  (stk: !stkarray(INV(a)) >> _, x0: a):<!wrt> Option_vt(a)
// end of [stkarray_insert_opt]

(* ****** ****** *)

fun{a:vt0p}
stkarray_takeout
  {m,n:int | n > 0}
(
  stk:
  !stkarray(INV(a), m, n) >> stkarray(a, m, n-1)
) :<!wrt> (a) // endfun

fun{a:vt0p}
stkarray_takeout_opt
  (stk: !stkarray(INV(a)) >> _):<!wrt> Option_vt(a)
// end of [stkarray_takeout_opt]

(* ****** ****** *)

fun{a:vt0p}
stkarray_getref_top
  {m,n:int | n > 0}
  (stk: !stkarray(INV(a), m, n)):<> cPtr1(a)
// end of [stkarray_getref_top]

(* ****** ****** *)
//
symintr stkarray_getref_at
//
fun{a:vt0p}
stkarray_getref_at_int
  {m,n:int}{i:nat | i < n}
  (stk: !stkarray(INV(a), m, n), i: int(i)):<> cPtr1(a)
//
fun{a:vt0p}
stkarray_getref_at_size
  {m,n:int}{i:nat | i < n}
  (stk: !stkarray(INV(a), m, n), i: size_t(i)):<> cPtr1(a)
//
overload stkarray_getref_at with stkarray_getref_at_int
overload stkarray_getref_at with stkarray_getref_at_size
//
(* ****** ****** *)
//
fun{
a:vt0p}{env:vt0p
} stkarray_foreach$cont(x: &a, env: &env): bool
fun{
a:vt0p}{env:vt0p
} stkarray_foreach$fwork(x: &a >> _, env: &(env) >> _): void
fun{
a:vt0p
} stkarray_foreach{m,n:int}
  (stk: !stkarray(INV(a), m, n)): sizeLte(n)
fun{
a:vt0p}{env:vt0p
} stkarray_foreach_env{m,n:int}
  (stk: !stkarray(INV(a), m, n), env: &(env) >> _): sizeLte(n)
//
(* ****** ****** *)

(* end of [stkarray.sats] *)

(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-2013 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 *)
(* Authoremail: hwxi AT cs DOT bu DOT edu *)
(* Start time: December, 2012 *)

(* ****** ****** *)

staload
UN = "prelude/SATS/unsafe.sats"

(* ****** ****** *)

staload "libats/SATS/qlist.sats"

(* ****** ****** *)

implement
{}(*tmp*)
qlist_make_nil
  () = pq where {
//
  val (
    pf, pfgc | p
  ) = ptr_alloc<qstruct> ()
//
  val pq = ptr2ptrlin (p)
  val () = qstruct_initize (!p)
//
  prval pfngc = qstruct_objfize (pf | pq)
  prval ((*freed*)) = mfree_gcngc_v_nullify (pfgc, pfngc)
//
} (* end of [qlist_make] *)

implement
{}(*tmp*)
qlist_free_nil
  {a}(pq) = () where
{
//
val () = __mfree(pq) where
{
  extern fun __mfree
    : qlist (a, 0) -<0,!wrt> void = "mac#atspre_mfree_gc"
} // end of [where] // end of [val]
//
} (* end of [qlist_free_nil] *)

(* ****** ****** *)

implement
{a}(*tmp*)
qlist_insert
  (pq, x) = let
//
val nx =
mynode_make_elt<a>(x) in qlist_insert_ngc<a>(pq, nx)
//
end // end of [qlist_insert]

implement
{a}(*tmp*)
qstruct_insert
  (que, x) = let
//
val pq = addr@(que)
val pq2 = ptr2ptrlin(pq)
//
prval
pfngc =
qstruct_objfize(view@(que)|pq2)
//
val () = qlist_insert<a>(pq2, x)
//
prval pfat = qstruct_unobjfize(pfngc | pq, pq2)
//
prval () =
  (view@(que) := pfat)
//
prval () = ptrlin_free(pq2)
//
in
  // nothing
end // end of [qstruct_insert]

(* ****** ****** *)

implement
{a}(*tmp*)
qlist_takeout(pq) = let
//
val nx0 =
qlist_takeout_ngc(pq) in mynode_getfree_elt<a>(nx0)
//
end // end of [qlist_takeout]

implement
{a}(*tmp*)
qlist_takeout_opt(pq) =
(
if qlist_isnot_nil(pq)
  then Some_vt{a}(qlist_takeout(pq)) else None_vt{a}()
// end of [if]
) // end of [qlist_takeout_opt]

(* ****** ****** *)

implement
{a}(*tmp*)
qstruct_takeout
  (que) = res where
{
//
val pq = addr@(que)
val pq2 = ptr2ptrlin(pq)
//
prval
pfngc =
qstruct_objfize(view@(que)|pq2)
//
val res = qlist_takeout<a>(pq2)
//
prval pfat = qstruct_unobjfize(pfngc | pq, pq2)
//
prval () =
  (view@(que) := pfat)
//
prval () = ptrlin_free(pq2)
//
} // end of [qstruct_takeout]

(* ****** ****** *)

stadef mykind = $extkind"atslib_qlist"

(* ****** ****** *)

datavtype
qlist_data(a:vt@ype+) = QLIST of (ptr, ptr)

(* ****** ****** *)

assume
qlist_vtype(a: vt0p, n: int) = qlist_data(a)

(* ****** ****** *)

implement
{a}(*tmp*)
qlist_is_nil
  {n} (pq) = let
//
val+@QLIST (nxf, p_nxr) = pq
val isnil = (addr@(nxf) = p_nxr)
prval () = fold@ (pq)
//
in
  $UN.cast{bool(n==0)}(isnil)
end // end of [qlist_is_nil]

implement
{a}(*tmp*)
qlist_isnot_nil
  {n} (pq) = let
//
val+@QLIST (nxf, p_nxr) = pq
val isnot = (addr@(nxf) != p_nxr)
prval ((*prf*)) = fold@ (pq)
//
in
  $UN.cast{bool(n > 0)}(isnot)
end // end of [qlist_isnot_nil]

(* ****** ****** *)

implement
{a}(*tmp*)
qlist_length
  {n} (pq) = let
//
implement
{a}{ env }
qlist_foreach$cont(x, env) = true
implement
qlist_foreach$fwork<a><int>(x, env) = env := env+1
//
var env: int = (0)
//
val () =
  $effmask_all(qlist_foreach_env<a><int>(pq, env))
//
in
  $UN.cast{int(n)}(env)
end // end of [qlist_length]

(* ****** ****** *)

implement
{}(*tmp*)
fprint_qlist$sep
  (out) = fprint_string (out, "->")
//
implement
{a}(*tmp*)
fprint_qlist
  (out, pq) = let
//
implement
{a}{ env }
qlist_foreach$cont
  (x, env) = true
//
implement
qlist_foreach$fwork<a><int>
  (x0, env) = let
  val () =
  if env > 0
    then fprint_qlist$sep<>(out)
  // end of [if]
  val () = (env := env + 1)
  val () = fprint_ref<a>(out, x0)
in
  // nothing
end // end of [qlist_foreach$fwork]
//
var env: int = 0
//
in
  qlist_foreach_env<a><int>(pq, env)
end // end of [fprint_qlist]

(* ****** ****** *)

implement
{a}(*tmp*)
fprint_qlist_sep
  (out, pq, sep) = let
//
implement
{}(* tmp *)
fprint_qlist$sep (out) = fprint_string (out, sep)
//
in
  fprint_qlist<a> (out, pq)
end // end of [fprint_qlist_sep]

(* ****** ****** *)

implement
{a}{ env }
qlist_foreach$cont(_x_, env) = true

implement
{a}(*tmp*)
qlist_foreach(pq) = let
//
var
env: void = () in qlist_foreach_env<a><void>(pq, env)
//
end // end of [qlist_foreach]

implement
{a}{ env }
qlist_foreach_env
  (pq, env) = let
//
fun loop
(
  p_nxf: ptr, p_nxr: ptr, env: &env
) : void = let
in
//
if p_nxf != p_nxr then let
//
val xs =
  $UN.ptr0_get<List1_vt(a)>(p_nxf)
// end of [val]
val+@list_vt_cons(x1, xs2) = xs
//
val test =
  qlist_foreach$cont<a><env>(x1, env)
//
val () =
(
//
if
test
then let
//
val () =
qlist_foreach$fwork<a><env>(x1, env)
//
in
  loop(addr@(xs2), p_nxr, env)
end // end of [then] // end of [if]
//
) : void // end of [val]
//
prval ((*proof*)) = fold@ (xs)
prval ((*proof*)) = $UN.cast2void(xs)
//
in
  // nothing
end else () // end of [if]
//
end // end of [loop]
//
val+@QLIST(nxf, p_nxr) = pq
//
val () = loop(addr@(nxf), p_nxr, env)
//
prval ((*folded*)) = fold@(pq)
//
in
  // nothing
end // end of [qlist_foreach_env]

(* ****** ****** *)

implement
{}(* tmp *)
qstruct_initize
  {a}(que) = let
//
val pq =
$UN.castvwtp0
  {qlist(a,0)}(addr@(que))
// end of [val]
//
val+@QLIST(nxf, p_nxr) = pq
val () = (p_nxr := addr@ (nxf))
//
prval () = fold@(pq)
//
prval () =
__assert(que, pq) where
{
  extern praxi
    __assert (que: &qstruct? >> qstruct(a, 0), pq: qlist(a, 0)): void
  // end of [extern]
} // end of [where] // end of [prval]
//
in
  (* DoNothing *)
end // end of [qstruct_initize]

(* ****** ****** *)

extern
castfn
mynode1_encode
  {a:vt0p}
  (xs: List1_vt(INV(a))):<> mynode1(a)
// end of [mynode1_encode]
extern
castfn
mynode1_decode
  {a:vt0p}
  (nx: mynode1(INV(a))):<> List1_vt(a)
// end of [mynode1_decode]

(* ****** ****** *)

implement
{}(*tmp*)
mynode_null{a}() =
  $UN.castvwtp0{mynode(a,null)}(list_vt_nil)
// end of [mynode_null]

(* ****** ****** *)

implement
{a}(*tmp*)
mynode_make_elt (x) =
  $UN.castvwtp0{mynode1(a)}(list_vt_cons{a}{0}(x, _))
// end of [mynode_make_elt]

implement
{a}(*tmp*)
mynode_free_elt
  (nx, res) = () where
{
//
val xs =
  mynode1_decode(nx)
//
val+~list_vt_cons(x1, xs2) = xs
//
val () = (res := x1)
//
prval () =
__assert (xs2) where {
  extern praxi __assert : {vt:vtype} (vt) -<prf> void
} // end of [where] // end of [prval]
//
} (* end of [mynode_free_elt] *)

(* ****** ****** *)

implement
{a}(*tmp*)
mynode_getfree_elt
  (nx) = (x1) where
{
//
val xs =
  mynode1_decode(nx)
//
val+~list_vt_cons(x1, xs2) = xs
//
prval () =
__assert(xs2) where {
  extern praxi __assert : {vt:vtype} (vt) -<prf> void
} // end of [where] // end of [prval]
//
} (* end of [mynode_getfree_elt] *)

(* ****** ****** *)

implement
{a}(*tmp*)
qlist_insert_ngc
  (pq, nx0) = let
//
val+@QLIST(nxf, p_nxr) = pq
//
val xs = mynode1_decode(nx0)
val+@list_vt_cons(_, xs2) = xs
//
val p2_nxr = addr@(xs2)
prval ((*folded*)) = fold@(xs)
//
val nx0 = mynode1_encode(xs)
//
val () = $UN.ptr0_set<mynode1(a)>(p_nxr, nx0)
//
val () = (p_nxr := p2_nxr)
//
prval ((*folded*)) = fold@ (pq)
//  
in
  // nothing
end // end of [qlist_insert_ngc]

(* ****** ****** *)

implement
{a}(*tmp*)
qlist_takeout_ngc
  (q0) = nx0 where
{
//
val+@QLIST(nxf, p_nxr) = q0
//
val nx0 =
$UN.castvwtp0{mynode1(a)}(nxf)
//
val xs = mynode1_decode(nx0)
val+@list_vt_cons (_, xs2) = xs
//
val p2_nxr = addr@(xs2)
prval ((*folded*)) = fold@(xs)
//
val nx0 = mynode1_encode(xs)
//
val () =
(
//
if
(p_nxr != p2_nxr)
then
(
nxf := $UN.ptr0_get<ptr>(p2_nxr)
) (* end of [then] *)
else p_nxr := addr@(nxf)
//
) : void // end of [val]
//
prval ((*folded*)) = fold@ (q0)
//
} // end of [qlist_takeout_ngc]

(* ****** ****** *)

implement
{}(* tmp *)
qlist_takeout_list
  {a}{n}(pq) = xs where
{
//
val+@QLIST(nxf, p_nxr) = pq
//
val () =
$UN.ptr0_set<ptr>(p_nxr, the_null_ptr)
//
val xs = $UN.castvwtp0{list_vt(a,n)}(nxf)
//
val () = p_nxr := addr@(nxf)
//
prval ((*folded*)) = fold@(pq)
//
} // end of [qlist_takeout_list]

implement
{}(* tmp *)
qstruct_takeout_list
  {a}{n}(que) = xs where
{
//
val pq = addr@(que)
val pq2 = ptr2ptrlin (pq)
//
prval
pfngc =
qstruct_objfize(view@(que)|pq2)
//
val xs = qlist_takeout_list(pq2)
prval pfat = qstruct_unobjfize(pfngc | pq, pq2)
//
prval () =
  (view@(que) := pfat)
//
prval () = ptrlin_free (pq2)
//
} (* end of [qstruct_takeout_list] *)

(* ****** ****** *)

(* end of [qlist.dats] *)

(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-2013 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 *)
(* Authoremail: hwxi AT cs DOT bu DOT edu *)
(* Start time: March, 2013 *)

(* ****** ****** *)

staload
UN = "prelude/SATS/unsafe.sats"

(* ****** ****** *)

staload "libats/SATS/gnode.sats"

(* ****** ****** *)

staload "libats/SATS/sllist.sats"

(* ****** ****** *)

#define nullp the_null_ptr

(* ****** ****** *)
//
extern
fun{a:vt0p}
g2node_make_elt
  (x: a):<!wrt> g2node1(a)
//
(* ****** ****** *)
//
extern
fun{a:t0p} // [a] is nonlinear
g2node_free
  (nx: g2node1(INV(a))):<!wrt> void
//
extern
fun{a:vt0p} // [a] may be linear
g2node_freelin
  (nx: g2node1(INV(a))):<!wrt> void
//
(* ****** ****** *)
//
extern
fun{a:vt0p}
g2node_free_elt
(
nx: g2node1(INV(a)), res: &(a?) >> a
) :<!wrt> void // end-of-function
//
extern
fun{a:vt0p}
g2node_getfree_elt(nx: g2node1(INV(a))):<!wrt>(a)
//
(* ****** ****** *)
//
extern
castfn
sllist0_encode
{a:vt0p}{n:int}
  (nx: g2node0(INV(a))) :<> sllist(a, n)
extern
castfn
sllist0_decode
{a:vt0p}{n:int}
  (xs: sllist(INV(a), n)) :<> g2node0(a)
//
extern
castfn
sllist1_encode
{a:vt0p}{n:int | n > 0}
  (nx: g2node1(INV(a))) :<> sllist(a, n)
extern
castfn
sllist1_decode
{a:vt0p}{n:int | n > 0}
  (xs: sllist(INV(a), n)) :<> g2node1(a)
//
(* ****** ****** *)
//
implement
{}(*tmp*)
sllist_nil() = sllist0_encode(gnode_null())
//
implement
{a}(*tmp*)
sllist_sing(x) = sllist_cons<a>(x, sllist_nil())
//
(* ****** ****** *)

implement
{a}(*tmp*)
sllist_cons
  (x, xs) = let
//
val nx =
g2node_make_elt<a>(x) in sllist_cons_ngc<a>(nx, xs)
//
end // end of [sllist_cons]

implement{a}
sllist_uncons
  (xs) = let
//
val nx0 =
sllist_uncons_ngc<a>(xs) in g2node_getfree_elt<a>(nx0)
//
end // end of [sllist_uncons]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_snoc
  (xs, x) = let
//
val nx = g2node_make_elt<a> (x) in sllist_snoc_ngc (xs, nx)
//
end // end of [sllist_snoc]

implement{a}
sllist_unsnoc
  (xs) = let
//
val nx0 = sllist_unsnoc_ngc (xs) in g2node_getfree_elt<a> (nx0)
//
end // end of [sllist_unsnoc]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_make_list
  {n}(xs) = let
//
fun loop (
  nx0: g2node1 (a), xs: List (a)
) : void = let
in
//
case+ xs of
| list_cons
    (x, xs) => let
    val nx1 = g2node_make_elt<a> (x)
    val () = gnode_link11 (nx0, nx1)
  in
    loop (nx1, xs)
  end // end of [loop]
| list_nil () => let
    val () = gnode_set_next_null (nx0)
  in
    // nothing
  end // end of [list_nil]
//
end // end of [loop]
//
in
//
case+ xs of
| list_cons
    (x, xs) => let
    val nx0 = g2node_make_elt<a> (x)
    val () = $effmask_all (loop (nx0, xs))
  in
    sllist0_encode (nx0)
  end // end of [list_cons]
| list_nil () => sllist_nil ()
//
end // end of [sllist_make_list]

(* ****** ****** *)
//
implement
{a}(*tmp*)
sllist_make_list_vt
  {n}(xs) = $UN.castvwtp0{sllist(a,n)}(xs)
//
(* ****** ****** *)

implement
{}(*tmp*)
sllist_is_nil
  {a}{n} (xs) = let
  val nxs = $UN.castvwtp1{g2node0(a)}(xs)
in
  $UN.cast{bool(n==0)}(gnodelst_is_nil (nxs))
end // end of [sllist_is_nil]

implement
{}(*tmp*)
sllist_is_cons
  {a}{n} (xs) = let
  val nxs = $UN.castvwtp1{g2node0(a)}(xs)
in
  $UN.cast{bool(n > 0)}(gnodelst_is_cons (nxs))
end // end of [sllist_is_cons]

(* ****** ****** *)

(*
fun{a:vt0p}
sllist_length
  {n:int} (xs: !sllist (INV(a), n)):<> int (n)
*)
implement
{a}(*tmp*)
sllist_length
  {n} (xs) = let
//
val nxs = $UN.castvwtp1{g2node0(a)}(xs)
//
in
  $UN.cast{int(n)}(gnodelst_length (nxs))
end // end of [sllist_length]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_get_elt
  (xs) = let
  val p_elt =
    sllist_getref_elt (xs) in $UN.cptr_get<a> (p_elt)
  // end of [val]
end // end of [sllist_get_elt]

implement
{a}(*tmp*)
sllist_set_elt
  (xs, x0) = let
  val p_elt = 
    sllist_getref_elt (xs) in $UN.cptr_set<a> (p_elt, x0)
  // end of [val]
end // end of [sllist_set_elt]

implement
{a}(*tmp*)
sllist_getref_elt (xs) = let
  val nxs =
    $UN.castvwtp1{g2node1(a)}(xs) in gnode_getref_elt (nxs)
  // end of [val]
end // end of [sllist_getref_elt]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_getref_next (xs) = let
  val nxs =
    $UN.castvwtp1{g2node1(a)}(xs) in cptr2ptr (gnode_getref_next (nxs))
  // end of [val]  
end // end of [sllist_getref_next]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_get_elt_at
  (xs, i) = let
  val p_elt =
    sllist_getref_elt_at (xs, i) in $UN.cptr_get<a> (p_elt)
  // end of [val]
end // end of [sllist_get_elt_at]

implement
{a}(*tmp*)
sllist_set_elt_at
  (xs, i, x0) = let
  val p_elt = 
    sllist_getref_elt_at (xs, i) in $UN.cptr_set<a> (p_elt, x0)
  // end of [val]
end // end of [sllist_set_elt_at]

implement
{a}(*tmp*)
sllist_getref_elt_at
  (xs, i) = let
//
fun loop
(
  nxs: g2node1 (a), i: int
) : g2node1 (a) =
  if i > 0 then let
    val nxs = gnode_get_next (nxs)
  in
    loop ($UN.cast{g2node1(a)}(nxs), i-1)
  end else nxs // end of [if]
//
val nxs0 = $UN.castvwtp1{g2node1(a)}(xs)
val nxs_i = $effmask_all (loop (nxs0, i))
//
in
  gnode_getref_elt (nxs_i) 
end // end of [sllist_getref_elt_at]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_getref_at (xs, i) = let
//
fun loop (
  p: Ptr1, i: int
) : Ptr1 = let
in
  if i > 0 then let
    val nx =
      $UN.ptr1_get<g2node1(a)> (p)
    // end of [val]
    val p2 = gnode_getref_next (nx)
  in
    loop (cptr2ptr (p2), i-1)
  end else (p) // end of [if]
end // end of [loop]
//
val p0 = $UN.cast{Ptr1}(addr@(xs))
//
in
  $effmask_all (loop (p0, i))
end // end of [sllist_getref_at]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_insert_at
  {n} (xs, i, x0) = let
  var xs = xs
  val p_i = sllist_getref_at (xs, i)
  val nx0 = g2node_make_elt<a> (x0)
  val nxs = $UN.ptr1_get<g2node0(a)> (p_i)
  val () = gnode_link10 (nx0, nxs)
  val () = $UN.ptr1_set<g2node1(a)> (p_i, nx0)
in
  $UN.castvwtp0{sllist(a, n+1)}(xs)
end // end of [sllist_insert_at]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_takeout_at
  {n} (xs, i) = let
  val p_i = sllist_getref_at (xs, i)
  val nxs = $UN.ptr1_get<g2node1(a)> (p_i)
  val nx0 = nxs
  val nxs = gnode_get_next (nx0)
  val () = $UN.ptr1_set<g2node0(a)> (p_i, nxs)
  prval (
  ) = __assert (xs) where {
    extern praxi __assert (xs: &sllist (a, n) >> sllist (a, n-1)): void
  } // end of [where] // end of [prval]
in
  g2node_getfree_elt (nx0)
end // end of [sllist_takeout_at]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_append
  {n1,n2} (xs1, xs2) = let
//
prval() = lemma_sllist_param(xs1)
prval() = lemma_sllist_param(xs2)
//
val iscons1 = sllist_is_cons(xs1)
//
in
//
if
iscons1
then let
  val iscons2 = sllist_is_cons(xs2)
in
//
if iscons2 then let
  val nxs1 = sllist1_decode (xs1)
  val nxs2 = sllist0_decode (xs2)
  val nxs1_end = gnodelst_next_all (nxs1)
  val _void_ = gnode_link10 (nxs1_end, nxs2)
in
  sllist0_encode (nxs1)
end else let
  prval () = sllist_free_nil (xs2) in xs1
end // end of [if]
//
end else let
  prval () = sllist_free_nil (xs1) in xs2
end // end of [if]
//
end // end of [sllist_append]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_reverse (xs) = let
in
  sllist_reverse_append (xs, sllist_nil ())
end // end of [sllist_reverse]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_reverse_append
  (xs1, xs2) = let
//
fun loop
(
  nxs: g2node0 (a), res: g2node1 (a)
) : g2node1 (a) = let
  val iscons = gnodelst_is_cons (nxs)
in
//
if
iscons
then let
  val nx0 = nxs
  val nxs = gnode_get_next (nx0)
  val () = gnode_link11 (nx0, res)
in
  loop (nxs, nx0)
end else res // end of [if]
//
end // end of [loop]
//
prval (
) = lemma_sllist_param (xs1)
//
val iscons = sllist_is_cons (xs1)
//
in
//
if
iscons
then let
  val nxs1 = sllist1_decode (xs1)
  val nx0 = nxs1
  val nxs1 = gnode_get_next (nx0)
  val () = gnode_link10 (nx0, sllist0_decode (xs2))
in
  sllist0_encode ($effmask_all (loop (nxs1, nx0)))
end else let
  prval () = sllist_free_nil (xs1)
in
  xs2
end // end of [if]
//
end // end of [sllist_reverse_append]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_free
  (xs) = let
//
fun
loop
(
  nxs: g2node0(a)
) : void = let
//
val
iscons =
gnodelst_is_cons(nxs)
//
in
//
if
iscons
then let
  val nxs2 =
    gnode_get_next(nxs)
  // end of [val]
  val () = g2node_free<a>(nxs)
in
  loop(nxs2)
end else () // end of [if]
//
end // end of [loop]
//
val nxs = sllist0_decode(xs)
//
in
  $effmask_all (loop(nxs))
end // end of [sllist_free]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_freelin
  (xs) = let
//
implement
(a2)(*tmp*)
gclear_ref<a2>(x0) =
{
prval () = $UN.castview2void_at(view@x0)
  val () = sllist_freelin$clear<a>(x0)
prval () = $UN.castview2void_at(view@x0)
} (* gclear_ref *)
//
fun
loop
(
  nxs: g2node0(a)
) : void = let
//
val
iscons =
gnodelst_is_cons(nxs)
//
in
//
if
iscons
then let
  val nxs2 =
    gnode_get_next(nxs)
  // end of [val]
  val () = g2node_freelin<a>(nxs)
in
  loop(nxs2)
end else () // end of [if]
//
end // end of [loop]
//
val nxs = sllist0_decode(xs)
//
in
  $effmask_all(loop(nxs))
end // end of [sllist_freelin]

(* ****** ****** *)

implement
{a}{b}
sllist_map{n}(xs) = let
//
fun
loop
(
  nxs: g2node0(a), p_res: ptr
) : void = let
//
val
iscons = gnodelst_is_cons(nxs)
//
in
//
if
iscons
then let
  val nx = nxs
  val nxs = gnode_get_next(nx)
  val p_x = gnode_getref_elt(nx)
  val (pf, fpf | p_x) = $UN.cptr_vtake{a}(p_x)
  val y = sllist_map$fopr<a><b>(!p_x)
prval ((*returned*)) = fpf(pf)
  val ny = g2node_make_elt<b>(y)
  val () = $UN.ptr0_set<g2node1(b)>(p_res, ny)
  val p_res = gnode_getref_next(ny)
in
  loop (nxs, cptr2ptr(p_res))
end else () // end of [if]
//
end (* end of [loop] *)
//
var res: ptr
val () = loop ($UN.castvwtp1{g2node0(a)}(xs), addr@(res))
//
in
  $UN.castvwtp0{sllist(b,n)}(res)
end (* end of [sllist_map] *)

(* ****** ****** *)

(*
fun{
a:vt0p}{env:vt0p
} sllist_foreach_env
  (xs: !Sllist (INV(a)), env: &env >> _): void
*)
implement
{a}{env}
sllist_foreach_env
  (xs, env) = let
//
fun loop (
  nxs: g2node0 (a), env: &env
) : void = let
  val iscons = gnodelst_is_cons (nxs)
in
//
if iscons then let
  val nx0 = nxs
  val nxs = gnode_get_next (nxs)
  val p_elt = gnode_getref_elt (nx0)
  val (pf, fpf | p_elt) = $UN.cptr_vtake {a} (p_elt)
  val test = sllist_foreach$cont (!p_elt, env)
in
  if test then let
    val () = sllist_foreach$fwork (!p_elt, env)
    prval () = fpf (pf)
  in
    loop (nxs, env)
  end else let
    prval () = fpf (pf)
  in
    // nothing
  end // end of [if]
end else () // end of [if]
//
end // end of [loop]
//
val nxs = $UN.castvwtp1{g2node0(a)}(xs)
//
in
  loop (nxs, env)
end // end of [sllist_foreach_env]

(* ****** ****** *)

implement
{}(*tmp*)
fprint_sllist$sep
  (out) = fprint_string (out, "->")
implement
{a}(*tmp*)
fprint_sllist (out, xs) = let
//
fun loop (
  out: FILEref, nxs: g2node0 (a), i: int
) : void = let
  val iscons = gnodelst_is_cons (nxs)
in
//
if iscons then let
  val nx0 = nxs
  val nxs = gnode_get_next (nx0)
  val () =
    if i > 0 then fprint_sllist$sep (out)
  // end of [val]
  val p_elt = gnode_getref_elt (nx0)
  val (pf, fpf | p_elt) = $UN.cptr_vtake {a} (p_elt)
  val () = fprint_ref (out, !p_elt)
  prval () = fpf (pf)
in
  loop (out, nxs, i+1)
end // end of [if]
//
end // end of [loop]
//
val nxs = $UN.castvwtp1{g2node0(a)}(xs)
//
in
  loop (out, nxs, 0)
end // end of [fprint_sllist]

(* ****** ****** *)

datavtype
slnode_vtype
  (a:vt@ype+) = SLNODE of (a, ptr(*next*))
// end of [slnode_vtype]

(* ****** ****** *)

vtypedef slnode (a:vt0p) = slnode_vtype (a)

(* ****** ****** *)

extern
praxi slnode_vfree {a:vt0p} (nx: slnode (a)): void
extern
castfn
g2node_decode {a:vt0p} (nx: g2node1 (INV(a))):<> slnode (a)
extern
castfn
g2node_encode {a:vt0p} (nx: slnode (INV(a))):<> g2node1 (a)

(* ****** ****** *)

implement
{a}(*tmp*)
g2node_make_elt
  (x) = let
in
  $UN.castvwtp0{g2node1(a)}(SLNODE{a}(x, _))
end // end of [g2node_make_elt]

(* ****** ****** *)
//
implement
{a}(*tmp*)
g2node_free(nx) = let
  val nx =
    g2node_decode (nx)
  // end of [val]
  val+~SLNODE (_, _) = (nx) in (*nothing*)
end // end of [g2node_free]
//
implement
{a}(*tmp*)
g2node_freelin(nx) = let
  val nx =
    g2node_decode (nx)
  // end of [val]
  val+@SLNODE(x0, _) = (nx)
  val ((*freed*)) = gclear_ref<a>(x0) in free@{a}(nx)
end // end of [g2node_free]
//
(* ****** ****** *)

implement
{a}(*tmp*)
g2node_free_elt
  (nx, res) = let
  val nx = g2node_decode (nx)
  val~SLNODE (x, _) = (nx); val () = res := x in (*nothing*)
end // end of [g2node_free_elt]

implement
{a}(*tmp*)
g2node_getfree_elt
  (nx) = let
  val nx = g2node_decode (nx)
  val~SLNODE (x, _) = (nx) in x
end // end of [g2node_getfree_elt]

(* ****** ****** *)

implement(a)
gnode_getref_elt<mytkind><a>
  (nx) = let
//
val nx = g2node_decode (nx)
//
val+@SLNODE (elt, _) = nx
val p_elt = addr@ (elt)
prval () = fold@ (nx)
prval () = slnode_vfree (nx)
//
in
  $UN.cast{cPtr1(a)}(p_elt)
end // end of [gnode_getref_elt]

(* ****** ****** *)

implement(a)
gnode_getref_next<mytkind><a>
  (nx) = let
//
val nx = g2node_decode (nx)
//
val+@SLNODE (_, next) = nx
val p_next = addr@ (next)
prval () = fold@ (nx)
prval () = slnode_vfree (nx)
//
in
  $UN.cast{cPtr1(g2node0(a))}(p_next)
end // end of [gnode_getref_next]

(* ****** ****** *)

implement(a)
gnode_link10<mytkind><a>
  (nx1, nx2) = gnode_set_next (nx1, nx2)
// end of [gnode_link10]

implement(a)
gnode_link11<mytkind><a>
  (nx1, nx2) = gnode_set_next (nx1, nx2)
// end of [gnode_link11]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_cons_ngc
  (nx0, xs) = let
//
val nxs = sllist0_decode (xs)
val _void_ = gnode_link10 (nx0, nxs)
//
in
  sllist0_encode (nx0)
end // end of [sllist_cons_ngc]

implement
{a}(*tmp*)
sllist_uncons_ngc
  (xs) = let
//
val nxs = sllist1_decode (xs)
val nxs2 = gnode_get_next (nxs)
val _void_ = xs := sllist0_encode (nxs2)
//
in
  nxs
end // end of [sllist_uncons_ngc]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_snoc_ngc
  {n} (xs, nx0) = let
//
vtypedef res = sllist(a,n+1)
//
val () = gnode_set_next_null (nx0)
//
val nxs = sllist0_decode (xs)
val iscons = gnodelst_is_cons (nxs)
//
in
//
if iscons then let
//
val nx_end = gnodelst_next_all (nxs)
val _void_ = gnode_link11 (nx_end, nx0)
//
in
  $UN.castvwtp0{res}(nxs)
end else
  $UN.castvwtp0{res}(nx0)
// end of [if]
//
end // end of [sllist_snoc_ngc]

(* ****** ****** *)

implement
{a}(*tmp*)
sllist_unsnoc_ngc
  {n} (xs) = let
//
fun loop
(
  xs: &Sllist1 (a) >> Sllist0(a)
) : g2node1(a) = let
//
val p = sllist_getref_next (xs)
//
val (pf, fpf | p) = $UN.ptr_vtake{Sllist0(a)}(p)
//
val iscons = sllist_is_cons (!p)
//
in
//
if iscons
  then let
    val res = loop (!p)
    prval () = fpf (pf) in res
  end // end of [then]
  else let
    prval () = fpf (pf)
    val nx = $UN.castvwtp0{g2node1(a)}(xs)
    val () = xs := sllist_nil{a}((*void*)) in nx
  end // end of [else]
// end of [if]
//
end (* end of [loop] *)
//
val res = $effmask_all (loop (xs))
//
prval [l:addr] EQADDR () = eqaddr_make_ptr (addr@xs)
//
prval () = view@xs := $UN.castview0{sllist(a,n-1)@l}(view@xs)
//
in
  res
end // end of [sllist_unsnoc_ngc]

(* ****** ****** *)

(* end of [sllist.dats] *)