random_access_list.mlw 7.98 KB
 Jean-Christophe Filliatre committed May 02, 2015 1 2 `````` (** Random Access Lists. `````` Jean-Christophe Filliatre committed May 20, 2015 3 `````` (Okasaki, "Purely Functional Data Structures", 10.1.2.) `````` Jean-Christophe Filliatre committed May 02, 2015 4 5 6 7 `````` The code below uses polymorphic recursion (both in the logic and in the programs). `````` Jean-Christophe Filliatre committed May 20, 2015 8 `````` Author: Jean-Christophe Filliâtre (CNRS) `````` Jean-Christophe Filliatre committed May 02, 2015 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)) `````` Jean-Christophe Filliatre committed Jul 06, 2015 25 26 `````` function flatten (l: list ('a, 'a)) : list 'a = match l with `````` Jean-Christophe Filliatre committed May 02, 2015 27 28 29 30 `````` | Nil -> Nil | Cons (x, y) l1 -> Cons x (Cons y (flatten l1)) end `````` Jean-Christophe Filliatre committed May 20, 2015 31 `````` let rec lemma length_flatten (l:list ('a, 'a)) `````` Martin Clochard committed May 04, 2015 32 33 `````` ensures { length (flatten l) = 2 * length l } variant { l } `````` Jean-Christophe Filliatre committed Jul 06, 2015 34 35 `````` = match l with `````` Martin Clochard committed May 04, 2015 36 37 38 39 `````` | Cons (_,_) q -> length_flatten q | Nil -> () end `````` Jean-Christophe Filliatre committed Jul 06, 2015 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 `````` Jean-Christophe Filliatre committed May 02, 2015 46 47 48 49 `````` let rec size (l: ral 'a) : int variant { l } ensures { result = length (elements l) } `````` Jean-Christophe Filliatre committed Jul 06, 2015 50 `````` = `````` Jean-Christophe Filliatre committed May 02, 2015 51 52 53 54 55 56 `````` match l with | Empty -> 0 | Zero l1 -> 2 * size l1 | One _ l1 -> 1 + 2 * size l1 end `````` Léon Gondelman committed Jul 03, 2015 57 `````` let rec cons (x: 'a) (l: ral 'a) : ral 'a `````` Jean-Christophe Filliatre committed May 02, 2015 58 59 `````` variant { l } ensures { elements result = Cons x (elements l) } `````` Jean-Christophe Filliatre committed Jul 06, 2015 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 `````` Jean-Christophe Filliatre committed May 02, 2015 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 } `````` Jean-Christophe Filliatre committed Jul 06, 2015 74 75 `````` = match l with `````` Jean-Christophe Filliatre committed May 02, 2015 76 77 78 79 `````` | Nil -> () | Cons _ r -> if i > 0 then nth_flatten (i-1) r end `````` Léon Gondelman committed Jul 03, 2015 80 `````` let rec lookup (i: int) (l: ral 'a) : 'a `````` Jean-Christophe Filliatre committed May 02, 2015 81 82 83 `````` requires { 0 <= i < length (elements l) } variant { i, l } ensures { nth i (elements l) = Some result } `````` Jean-Christophe Filliatre committed Jul 06, 2015 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 `````` Jean-Christophe Filliatre committed May 02, 2015 91 `````` `````` Jean-Christophe Filliatre committed Jun 24, 2015 92 `````` let rec tail (l: ral 'a) : ral 'a `````` Léon Gondelman committed Jun 23, 2015 93 `````` requires { elements l <> Nil } `````` Jean-Christophe Filliatre committed Jun 24, 2015 94 95 96 97 98 `````` variant { l } ensures { match elements l with | Nil -> false | Cons _ l -> elements result = l end } `````` Jean-Christophe Filliatre committed Jul 06, 2015 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 `````` Léon Gondelman committed Jun 23, 2015 105 `````` `````` Léon Gondelman committed Jul 03, 2015 106 `````` let rec update (i: int) (y: 'a) (l: ral 'a) : ral 'a `````` Léon Gondelman committed Jun 23, 2015 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 } `````` Jean-Christophe Filliatre committed Jul 06, 2015 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 `````` Léon Gondelman committed Jun 23, 2015 137 `````` `````` Jean-Christophe Filliatre committed May 02, 2015 138 ``````end `````` Jean-Christophe Filliatre committed May 02, 2015 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 } `````` Guillaume Melquiond committed Mar 16, 2016 153 `````` invariant { l = elements r } `````` Jean-Christophe Filliatre committed May 02, 2015 154 155 156 `````` let empty () : t 'a ensures { result.l = Nil } `````` Jean-Christophe Filliatre committed Jul 06, 2015 157 `````` = `````` Jean-Christophe Filliatre committed May 02, 2015 158 159 160 161 `````` { r = Empty; l = Nil } let size (t: t 'a) : int ensures { result = length t.l } `````` Jean-Christophe Filliatre committed Jul 06, 2015 162 `````` = `````` Jean-Christophe Filliatre committed May 02, 2015 163 164 165 166 `````` size t.r let cons (x: 'a) (s: t 'a) : t 'a ensures { result.l = Cons x s.l } `````` Jean-Christophe Filliatre committed Jul 06, 2015 167 `````` = `````` Léon Gondelman committed Jul 03, 2015 168 `````` { r = cons x s.r; l = Cons x s.l } `````` Jean-Christophe Filliatre committed May 02, 2015 169 `````` `````` Léon Gondelman committed Jul 03, 2015 170 `````` let lookup (i: int) (s: t 'a) : 'a `````` Jean-Christophe Filliatre committed May 02, 2015 171 172 `````` requires { 0 <= i < length s.l } ensures { Some result = nth i s.l } `````` Jean-Christophe Filliatre committed Jul 06, 2015 173 `````` = `````` Léon Gondelman committed Jul 03, 2015 174 `````` lookup i s.r `````` Jean-Christophe Filliatre committed May 02, 2015 175 176 177 `````` end `````` Jean-Christophe Filliatre committed Jun 24, 2015 178 179 ``````(** Model using sequences instead of lists *) `````` Jean-Christophe Filliatre committed Jun 22, 2015 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)) `````` Jean-Christophe Filliatre committed Jul 06, 2015 191 192 `````` function flatten (s: seq ('a, 'a)) : seq 'a = create (2 * length s) `````` Guillaume Melquiond committed Mar 16, 2016 193 194 `````` (fun i -> let (x0, x1) = s[div i 2] in if mod i 2 = 0 then x0 else x1) `````` Jean-Christophe Filliatre committed Jun 22, 2015 195 `````` `````` Martin Clochard committed Feb 16, 2018 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] ) `````` Jean-Christophe Filliatre committed Jul 06, 2015 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 `````` Jean-Christophe Filliatre committed Jun 22, 2015 210 211 212 213 `````` let rec size (l: ral 'a) : int variant { l } ensures { result = length (elements l) } `````` Jean-Christophe Filliatre committed Jul 06, 2015 214 `````` = `````` Jean-Christophe Filliatre committed Jun 22, 2015 215 216 217 218 219 220 `````` match l with | Empty -> 0 | Zero l1 -> 2 * size l1 | One _ l1 -> 1 + 2 * size l1 end `````` Léon Gondelman committed Jul 03, 2015 221 `````` let rec cons (x: 'a) (l: ral 'a) : ral 'a `````` Jean-Christophe Filliatre committed Jun 22, 2015 222 223 `````` variant { l } ensures { elements result == cons x (elements l) } `````` Jean-Christophe Filliatre committed Jul 06, 2015 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 `````` Jean-Christophe Filliatre committed Jun 22, 2015 230 `````` `````` Léon Gondelman committed Jul 03, 2015 231 `````` let rec lookup (i: int) (l: ral 'a) : 'a `````` Jean-Christophe Filliatre committed Jun 22, 2015 232 233 234 `````` requires { 0 <= i < length (elements l) } variant { i, l } ensures { (elements l)[i] = result } `````` Jean-Christophe Filliatre committed Jul 06, 2015 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 `````` Jean-Christophe Filliatre committed Jun 22, 2015 242 `````` `````` Léon Gondelman committed Jun 23, 2015 243 `````` let rec tail (l: ral 'a) : ral 'a `````` Jean-Christophe Filliatre committed Jun 24, 2015 244 245 246 `````` requires { 0 < length (elements l) } variant { l } ensures { elements result == (elements l)[1 .. ] } `````` Jean-Christophe Filliatre committed Jul 06, 2015 247 248 249 250 `````` = match l with | Empty -> absurd | One _ l1 -> Zero l1 `````` Martin Clochard committed Feb 16, 2018 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 `````` Jean-Christophe Filliatre committed Jul 06, 2015 255 `````` end `````` Léon Gondelman committed Jul 03, 2015 256 `````` `````` Jean-Christophe Filliatre committed Jul 06, 2015 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 *) `````` Léon Gondelman committed Jul 03, 2015 260 `````` `````` Jean-Christophe Filliatre committed Jul 06, 2015 261 262 `````` function setf (s: seq 'a) (i: int) (f: 'a -> 'a) : seq 'a = set s i (f s[i]) `````` Léon Gondelman committed Jul 03, 2015 263 `````` `````` Guillaume Melquiond committed Mar 21, 2016 264 `````` let function aux (i: int) (f: 'a -> 'a) : ('a, 'a) -> ('a, 'a) = `````` Guillaume Melquiond committed Mar 16, 2016 265 `````` fun z -> let (x,y) = z in if mod i 2 = 0 then (f x, y) else (x, f y) `````` Léon Gondelman committed Jul 03, 2015 266 `````` `````` Jean-Christophe Filliatre committed Jul 06, 2015 267 `````` let rec fupdate (f: 'a -> 'a) (i: int) (l: ral 'a) : ral 'a `````` Léon Gondelman committed Jun 23, 2015 268 `````` requires { 0 <= i < length (elements l) } `````` Martin Clochard committed Feb 16, 2018 269 270 `````` variant { i, l } ensures { elements result == setf (elements l) i f } `````` Jean-Christophe Filliatre committed Jul 06, 2015 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)) `````` Martin Clochard committed Feb 16, 2018 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 `````` Jean-Christophe Filliatre committed Jul 06, 2015 285 286 `````` end `````` Guillaume Melquiond committed Mar 18, 2016 287 `````` let function f (y: 'a) : 'a -> 'a = fun _ -> y `````` Jean-Christophe Filliatre committed Jul 06, 2015 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 `````` Léon Gondelman committed Jul 03, 2015 294 `````` `````` Jean-Christophe Filliatre committed Jun 22, 2015 295 ``end``