ats2-lang 0.1.3-1 / usr / lib / ats2-postiats-0.1.3 / prelude / SATS / array.sats

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

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

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

(*
** Source:
** $PATSHOME/prelude/SATS/CODEGEN/array.atxt
** Time of generation: Fri Sep 26 22:20:50 2014
*)

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

(* Author: Hongwei Xi *)
(* Authoremail: hwxi AT cs DOT bu DOT edu *)
(* Start time: Feburary, 2012 *)

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

vtypedef
RD(a:vt0p) = a // for commenting: read-only
#define NSH (x) x // for commenting: no sharing
#define SHR (x) x // for commenting: it is shared

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

sortdef t0p = t@ype
sortdef vtp = viewtype
sortdef vt0p = viewt@ype

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

(*
//
// HX: [array_v] can also be defined as follows:
//
dataview
array_v
(
  a:vt@ype+, addr, int
) = // HX: for arry view
  | {l:addr}{n:int}
    array_v_cons (a, l, n+1) of (a @ l, array_v (a, l+sizeof a, n))
  | {l:addr} array_v_nil (a, l, 0)
// end of [array_v]
*)

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

dataview
arrayopt_v
(
  a:vt@ype+, addr, int, bool
) = // HX: for optional array view
  | {l:addr}{n:int}
    arrayopt_v_some (a, l, n, true) of array_v (a, l, n)
  | {l:addr}{n:int}
    arrayopt_v_none (a, l, n, false) of array_v (a?, l, n)
// end of [arrayopt_v]

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

exception
ArraySubscriptExn of ()
(*
fun ArraySubscriptExn ():<> exn = "mac#%ArraySubscriptExn_make"
fun isArraySubscriptExn (x: !exn):<> bool = "mac#%isArraySubscriptExn"
macdef
ifArraySubscriptExn
  {tres}(exn, body) =
(
let val x = ,(exn) in
(
if isArraySubscriptExn(x)
  then
    let prval () = __vfree_exn (x) in ,(body) end
  else $raise (x)
) : tres // end of [if]
end (* end of [let] *)
) // end of [ifArraySubscriptExn]
*)

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

praxi
lemma_array_param{a:vt0p}
  {l:addr}{n:int} (A: &(@[INV(a)][n])): [n >= 0] void
// end of [lemma_array_param]
praxi
lemma_array_v_param{a:vt0p}
  {l:addr}{n:int} (pf: !array_v (INV(a), l, n)): [n >= 0] void
// end of [lemma_array_v_param]

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

praxi array_v_nil :
  {a:vt0p}{l:addr} () -<prf> array_v (a, l, 0)
praxi array_v_unnil :
  {a:vt0p}{l:addr} array_v (a, l, 0) -<prf> void

prfun array_v_unnil_nil :
  {a1,a2:vt0p}{l:addr} array_v (a1, l, 0) -<prf> array_v (a2, l, 0)
// end of [array_v_unnil_nil]

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

praxi array_v_cons :
  {a:vt0p}{l:addr}{n:int}
  (a @ l, array_v (INV(a), l+sizeof(a), n)) -<prf> array_v (a, l, n+1)
praxi array_v_uncons :
  {a:vt0p}{l:addr}{n:int | n > 0}
  array_v (INV(a), l, n) -<prf> (a @ l, array_v (a, l+sizeof(a), n-1))

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

prfun array_v_sing
  {a:vt0p}{l:addr} (pf: INV(a) @ l): array_v (a, l, 1)
prfun array_v_unsing
  {a:vt0p}{l:addr} (pf: array_v (INV(a), l, 1)): a @ l

(* ****** ****** *)
//
fun{a:vt0p}
array_getref_at
  {n:int} (A: &RD(@[INV(a)][n]), i: sizeLt n):<> cPtr1 (a)
//
(* ****** ****** *)

fun{
a:t0p}{tk:tk
} array_get_at_gint
  {n:int} (A: &RD(@[INV(a)][n]), i: g1intLt (tk, n)):<> a
