cursor.mlw 2.04 KB
Newer Older
Mário Pereira's avatar
Mário Pereira committed
1 2
module Cursor

3
  use seq.Seq
Mário Pereira's avatar
Mário Pereira committed
4 5

  type cursor 'a = private {
6
    ghost mutable visited : seq 'a;
Mário Pereira's avatar
Mário Pereira committed
7 8
  }

9 10 11 12
  predicate permitted (cursor 'a)
  axiom permitted_empty: forall c: cursor 'a. c.visited = empty -> permitted c

  predicate complete  (cursor 'a)
Mário Pereira's avatar
Mário Pereira committed
13 14

  val next (c: cursor 'a) : 'a
15 16
    requires { not (complete c) }
    requires { permitted c }
Mário Pereira's avatar
Mário Pereira committed
17 18
    writes   { c.visited }
    ensures  { c.visited = snoc (old c).visited result }
19
    ensures  { permitted c }
Mário Pereira's avatar
Mário Pereira committed
20 21

  val has_next (c: cursor 'a) : bool
22 23
    requires { permitted c }
    ensures  { result <-> not (complete c) }
Mário Pereira's avatar
Mário Pereira committed
24 25

end
26

Mário Pereira's avatar
Mário Pereira committed
27
module ListCursor
28

29 30 31 32
  use seq.Seq
  use seq.OfList
  use list.List
  use int.Int
33 34

  type cursor 'a = private {
Mário Pereira's avatar
Mário Pereira committed
35 36
    ghost mutable visited    : seq 'a;
    ghost         collection : list 'a;
37 38 39
  }

  predicate permitted (c: cursor 'a) =
Mário Pereira's avatar
Mário Pereira committed
40 41
    length c.visited <= length c.collection /\
    forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i]
42 43

  predicate complete  (c: cursor 'a) =
Mário Pereira's avatar
Mário Pereira committed
44
    length c.visited = length c.collection
45 46 47 48

  val create (l: list 'a) : cursor 'a
    ensures { permitted result }
    ensures { result.visited = empty }
Mário Pereira's avatar
Mário Pereira committed
49
    ensures { result.collection = l }
50

51
  clone Cursor as C with
52 53 54 55 56 57 58
    type cursor = cursor,
    predicate permitted = permitted,
    predicate complete  = complete,
    goal permitted_empty

end

59
module ArrayCursor
60

61 62 63 64 65
  use array.Array
  use array.ToSeq
  use seq.Seq
  use seq.OfList
  use int.Int
66 67

  type cursor 'a = private {
68 69
    ghost mutable visited    : seq 'a;
    ghost         collection : seq 'a;
70 71 72
  }

  predicate permitted (c: cursor 'a) =
73 74
    length c.visited <= length c.collection /\
    forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i]
75 76

  predicate complete  (c: cursor 'a) =
77
    length c.visited = length c.collection
78 79 80 81

  val create (a: array 'a) : cursor 'a
    ensures { permitted result }
    ensures { result.visited = empty }
82
    ensures { result.collection = to_seq a }
83

84
  clone Cursor as C with
85 86 87 88 89
    type cursor = cursor,
    predicate permitted = permitted,
    predicate complete  = complete,
    goal permitted_empty

90
end