stdlib/cursor.mlw

   1 (** {1 Cursors} *)
   2
   3 module Cursor
   4
   5   use seq.Seq
   6
   7   type cursor 'a = private {
   8     ghost mutable visited : seq 'a;
   9   }
  10
  11   predicate permitted (cursor 'a)
  12   axiom permitted_empty: forall c: cursor 'a. c.visited = empty -> permitted c
  13
  14   predicate complete  (cursor 'a)
  15
  16   val next (c: cursor 'a) : 'a
  17     requires { not (complete c) }
  18     requires { permitted c }
  19     writes   { c.visited }
  20     ensures  { c.visited = snoc (old c).visited result }
  21     ensures  { permitted c }
  22
  23   val has_next (c: cursor 'a) : bool
  24     requires { permitted c }
  25     ensures  { result <-> not (complete c) }
  26
  27 end
  28
  29 module ListCursor
  30
  31   use seq.Seq
  32   use seq.OfList
  33   use list.List
  34   use int.Int
  35
  36   type cursor 'a = private {
  37     ghost mutable visited    : seq 'a;
  38     ghost         collection : list 'a;
  39   }
  40
  41   predicate permitted (c: cursor 'a) =
  42     length c.visited <= length c.collection /\
  43     forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i]
  44
  45   predicate complete  (c: cursor 'a) =
  46     length c.visited = length c.collection
  47
  48   val create (l: list 'a) : cursor 'a
  49     ensures { permitted result }
  50     ensures { result.visited = empty }
  51     ensures { result.collection = l }
  52
  53   clone Cursor as C with
  54     type cursor = cursor,
  55     predicate permitted = permitted,
  56     predicate complete  = complete,
  57     goal permitted_empty
  58
  59 end
  60
  61 module ArrayCursor
  62
  63   use array.Array
  64   use array.ToSeq
  65   use seq.Seq
  66   use seq.OfList
  67   use int.Int
  68
  69   type cursor 'a = private {
  70     ghost mutable visited    : seq 'a;
  71     ghost         collection : seq 'a;
  72   }
  73
  74   predicate permitted (c: cursor 'a) =
  75     length c.visited <= length c.collection /\
  76     forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i]
  77
  78   predicate complete  (c: cursor 'a) =
  79     length c.visited = length c.collection
  80
  81   val create (a: array 'a) : cursor 'a
  82     ensures { permitted result }
  83     ensures { result.visited = empty }
  84     ensures { result.collection = to_seq a }
  85
  86   clone Cursor as C with
  87     type cursor = cursor,
  88     predicate permitted = permitted,
  89     predicate complete  = complete,
  90     goal permitted_empty
  91
  92 end