overload [] with array_get_at_gint of 0

fun{
a:t0p}{tk:tk
} array_get_at_guint
  {n:int} (A: &RD(@[INV(a)][n]), i: g1uintLt (tk, n)):<> a
overload [] with array_get_at_guint of 0

symintr array_get_at
overload array_get_at with array_get_at_gint of 0
overload array_get_at with array_get_at_guint of 0

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

fun{
a:t0p}{tk:tk
} array_set_at_gint
  {n:int} (A: &(@[INV(a)][n]), i: g1intLt (tk, n), x: a):<!wrt> void
overload [] with array_set_at_gint of 0

fun{
a:t0p}{tk:tk
} array_set_at_guint
  {n:int} (A: &(@[INV(a)][n]), i: g1uintLt (tk, n), x: a):<!wrt> void
overload [] with array_set_at_guint of 0

symintr array_set_at
overload array_set_at with array_set_at_gint of 0
overload array_set_at with array_set_at_guint of 0

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

fun{
a:vt0p}{tk:tk
} array_exch_at_gint{n:int}
(
  A: &(@[INV(a)][n]), i: g1intLt (tk, n), x: &a >> _
) :<!wrt> void
fun{
a:vt0p}{tk:tk
} array_exch_at_guint{n:int}
(
  A: &(@[INV(a)][n]), i: g1uintLt (tk, n), x: &a >> _
) :<!wrt> void

symintr array_exch_at
overload array_exch_at with array_exch_at_gint of 0
overload array_exch_at with array_exch_at_guint of 0

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

fun{a:vt0p}
array_interchange{n:int}
(
  A: &(@[INV(a)][n]), i: sizeLt (n), j: sizeLt (n)
) :<!wrt> void // end of [array_interchange]

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

fun{a:vt0p}
array_subcirculate{n:int}
(
  A: &(@[INV(a)][n]), i: sizeLt (n), j: sizeLt (n)
) :<!wrt> void // end of [array_subcirculate]

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

fun{a:vt0p}
array_ptr_takeout
  {l:addr}{n:int}{i:nat | i < n}
(
  array_v (INV(a), l, n) | ptr l, size_t i
) : (
  a @ (l+i*sizeof(a))
, a @ (l+i*sizeof(a)) -<lin,prf> array_v (a, l, n)
| ptr (l+i*sizeof(a))
) // end of [array_ptr_takeout]

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

fun{a:vt0p}
array_ptr_alloc
  {n:int}
(
  asz: size_t n
) :<!wrt> [l:agz]
(
  array_v (a?, l, n), mfree_gc_v (l) | ptr l
) // end of [array_ptr_alloc]

fun{}
array_ptr_free
  {a:vt0p}{l:addr}{n:int}
(
  array_v (a?, l, n), mfree_gc_v (l) | ptr l
) :<!wrt> void // end of [array_ptr_free]

(* ****** ****** *)
//
fun{}
fprint_array$sep (out: FILEref): void
//
fun{a:vt0p}
fprint_array_int{n:int}
(
  out: FILEref, A: &RD(@[INV(a)][n]), n: int(n)
) : void // end of [fprint_array_int]
fun{a:vt0p}
fprint_array_size{n:int}
(
  out: FILEref, A: &RD(@[INV(a)][n]), n: size_t(n)
) : void // end of [fprint_array_size]
//
symintr fprint_array
overload fprint_array with fprint_array_int
overload fprint_array with fprint_array_size
//
fun{a:vt0p}
fprint_array_sep{n:int}
(
  out: FILEref
, A: &RD(@[INV(a)][n]), n: size_t n, sep: NSH(string)
) : void // end of [fprint_array_sep]
//
(* ****** ****** *)

overload fprint with fprint_array
overload fprint with fprint_array_sep

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

