IndexedTraversals done + some other std library tweaks

This commit is contained in:
Paul Chiusano 2016-08-28 23:51:13 -04:00
parent c0663e2fe8
commit 02227a56e9
4 changed files with 87 additions and 18 deletions

View File

@ -208,8 +208,8 @@ make logger blockStore crypto = do
Right x -> right $ Term.text x
Left x -> left . Term.text . Text.pack $ show x
x -> pure $ Term.ref r `Term.app` x
op _ = fail "Http.getUrl# unpossible"
in (r, Just (I.Primop 1 op), unsafeParseType "Text -> Either Text Text", prefix "Http.getUrl#")
op _ = fail "Http.get-url# unpossible"
in (r, Just (I.Primop 1 op), unsafeParseType "Text -> Either Text Text", prefix "Http.get-url#")
-- Hashing
-- add erase, comparison functions

View File

@ -319,7 +319,7 @@ makeBuiltins logger whnf =
Term.Vector' init -> Term.vector' (Vector.snoc init last)
init -> Term.ref r `Term.app` last `Term.app` init
op _ = fail "Vector.append unpossible"
in (r, Just (I.Primop 2 op), unsafeParseType "forall a . a -> Vector a -> Vector a", prefix "append")
in (r, Just (I.Primop 2 op), unsafeParseType "forall a . a -> Vector a -> Vector a", prefix "Vector.append")
, let r = R.Builtin "Vector.concatenate"
op [a,b] = do
ar <- whnf a

View File

@ -27,6 +27,9 @@ rest p = Pair.fold (x y -> y) p;
4th = rest `then` (rest `then` (rest `then` first));
5th = rest `then` (rest `then` (rest `then` (rest `then` first)));
set-1st : ∀ a a2 b . a2 -> Pair a b -> Pair a2 b;
set-1st new-first p = Pair new-first (rest p);
Order.compare : ∀ a . Order a -> a -> a -> Comparison;
Order.compare o a1 a2 = Order.Key.compare (Order.key o a1) (Order.key o a2);
@ -73,15 +76,39 @@ Vector.all? f vs = Vector.fold-balanced and True (Vector.map f vs);
Vector.sort : ∀ k a . Order k -> (a -> k) -> Vector a -> Vector a;
Vector.sort ok f v = Vector.sort-keyed (f `then` Order.key ok) v;
Remote.transfer : Node -> Remote Unit;
Remote.transfer node = Remote.at node unit;
Remote.map : ∀ a b . (a -> b) -> Remote a -> Remote b;
Remote.map f = Remote.bind (f `then` Remote.pure);
Remote.map2 : ∀ a b c . (a -> b -> c) -> Remote a -> Remote b -> Remote c;
Remote.map2 f a b = do Remote
a := a;
b := b;
pure (f a b);;
;
Remote.map2' : ∀ a b c . (a -> b -> Remote c) -> Remote a -> Remote b -> Remote c;
Remote.map2' f a b = Remote.map2 f a b |> Remote.join;
Remote.join : ∀ a . Remote (Remote a) -> Remote a;
Remote.join = Remote.bind identity;
Remote.replicate : ∀ a . Number -> Remote a -> Remote (Vector a);
Remote.replicate n r = Remote.sequence (Vector.replicate n r);
Remote.unfold : ∀ s a . s -> (s -> Remote (Optional (a, s))) -> Remote (Vector a);
Remote.unfold s f = let rec
go s acc = do Remote
ht := f s;
ht |> Optional.fold
(pure acc)
(ht -> go (2nd ht) (Vector.append (1st ht) acc));;
;
go s Vector.empty;;
;
Remote.transfer : Node -> Remote Unit;
Remote.transfer node = Remote.at node unit;
Remote.race : ∀ a . Duration -> Vector (Remote a) -> Remote a;
Remote.race timeout rs = do Remote
here := Remote.here;
@ -102,13 +129,6 @@ Remote.timeout timeout r =
do Remote Remote.delay timeout; pure None;;
];
Remote.lift2 : ∀ a b c . (a -> b -> c) -> Remote a -> Remote b -> Remote c;
Remote.lift2 f a b = do Remote
a := a;
b := b;
pure (f a b);;
;
Remote.at' : ∀ a . Node -> Remote a -> Remote a;
Remote.at' node r = do Remote Remote.transfer node; r;;;
@ -123,13 +143,13 @@ Remote.start timeout r = do Remote
Remote.traverse : ∀ a b . (a -> Remote b) -> Vector a -> Remote (Vector b);
Remote.traverse f vs =
Vector.fold-balanced (Remote.lift2 Vector.concatenate)
Vector.fold-balanced (Remote.map2 Vector.concatenate)
(Remote.pure Vector.empty)
(Vector.map (f `then` Remote.map Vector.single) vs);
Remote.sequence : ∀ a . Vector (Remote a) -> Remote (Vector a);
Remote.sequence vs =
Vector.fold-balanced (Remote.lift2 Vector.concatenate)
Vector.fold-balanced (Remote.map2 Vector.concatenate)
(Remote.pure Vector.empty)
(Vector.map (Remote.map Vector.single) vs);
@ -159,8 +179,8 @@ Optional.getOr a = Optional.fold a identity;
Optional.somes : ∀ a . Vector (Optional a) -> Vector a;
Optional.somes = Vector.bind (Optional.fold Vector.empty Vector.single);
Optional.lift2 : ∀ a b c . (a -> b -> c) -> Optional a -> Optional b -> Optional c;
Optional.lift2 f a b = do Optional
Optional.map2 : ∀ a b c . (a -> b -> c) -> Optional a -> Optional b -> Optional c;
Optional.map2 f a b = do Optional
a := a;
b := b;
pure (f a b);;

