random_access_list.mlw 7.32 KB
Newer Older
1 2

(** Random Access Lists.
3
    (Okasaki, "Purely Functional Data Structures", 10.1.2.)
4 5 6 7

    The code below uses polymorphic recursion (both in the logic
    and in the programs).

8
    Author: Jean-Christophe Filliâtre (CNRS)
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
 *)

module RandomAccessList

  use import int.Int
  use import int.ComputerDivision
  use import list.List
  use import list.Length
  use import list.Nth
  use import option.Option

  type ral 'a =
  | Empty
  | Zero    (ral ('a, 'a))
  | One  'a (ral ('a, 'a))

25 26
  function flatten (l: list ('a, 'a)) : list 'a =
    match l with
27 28 29 30
    | Nil -> Nil
    | Cons (x, y) l1 -> Cons x (Cons y (flatten l1))
    end

31
  let rec lemma length_flatten (l:list ('a, 'a))
32 33
    ensures { length (flatten l) = 2 * length l }
    variant { l }
34 35
    =
    match l with
36 37 38 39
    | Cons (_,_) q -> length_flatten q
    | Nil -> ()
    end

40 41 42 43 44 45
  function elements (l: ral 'a) : list 'a =
    match l with
    | Empty    -> Nil
    | Zero l1  -> flatten (elements l1)
    | One x l1 -> Cons x (flatten (elements l1))
    end
46 47 48 49

  let rec size (l: ral 'a) : int
    variant { l }
    ensures { result = length (elements l) }
50
    =
51 52 53 54 55 56
    match l with
    | Empty    -> 0
    | Zero  l1 ->     2 * size l1
    | One _ l1 -> 1 + 2 * size l1
    end

57
  let rec cons (x: 'a) (l: ral 'a) : ral 'a
58 59
    variant { l }
    ensures { elements result = Cons x (elements l) }
60 61 62 63 64 65
    =
    match l with
    | Empty    -> One x Empty
    | Zero l1  -> One x l1
    | One y l1 -> Zero (cons (x, y) l1)
    end
66 67 68 69 70 71 72 73

  let rec lemma nth_flatten (i: int) (l: list ('a, 'a))
    requires { 0 <= i < length l }
    variant  { l }
    ensures  { match nth i l with
               | None -> false
               | Some (x0, x1) -> Some x0 = nth (2 * i)     (flatten l) /\
                                  Some x1 = nth (2 * i + 1) (flatten l) end }
74 75
    =
    match l with
76 77 78 79
    | Nil -> ()
    | Cons _ r -> if i > 0 then nth_flatten (i-1) r
    end

80
  let rec lookup (i: int) (l: ral 'a) : 'a
81 82 83
    requires { 0 <= i < length (elements l) }
    variant  { i, l }
    ensures  { nth i (elements l) = Some result }
84 85 86 87 88 89 90
    =
    match l with
    | Empty    -> absurd
    | One x l1 -> if i = 0 then x else lookup (i-1) (Zero l1)
    | Zero l1  -> let (x0, x1) = lookup (div i 2) l1 in
                  if mod i 2 = 0 then x0 else x1
    end
91

92
  let rec tail (l: ral 'a) : ral 'a
93
    requires { elements l <> Nil }
94 95 96 97 98
    variant  { l }
    ensures  { match elements l with
               | Nil -> false
               | Cons _ l -> elements result = l
               end }
99 100 101 102 103 104
    =
    match l with
    | Empty    -> absurd
    | One _ l1 -> Zero l1
    | Zero  l1 -> let (_, x1) = lookup 0 l1 in One x1 (tail l1)
    end
105

106
  let rec update (i: int) (y: 'a) (l: ral 'a) : ral 'a
107 108 109 110 111 112 113 114 115 116
    requires { 0 <= i < length (elements l) }
    variant  { i, l}
    ensures  { nth i (elements result) = Some y}
    ensures  { forall j. 0 <= j < length (elements l) ->
               j <> i -> nth j (elements result) = nth j (elements l) }
    ensures  { length (elements result) = length (elements l) }
    ensures  { match result, l with
               | One _ _, One _ _ | Zero _, Zero _ -> true
               | _                                 -> false
               end }
117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
    =
    match l with
    | Empty    -> absurd
    | One x l1 -> if i = 0 then One y l1 else
                  match update (i-1) y (Zero l1) with
                  | Empty | One _ _ -> absurd
                  | Zero l1         -> One x l1
                  end
    | Zero l1  ->
        let (x0, x1) = lookup (div i 2) l1 in
        let l1' =
          update (div i 2) (if mod i 2 = 0 then (y,x1) else (x0,y)) l1 in
        assert { forall j. 0 <= j < length (elements l) -> j <> i ->
                 match nth (div j 2) (elements l1) with
                 | None -> false
                 | Some (x0,_) -> Some x0 = nth (2 * (div j 2)) (elements l)
                 end
                 && nth j (elements l) = nth j (elements (Zero l1')) };
        Zero l1'
    end
137

138
end
139 140 141 142 143 144 145 146 147 148 149 150 151 152

(** A straightforward encapsulation with a list ghost model
    (in anticipation of module refinement) *)

module RAL

  use import int.Int
  use import RandomAccessList as R
  use import list.List
  use import list.Length
  use import option.Option
  use import list.Nth

  type t 'a = { r: ral 'a; ghost l: list 'a }
153
    invariant { l = elements r }
154 155 156

  let empty () : t 'a
    ensures { result.l = Nil }
157
    =
158 159 160 161
    { r = Empty; l = Nil }

  let size (t: t 'a) : int
    ensures { result = length t.l }
162
    =
163 164 165 166
    size t.r

  let cons (x: 'a) (s: t 'a) : t 'a
    ensures { result.l = Cons x s.l }
167
    =
168
    { r = cons x s.r; l = Cons x s.l }
169

170
  let lookup (i: int) (s: t 'a) : 'a
171 172
    requires { 0 <= i < length s.l }
    ensures { Some result = nth i s.l }
173
    =
174
    lookup i s.r
175 176 177

end

178 179
(** Model using sequences instead of lists *)

180 181 182 183 184 185 186 187 188 189 190
module RandomAccessListWithSeq

  use import int.Int
  use import int.ComputerDivision
  use import seq.Seq

  type ral 'a =
  | Empty
  | Zero    (ral ('a, 'a))
  | One  'a (ral ('a, 'a))

191 192
  function flatten (s: seq ('a, 'a)) : seq 'a =
    create (2 * length s)
193 194
           (fun i -> let (x0, x1) = s[div i 2] in
                     if mod i 2 = 0 then x0 else x1)
195

196 197 198 199 200 201
  function elements (l: ral 'a) : seq 'a =
    match l with
    | Empty    -> empty
    | Zero l1  -> flatten (elements l1)
    | One x l1 -> cons x (flatten (elements l1))
    end
202 203 204 205

  let rec size (l: ral 'a) : int
    variant { l }
    ensures { result = length (elements l) }
206
    =
207 208 209 210 211 212
    match l with
    | Empty    -> 0
    | Zero  l1 ->     2 * size l1
    | One _ l1 -> 1 + 2 * size l1
    end

213
  let rec cons (x: 'a) (l: ral 'a) : ral 'a
214 215
    variant { l }
    ensures { elements result == cons x (elements l) }
216 217 218 219 220 221
    =
    match l with
    | Empty    -> One x Empty
    | Zero l1  -> One x l1
    | One y l1 -> Zero (cons (x, y) l1)
    end
222

223
  let rec lookup (i: int) (l: ral 'a) : 'a
224 225 226
    requires { 0 <= i < length (elements l) }
    variant  { i, l }
    ensures  { (elements l)[i] = result }
227 228 229 230 231 232 233
    =
    match l with
    | Empty    -> absurd
    | One x l1 -> if i = 0 then x else lookup (i-1) (Zero l1)
    | Zero l1  -> let (x0, x1) = lookup (div i 2) l1 in
                  if mod i 2 = 0 then x0 else x1
    end
234

235
  let rec tail (l: ral 'a) : ral 'a
236 237 238
    requires { 0 < length (elements l) }
    variant  { l }
    ensures  { elements result == (elements l)[1 .. ] }
239 240 241 242 243 244
    =
    match l with
    | Empty    -> absurd
    | One _ l1 -> Zero l1
    | Zero  l1 -> let (_, x1) = lookup 0 l1 in One x1 (tail l1)
    end
245

246 247 248
  (** update in O(log n)
      for this, we need to pass a function that will update the element
      when we find it *)
249

250 251
  function setf (s: seq 'a) (i: int) (f: 'a -> 'a) : seq 'a =
    set s i (f s[i])
252

253
  function aux (i: int) (f: 'a -> 'a) : ('a, 'a) -> ('a, 'a) =
254
    fun z -> let (x,y) = z in if mod i 2 = 0 then (f x, y) else (x, f y)
255

256
  let rec fupdate (f: 'a -> 'a) (i: int) (l: ral 'a) : ral 'a
257 258
    requires { 0 <= i < length (elements l) }
    variant  { i, l}
259
    ensures  { elements result == setf (elements l) i f}
260 261 262 263 264 265 266 267
    =
    match l with
    | Empty    -> absurd
    | One x l1 -> if i = 0 then One (f x) l1 else
                  cons x (fupdate f (i-1) (Zero l1))
    | Zero l1  -> Zero (fupdate (aux i f) (div i 2) l1)
    end

268
  let function f (y: 'a) : 'a -> 'a = fun _ -> y
269 270 271 272 273 274

  let update (i: int) (y: 'a) (l: ral 'a) : ral 'a
    requires { 0 <= i < length (elements l) }
    ensures  { elements result == set (elements l) i y}
    =
    fupdate (f y) i  l
275

276
end