Merge pull request #2191 from BlockScope/remove/namespace-files-2819

Delete 9 files with namespace blocks.
This commit is contained in:
mergify[bot] 2021-07-12 18:57:06 +00:00 committed by GitHub
commit cd77bcdfcd
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 0 additions and 637 deletions

View File

@ -1,20 +0,0 @@
type Cofree f a = Cofree a (f (Cofree f a))
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 = match fn with
Functor map -> map f
use Cofree Cofree
namespace Cofree where
extract : Cofree f a -> a
extract = cases
Cofree a _ -> a
duplicate : Functor f -> Cofree f a -> Cofree f (Cofree f a)
duplicate f c = match c with
Cofree a p -> Cofree c (fmap f (duplicate f) p)

View File

@ -1,263 +0,0 @@
use Test Success Status Report Test Scope
use Test.Status Failed Expected Unexpected Pending
use Test.Success Passed Proved
use Test.Report Report
use Test.Test Test
use Test passed proved failed expected unexpected pending finished label
use Test.Scope Scope
use List flatMap
type Test.Success = Passed Nat | Proved
type Test.Status = Failed
| Expected Test.Success
| Unexpected Test.Success
| Pending
-- Current scope together with accumulated test report.
type Test.Report = Report (Trie Text Test.Status)
type Test.Test = Test (Test.Scope -> Test.Report)
unique type Test.Scope = Scope [Text]
foldSuccess : (Nat -> r) -> r -> Success -> r
foldSuccess passed proved = cases
Passed n -> passed n
Proved -> proved
foldStatus : r -> (Success -> r) -> (Success -> r) -> r -> Status -> r
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 = 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 (Report . foldScope (sc -> Trie.singleton sc st))
Test.failed : Test
Test.failed = finished Failed
Test.proved : Test
Test.proved = finished <| Expected Proved
Test.passed : Test
Test.passed = finished . Expected <| Passed 1
Test.passedUnexpectedly : Test
Test.passedUnexpectedly = finished . Unexpected <| Passed 1
Test.provedUnexpectedly : Test
Test.provedUnexpectedly = finished <| Unexpected Proved
-- Basic test combinators
Test.modifyStatus : (Status -> Status) -> Test -> Test
Test.modifyStatus f =
cases Test k -> Test (foldReport (Report . map f) . k)
Test.label : Text -> Test -> Test
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 = match (a,b) with
(Test k1, Test k2) ->
Test (
scope ->
let r1 = k1 scope
r2 = k2 scope
combine r1 r2)
Test.passedWith : Text -> Test
Test.passedWith m = label m passed
Test.provedWith : Text -> Test
Test.provedWith m = label m proved
Test.failedWith : Text -> Test
Test.failedWith m = Test.label m Test.failed
-- Report combinators
Test.Report.combine : Report -> Report -> Report
Test.Report.combine r1 r2 = match (r1, r2) with
(Test.Report.Report t1, Test.Report.Report t2) ->
Report <| Trie.unionWith Status.combine t1 t2
Test.Report.empty : Report
Test.Report.empty = Report empty
Test.Report.toCLIResult : Report -> [Test.Result]
Test.Report.toCLIResult r =
descend scope = cases (k, t) ->
go ((if scope != "" then (scope ++ ".") else "") ++ k) t
convert : Text -> Test.Status -> Test.Result
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 =
rest = flatMap (descend scope) (Map.toList (tail t))
match head t with
Optional.Some status ->
cons (convert scope status) rest
Optional.None -> rest
match r with Test.Report.Report t -> go "" t
Test.report : Test -> Report
Test.report = cases Test k -> k (Scope [])
-- Running tests
Test.run : Test -> [Test.Result]
Test.run = Test.Report.toCLIResult . Test.report
Test.runAll : [Test] -> [Test.Result]
Test.runAll = flatMap Test.run
-- Status combinators
Status.combine : Test.Status -> Test.Status -> Test.Status
Status.combine s1 s2 = match (s1, s2) with
(_, Pending) -> Pending
(Pending, _) -> Pending
(Failed, _) -> Failed
(_, Failed) -> Failed
(Unexpected a, Unexpected b) -> Unexpected (Success.combine a b)
(Unexpected a, _) -> Unexpected a
(_, Unexpected b) -> Unexpected b
(Expected a, Expected b) -> Expected (Success.combine a b)
Status.pending : Test.Status -> Test.Status
Status.pending = cases
Failed -> Pending
Expected s -> Unexpected s
Unexpected s -> Pending
Pending -> Pending
-- Make a test pending
Test.pending : Test -> Test
Test.pending = modifyStatus Status.pending
Test.modifyScope : (Scope -> Scope) -> Test -> Test
Test.modifyScope f = cases Test k -> Test (k . f)
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
(Proved, Proved) -> Proved
-- Test case generation
-- A domain is either small, in which case we can exhaustively list all the
-- values in the domain, or it's large, in which case we can ask for a value
-- of a particular size.
type Domain a = Small [a] | Large (Weighted a)
-- The domain of natural numbers is large.
Domain.nats : Domain Nat
Domain.nats = Large Weighted.nats
-- The domain of all integers
Domain.ints : Domain Int
Domain.ints = let
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
[+0, +1, -1, maxInt, minInt] <|> go +2)
use Universal == < >
namespace Domain where
-- The threshold of "small" domains.
smallSize = 10000
-- The Boolean domain is small
boolean : Domain Boolean
boolean = Small [false, true]
-- The domain of lists of arbitrary data is large
listsOf : Domain a -> Domain [a]
listsOf d =
Large (Weighted.lists match d with
Domain.Small as -> Weighted.fromList as
Domain.Large w -> w)
lists : Domain [()]
lists = Domain.listsOf (Small [()])
sample : Nat -> Domain a -> [a]
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 = cases
Domain.Large w -> Domain.Large (Weighted.map f w)
Domain.Small as -> Domain.Small (List.map f as)
pairs : Domain a -> Domain (a,a)
pairs d = lift2 (a b -> (a,b)) d d
tuples : Domain a -> Domain b -> Domain (Pair a b)
tuples = lift2 (a b -> Pair a b)
lift2 : (a -> b -> c) -> Domain a -> Domain b -> Domain c
lift2 f da db = let
wa = weighted da
wb = weighted db
wc = mergeWith (a1 a2 -> f a1 a2) wa wb
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 = 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 =
List.map (
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 <|
match domain with
Domain.Small xs -> check (take maxSize xs) Proved
Domain.Large _ -> check (sample maxSize domain) (Passed 1)
Test.check' : Boolean -> Test
Test.check' b = if b then Test.proved else Test.failed
Test.forAll : Nat -> Domain a -> (a -> Boolean) -> [Test.Result]
Test.forAll n d p = Test.run (Test.forAll' n d p)
Test.check : Boolean -> [Test.Result]
Test.check = Test.run . Test.check'

View File

@ -1,39 +0,0 @@
type Trie k v = { head : Optional v, tail : Map k (Trie k v) }
namespace Trie where
empty : Trie k v
empty = Trie None Map.empty
lookup : [k] -> Trie k v -> Optional v
lookup path t = match path with
[] -> Trie.head t
p +: ps -> flatMap (lookup ps) (Map.lookup p (Trie.tail t))
unionWith : (v -> v -> v) -> Trie k v -> Trie k v -> Trie k v
unionWith f t1 t2 =
h1 = Trie.head t1
h2 = Trie.head t2
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
Trie.union = Trie.unionWith const
Trie.insert : [k] -> v -> Trie k v -> Trie k v
Trie.insert path v t =
Trie.unionWith const (Trie.singleton path v) t
Trie.singleton : [k] -> v -> Trie k v
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
Trie.map : (v1 -> v2) -> Trie k v1 -> Trie k v2
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)))