fun{a:vt0p}
array_copy{n:int}
(
  to: &(@[a?][n]) >> @[a][n]
, from: &RD(@[INV(a)][n]) >> @[a?!][n]
, n: size_t (n)
) :<!wrt> void // end of [array_copy]

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

fun{a:t0p}
array_copy_from_list{n:int}
(
  A: &(@[a?][n]) >> @[a][n], xs: list (INV(a), n)
) :<!wrt> void // end of [array_copy_from_list]

fun{a:vt0p}
array_copy_from_list_vt{n:int}
(
  A: &(@[a?][n]) >> @[a][n], xs: list_vt (INV(a), n)
) :<!wrt> void // end of [array_copy_from_list_vt]

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

fun{a:vt0p}
array_copy_to_list_vt{n:int}
(
  A: &RD(@[INV(a)][n]) >> @[a?!][n], n: size_t n
) :<!wrt> list_vt (a, n) // endfun

macdef array2list = array_copy_to_list_vt

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

fun{a:vt0p}
array_tabulate$fopr (i: size_t): (a)
fun{a:vt0p}
array_ptr_tabulate
  {n:int} (asz: size_t n)
  : [l:addr] (array_v (a, l, n), mfree_gc_v (l) | ptr l)
// end of [arrayptr_tabulate]

(* ****** ****** *)
//
fun{
a:vt0p
} array_foreach{n:int}
(
  A: &(@[INV(a)][n]) >> @[a][n], asz: size_t n
) : sizeLte (n) // end of [array_foreach]
//
fun{
a:vt0p}{env:vt0p
} array_foreach_env{n:int}
(
  A: &(@[INV(a)][n]) >> @[a][n], asz: size_t n, env: &(env) >> _
) : sizeLte (n) // end of [array_foreach_env]
//
fun{
a:vt0p}{env:vt0p
} array_foreach$cont (x: &a, env: &env): bool
fun{
a:vt0p}{env:vt0p
} array_foreach$fwork (x: &a >> _, env: &(env) >> _): void
//
(* ****** ****** *)
//
fun{a:vt0p}
array_foreach_funenv
  {v:view}
  {vt:vtype}
  {n:int}
  {fe:eff}
(
  pfv: !v
| A: &(@[INV(a)][n]) >> @[a][n]
, asz: size_t n
, f: (!v | &a >> _, !vt) -<fun,fe> void
, env: !vt
) :<fe> void
// end of [array_foreach_funenv]
//
fun
array_foreach_funenv_tsz
  {a:vt0p}
  {v:view}
  {vt:vtype}
  {n:int}
  {fe:eff}
(
  pfv: !v
| A: &(@[INV(a)][n]) >> @[a][n]
, asz: size_t(n), tsz: sizeof_t(a)
, f: (!v | &a >> _, !vt) -<fun,fe> void
, env: !vt
) :<fe> void = "ext#%"
// end of [array_foreach_funenv_tsz]
//
(* ****** ****** *)
//
fun{a:vt0p}
array_foreach_fun
  {n:int}{fe:eff}
(
  &(@[INV(a)][n]) >> @[a][n]
, size_t (n), (&a >> _) -<fun,fe> void
) :<fe> void // end of [array_foreach_fun]
fun{a:vt0p}
array_foreach_clo
  {n:int}{fe:eff}
(
  A: &(@[INV(a)][n]) >> @[a][n]
, asz: size_t (n), f: &(&a >> _) -<clo,fe> void
) :<fe> void // end of [array_foreach_clo]
fun{a:vt0p}
array_foreach_cloptr
  {n:int}{fe:eff}
(
  A: &(@[INV(a)][n]) >> @[a][n]
, asz: size_t n, f: (&a >> _) -<cloptr,fe> void
) :<fe> void // end of [array_foreach_cloptr]
fun{a:vt0p}
array_foreach_cloref
  {n:int}{fe:eff}
