blob: ecc0613790441400b71d47f5ba9d4c427659314f (
plain)
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
|
default Order dec
(* A function which is merely parametrised by a size does not need to be
monomorphised *)
val forall 'n, 'n in {32,64}. [:'n:] -> bit[64] effect pure parametric
function parametric(n) = {
let (bit['n]) x = exts(0x80000000) in
extz(x)
}
(* But if we do a calculation on the size then we'll need to case split *)
val forall 'n, 'n in {16,32}. [:'n:] -> bit[64] effect pure depends
function depends(n) = {
let 'm = 2 * n in
let (bit['m]) x = exts(0x80000000) in
extz(x)
}
val unit -> bool effect pure run
function run () =
parametric(32) == 0x0000000080000000 &
parametric(64) == 0xffffffff80000000 &
depends(16) == 0x0000000080000000 &
depends(32) == 0xffffffff80000000
|