View File

@ -1,69 +0,0 @@
-- A data structure that allows giving computations weight such that the
-- lowest-cost computation will be returned first. Allows searching
-- infinite spaces productively.
--
-- Adapted from http://hackage.haskell.org/package/weighted-search-0.1.0.1
use Universal == < >
type Weighted a
= Fail
| Yield a (Weighted a)
| Weight Nat (() -> Weighted a)
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 = cases
Weighted.Fail -> Weighted.Fail
Weighted.Yield x w -> Yield (f x) (map f w)
Weighted.Weight a w -> weight a '(map f !w)
yield : a -> Weighted a
yield a = Yield a Fail
flatMap : (a -> Weighted b) -> Weighted a -> Weighted b
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)
mergeWith : (a -> b -> c) -> Weighted a -> Weighted b -> Weighted c
mergeWith f as bs =
flatMap (a -> map (b -> f a b) bs) as
(<|>): Weighted a -> Weighted a -> Weighted a
(<|>) 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) ->
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)
else if w == w' then Weight w '(!m <|> !n)
else Weight w '(Weight (w `drop` w') m <|> !n)
sample : Nat -> Weighted a -> [a]
sample n wsa =
if n > 0 then
match wsa with
Weighted.Fail -> []
Weighted.Yield a ms -> cons a (sample (n `drop` 1) ms)
Weighted.Weight _ w -> sample n !w
else []
nats : Weighted Nat
nats = let
go n = yield n <|> weight 1 '(go (n + 1))
go 0
lists : Weighted a -> Weighted [a]
lists w = yield [] <|> weight 1 '(mergeWith cons w (lists w))
fromList : [a] -> Weighted a
fromList = cases
[] -> Weighted.Fail
a +: as -> yield a <|> weight 1 '(fromList as)

