examples/random_access_list.mlw

   1
   2 (** Random Access Lists.
   3     (Okasaki, "Purely Functional Data Structures", 10.1.2.)
   4
   5     The code below uses polymorphic recursion (both in the logic
   6     and in the programs).
   7
   8     Author: Jean-Christophe Filliâtre (CNRS)
   9  *)
  10
  11 module RandomAccessList
  12
  13   use int.Int
  14   use int.ComputerDivision
  15   use list.List
  16   use list.Length
  17   use list.Nth
  18   use option.Option
  19
  20   type ral 'a =
  21   | Empty
  22   | Zero    (ral ('a, 'a))
  23   | One  'a (ral ('a, 'a))
  24
  25   function flatten (l: list ('a, 'a)) : list 'a =
  26     match l with
  27     | Nil -> Nil
  28     | Cons (x, y) l1 -> Cons x (Cons y (flatten l1))
  29     end
  30
  31   let rec lemma length_flatten (l:list ('a, 'a))
  32     ensures { length (flatten l) = 2 * length l }
  33     variant { l }
  34     =
  35     match l with
  36     | Cons (_,_) q -> length_flatten q
  37     | Nil -> ()
  38     end
  39
  40   function elements (l: ral 'a) : list 'a =
  41     match l with
  42     | Empty    -> Nil
  43     | Zero l1  -> flatten (elements l1)
  44     | One x l1 -> Cons x (flatten (elements l1))
  45     end
  46
  47   let rec size (l: ral 'a) : int
  48     variant { l }
  49     ensures { result = length (elements l) }
  50     =
  51     match l with
  52     | Empty    -> 0
  53     | Zero  l1 ->     2 * size l1
  54     | One _ l1 -> 1 + 2 * size l1
  55     end
  56
  57   let rec cons (x: 'a) (l: ral 'a) : ral 'a
  58     variant { l }
  59     ensures { elements result = Cons x (elements l) }
  60     =
  61     match l with
  62     | Empty    -> One x Empty
  63     | Zero l1  -> One x l1
  64     | One y l1 -> Zero (cons (x, y) l1)
  65     end
  66
  67   let rec lemma nth_flatten (i: int) (l: list ('a, 'a))
  68     requires { 0 <= i < length l }
  69     variant  { l }
  70     ensures  { match nth i l with
  71                | None -> false
  72                | Some (x0, x1) -> Some x0 = nth (2 * i)     (flatten l) /\
  73                                   Some x1 = nth (2 * i + 1) (flatten l) end }
  74     =
  75     match l with
  76     | Nil -> ()
  77     | Cons _ r -> if i > 0 then nth_flatten (i-1) r
  78     end
  79
  80   let rec lookup (i: int) (l: ral 'a) : 'a
  81     requires { 0 <= i < length (elements l) }
  82     variant  { i, l }
  83     ensures  { nth i (elements l) = Some result }
  84     =
  85     match l with
  86     | Empty    -> absurd
  87     | One x l1 -> if i = 0 then x else lookup (i-1) (Zero l1)
  88     | Zero l1  -> let (x0, x1) = lookup (div i 2) l1 in
  89                   if mod i 2 = 0 then x0 else x1
  90     end
  91
  92   let rec tail (l: ral 'a) : ral 'a
  93     requires { elements l <> Nil }
  94     variant  { l }
  95     ensures  { match elements l with
  96                | Nil -> false
  97                | Cons _ l -> elements result = l
  98                end }
  99     =
 100     match l with
 101     | Empty    -> absurd
 102     | One _ l1 -> Zero l1
 103     | Zero  l1 -> let (_, x1) = lookup 0 l1 in One x1 (tail l1)
 104     end
 105
 106   let rec update (i: int) (y: 'a) (l: ral 'a) : ral 'a
 107     requires { 0 <= i < length (elements l) }
 108     variant  { i, l}
 109     ensures  { nth i (elements result) = Some y}
 110     ensures  { forall j. 0 <= j < length (elements l) ->
 111                j <> i -> nth j (elements result) = nth j (elements l) }
 112     ensures  { length (elements result) = length (elements l) }
 113     ensures  { match result, l with
 114                | One _ _, One _ _ | Zero _, Zero _ -> true
 115                | _                                 -> false
 116                end }
 117     =
 118     match l with
 119     | Empty    -> absurd
 120     | One x l1 -> if i = 0 then One y l1 else
 121                   match update (i-1) y (Zero l1) with
 122                   | Empty | One _ _ -> absurd
 123                   | Zero l1         -> One x l1
 124                   end
 125     | Zero l1  ->
 126         let (x0, x1) = lookup (div i 2) l1 in
 127         let l1' =
 128           update (div i 2) (if mod i 2 = 0 then (y,x1) else (x0,y)) l1 in
 129         assert { forall j. 0 <= j < length (elements l) -> j <> i ->
 130                  match nth (div j 2) (elements l1) with
 131                  | None -> false
 132                  | Some (x0,_) -> Some x0 = nth (2 * (div j 2)) (elements l)
 133                  end
 134                  && nth j (elements l) = nth j (elements (Zero l1')) };
 135         Zero l1'
 136     end
 137
 138 end
 139
 140 (** A straightforward encapsulation with a list ghost model
 141     (in anticipation of module refinement) *)
 142
 143 module RAL
 144
 145   use int.Int
 146   use list.List
 147   use list.Length
 148   use option.Option
 149   use list.Nth
 150   use RandomAccessList
 151
 152   type t 'a = { r: ral 'a; ghost l: list 'a }
 153     invariant { l = elements r }
 154
 155   let constant empty : t 'a = { r = Empty; l = Nil }
 156     ensures { result.l = Nil }
 157
 158   let size (t: t 'a) : int
 159     ensures { result = length t.l }
 160     =
 161     size t.r
 162
 163   let cons (x: 'a) (s: t 'a) : t 'a
 164     ensures { result.l = Cons x s.l }
 165     =
 166     { r = cons x s.r; l = Cons x s.l }
 167
 168   let lookup (i: int) (s: t 'a) : 'a
 169     requires { 0 <= i < length s.l }
 170     ensures { Some result = nth i s.l }
 171     =
 172     lookup i s.r
 173
 174 end
 175
 176 (** Model using sequences instead of lists *)
 177
 178 module RandomAccessListWithSeq
 179
 180   use int.Int
 181   use int.ComputerDivision
 182   use seq.Seq
 183
 184   type ral 'a =
 185   | Empty
 186   | Zero    (ral ('a, 'a))
 187   | One  'a (ral ('a, 'a))
 188
 189   function flatten (s: seq ('a, 'a)) : seq 'a =
 190     create (2 * length s)
 191            (fun i -> let (x0, x1) = s[div i 2] in
 192                      if mod i 2 = 0 then x0 else x1)
 193
 194   lemma cons_flatten : forall x y :'a,s:seq ('a,'a).
 195     let a = flatten (cons (x,y) s) in
 196     let b = cons x (cons y (flatten s)) in
 197     a = b by a == b by forall i. 0 <= i < a.length -> a[i] = b[i]
 198     by (i <= 1 so (cons (x,y) s)[div i 2] = (x,y))
 199        \/ (i >= 2 so (cons (x,y) s)[div i 2] = s[div (i-2) 2]
 200        )
 201
 202   function elements (l: ral 'a) : seq 'a =
 203     match l with
 204     | Empty    -> empty
 205     | Zero l1  -> flatten (elements l1)
 206     | One x l1 -> cons x (flatten (elements l1))
 207     end
 208
 209   let rec size (l: ral 'a) : int
 210     variant { l }
 211     ensures { result = length (elements l) }
 212     =
 213     match l with
 214     | Empty    -> 0
 215     | Zero  l1 ->     2 * size l1
 216     | One _ l1 -> 1 + 2 * size l1
 217     end
 218
 219   let rec cons (x: 'a) (l: ral 'a) : ral 'a
 220     variant { l }
 221     ensures { elements result == cons x (elements l) }
 222     =
 223     match l with
 224     | Empty    -> One x Empty
 225     | Zero l1  -> One x l1
 226     | One y l1 -> Zero (cons (x, y) l1)
 227     end
 228
 229   let rec lookup (i: int) (l: ral 'a) : 'a
 230     requires { 0 <= i < length (elements l) }
 231     variant  { i, l }
 232     ensures  { (elements l)[i] = result }
 233     =
 234     match l with
 235     | Empty    -> absurd
 236     | One x l1 -> if i = 0 then x else lookup (i-1) (Zero l1)
 237     | Zero l1  -> let (x0, x1) = lookup (div i 2) l1 in
 238                   if mod i 2 = 0 then x0 else x1
 239     end
 240
 241    let rec tail (l: ral 'a) : ral 'a
 242     requires { 0 < length (elements l) }
 243     variant  { l }
 244     ensures  { elements result == (elements l)[1..] }
 245     =
 246     match l with
 247     | Empty    -> absurd
 248     | One _ l1 -> Zero l1
 249     | Zero  l1 -> let (_, x1) as p = lookup 0 l1 in
 250       let tl = tail l1 in
 251       assert { elements l1 == cons p (elements tl) };
 252       One x1 tl
 253     end
 254
 255   (** update in O(log n)
 256       for this, we need to pass a function that will update the element
 257       when we find it *)
 258
 259   function setf (s: seq 'a) (i: int) (f: 'a -> 'a) : seq 'a =
 260     set s i (f s[i])
 261
 262   let function aux (i: int) (f: 'a -> 'a) : ('a, 'a) -> ('a, 'a) =
 263     fun z -> let (x,y) = z in if mod i 2 = 0 then (f x, y) else (x, f y)
 264
 265   let rec fupdate (f: 'a -> 'a) (i: int) (l: ral 'a) : ral 'a
 266     requires { 0 <= i < length (elements l) }
 267     variant  { i, l }
 268     ensures  { elements result == setf (elements l) i f }
 269     =
 270     match l with
 271     | Empty    -> absurd
 272     | One x l1 -> if i = 0 then One (f x) l1 else
 273                   cons x (fupdate f (i-1) (Zero l1))
 274     | Zero l1  ->
 275       let ul1 = fupdate (aux i f) (div i 2) l1 in
 276       let res = Zero ul1 in
 277       assert { forall j. 0 <= j < length (elements res) ->
 278         (elements res)[j] = (setf (elements l) i f)[j]
 279         by div j 2 <> div i 2 ->
 280           (elements ul1)[div j 2] = (elements l1)[div j 2]
 281       };
 282       res
 283     end
 284
 285   let function f (y: 'a) : 'a -> 'a = fun _ -> y
 286
 287   let update (i: int) (y: 'a) (l: ral 'a) : ral 'a
 288     requires { 0 <= i < length (elements l) }
 289     ensures  { elements result == set (elements l) i y}
 290     =
 291     fupdate (f y) i  l
 292
 293 end