Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
View equalities in templates
#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] *)
@ashalkhakov

This comment has been minimized.

Copy link
Owner Author

@ashalkhakov ashalkhakov commented Mar 27, 2015

Edited as per Hongwei Xi's suggestion.

@ashalkhakov

This comment has been minimized.

Copy link
Owner Author

@ashalkhakov ashalkhakov commented Mar 30, 2015

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]).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment