Test/dafny0/RankPos.dfy


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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79

datatype list<A> = Nil | Cons(head: A, tail: list<A>);
datatype d = A | B(ds: list<d>);
datatype d2 = A2 | B2(ds: seq<d2>);
datatype d3 = A3 | B3(ds: set<d3>);

function d_size(x: d): int
{
  match x
  case A => 1
  case B(ds) => 1+ds_size(ds)
}

function ds_size(xs: list<d>): int
{
  match xs
  case Nil => 1
  case Cons(head, tail) => d_size(head)+ds_size(tail)
}

function d2_size(x: d2): int
{
  match x
  case A2 => 1
  case B2(ds) => 1+ds2_size(ds)
}

function ds2_size(xs: seq<d2>): int
{
  if (|xs|==0) then 1 else 1+d2_size(xs[0])+ds2_size(xs[1..])
}

function seq_dec_drop(xs: seq<int>): int
{
  if (|xs|==0) then 0 else
  1+seq_dec_drop(xs[1..])
}

function seq_dec_take(xs: seq<int>): int
{
  if (|xs|==0) then 0 else
  1+seq_dec_take(xs[..|xs|-1])
}

function seq_dec(xs: seq<int>): int
{
  if (|xs|==0) then 0 else
  var i :| 0 < i <= |xs|;
  i+seq_dec(xs[i..])
}

function seq_dec'(xs: seq<int>): int
{
  if (|xs|==0) then 0 else
  var i :| 0 <= i < |xs|;
  i+seq_dec'(xs[..i])
}

function seq_dec''(xs: seq<int>): int
{
  if (|xs|==0) then 0 else
  var i :| 0 <= i < |xs|;
  assert xs[0..i] == xs[..i];
  i+seq_dec''(xs[0..i])
}

function seq_dec'''(xs: seq<int>): int
  decreases |xs|;
{
  if (|xs|==0) then 0 else
  var i :| 0 <= i < |xs|;
  i+seq_dec'''(xs[..i]+xs[i+1..])
}

function seq_dec''''(xs: seq<int>): int
{
  if (|xs|==0) then 0 else
  var i :| 0 <= i < |xs|;
  i+seq_dec''''(xs[..i]+xs[i+1..])
}