random_access_list.mlw 7.98 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 202 203
  lemma cons_flatten : forall x y :'a,s:seq ('a,'a).
    let a = flatten (cons (x,y) s) in
    let b = cons x (cons y (flatten s)) in
    a = b by a == b by forall i. 0 <= i < a.length -> a[i] = b[i]
    by (i <= 1 so (cons (x,y) s)[div i 2] = (x,y))
       \/ (i >= 2 so (cons (x,y) s)[div i 2] = s[div (i-2) 2]
       )

204 205 206 207 208 209
  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
210 211 212 213

  let rec size (l: ral 'a) : int
    variant { l }
    ensures { result = length (elements l) }
214
    =
215 216 217 218 219 220
    match l with
    | Empty    -> 0
    | Zero  l1 ->     2 * size l1
    | One _ l1 -> 1 + 2 * size l1
    end

221
  let rec cons (x: 'a) (l: ral 'a) : ral 'a
222 223
    variant { l }
    ensures { elements result == cons x (elements l) }
224 225 226 227 228 229
    =
    match l with
    | Empty    -> One x Empty
    | Zero l1  -> One x l1
    | One y l1 -> Zero (cons (x, y) l1)
    end
230

231
  let rec lookup (i: int) (l: ral 'a) : 'a
232 233 234
    requires { 0 <= i < length (elements l) }
    variant  { i, l }
    ensures  { (elements l)[i] = result }
235 236 237 238 239 240 241
    =
    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
242

243
  let rec tail (l: ral 'a) : ral 'a
244 245
    requires { 0 < length (elements l) }
    variant  { l }
246
    ensures  { elements result == (elements l)[1..] }
247 248 249 250
    =
    match l with
    | Empty    -> absurd
    | One _ l1 -> Zero l1
251 252 253 254
    | Zero  l1 -> let (_, x1) as p = lookup 0 l1 in
      let tl = tail l1 in
      assert { elements l1 == cons p (elements tl) };
      One x1 tl
255
    end
256

257 258 259
  (** update in O(log n)
      for this, we need to pass a function that will update the element
      when we find it *)
260

261 262
  function setf (s: seq 'a) (i: int) (f: 'a -> 'a) : seq 'a =
    set s i (f s[i])
263

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

267
  let rec fupdate (f: 'a -> 'a) (i: int) (l: ral 'a) : ral 'a
268
    requires { 0 <= i < length (elements l) }
269 270
    variant  { i, l }
    ensures  { elements result == setf (elements l) i f }
271 272 273 274 275
    =
    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))
276 277 278 279 280 281 282 283 284
    | Zero l1  ->
      let ul1 = fupdate (aux i f) (div i 2) l1 in
      let res = Zero ul1 in
      assert { forall j. 0 <= j < length (elements res) ->
        (elements res)[j] = (setf (elements l) i f)[j]
        by div j 2 <> div i 2 ->
          (elements ul1)[div j 2] = (elements l1)[div j 2]
      };
      res
285 286
    end

287
  let function f (y: 'a) : 'a -> 'a = fun _ -> y
288 289 290 291 292 293

  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
294

295
end