Commit fb0b65dc authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

examples: replace unused lambda-binders with underscores

parent e43c3352
......@@ -4,44 +4,44 @@
(** {2 Association with respect to an equivalence relation} *)
module Assoc
(** Abstract type for objects identified by keys. *)
clone import key_type.KeyType as K
(** Abstract equivalence relation. *)
clone import relations.Equivalence as Eq with type t = key
use import list.List
use import list.Mem
use import list.Append
use import option.Option
use import HighOrd
(** Existence of an element identified by key [k] in list [l]. *)
predicate appear (k:key) (l:list (t 'a)) =
exists x. mem x l /\ Eq.rel k x.key
lemma appear_append : forall k:key,l r:list (t 'a).
appear k (l++r) <-> appear k l \/ appear k r
(** Unique occurence of every key *)
predicate unique (l:list (t 'a)) = match l with
| Nil -> true
| Cons x q -> not appear x.key q /\ unique q
end
(** Functional update with equivalence classes. *)
function equiv_update (f:key -> 'b) (k:key) (b:'b) : key -> 'b =
\k2. if Eq.rel k k2 then b else f k2
function const_none : 'a -> option 'b = \x.None
function const_none : 'a -> option 'b = \_.None
(** Association list viewed as a partial mapping *)
function model (l:list (t 'a)) : key -> option (t 'a) =
match l with
| Nil -> const_none
| Cons d q -> equiv_update (model q) d.key (Some d)
end
(** A key is bound iff it occurs in the association lists.
Equivalently, [appear] describe the domain of the partial mapping. *)
let rec lemma model_domain (k:key) (l:list (t 'a)) : unit
......@@ -50,14 +50,14 @@ module Assoc
ensures { not appear k l <-> model l k = None }
variant { l }
= match l with Cons _ q -> model_domain k q | _ -> () end
(** A key is bound to a value with an equivalent key. *)
let rec lemma model_key (k:key) (l:list (t 'a)) : unit
ensures { match model l k with None -> true
| Some d -> Eq.rel k d.key end }
variant { l }
= match l with Cons _ q -> model_key k q | _ -> () end
(** Congruence lemma. *)
let rec lemma model_congruence (k1 k2:key) (l:list (t 'a)) : unit
requires { Eq.rel k1 k2 }
......@@ -67,7 +67,7 @@ module Assoc
| Cons _ q -> model_congruence k1 k2 q
| _ -> ()
end
(** If the list satisfies the uniqueness property,
then every value occuring in the list is the image of its key. *)
let rec lemma model_unique (k:key) (l:list (t 'a)) : unit
......@@ -75,12 +75,12 @@ module Assoc
ensures { forall d. mem d l -> model l d.key = Some d }
variant { l }
= match l with Cons _ q -> model_unique k q | _ -> () end
(** Singleton association list. *)
let lemma model_singleton (k:key) (d:t 'a) : unit
ensures { model (Cons d Nil) k = if rel k d.key then Some d else None }
= ()
(** Link between disjoint concatenation and disjoint union of
partial mappings. *)
let rec lemma model_concat (k:key) (l r:list (t 'a)) : unit
......@@ -97,19 +97,19 @@ module Assoc
| Nil -> ()
| Cons _ q -> model_concat k q r
end
end
(** {2 Sorted association lists} *)
module AssocSorted
use import list.List
use import list.Append
use import list.Mem
use import option.Option
(** It is an instance of association lists. *)
clone import key_type.KeyType as K
clone import preorder.Full as O with type t = key
......@@ -126,14 +126,14 @@ module AssocSorted
function K.key = K.key,
predicate O.rel = O.lt,
goal O.Trans
(** Sorted lists have unicity property. *)
let rec lemma increasing_unique (l:list (t 'a)) : unit
requires { S.increasing l }
ensures { unique l }
variant { l }
= match l with Cons _ q -> increasing_unique q | _ -> () end
(** Description of the partial mapping corresponding to the concatenation
of increasing lists separated by a known key in the middle. *)
let lemma model_cut (k:key) (l r:list (t 'a)) : unit
......@@ -165,7 +165,7 @@ module AssocSorted
end && false };
assert { forall k2. eq k k2 -> model (l++r) k2 <> None ->
(not appear k2 l /\ not appear k2 r) && false }
(** Description of the partial mapping corresponding to a list
split around a midpoint. *)
let lemma model_split (d:t 'a) (l r:list (t 'a)) : unit
......@@ -179,6 +179,6 @@ module AssocSorted
ensures { forall k2. lt k2 d.key -> model (l++Cons d r) k2 = model l k2 }
ensures { forall k2. le d.key k2 -> model l k2 = None }
= ()
end
......@@ -4,11 +4,11 @@
(** {2 Preliminary definitions} *)
theory SelectionTypes
use import list.List
use import option.Option
use import list.Append
(** Describe a position in the list [left ++ middle ++ right]
(see [rebuild]) *)
type split 'a = {
......@@ -16,53 +16,53 @@ theory SelectionTypes
middle : option 'a;
right : list 'a;
}
(** Describe reduced problem for selection (see [selected_part]) *)
type part_base 'a = Left 'a
| Right 'a
| Here
(** Reconstruct the list associated to a split. *)
function rebuild (p:split 'a) : list 'a =
match p.middle with
| Some x -> p.left ++ Cons x p.right
| None -> p.left ++ p.right
end
function option_to_list (o:option 'a) : list 'a =
match o with
| Some x -> Cons x Nil
| None -> Nil
end
(** Alternative definition for [rebuild]. *)
lemma rebuild_aternative_def : forall p:split 'a.
rebuild p = p.left ++ option_to_list p.middle ++ p.right
(** Shortcuts for extending a split on the left/right. *)
function left_extend (l:list 'a) (d:'a) (e:split 'a) : split 'a =
{ e with left = l ++ Cons d e.left }
function right_extend (e:split 'a) (d:'a) (r:list 'a) : split 'a =
{ e with right = e.right ++ Cons d r }
end
(** {2 AVL trees} *)
module AVL
(** {3 Rebalancing code}
The first part of the module implements the rebalancing code.
It can also be seen as an implementation of logarithmic-time
catenable dequeues with a constant-time nearly-fair splitting
operation (derived from tree pattern-matching).
(About the time complexity bounds: a call to an abstract
routine (monoid operations, element measure,...) is assumed to
take constant time) *)
use import int.Int
use import bool.Bool
use import list.List
......@@ -70,7 +70,7 @@ module AVL
use import HighOrd
use import option.Option
use import ref.Ref
(** The implementation is parameterized by an abstract monoid.
The elements of the monoid will be used as summaries of
sequence of elements, obtained by aggregation of the elements of
......@@ -83,33 +83,33 @@ module AVL
function M.op = M.op,
goal M.assoc,
goal M.neutral
(** Abstract description of the data stored in the tree. *)
namespace D
type t 'a
(** Elements can be measured. *)
function measure (t 'a) : M.t
val measure (x:t 'a) : M.t ensures { measure x = result }
end
(** Actual height difference permitted between subtrees.
The balancing can be any positive integer. This is a trade-off between
the cost of balancing and the cost of finding:
the bigger the balancing constant is, the lesser is the need for
balancing the tree, but the deeper the trees may be. *)
constant balancing : int
axiom balancing_positive : balancing > 0
(** tree representation.
Height and monoidal summary are cached at every node. *)
type tree 'a =
| Empty
| Node (tree 'a) (D.t 'a) (tree 'a) int M.t
(** Logical model of an AVL tree.
An AVL tree is intended to represent a sequence of elements, which we
model using a list. It corresponds to the sequence of elements obtained
by left-to-right infix order (note that this sequence is invariant by
......@@ -121,24 +121,24 @@ module AVL
lis : list (D.t 'a);
hgt : int;
}
function node_model (l:list 'a) (d:'a) (r:list 'a) : list 'a =
l ++ Cons d r
(** Sequence of elements obtained by infix-order traversal. *)
function list_model (t:tree 'a) : list (D.t 'a) =
match t with
| Empty -> Nil
| Node l d r _ _ -> node_model (list_model l) d (list_model r)
end
(** Height of the tree. *)
function real_height (t:tree 'a) : int = match t with
| Empty -> 0
| Node l _ r _ _ -> let hl = real_height l in let hr = real_height r in
1 + if hl < hr then hr else hl
end
(** Height is non-negative. *)
let rec lemma real_height_nonnegative (t:tree 'a) : unit
ensures { real_height t >= 0 }
......@@ -147,14 +147,14 @@ module AVL
| Empty -> ()
| Node l _ r _ _ -> real_height_nonnegative l; real_height_nonnegative r
end
(** Balanced tree + correctness of cached annotations: at every node,
1) The additional integer is the height of the corresponding subtree
2) The monoidal value corresponds to the summary of the sequence of
elements associated with the subtree associated with the node
3) Left and right subtrees are [balancing]-height-balanced *)
predicate balanced (t:tree 'a) = match t with
| Empty -> true
......@@ -163,12 +163,12 @@ module AVL
-balancing <= real_height r - real_height l <= balancing /\
balanced l /\ balanced r
end
(** Tree rotations preserve the in-order sequence of element *)
lemma rotation_preserve_model : forall ld rd:'a,fl fm fr:list 'a.
node_model (node_model fl ld fm) rd fr =
node_model fl ld (node_model fm rd fr)
(** Actual program type for AVL trees *)
type t 'a = {
(* Representation as a binary tree. *)
......@@ -176,14 +176,14 @@ module AVL
(* Model. *)
ghost m : m 'a;
}
(** Invariant (c as correct). *)
predicate c (a:t 'a) =
let tree = a.repr in
balanced tree /\
a.m.lis = list_model tree /\
a.m.hgt = real_height tree
(** Compute the height of the tree. O(1) since the height is cached. *)
let height (t:t 'a) : int
requires { c t }
......@@ -192,7 +192,7 @@ module AVL
| Empty -> 0
| Node _ _ _ h _ -> h
end
(** Compute the monoidal summary of the elements stored in the structure.
constant-time. *)
let total (t:t 'a) : M.t
......@@ -202,12 +202,12 @@ module AVL
| Empty -> M.zero ()
| Node _ _ _ _ m -> m
end
(** Create an empty AVL tree. *)
let empty () : t 'a
ensures { result.m.lis = Nil /\ result.m.hgt = 0 /\ c result }
= { repr = Empty; m = { lis = Nil; hgt = 0 } }
(** re-specify the node constructor in terms of the logical model. *)
let node (l:t 'a) (d:D.t 'a) (r:t 'a) : t 'a
requires { -balancing <= l.m.hgt - r.m.hgt <= balancing /\ c l /\ c r }
......@@ -220,13 +220,13 @@ module AVL
{ repr = Node l.repr d r.repr h s;
m = { lis = node_model l.m.lis d r.m.lis;
hgt = h } }
(** Create a one-element AVL tree. *)
let singleton (d:D.t 'a) : t 'a
ensures { result.m.lis = Cons d Nil /\ result.m.hgt = 1 /\ c result }
= { repr = Node Empty d Empty 1 (D.measure d);
m = { lis = Cons d Nil; hgt = 1 } }
(** Emptyness test. constant-time. *)
let is_empty (t:t 'a) : bool
requires { c t }
......@@ -235,12 +235,12 @@ module AVL
| Empty -> true
| _ -> false
end
(** View of an AVL tree for pattern-matching. *)
type view 'a =
| AEmpty
| ANode (t 'a) (D.t 'a) (t 'a) int M.t
(** Specification wrapper around pattern-matching, in terms
of the logical model only. In terms of the model, it corresponds
to an operation splitting a non-empty list into three parts,
......@@ -267,7 +267,7 @@ module AVL
h
s
end
(** First re-balancing constructor: [balance l d r]
build the same sequence as [node l d r], but permit slightly
unbalanced input, and might decrement the expected height by one.
......@@ -312,7 +312,7 @@ module AVL
end
end
else node l d r
(** Internal routine. Decompose [l ++ [d] ++ r] as [[head]++tail],
with sequences represented by AVL trees. *)
let rec decompose_front_node (l:t 'a) (d:D.t 'a) (r:t 'a) : (D.t 'a,t 'a)
......@@ -327,7 +327,7 @@ module AVL
| ANode l d2 r2 _ _ -> let (d3,left) = decompose_front_node l d2 r2 in
(d3,balance left d r)
end
(** Pattern-matching over the front of the sequence. Time proportional
to the height (logarithmic in the size of the tree). *)
let decompose_front (t:t 'a) : option (D.t 'a,t 'a)
......@@ -338,8 +338,8 @@ module AVL
| AEmpty -> None
| ANode l d r _ _ -> Some (decompose_front_node l d r)
end
(** Internal routine, mirror of [decompose_front_node]. *)
let rec decompose_back_node (l:t 'a) (d:D.t 'a) (r:t 'a) : (t 'a,D.t 'a)
requires { -balancing <= l.m.hgt - r.m.hgt <= balancing /\ c l /\ c r }
......@@ -354,7 +354,7 @@ module AVL
| ANode l2 d2 r _ _ -> let (right,d3) = decompose_back_node l2 d2 r in
(balance l d right,d3)
end
(** Pattern-matching over the back of the sequence. Time proportional
to the height (logarithmic in the size of the tree). *)
let decompose_back (t:t 'a) : option (t 'a,D.t 'a)
......@@ -365,7 +365,7 @@ module AVL
| AEmpty -> None
| ANode l d r _ _ -> Some (decompose_back_node l d r)
end
(** Internal routine. *)
let rec front_node (ghost li:ref (list (D.t 'a))) (l:t 'a)
(d:D.t 'a) : D.t 'a
......@@ -377,7 +377,7 @@ module AVL
| ANode l d2 r _ _ -> let res = front_node li l d2 in
li := !li ++ r.m.lis ++ Cons d Nil; res
end
(** Get the first element of a non-empty sequence.
The ghost reference is used to get an explicit
view of the tail (no existential). logarithmic-time. *)
......@@ -389,7 +389,7 @@ module AVL
| ANode l d2 r _ _ -> let res = front_node li l d2 in
li := !li ++ r.m.lis; res
end
(** Internal routine. *)
let rec back_node (ghost li:ref (list (D.t 'a))) (d:D.t 'a)
(r:t 'a) : D.t 'a
......@@ -401,7 +401,7 @@ module AVL
| ANode l d2 r _ _ -> let res = back_node li d2 r in
li := Cons d l.m.lis ++ !li; res
end
(** Get the back of a non-empty sequence. logarithmic-time. *)
let back (ghost li:ref (list (D.t 'a))) (t:t 'a) : D.t 'a
requires { match t.m.lis with Nil -> false | _ -> true end /\ c t }
......@@ -411,7 +411,7 @@ module AVL
| ANode l d2 r _ _ -> let res = back_node li d2 r in
li := l.m.lis ++ !li; res
end
(** Catenation with balanced inputs (like sibling subtrees).
logarithmic-time. *)
let fuse (l r:t 'a) : t 'a
......@@ -429,7 +429,7 @@ module AVL
balance l d0 r'
end
end
(** List cons: build the sequence [[d]++t]. logarithmic-time. *)
let rec cons (d:D.t 'a) (t:t 'a) : t 'a
requires { c t }
......@@ -440,7 +440,7 @@ module AVL
| AEmpty -> singleton d
| ANode l d2 r _ _ -> balance (cons d l) d2 r
end
(** Reverse cons: build [t++[d]]. logarithmic-time. *)
let rec snoc (t:t 'a) (d:D.t 'a) : t 'a
requires { c t }
......@@ -451,7 +451,7 @@ module AVL
| AEmpty -> singleton d
| ANode l d2 r _ _ -> balance l d2 (snoc r d)
end
(** Variant of the node constructor without any height hypothesis.
The time complexity is proportional to the height
difference between [l] and [r] (O(|l.m.hgt-r.m.hgt|)) (in particular,
......@@ -475,7 +475,7 @@ module AVL
else node l d r
end
end
(** Catenation, without height hypothesis. logarithmic-time. *)
let concat (l r:t 'a) : t 'a
requires { c l /\ c r }
......@@ -488,65 +488,65 @@ module AVL
join l d0 r'
end
end
(** {3 Selection of elements}
This part of the module provide an implementation of a generalisation
of the usual insertion/removal/lookup/spliting/etc algorithms on
AVL trees. The generalisation is done with respect to an abstract
binary search mechanism. It is based on the observation that
all those algorithms have the shame shape:
1) find a particular position in the tree by binary search (either
a node, or an empty leaf if finding nothing)
2) extract some piece of information from this position/recompute
another tree (which is either trivial or done only using
rebalancing)
By using different search mechanisms in step 1), we can get a variety
of data structures. Note that thanks to monoidal annotations,
efficient search mechanisms other than comparison-based exists.
For example, using the integer monoid we can keep track of the size
of every subtrees, which can be used to implement efficient
random access.
The positions found in step 1) corresponds readily to splits of
the sequence, as defined in the [SelectionTypes] module. We consider
that the objective of the search is to find a split with particular
properties.
*)
use export SelectionTypes
(** Parameter: selector type. The elements of that type
are intended to describe the class of splits we wish to find. *)
type selector
(** Parameter: interpretation of the selector. *)
predicate selected selector (split (D.t 'a))
(** Parameter: correctness predicate for a selector with respect to a list.
It is intended to mean that we can actually find such a split in
the list using binary search. *)
predicate selection_possible selector (list (D.t 'a))
(** Parameter: a correct selector for the empty list
always select its only possible split. *)
axiom selection_empty : forall s. let nil = (Nil:list (D.t 'a)) in
selection_possible s nil ->
selected s { left = nil ; middle = None ; right = nil }
(** On nodes, binary search works by reducing the problem of selecting of a
split on the whole tree to either:
1) The problem of selecting a split on the left subtree
2) The problem of selecting a split on the right subtree
3) Taking the split induced by the node *)
type part = part_base selector
(** Parameter: [selected_part llis rlis s l d r] effectively compute
the reduction of the selection to one of the three part of a node.
It uses the monoidal summaries to get informations about the
......@@ -564,16 +564,16 @@ module AVL
| Right sr -> selection_possible sr rlis /\
forall e. selected sr e /\ rebuild e = rlis ->
selected s (left_extend llis d e) }
use import ref.Ref
(** Create a reference over a dummy split. All the binary-search-based
routines take a ghost reference to explicitly return the existential
witness corresponding to the found split, this is a shortcut for
creating such a reference. *)
let ghost default_split () : ref (split 'a) =
ref { left = Nil; middle = None; right = Nil }
(** Insertion of an element into the sequence.
[insert r s d t] split the sequence [t] using [s] as [lf ++ o ++ rg],
and rebuild it with [d] in the middle, potentially erasing whatever
......@@ -605,7 +605,7 @@ module AVL
node tl d tr
end
end
(** Remove an element from the sequence.