mirror of
https://github.com/unisonweb/unison.git
synced 2024-10-05 14:17:33 +03:00
fix stray case .. of
instances and opportunities for cases
in unison-src
This commit is contained in:
parent
652ae4ac76
commit
5a841f30f5
@ -26,29 +26,29 @@ use Tuple Cons
|
||||
|
||||
namespace Tuple where
|
||||
at1 : Tuple a b -> a
|
||||
at1 p = case p of Cons a _ -> a
|
||||
at1 = cases Cons a _ -> a
|
||||
|
||||
at2 : Tuple a (Tuple b c) -> b
|
||||
at2 p = case p of Cons _ (Cons b _) -> b
|
||||
at2 = cases Cons _ (Cons b _) -> b
|
||||
|
||||
at3 : Tuple a (Tuple b (Tuple c d)) -> c
|
||||
at3 p = case p of Cons _ (Cons _ (Cons c _)) -> c
|
||||
at3 = cases Cons _ (Cons _ (Cons c _)) -> c
|
||||
|
||||
at4 : Tuple a (Tuple b (Tuple c (Tuple d e))) -> d
|
||||
at4 p = case p of Cons _ (Cons _ (Cons _ (Cons d _))) -> d
|
||||
at4 = cases Cons _ (Cons _ (Cons _ (Cons d _))) -> d
|
||||
|
||||
namespace List where
|
||||
|
||||
map : (a -> b) -> [a] -> [b]
|
||||
map f a =
|
||||
go i as acc = case List.at i as of
|
||||
go i as acc = match List.at i as with
|
||||
None -> acc
|
||||
Some a -> go (i + 1) as (acc `snoc` f a)
|
||||
go 0 a []
|
||||
|
||||
zip : [a] -> [b] -> [(a,b)]
|
||||
zip as bs =
|
||||
go acc i = case (at i as, at i bs) of
|
||||
go acc i = match (at i as, at i bs) with
|
||||
(None,_) -> acc
|
||||
(_,None) -> acc
|
||||
(Some a, Some b) -> go (acc `snoc` (a,b)) (i + 1)
|
||||
@ -65,13 +65,13 @@ namespace List where
|
||||
take (stopExclusive `Nat.drop` start) (drop start s)
|
||||
|
||||
unsafeAt : Nat -> [a] -> a
|
||||
unsafeAt n as = case at n as of
|
||||
unsafeAt n as = match at n as with
|
||||
Some a -> a
|
||||
None -> Debug.watch "oh noes" (unsafeAt n as) -- Debug.crash "oh noes!"
|
||||
|
||||
foldl : (b -> a -> b) -> b -> [a] -> b
|
||||
foldl f b as =
|
||||
go b i = case List.at i as of
|
||||
go b i = match List.at i as with
|
||||
None -> b
|
||||
Some a -> go (f b a) (i + 1)
|
||||
go b 0
|
||||
@ -80,7 +80,7 @@ namespace List where
|
||||
foldb f op z as =
|
||||
if List.size as == 0 then z
|
||||
else if List.size as == 1 then f (unsafeAt 0 as)
|
||||
else case halve as of (left, right) ->
|
||||
else match halve as with (left, right) ->
|
||||
foldb f op z left `op` foldb f op z right
|
||||
|
||||
reverse : [a] -> [a]
|
||||
@ -91,7 +91,7 @@ namespace List where
|
||||
|
||||
sortBy : (a -> b) -> [a] -> [a]
|
||||
sortBy f as =
|
||||
tweak p = case p of (p1,p2) -> (f p1, p2, p1)
|
||||
tweak p = match p with (p1,p2) -> (f p1, p2, p1)
|
||||
Heap.sort (map tweak (indexed as)) |> map Tuple.at3
|
||||
|
||||
halve : [a] -> ([a], [a])
|
||||
@ -101,20 +101,20 @@ namespace List where
|
||||
|
||||
unfold : s -> (s -> Optional (a, s)) -> [a]
|
||||
unfold s0 f =
|
||||
go f s acc = case f s of
|
||||
go f s acc = match f s with
|
||||
None -> acc
|
||||
Some (a, s) -> go f s (acc `snoc` a)
|
||||
go f s0 []
|
||||
|
||||
uncons : [a] -> Optional (a, [a])
|
||||
uncons as = case at 0 as of
|
||||
uncons as = match at 0 as with
|
||||
None -> None
|
||||
Some a -> Some (a, drop 1 as)
|
||||
|
||||
unsnoc : [a] -> Optional ([a], a)
|
||||
unsnoc as =
|
||||
i = size (drop 1 as)
|
||||
case at i as of
|
||||
match at i as with
|
||||
None -> None
|
||||
Some a -> Some (take i as, a)
|
||||
|
||||
@ -131,7 +131,7 @@ namespace List where
|
||||
|
||||
distinct : [a] -> [a]
|
||||
distinct as =
|
||||
go i seen acc = case List.at i as of
|
||||
go i seen acc = match List.at i as with
|
||||
None -> acc
|
||||
Some a -> if Set.contains a seen then go (i + 1) seen acc
|
||||
else go (i + 1) (Set.insert a seen) (acc `snoc` a)
|
||||
@ -143,11 +143,11 @@ namespace List where
|
||||
diagonal =
|
||||
let
|
||||
x = 23
|
||||
stripe aas = case aas of
|
||||
stripe = cases
|
||||
[] -> []
|
||||
[] +: xxs -> stripe xxs
|
||||
(x +: xs) +: xxs -> cons [x] (zipCons xs (stripe xxs))
|
||||
zipCons xs ys = case (xs, ys) of
|
||||
zipCons xs ys = match (xs, ys) with
|
||||
([], ys) -> ys
|
||||
(xs, []) -> map (x -> [x]) xs
|
||||
(x +: xs, y +: ys) -> cons (cons x y) (zipCons xs ys)
|
||||
@ -183,7 +183,7 @@ namespace Search where
|
||||
if bot >= top then top
|
||||
else
|
||||
mid = (bot + top) / 2
|
||||
case hit mid of
|
||||
match hit mid with
|
||||
+0 -> mid
|
||||
-1 -> lub hit bot mid
|
||||
+1 -> lub hit (mid + 1) top
|
||||
@ -193,7 +193,7 @@ namespace Search where
|
||||
if bot >= top then None
|
||||
else
|
||||
mid = (bot + top) / 2
|
||||
case hit mid of
|
||||
match hit mid with
|
||||
+0 -> Some mid
|
||||
-1 -> exact hit bot mid
|
||||
+1 -> exact hit (mid + 1) top
|
||||
@ -222,7 +222,7 @@ namespace Map where
|
||||
|
||||
fromList : [(k,v)] -> Map k v
|
||||
fromList kvs =
|
||||
go acc i = case List.at i kvs of
|
||||
go acc i = match List.at i kvs with
|
||||
None -> acc
|
||||
Some (k,v) -> go (insert k v acc) (i + 1)
|
||||
go empty 0
|
||||
@ -234,21 +234,21 @@ namespace Map where
|
||||
size s = List.size (keys s)
|
||||
|
||||
lookup : k -> Map k v -> Optional v
|
||||
lookup k m = case m of
|
||||
Map ks vs -> case Search.indexOf k ks of
|
||||
lookup k = cases
|
||||
Map ks vs -> match Search.indexOf k ks with
|
||||
None -> None
|
||||
Some i -> at i vs
|
||||
|
||||
contains : k -> Map k v -> Boolean
|
||||
contains k m = case m of Map ks _ -> case Search.indexOf k ks of
|
||||
contains k cases Map ks _ -> match Search.indexOf k ks with
|
||||
None -> false
|
||||
_ -> true
|
||||
|
||||
insert : k -> v -> Map k v -> Map k v
|
||||
insert k v m = case m of Map ks vs ->
|
||||
insert k v = cases Map ks vs ->
|
||||
use Search lubIndexOf
|
||||
i = lubIndexOf k ks
|
||||
case at i ks of
|
||||
match at i ks with
|
||||
Some k' ->
|
||||
if k == k' then Map ks (List.replace i v vs)
|
||||
else Map (List.insert i k ks) (List.insert i v vs)
|
||||
@ -264,8 +264,8 @@ namespace Map where
|
||||
union = unionWith (_ v -> v)
|
||||
|
||||
unionWith : (v -> v -> v) -> Map k v -> Map k v -> Map k v
|
||||
unionWith f m1 m2 = case (m1, m2) of (Map k1 v1, Map k2 v2) ->
|
||||
go i j ko vo = case (at i k1, at j k2) of
|
||||
unionWith f m1 m2 = match (m1, m2) with (Map k1 v1, Map k2 v2) ->
|
||||
go i j ko vo = match (at i k1, at j k2) with
|
||||
(None, _) -> Map (ko ++ drop j k2) (vo ++ drop j v2)
|
||||
(_, None) -> Map (ko ++ drop i k1) (vo ++ drop i v1)
|
||||
(Some kx, Some ky) ->
|
||||
@ -287,8 +287,8 @@ namespace Map where
|
||||
intersect = intersectWith (_ v -> v)
|
||||
|
||||
intersectWith : (v -> v -> v2) -> Map k v -> Map k v -> Map k v2
|
||||
intersectWith f m1 m2 = case (m1, m2) of (Map k1 v1, Map k2 v2) ->
|
||||
go i j ko vo = case (at i k1, at j k2) of
|
||||
intersectWith f m1 m2 = match (m1, m2) with (Map k1 v1, Map k2 v2) ->
|
||||
go i j ko vo = match (at i k1, at j k2) with
|
||||
(None, _) -> Map ko vo
|
||||
(_, None) -> Map ko vo
|
||||
(Some kx, Some ky) ->
|
||||
@ -305,15 +305,15 @@ namespace Map where
|
||||
go 0 0 [] []
|
||||
|
||||
keys : Map k v -> [k]
|
||||
keys m = case m of Map ks _ -> ks
|
||||
keys = cases Map ks _ -> ks
|
||||
|
||||
values : Map k v -> [v]
|
||||
values m = case m of Map _ vs -> vs
|
||||
values = cases Map _ vs -> vs
|
||||
|
||||
namespace Multimap where
|
||||
|
||||
insert : k -> v -> Map k [v] -> Map k [v]
|
||||
insert k v m = case Map.lookup k m of
|
||||
insert k v m = match Map.lookup k m with
|
||||
None -> Map.insert k [v] m
|
||||
Some vs -> Map.insert k (vs `snoc` v) m
|
||||
|
||||
@ -329,22 +329,22 @@ namespace Set where
|
||||
empty = Set Map.empty
|
||||
|
||||
underlying : Set k -> Map k ()
|
||||
underlying s = case s of Set s -> s
|
||||
underlying = cases Set s -> s
|
||||
|
||||
toMap : (k -> v) -> Set k -> Map k v
|
||||
toMap f s = case s of Set (Map ks vs) -> Map ks (List.map f ks)
|
||||
toMap f = cases Set (Map ks vs) -> Map ks (List.map f ks)
|
||||
|
||||
fromList : [k] -> Set k
|
||||
fromList ks = Set (Map.fromList (List.map (k -> (k,())) ks))
|
||||
|
||||
toList : Set k -> [k]
|
||||
toList s = case s of Set (Map ks _) -> ks
|
||||
toList = cases Set (Map ks _) -> ks
|
||||
|
||||
contains : k -> Set k -> Boolean
|
||||
contains k s = case s of Set m -> Map.contains k m
|
||||
contains k = cases Set m -> Map.contains k m
|
||||
|
||||
insert : k -> Set k -> Set k
|
||||
insert k s = case s of Set s -> Set (Map.insert k () s)
|
||||
insert k = cases Set s -> Set (Map.insert k () s)
|
||||
|
||||
union : Set k -> Set k -> Set k
|
||||
union s1 s2 = Set (Map.union (underlying s1) (underlying s2))
|
||||
@ -364,10 +364,10 @@ namespace Heap where
|
||||
singleton k v = Heap 1 k v []
|
||||
|
||||
size : Heap k v -> Nat
|
||||
size h = case h of Heap n _ _ _ -> n
|
||||
size = cases Heap n _ _ _ -> n
|
||||
|
||||
union : Heap k v -> Heap k v -> Heap k v
|
||||
union h1 h2 = case (h1, h2) of
|
||||
union h1 h2 = match (h1, h2) with
|
||||
(Heap n k1 v1 hs1, Heap m k2 v2 hs2) ->
|
||||
if k1 >= k2 then Heap (n + m) k1 v1 (cons h2 hs1)
|
||||
else Heap (n + m) k2 v2 (cons h1 hs2)
|
||||
@ -379,27 +379,27 @@ namespace Heap where
|
||||
if size subs == 0 then h
|
||||
else if size subs == 1 then h `union` unsafeAt 0 subs
|
||||
else union h (unsafeAt 0 subs) `union` go (unsafeAt 1 subs) (drop 2 subs)
|
||||
case List.uncons (children h) of
|
||||
match List.uncons (children h) with
|
||||
None -> None
|
||||
Some (s0, subs) -> Some (go s0 subs)
|
||||
|
||||
children : Heap k v -> [Heap k v]
|
||||
children h = case h of Heap _ _ _ cs -> cs
|
||||
children = cases Heap _ _ _ cs -> cs
|
||||
|
||||
max : Heap k v -> (k, v)
|
||||
max h = case h of Heap _ k v _ -> (k, v)
|
||||
max = cases Heap _ k v _ -> (k, v)
|
||||
|
||||
maxKey : Heap k v -> k
|
||||
maxKey h = case h of Heap _ k _ _ -> k
|
||||
maxKey = cases Heap _ k _ _ -> k
|
||||
|
||||
fromList : [(k,v)] -> Optional (Heap k v)
|
||||
fromList kvs =
|
||||
op a b = case a of
|
||||
op a b = match a with
|
||||
None -> b
|
||||
Some a -> case b of
|
||||
Some a -> match b with
|
||||
None -> Some a
|
||||
Some b -> Some (union a b)
|
||||
single kv = case kv of
|
||||
single = cases
|
||||
(k, v) -> Some (singleton k v)
|
||||
List.foldb single op None kvs
|
||||
|
||||
@ -408,7 +408,7 @@ namespace Heap where
|
||||
|
||||
sortDescending : [a] -> [a]
|
||||
sortDescending as =
|
||||
step o = case o of
|
||||
step = cases
|
||||
None -> None
|
||||
Some h -> Some (max h, pop h)
|
||||
List.unfold (fromKeys as) step |> List.map Tuple.at1
|
||||
@ -421,22 +421,22 @@ namespace Heap where
|
||||
namespace Optional where
|
||||
|
||||
map : (a -> b) -> Optional a -> Optional b
|
||||
map f o = case o of
|
||||
map f = cases
|
||||
None -> None
|
||||
Some a -> Some (f a)
|
||||
|
||||
orDefault : a -> Optional a -> a
|
||||
orDefault a o = case o of
|
||||
orDefault a = cases
|
||||
None -> a
|
||||
Some a -> a
|
||||
|
||||
orElse : Optional a -> Optional a -> Optional a
|
||||
orElse a b = case a of
|
||||
orElse a b = match a with
|
||||
None -> b
|
||||
Some _ -> a
|
||||
|
||||
flatMap : (a -> Optional b) -> Optional a -> Optional b
|
||||
flatMap f o = case o of
|
||||
flatMap f = cases
|
||||
None -> None
|
||||
Some a -> f a
|
||||
|
||||
|
@ -4,7 +4,7 @@ type Functor f = Functor (forall a b. (a ->{} b) -> f a ->{} f b)
|
||||
|
||||
use Functor Functor
|
||||
fmap : Functor f -> (a -> b) -> f a -> f b
|
||||
fmap fn f = case fn of
|
||||
fmap fn f = match fn with
|
||||
Functor map -> map f
|
||||
|
||||
use Cofree Cofree
|
||||
@ -12,10 +12,9 @@ use Cofree Cofree
|
||||
namespace Cofree where
|
||||
|
||||
extract : Cofree f a -> a
|
||||
extract c = case c of
|
||||
extract = cases
|
||||
Cofree a _ -> a
|
||||
|
||||
duplicate : Functor f -> Cofree f a -> Cofree f (Cofree f a)
|
||||
duplicate f c = case c of
|
||||
duplicate f c = match c with
|
||||
Cofree a p -> Cofree c (fmap f (duplicate f) p)
|
||||
|
||||
|
@ -9,7 +9,7 @@ use List flatMap
|
||||
|
||||
type Test.Success = Passed Nat | Proved
|
||||
|
||||
type Test.Status = Failed
|
||||
type Test.Status = Failed
|
||||
| Expected Test.Success
|
||||
| Unexpected Test.Success
|
||||
| Pending
|
||||
@ -22,29 +22,29 @@ type Test.Test = Test (Test.Scope -> Test.Report)
|
||||
unique type Test.Scope = Scope [Text]
|
||||
|
||||
foldSuccess : (Nat -> r) -> r -> Success -> r
|
||||
foldSuccess passed proved s = case s of
|
||||
foldSuccess passed proved = cases
|
||||
Passed n -> passed n
|
||||
Proved -> proved
|
||||
|
||||
foldStatus : r -> (Success -> r) -> (Success -> r) -> r -> Status -> r
|
||||
foldStatus failed expected unexpected pending status = case status of
|
||||
foldStatus failed expected unexpected pending = cases
|
||||
Failed -> failed
|
||||
Expected s -> expected s
|
||||
Unexpected s -> unexpected s
|
||||
Pending -> pending
|
||||
|
||||
|
||||
foldReport : (Trie Text Test.Status -> r) -> Report -> r
|
||||
foldReport k r = case r of Report t -> k t
|
||||
|
||||
foldScope : ([Text] -> r) -> Scope -> r
|
||||
foldScope k s = case s of Scope ss -> k ss
|
||||
foldScope k = cases Scope ss -> k ss
|
||||
|
||||
Scope.cons : Text -> Scope -> Scope
|
||||
Scope.cons n = foldScope (Scope . List.cons n)
|
||||
|
||||
-- Basic building blocks of tests
|
||||
Test.finished : Status -> Test
|
||||
Test.finished st =
|
||||
Test.finished st =
|
||||
Test (Report . foldScope (sc -> Trie.singleton sc st))
|
||||
|
||||
Test.failed : Test
|
||||
@ -65,20 +65,20 @@ Test.provedUnexpectedly = finished <| Unexpected Proved
|
||||
-- Basic test combinators
|
||||
|
||||
Test.modifyStatus : (Status -> Status) -> Test -> Test
|
||||
Test.modifyStatus f t =
|
||||
case t of Test k -> Test (foldReport (Report . map f) . k)
|
||||
Test.modifyStatus f =
|
||||
cases Test k -> Test (foldReport (Report . map f) . k)
|
||||
|
||||
Test.label : Text -> Test -> Test
|
||||
Test.label n t = case t of
|
||||
Test.label n = cases
|
||||
Test.Test.Test k -> Test (scope -> k <| Scope.cons n scope)
|
||||
|
||||
use Test.Report combine
|
||||
|
||||
(Test.&&) : Test -> Test -> Test
|
||||
(Test.&&) a b = case (a,b) of
|
||||
(Test.&&) a b = match (a,b) with
|
||||
(Test k1, Test k2) ->
|
||||
Test (
|
||||
scope ->
|
||||
scope ->
|
||||
let r1 = k1 scope
|
||||
r2 = k2 scope
|
||||
combine r1 r2)
|
||||
@ -95,7 +95,7 @@ Test.failedWith m = Test.label m Test.failed
|
||||
-- Report combinators
|
||||
|
||||
Test.Report.combine : Report -> Report -> Report
|
||||
Test.Report.combine r1 r2 = case (r1, r2) of
|
||||
Test.Report.combine r1 r2 = match (r1, r2) with
|
||||
(Test.Report.Report t1, Test.Report.Report t2) ->
|
||||
Report <| Trie.unionWith Status.combine t1 t2
|
||||
|
||||
@ -104,26 +104,26 @@ Test.Report.empty = Report empty
|
||||
|
||||
Test.Report.toCLIResult : Report -> [Test.Result]
|
||||
Test.Report.toCLIResult r =
|
||||
descend scope p = case p of (k, t) ->
|
||||
descend scope = cases (k, t) ->
|
||||
go ((if scope != "" then (scope ++ ".") else "") ++ k) t
|
||||
convert : Text -> Test.Status -> Test.Result
|
||||
convert scope s = case s of
|
||||
convert scope = cases
|
||||
Test.Status.Failed -> Test.Result.Fail scope
|
||||
Test.Status.Expected (Test.Success.Passed n) ->
|
||||
Test.Result.Ok (scope ++ " : Passed " ++ Nat.toText n ++ " tests.")
|
||||
Test.Status.Expected (Test.Success.Proved) ->
|
||||
Test.Result.Ok (scope ++ " : Proved.")
|
||||
go : Text -> Trie Text Test.Status -> [Test.Result]
|
||||
go scope t =
|
||||
go scope t =
|
||||
rest = flatMap (descend scope) (Map.toList (tail t))
|
||||
case head t of
|
||||
Optional.Some status ->
|
||||
match head t with
|
||||
Optional.Some status ->
|
||||
cons (convert scope status) rest
|
||||
Optional.None -> rest
|
||||
case r of Test.Report.Report t -> go "" t
|
||||
match r with Test.Report.Report t -> go "" t
|
||||
|
||||
Test.report : Test -> Report
|
||||
Test.report t = case t of Test k -> k (Scope [])
|
||||
Test.report = cases Test k -> k (Scope [])
|
||||
|
||||
-- Running tests
|
||||
|
||||
@ -136,7 +136,7 @@ Test.runAll = flatMap Test.run
|
||||
-- Status combinators
|
||||
|
||||
Status.combine : Test.Status -> Test.Status -> Test.Status
|
||||
Status.combine s1 s2 = case (s1, s2) of
|
||||
Status.combine s1 s2 = match (s1, s2) with
|
||||
(_, Pending) -> Pending
|
||||
(Pending, _) -> Pending
|
||||
(Failed, _) -> Failed
|
||||
@ -148,7 +148,7 @@ Status.combine s1 s2 = case (s1, s2) of
|
||||
|
||||
|
||||
Status.pending : Test.Status -> Test.Status
|
||||
Status.pending s = case s of
|
||||
Status.pending = cases
|
||||
Failed -> Pending
|
||||
Expected s -> Unexpected s
|
||||
Unexpected s -> Pending
|
||||
@ -156,12 +156,12 @@ Status.pending s = case s of
|
||||
|
||||
-- Make a test pending
|
||||
Test.pending : Test -> Test
|
||||
Test.pending = modifyStatus Status.pending
|
||||
Test.pending = modifyStatus Status.pending
|
||||
|
||||
Test.modifyScope : (Scope -> Scope) -> Test -> Test
|
||||
Test.modifyScope f t = case t of Test k -> Test (k . f)
|
||||
Test.modifyScope f = cases Test k -> Test (k . f)
|
||||
|
||||
Success.combine s1 s2 = case (s1, s2) of
|
||||
Success.combine s1 s2 = match (s1, s2) with
|
||||
(Passed n, Passed m) -> Passed (n + m)
|
||||
(Passed n, Proved) -> Passed n
|
||||
(Proved, Passed n) -> Passed n
|
||||
@ -181,10 +181,10 @@ Domain.nats = Large Weighted.nats
|
||||
-- The domain of all integers
|
||||
Domain.ints : Domain Int
|
||||
Domain.ints = let
|
||||
go n = yield n <|> weight 1
|
||||
go n = yield n <|> weight 1
|
||||
'(go (if n > +0 then negate n else increment (negate n)))
|
||||
Large (List.foldl (a n -> a <|> yield n)
|
||||
Weighted.Fail
|
||||
Weighted.Fail
|
||||
[+0, +1, -1, maxInt, minInt] <|> go +2)
|
||||
|
||||
use Universal == < >
|
||||
@ -200,8 +200,8 @@ namespace Domain where
|
||||
|
||||
-- The domain of lists of arbitrary data is large
|
||||
listsOf : Domain a -> Domain [a]
|
||||
listsOf d =
|
||||
Large (Weighted.lists case d of
|
||||
listsOf d =
|
||||
Large (Weighted.lists match d with
|
||||
Domain.Small as -> Weighted.fromList as
|
||||
Domain.Large w -> w)
|
||||
|
||||
@ -209,13 +209,12 @@ namespace Domain where
|
||||
lists = Domain.listsOf (Small [()])
|
||||
|
||||
sample : Nat -> Domain a -> [a]
|
||||
sample n d =
|
||||
case d of
|
||||
Domain.Large w -> Weighted.sample n w
|
||||
Domain.Small xs -> take n xs
|
||||
sample n = cases
|
||||
Domain.Large w -> Weighted.sample n w
|
||||
Domain.Small xs -> take n xs
|
||||
|
||||
map : (a -> b) -> Domain a -> Domain b
|
||||
map f d = case d of
|
||||
map f = cases
|
||||
Domain.Large w -> Domain.Large (Weighted.map f w)
|
||||
Domain.Small as -> Domain.Small (List.map f as)
|
||||
|
||||
@ -230,27 +229,27 @@ namespace Domain where
|
||||
wa = weighted da
|
||||
wb = weighted db
|
||||
wc = mergeWith (a1 a2 -> f a1 a2) wa wb
|
||||
case (da, db) of
|
||||
match (da, db) with
|
||||
(Domain.Small as, Domain.Small bs) | size as + size bs < smallSize ->
|
||||
Small (Weighted.sample smallSize wc)
|
||||
_ -> Large wc
|
||||
|
||||
weighted : Domain a -> Weighted a
|
||||
weighted d = case d of
|
||||
weighted = cases
|
||||
Domain.Small as -> Weighted.fromList as
|
||||
Domain.Large w -> w
|
||||
|
||||
-- Test a property for a given domain up to a maximum size
|
||||
Test.forAll' : Nat -> Domain a -> (a -> Boolean) -> Test
|
||||
Test.forAll' maxSize domain property =
|
||||
check xs s =
|
||||
check xs s =
|
||||
List.map (
|
||||
a -> case a of (c, i) ->
|
||||
cases (c, i) ->
|
||||
if property c then finished (Expected s)
|
||||
else label ("test case " ++ Nat.toText i) (finished Failed)
|
||||
) (indexed xs)
|
||||
List.foldb id (Test.&&) proved <|
|
||||
case domain of
|
||||
List.foldb id (Test.&&) proved <|
|
||||
match domain with
|
||||
Domain.Small xs -> check (take maxSize xs) Proved
|
||||
Domain.Large _ -> check (sample maxSize domain) (Passed 1)
|
||||
|
||||
|
@ -5,7 +5,7 @@ namespace Trie where
|
||||
empty = Trie None Map.empty
|
||||
|
||||
lookup : [k] -> Trie k v -> Optional v
|
||||
lookup path t = case path of
|
||||
lookup path t = match path with
|
||||
[] -> Trie.head t
|
||||
p +: ps -> flatMap (lookup ps) (Map.lookup p (Trie.tail t))
|
||||
|
||||
@ -13,7 +13,7 @@ namespace Trie where
|
||||
unionWith f t1 t2 =
|
||||
h1 = Trie.head t1
|
||||
h2 = Trie.head t2
|
||||
Trie (map2 f h1 h2 `orElse` h1 `orElse` h2)
|
||||
Trie (map2 f h1 h2 `orElse` h1 `orElse` h2)
|
||||
(Map.unionWith (unionWith f) (Trie.tail t1) (Trie.tail t2))
|
||||
|
||||
Trie.union : Trie k v -> Trie k v -> Trie k v
|
||||
@ -24,9 +24,9 @@ Trie.insert path v t =
|
||||
Trie.unionWith const (Trie.singleton path v) t
|
||||
|
||||
Trie.singleton : [k] -> v -> Trie k v
|
||||
Trie.singleton path v =
|
||||
case path of
|
||||
[] -> Trie (Some v) empty
|
||||
Trie.singleton path v =
|
||||
match path with
|
||||
[] -> Trie (Some v) empty
|
||||
k +: ks -> Trie None (Map.fromList [(k, Trie.singleton ks v)])
|
||||
|
||||
use Trie tail head
|
||||
@ -37,4 +37,3 @@ Trie.map f t = Trie (map f (head t)) (map (Trie.map f) (tail t))
|
||||
Trie.mapKeys : (k1 -> k2) -> Trie k1 v -> Trie k2 v
|
||||
Trie.mapKeys f t =
|
||||
Trie (head t) (Map.mapKeys f (Map.map (Trie.mapKeys f) (tail t)))
|
||||
|
||||
|
@ -5,7 +5,7 @@
|
||||
-- Adapted from http://hackage.haskell.org/package/weighted-search-0.1.0.1
|
||||
use Universal == < >
|
||||
|
||||
type Weighted a
|
||||
type Weighted a
|
||||
= Fail
|
||||
| Yield a (Weighted a)
|
||||
| Weight Nat (() -> Weighted a)
|
||||
@ -14,9 +14,9 @@ namespace Weighted where
|
||||
|
||||
weight : Nat ->{e} (() ->{e} Weighted a) ->{e} Weighted a
|
||||
weight w ws = Weight w ws
|
||||
|
||||
|
||||
map : (a ->{e} b) -> Weighted a ->{e} Weighted b
|
||||
map f wsa = case wsa of
|
||||
map f = cases
|
||||
Weighted.Fail -> Weighted.Fail
|
||||
Weighted.Yield x w -> Yield (f x) (map f w)
|
||||
Weighted.Weight a w -> weight a '(map f !w)
|
||||
@ -25,7 +25,7 @@ namespace Weighted where
|
||||
yield a = Yield a Fail
|
||||
|
||||
flatMap : (a -> Weighted b) -> Weighted a -> Weighted b
|
||||
flatMap f wsa = case wsa of
|
||||
flatMap f = cases
|
||||
Weighted.Fail -> Weighted.Fail
|
||||
Weighted.Yield x m -> f x <|> flatMap f m
|
||||
Weighted.Weight w m -> Weight w '(flatMap f !m)
|
||||
@ -35,11 +35,11 @@ namespace Weighted where
|
||||
flatMap (a -> map (b -> f a b) bs) as
|
||||
|
||||
(<|>): Weighted a -> Weighted a -> Weighted a
|
||||
(<|>) m n = case (m, n) of
|
||||
(<|>) m n = match (m, n) with
|
||||
(Weighted.Fail, n) -> n
|
||||
(Weighted.Yield x m, n) -> Yield x (m <|> n)
|
||||
(Weighted.Weight w m, Weighted.Fail) -> Weight w m
|
||||
(Weighted.Weight w m, Weighted.Yield x n) ->
|
||||
(Weighted.Weight w m, Weighted.Yield x n) ->
|
||||
Yield x (Weight w m <|> n)
|
||||
(Weighted.Weight w m, Weighted.Weight w' n) ->
|
||||
if w < w' then Weight w '(!m <|> Weight (w' `drop` w) n)
|
||||
@ -47,9 +47,9 @@ namespace Weighted where
|
||||
else Weight w '(Weight (w `drop` w') m <|> !n)
|
||||
|
||||
sample : Nat -> Weighted a -> [a]
|
||||
sample n wsa =
|
||||
sample n wsa =
|
||||
if n > 0 then
|
||||
case wsa of
|
||||
match wsa with
|
||||
Weighted.Fail -> []
|
||||
Weighted.Yield a ms -> cons a (sample (n `drop` 1) ms)
|
||||
Weighted.Weight _ w -> sample n !w
|
||||
@ -64,8 +64,6 @@ namespace Weighted where
|
||||
lists w = yield [] <|> weight 1 '(mergeWith cons w (lists w))
|
||||
|
||||
fromList : [a] -> Weighted a
|
||||
fromList as =
|
||||
case as of
|
||||
[] -> Weighted.Fail
|
||||
a +: as -> yield a <|> weight 1 '(fromList as)
|
||||
|
||||
fromList = cases
|
||||
[] -> Weighted.Fail
|
||||
a +: as -> yield a <|> weight 1 '(fromList as)
|
||||
|
@ -25,8 +25,8 @@ toInteger : Nat -> Integer
|
||||
toInteger x = _
|
||||
|
||||
bigEndian : Words -> Integer
|
||||
bigEndian ws = case ws of
|
||||
Words.Words s ->
|
||||
bigEndian = cases
|
||||
Words.Words s ->
|
||||
foldLeft Integer.zero (acc w -> shiftLeft 8 acc + toInteger w) s
|
||||
|
||||
-- TODO: Need some conversions between integers and machine integers
|
||||
@ -46,17 +46,15 @@ codeString : Text
|
||||
codeString = "123456789ABCDEFGHJKLMNPQRSTUVWXYZabcdefghijkmnopqrstuvwxyz"
|
||||
|
||||
base58Encode : Words -> Text
|
||||
base58Encode ws =
|
||||
base58Encode ws =
|
||||
x = bigEndian ws
|
||||
base58 : Integer -> Optional (Integer, Text)
|
||||
base58 a =
|
||||
base58 a =
|
||||
if a == 0
|
||||
then Optional.None
|
||||
else case divmod a 58 of
|
||||
else match divmod a 58 with
|
||||
(d, m) -> Optional.Some (d, charAt m codeString)
|
||||
foldLeft "" Text.concatenate (unfoldRight base58 x)
|
||||
|
||||
base58Decode : Text -> Words
|
||||
base58Decode txt = _
|
||||
|
||||
|
||||
|
@ -25,9 +25,9 @@ merge : (a -> a -> Boolean) -> [a] -> [a] -> [a]
|
||||
merge lte a b =
|
||||
use Sequence ++
|
||||
use Optional None Some
|
||||
go acc a b = case at 0 a of
|
||||
go acc a b = match at 0 a with
|
||||
None -> acc ++ b
|
||||
Some hd1 -> case at 0 b of
|
||||
Some hd1 -> match at 0 b with
|
||||
None -> acc ++ a
|
||||
Some hd2 ->
|
||||
if hd1 `lte` hd2 then go (acc `snoc` hd1) (drop 1 a) b
|
||||
|
@ -2,7 +2,7 @@ use Optional None Some
|
||||
use Universal <
|
||||
|
||||
uncons : [a] -> Optional (a, [a])
|
||||
uncons as = case at 0 as of
|
||||
uncons as = match at 0 as with
|
||||
None -> None
|
||||
Some hd -> Some (hd, drop 1 as)
|
||||
|
||||
@ -15,7 +15,7 @@ splitAt n as = (take n as, drop n as)
|
||||
merge : (a -> a -> Boolean) -> [a] -> [a] -> [a]
|
||||
merge lte a b =
|
||||
use List ++
|
||||
go out a b = case (uncons a, uncons b) of
|
||||
go out a b = match (uncons a, uncons b) with
|
||||
(None,_) -> out ++ b
|
||||
(_,None) -> out ++ a
|
||||
(Some (hA, tA), Some (hB, tB)) ->
|
||||
@ -26,7 +26,7 @@ merge lte a b =
|
||||
sort : (a -> a -> Boolean) -> [a] -> [a]
|
||||
sort lte as =
|
||||
if size as < 2 then as
|
||||
else case halve as of (left, right) ->
|
||||
else match halve as with (left, right) ->
|
||||
l = sort lte left
|
||||
r = sort lte right
|
||||
merge lte l r
|
||||
|
@ -13,7 +13,7 @@ ability Remote where
|
||||
type Node = Node Nat -- more realistic would be perhaps a (Hostname, PublicKey) pair
|
||||
|
||||
force : Future a ->{Remote} a
|
||||
force f = case f of Future.Future r -> !r
|
||||
force = cases Future.Future r -> !r
|
||||
|
||||
-- Let's test out this beast! do we need to deploy our code to some EC2 instances??
|
||||
-- Gak, no not yet, we just want to test locally, let's write a handler
|
||||
@ -27,22 +27,22 @@ use Universal <
|
||||
|
||||
List.map : (a ->{e} b) -> [a] ->{e} [b]
|
||||
List.map f as =
|
||||
go f acc as i = case at i as of
|
||||
go f acc as i = match at i as with
|
||||
None -> acc
|
||||
Some a -> go f (acc `snoc` f a) as (i + 1)
|
||||
go f [] as 0
|
||||
|
||||
type Monoid a = Monoid (a -> a -> a) a
|
||||
|
||||
Monoid.zero m = case m of Monoid.Monoid op z -> z
|
||||
Monoid.op m = case m of Monoid.Monoid op z -> op
|
||||
Monoid.zero = cases Monoid.Monoid op z -> z
|
||||
Monoid.op = cases Monoid.Monoid op z -> op
|
||||
|
||||
Monoid.orElse m a = case a of
|
||||
Monoid.orElse m = cases
|
||||
None -> Monoid.zero m
|
||||
Some a -> a
|
||||
|
||||
uncons : [a] -> Optional (a, [a])
|
||||
uncons as = case at 0 as of
|
||||
uncons as = match at 0 as with
|
||||
None -> None
|
||||
Some hd -> Some (hd, drop 1 as)
|
||||
|
||||
@ -71,11 +71,11 @@ splitAt n as = (take n as, drop n as)
|
||||
Node.increment : Node -> Node
|
||||
Node.increment n =
|
||||
use Node.Node -- the constructor
|
||||
case n of Node n -> Node (n + 1)
|
||||
match n with Node n -> Node (n + 1)
|
||||
|
||||
Remote.runLocal : '{Remote} a -> a
|
||||
Remote.runLocal r =
|
||||
step nid r = case r of
|
||||
step nid = cases
|
||||
{Remote.spawn -> k} -> handle (step (Node.increment nid)) in k nid
|
||||
{Remote.at _ t -> k} -> handle (step nid) in k (Future t)
|
||||
{a} -> a -- the pure case
|
||||
@ -83,7 +83,7 @@ Remote.runLocal r =
|
||||
|
||||
merge : (a -> a -> Boolean) -> [a] -> [a] -> [a]
|
||||
merge lte a b =
|
||||
go out a b = case (uncons a, uncons b) of
|
||||
go out a b = match (uncons a, uncons b) with
|
||||
(None,_) -> out ++ b
|
||||
(_,None) -> out ++ a
|
||||
(Some (hA, tA), Some (hB, tB)) ->
|
||||
@ -96,7 +96,7 @@ merge lte a b =
|
||||
sort : (a -> a -> Boolean) -> [a] -> [a]
|
||||
sort lte as =
|
||||
if size as < 2 then as
|
||||
else case halve as of (left, right) ->
|
||||
else match halve as with (left, right) ->
|
||||
l = sort lte left
|
||||
r = sort lte right
|
||||
merge lte l r
|
||||
@ -105,7 +105,7 @@ dsort : (a -> a -> Boolean) -> [a] ->{Remote} [a]
|
||||
dsort lte as =
|
||||
use Remote at spawn
|
||||
if size as < 2 then as
|
||||
else case halve as of (left, right) ->
|
||||
else match halve as with (left, right) ->
|
||||
r1 = at spawn '(dsort lte left)
|
||||
r2 = at spawn '(dsort lte right)
|
||||
merge lte (force r1) (force r2)
|
||||
@ -113,4 +113,3 @@ dsort lte as =
|
||||
> sort (<) [1,2,3,234,6,2,4,66,2,33,4,2,57]
|
||||
|
||||
> Remote.runLocal '(dsort (<) [1,2,3,234,6,2,4,66,2,33,4,2,57])
|
||||
|
||||
|
@ -1,3 +1,3 @@
|
||||
case 3 of
|
||||
match 3 with
|
||||
3 -> 4
|
||||
4 -> "Surprise!"
|
||||
|
@ -1,2 +1,2 @@
|
||||
case 3 of
|
||||
match 3 with
|
||||
3 | 3 -> 4
|
||||
|
@ -1,3 +1,3 @@
|
||||
case 3 of
|
||||
match 3 with
|
||||
3 -> "Great!"
|
||||
"Great" -> "Terrible."
|
||||
|
@ -2,7 +2,7 @@ type Foo a b = Foo a b
|
||||
use Foo Foo
|
||||
use Optional Some
|
||||
setA : Foo a b -> Optional a -> Foo a b
|
||||
setA foo a = case (foo, a) of
|
||||
setA foo a = match (foo, a) with
|
||||
(Foo _ b, Some a) -> Foo a b
|
||||
_ -> foo
|
||||
|
||||
|
@ -1,4 +1,4 @@
|
||||
notid : Int -> Boolean
|
||||
notid a = true
|
||||
case 3 of
|
||||
match 3 with
|
||||
3 | notid 3 -> 4
|
||||
|
@ -1,2 +1,2 @@
|
||||
case 3 of
|
||||
match 3 with
|
||||
3 | (3 : Boolean) -> 4
|
||||
|
@ -6,15 +6,14 @@ ability Console where
|
||||
read : () -> {Console} (Optional Text)
|
||||
write : Text -> {Console} ()
|
||||
|
||||
fst x = case x of Tuple.Cons a _ -> a
|
||||
fst = cases Tuple.Cons a _ -> a
|
||||
|
||||
snd x = case x of Tuple.Cons _ (Tuple.Cons b _) -> b
|
||||
snd = cases Tuple.Cons _ (Tuple.Cons b _) -> b
|
||||
|
||||
namespace Console where
|
||||
|
||||
simulate : Request Console a -> {State ([Text], [Text])} a
|
||||
simulate c = case c of
|
||||
{Console.read _ -> k} -> k Optional.None
|
||||
simulate = cases
|
||||
{Console.read _ -> k} -> k Optional.None
|
||||
|
||||
Console.simulate
|
||||
|
||||
|
@ -6,14 +6,14 @@ ability Console where
|
||||
read : {Console} (Optional Text)
|
||||
write : Text -> {Console} ()
|
||||
|
||||
fst x = case x of Tuple.Cons a _ -> a
|
||||
fst = cases Tuple.Cons a _ -> a
|
||||
|
||||
snd x = case x of Tuple.Cons _ (Tuple.Cons b _) -> b
|
||||
snd = cases Tuple.Cons _ (Tuple.Cons b _) -> b
|
||||
|
||||
namespace Console where
|
||||
|
||||
simulate : Request Console a -> {State ([Text], [Text])} a
|
||||
simulate c = case c of
|
||||
simulate = cases
|
||||
{Console.read -> k} ->
|
||||
io = State.get
|
||||
ins = fst io
|
||||
@ -27,4 +27,3 @@ namespace Console where
|
||||
k (State.set (ins, cons t outs)) -- this is missing recursive call
|
||||
|
||||
()
|
||||
|
||||
|
@ -1,7 +1,7 @@
|
||||
use Optional None Some
|
||||
|
||||
foo : Optional a -> [a]
|
||||
foo a = case a of
|
||||
foo = cases
|
||||
None -> []
|
||||
Some a -> [a]
|
||||
|
||||
@ -16,7 +16,7 @@ foo a = case a of
|
||||
-- e <- errorTerm
|
||||
-- b <- isFunctionCall
|
||||
-- if b then do
|
||||
--
|
||||
--
|
||||
|
||||
|
||||
-- in reply to `> why err1`:
|
||||
@ -44,6 +44,6 @@ and x 4
|
||||
and 3 4
|
||||
-- but the literal `3` has type `Nat`.
|
||||
|
||||
case 3 of
|
||||
match 3 with
|
||||
3 -> "text"
|
||||
4 -> 4.0
|
||||
|
@ -3,7 +3,7 @@ ability State s where
|
||||
get : ∀ s . () -> {State s} s
|
||||
set : ∀ s . s -> {State s} ()
|
||||
state : ∀ a s . s -> Request (State s) a -> a
|
||||
state s e = case e of
|
||||
state s = cases
|
||||
{a} -> a
|
||||
{State.get _ -> k} -> handle state s in k s
|
||||
{State.set s -> k} -> handle state s in k ()
|
||||
|
@ -4,7 +4,7 @@ ability State se2 where
|
||||
get : ∀ se . () -> {State se} se
|
||||
|
||||
state : ∀ s a . s -> Request (State s) a -> (s, a)
|
||||
state woot eff = case eff of
|
||||
state woot = cases
|
||||
{ State.get () -> k } -> handle (state woot) in (k woot)
|
||||
{ State.put snew -> k } -> handle (state snew) in (k ())
|
||||
|
||||
|
@ -24,10 +24,10 @@ use Remote fork spawn at
|
||||
namespace Monoid where
|
||||
|
||||
zero : Monoid a -> a
|
||||
zero m = case m of Monoid _ z -> z
|
||||
zero = cases Monoid _ z -> z
|
||||
|
||||
op : Monoid a -> a -> a -> a
|
||||
op m = case m of Monoid op _ -> op
|
||||
op = cases Monoid op _ -> op
|
||||
|
||||
foldMap : (a -> {e} b) -> Monoid b -> [a] -> {e} b
|
||||
foldMap f m as =
|
||||
@ -36,7 +36,7 @@ namespace Monoid where
|
||||
-- and `zero m` is of type `b`, but `as` is of type `[a]`
|
||||
-- 👇
|
||||
if size as < 2 then Sequence.foldLeft op (zero m) as
|
||||
else case Sequence.halve as of (l, r) -> foldMap f m l `op` foldMap f m r
|
||||
else match Sequence.halve as with (l, r) -> foldMap f m l `op` foldMap f m r
|
||||
|
||||
par : Monoid a -> Monoid ('{Remote n} a)
|
||||
par m =
|
||||
@ -79,7 +79,7 @@ parApply f a b = 'let
|
||||
Remote.runLocal : '{Remote Nat} a -> a
|
||||
Remote.runLocal r =
|
||||
step : Nat -> Request (Remote Nat) a -> a
|
||||
step nid r = case r of
|
||||
step nid = cases
|
||||
{a} -> a
|
||||
{Remote.fork t -> k} -> handle (step nid) in k t
|
||||
{Remote.spawn -> k} -> handle (step (nid + 1)) in k nid
|
||||
@ -100,4 +100,3 @@ i |> f = f i
|
||||
Stream.fromNat 1
|
||||
|> Stream.take 15
|
||||
|> Stream.toSequence
|
||||
|
||||
|
@ -5,7 +5,7 @@ ability Noop where
|
||||
type List a = Nil | Cons a (List a)
|
||||
|
||||
map : (a ->{} b) -> List a -> List b
|
||||
map f as = case as of
|
||||
map f = cases
|
||||
List.Nil -> List.Nil
|
||||
List.Cons h t -> List.Cons (f h) (map f t)
|
||||
|
||||
|
@ -1,5 +1,5 @@
|
||||
reduce2 : a -> (a -> a -> a) -> Sequence a -> a
|
||||
reduce2 a0 f s = case at 0 s of
|
||||
reduce2 a0 f s = match at 0 s with
|
||||
Optional.None -> a0
|
||||
Optional.Some a1 -> reduce (f a0 a1) f (drop 1 s)
|
||||
|
||||
|
@ -12,20 +12,20 @@ ability Console where
|
||||
read : {Console} (Optional Text)
|
||||
write : Text -> {Console} ()
|
||||
|
||||
fst x = case x of Tuple.Cons a _ -> a
|
||||
fst = cases Tuple.Cons a _ -> a
|
||||
|
||||
snd x = case x of Tuple.Cons _ (Tuple.Cons b _) -> b
|
||||
snd = cases Tuple.Cons _ (Tuple.Cons b _) -> b
|
||||
|
||||
namespace Console where
|
||||
|
||||
state : s -> Request (State s) a -> a
|
||||
state s c = case c of
|
||||
state s = cases
|
||||
{State.get -> k} -> handle state s in k s
|
||||
{State.set s' -> k} -> handle state s' in k ()
|
||||
{a} -> a
|
||||
|
||||
simulate : Request Console d -> {State ([Text], [Text])} d
|
||||
simulate c = case c of
|
||||
simulate = cases
|
||||
{Console.read -> k} ->
|
||||
io = State.get
|
||||
ins = fst io
|
||||
@ -33,26 +33,25 @@ namespace Console where
|
||||
State.set (drop 1 ins, outs)
|
||||
-- this really should typecheck but doesn't for some reason
|
||||
-- error is that `simulate` doesn't check against `Request Console c -> r`,
|
||||
-- but seems like that `r` should get instantiated as `{State (..)} c`.
|
||||
-- but seems like that `r` should get instantiated as `{State (..)} c`.
|
||||
handle simulate in k (at 0 ins)
|
||||
{Console.write t -> k} ->
|
||||
io = State.get
|
||||
ins = fst io
|
||||
outs = snd io
|
||||
-- same deal here
|
||||
-- same deal here
|
||||
handle simulate in k (State.set (ins, cons t outs))
|
||||
{a} -> a
|
||||
|
||||
(++) = concatenate
|
||||
|
||||
handle
|
||||
handle Console.simulate in
|
||||
handle
|
||||
handle Console.simulate in
|
||||
use Console read write
|
||||
use Optional Some None
|
||||
write "What's your name?"
|
||||
case read of
|
||||
match read with
|
||||
Some name -> write ("Hello" ++ name)
|
||||
None -> write "Fine, be that way."
|
||||
|
||||
()
|
||||
|
||||
|
@ -9,7 +9,7 @@ id5 a b c d e = (a, b, c, d, e)
|
||||
|
||||
id5 1 +2 3 4 5
|
||||
|
||||
-- (case true of
|
||||
-- (match true with
|
||||
-- true -> first
|
||||
-- false -> second) 1 +2
|
||||
|
||||
|
@ -12,7 +12,7 @@ ability State s where
|
||||
get : {State s} s
|
||||
|
||||
state : s -> Request (State s) a -> (s, a)
|
||||
state woot eff = case eff of
|
||||
state woot = cases
|
||||
{ State.get -> k } -> handle (state woot) in (k woot)
|
||||
{ State.put snew -> k } -> handle (state snew) in (k ())
|
||||
{ a } -> (woot, a)
|
||||
@ -24,7 +24,7 @@ increment : '{State Nat} ()
|
||||
increment = '(modify ((+) 1))
|
||||
|
||||
first : (a, b) -> a
|
||||
first p = case p of (a,_) -> a
|
||||
first = cases (a,_) -> a
|
||||
|
||||
ex : Nat
|
||||
ex =
|
||||
@ -38,5 +38,3 @@ ex =
|
||||
first result
|
||||
|
||||
()
|
||||
|
||||
|
||||
|
@ -15,11 +15,10 @@ ability Ask foo where
|
||||
ask : () -> {Ask a} a
|
||||
|
||||
supply : Text -> Request (Ask Text) a -> a
|
||||
supply t e = case e of
|
||||
supply t = cases
|
||||
{a} -> a
|
||||
-- `k` should be of type `Text -> Request Ask a`,
|
||||
-- so calling it with `()` here should be a type error
|
||||
{Ask.ask _ -> k} -> handle supply t in k ()
|
||||
|
||||
supply
|
||||
|
||||
|
@ -1,12 +1,12 @@
|
||||
--mismatched case result types
|
||||
type Optional a = None | Some a
|
||||
case Optional.Some 3 of
|
||||
match Optional.Some 3 with
|
||||
x -> 1
|
||||
y -> "boo"
|
||||
|
||||
-- as of 5ae98f7, produces this message:
|
||||
|
||||
--Each case of a case/of expression need to have the same type.
|
||||
--Each case of a match/with expression need to have the same type.
|
||||
-- Here, one is Nat, and another is Text:
|
||||
--
|
||||
-- 4 | x -> 1 -- x is highlighted
|
||||
|
@ -14,9 +14,8 @@ ability Ask a where
|
||||
ask : {Ask a} a
|
||||
|
||||
supply : Text -> Request (Ask Text) a -> a
|
||||
supply t e = case e of
|
||||
supply t = cases
|
||||
{a} -> "foo" -- a
|
||||
{Ask.ask -> k} -> handle supply t in k ()
|
||||
|
||||
()
|
||||
|
||||
|
@ -6,12 +6,12 @@ type Board = Board P P
|
||||
use Board.Board
|
||||
use P O X E
|
||||
|
||||
case Board X O X
|
||||
of Board a b c -> a
|
||||
match Board X O X
|
||||
with Board a b c -> a
|
||||
|
||||
|
||||
-- gives this error:
|
||||
-- This looks like a function call, but with a Board where the function should be. Are you missing an operator?
|
||||
-- ^^^^^
|
||||
-- 13 | case Board X O X
|
||||
-- 13 | match Board X O X
|
||||
-- ^^^^^
|
||||
|
@ -1,11 +1,10 @@
|
||||
-- The location of the error is imprecise. It should point to
|
||||
-- The location of the error is imprecise. It should point to
|
||||
-- the pattern `Bar.Bar`.
|
||||
|
||||
unique type Foo = Foo
|
||||
unique type Bar = Bar
|
||||
|
||||
foo : Foo -> Foo
|
||||
foo x = case x of
|
||||
foo = cases
|
||||
Foo.Foo -> Foo
|
||||
Bar.Bar -> Foo
|
||||
|
||||
|
@ -7,18 +7,18 @@ use Foo0 Foo0
|
||||
use Foo1 Foo1
|
||||
use Foo2 Foo2
|
||||
|
||||
x = case Foo0 of
|
||||
x = match Foo0 with
|
||||
Foo0 -> 1
|
||||
|
||||
y = case Foo1 1 of
|
||||
y = match Foo1 1 with
|
||||
Foo1 1 -> 0
|
||||
Foo1 _ -> 10
|
||||
|
||||
z = case Foo2 1 "hi" of
|
||||
z = match Foo2 1 "hi" with
|
||||
Foo2 x _ -> x
|
||||
Foo2 1 _ -> 1
|
||||
|
||||
w = case Foo3.Foo3 1 2 "bye" of
|
||||
w = match Foo3.Foo3 1 2 "bye" with
|
||||
Foo3.Foo3 1 2 x -> Text.concatenate x "bye"
|
||||
-- where the heck are these locations coming from?
|
||||
-- I feel, since concatenate isn't polymorphic, that `Text`
|
||||
|
@ -13,7 +13,7 @@ iterate a n f =
|
||||
|
||||
use Optional Some None
|
||||
reduce : a -> (a -> a -> a) -> Sequence a -> a
|
||||
reduce a0 f s = case at 0 s of
|
||||
reduce a0 f s = match at 0 s with
|
||||
Optional.None -> a0
|
||||
Optional.Some a1 -> reduce (f a0 a1) f (drop 1 s)
|
||||
|
||||
|
@ -8,8 +8,8 @@ use Board.Board
|
||||
-- x = 1
|
||||
-- y = 2
|
||||
|
||||
ex = case Board 77 88 99
|
||||
of Board a b c -> c
|
||||
ex = match Board 77 88 99
|
||||
with Board a b c -> c
|
||||
|
||||
-- yields:
|
||||
|
||||
@ -18,7 +18,7 @@ ex = case Board 77 88 99
|
||||
-- I was expecting an indented block following the`of` keyword
|
||||
-- but instead found an outdent:
|
||||
--
|
||||
-- 12 | of Board a b c -> c
|
||||
-- 12 | with Board a b c -> c
|
||||
-- SourcePos {sourceName = "/Users/pchiusano/work/unison/unison-src/tests/tictactoe0-array-oob1.u", sourceLine = Pos 12, sourceColumn = Pos 3}
|
||||
|
||||
-- What's with the `SourcePos` default show instance here?
|
||||
|
@ -1,3 +1,3 @@
|
||||
test : [a] -> ([a], [a])
|
||||
test l = case l of
|
||||
test l = match l with
|
||||
x ++ y -> (x, y)
|
||||
|
@ -1,6 +1,5 @@
|
||||
--mismatched case result types
|
||||
type Optional a = None | Some a
|
||||
case Optional.Some 3 of
|
||||
match Optional.Some 3 with
|
||||
x -> 1
|
||||
y -> "boo"
|
||||
|
||||
|
@ -1,7 +1,7 @@
|
||||
--Type.apply
|
||||
type List a = Nil | Cons a (List a)
|
||||
map : ∀ a b . (a -> b) -> List a -> List b
|
||||
map f as = case as of
|
||||
map f = cases
|
||||
List.Nil -> List.Nil
|
||||
List.Cons h t -> List.Cons h (map f t) -- should not typecheck, missing (f h)
|
||||
-- definitely should not typecheck!
|
||||
@ -13,4 +13,3 @@ ex = c 1 (c 2 (c 3 z))
|
||||
pureMap : List Int -- should fail, output is a `List Text`
|
||||
pureMap = map (a -> "hi") ex
|
||||
()
|
||||
|
||||
|
@ -3,7 +3,7 @@ ability Ask a where
|
||||
ask : {Ask a} a
|
||||
|
||||
supply : Text -> Request (Ask Text) a -> a
|
||||
supply t e = case e of
|
||||
supply t = cases
|
||||
{a} -> a
|
||||
-- `k` should be of type `Text -> Request Ask a`,
|
||||
-- so calling it with `()` here should be a type error
|
||||
|
@ -1,3 +1,3 @@
|
||||
foo n = case n of
|
||||
foo n = match n with
|
||||
|
||||
bar = 3
|
||||
bar = 3
|
||||
|
@ -34,16 +34,16 @@ type Future.Error = UnknownFuture | UnreachableLocation | UnresponsiveLocation |
|
||||
-- Remote.server computation =
|
||||
|
||||
Future.join : Future loc a ->{Remote loc, Error Future.Error} a
|
||||
Future.join f = case f of Future.Future (b, c, s, j) -> !j
|
||||
Future.join = cases Future.Future (b, c, s, j) -> !j
|
||||
|
||||
Future.cancel : Future loc a ->{Remote loc} ()
|
||||
Future.cancel f = case f of Future.Future (b, c, s, j) -> !c
|
||||
Future.cancel = cases Future.Future (b, c, s, j) -> !c
|
||||
|
||||
Future.status : Future loc a ->{Remote loc} Status
|
||||
Future.status f = case f of Future.Future (b, c, s, j) -> !s
|
||||
Future.status = cases Future.Future (b, c, s, j) -> !s
|
||||
|
||||
Future.begin : Future loc a ->{Remote loc} ()
|
||||
Future.begin f = case f of Future.Future (b, c, s, j) -> !b
|
||||
Future.begin = cases Future.Future (b, c, s, j) -> !b
|
||||
|
||||
|
||||
type UnitLoc e = UnitLoc
|
||||
@ -51,7 +51,7 @@ type UnitLoc e = UnitLoc
|
||||
-- Remote.runSequential : '{Remote UnitLoc, Error e} a -> Either e a
|
||||
-- Remote.runSequential r =
|
||||
-- step : Request {Remote UnitLoc} a -> a
|
||||
-- step r = case r of
|
||||
-- step = cases
|
||||
-- {a} -> a
|
||||
-- {Remote.fork loc t -> k} ->
|
||||
-- join = Right !t
|
||||
@ -60,7 +60,7 @@ type UnitLoc e = UnitLoc
|
||||
-- keepalive d = ()
|
||||
-- handle step in k (Future ('join, 'cancel, 'status, keepalive))
|
||||
-- err : Request {Error e} a -> Either e a
|
||||
-- err e = case e of
|
||||
-- err = cases
|
||||
-- {a} -> Right a
|
||||
-- {Error.error t -> k} ->handle err in k (Left t)
|
||||
-- handle err in handle step in !r
|
||||
@ -70,7 +70,7 @@ type UnitLoc e = UnitLoc
|
||||
-- use Optional Some None
|
||||
-- use Either Left Right
|
||||
-- Either.join : Either a (Either a b) -> Either a b
|
||||
-- Either.join e = case e of
|
||||
-- Either.join = cases
|
||||
-- Left a -> Left a
|
||||
-- Right e -> e
|
||||
--
|
||||
@ -80,7 +80,7 @@ type UnitLoc e = UnitLoc
|
||||
-- merge z l r =
|
||||
-- l0 = at 0 l
|
||||
-- r0 = at 0 r
|
||||
-- case (l0, r0) of
|
||||
-- match (l0, r0) with
|
||||
-- (None, _) -> z ++ r
|
||||
-- (_, None) -> z ++ l
|
||||
-- (Some l0, Some r0) ->
|
||||
|
@ -32,7 +32,7 @@ ex1 n a =
|
||||
|
||||
Remote.runLocal : '{Remote} a -> a
|
||||
Remote.runLocal r =
|
||||
step nid r = case r of
|
||||
step nid = cases
|
||||
{a} -> a
|
||||
{Remote.fork t -> k} -> handle (step nid) in k t
|
||||
{Remote.spawn -> k} -> handle (step (Node.increment nid)) in k nid
|
||||
@ -64,4 +64,4 @@ Remote.forkAt node r = Remote.fork '(Remote.at node r)
|
||||
Node.increment : Node -> Node
|
||||
Node.increment n =
|
||||
use Node.Node -- the constructor
|
||||
case n of Node n -> Node (n + 1)
|
||||
match n with Node n -> Node (n + 1)
|
||||
|
@ -13,14 +13,14 @@ namespace Suit where
|
||||
|
||||
namespace Rank where
|
||||
all = [A, _10, K, Q, J, _9, _8, _7]
|
||||
points r = case r of
|
||||
points = cases
|
||||
A -> 11
|
||||
_10 -> 10
|
||||
K -> 4
|
||||
Q -> 3
|
||||
J -> 2
|
||||
_ -> 0
|
||||
toText r = case r of
|
||||
toText = cases
|
||||
A -> "A"
|
||||
K -> "K"
|
||||
Q -> "Q"
|
||||
@ -31,9 +31,9 @@ namespace Rank where
|
||||
_7 -> "7"
|
||||
|
||||
namespace NonEmpty where
|
||||
toList n = case n of
|
||||
toList = cases
|
||||
NonEmpty h t -> Sequence.cons h t
|
||||
fromList : [a] -> Optional (NonEmpty a)
|
||||
fromList l = case Sequence.at 0 l of
|
||||
fromList l = match Sequence.at 0 l with
|
||||
None -> None
|
||||
Some a -> Some (NonEmpty a (Sequence.drop 1 l))
|
||||
|
@ -1,7 +1,7 @@
|
||||
type Optional a = None | Some a
|
||||
|
||||
Optional.isEmpty : Optional a -> Boolean
|
||||
Optional.isEmpty o = match o with
|
||||
Optional.isEmpty = cases
|
||||
Optional.None -> true
|
||||
Optional.Some _ -> false
|
||||
|
||||
|
@ -2,7 +2,7 @@
|
||||
ability Abort where
|
||||
Abort : forall a . () -> {Abort} a
|
||||
eff : forall a b . (a -> b) -> b -> Request Abort a -> b
|
||||
eff f z e = match e with
|
||||
eff f z = cases
|
||||
{ Abort.Abort _ -> k } -> z
|
||||
{ a } -> f a
|
||||
-- heff : Nat
|
||||
|
@ -8,9 +8,8 @@
|
||||
|
||||
use Universal ==
|
||||
|
||||
f blah =
|
||||
match blah with
|
||||
x | x == "woot" -> false
|
||||
y | y == "foo" -> true
|
||||
f = cases
|
||||
x | x == "woot" -> false
|
||||
y | y == "foo" -> true
|
||||
|
||||
-- > f "woot"
|
||||
|
@ -19,7 +19,7 @@ ability Remote where
|
||||
type Node = Node Nat -- more realistic would be perhaps a (Hostname, PublicKey) pair
|
||||
|
||||
force : Future a ->{Remote} a
|
||||
force f = match f with Future.Future r -> !r
|
||||
force = cases Future.Future r -> !r
|
||||
|
||||
Future.fromThunk : '{Remote} a -> Future a
|
||||
Future.fromThunk = Future.Future
|
||||
@ -30,7 +30,7 @@ Future.fromThunk = Future.Future
|
||||
|
||||
Remote.runLocal : '{Remote} a -> a
|
||||
Remote.runLocal r =
|
||||
step nid r = match r with
|
||||
step nid = cases
|
||||
{a} -> a
|
||||
{Remote.fork t -> k} -> handle k (Future.fromThunk t) with step nid
|
||||
{Remote.spawn -> k} -> handle k nid with step (Node.increment nid)
|
||||
@ -53,10 +53,10 @@ List.map f as =
|
||||
|
||||
type Monoid a = Monoid (a -> a -> a) a
|
||||
|
||||
Monoid.zero m = match m with Monoid.Monoid op z -> z
|
||||
Monoid.op m = match m with Monoid.Monoid op z -> op
|
||||
Monoid.zero = cases Monoid.Monoid op z -> z
|
||||
Monoid.op = cases Monoid.Monoid op z -> op
|
||||
|
||||
Monoid.orElse m a = match a with
|
||||
Monoid.orElse m = cases
|
||||
None -> Monoid.zero m
|
||||
Some a -> a
|
||||
|
||||
|
@ -6,21 +6,21 @@ ability Console where
|
||||
read : {Console} (Optional Text)
|
||||
write : Text -> {Console} ()
|
||||
|
||||
fst x = match x with Tuple.Cons a _ -> a
|
||||
fst = cases Tuple.Cons a _ -> a
|
||||
|
||||
--TODO type is wrongly being inferred (or at least displayed) as `Tuple a (Tuple a b) ->{} a`
|
||||
snd x = match x with Tuple.Cons _ (Tuple.Cons b _) -> b
|
||||
snd = cases Tuple.Cons _ (Tuple.Cons b _) -> b
|
||||
|
||||
namespace Console where
|
||||
|
||||
state : s -> Request (State s) a -> a
|
||||
state s c = match c with
|
||||
state s = cases
|
||||
{State.get -> k} -> handle k s with state s
|
||||
{State.set s' -> k} -> handle k () with state s'
|
||||
{a} -> a
|
||||
|
||||
simulate : Request Console d -> {State ([Text], [Text])} d
|
||||
simulate c = match c with
|
||||
simulate = cases
|
||||
{Console.read -> k} ->
|
||||
io = State.get
|
||||
ins = fst io
|
||||
|
@ -11,14 +11,14 @@ ability Console where
|
||||
|
||||
use Console simulate
|
||||
|
||||
fst x = match x with Tuple.Cons a _ -> a
|
||||
fst = cases Tuple.Cons a _ -> a
|
||||
|
||||
snd x = match x with Tuple.Cons _ (Tuple.Cons b _) -> b
|
||||
snd = cases Tuple.Cons _ (Tuple.Cons b _) -> b
|
||||
|
||||
namespace Console where
|
||||
|
||||
simulate : Request Console a -> {State ([Text], [Text])} a
|
||||
simulate c = match c with
|
||||
simulate = cases
|
||||
{Console.read -> k} -> handle
|
||||
io = State.get
|
||||
ins = fst io
|
||||
|
@ -1,11 +1,8 @@
|
||||
|
||||
eff : forall a b . (a -> b) -> b -> Request Abort a -> b
|
||||
eff f z e = match e with
|
||||
eff f z = cases
|
||||
{ Abort.Abort _ -> k } -> z
|
||||
{ a } -> f a
|
||||
|
||||
ability Abort where
|
||||
Abort : forall a . () -> {Abort} a
|
||||
|
||||
|
||||
|
||||
|
@ -1,11 +1,11 @@
|
||||
type Foo = Foo Boolean Boolean
|
||||
|
||||
f : Foo -> Boolean
|
||||
f x = match x with
|
||||
f = cases
|
||||
Foo.Foo a b | a || b -> true
|
||||
_ -> false
|
||||
|
||||
g : Foo -> Boolean
|
||||
g x = match x with
|
||||
g = cases
|
||||
Foo.Foo a b | a && b -> true
|
||||
_ -> false
|
||||
|
@ -23,12 +23,12 @@ ability Writer w where
|
||||
tell : w -> {Writer w} ()
|
||||
|
||||
stateHandler : s -> Request {State s} a -> (s, a)
|
||||
stateHandler s x = match x with
|
||||
stateHandler s = cases
|
||||
{ State.get -> k } -> handle k s with stateHandler s
|
||||
{ State.put s -> k } -> handle k () with stateHandler s
|
||||
{ a } -> (s, a)
|
||||
|
||||
writerHandler : [w] -> Request {Writer w} a -> ([w], a)
|
||||
writerHandler ww x = match x with
|
||||
writerHandler ww = cases
|
||||
{ Writer.tell w -> k } -> handle k () with writerHandler (ww `snoc` w)
|
||||
{ a } -> (ww, a)
|
||||
|
@ -20,7 +20,7 @@ ability Remote where
|
||||
type Node = Node Nat -- more realistic would be perhaps a (Hostname, PublicKey) pair
|
||||
|
||||
force : Future a ->{Remote} a
|
||||
force f = match f with Future.Future r -> !r
|
||||
force = cases Future.Future r -> !r
|
||||
|
||||
-- Let's test out this beast! do we need to deploy our code to some EC2 instances??
|
||||
-- Gak, no not yet, we just want to test locally, let's write a handler
|
||||
@ -29,7 +29,7 @@ force f = match f with Future.Future r -> !r
|
||||
Remote.runLocal : '{Remote} a -> a
|
||||
Remote.runLocal r =
|
||||
use Future Future
|
||||
step nid r = match r with
|
||||
step nid = cases
|
||||
{a} -> a
|
||||
{Remote.fork t -> k} -> handle k (Future t) with step nid
|
||||
{Remote.spawn -> k} -> handle k nid with step (Node.increment nid)
|
||||
|
@ -8,7 +8,7 @@ ability Noop2 where
|
||||
type List a = Nil | Cons a (List a)
|
||||
|
||||
map : ∀ a b e . (a -> {e} b) -> List a -> {e} (List b)
|
||||
map f as = match as with
|
||||
map f = cases
|
||||
List.Nil -> List.Nil
|
||||
List.Cons h t -> List.Cons (f h) (map f t)
|
||||
|
||||
@ -28,5 +28,3 @@ zappy u = map (zap -> (Noop.noop (zap Nat.+ 1))) ex
|
||||
-- mixing multiple abilitys in a call to `map` works fine
|
||||
zappy2 : () -> {Noop, Noop2} (List Nat)
|
||||
zappy2 u = map (zap -> Noop.noop (zap Nat.+ Noop2.noop2 2 7)) ex
|
||||
|
||||
|
||||
|
@ -8,7 +8,7 @@ ability Noop2 where
|
||||
type List a = Nil | Cons a (List a)
|
||||
|
||||
map : (a -> b) -> List a -> List b
|
||||
map f as = match as with
|
||||
map f = cases
|
||||
List.Nil -> List.Nil
|
||||
List.Cons h t -> List.Cons (f h) (map f t)
|
||||
|
||||
@ -30,6 +30,3 @@ zappy = 'let map (zap -> Noop.noop (zap Nat.+ 1)) ex
|
||||
zappy2 : '{Noop, Noop2} (List Nat)
|
||||
zappy2 = 'let
|
||||
map (zap -> Noop.noop (zap Nat.+ Noop2.noop2 2 7)) ex
|
||||
|
||||
|
||||
|
||||
|
@ -4,7 +4,7 @@
|
||||
ability A where
|
||||
woot : {A} Nat
|
||||
|
||||
unA w = match w with
|
||||
unA = cases
|
||||
{a} -> a
|
||||
{A.woot -> k} -> handle k 10 with unA
|
||||
|
||||
|
@ -5,7 +5,7 @@
|
||||
type Woot = Woot Nat Nat Nat Nat
|
||||
|
||||
toSeq : Woot -> [Nat]
|
||||
toSeq w = match w with
|
||||
toSeq = cases
|
||||
Woot a b c d -> [a,b,c,d]
|
||||
|
||||
use Woot Woot
|
||||
@ -27,5 +27,3 @@ underapply2t =
|
||||
f 4
|
||||
|
||||
> (toSeq exactt, toSeq underapply0t, toSeq underapply1t, toSeq underapply2t)
|
||||
|
||||
|
||||
|
@ -6,7 +6,7 @@ ability Zing where
|
||||
zing : Nat -> {Zing} (Nat -> Nat)
|
||||
zing2 : Nat -> Nat ->{Zing} (Nat -> Nat -> [Nat])
|
||||
|
||||
unzing z = match z with
|
||||
unzing = cases
|
||||
{a} -> a
|
||||
{Zing.zing n -> k} -> handle k (x -> x `drop` n) with unzing
|
||||
{Zing.zing2 n1 n2 -> k} -> handle k (n3 n4 -> [n1, n2, n3, n4]) with unzing
|
||||
|
@ -7,15 +7,15 @@ pat1 x y p = match p with x0 -> (x0, x, y, p)
|
||||
|
||||
pat2 x y p = match p with _ -> (x, y, p)
|
||||
|
||||
pat3 x y p = match p with (x, y) -> (y, x)
|
||||
pat3 x y = cases (x, y) -> (y, x)
|
||||
|
||||
pat4 x y p = match p with (p1, _) -> (x, y, p1)
|
||||
pat4 x y = cases (p1, _) -> (x, y, p1)
|
||||
|
||||
pat5 x y p = match p with (_, p2) -> (x, y, p2)
|
||||
pat5 x y = cases (_, p2) -> (x, y, p2)
|
||||
|
||||
pat6 x y p = match p with (p1, _) -> (x + y : Nat, p1)
|
||||
pat6 x y = cases (p1, _) -> (x + y : Nat, p1)
|
||||
|
||||
pat7 x y p = match p with
|
||||
pat7 x y = cases
|
||||
(p1, _) | p1 == 9 -> (x + y : Nat, p1)
|
||||
(p1, _) | true -> (0, p1)
|
||||
|
||||
@ -26,4 +26,3 @@ pat7 x y p = match p with
|
||||
pat5 0 1 (3, 2),
|
||||
pat6 1 2 (3, 4),
|
||||
pat7 1 2 (20, 10))
|
||||
|
||||
|
@ -8,7 +8,7 @@ ability Console where
|
||||
|
||||
namespace Console where
|
||||
state : s -> Request (State s) a -> a
|
||||
state s c = match c with
|
||||
state s = cases
|
||||
{State.get -> k} -> handle k s with state s
|
||||
{State.set s' -> k} -> handle k () with state s'
|
||||
{a} -> a
|
||||
|
@ -1,60 +1,60 @@
|
||||
use Optional None Some
|
||||
|
||||
optionToList : Optional a -> [a]
|
||||
optionToList o = match o with
|
||||
optionToList = cases
|
||||
Some a -> [a]
|
||||
None -> []
|
||||
|
||||
lenLit : [a] -> Nat
|
||||
lenLit l = match l with
|
||||
lenLit = cases
|
||||
[] -> 0
|
||||
[_] -> 1
|
||||
[_, _] -> 2
|
||||
[_, _, _] -> 3
|
||||
|
||||
lenCons : [a] -> Nat
|
||||
lenCons l = match l with
|
||||
lenCons = cases
|
||||
[] -> 0
|
||||
_ +: t -> 1 + lenCons t
|
||||
_ +: (_ +: t) -> 2 + lenCons t
|
||||
|
||||
lenSnoc : [a] -> Nat
|
||||
lenSnoc l = match l with
|
||||
lenSnoc = cases
|
||||
[] -> 0
|
||||
t :+ _ -> 1 + lenSnoc t
|
||||
|
||||
lenConcat1 : [a] -> Nat
|
||||
lenConcat1 l = match l with
|
||||
lenConcat1 = cases
|
||||
[] -> 0
|
||||
[_] ++ tail -> 1 + lenConcat1 tail
|
||||
|
||||
lenConcat2 : [a] -> Nat
|
||||
lenConcat2 l = match l with
|
||||
lenConcat2 = cases
|
||||
[] -> 0
|
||||
prefix ++ [_] -> 1 + lenConcat2 prefix
|
||||
|
||||
head : [a] -> Optional a
|
||||
head l = match l with
|
||||
head = cases
|
||||
h +: _ -> Some h
|
||||
_ -> None
|
||||
|
||||
firstTwo : [a] -> Optional (a, a)
|
||||
firstTwo l = match l with
|
||||
firstTwo = cases
|
||||
x +: (y +: _) -> Some (x, y)
|
||||
_ -> None
|
||||
|
||||
lastTwo : [a] -> Optional (a, a)
|
||||
lastTwo l = match l with
|
||||
lastTwo = cases
|
||||
_ :+ x :+ y -> Some (x, y)
|
||||
_ -> None
|
||||
|
||||
middle : [a] -> Optional [a]
|
||||
middle l = match l with
|
||||
middle = cases
|
||||
[_] ++ m ++ [_] -> Some m
|
||||
_ -> None
|
||||
|
||||
middleNel : [a] -> Optional (a, [a])
|
||||
middleNel l = match l with
|
||||
middleNel = cases
|
||||
[_] ++ (h +: t) ++ [_] -> Some (h, t)
|
||||
_ -> None
|
||||
|
||||
|
@ -23,13 +23,13 @@ w = match Foo3.Foo3 1 2 "bye" with
|
||||
Foo3.Foo3 1 2 x -> x Text.++ "bye"
|
||||
_ -> ""
|
||||
|
||||
w2 foo = match foo with
|
||||
w2 = cases
|
||||
Foo3.Foo3 1 4 x -> x Text.++ "bye"
|
||||
Foo3.Foo3 x y z -> z Text.++ z
|
||||
_ -> "hi"
|
||||
|
||||
len : List a -> Nat
|
||||
len l = match l with
|
||||
len = cases
|
||||
List.Nil -> 0
|
||||
List.Cons _ t -> len t + 1
|
||||
|
||||
|
@ -2,7 +2,7 @@ type Value = String Text
|
||||
| Bool Boolean
|
||||
|
||||
f : Value -> Nat
|
||||
f v = match v with
|
||||
f = cases
|
||||
Value.Bool true -> 3
|
||||
_ -> 4
|
||||
|
||||
|
@ -1,5 +1,3 @@
|
||||
r4 : Int -> Int
|
||||
r4 x = match x with
|
||||
r4 = cases
|
||||
+1 -> +1
|
||||
|
||||
|
||||
|
@ -1,5 +1,5 @@
|
||||
type X a = X [a]
|
||||
|
||||
f : X a -> a
|
||||
f x = match x with
|
||||
f = cases
|
||||
X.X [b] -> b
|
||||
|
@ -20,7 +20,7 @@ ability Remote where
|
||||
type Node = Node Nat -- more realistic would be perhaps a (Hostname, PublicKey) pair
|
||||
|
||||
force : Future a ->{Remote} a
|
||||
force f = match f with Future.Future r -> !r
|
||||
force = cases Future.Future r -> !r
|
||||
|
||||
-- Let's test out this beast! do we need to deploy our code to some EC2 instances??
|
||||
-- Gak, no not yet, we just want to test locally, let's write a handler
|
||||
@ -29,7 +29,7 @@ force f = match f with Future.Future r -> !r
|
||||
Remote.runLocal : '{Remote} a -> a
|
||||
Remote.runLocal r =
|
||||
use Future Future
|
||||
step nid r = match r with
|
||||
step nid = cases
|
||||
{a} -> a
|
||||
{Remote.fork t -> k} -> handle k (Future t) with step nid
|
||||
{Remote.spawn -> k} -> handle k nid with step (Node.increment nid)
|
||||
@ -52,10 +52,10 @@ List.map f as =
|
||||
|
||||
type Monoid a = Monoid (a -> a -> a) a
|
||||
|
||||
Monoid.zero m = match m with Monoid.Monoid op z -> z
|
||||
Monoid.op m = match m with Monoid.Monoid op z -> op
|
||||
Monoid.zero = cases Monoid.Monoid op z -> z
|
||||
Monoid.op = cases Monoid.Monoid op z -> op
|
||||
|
||||
Monoid.orElse m a = match a with
|
||||
Monoid.orElse m = cases
|
||||
None -> Monoid.zero m
|
||||
Some a -> a
|
||||
|
||||
|
@ -4,7 +4,7 @@ ability State se2 where
|
||||
get : ∀ se . () -> {State se} se
|
||||
|
||||
-- state : ∀ s a . s -> Request (State s) a -> (s, a)
|
||||
state woot eff = match eff with
|
||||
state woot = cases
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ State.get () -> k } -> handle k woot with state woot
|
||||
{ a } -> (woot, a)
|
||||
|
@ -3,10 +3,9 @@ ability State se2 where
|
||||
put : ∀ se . se -> {State se} ()
|
||||
get : ∀ se . () -> {State se} se
|
||||
state : ∀ s a . s -> Request (State s) a -> (s, a)
|
||||
state woot eff = match eff with
|
||||
state woot = cases
|
||||
{ State.get () -> k } -> handle k woot with state woot
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> (woot, a)
|
||||
|
||||
> ()
|
||||
|
||||
|
@ -3,7 +3,7 @@ ability State s where
|
||||
put : s -> {State s} ()
|
||||
|
||||
state : s -> Request (State s) a -> a
|
||||
state s eff = match eff with
|
||||
state s = cases
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> a
|
||||
|
||||
|
@ -7,7 +7,7 @@ ability State s where
|
||||
get : {State s} s
|
||||
|
||||
state : s -> Request (State s) a -> (s, a)
|
||||
state s eff = match eff with
|
||||
state s = cases
|
||||
{ State.get -> k } -> handle k s with state s
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> (s, a)
|
||||
@ -22,10 +22,10 @@ increment : '{State Nat} ()
|
||||
increment = '(modify ((+) 1))
|
||||
|
||||
second : (a, b) -> b
|
||||
second p = match p with (_,b) -> b
|
||||
second = cases (_,b) -> b
|
||||
|
||||
first : (a, b) -> a
|
||||
first p = match p with (a,_) -> a
|
||||
first = cases (a,_) -> a
|
||||
|
||||
ex : Text
|
||||
ex =
|
||||
|
@ -7,7 +7,7 @@ ability State s where
|
||||
get : {State s} s
|
||||
|
||||
state : s -> Request (State s) a -> (s, a)
|
||||
state s eff = match eff with
|
||||
state s = cases
|
||||
{ State.get -> k } -> handle (state s) in k s
|
||||
{ State.put snew -> k } -> handle (state snew) in k ()
|
||||
{ a } -> (s, a)
|
||||
@ -28,4 +28,3 @@ they can't bind to the universals nor does that really make sense
|
||||
|
||||
would need some nondeterminism or multiple phases in the typechecking process to
|
||||
do better
|
||||
|
||||
|
@ -3,7 +3,7 @@ ability State s where
|
||||
put : s -> {State s} ()
|
||||
|
||||
state : s -> Request (State s) a -> s
|
||||
state s eff = match eff with
|
||||
state s = cases
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> s
|
||||
|
||||
|
@ -7,7 +7,7 @@ ability State s where
|
||||
get : {State s} s
|
||||
|
||||
state : s -> Request (State s) a -> (s, a)
|
||||
state s eff = match eff with
|
||||
state s = cases
|
||||
{ State.get -> k } -> handle k s with state s
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> (s, a)
|
||||
@ -19,10 +19,10 @@ increment : '{State Nat} ()
|
||||
increment = '(modify ((+) 1))
|
||||
|
||||
second : (a, b) -> b
|
||||
second p = match p with (_,b) -> b
|
||||
second = cases (_,b) -> b
|
||||
|
||||
first : (a, b) -> a
|
||||
first p = match p with (a,_) -> a
|
||||
first = cases (a,_) -> a
|
||||
|
||||
ex : Nat
|
||||
ex =
|
||||
|
@ -4,7 +4,7 @@ ability State se2 where
|
||||
get : ∀ se . () -> {State se} se
|
||||
|
||||
state : ∀ s a . s -> Request (State s) a -> (s, a)
|
||||
state woot eff = match eff with
|
||||
state woot = cases
|
||||
{ State.get () -> k } -> handle k woot with state woot
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> (woot, a)
|
||||
|
@ -3,7 +3,7 @@ ability State s where
|
||||
get : {State s} s
|
||||
|
||||
state : s -> Request (State s) a -> s
|
||||
state s eff = match eff with
|
||||
state s = cases
|
||||
{ State.get -> k } -> handle k s with state s
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> s
|
||||
|
@ -3,7 +3,7 @@ ability State s where
|
||||
get : {State s} s
|
||||
|
||||
state : s -> Request (State s) a -> s
|
||||
state s eff = match eff with
|
||||
state s = cases
|
||||
{ State.get -> k } -> handle k s with state s
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> s
|
||||
|
@ -18,9 +18,9 @@ namespace Stream where
|
||||
Stream '(step s)
|
||||
|
||||
run : Stream e a r ->{e, Emit a} r
|
||||
run s = match s with Stream c -> !c
|
||||
run = cases Stream c -> !c
|
||||
|
||||
run' s = match s with Stream s -> s
|
||||
run' = cases Stream s -> s
|
||||
|
||||
(++) : Stream {e} a r -> Stream {e} a r -> Stream {e} a r
|
||||
s1 ++ s2 = Stream '(forceBoth (run' s1) (run' s2))
|
||||
@ -30,7 +30,7 @@ namespace Stream where
|
||||
|
||||
-- take : Nat -> Stream {} a () -> Stream {} a ()
|
||||
take n s =
|
||||
step n e = match e with
|
||||
step n = cases
|
||||
{Emit.emit a -> k} ->
|
||||
if n Nat.== 0 then ()
|
||||
else
|
||||
@ -41,7 +41,7 @@ namespace Stream where
|
||||
|
||||
-- map : (a -> b) -> Stream {e} a r -> Stream {e} b r
|
||||
map f s =
|
||||
step e = match e with
|
||||
step = cases
|
||||
{r} -> r
|
||||
{Emit.emit a -> k} ->
|
||||
Emit.emit (f a)
|
||||
@ -50,7 +50,7 @@ namespace Stream where
|
||||
|
||||
-- toSeq : Stream {e} a r ->{e} [a]
|
||||
toSeq s =
|
||||
step acc e = match e with
|
||||
step acc = cases
|
||||
{Emit.emit a -> k} -> handle k () with step (acc `snoc` a)
|
||||
{_} -> acc
|
||||
handle run s with step []
|
||||
@ -70,4 +70,3 @@ namespace Stream where
|
||||
forceBoth a b =
|
||||
!a
|
||||
!b
|
||||
|
||||
|
@ -12,7 +12,7 @@ namespace Stream where
|
||||
step :
|
||||
(a ->{e} b) ->
|
||||
Request {Emit a} r ->{e, Emit b} r
|
||||
step f e = match e with
|
||||
step f = cases
|
||||
{r} -> r
|
||||
{Emit.emit a -> k} ->
|
||||
Emit.emit (f a)
|
||||
@ -25,13 +25,13 @@ namespace Stream where
|
||||
map f s = Stream ' handle step f in run s
|
||||
|
||||
run : Stream e a r ->{e, Emit a} r
|
||||
run s = match s with Stream c -> !c
|
||||
run = cases Stream c -> !c
|
||||
|
||||
---
|
||||
-- run' s = match s with Stream s -> s
|
||||
-- run' = cases Stream s -> s
|
||||
-- unfold : s -> (s ->{} Optional (a, s)) -> Stream e a ()
|
||||
unfold s f =
|
||||
step s = match f s with
|
||||
step = cases
|
||||
None -> ()
|
||||
Some (a, s) -> emit a
|
||||
step s
|
||||
@ -46,7 +46,7 @@ namespace Stream where
|
||||
|
||||
-- take : Nat -> Stream {} a () -> Stream {} a ()
|
||||
take n s =
|
||||
step n e = match e with
|
||||
step n = cases
|
||||
{Emit.emit a -> k} ->
|
||||
if n Nat.== 0 then ()
|
||||
else
|
||||
@ -59,7 +59,7 @@ namespace Stream where
|
||||
---
|
||||
-- toSeq : Stream {e} a r ->{e} [a]
|
||||
toSeq s =
|
||||
step acc e = match e with
|
||||
step acc = cases
|
||||
{Emit.emit a -> k} -> handle step (acc `snoc` a) in k ()
|
||||
{_} -> acc
|
||||
handle step [] in run s
|
||||
@ -79,4 +79,3 @@ namespace Stream where
|
||||
a !! b =
|
||||
!a
|
||||
!b
|
||||
|
||||
|
@ -12,7 +12,7 @@ namespace Stream where
|
||||
step :
|
||||
(a ->{e} b) ->
|
||||
Request {Emit a} r ->{e, Emit b} r
|
||||
step f e = match e with
|
||||
step f = cases
|
||||
{r} -> r
|
||||
{Emit.emit a -> k} ->
|
||||
Emit.emit (f a)
|
||||
@ -28,7 +28,7 @@ namespace Stream where
|
||||
|
||||
-- 1. inferred type of `map` required an `o -> o` for some reason
|
||||
map1 f s =
|
||||
step f e = match e with
|
||||
step f = cases
|
||||
{r} -> r
|
||||
{Emit.emit a -> k} ->
|
||||
Emit.emit (f a)
|
||||
@ -40,7 +40,7 @@ namespace Stream where
|
||||
step :
|
||||
(a ->{e} b) ->
|
||||
Request {Emit a} r ->{e, Emit b} r
|
||||
step f e = match e with
|
||||
step f = cases
|
||||
{r} -> r
|
||||
{Emit.emit a -> k} ->
|
||||
Emit.emit (f a)
|
||||
@ -48,7 +48,7 @@ namespace Stream where
|
||||
Stream ' handle step f in run s
|
||||
|
||||
run : Stream e a r ->{e, Emit a} r
|
||||
run s = match s with Stream c -> !c
|
||||
run = cases Stream c -> !c
|
||||
|
||||
ability Abort where
|
||||
abort : {Abort} a
|
||||
|
@ -7,12 +7,12 @@ foo : Int
|
||||
foo = +1
|
||||
|
||||
-- no imports needed here, even though FQNs are builtin.Optional.{None,Some}
|
||||
ex1 o = match o with
|
||||
ex1 = cases
|
||||
None -> 0
|
||||
Some a -> a + 1
|
||||
|
||||
-- you can still use the
|
||||
ex2 o = match o with
|
||||
ex2 = cases
|
||||
Optional.None -> 99
|
||||
Optional.Some _ -> 0
|
||||
|
||||
|
@ -1,4 +1,4 @@
|
||||
foo x = match x with
|
||||
foo = cases
|
||||
"xyz" -> false
|
||||
"abc" -> true
|
||||
_ -> false
|
||||
|
@ -5,7 +5,7 @@ ability Foo where
|
||||
type Wrap a = Wrap Nat
|
||||
|
||||
blah : Wrap {Foo} -> Nat
|
||||
blah w = match w with
|
||||
blah = cases
|
||||
Wrap.Wrap n -> n + 1
|
||||
|
||||
> blah (Wrap 99)
|
||||
|
@ -2,7 +2,7 @@ The same kind of thing happens with `map`. Are we saying this is incorrect behav
|
||||
|
||||
```unison
|
||||
map : (a -> b) -> [a] -> [b]
|
||||
map f xs = match xs with
|
||||
map f = cases
|
||||
x +: xs -> f x +: map f xs
|
||||
[] -> []
|
||||
```
|
||||
@ -31,12 +31,11 @@ map f xs = match xs with
|
||||
.> view map
|
||||
|
||||
map : (a -> b) -> [a] -> [b]
|
||||
map f xs =
|
||||
match xs with
|
||||
x +: xs ->
|
||||
use builtin.List +:
|
||||
f x +: map f xs
|
||||
[] -> []
|
||||
map f = cases
|
||||
x +: xs ->
|
||||
use builtin.List +:
|
||||
f x +: map f xs
|
||||
[] -> []
|
||||
|
||||
.> find map
|
||||
|
||||
|
@ -12,7 +12,7 @@ foo.bar.a : Int
|
||||
foo.bar.a = +99
|
||||
|
||||
-- No imports needed even though FQN is `builtin.Optional.{None,Some}`
|
||||
optional.isNone o = match o with
|
||||
optional.isNone = cases
|
||||
None -> true
|
||||
Some _ -> false
|
||||
```
|
||||
|
@ -8,7 +8,7 @@ foo.bar.a : Int
|
||||
foo.bar.a = +99
|
||||
|
||||
-- No imports needed even though FQN is `builtin.Optional.{None,Some}`
|
||||
optional.isNone o = match o with
|
||||
optional.isNone = cases
|
||||
None -> true
|
||||
Some _ -> false
|
||||
```
|
||||
@ -18,12 +18,12 @@ optional.isNone o = match o with
|
||||
I found and typechecked these definitions in scratch.u. If you
|
||||
do an `add` or `update`, here's how your codebase would
|
||||
change:
|
||||
|
||||
|
||||
⍟ These new definitions are ok to `add`:
|
||||
|
||||
|
||||
foo.bar.a : Int
|
||||
optional.isNone : Optional a -> Boolean
|
||||
|
||||
|
||||
Now evaluating any watch expressions (lines starting with
|
||||
`>`)... Ctrl+C cancels.
|
||||
|
||||
@ -36,7 +36,7 @@ This also affects commands like find. Notice lack of qualified names in output:
|
||||
1. builtin.Bytes.take : Nat -> Bytes -> Bytes
|
||||
2. builtin.List.take : Nat -> [a] -> [a]
|
||||
3. builtin.Text.take : Nat -> Text -> Text
|
||||
|
||||
|
||||
|
||||
```
|
||||
In the signature, we don't see `base.Nat`, just `Nat`. The full declaration name is still shown for each search result though.
|
||||
@ -48,6 +48,6 @@ Type-based search also benefits from this, we can just say `Nat` rather than `.b
|
||||
|
||||
1. builtin.List.drop : Nat -> [a] -> [a]
|
||||
2. builtin.List.take : Nat -> [a] -> [a]
|
||||
|
||||
|
||||
|
||||
```
|
||||
|
Loading…
Reference in New Issue
Block a user