(
  A: &(@[INV(a)][n]) >> @[a][n]
, asz: size_t(n), f: (&a >> _) -<cloref,fe> void
) :<fe> void // end of [array_foreach_cloref]
//
(* ****** ****** *)
//
fun{a:vt0p}
array_foreach_vclo
  {v:view}{n:int}{fe:eff}
(
  pfv: !v
| A: &(@[INV(a)][n]) >> @[a][n]
, asz: size_t n, f: &(!v | &a >> _) -<clo,fe> void
) :<fe> void // end of [array_foreach_vclo]
fun{a:vt0p}
array_foreach_vcloptr
  {v:view}{n:int}{fe:eff}
(
  pfv: !v
| A: &(@[INV(a)][n]) >> @[a][n]
, asz: size_t(n), f: !(!v | &a >> _) -<cloptr,fe> void
) :<fe> void // end of [array_foreach_vcloptr]
//
(* ****** ****** *)

fun{
a1,a2:vt0p
} array_foreach2
  {n:int}
(
  A1: &(@[INV(a1)][n]) >> @[a1][n]
, A2: &(@[INV(a2)][n]) >> @[a2][n]
, asz: size_t (n)
) : sizeLte (n) // end of [array_foreach2]
//
fun{
a1,a2:vt0p}{env:vt0p
} array_foreach2_env
  {n:int}
(
  A1: &(@[INV(a1)][n]) >> @[a1][n]
, A2: &(@[INV(a2)][n]) >> @[a2][n]
, asz:size_t (n)
, env: &(env) >> env
) : sizeLte (n) // end of [array_foreach2_env]
//
fun{
a1,a2:vt0p}{env:vt0p
} array_foreach2$cont
  (x1: &a1, x2: &a2, env: &env): bool
fun{
a1,a2:vt0p}{env:vt0p
} array_foreach2$fwork
  (x1: &a1 >> _, x2: &a2 >> _, env: &(env) >> _): void
//
(* ****** ****** *)

fun{
a:vt0p
} array_iforeach{n:int}
(
  A: &(@[INV(a)][n]) >> @[a][n], asz: size_t n
) : sizeLte (n) // end of [array_iforeach]
//
fun{
a:vt0p}{env:vt0p
} array_iforeach_env{n:int}
(
  A: &(@[INV(a)][n]) >> @[a][n], asz: size_t n, env: &(env) >> _
) : sizeLte (n) // end of [array_iforeach_env]
//
fun{
a:vt0p}{env:vt0p
} array_iforeach$cont (i: size_t, x: &a, env: &env): bool
fun{
a:vt0p}{env:vt0p
} array_iforeach$fwork (i: size_t, x: &a >> _, env: &(env) >> _): void
//
(* ****** ****** *)

fun{
a:vt0p
} array_rforeach{n:int}
(
  A: &(@[INV(a)][n]) >> @[a][n], asz: size_t n
) : sizeLte (n) // end of [array_rforeach]
//
fun{
a:vt0p}{env:vt0p
} array_rforeach_env{n:int}
(
  A: &(@[INV(a)][n]) >> @[a][n], asz: size_t n, env: &(env) >> _
) : sizeLte (n) // end of [array_rforeach_env]
//
fun{
a:vt0p}{env:vt0p
} array_rforeach$cont (x: &a, env: &env): bool
fun{
a:vt0p}{env:vt0p
} array_rforeach$fwork (x: &a >> _, env: &(env) >> _): void
//
(* ****** ****** *)
//
fun{a:vt0p}
array_initize{n:int}
(
  A: &(@[a?][n]) >> @[a][n], asz: size_t n
) : void // end of [array_initize]
//
fun{a:vt0p}
array_initize$init (i: size_t, x: &a? >> a): void
//
(* ****** ****** *)

fun{a:t0p}
array_initize_elt{n:int}
(
  A: &(@[a?][n]) >> @[a][n], asz: size_t n, elt: a
) :<!wrt> void // end of [array_initize_elt]

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

