summaryrefslogtreecommitdiff
path: root/Test/datatypes/t2.bpl
blob: d4d2bf3f2ca791f0bc89a43cf1eb2a14b1dee35d (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
type TT;
type {:datatype} Tree;
function {:constructor} leaf`0() : Tree;
function {:constructor} node`2(value:TT, children:TreeList) : Tree;

type {:datatype} TreeList;
function {:constructor} cons`2(car:Tree, cdr:TreeList) : TreeList;
function {:constructor} nil`0() : TreeList;

procedure foo() 
{
  var a: Tree;
  var b: TreeList;
  var x: TT;

  assert value#node`2(node`2(x, nil`0())) == x;
  assert children#node`2(node`2(x, nil`0())) == nil`0();
  
  assert (cons`2(leaf`0(), nil`0()) != nil`0());

  assert is#nil`0(nil`0());

  assert is#node`2(leaf`0());
}