File: tuple_cast_insertion.sail

package info (click to toggle)
sail-ocaml 0.19.1%2Bdfsg5-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 18,008 kB
  • sloc: ml: 75,941; ansic: 8,848; python: 1,342; exp: 560; sh: 474; makefile: 218; cpp: 36
file content (18 lines) | stat: -rw-r--r-- 517 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
default Order dec
$include <prelude.sail>

val f0 : forall 'n, 'n >= 0. int('n) -> (vector('n, dec, bool), vector('n, dec, bool))

/* Sail usually inserts a cast when translating the tuple assignment, but the
   type variable for `unsigned(v0)` was leaking into these casts.  It should
   manage to use 'n instead. */

val f : bits(4) -> unit

function f(v0) = {
  let num = unsigned(v0) * 8;
  let 'n = num;
  v1 : vector('n, dec, bool) = undefined;
  v2 : vector('n, dec, bool) = undefined;
  (v1, v2) = f0(num);
}