View File

@ -1,19 +0,0 @@
ability State s where
get : Nat -> {State s} s
set : s -> {State s} ()
ability Console where
read : () -> {Console} (Optional Text)
write : Text -> {Console} ()
fst = cases Tuple.Cons a _ -> a
snd = cases Tuple.Cons _ (Tuple.Cons b _) -> b
namespace Console where
simulate : Request Console a -> {State ([Text], [Text])} a
simulate = cases
{Console.read _ -> k} -> k Optional.None
Console.simulate

View File

@ -1,29 +0,0 @@
ability State s where
get : {State s} s
set : s -> {State s} ()
ability Console where
read : {Console} (Optional Text)
write : Text -> {Console} ()
fst = cases Tuple.Cons a _ -> a
snd = cases Tuple.Cons _ (Tuple.Cons b _) -> b
namespace Console where
simulate : Request Console a -> {State ([Text], [Text])} a
simulate = cases
{Console.read -> k} ->
io = State.get
ins = fst io
outs = snd io
State.set (drop 1 ins, outs)
k (at 0 ins) -- this is missing recursive call to handle
{Console.write t -> k} ->
io = State.get
ins = fst io
outs = snd io
k (State.set (ins, cons t outs)) -- this is missing recursive call
()

View File

@ -1,102 +0,0 @@
-- A simple distributed computation ability
ability Remote n where
-- Spawn a new node, of type `n`
spawn : {Remote n} n
-- Sequentially evaluate the given thunk on another node
-- then return to the current node when it completes
at : n -> '{Remote n} a -> {Remote n} a
-- Start a computation running, returning an `r` that can be forced to
-- await the result of the computation
fork : '{Remote n} a -> {Remote n} ('{Remote n} a)
type Monoid a = Monoid (a -> a -> a) a
use Nat + - * / == <
use Sequence map take drop size foldLeft halve
use Optional None Some
use Monoid.Monoid -- import the constructor
use Remote fork spawn at
namespace Monoid where
zero : Monoid a -> a
zero = cases Monoid _ z -> z
op : Monoid a -> a -> a -> a
op = cases Monoid op _ -> op
foldMap : (a -> {e} b) -> Monoid b -> [a] -> {e} b
foldMap f m as =
op = Monoid.op m
-- this line has a type error, `op` is (b -> b -> b)
-- 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 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 =
o = op m
z = zero m
-- note - does not typecheck if flip the order of the constructor!
-- the 'z has type 'a, which fails to match the later remote thunk
Monoid (a1 a2 -> parApply o a1 a2) 'z
force : '{e} a -> {e} a
force a = !a
mapReduce : (a -> {Remote n} b) -> Monoid b -> [a] -> {Remote n} b
mapReduce f m a =
force <| Monoid.foldMap (a -> fork '(f a)) (Monoid.par m) a
namespace Sequence where
foldLeft : (b -> a -> b) -> b -> [a] -> b
foldLeft f z as = _todo2
halve : [a] -> ([a], [a])
halve as = (take (size as / 2) as, drop (size as / 2) as)
ex : '{Remote n} Nat
ex = 'let
alice = spawn
bob = spawn
f1 = fork '(1 + 1)
f2 = fork '(2 + 2)
!f1 + !f2
parApply : (a -> b -> c) -> '{Remote n} a -> '{Remote n} b -> '{Remote n} c
parApply f a b = 'let
x = fork a
y = fork b
f !x !y
-- this currently crashes the compiler
Remote.runLocal : '{Remote Nat} a -> a
Remote.runLocal r =
step : Nat -> Request (Remote Nat) a -> a
step nid = cases
{a} -> a
{Remote.fork t -> k} -> handle k t with step nid
{Remote.spawn -> k} -> handle k nid with step (nid + 1)
{Remote.at _ t -> k} -> handle k !t with step (nid + 1)
handle !r with step 0
uno : '{e} a -> '{e} a -> {e} a
uno a a2 = !a
dos : (a -> a -> a) -> '{e} a -> '{e} a -> {e} a
dos f a a2 = f !a !a2
(<|) : (i -> o) -> i -> o
f <| i = f i
i |> f = f i
Stream.fromNat 1
|> Stream.take 15
|> Stream.toSequence

View File

@ -1,57 +0,0 @@
-- Token {payload = Semi, start = Pos 51 1, end = Pos 51 1} :| []
-- bootstrap: unison-src/tests/console.uu:51:1:
-- unexpected Semi
-- expecting : or the rest of infixApp
-- 51 | ()
ability State s where
get : {State s} s
set : s -> {State s} ()
ability Console where
read : {Console} (Optional Text)
write : Text -> {Console} ()
fst = cases Tuple.Cons a _ -> a
snd = cases Tuple.Cons _ (Tuple.Cons b _) -> b
namespace Console where
state : s -> Request (State s) a -> a
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 = cases
{Console.read -> k} ->
io = State.get
ins = fst io
outs = snd io
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`.
handle k (at 0 ins) with simulate
{Console.write t -> k} ->
io = State.get
ins = fst io
outs = snd io
-- same deal here
handle k (State.set (ins, cons t outs)) with simulate
{a} -> a
(++) = concatenate
handle
handle
use Console read write
use Optional Some None
write "What's your name?"
match read with
Some name -> write ("Hello" ++ name)
None -> write "Fine, be that way."
with Console.simulate
()

View File

@ -1,39 +0,0 @@
type Suit = Club | Spade | Heart | Diamond
type Card = Card Rank Suit
type Rank = A | K | Q | J | _10 | _9 | _8 | _7
type NonEmpty a = NonEmpty a [a]
use Rank A K Q J _10 _9 _8 _7
use Suit Club Spade Heart Diamond
use NonEmpty NonEmpty
use Optional Some None
namespace Suit where
all = [Club, Spade, Heart, Diamond]
namespace Rank where
all = [A, _10, K, Q, J, _9, _8, _7]
points = cases
A -> 11
_10 -> 10
K -> 4
Q -> 3
J -> 2
_ -> 0
toText = cases
A -> "A"
K -> "K"
Q -> "Q"
J -> "J"
_10 -> "10"
_9 -> "9"
_8 -> "8"
_7 -> "7"
namespace NonEmpty where
toList = cases
NonEmpty h t -> Sequence.cons h t
fromList : [a] -> Optional (NonEmpty a)
fromList l = match Sequence.at 0 l with
None -> None
Some a -> Some (NonEmpty a (Sequence.drop 1 l))