View equalities in templates

template-view-eq.dats

#include
"share/atspre_staload.hats"

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

#define N 5

extern
fun{env:vt@ype}
loop$fwork (natLt(N), &(env) >> _): void

extern
fun{env:vt@ype}
loop (&(env) >> _): void

implement{env}
loop (env) = {
  var ix : int = 0
  val () =
  // please disregard the [while] loop,
  // just an exercise
  while* {i:nat | i <= N} .<N-i>. (ix: int i) =>
    (ix < N) {
    val () = loop$fwork<env> (ix, env)
    val () = ix := ix + 1
  } // end of [val]
} (* end of [loop] *)

implement
main0 () = {
//
var A = @[int][N](0,1,2,3,4,5,6,7,8,9)
var B = @[int][N](9,8,7,6,5,6,7,8,9,0)
var C = @[int][N](0)
//
absvt@ype VT = void
assume VT = (@[int][N] @ A, @[int][N] @ B, @[int][N] @ C | void)
//
implement
loop$fwork<VT> (i, env) = {
  val x = A.[i] + B.[i]
  val () = C.[i] := x
  val () = println!(x)
}
//
var env = (view@A, view@B, view@C | ())
val () = loop<VT> (env)
//
prval () = view@A := env.0
and () = view@B := env.1
and () = view@C := env.2
//
} (* end of [main0] *)

Edited as per Hongwei Xi's suggestion.

NOTE: as it turns out, every VT can be [assume]d at most once, so the code as presented won't compile if there are more than one function in a module using this trick. So, the way forward is through [prfun]s for casting between [VT] and a specific view (in this case, the view would be [@[int][N] @ A, @[int][N] @ B, @[int]N] @ C]).