generated from koka-community/template
-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
9f74376
commit 03c35d7
Showing
7 changed files
with
213 additions
and
29 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
effect efind<b> | ||
final ctl not-found(): a | ||
final ctl found(b: b): b | ||
|
||
effect err-empty | ||
final ctl err-empty(): a | ||
|
||
type find<v> | ||
Found(v: v) | ||
NotFound |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
import errors | ||
|
||
struct finite-map<m,k,v> | ||
s-empty: m<k,v> | ||
s-insert: (m<k,v>, k, v) -> m<k,v> | ||
s-lookup: (m<k,v>, k) -> efind<k> v | ||
|
||
pub type tree<k,v> | ||
E | ||
T(l: tree<k,v>, key: k, value: v, r: tree<k,v>) | ||
|
||
struct map<k,v> | ||
internal: tree<k,v> | ||
|
||
fun map/empty(): map<k,v> | ||
Map(E) | ||
|
||
fun tree/lookup(s: tree<k,v>, x: k, ?(<): (k,k) -> bool): efind<v> v | ||
match s | ||
E -> not-found() | ||
T(l, y, v, r) -> if x < y then lookup(l, x) else if y < x then lookup(r, x) else v | ||
|
||
fun map/lookup(m: map<k,v>, x: k, ?(<): (k,k) -> bool): exn v | ||
with handler | ||
final ctl found(a) a | ||
final ctl not-found() throw("not found") | ||
tree/lookup(m.internal, x) | ||
|
||
fun tree/bind(s: tree<k,v>, x: k, y: v, ?(<): (k,k) -> bool): tree<k,v> | ||
match s | ||
E -> T(E, x, y, E) | ||
T(l, z, w, r) -> if x < z then T(bind(l, x, y), z, w, r) else if z < x then T(l, z, w, bind(r, x, y)) else T(l, x, y, r) | ||
|
||
fun map/bind(m: map<k,v>, x: k, y: v, ?(<): (k,k) -> bool): map<k,v> | ||
Map(tree/bind(m.internal, x, y)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,81 @@ | ||
import errors | ||
import std/core/undiv | ||
|
||
struct heap<m,k> | ||
h-empty: m<k> | ||
h-is-empty: m<k> -> bool | ||
h-insert: (m<k>, k) -> m<k> | ||
h-merge: (m<k>, m<k>) -> m<k> | ||
h-find-min: m<k> -> err-empty k | ||
h-delete-min: m<k> -> err-empty m<k> | ||
|
||
// Leftist heap | ||
// Property: Rank of any left child is at least as large as the range of it's right sibling | ||
pub type tree<k> | ||
E | ||
T(rank: int, l: tree<k>, value: k, r: tree<k>) | ||
|
||
struct leftist-heap<k> | ||
internal: tree<k> | ||
|
||
fun rank(s: tree<k>): int | ||
match s | ||
E -> 0 | ||
T(r,_,_,_) -> r | ||
|
||
fun makeT(a: tree<k>, x: k, b: tree<k>): tree<k> | ||
if rank(a) >= rank(b) then T(rank(b) + 1, a, x, b) else T(rank(a) + 1, b, x, a) | ||
|
||
fun empty() | ||
Leftist-heap(E) | ||
|
||
fun is-empty(this: leftist-heap<k>) | ||
this.internal.is-E | ||
|
||
fun tree/merge(l: tree<k>, r: tree<k>, ?(<=): (k, k) -> bool): tree<k> | ||
match (l, r) | ||
(E, _) -> r | ||
(_, E) -> l | ||
(T(_,a,x,b), T(_,c,y,d)) -> | ||
if x <= y then makeT(a, x, merge(b.pretend-decreasing, r)) | ||
else makeT(c, y, merge(l.pretend-decreasing, d)) | ||
|
||
fun heap/merge(l: leftist-heap<k>, r: leftist-heap<k>, ?(<=): (k, k) -> bool): leftist-heap<k> | ||
Leftist-heap(tree/merge(l.internal, r.internal)) | ||
|
||
fun insert(x: k, h: leftist-heap<k>, ?(<=): (k, k) -> bool): leftist-heap<k> | ||
Leftist-heap(merge(T(1, E, x, E), h.internal)) | ||
|
||
fun err/find-min(h: leftist-heap<k>): err-empty k | ||
match h.internal | ||
E -> err-empty() | ||
T(_, _, x, _) -> x | ||
|
||
fun maybe/min(h: leftist-heap<k>): maybe<k> | ||
match h.internal | ||
E -> Nothing | ||
T(_, _, x, _) -> Just(x) | ||
|
||
fun err/delete-min(h: leftist-heap<k>, ?(<=): (k, k) -> bool): err-empty leftist-heap<k> | ||
match h.internal | ||
E -> err-empty() | ||
T(_, a, _, b) -> Leftist-heap(merge(a, b)) | ||
|
||
fun maybe/delete(h: leftist-heap<k>, ?(<=): (k, k) -> bool): maybe<leftist-heap<k>> | ||
match h.internal | ||
E -> Nothing | ||
T(_, a, _, b) -> Just(Leftist-heap(merge(a, b))) | ||
|
||
|
||
// Exercise 3.1: Prove that the right spine of a leftist heap of size n contains at most floor(log2(n + 1)) elements. | ||
// Exercise 3.2: Define insert directly rather than via a call to merge | ||
// Exercise 3.3: Implement a function fromList of type list<t> -> leftist-heap<t> that converts an unordered list by transforming into singleton heaps and then mergine | ||
// Instead of using one pass using fold, merge the heaps in ceil(log2(n)) passes where each pass merges adjacent pairs of heaps. | ||
// Show that it only takes O(n) time total | ||
// Exercise 3.4: Cho and Sahni: Weight-biased leftist heaps (change the leftist property to the size of any left child is at least as large as the size of its right sibling) | ||
// a) Prove that the right spine contains at most floor(log2(n + 1)) elements | ||
// b) Modify leftist heaps to implement weight biased leftist heaps | ||
// c) Currently merge operates in two passes - top down to merge, and bottom up to makeT. Modify merge to operate in one top-down pass. | ||
// d) What advantages would the top-down version of merge have in a lazy environment? In a concurrent environment? | ||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,30 @@ | ||
import errors | ||
import std/core/undiv | ||
|
||
struct heap<m,k> | ||
h-empty: m<k> | ||
h-is-empty: m<k> -> bool | ||
h-insert: (m<k>, k) -> m<k> | ||
h-merge: (m<k>, m<k>) -> m<k> | ||
h-find-min: m<k> -> err-empty k | ||
h-delete-min: m<k> -> err-empty m<k> | ||
|
||
// Binomial heap (Binomial queues Vui 78, Bro 78) | ||
// Property: rank 0 node is a singleton, rank r + 1 node is formed by linking two binomial trees of rank r | ||
// Property: rank r node has 2^r children | ||
// Property: Each list of children is in decreaesing order of rank, and elements are stored in heap order | ||
pub type tree<k> | ||
T(rank: int, value: k, ts: list<tree<k>>) | ||
|
||
// A heap is a collection of heap-ordered binomial trees in which no two trees have the same rank. | ||
struct binomial-heap<k> | ||
trees: list<tree<k>> | ||
|
||
fun link(t1: tree<k>, t2: tree<k>, ?(<=) : (k,k) -> bool): tree<k> | ||
match (t1, t2) | ||
(T(r, x1, ts1), T(_, x2, ts2)) -> | ||
if x1 <= x2 then T(r + 1, x1, Cons(t2, ts1)) | ||
else T(r + 1, x2, Cons(t1, ts2)) | ||
|
||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,49 @@ | ||
struct unbalanced-set<s,a> | ||
s-empty: s<a> | ||
s-member: (s<a>, a) -> bool | ||
s-insert: (s<a>, a) -> s<a> | ||
|
||
pub type tree<t> | ||
E | ||
T(t: tree<t>, value: t, t: tree<t>) | ||
|
||
struct set<t> | ||
internal: tree<t> | ||
|
||
pub fun set/member(s: set<t>, x: t, ?(<): (t,t) -> bool): bool | ||
s.internal.member(x) | ||
|
||
pub fun tree/member(s: tree<t>, x: t, ?(<): (t,t) -> bool): bool | ||
match s | ||
E -> False | ||
T(l, y, r) -> if x < y then member(l, x) else if y < x then member(r, x) else True | ||
|
||
pub fun set/insert(s: set<t>, x: t, ?(<): (t,t) -> bool): set<t> | ||
Set(s.internal.insert(x)) | ||
|
||
pub fun tree/insert(s: tree<t>, x: t, ?(<): (t,t) -> bool): tree<t> | ||
match s | ||
E -> T(E, x, E) | ||
T(l, y, r) -> if x < y then T(l.insert(x), y, r) else if y < x then T(l, y, r.insert(x)) else T(l, x, r) | ||
|
||
// Exercise 2.2: Andersson[91] | ||
// Rewrite member to take more than d + 1 comparisons by keeping track of a candidate element | ||
// that might be equal to the query element (the last element for which < returned false or <= returned true) | ||
// and checking for equality only when you hit the bottom of the tree | ||
// pub fun tree/insertd(s: tree<t>, x: t, ?(<): (t,t) -> bool): maybe<tree<t>> | ||
|
||
// Exercise 2.3: | ||
// Inserting an existing element copies everything even if the element is not changed. Rewrite using exceptions. | ||
// Note: Koka should be good at this (by returning unchanged the input, or jumping out of a tail recursive optimized call). | ||
// How would this look with ctx<>? | ||
|
||
// Exercise 2.4: | ||
// Combine the previous two exercises | ||
|
||
// Exercise 2.5: Use sharing | ||
// a) complete(x:elem, d:int) create a complete tree of depth `d` with `x` in every node. With sharing this should run in `O(d)` time. | ||
// b) Extend the function to create balanced trees of arbitrary size. This function should run in O(log n) time. | ||
// For a node, the two subtrees should differ in size by at most one. | ||
// (Hint: use a helper function create2 that, given a size m, creates a pair of trees, one of size m, and one of size m + 1) | ||
|
||
// Exercise 2.6: Adapt to suport finite maps rather than sets. |