File: existential_cast.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 (34 lines) | stat: -rw-r--r-- 690 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
default Order dec
$include <prelude.sail>

/* In the let x = ... the x will get an existential type, and we need
   to take care not to accidentally cast it because the type variable
   doesn't match the original.

   Also incidentally tests that we can generate an initial value for a
   type with a range inside.
 */

struct Params = {
  size : {2,4},
}

union Foo ('a : Type) = {
  Ok : 'a,
  Nope : unit,
}

register r : bits(1)

val f : forall 'n, 'n > 0. int('n) -> Foo(bits(8 * 'n))
function f(sz) = Ok(sail_zero_extend(r, 8 * sz))

val g : Params -> bits(64)

function g(p) = {
  let x = f(p.size);
  match x {
  Ok(v) => sail_zero_extend(v, 64),
  Nope(_) => sail_zeros(64),
  }
}