(***********************************************************************) (* *) (* 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: Mon Jun 4 01:42:39 2018 *) (* ****** ****** *) (* 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 = vtype sortdef vt0p = vt@ype (* ****** ****** *) (* // // HX: [array_v] can also be defined as follows: // dataview array_v ( a:vt@ype+, addr, int ) = // HX: for arry view | {l:addr} array_v_nil (a, l, 0) | {l:addr}{n:int} array_v_cons (a, l, n+1) of (a @ l, array_v (a, l+sizeof a, n)) // end of [array_v] *) (* ****** ****** *) dataview arrayopt_v(a: vt@ype+, addr, int, bool) = | {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} () - array_v(a, l, 0) // praxi array_v_unnil : {a:vt0p} {l:addr} array_v(a, l, 0) - void // prfun array_v_unnil_nil : { a1, a2 : vt0p } {l:addr} array_v(a1, l, 0) - 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)) - array_v(a, l, n+1) // praxi array_v_uncons : {a:vt0p} {l:addr} { n : int | n > 0 } array_v(INV(a), l, n) - (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 // 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_gint of 0 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 ) : void // fun {a:t0p}{tk:tk} array_set_at_guint {n:int} ( A : &(@[INV(a)][n]) , i : g1uintLt(tk, n) , x : a ) : void // overload [] with array_set_at_gint of 0 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 >> _ ) : void fun {a:vt0p}{tk:tk} array_exch_at_guint {n:int} ( A : &(@[INV(a)][n]) , i : g1uintLt(tk, n) , x : &a >> _ ) : 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_subreverse {n:int}{ i, j : int | 0 <= i; i <= j; j <= n } ( A : &(@[INV(a)][n]) , i : size_t(i) , j : size_t(j) ) : void // end of [array_subreverse] (* ****** ****** *) fun {a:vt0p} array_interchange {n:int} ( A : &(@[INV(a)][n]) , i : sizeLt(n) , j : sizeLt(n) ) : void // end of [array_interchange] (* ****** ****** *) fun {a:vt0p} array_subcirculate {n:int} ( A : &(@[INV(a)][n]) , i : sizeLt(n) , j : sizeLt(n) ) : 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) - 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)) : [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)) : void // end-of-function (* ****** ****** *) // 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) ) : void // end of [array_copy] (* ****** ****** *) // fun {a:t0p} array_copy_from_list {n:int} ( A : &(@[a?][n]) >> @[a][n] , xs : list(INV(a), n) ) : 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)) : 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)) : 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} (pf : !v | A0 : &(@[INV(a)][n]) >> @[a][n], asz : size_t(n), f0 : (!v | &a >> _, !vt) - void, env : !vt) : void // end of [array_foreach_funenv] // fun array_foreach_funenv_tsz {a:vt0p}{v:view}{vt:vtype}{n:int}{fe:eff}( pf : !v | A0 : &(@[INV(a)][n]) >> @[a][n] , asz : size_t(n) , tsz : sizeof_t(a) , f0 : (!v | &a >> _, !vt) - void , env : !vt ) : void = "ext#%" // end of [array_foreach_funenv_tsz] // (* ****** ****** *) 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} ( A0 : &(@[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} (A0 : &(@[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} (A0 : &(@[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) ) : 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) ) : 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) ) : 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) ) : 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) ) : void // end of [array_initize_rlist_vt] (* ****** ****** *) // fun {a:vt0p} array_uninitize {n:int} ( A0 : &(@[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$ford (x : &RD(a)) :<> int // fun {a:vt0p} array_bsearch {n:int} (A : &RD(@[a][n]), n : size_t(n)) :<> sizeLte(n) // fun {a:vt0p} array_bsearch_fun {n:int} ( A0 : &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} ( A0 : &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) ) : void // end-of-function 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)) : 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 // (* ****** ****** *) // (* HX-2016: Fisher–Yates shuffle *) // 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] *)