fun{a:t0p}
array_initize_list{n:int}
(
  A: &(@[a?][n]) >> @[a][n], asz: int n, xs: list (INV(a), n)
) :<!wrt> void // end of [array_initize_list]
fun{a:t0p}
array_initize_rlist{n:int}
(
  A: &(@[a?][n]) >> @[a][n], asz: int n, xs: list (INV(a), n)
) :<!wrt> void // end of [array_initize_rlist]

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

fun{a:vt0p}
array_initize_list_vt{n:int}
(
  A: &(@[a?][n]) >> @[a][n], asz: int n, xs: list_vt (INV(a), n)
) :<!wrt> void // end of [array_initize_list_vt]
fun{a:vt0p}
array_initize_rlist_vt{n:int}
(
  A: &(@[a?][n]) >> @[a][n], asz: int n, xs: list_vt (INV(a), n)
) :<!wrt> void // end of [array_initize_rlist_vt]

(* ****** ****** *)
//
fun{a:vt0p}
array_uninitize{n:int}
(
  A: &(@[INV(a)][n]) >> @[a?][n], asz: size_t n
) : void // end of [array_uninitize]
//
fun{a:vt0p}
array_uninitize$clear (i: size_t, x: &a >> a?): void
//
(* ****** ****** *)
//
fun{a:vt0p}
array_bsearch
  {n:int} (A: &RD(@[a][n]), n: size_t (n)):<> sizeLte (n)
//
fun{a:vt0p}
array_bsearch$ford (x: &RD(a)):<> int
//
fun{a:vt0p}
array_bsearch_fun{n:int}
(
  A: &RD(@[a][n]), asz: size_t (n), key: &RD(a), cmp: cmpref (a)
) :<> sizeLte (n) // end of [array_bsearch_fun]
//
(* ****** ****** *)

(*
** HX: this one is based on [bsearch] in [stdlib]
*)
fun{a:vt0p}
array_bsearch_stdlib{n:int}
(
  A: &RD(@[a][n]), asz: size_t (n), key: &RD(a), cmp: cmpref (a)
) :<> Ptr0 (* found/~found : ~null/null *)

(* ****** ****** *)
//
fun{a:vt0p}
array_quicksort{n:int}
  (A: &(@[INV(a)][n]) >> @[a][n], n: size_t n):<!wrt> void
fun{a:vt0p}
array_quicksort$cmp (x1: &RD(a), x2: &RD(a)):<> int(*sgn*)
//
(* ****** ****** *)

(*
** HX: this one is based on [qsort] in [stdlib]
*)
fun{a:vt0p}
array_quicksort_stdlib{n:int}
(
  A: &(@[INV(a)][n]) >> @[a][n], n: size_t n, cmp: cmpref (a)
) :<!wrt> void // end of [array_quicksort_stdlib]

(* ****** ****** *)
//
fun{
a:vt0p}{b:vt0p
} array_mapto{n:int}
(
  A: &array(INV(a), n)
, B: &array(b?, n) >> array (b, n)
, n: size_t (n)
) : void // end of [array_mapto]
//
fun{
a:vt0p}{b:vt0p
} array_mapto$fwork (x: &a, y: &b? >> b) : void
//
(* ****** ****** *)
//
fun{
a,b:vt0p}{c:vt0p
} array_map2to{n:int}
(
  A: &array(INV(a), n)
, B: &array(INV(b), n)
, C: &array(c?, n) >> array (c, n)
, n: size_t (n)
) : void // end of [array_map2to]
//
fun{
a,b:vt0p}{c:vt0p
} array_map2to$fwork (x: &a, y: &b, z: &c? >> c) : void
//
(* ****** ****** *)
//
fun{a:vt0p}
array_permute{n:int}
  (A: &(@[INV(a)][n]) >> @[a][n], n: size_t n): void
//
fun{}
array_permute$randint {n:int | n > 0} (size_t n): sizeLt (n)
//
(* ****** ****** *)

(* end of [array.sats] *)