View equality in template function

[Artyom Shalkhakov]

Hello all,

Here's an issue:

https://gist.github.com/ashalkhakov/85b3046c0432f93d08df

Is there a solution not involving unsafe casts? This sort of loop-construction seems like a very common thing to do. Threading views is also common, but templates do not allow that. If env is given a viewtype (@[int][N] @ A | void), it still doesn't work (no template is found for fwork).

[gmhwxi]

Unfortunately, this cannot be done.

The only way I can see to make it safe is this:

absvtype myenv = void
// implement the following two proof functions
prfun myenv_decode (&myenv >> void): @[int][N]@A
prfun myenv_encode (&void >> myenv, @[int][N]@A): void

implement
loop$fwork<myenv> (env) = ... // using decode and encode

...loop<myenv>()...

[Artyom Shalkhakov]

On Thursday, March 26, 2015 at 11:51:16 PM UTC+6, gmhwxi wrote:

Unfortunately, this cannot be done.

The only way I can see to make it safe is this:

absvtype myenv = void
// implement the following two proof functions
prfun myenv_decode (&myenv >> void): @[int][N]@A
prfun myenv_encode (&void >> myenv, @[int][N]@A): void

implement
loop$fwork<myenv> (env) = ... // using decode and encode

...loop<myenv>()...

Okay, if you say so. I'll be using some unsafe casts then.