fix compile errors in dindex.u and extra.u

This commit is contained in:
Paul Chiusano 2016-09-13 11:54:59 -04:00
parent 2f70ae7407
commit 0dc9e37a47
2 changed files with 29 additions and 29 deletions

View File

@ -11,13 +11,13 @@ alias DIndex k v = Index Node (Index k v);
DIndex.empty : ∀ k v . Remote (DIndex k v);
DIndex.empty = Index.empty;
-- Pick the nodes responsible for a key, using HRW hashing
-- Pick the nodes responsible for a key, using HRW hashing
DIndex.nodesForKey : ∀ k v . k -> DIndex k v -> Remote (Vector Node);
DIndex.nodesForKey k ind = do Remote
nodes := Index.keys ind;
hashes := Remote.traverse (node -> hash! (node, k)) nodes;
hashes := Remote.traverse (node -> hash! (node, k)) nodes;
(nodes `Vector.zip` hashes)
|> Vector.sort Hash.Order 2nd
|> Vector.sort Hash.Order 2nd
|> Vector.take DIndex.Replication-Factor
|> Vector.map 1st
|> pure;;
@ -40,7 +40,7 @@ DIndex.lookup k ind = do Remote
pure (Vector.at 0 rs |> Optional.bind identity);;
;
DIndex.insert : ∀ k v . k -> v -> DIndex k v -> Remote Unit;
DIndex.insert : ∀ k v . k -> v -> DIndex k v -> Remote Unit;
DIndex.insert k v ind = do Remote
nodes := DIndex.nodesForKey k ind;
localInsert = node -> (do Remote
@ -53,7 +53,7 @@ DIndex.insert k v ind = do Remote
;
DIndex.join : ∀ k v . DIndex k v -> Remote Unit;
DIndex.join ind = do Remote
DIndex.join ind = do Remote
here := Remote.here;
localInd := Index.empty;
Index.insert here localInd ind;;
@ -61,12 +61,12 @@ DIndex.join ind = do Remote
DIndex.indicesForKey : ∀ k v . k -> DIndex k v -> Remote (Vector (Index k v));
DIndex.indicesForKey k ind = do Remote
nodes := DIndex.nodesForKey k ind;
nodes := DIndex.nodesForKey k ind;
indices := Remote.traverse (node -> Index.lookup node ind) nodes;
pure (Optional.somes indices);;
;
DIndex.rebalance : ∀ k v . k -> DIndex k v -> Remote Unit;
DIndex.rebalance : ∀ k v . k -> DIndex k v -> Remote Unit;
DIndex.rebalance k ind = do Remote
indices := DIndex.indicesForKey k ind;
t = DIndex.Timeout;
@ -74,15 +74,15 @@ DIndex.rebalance k ind = do Remote
resultsHashes := Remote.traverse hash! results;
uh := hash! None;
hd = uh `Optional.get-or` Vector.at 0 resultsHashes;
eq = h1 h2 -> Hash.equal (Hash.erase h1) (Hash.erase h2);
if (Vector.all? (eq hd) resultsHashes)
-- all results matched, we're good
eq = h1 h2 -> Hash.erase h1 ==_Hash Hash.erase h2;
if (Vector.all? (eq hd) resultsHashes)
-- all results matched, we're good
(pure Unit)
-- not all results matched, reinsert
(do Remote
-- not all results matched, reinsert
(do Remote
ov := DIndex.lookup k ind;
Optional.fold (pure Unit)
(v -> DIndex.insert k v ind)
Optional.fold (pure Unit)
(v -> DIndex.insert k v ind)
ov;;)
;;
;
@ -92,7 +92,7 @@ DIndex.leave node ind = do Remote
Index.delete node ind;
Optional.fold
(pure Unit)
(local-ind -> do Remote
(local-ind -> do Remote
keys := Index.keys local-ind;
Remote.fork <| Remote.traverse (k -> DIndex.rebalance k ind) keys;;)
local-ind;;

View File

@ -9,16 +9,16 @@ Index.1st-key : ∀ k v . Index k v -> Remote (Optional k);
Index.1st-key = Index.from-unsafe Index.1st-key#;
Index.increment : ∀ k v . k -> Index k v -> Remote (Optional k);
Index.increment k = Index.from-unsafe (Index.increment# k);
Index.increment k = Index.from-unsafe (Index.increment# k);
Index.lookup : ∀ k v . k -> Index k v -> Remote (Optional v);
Index.lookup k = Index.from-unsafe (Index.lookup# k);
Index.lookup-or : v -> k -> Index k v -> Remote v;
Index.lookup-or : ∀ k v . v -> k -> Index k v -> Remote v;
Index.lookup-or v k ind =
Remote.map (Optional.get-or v) (Index.lookup k ind);
Index.delete : ∀ k v . k -> Index k v -> Remote Unit;
Index.delete : ∀ k v . k -> Index k v -> Remote Unit;
Index.delete k = Index.from-unsafe (Index.delete# k);
Index.insert : ∀ k v . k -> v -> Index k v -> Remote Unit;
@ -30,7 +30,7 @@ Index.from-unsafe f ind = let
Remote.map f (Remote.at (1st p) (2nd p));;
;
alias IndexedTraversal k v =
alias IndexedTraversal k v =
( Remote (Optional k)
, k -> Remote (Optional v)
, k -> Remote (Optional k));
@ -44,25 +44,25 @@ IndexedTraversal.lookup k t = 2nd t k;
IndexedTraversal.increment : ∀ k v . k -> IndexedTraversal k v -> Remote (Optional k);
IndexedTraversal.increment k t = 3rd t k;
Index.traversal : ∀ k v . Index k v -> IndexedTraversal (k, Hash k) v;
Index.traversal ind = let
Index.traversal : ∀ k v . Index k v -> IndexedTraversal (k, Hash k) v;
Index.traversal ind = let
add-hash = Optional.map (k -> (k, hash# k));
( Index.1st-key ind |> Remote.map add-hash
, k -> Index.lookup (1st k) ind
, k -> Index.increment (1st k) ind |> Remote.map add-hash
, k -> Index.increment (1st k) ind |> Remote.map add-hash
);;
;
IndexedTraversal.empty : ∀ k v . IndexedTraversal k v;
IndexedTraversal.empty =
IndexedTraversal.empty =
(Remote.pure None, const (Remote.pure None), const (Remote.pure None));
IndexedTraversal.intersect : ∀ k v . Order k
-> IndexedTraversal k v
-> IndexedTraversal k v
IndexedTraversal.intersect : ∀ k v . Order k
-> IndexedTraversal k v
-> IndexedTraversal k v
-> IndexedTraversal k v;
IndexedTraversal.intersect o t1 t2 = let rec
align-key k1 k2 = Optional.get-or (Remote.pure None) <| Optional.map2
IndexedTraversal.intersect o t1 t2 = let rec
align-key k1 k2 = Optional.get-or (Remote.pure None) <| Optional.map2
(k1 k2 -> Order.compare o k1 k2 |> Comparison.fold
(IndexedTraversal.increment k2 t1 |> Remote.bind (k1 -> align-key k1 (Some k2)))
(Remote.pure (Some k1))
@ -79,7 +79,7 @@ IndexedTraversal.intersect o t1 t2 = let rec
IndexedTraversal.1st-entry : ∀ k v . IndexedTraversal k v -> Remote (Optional (k, v));
IndexedTraversal.1st-entry t = IndexedTraversal.entry-at (1st t) t;
IndexedTraversal.entry-at : ∀ k v .
IndexedTraversal.entry-at : ∀ k v .
Remote (Optional k) -> IndexedTraversal k v -> Remote (Optional (k, v));
IndexedTraversal.entry-at k t = do Remote
k := k;