staload
"share/atspre_staload.hats"
staload
_ = "prelude/DATS/integer.dats"
staload
_ = "prelude/DATS/pointer.dats"
staload
_ = "prelude/DATS/array.dats"
staload
_ = "prelude/DATS/matrix.dats"
staload
_ = "prelude/DATS/pointer.dats"
staload
_ = "prelude/DATS/reference.dats"
staload
_ = "prelude/DATS/unsafe.dats" // used by matrix functions
extern
fun
multable_init (
mat: &(@[@[int][10]][10])? >> _
): void // end of [multable_init]
//
(* ****** ****** *)
//
implement
multable_init (m) = {
//
#define NCOL 10
#define NROW 10
typedef T = int
typedef COL_T = @[T][NCOL]
//
fun aux_col {lres:addr} (
pf_res: !COL_T? @ lres >> COL_T @ lres
| pres: ptr lres, i: natLt(NCOL)
): void = {
//
var j: int = 0
var p = pres
prvar pf0 = array_v_nil {T} ()
prvar pf1 = pf_res
//
val () =
while* {j:nat | j <= NROW} .<NROW-j>. (
j: int (j)
, p: ptr (lres + j*sizeof(T))
, pf0: array_v (T, lres, j)
, pf1: array_v (T?, lres+j*sizeof(T), NROW-j)
) : (
pf0: array_v (T, lres, NROW)
, pf1: array_v (T?, lres+j*sizeof(T), 0)
) => (
j < NROW
) {
//
prval (pf_at, pf1_res) = array_v_uncons {T?} (pf1)
prval () = pf1 := pf1_res
//
val () = ptr_set<T> (pf_at | p, (g0ofg1)(i * j))
val () = p := ptr1_succ<T> (p)
//
prval () = pf0 := array_v_extend {T} (pf0, pf_at)
val () = j := j + 1
//
} // end of [val]
//
prval () = pf_res := pf0
prval () = array_v_unnil {T?} (pf1)
//
} (* end of [loop] *)
//
fun
aux {lres:addr} (
pf_res : !(@[COL_T?][NCOL] @ lres) >> @[COL_T][NCOL] @ lres
| pres: ptr lres
): void = {
//
var i: int = 0
var p = pres
prvar pf0 = array_v_nil {COL_T} ()
prvar pf1 = pf_res
//
val () =
while* {i:nat | i <= NCOL} .<NCOL-i>. (
i: int (i)
, p: ptr (lres + i*(NCOL*sizeof(T)))
, pf0: array_v (COL_T, lres, i)
, pf1: array_v (COL_T?, lres+i*sizeof(COL_T), NCOL-i)
) : (
pf0: array_v (COL_T, lres, NCOL)
, pf1: array_v (COL_T?, lres+i*sizeof(COL_T), 0)
) => (
i < NCOL
) {
//
prval (pf_at, pf1_res) = array_v_uncons {COL_T?} (pf1)
prval () = pf1 := pf1_res
//
prval () = __trustme () where {
extern prfun __trustme (): [i * (NROW * sizeof(T)) == i * sizeof(@[T][NROW])] void
}
//
val () = aux_col (pf_at | p, i)
//
//
val () = p := ptr_add<T> (p, NCOL)
//
prval () = pf0 := array_v_extend {COL_T} (pf0, pf_at)
val () = i := i + 1
//
} // end of [val]
//
prval () = pf_res := pf0
prval () = array_v_unnil {COL_T?} (pf1)
//
} (* end of [aux] *)
//
val () = aux (view@m | addr@m)
//
} (* end of [multable_init] *)
var multable : @[int?][100]
val p_multable = addr@multable
prval pf_multable = array_v_group (view@multable)
val () = multable_init (!p_multable)
prval pf_multable = array_v_ungroup (pf_multable)
prval pf_multable = array2matrix_v (pf_multable)
val theMultable = ref_make_viewptr {matrix (int, 10, 10)} (pf_multable | p_multable)
implement main0 () = let
val (pf_multab, fpf | p_multab) = $effmask_ref (ref_vtakeout (theMultable))
val res = matrix_get_at_int (!p_multab, 3, 10, 4)
val () = println!("the result of 3 * 4 = ", res)
val res = matrix_get_at_int (!p_multab, 4, 10, 7)
val () = println!("the result of 4 * 7 = ", res)
prval () = fpf (pf_multab)
in
end