View File

@ -31,6 +31,15 @@ alias IndexedTraversal k v =
, k -> Remote (Optional v)
, k -> Remote (Optional k));
IndexedTraversal.1st-key : ∀ k v . IndexedTraversal k v -> Remote (Optional k);
IndexedTraversal.1st-key t = 1st t;
IndexedTraversal.lookup : ∀ k v . k -> IndexedTraversal k v -> Remote (Optional v);
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
add-hash = Optional.map (k -> (k, hash# k));
@ -44,8 +53,48 @@ IndexedTraversal.empty : ∀ k v . IndexedTraversal k v;
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 k v;
IndexedTraversal.intersect o t1 t2 = let rec
align-key k1 k2 = Optional.getOr (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))
(IndexedTraversal.increment k1 t2 |> Remote.bind (k2 -> align-key (Some k1) k2))
)
k1 k2
;
1st-key = Remote.map2' align-key (1st t1) (1st t2);
lookup k = 2nd t1 k |> Remote.bind (Optional.fold (Remote.pure None) (a -> 2nd t2 k));
increment k = Remote.map2' align-key (3rd t1 k) (3rd t2 k);
(1st-key, lookup, increment);;
;
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 .
Remote (Optional k) -> IndexedTraversal k v -> Remote (Optional (k, v));
IndexedTraversal.entry-at k t = do Remote
k := k;
v := Optional.fold (pure None) (2nd t) k;
pure (Optional.map2 (k v -> (k,v)) k v);;
;
IndexedTraversal.take : ∀ k v . Number -> IndexedTraversal k v -> Remote (Vector (k,v));
IndexedTraversal.take n t =
Remote.unfold (t, n) (tn -> let
t = 1st tn;
n = 2nd tn;
step e = (e, (set-1st (IndexedTraversal.increment (1st e) t) t, n - 1));
if (n <=_Number 0) (Remote.pure None)
(IndexedTraversal.1st-entry t |> Remote.map (Optional.map step));;
);
Http.get-url : Text -> Remote (Either Text Text);
Http.get-url url = Remote.map Http.getUrl# (Remote.pure url);
Http.get-url url = Remote.map Http.get-url# (Remote.pure url);
hash! : ∀ a . a -> Remote (Hash a);
hash! a = Remote.map hash# (Remote.pure a);