random_access_lists: consistent indentation

parent d0b4d95b
......@@ -22,8 +22,8 @@ module RandomAccessList
| Zero (ral ('a, 'a))
| One 'a (ral ('a, 'a))
function flatten (l: list ('a, 'a)) : list 'a
= match l with
function flatten (l: list ('a, 'a)) : list 'a =
match l with
| Nil -> Nil
| Cons (x, y) l1 -> Cons x (Cons y (flatten l1))
end
......@@ -31,22 +31,23 @@ module RandomAccessList
let rec lemma length_flatten (l:list ('a, 'a))
ensures { length (flatten l) = 2 * length l }
variant { l }
= match l with
=
match l with
| Cons (_,_) q -> length_flatten q
| Nil -> ()
end
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
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
let rec size (l: ral 'a) : int
variant { l }
ensures { result = length (elements l) }
=
=
match l with
| Empty -> 0
| Zero l1 -> 2 * size l1
......@@ -56,11 +57,12 @@ module RandomAccessList
let rec cons (x: 'a) (l: ral 'a) : ral 'a
variant { l }
ensures { elements result = Cons x (elements l) }
= match l with
| Empty -> One x Empty
| Zero l1 -> One x l1
| One y l1 -> Zero (cons (x, y) l1)
end
=
match l with
| Empty -> One x Empty
| Zero l1 -> One x l1
| One y l1 -> Zero (cons (x, y) l1)
end
let rec lemma nth_flatten (i: int) (l: list ('a, 'a))
requires { 0 <= i < length l }
......@@ -69,7 +71,8 @@ module RandomAccessList
| None -> false
| Some (x0, x1) -> Some x0 = nth (2 * i) (flatten l) /\
Some x1 = nth (2 * i + 1) (flatten l) end }
= match l with
=
match l with
| Nil -> ()
| Cons _ r -> if i > 0 then nth_flatten (i-1) r
end
......@@ -78,12 +81,13 @@ module RandomAccessList
requires { 0 <= i < length (elements l) }
variant { i, l }
ensures { nth i (elements l) = Some result }
= 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
=
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
let rec tail (l: ral 'a) : ral 'a
requires { elements l <> Nil }
......@@ -92,11 +96,12 @@ module RandomAccessList
| Nil -> false
| Cons _ l -> elements result = l
end }
= match l with
| Empty -> absurd
| One _ l1 -> Zero l1
| Zero l1 -> let (_, x1) = lookup 0 l1 in One x1 (tail l1)
end
=
match l with
| Empty -> absurd
| One _ l1 -> Zero l1
| Zero l1 -> let (_, x1) = lookup 0 l1 in One x1 (tail l1)
end
let rec update (i: int) (y: 'a) (l: ral 'a) : ral 'a
requires { 0 <= i < length (elements l) }
......@@ -109,24 +114,26 @@ module RandomAccessList
| One _ _, One _ _ | Zero _, Zero _ -> true
| _ -> false
end }
= 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
=
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
end
......@@ -147,23 +154,23 @@ module RAL
let empty () : t 'a
ensures { result.l = Nil }
=
=
{ r = Empty; l = Nil }
let size (t: t 'a) : int
ensures { result = length t.l }
=
=
size t.r
let cons (x: 'a) (s: t 'a) : t 'a
ensures { result.l = Cons x s.l }
=
=
{ r = cons x s.r; l = Cons x s.l }
let lookup (i: int) (s: t 'a) : 'a
requires { 0 <= i < length s.l }
ensures { Some result = nth i s.l }
=
=
lookup i s.r
end
......@@ -181,22 +188,22 @@ module RandomAccessListWithSeq
| Zero (ral ('a, 'a))
| One 'a (ral ('a, 'a))
function flatten (s: seq ('a, 'a)) : seq 'a
= create (2 * length s)
(\ i: int. let (x0, x1) = s[div i 2] in
if mod i 2 = 0 then x0 else x1)
function flatten (s: seq ('a, 'a)) : seq 'a =
create (2 * length s)
(\ i: int. let (x0, x1) = s[div i 2] in
if mod i 2 = 0 then x0 else x1)
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
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
let rec size (l: ral 'a) : int
variant { l }
ensures { result = length (elements l) }
=
=
match l with
| Empty -> 0
| Zero l1 -> 2 * size l1
......@@ -206,58 +213,64 @@ module RandomAccessListWithSeq
let rec cons (x: 'a) (l: ral 'a) : ral 'a
variant { l }
ensures { elements result == cons x (elements l) }
= match l with
| Empty -> One x Empty
| Zero l1 -> One x l1
| One y l1 -> Zero (cons (x, y) l1)
end
=
match l with
| Empty -> One x Empty
| Zero l1 -> One x l1
| One y l1 -> Zero (cons (x, y) l1)
end
let rec lookup (i: int) (l: ral 'a) : 'a
requires { 0 <= i < length (elements l) }
variant { i, l }
ensures { (elements l)[i] = result }
= 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
=
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
let rec tail (l: ral 'a) : ral 'a
requires { 0 < length (elements l) }
variant { l }
ensures { elements result == (elements l)[1 .. ] }
= match l with
| Empty -> absurd
| One _ l1 -> Zero l1
| Zero l1 -> let (_, x1) = lookup 0 l1 in One x1 (tail l1)
end
=
match l with
| Empty -> absurd
| One _ l1 -> Zero l1
| Zero l1 -> let (_, x1) = lookup 0 l1 in One x1 (tail l1)
end
function setf (s: seq 'a) (i:int) (f: 'a -> 'a) : seq 'a =
set s i (f s[i])
(** update in O(log n)
for this, we need to pass a function that will update the element
when we find it *)
function setf (s: seq 'a) (i: int) (f: 'a -> 'a) : seq 'a =
set s i (f s[i])
function aux (i: int) (f: 'a -> 'a) : ('a,'a) -> ('a, 'a) =
\ z. let (x,y) = z in if mod i 2 = 0 then (f x, y) else (x, f y)
function aux (i: int) (f: 'a -> 'a) : ('a, 'a) -> ('a, 'a) =
\ z. let (x,y) = z in if mod i 2 = 0 then (f x, y) else (x, f y)
let rec fupdate (f: 'a -> 'a) (i: int) (l: ral 'a) : ral 'a
let rec fupdate (f: 'a -> 'a) (i: int) (l: ral 'a) : ral 'a
requires { 0 <= i < length (elements l) }
variant { i, l}
ensures { elements result == setf (elements l) i f}
= 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
function f (y: 'a) : 'a -> 'a = \ _. y
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
=
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
function f (y: 'a) : 'a -> 'a = \ _. y
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
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment