summaryrefslogtreecommitdiff
path: root/src/test/test1.sail
blob: 64722089446faa0f01a9f268cf667446d9f830e5 (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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
default Nat 'i
default Order 'o
default bool b
default forall 'a. list<'a> b
val forall 'a, 'b . ('a, 'b) -> 'b effect pure snd
val forall Type 'i, 'b. ('i, 'b) -> 'i effect pure fst
typedef int_list [name = "il"] = list<nat>
typedef reco = const struct forall 'i, 'a, 'b. { 'a['i] v; 'b w; }
typedef maybe = const union forall 'a. { Nne; 'a Sme; }
typedef colors = enumerate { red; green; blue }
typedef creg = register bits [5:10] { 5 : h ; 6..7 : j}
let bool e = true
val forall Nat 'a, Nat 'b. bit['a:'b] sliced
let bit v = bitzero
let ( bit [ 32 ] ) v1 = 0b101

val forall Type 'a. 'a -> 'a effect pure identity
function forall Type 'a. 'a identity i = i

function unit ignore(x) = ()

(* scattered function definition and union definition *)
scattered typedef ast = const union
scattered function ast f

union ast member  (bit, bit, bit) A
function clause f (  A (a,b,c) ) = C(a)

union ast member  (bit, bit) B
function clause f (  B (a,b) ) = C(a)

union ast member  bit C
function clause f (  C (a) ) = C(a)

end ast
end f

function unit a (bit) b = if identity(b) then (identity()) else ()

function bit sw s = switch s { case 0 -> bitzero }

function bit main _ = {ignore(sw(0)); v1[0] }