unisonweb/unison
1
0
Fork 0
mirror of https://github.com/unisonweb/unison.git synced 2024-09-11 10:35:57 +03:00
Code Issues Projects Releases Wiki Activity

restore unison-src

Browse Source
This commit is contained in:
Arya Irani 2020-10-19 10:34:23 -04:00
parent 22f07828d0
commit 8025f85d2d
394 changed files with 15902 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

444
unison-src/Base.u Normal file
View File

@ -0,0 +1,444 @@
namespace Nat where
maxNat = 18446744073709551615
(-) : Nat -> Nat -> Int
(-) = Nat.sub
namespace Int where
maxInt = +9223372036854775807
minInt = -9223372036854775808
use Universal == < > >=
use Optional None Some
-- Function composition
dot : (b -> c) -> (a -> b) -> a -> c
dot f g x = f (g x)
-- Function composition
andThen : (a -> b) -> (b -> c) -> a -> c
andThen f g x = g (f x)
const : a -> b -> a
const a _ = a
use Tuple Cons
namespace Tuple where
at1 : Tuple a b -> a
at1 = cases Cons a _ -> a
at2 : Tuple a (Tuple b c) -> b
at2 = cases Cons _ (Cons b _) -> b
at3 : Tuple a (Tuple b (Tuple c d)) -> c
at3 = cases Cons _ (Cons _ (Cons c _)) -> c
at4 : Tuple a (Tuple b (Tuple c (Tuple d e))) -> d
at4 = cases Cons _ (Cons _ (Cons _ (Cons d _))) -> d
namespace List where
map : (a -> b) -> [a] -> [b]
map f a =
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 = match (at i as, at i bs) with
(None,_) -> acc
(_,None) -> acc
(Some a, Some b) -> go (acc `snoc` (a,b)) (i + 1)
go [] 0
insert : Nat -> a -> [a] -> [a]
insert i a as = take i as ++ [a] ++ drop i as
replace : Nat -> a -> [a] -> [a]
replace i a as = take i as ++ [a] ++ drop (i + 1) as
slice : Nat -> Nat -> [a] -> [a]
slice start stopExclusive s =
take (stopExclusive `Nat.drop` start) (drop start s)
unsafeAt : Nat -> [a] -> a
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 = match List.at i as with
None -> b
Some a -> go (f b a) (i + 1)
go b 0
foldb : (a -> b) -> (b -> b -> b) -> b -> [a] -> b
foldb f op z as =
if List.size as == 0 then z
else if List.size as == 1 then f (unsafeAt 0 as)
else match halve as with (left, right) ->
foldb f op z left `op` foldb f op z right
reverse : [a] -> [a]
reverse as = foldl (acc a -> List.cons a acc) [] as
indexed : [a] -> [(a, Nat)]
indexed as = as `zip` range 0 (size as)
sortBy : (a -> b) -> [a] -> [a]
sortBy f as =
tweak p = match p with (p1,p2) -> (f p1, p2, p1)
Heap.sort (map tweak (indexed as)) |> map Tuple.at3
halve : [a] -> ([a], [a])
halve s =
n = size s / 2
(take n s, drop n s)
unfold : s -> (s -> Optional (a, s)) -> [a]
unfold s0 f =
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 = 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)
match at i as with
None -> None
Some a -> Some (take i as, a)
join : [[a]] -> [a]
join = foldl (++) []
flatMap : (a -> [b]) -> [a] -> [b]
flatMap f as = join (map f as)
range : Nat -> Nat -> [Nat]
range start stopExclusive =
f i = if i < stopExclusive then Some (i, i + 1) else None
unfold start f
distinct : [a] -> [a]
distinct as =
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)
go 0 Set.empty []
-- Joins a list of lists in a "fair diagonal" fashion.
-- Adapted from the Haskell version written by Luke Palmer.
diagonal : [[a]] -> [a]
diagonal =
let
x = 23
stripe = cases
[] -> []
[] +: xxs -> stripe xxs
(x +: xs) +: xxs -> cons [x] (zipCons xs (stripe xxs))
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)
List.join `dot` stripe
-- > List.foldb "" (t t2 -> "(" ++ t ++ " " ++ t2 ++ ")") (x -> x) ["Alice", "Bob", "Carol", "Dave", "Eve", "Frank", "Gerald", "Henry"]
-- Sorted maps, represented as a pair of sequences
-- Use binary search to do lookups and find insertion points
-- This relies on the underlying sequence having efficient
-- slicing and concatenation
type Map k v = Map [k] [v]
use Map Map
namespace Search where
indexOf : a -> [a] -> Optional Nat
indexOf a s =
ao = Some a
Search.exact (i -> ao `compare` List.at i s) 0 (size s)
lubIndexOf' : a -> Nat -> [a] -> Nat
lubIndexOf' a start s =
ao = Some a
Search.lub (i -> ao `compare` List.at i s) start (size s)
lubIndexOf : a -> [a] -> Nat
lubIndexOf a s = lubIndexOf' a 0 s
lub : (Nat -> Int) -> Nat -> Nat -> Nat
lub hit bot top =
if bot >= top then top
else
mid = (bot + top) / 2
match hit mid with
+0 -> mid
-1 -> lub hit bot mid
+1 -> lub hit (mid + 1) top
exact : (Nat -> Int) -> Nat -> Nat -> Optional Nat
exact hit bot top =
if bot >= top then None
else
mid = (bot + top) / 2
match hit mid with
+0 -> Some mid
-1 -> exact hit bot mid
+1 -> exact hit (mid + 1) top
-- > ex = [0,2,4,6,77,192,3838,12000]
-- > List.map (e -> indexOf e ex) ex
-- > lubIndexOf 193 ex
(|>) : a -> (a -> b) -> b
a |> f = f a
(<|) : (a -> b) -> a -> b
f <| a = f a
id : a -> a
id a = a
namespace Map where
empty : Map k v
empty = Map [] []
singleton : k -> v -> Map k v
singleton k v = Map [k] [v]
fromList : [(k,v)] -> Map k v
fromList kvs =
go acc i = match List.at i kvs with
None -> acc
Some (k,v) -> go (insert k v acc) (i + 1)
go empty 0
toList : Map k v -> [(k,v)]
toList m = List.zip (keys m) (values m)
size : Map k v -> Nat
size s = List.size (keys s)
lookup : k -> Map k v -> Optional v
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 cases Map ks _ -> match Search.indexOf k ks with
None -> false
_ -> true
insert : k -> v -> Map k v -> Map k v
insert k v = cases Map ks vs ->
use Search lubIndexOf
i = lubIndexOf k ks
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)
None -> Map (ks `snoc` k) (vs `snoc` v)
map : (v -> v2) -> Map k v -> Map k v2
map f m = Map (keys m) (List.map f (values m))
mapKeys : (k -> k2) -> Map k v -> Map k2 v
mapKeys f m = Map (List.map f (keys m)) (values m)
union : Map k v -> Map k v -> Map k v
union = unionWith (_ v -> v)
unionWith : (v -> v -> v) -> Map k v -> Map k v -> Map k v
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) ->
use List slice unsafeAt
use Search lubIndexOf'
if kx == ky then
go (i + 1) (j + 1)
(ko `snoc` kx)
(vo `snoc` f (unsafeAt i v1) (unsafeAt j v2))
else if kx < ky then
i' = lubIndexOf' ky i k1
go i' j (ko ++ slice i i' k1) (vo ++ slice i i' v1)
else
j' = lubIndexOf' kx j k2
go i j' (ko ++ slice j j' k2) (vo ++ slice j j' v2)
go 0 0 [] []
intersect : Map k v -> Map k v -> Map k v
intersect = intersectWith (_ v -> v)
intersectWith : (v -> v -> v2) -> Map k v -> Map k v -> Map k v2
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) ->
if kx == ky then
go (i + 1) (j + 1)
(ko `snoc` kx)
(vo `snoc` f (List.unsafeAt i v1) (List.unsafeAt j v2))
else if kx < ky then
i' = Search.lubIndexOf' ky i k1
go i' j ko vo
else
j' = Search.lubIndexOf' kx j k2
go i j' ko vo
go 0 0 [] []
keys : Map k v -> [k]
keys = cases Map ks _ -> ks
values : Map k v -> [v]
values = cases Map _ vs -> vs
namespace Multimap where
insert : k -> v -> Map k [v] -> Map k [v]
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
lookup : k -> Map k [v] -> [v]
lookup k m = Optional.orDefault [] (Map.lookup k m)
type Set a = Set (Map a ())
use Set Set
namespace Set where
empty : Set k
empty = Set Map.empty
underlying : Set k -> Map k ()
underlying = cases Set s -> s
toMap : (k -> v) -> Set k -> Map k v
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 = cases Set (Map ks _) -> ks
contains : k -> Set k -> Boolean
contains k = cases Set m -> Map.contains k m
insert : k -> Set k -> Set k
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))
size : Set k -> Nat
size s = Map.size (underlying s)
intersect : Set k -> Set k -> Set k
intersect s1 s2 = Set (Map.intersect (underlying s1) (underlying s2))
type Heap k v = Heap Nat k v [Heap k v]
use Heap Heap
namespace Heap where
singleton : k -> v -> Heap k v
singleton k v = Heap 1 k v []
size : Heap k v -> Nat
size = cases Heap n _ _ _ -> n
union : Heap k v -> Heap k v -> Heap k v
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)
pop : Heap k v -> Optional (Heap k v)
pop h =
go h subs =
use List drop size unsafeAt
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)
match List.uncons (children h) with
None -> None
Some (s0, subs) -> Some (go s0 subs)
children : Heap k v -> [Heap k v]
children = cases Heap _ _ _ cs -> cs
max : Heap k v -> (k, v)
max = cases Heap _ k v _ -> (k, v)
maxKey : Heap k v -> k
maxKey = cases Heap _ k _ _ -> k
fromList : [(k,v)] -> Optional (Heap k v)
fromList kvs =
op a b = match a with
None -> b
Some a -> match b with
None -> Some a
Some b -> Some (union a b)
single = cases
(k, v) -> Some (singleton k v)
List.foldb single op None kvs
fromKeys : [a] -> Optional (Heap a a)
fromKeys as = fromList (List.map (a -> (a,a)) as)
sortDescending : [a] -> [a]
sortDescending as =
step = cases
None -> None
Some h -> Some (max h, pop h)
List.unfold (fromKeys as) step |> List.map Tuple.at1
sort : [a] -> [a]
sort as = sortDescending as |> List.reverse
-- > sort [11,9,8,4,5,6,7,3,2,10,1]
namespace Optional where
map : (a -> b) -> Optional a -> Optional b
map f = cases
None -> None
Some a -> Some (f a)
orDefault : a -> Optional a -> a
orDefault a = cases
None -> a
Some a -> a
orElse : Optional a -> Optional a -> Optional a
orElse a b = match a with
None -> b
Some _ -> a
flatMap : (a -> Optional b) -> Optional a -> Optional b
flatMap f = cases
None -> None
Some a -> f a
map2 : (a -> b -> c) -> Optional a -> Optional b -> Optional c
map2 f oa ob = flatMap (a -> map (f a) ob) oa

20
unison-src/Cofree.u Normal file
View File

@ -0,0 +1,20 @@
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)

263
unison-src/EasyTest.u Normal file
View File

@ -0,0 +1,263 @@
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'

39
unison-src/Trie.u Normal file
View File

@ -0,0 +1,39 @@
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)))

69
unison-src/WeightedSearch.u Normal file
View File

@ -0,0 +1,69 @@
-- 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)

60
unison-src/base58.u Normal file
View File

@ -0,0 +1,60 @@
-- TODO: Characters
-- TODO: Bytes
type Optional a = Some a | None
type Words = Words (List Nat)
type Integer = Integer
Integer.zero : Integer
Integer.zero = _
shiftLeft : Nat -> Integer -> Integer
shiftLeft x y = _
(+) : Integer -> Integer -> Integer
(+) x y = _
unfoldRight : ∀ a b . (a -> Optional (a, b)) -> a -> List b
unfoldRight f z = _
foldLeft : ∀ a b . a -> (a -> b -> a) -> List b -> a
foldLeft z f s = _
toInteger : Nat -> Integer
toInteger x = _
bigEndian : Words -> Integer
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
divmod : Integer -> Nat -> (Integer, Nat)
divmod x y = _
(|>) : ∀ a b c . (a -> b) -> (b -> c) -> a -> c
(|>) g f x = f (g x)
(==) : Integer -> Nat -> Boolean
(==) a b = _
charAt : Nat -> Text -> Text
charAt n = Text.drop n |> Text.take 1
codeString : Text
codeString = "123456789ABCDEFGHJKLMNPQRSTUVWXYZabcdefghijkmnopqrstuvwxyz"
base58Encode : Words -> Text
base58Encode ws =
x = bigEndian ws
base58 : Integer -> Optional (Integer, Text)
base58 a =
if a == 0
then Optional.None
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 = _

72
unison-src/basics.u Normal file
View File

@ -0,0 +1,72 @@
-- Unison is a statically typed functional language
increment : Nat -> Nat -- signature is optional
increment n = n + 1
-- Lines starting with `>` are evaluated and printed on every file save.
> increment 99
replicate : Nat -> a -> [a]
replicate n a = toSequence (take n (constant a))
-- this is nice for quick testing!
> replicate 3 "bye"
-- can ask Unison for the type of any expression just by adding `?` to the end of it
-- > (replicate 4)?
-- here's a more interesting example, mergesort -
-- First we define the merge function, it merges two sorted lists
merge : (a -> a -> Boolean) -> [a] -> [a] -> [a]
merge lte a b =
use Sequence ++
use Optional None Some
go acc a b = match at 0 a with
None -> acc ++ b
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
else go (acc `snoc` hd2) a (drop 1 b)
go [] a b
-- let's make sure it works
> merge (<) [1,3,4,99,504,799] [0,19,22,23]
-- looks good, now let's write mergesort
sort : (a -> a -> Boolean) -> [a] -> [a]
sort lte a =
if Sequence.size a < 2 then a
else
l = sort lte (take (size a / 2) a)
r = sort lte (drop (size a / 2) a)
merge lte l r
-- let's make sure it works
> sort (<) [3,2,1,1,2,3,9182,1,2,34,1,80]
> sort (<) ["Dave", "Carol", "Eve", "Alice", "Bob", "Francis", "Hal", "Illy", "Joanna", "Greg", "Karen"]
-- SHIP IT!! 🚢
-- If you make a mistake, we try to have nice friendly error messages, not:
-- 🤖 ERROR DETECTED ⚡️ BEEP BOOP ⚡️ PLS RESUBMIT PROGRAM TO MAINFRAME
-- a few examples of failing programs -
--err1 =
-- a = "3"
-- sort (<) [1,2,a]
-- err1a = sort (<) "not a list"
--err2 : x -> y -> x
--err2 thing1 thing2 =
-- if true then thing1
-- else thing2

6
unison-src/demo/1.u Normal file
View File

@ -0,0 +1,6 @@
increment : Nat -> Nat
increment n = n + 1
> x = 1 + 40
> increment x

46
unison-src/demo/2.u Normal file
View File

@ -0,0 +1,46 @@
use Optional None Some
use Universal <
uncons : [a] -> Optional (a, [a])
uncons as = match at 0 as with
None -> None
Some hd -> Some (hd, drop 1 as)
halve : [a] -> ([a], [a])
halve s = splitAt (size s / 2) s
splitAt : Nat -> [a] -> ([a], [a])
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 = match (uncons a, uncons b) with
(None,_) -> out ++ b
(_,None) -> out ++ a
(Some (hA, tA), Some (hB, tB)) ->
if hA `lte` hB then go (out `snoc` hA) tA b
else go (out `snoc` hB) a tB
go [] a b
sort : (a -> a -> Boolean) -> [a] -> [a]
sort lte as =
if size as < 2 then as
else match halve as with (left, right) ->
l = sort lte left
r = sort lte right
merge lte l r
-- let's make sure it works
> uncons [1, 2, 3]
> sort (<) [3,2,1,1,2,3,9182,1,2,34,1,23]
> sort (<) ["Dave", "Carol", "Eve", "Alice", "Bob", "Francis", "Hal", "Illy", "Joanna", "Greg", "Karen"]
-- these programs have some type errors
-- > sort (<) [3,2,1,1,2,3,9182,1,2,34,1,"oops"]
-- > merge (<) [1,4,5,90,102] ["a", "b"]

115
unison-src/demo/3.u Normal file
View File

@ -0,0 +1,115 @@
type Future a = Future ('{Remote} a)
-- A simple distributed computation ability
ability Remote where
-- Spawn a new node
spawn : {Remote} Node
-- Start evaluating a computation on another node
at : Node -> '{Remote} a ->{Remote} Future a
type Node = Node Nat -- more realistic would be perhaps a (Hostname, PublicKey) pair
force : Future a ->{Remote} a
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
-- for the `Remote` ability that simulates everything locally!
use Future Future
use Optional None Some
use Monoid Monoid
use List ++ at
use Universal <
List.map : (a ->{e} b) -> [a] ->{e} [b]
List.map f as =
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 = cases Monoid.Monoid op z -> z
Monoid.op = cases Monoid.Monoid op z -> op
Monoid.orElse m = cases
None -> Monoid.zero m
Some a -> a
uncons : [a] -> Optional (a, [a])
uncons as = match at 0 as with
None -> None
Some hd -> Some (hd, drop 1 as)
dreduce : Monoid a -> [a] ->{Remote} a
dreduce m a =
if size a < 2 then Monoid.orElse m (List.at 0 a)
else
l = Remote.at Remote.spawn '(dreduce m (take (size a / 2) a))
r = Remote.at Remote.spawn '(dreduce m (drop (size a / 2) a))
Monoid.op m (force l) (force r)
dmapReduce : (a ->{Remote} b) -> Monoid b -> [a] ->{Remote} b
dmapReduce f m as = dreduce m (List.map f as)
dsort2 : (a -> a -> Boolean) -> [a] ->{Remote} [a]
dsort2 lte as =
dreduce (Monoid (merge lte) [])
(List.map (a -> [a]) as)
halve : [a] -> ([a], [a])
halve s = splitAt (size s / 2) s
splitAt : Nat -> [a] -> ([a], [a])
splitAt n as = (take n as, drop n as)
Node.increment : Node -> Node
Node.increment n =
use Node.Node -- the constructor
match n with Node n -> Node (n + 1)
Remote.runLocal : '{Remote} a -> a
Remote.runLocal r =
step nid = cases
{Remote.spawn -> k} -> handle k nid with step (Node.increment nid)
{Remote.at _ t -> k} -> handle k (Future t) with step nid
{a} -> a -- the pure case
handle !r with step (Node.Node 0)
merge : (a -> a -> Boolean) -> [a] -> [a] -> [a]
merge lte a b =
go out a b = match (uncons a, uncons b) with
(None,_) -> out ++ b
(_,None) -> out ++ a
(Some (hA, tA), Some (hB, tB)) ->
if hA `lte` hB then go (out `snoc` hA) tA b
else go (out `snoc` hB) a tB
go [] a b
> merge (<) [1,3,4,99,504,799] [0,19,22,23]
sort : (a -> a -> Boolean) -> [a] -> [a]
sort lte as =
if size as < 2 then as
else match halve as with (left, right) ->
l = sort lte left
r = sort lte right
merge lte l r
dsort : (a -> a -> Boolean) -> [a] ->{Remote} [a]
dsort lte as =
use Remote at spawn
if size as < 2 then as
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)
> 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])

8
unison-src/errors/407.u Normal file
View File

@ -0,0 +1,8 @@
use Universal <
foo : x -> x -> Nat
foo x y = 42
> foo "hi" 2

6
unison-src/errors/X-array.u Normal file
View File

@ -0,0 +1,6 @@
type X = S Text | I Nat
foo : a -> b -> c -> X
foo x y z = X.S ""
[foo +1 1 1.0, 1]

9
unison-src/errors/abort-ability-checks-against-pure.u Normal file
View File

@ -0,0 +1,9 @@
--Abort
ability Abort where
Abort : forall a . () -> {Abort} a
bork = u -> 1 + (Abort.Abort ())
(bork : () -> {} Nat)
-- failing to fail in commit 2819c206acf80f926c6d970a4ffd47c961fa4502

43
unison-src/errors/all-errors.u Normal file
View File

@ -0,0 +1,43 @@
type Optional a = Some a | None
ability Abort where
Abort : forall a . () -> {Abort} a
ability Abort2 where
Abort2 : forall a . () -> {Abort2} a
Abort2' : forall a . () -> {Abort2} a
app : Optional Int
app = Optional.Some 3
app' : Optional Int
app' = 3
arrow : Int -> Int -> Int
arrow a = 3
ability' : Nat -> { Abort } Int
ability' n = Abort2.Abort2 ()
id : forall a . a -> a
id x = 3
f2 : forall a . a -> a -> a
f2 x = x
const : forall a b . a -> b -> a
const a b = 3
y : (Optional Int)
y = 3
z' : (Optional Int, Optional Text, Optional Float)
z' = (None, 3)
z : (Optional Int, Optional Text, Optional Float)
z = 3
x : ()
x = 3
()

7
unison-src/errors/check-for-regressions/and.u Normal file
View File

@ -0,0 +1,7 @@
and true 3
-- InSubtype t1=Nat, t2=Boolean
-- InCheck e=3, t=Boolean
-- InSynthesizeApp t=Boolean -> Boolean, e=3, n=2
-- InAndApp
-- InSynthesize e=and true 3

4
unison-src/errors/check-for-regressions/app-polymorphic.u Normal file
View File

@ -0,0 +1,4 @@
foo : a -> a -> a -> a -> a -> a
foo a b c d e = e
foo 1 2 3 "ha" 5

4
unison-src/errors/check-for-regressions/app.u Normal file
View File

@ -0,0 +1,4 @@
foo : Nat -> Nat -> Nat -> Nat -> Nat -> Nat
foo a b c d e = a + b + c + d + e
foo 1 2 3 "ha" 5

4
unison-src/errors/check-for-regressions/applying-non-function.u Normal file
View File

@ -0,0 +1,4 @@
-- "Hello" "world"
id a = a
id 1 1

3
unison-src/errors/check-for-regressions/casebody.u Normal file
View File

@ -0,0 +1,3 @@
match 3 with
3 -> 4
4 -> "Surprise!"

2
unison-src/errors/check-for-regressions/caseguard.u Normal file
View File

@ -0,0 +1,2 @@
match 3 with
3 | 3 -> 4

3
unison-src/errors/check-for-regressions/casepattern.u Normal file
View File

@ -0,0 +1,3 @@
match 3 with
3 -> "Great!"
"Great" -> "Terrible."

1
unison-src/errors/check-for-regressions/ifcond.u Normal file
View File

@ -0,0 +1 @@
if 3 then 4 else 5

1
unison-src/errors/check-for-regressions/ifelse.u Normal file
View File

@ -0,0 +1 @@
if true then 4 else "Surprise!"

9
unison-src/errors/check-for-regressions/lens.u Normal file
View File

@ -0,0 +1,9 @@
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 = match (foo, a) with
(Foo _ b, Some a) -> Foo a b
_ -> foo
setA (Foo "hello" 3) (Some 7)

14
unison-src/errors/check-for-regressions/not-and.u Normal file
View File

@ -0,0 +1,14 @@
notid : Int -> Boolean
notid a = true
and (notid 3) true
-- InSubtype t1=Nat, t2=Int
-- InCheck e=3, t=Int
-- InSynthesizeApp t=Int -> Boolean, e=3, n=1
-- InSynthesizeApps f=notid1 ft=Int -> Boolean, es=[3]
-- InSynthesize e=notid1 3
-- InCheck e=notid1 3, t=Boolean
-- InSynthesizeApp t=Boolean -> Boolean -> Boolean, e=notid1 3, n=1
-- InAndApp
-- InSynthesize e=and notid1 3 true
-- InSynthesize e=Cycle (notid. (let r...

9
unison-src/errors/check-for-regressions/not-and0.u Normal file
View File

@ -0,0 +1,9 @@
and (3 : Boolean) true
-- InSubtype t1=Nat, t2=Boolean
-- InCheck e=3, t=Boolean
-- InSynthesize e=3:Boolean
-- InCheck e=3:Boolean, t=Boolean
-- InSynthesizeApp t=Boolean -> Boolean -> Boolean, e=3:Boolean, n=1
-- InAndApp
-- InSynthesize e=and 3:Boolean true

4
unison-src/errors/check-for-regressions/not-caseguard.u Normal file
View File

@ -0,0 +1,4 @@
notid : Int -> Boolean
notid a = true
match 3 with
3 | notid 3 -> 4

2
unison-src/errors/check-for-regressions/not-caseguard2.u Normal file
View File

@ -0,0 +1,2 @@
match 3 with
3 | (3 : Boolean) -> 4

1
unison-src/errors/check-for-regressions/not-or.u Normal file
View File

@ -0,0 +1 @@
or (3 : Boolean) true

1
unison-src/errors/check-for-regressions/not-vector.u Normal file
View File

@ -0,0 +1 @@
[1, +1 : Nat]

1
unison-src/errors/check-for-regressions/or.u Normal file
View File

@ -0,0 +1 @@
or true 3

1
unison-src/errors/check-for-regressions/vector.u Normal file
View File

@ -0,0 +1 @@
[1, +1]

5
unison-src/errors/compiler-bug.u Normal file
View File

@ -0,0 +1,5 @@
x = 1
Foo.y = 4.0
a =
x + y
()

19
unison-src/errors/console.u Normal file
View File

@ -0,0 +1,19 @@
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

29
unison-src/errors/console2.u Normal file
View File

@ -0,0 +1,29 @@
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
()

8
unison-src/errors/cyclic-unguarded.u Normal file
View File

@ -0,0 +1,8 @@
x = y + 1
y = x + 1
> x

12
unison-src/errors/effect-inference1.u Normal file
View File

@ -0,0 +1,12 @@
ability Abort where
Abort : forall a . () -> {Abort} a
foo n = if n >= 1000 then n else !Abort.Abort
bar : (Nat -> {} Nat) -> Nat -> Nat
bar f i = f i
bar foo 3
-- as of 3935b366383fe8184f96cfe714c31ca04234cf27, this typechecks (unexpected)
-- and then bombs in the runtime because the Abort ability isn't handled.

20
unison-src/errors/effect_unknown_type.uu Executable file
View File

@ -0,0 +1,20 @@
ability T where
a : Unknown -> {T} ()
--b : Unknown
--b = ()
----
unison: can't hashComponents if bindings have free variables:
["Unknown"]
["T"]
CallStack (from HasCallStack):
error, called at src/Unison/ABT.hs:504:11 in unison-parser-typechecker-0.1-I7C95FdIglBGnISbV534LW:Unison.ABT
-- Typechecker emits a helpful error about b's use of an unknown type, but not a's.
--
-- Error for b:
-- typechecker.tests/ability_unknown_type.u FAILURE I don't know about the type Unknown. Make sure it's imported and spelled correctly:
--
-- 22 | b : Unknown

1
unison-src/errors/empty-block.u Normal file
View File

@ -0,0 +1 @@
foo =

49
unison-src/errors/ex1.u Normal file
View File

@ -0,0 +1,49 @@
use Optional None Some
foo : Optional a -> [a]
foo = cases
None -> []
Some a -> [a]
"hello" `Sequence.cons` foo (Some 3)
-- Sequence.cons has type `a -> [a] -> [a]`
-- `a` was determined to be `Text` because "hello" had type `Text`.
-- Therefore `foo (Some 3)` was checked against `[Text]`
-- but it actually had type `[Nat]`. Use `> why err1` for more detail.
-- type Extractor v loc a = Note v loc -> Maybe a
-- do
-- e <- errorTerm
-- b <- isFunctionCall
-- if b then do
--
-- in reply to `> why err1`:
-- `foo` has type `Optional a -> [a]`
-- `a` was determined to be `Nat` because
-- `Some 3` has type `Optional Nat`. Use `> why err2` for more detail
-- in reply to `> why err2`:
-- `Some` has type `a -> Optional a`
-- `a` was determinewd to be `Nat` because `3` has type `Nat`
x = 3
and x 4
------------- generic synthesizeApp possibility
-- `and` has type `Boolean -> Boolean -> Boolean`
-- .. (no typevars to explain, so skip)
-- Therefore `3` was checked against `Boolean`,
-- but it actually had type `Nat`.
------------- specialized "and" possibility
-- The arguments to `and` must be of type `Boolean`,
-- but `x` has type `Nat`. Use `> why err1` for more detail.
and 3 4
-- but the literal `3` has type `Nat`.
match 3 with
3 -> "text"
4 -> 4.0

19
unison-src/errors/fix745.u Normal file
View File

@ -0,0 +1,19 @@
unique ability A where a : Nat
unique ability B where b : Nat
noGood : Nat ->{A} '{B} ()
noGood n unit =
-- The A.a should be an ability check failure, since we are in the body
-- of an arrow which only has the {B} ability set.
A.a
B.b
()
ok : Nat ->{A} '{B} ()
ok n =
-- This is okay, because the A.a is being evaluated in the body of an
-- arrow with {A}. The result of the body is another lambda which
-- is allowed {B} requests by type signature of `ok`.
A.a
'let B.b; ()

22
unison-src/errors/handle-inference.u Normal file
View File

@ -0,0 +1,22 @@
--handle inference
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 = cases
{a} -> a
{State.get _ -> k} -> handle k s with state s
{State.set s -> k} -> handle k () with state s
-- modify : ∀ s . (s -> s) -> {State s} ()
-- modify f = State.set (f (State.get()))
ex : () -> {State Nat} Nat
ex blah =
State.get() Nat.+ 42
-- note this currently succeeds, the handle block
-- gets an inferred type of ∀ a . a, it appears that
-- the existential `a` which gets instantiated for the
-- state call never gets refined, most likely due to
-- missing a subtype check in handle
y : Text
y = handle ex () with state 5
()

29
unison-src/errors/handler-coverage-checking.uu Normal file
View File

@ -0,0 +1,29 @@
--State3 ability
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 = cases
{ State.get () -> k } -> handle k woot with state woot
{ State.put snew -> k } -> handle k () with state snew
ex1 : (Nat, Nat)
ex1 = handle State.get () with state 42
ex1a : (Nat, Nat)
ex1a = handle 49 with state 42
ex1b = handle 0 with x -> 10
ex1c : Nat
ex1c = handle 0 with x -> 10
ex1d = handle 49 with state 42
ex2 = handle State.get () with state 42
ex3 : (Nat, Nat)
ex3 = ex2
()

3
unison-src/errors/id.u Normal file
View File

@ -0,0 +1,3 @@
id a = a
(id 42 : Text)

9
unison-src/errors/io-effect.u Normal file
View File

@ -0,0 +1,9 @@
--IO ability
ability IO where
launchMissiles : () -> {IO} ()
-- binding is not guarded by a lambda, it only can access
-- ambient abilities (which will be empty)
ex1 : {IO} ()
ex1 = IO.launchMissiles()
()

17
unison-src/errors/io-state1.u Normal file
View File

@ -0,0 +1,17 @@
--IO/State1 ability
ability IO where
launchMissiles : {IO} ()
ability State se2 where
put : ∀ se . se -> {State se} ()
get : ∀ se . () -> {State se} se
foo : () -> {IO} ()
foo unit =
-- inner binding can't access outer abilities unless it declares
-- them explicitly
incBy : Int -> {State Int} ()
incBy i =
launchMissiles -- not allowed
y = State.get()
State.put (y Int.+ i)
()
()

102
unison-src/errors/map-reduce.u Normal file
View File

@ -0,0 +1,102 @@
-- 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

26
unison-src/errors/map-traverse3.u Normal file
View File

@ -0,0 +1,26 @@
--map/traverse
ability Noop where
noop : a -> {Noop} a
type List a = Nil | Cons a (List a)
map : (a ->{} b) -> List a -> List b
map f = cases
List.Nil -> List.Nil
List.Cons h t -> List.Cons (f h) (map f t)
c = List.Cons
z : ∀ a . List a
z = List.Nil
ex = c 1 (c 2 (c 3 z))
pureMap : List Text
pureMap = map (a -> "hello") ex
-- this should not typecheck because map is annotated to take a pure function
zappy : '{Noop} (List Nat)
zappy = 'let map (zap -> Noop.noop (zap Nat.+ 1)) ex
pureMap

4
unison-src/errors/mismatched-braces.u Normal file
View File

@ -0,0 +1,4 @@
}
x = 3

7
unison-src/errors/need-nominal-type.uu Normal file
View File

@ -0,0 +1,7 @@
type Foo = Foo
type Bar = Bar
x : Foo
x = Bar.Bar
x

27
unison-src/errors/poor-error-message/ability-check-fail-by-calling-wrong-function.u Normal file
View File

@ -0,0 +1,27 @@
reduce2 : a -> (a -> a -> a) -> Sequence a -> a
reduce2 a0 f s = match at 0 s with
Optional.None -> a0
Optional.Some a1 -> reduce (f a0 a1) f (drop 1 s)
()
-- as of commit a48fa3b, we get the following error
--The expression at Line 18, columns 40-41 (in red below) is requesting
-- {𝛆3} abilitys, but this location only has access to
-- {}
--
-- 18 | Optional.Some a1 -> reduce (f a0 a1) f (drop 1 s)
-- ^
-- simple cause:
-- AbilityCheckFailure: ambient={} requested={𝛆3}
-- The problem is that I've accidentally called `reduce` instead of `reduce2`,
-- which TDNRs to `Stream.reduce`, which doesn't allow abilitys, and `f` isn't
-- restricted to be pure.
-- I'd like to know:
-- a) reduce is the built-in
-- Stream.reduce : a -> (a ->{} a ->{} a) -> Stream a -> a
-- b) maybe those suggestions, like did you mean reduce2 instead of reduce,
-- which would typecheck. I understand that would not be a quick fix.

57
unison-src/errors/poor-error-message/consoleh.u Normal file
View File

@ -0,0 +1,57 @@
-- 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
()

5
unison-src/errors/poor-error-message/doesnt-match-annotation.u Normal file
View File

@ -0,0 +1,5 @@
crazyTuple : a -> b -> (a,b)-- -> (a,b)
crazyTuple a b c = c
()

11
unison-src/errors/poor-error-message/function-calls.u Normal file
View File

@ -0,0 +1,11 @@
f1 : Int -> Int
f1 n = n + +1
f1 (3 Nat.+ 3)
-- idea:
-- I was expecting Int
-- vs
-- f1 was expecting Int
-- "In the call below" vs "In the call to `foo`"

16
unison-src/errors/poor-error-message/function-calls1.u Normal file
View File

@ -0,0 +1,16 @@
f1 : Int -> Int
f1 n = n + +1
f1 (3 Nat.+ 3)
-- issues:
-- - the highlight term is '3' but should be (3 + 3)
-- -
-- Paul Thought:
-- Whenever we synthesize a type, we can set the location
-- of the synthesized type to be the location of the
-- synthesized expression.
-- Arya & Runar: isn't that what we already do
-- Paul: No, we only something something when we refine an existential

19
unison-src/errors/poor-error-message/function-calls2.u Normal file
View File

@ -0,0 +1,19 @@
id : a -> a
id a = a
f1 : Int -> Int
f1 n = n + +1
f1 (id 3)
-- issues:
-- - the highlight term is '3' but should be (3 + 3)
-- -
-- Paul Thought:
-- Whenever we synthesize a type, we can set the location
-- of the synthesized type to be the location of the
-- synthesized expression.
-- Arya & Runar: isn't that what we already do
-- Paul: No, we only something something when we refine an existential

26
unison-src/errors/poor-error-message/function-calls3.u Normal file
View File

@ -0,0 +1,26 @@
-- first : a -> a -> a
-- first a b = a
id5 : a -> a -> a -> a -> a -> (a,a,a,a,a)
id5 a b c d e = (a, b, c, d, e)
-- second : a -> a -> a
-- second a b = b
id5 1 +2 3 4 5
-- (match true with
-- true -> first
-- false -> second) 1 +2
-- issues:
-- - the highlight term is '3' but should be (3 + 3)
-- -
-- Paul Thought:
-- Whenever we synthesize a type, we can set the location
-- of the synthesized type to be the location of the
-- synthesized expression.
-- Arya & Runar: isn't that what we already do
-- Paul: No, we only something something when we refine an existential

40
unison-src/errors/poor-error-message/handle.u Normal file
View File

@ -0,0 +1,40 @@
--Parsing/typechecking...
--Token {payload = Close, start = Pos 27 5, end = Pos 27 5} :| []
--bootstrap: /Users/pchiusano/work/unison/unison-src/tests/state2.u:27:5:
--unexpected Close
-- 27 | let
--
type Optional a = None | Some a
ability State s where
put : s -> {State s} ()
get : {State s} s
state : s -> Request (State s) a -> (s, a)
state woot = cases
{ State.get -> k } -> handle k woot with state woot
{ State.put snew -> k } -> handle k () with state snew
{ a } -> (woot, a)
modify : (s -> s) -> {State s} ()
modify f = State.put (f State.get)
increment : '{State Nat} ()
increment = '(modify ((+) 1))
first : (a, b) -> a
first = cases (a,_) -> a
ex : Nat
ex =
result = handle (state 0)
let
x = State.get
!increment
!increment
()
first result
()

24
unison-src/errors/poor-error-message/handler-ex.u Normal file
View File

@ -0,0 +1,24 @@
--Line 13, columns 44-46 has a type mismatch (in red below):
--
-- 13 | {Ask.ask _ -> k} -> handle k () with supply t
--
--The two types involved are:
--
-- () (an intrinsic, in blue)
-- Text (line 8, columns 30-34, in green)
--
-- 8 | supply : Text -> Request (Ask Text) a -> a
--
-- Verbiage could be improved, but also the `()` location should
-- point to line 22, the `k ()` call.
ability Ask foo where
ask : () -> {Ask a} a
supply : Text -> Request (Ask Text) a -> a
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 k () with supply t
supply

20
unison-src/errors/poor-error-message/mismatched-case-result-types.u Normal file
View File

@ -0,0 +1,20 @@
--mismatched case result types
type Optional a = None | Some a
match Optional.Some 3 with
x -> 1
y -> "boo"
-- as of 5ae98f7, produces this message:
--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
-- 5 | y -> "boo" -- "boo" is highlighted
--
-- from right here:
--
-- 4 | x -> 1 -- 1 is highlighted
-- IMO, 1 should be highlighted instead of x on line 12;
-- then lines 14-17 would be omitted.

21
unison-src/errors/poor-error-message/notaguard.u Normal file
View File

@ -0,0 +1,21 @@
-- Getting the error
--The guard expression for a case has to be Boolean, but this one is a7:
--
-- 13 | {Ask.ask -> k} -> handle k () with supply t
--
-- from right here:
--
-- 8 | supply : Text -> Request (Ask Text) a -> a
--
--
-- even though this program doesn't use guards!
ability Ask a where
ask : {Ask a} a
supply : Text -> Request (Ask Text) a -> a
supply t = cases
{a} -> "foo" -- a
{Ask.ask -> k} -> handle k () with supply t
()

17
unison-src/errors/poor-error-message/overapplied-data-constructor-loc.u Normal file
View File

@ -0,0 +1,17 @@
-- board piece
type P = X | O | E
type Board = Board P P
use Board.Board
use P O X E
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 | match Board X O X
-- ^^^^^

10
unison-src/errors/poor-error-message/pattern-case-location.u Normal file
View File

@ -0,0 +1,10 @@
-- 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 = cases
Foo.Foo -> Foo
Bar.Bar -> Foo

28
unison-src/errors/poor-error-message/pattern-matching-1.u Normal file
View File

@ -0,0 +1,28 @@
type Foo0 = Foo0
type Foo1 a = Foo1 a
type Foo2 a b = Foo2 a b
type Foo3 a b c = Foo3 a b c
use Foo0 Foo0
use Foo1 Foo1
use Foo2 Foo2
x = match Foo0 with
Foo0 -> 1
y = match Foo1 1 with
Foo1 1 -> 0
Foo1 _ -> 10
z = match Foo2 1 "hi" with
Foo2 x _ -> x
Foo2 1 _ -> 1
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`
-- should come from there, not from `x`.
_ -> ()
()

55
unison-src/errors/poor-error-message/tdnr-demo.u Normal file
View File

@ -0,0 +1,55 @@
left = take 3 (fromNat 5)
right = take 10 (fromNat 100)
sum = reduce 0 (+)
iterate : a -> Nat -> (a -> a) -> Sequence a
iterate a n f =
iterate0 a n f acc =
if n > 0 then
a' = f a
iterate0 a' (n `drop` 1) f (snoc acc a')
else acc
iterate0 a n f []
use Optional Some None
reduce : a -> (a -> a -> a) -> Sequence a -> a
reduce a0 f s = match at 0 s with
Optional.None -> a0
Optional.Some a1 -> reduce (f a0 a1) f (drop 1 s)
pseudo-Stream : Sequence Nat
pseudo-Stream = iterate 0 200 increment
left2 = take 3 (drop 3 pseudo-Stream)
right2 = take 10 (drop 99 pseudo-Stream)
sum2 = reduce 0 (+)
(sum (append left right)) == (sum2 (left2 ++ right2))
-- local definition of `reduce` for Sequence understandably breaks TDNR
-- of Stream.reduce on line 3, which makes `sum` on line 3 expect
-- `Sequence Nat`, which constrains `append` on line 26 to return
-- `Sequence Nat`, so it no longer matches `Stream Nat -> Stream Nat -> 'a`,
-- which breaks TDNR of Stream.append, resulting in the error message:
--Sorry, you hit an error we didn't make a nice message for yet.
--
--Here is a summary of the Note:
-- simple cause:
-- SolvedBlank: Resolve "append" Line 26, columns 7-13 v=_170 t=Stream Nat -> Stream Nat -> [Nat]
-- path:
-- InSynthesize e=(let reduce1 0 (UInt...
-- InSynthesize e=(let (Sequence.take:...
-- InSynthesize e=(let (Sequence.take:...
-- InSynthesize e=(let (iterate:(𝛆. (a...
-- InSynthesize e=(let (λ (a. (λ (n. (...
-- InSynthesize e=(let reduce1 0 (UInt...
-- InSynthesize e=Cycle (left. (right....
--
--
--I'm not sure what append means at Line 26, columns 7-13
--
-- 26 | (sum (append left right)) == (sum2 (left2 ++ right2))
--
--Whatever it is, it has a type that conforms to Stream Nat -> Stream Nat -> [Nat]
-- Commenting out the local definition of `reduce` mysteriously fixes TDNR of `append` for the above reasons.

25
unison-src/errors/poor-error-message/token-printing.u Normal file
View File

@ -0,0 +1,25 @@
-- board piece
type Board = Board Nat Nat Nat
use Board.Board
-- uncommenting these gives errors from NPE to array index out of bounds -1, -2
-- x = 1
-- y = 2
ex = match Board 77 88 99
with Board a b c -> c
-- yields:
-- master>
-- I was expecting an indented block following the`of` keyword
-- but instead found an outdent:
--
-- 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?
-- Expecting it to just color the token or something

8
unison-src/errors/rank2a.u Normal file
View File

@ -0,0 +1,8 @@
-- We expect this to not typecheck since a `Nat -> Nat` cannot
-- be passed where a `∀ a . a -> a` is expected.
rank2a : (Nat -> Nat) -> Nat
rank2a =
inner : (∀ a . a -> a) -> Nat
inner f = 42
inner

3
unison-src/errors/seq-concat-constant-length.u Normal file
View File

@ -0,0 +1,3 @@
test : [a] -> ([a], [a])
test l = match l with
x ++ y -> (x, y)

13
unison-src/errors/state4.u Normal file
View File

@ -0,0 +1,13 @@
--State4 ability
ability State se2 where
put : ∀ se . se -> {State se} ()
get : ∀ se . () -> {State se} se
-- binding is not guarded by a lambda, it only can access
-- ambient abilities (which will be empty)
ex1 : {State Int} ()
ex1 =
y = State.get
State.put (y Int.+ +1)
()
()

3
unison-src/errors/tdnr.u Normal file
View File

@ -0,0 +1,3 @@
foo a b = a + b
foo

1
unison-src/errors/tdnr2.u Normal file
View File

@ -0,0 +1 @@
2.0 + 4

10
unison-src/errors/tdnr3.u Normal file
View File

@ -0,0 +1,10 @@
-- + Should get resolved to Nat.+, making this fail
x : Nat
x = 42
Foo.z : Float
Foo.z = 4.0
a = x + z

9
unison-src/errors/term-functor-inspired/effect1.u Normal file
View File

@ -0,0 +1,9 @@
ability State s where
get : () -> {State s} s
set : s -> {State s} ()
x : {State Nat} Nat
x =
State.get ()
()

3
unison-src/errors/term-functor-inspired/if-body-mismatch.u Normal file
View File

@ -0,0 +1,3 @@
if true
then 1
else 1.0

1
unison-src/errors/term-functor-inspired/if-cond-not-bool.u Normal file
View File

@ -0,0 +1 @@
if "true" then 1 else 1

5
unison-src/errors/term-functor-inspired/mismatched-case-result-types.u Normal file
View File

@ -0,0 +1,5 @@
--mismatched case result types
type Optional a = None | Some a
match Optional.Some 3 with
x -> 1
y -> "boo"

15
unison-src/errors/type-apply.u Normal file
View File

@ -0,0 +1,15 @@
--Type.apply
type List a = Nil | Cons a (List a)
map : ∀ a b . (a -> b) -> List a -> List b
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!
map2 : ∀ a . a
map2 = map
c = List.Cons
z = List.Nil
ex = c 1 (c 2 (c 3 z))
pureMap : List Int -- should fail, output is a `List Text`
pureMap = map (a -> "hi") ex
()

4
unison-src/errors/type-functor-inspired/app2.u Normal file
View File

@ -0,0 +1,4 @@
type Optional a = Some a | None
app' : Optional Int
app' = 3
()

3
unison-src/errors/type-functor-inspired/arrow1.u Normal file
View File

@ -0,0 +1,3 @@
arrow : Int -> Int -> Int
arrow a = 3
()

11
unison-src/errors/type-functor-inspired/effect2.u Normal file
View File

@ -0,0 +1,11 @@
ability Abort where
Abort : forall a . () -> {Abort} a
ability Abort2 where
Abort2 : forall a . () -> {Abort2} a
Abort2' : forall a . () -> {Abort2} a
ability' : Nat -> { Abort } Int
ability' n = Abort2.Abort2 ()
()

3
unison-src/errors/type-functor-inspired/forall-arrow.u Normal file
View File

@ -0,0 +1,3 @@
id : forall a . a -> a
id x = 3
()

4
unison-src/errors/type-functor-inspired/forall-arrow2.u Normal file
View File

@ -0,0 +1,4 @@
f2 : forall a . a -> a -> a
f2 x = x
()

4
unison-src/errors/type-functor-inspired/forall-arrow3.u Normal file
View File

@ -0,0 +1,4 @@
const : forall a b . a -> b -> a
const a b = 3
()

12
unison-src/errors/type-functor-inspired/need-nonstructural-types.uu Normal file
View File

@ -0,0 +1,12 @@
ability Abort where
Abort : forall a . () -> {Abort} a
ability Abort2 where
Abort2 : forall a . () -> {Abort2} a
ability' : Nat -> { Abort } Int
ability' n = Abort2.Abort2 ()
()
-- oops, Abort and Abort2 end up being synonyms

4
unison-src/errors/type-functor-inspired/parens.u Normal file
View File

@ -0,0 +1,4 @@
type Optional a = Some a | None
y : (Optional Int)
y = 3
()

5
unison-src/errors/type-functor-inspired/subtuple.u Normal file
View File

@ -0,0 +1,5 @@
type Optional a = Some a | None
z' : (Optional Int, Optional Text, Optional Float)
z' = (None, 3)
()

4
unison-src/errors/type-functor-inspired/synthesizeApp.u Normal file
View File

@ -0,0 +1,4 @@
foo : a -> a -> Nat
foo x z = 42
foo +1 "hi"

4
unison-src/errors/type-functor-inspired/tuple.u Normal file
View File

@ -0,0 +1,4 @@
type Optional a = Some a | None
z : (Optional Int, Optional Text, Optional Float)
z = 3
()

3
unison-src/errors/type-functor-inspired/tuple2.u Normal file
View File

@ -0,0 +1,3 @@
y : (Nat, Optional Int, Text)
y = (42, 3, "")
y

3
unison-src/errors/type-functor-inspired/unit.u Normal file
View File

@ -0,0 +1,3 @@
x : ()
x = 3
()

11
unison-src/errors/unexpected-loop.u Normal file
View File

@ -0,0 +1,11 @@
--Abort
ability Abort where
Abort : forall a . () -> {Abort} a
use Nat +
bork = u -> 1 + (Abort.Abort ())
(bork : Nat)
-- fails with loop instead of with type mismatch in commit 2819c206acf80f926c6d970a4ffd47c961fa4502

6
unison-src/errors/unresolved-symbol-1.u Normal file
View File

@ -0,0 +1,6 @@
let
(|>) : a -> (a -> WHat) -> b -- unresolved symbol
a |> f = f a
Stream.fromInt -3
|> Stream.take 10
|> Stream.foldLeft +0 (Int.+)

12
unison-src/errors/unsound-cont.u Normal file
View File

@ -0,0 +1,12 @@
ability Ask a where
ask : {Ask a} a
supply : Text -> Request (Ask Text) a -> a
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 k () with supply t
()

181
unison-src/example-errors.u Normal file
View File

@ -0,0 +1,181 @@
-- Each of the programs in this file generates an error of some sort.
-- We want error messages to be awesome so for each wrong program we
-- give "the ideal error message" and a uniform, simple algorithm for producing
-- that message.
ex1 : Int
ex1 = "hello"
{- Ideal error:
Type mismatch in example-errors.u, line 6: `Text` vs `Int`
|
6 | ex1 = "hello"
| ^^^^^^^
`Text` comes from a literal:
|
6 | ex1 = "hello"
| ^^^^^^^
`Int` comes from type signature:
|
5 | ex1 : Int
| ^^^^^
Thoughts:
* The first line marker is the _site of the error_
* The next two line markers are the _provenance of the mismatched types_
* In this case, the provenance of `Text` is the same location as the error,
but this won't always be the case. Optimized message just omits the
site of the error if it matches the provenance location of either of
the mismatched types.
* The backticks might be in color, formatted as bold, whatever, be
thoughtful about using visual indicators to draw attention to most important
aspects of the message.
* For implementation - when `check e t` hits `Term.Text'`, it does:
`subtype Type.text t`, but `Type.text` requires a `loc`, and we'll provide
`ABT.annotation e`. This logic can go in synthesize.
* Q: should we just ALWAYS set the location of a synthesized type
to be the location of the term that type was synthesized from?
* A: No,
foo : Text
foo x =
y = x + 1
x
In this example, x will synthesize to the type `Int`, but the location
of that type shouldn't just be
* When you synthesize a type for a lambda, `x -> x`
the location of the synthesized type `∀ a . a -> a`
is just the location of `x -> x`.
The location of the `a` also needs to be this same location.
Might want to have a special kind of location which indicates
that the location came from an inferred type.
-}
ex2 : Int -- `Int` comes from
ex2 =
y = "hello" -- `Text` comes from "hello"
y
{- Ideal error:
example-errors.u contained errors:
The highlighted expression on line 42
|
42 | y
| ^
was inferred to have type `Text` but was expected to have type `Int`
`Int` comes from type signature:
|
39 | ex2 : Int
| ^^^^^
`Text` was inferred from a literal:
|
41 | y = "hello"
| ^^^^^^^
Thoughts:
* `y` is the body of the block, and the body of the block is expected to
have type `Int`
* Maybe use bold or some visual indicator rather than the ^^^ nonsense
* Do we include parent scopes?
-}
ex3 =
x = 1 + 1
if x then 42 else "hkjh"
{-
example-errors.u contained 1 error:
-- 1 -------------------------------------------------------
The highlighted expression on line 73
|
73 | if x then 42 else -1
| ^
has type `Nat` but was expected to have type `Boolean`
`Boolean` comes from `if`, whose first argument must be of type `Boolean`
`Nat` comes from line 72:
|
72 | x = 1 + 1
| ^
x = id 42
^^^^^
^^
* "The function <...> expects its <n>th argument to be of type <...>, but
on line <m> it appears to have type <...>."
* `synthesizeApp` can take an argument for what numberth argument it's
testing
* "An if-expression expects its condition to be of type Boolean, but
* In a `synthesizeApp`, report the function input type first, as the
"expected" type.
* `if` and other builtin syntax should have some special treatment.
* Might want signature of function whose application was involved in the
mismatched types. (But don't necessarily want to dump this on users up
front, like GHC tells you the type of every binding in the vicinity)
* Issue maybe not that you didn't know the function's type, but that
you were wrong about the types of the args you passed; also, you might
accidentally omit an argument, supply an extra argument, or supply
arguments in the wrong order.
* We don't bother reporting the other type errors in the same expression,
but we potentially could have an algorithm that could do more fine-grained
recovery.
* Not totally sure on the location of the `Nat`, but the thought
is that if `+` is monomorophic in its return type (always `Nat`),
then it makes sense to attribute the `Nat` of `x` to the `+` call site.
(why not attibute that to the definition site of `+`?)
* Is this inconsistent with treatment of `Boolean` location??
* Since `if` is monomorphic in its first arg, we could use the same logic to
say that the location of that Boolean argument type is the call site
rather than its definition site.
* When encounter an error for a variable x, can add that to an erroneous
variables set - if you ever encounter a subexpression that references
those variables, skip over it?
-}
ex4 f x =
if f x then f 42 else 50
{-
Type mismatch on line <line>: `Nat` vs `Boolean`.
`Nat` comes from the literal:
|
42 | if f x then f 42 else 50
| ^^
∀ a -> [(a, Tree (Text a)) -> (a -> Text -> Text) -> Tree Text
∀ a . Boolean -> a -> a
Not sure what to report for the origin of the `Boolean`:
`Boolean` comes from `f 42`??
`Boolean` comes from `f : Nat -> Boolean`??
But then why does `f` have that type?
Because `if` takes a `Boolean` as first arg..
`Boolean` comes from `if`
`f 42` has type `Boolean` because `f` had to have type `x -> Boolean`
because `f x` was passed as the first argument of `if`:
if f x then f 42 else 50
^^^
Arya thought - when there's a type mismatch between A and B, and A and B
are both inferred types, might make sense to provide more info about provenance.
-}

1
unison-src/new-runtime-transcripts/README Normal file
View File

@ -0,0 +1 @@
Transcripts in this directory are only run using the new runtime.

15
unison-src/new-runtime-transcripts/fix1709.md Normal file
View File

@ -0,0 +1,15 @@
```unison
id x = x
id2 x =
z = 384849
id x
```
```ucm
.scratch> add
```
```unison
> id2 "hi"
```

49
unison-src/new-runtime-transcripts/fix1709.output.md Normal file
View File

@ -0,0 +1,49 @@
```unison
id x = x
id2 x =
z = 384849
id x
```
```ucm
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`:
id : x -> x
id2 : x -> x
```
```ucm
☝️ The namespace .scratch is empty.
.scratch> add
⍟ I've added these definitions:
id : x -> x
id2 : x -> x
```
```unison
> id2 "hi"
```
```ucm
✅
scratch.u changed.
Now evaluating any watch expressions (lines starting with
`>`)... Ctrl+C cancels.
1 | > id2 "hi"
⧩
"hi"
```

264
unison-src/new-runtime-transcripts/hashing.md Normal file
View File

@ -0,0 +1,264 @@
# Hashing and HMAC builtins
```ucm:hide
.> builtins.merge
.> cd builtin
```
Unison has cryptographic builtins for hashing and computing [HMACs](https://en.wikipedia.org/wiki/HMAC) (hash-based message authentication codes). This transcript shows their usage and has some test cases.
## Setup
You can skip this section, which is just needed to make the transcript self-contained. In order to print out and test these hashes we will be using some builtins for base16 (aka hexidecimal) encoding and decoding.
```ucm
.builtin> ls Bytes
```
Notice the `fromBase16` and `toBase16` functions. Here's some (somewhat inefficient) convenience functions for converting `Bytes` to and from base-16 `Text`. These could be replaced by use of `Text.toUtf8` and `Text.tryFromUtf8` once those builtins exist:
```unison:hide
a |> f = f a
List.map f as =
go acc = cases
[] -> acc
(h +: t) -> go (acc :+ f h) t
go [] as
-- not very efficient, but okay for testing
hex : Bytes -> Text
hex b =
Bytes.toBase16 b
|> Bytes.toList
|> List.map Char.fromNat
|> Text.fromCharList
ascii : Text -> Bytes
ascii t = Text.toCharList t |> List.map Char.toNat |> Bytes.fromList
fromHex : Text -> Bytes
fromHex txt =
match Text.toCharList txt
|> List.map Char.toNat
|> Bytes.fromList
|> Bytes.fromBase16
with
Left e -> bug e
Right bs -> bs
check : Boolean -> [Result]
check b = if b then [Result.Ok "Passed."]
else [Result.Fail "Failed."]
test> hex.tests.ex1 = check let
s = "3984af9b"
hex (fromHex s) == s
```
```ucm:hide
.scratch> add
```
The test shows that `hex (fromHex str) == str` as expected.
```ucm
.scratch> test
```
## API overview
Here's a few usage examples:
```unison
ex1 = fromHex "2947db"
|> crypto.hashBytes Sha3_512
|> hex
ex2 = fromHex "02f3ab"
|> crypto.hashBytes Blake2b_256
|> hex
mysecret : Bytes
mysecret = fromHex "237be2"
ex3 = fromHex "50d3ab"
|> crypto.hmacBytes Sha2_256 mysecret
|> hex
> ex1
> ex2
> ex3
```
And here's the full API:
```ucm
.builtin.crypto> find
```
Note that the universal versions of `hash` and `hmac` are currently unimplemented and will bomb at runtime:
```
> crypto.hash Sha3_256 (fromHex "3849238492")
```
## Hashing tests
Here are some test vectors (taken from [here](https://www.di-mgt.com.au/sha_testvectors.html) and [here](https://en.wikipedia.org/wiki/BLAKE_(hash_function))) for the various hashing algorithms:
```unison:hide
ex alg input expected = check let
hashBytes alg (ascii input) ==
fromHex expected
test> sha3_512.tests.ex1 =
ex Sha3_512
"abc"
"b751850b1a57168a5693cd924b6b096e08f621827444f70d884f5d0240d2712e10e116e9192af3c91a7ec57647e3934057340b4cf408d5a56592f8274eec53f0"
test> sha3_512.tests.ex2 =
ex Sha3_512
""
"a69f73cca23a9ac5c8b567dc185a756e97c982164fe25859e0d1dcc1475c80a615b2123af1f5f94c11e3e9402c3ac558f500199d95b6d3e301758586281dcd26"
test> sha3_512.tests.ex3 =
ex Sha3_512
"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
"04a371e84ecfb5b8b77cb48610fca8182dd457ce6f326a0fd3d7ec2f1e91636dee691fbe0c985302ba1b0d8dc78c086346b533b49c030d99a27daf1139d6e75e"
test> sha3_512.tests.ex4 =
ex Sha3_512
"abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
"afebb2ef542e6579c50cad06d2e578f9f8dd6881d7dc824d26360feebf18a4fa73e3261122948efcfd492e74e82e2189ed0fb440d187f382270cb455f21dd185"
test> sha3_256.tests.ex1 =
ex Sha3_256
"abc"
"3a985da74fe225b2045c172d6bd390bd855f086e3e9d525b46bfe24511431532"
test> sha3_256.tests.ex2 =
ex Sha3_256
""
"a7ffc6f8bf1ed76651c14756a061d662f580ff4de43b49fa82d80a4b80f8434a"
test> sha3_256.tests.ex3 =
ex Sha3_256
"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
"41c0dba2a9d6240849100376a8235e2c82e1b9998a999e21db32dd97496d3376"
test> sha3_256.tests.ex4 =
ex Sha3_256
"abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
"916f6061fe879741ca6469b43971dfdb28b1a32dc36cb3254e812be27aad1d18"
test> sha2_512.tests.ex1 =
ex Sha2_512
"abc"
"ddaf35a193617abacc417349ae20413112e6fa4e89a97ea20a9eeee64b55d39a2192992a274fc1a836ba3c23a3feebbd454d4423643ce80e2a9ac94fa54ca49f"
test> sha2_512.tests.ex2 =
ex Sha2_512
""
"cf83e1357eefb8bdf1542850d66d8007d620e4050b5715dc83f4a921d36ce9ce47d0d13c5d85f2b0ff8318d2877eec2f63b931bd47417a81a538327af927da3e"
test> sha2_512.tests.ex3 =
ex Sha2_512
"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
"204a8fc6dda82f0a0ced7beb8e08a41657c16ef468b228a8279be331a703c33596fd15c13b1b07f9aa1d3bea57789ca031ad85c7a71dd70354ec631238ca3445"
test> sha2_512.tests.ex4 =
ex Sha2_512
"abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
"8e959b75dae313da8cf4f72814fc143f8f7779c6eb9f7fa17299aeadb6889018501d289e4900f7e4331b99dec4b5433ac7d329eeb6dd26545e96e55b874be909"
test> sha2_256.tests.ex1 =
ex Sha2_256
"abc"
"ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad"
test> sha2_256.tests.ex2 =
ex Sha2_256
""
"e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
test> sha2_256.tests.ex3 =
ex Sha2_256
"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
"248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1"
test> sha2_256.tests.ex4 =
ex Sha2_256
"abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
"cf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1"
test> blake2s_256.tests.ex1 =
ex Blake2s_256
""
"69217a3079908094e11121d042354a7c1f55b6482ca1a51e1b250dfd1ed0eef9"
test> blake2b_512.tests.ex1 =
ex Blake2b_512
""
"786a02f742015903c6c6fd852552d272912f4740e15847618a86e217f71f5419d25e1031afee585313896444934eb04b903a685b1448b755d56f701afe9be2ce"
test> blake2b_512.tests.ex2 =
ex Blake2b_512
"The quick brown fox jumps over the lazy dog"
"a8add4bdddfd93e4877d2746e62817b116364a1fa7bc148d95090bc7333b3673f82401cf7aa2e4cb1ecd90296e3f14cb5413f8ed77be73045b13914cdcd6a918"
test> blake2b_512.tests.ex3 =
ex Blake2b_512
"The quick brown fox jumps over the lazy dof"
"ab6b007747d8068c02e25a6008db8a77c218d94f3b40d2291a7dc8a62090a744c082ea27af01521a102e42f480a31e9844053f456b4b41e8aa78bbe5c12957bb"
```
```ucm:hide
.scratch> add
```
```ucm
.scratch> test
```
## HMAC tests
These test vectors are taken from [RFC 4231](https://tools.ietf.org/html/rfc4231#section-4.3).
```unison
ex' alg secret msg expected = check let
hmacBytes alg (fromHex secret) (ascii msg) ==
fromHex expected
test> hmac_sha2_256.tests.ex1 =
ex' Sha2_256
"0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b"
"Hi There"
"b0344c61d8db38535ca8afceaf0bf12b881dc200c9833da726e9376c2e32cff7"
test> hmac_sha2_512.tests.ex1 =
ex' Sha2_512
"0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b"
"Hi There"
"87aa7cdea5ef619d4ff0b4241a1d6cb02379f4e2ce4ec2787ad0b30545e17cdedaa833b7d6b8a702038b274eaea3f4e4be9d914eeb61f1702e696c203a126854"
test> hmac_sha2_256.tests.ex2 =
ex' Sha2_256
"4a656665"
"what do ya want for nothing?"
"5bdcc146bf60754e6a042426089575c75a003f089d2739839dec58b964ec3843"
test> hmac_sha2_512.tests.ex2 =
ex' Sha2_512
"4a656665"
"what do ya want for nothing?"
"164b7a7bfcf819e2e395fbe73b56e0a387bd64222e831fd610270cd7ea2505549758bf75c05a994a6d034f65f8f0e6fdcaeab1a34d4a6b4b636e070a38bce737"
```
```ucm:hide
.scratch> add
```
```ucm
.scratch> test
```

418
unison-src/new-runtime-transcripts/hashing.output.md Normal file
View File

@ -0,0 +1,418 @@
# Hashing and HMAC builtins
Unison has cryptographic builtins for hashing and computing [HMACs](https://en.wikipedia.org/wiki/HMAC) (hash-based message authentication codes). This transcript shows their usage and has some test cases.
## Setup
You can skip this section, which is just needed to make the transcript self-contained. In order to print out and test these hashes we will be using some builtins for base16 (aka hexidecimal) encoding and decoding.
```ucm
.builtin> ls Bytes
1. ++ (Bytes -> Bytes -> Bytes)
2. at (Nat -> Bytes -> Optional Nat)
3. drop (Nat -> Bytes -> Bytes)
4. empty (Bytes)
5. flatten (Bytes -> Bytes)
6. fromBase16 (Bytes -> Either Text Bytes)
7. fromBase32 (Bytes -> Either Text Bytes)
8. fromBase64 (Bytes -> Either Text Bytes)
9. fromBase64UrlUnpadded (Bytes -> Either Text Bytes)
10. fromList ([Nat] -> Bytes)
11. size (Bytes -> Nat)
12. take (Nat -> Bytes -> Bytes)
13. toBase16 (Bytes -> Bytes)
14. toBase32 (Bytes -> Bytes)
15. toBase64 (Bytes -> Bytes)
16. toBase64UrlUnpadded (Bytes -> Bytes)
17. toList (Bytes -> [Nat])
```
Notice the `fromBase16` and `toBase16` functions. Here's some (somewhat inefficient) convenience functions for converting `Bytes` to and from base-16 `Text`. These could be replaced by use of `Text.toUtf8` and `Text.tryFromUtf8` once those builtins exist:
```unison
a |> f = f a
List.map f as =
go acc = cases
[] -> acc
(h +: t) -> go (acc :+ f h) t
go [] as
-- not very efficient, but okay for testing
hex : Bytes -> Text
hex b =
Bytes.toBase16 b
|> Bytes.toList
|> List.map Char.fromNat
|> Text.fromCharList
ascii : Text -> Bytes
ascii t = Text.toCharList t |> List.map Char.toNat |> Bytes.fromList
fromHex : Text -> Bytes
fromHex txt =
match Text.toCharList txt
|> List.map Char.toNat
|> Bytes.fromList
|> Bytes.fromBase16
with
Left e -> bug e
Right bs -> bs
check : Boolean -> [Result]
check b = if b then [Result.Ok "Passed."]
else [Result.Fail "Failed."]
test> hex.tests.ex1 = check let
s = "3984af9b"
hex (fromHex s) == s
```
The test shows that `hex (fromHex str) == str` as expected.
```ucm
.scratch> test
Cached test results (`help testcache` to learn more)
◉ hex.tests.ex1 Passed.
✅ 1 test(s) passing
Tip: Use view hex.tests.ex1 to view the source of a test.
```
## API overview
Here's a few usage examples:
```unison
ex1 = fromHex "2947db"
|> crypto.hashBytes Sha3_512
|> hex
ex2 = fromHex "02f3ab"
|> crypto.hashBytes Blake2b_256
|> hex
mysecret : Bytes
mysecret = fromHex "237be2"
ex3 = fromHex "50d3ab"
|> crypto.hmacBytes Sha2_256 mysecret
|> hex
> ex1
> ex2
> ex3
```
```ucm
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`:
ex1 : Text
ex2 : Text
ex3 : Text
mysecret : Bytes
Now evaluating any watch expressions (lines starting with
`>`)... Ctrl+C cancels.
16 | > ex1
⧩
"f3c342040674c50ab45cb1874b6dbc81447af5958201ed4127e03b56725664d7cc44b88b9afadb371898fcaf5d0adeff60837ef93b514f99da43539d79820c99"
17 | > ex2
⧩
"84bb437497f26fc33c51e57e64c37958c3918d50dfe75b91c661a85c2f8f8304"
18 | > ex3
⧩
"c692fc54df921f7fa51aad9178327c5a097784b02212d571fb40facdfff881fd"
```
And here's the full API:
```ucm
.builtin.crypto> find
1. builtin type HashAlgorithm
2. HashAlgorithm.Blake2b_256 : HashAlgorithm
3. HashAlgorithm.Blake2b_512 : HashAlgorithm
4. HashAlgorithm.Blake2s_256 : HashAlgorithm
5. HashAlgorithm.Sha2_256 : HashAlgorithm
6. HashAlgorithm.Sha2_512 : HashAlgorithm
7. HashAlgorithm.Sha3_256 : HashAlgorithm
8. HashAlgorithm.Sha3_512 : HashAlgorithm
9. hash : HashAlgorithm -> a -> Bytes
10. hashBytes : HashAlgorithm -> Bytes -> Bytes
11. hmac : HashAlgorithm -> Bytes -> a -> Bytes
12. hmacBytes : HashAlgorithm -> Bytes -> Bytes -> Bytes
```
Note that the universal versions of `hash` and `hmac` are currently unimplemented and will bomb at runtime:
```
> crypto.hash Sha3_256 (fromHex "3849238492")
```
## Hashing tests
Here are some test vectors (taken from [here](https://www.di-mgt.com.au/sha_testvectors.html) and [here](https://en.wikipedia.org/wiki/BLAKE_(hash_function))) for the various hashing algorithms:
```unison
ex alg input expected = check let
hashBytes alg (ascii input) ==
fromHex expected
test> sha3_512.tests.ex1 =
ex Sha3_512
"abc"
"b751850b1a57168a5693cd924b6b096e08f621827444f70d884f5d0240d2712e10e116e9192af3c91a7ec57647e3934057340b4cf408d5a56592f8274eec53f0"
test> sha3_512.tests.ex2 =
ex Sha3_512
""
"a69f73cca23a9ac5c8b567dc185a756e97c982164fe25859e0d1dcc1475c80a615b2123af1f5f94c11e3e9402c3ac558f500199d95b6d3e301758586281dcd26"
test> sha3_512.tests.ex3 =
ex Sha3_512
"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
"04a371e84ecfb5b8b77cb48610fca8182dd457ce6f326a0fd3d7ec2f1e91636dee691fbe0c985302ba1b0d8dc78c086346b533b49c030d99a27daf1139d6e75e"
test> sha3_512.tests.ex4 =
ex Sha3_512
"abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
"afebb2ef542e6579c50cad06d2e578f9f8dd6881d7dc824d26360feebf18a4fa73e3261122948efcfd492e74e82e2189ed0fb440d187f382270cb455f21dd185"
test> sha3_256.tests.ex1 =
ex Sha3_256
"abc"
"3a985da74fe225b2045c172d6bd390bd855f086e3e9d525b46bfe24511431532"
test> sha3_256.tests.ex2 =
ex Sha3_256
""
"a7ffc6f8bf1ed76651c14756a061d662f580ff4de43b49fa82d80a4b80f8434a"
test> sha3_256.tests.ex3 =
ex Sha3_256
"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
"41c0dba2a9d6240849100376a8235e2c82e1b9998a999e21db32dd97496d3376"
test> sha3_256.tests.ex4 =
ex Sha3_256
"abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
"916f6061fe879741ca6469b43971dfdb28b1a32dc36cb3254e812be27aad1d18"
test> sha2_512.tests.ex1 =
ex Sha2_512
"abc"
"ddaf35a193617abacc417349ae20413112e6fa4e89a97ea20a9eeee64b55d39a2192992a274fc1a836ba3c23a3feebbd454d4423643ce80e2a9ac94fa54ca49f"
test> sha2_512.tests.ex2 =
ex Sha2_512
""
"cf83e1357eefb8bdf1542850d66d8007d620e4050b5715dc83f4a921d36ce9ce47d0d13c5d85f2b0ff8318d2877eec2f63b931bd47417a81a538327af927da3e"
test> sha2_512.tests.ex3 =
ex Sha2_512
"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
"204a8fc6dda82f0a0ced7beb8e08a41657c16ef468b228a8279be331a703c33596fd15c13b1b07f9aa1d3bea57789ca031ad85c7a71dd70354ec631238ca3445"
test> sha2_512.tests.ex4 =
ex Sha2_512
"abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
"8e959b75dae313da8cf4f72814fc143f8f7779c6eb9f7fa17299aeadb6889018501d289e4900f7e4331b99dec4b5433ac7d329eeb6dd26545e96e55b874be909"
test> sha2_256.tests.ex1 =
ex Sha2_256
"abc"
"ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad"
test> sha2_256.tests.ex2 =
ex Sha2_256
""
"e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
test> sha2_256.tests.ex3 =
ex Sha2_256
"abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
"248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1"
test> sha2_256.tests.ex4 =
ex Sha2_256
"abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
"cf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1"
test> blake2s_256.tests.ex1 =
ex Blake2s_256
""
"69217a3079908094e11121d042354a7c1f55b6482ca1a51e1b250dfd1ed0eef9"
test> blake2b_512.tests.ex1 =
ex Blake2b_512
""
"786a02f742015903c6c6fd852552d272912f4740e15847618a86e217f71f5419d25e1031afee585313896444934eb04b903a685b1448b755d56f701afe9be2ce"
test> blake2b_512.tests.ex2 =
ex Blake2b_512
"The quick brown fox jumps over the lazy dog"
"a8add4bdddfd93e4877d2746e62817b116364a1fa7bc148d95090bc7333b3673f82401cf7aa2e4cb1ecd90296e3f14cb5413f8ed77be73045b13914cdcd6a918"
test> blake2b_512.tests.ex3 =
ex Blake2b_512
"The quick brown fox jumps over the lazy dof"
"ab6b007747d8068c02e25a6008db8a77c218d94f3b40d2291a7dc8a62090a744c082ea27af01521a102e42f480a31e9844053f456b4b41e8aa78bbe5c12957bb"
```
```ucm
.scratch> test
Cached test results (`help testcache` to learn more)
◉ blake2s_256.tests.ex1 Passed.
◉ sha2_256.tests.ex2 Passed.
◉ hex.tests.ex1 Passed.
◉ sha2_256.tests.ex3 Passed.
◉ sha3_512.tests.ex2 Passed.
◉ blake2b_512.tests.ex1 Passed.
◉ sha3_512.tests.ex1 Passed.
◉ sha3_256.tests.ex2 Passed.
◉ sha3_512.tests.ex3 Passed.
◉ sha2_512.tests.ex1 Passed.
◉ sha2_256.tests.ex4 Passed.
◉ blake2b_512.tests.ex3 Passed.
◉ sha3_256.tests.ex1 Passed.
◉ sha2_512.tests.ex4 Passed.
◉ sha3_256.tests.ex4 Passed.
◉ sha3_256.tests.ex3 Passed.
◉ sha3_512.tests.ex4 Passed.
◉ sha2_256.tests.ex1 Passed.
◉ sha2_512.tests.ex3 Passed.
◉ blake2b_512.tests.ex2 Passed.
◉ sha2_512.tests.ex2 Passed.
✅ 21 test(s) passing
Tip: Use view blake2s_256.tests.ex1 to view the source of a
test.
```
## HMAC tests
These test vectors are taken from [RFC 4231](https://tools.ietf.org/html/rfc4231#section-4.3).
```unison
ex' alg secret msg expected = check let
hmacBytes alg (fromHex secret) (ascii msg) ==
fromHex expected
test> hmac_sha2_256.tests.ex1 =
ex' Sha2_256
"0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b"
"Hi There"
"b0344c61d8db38535ca8afceaf0bf12b881dc200c9833da726e9376c2e32cff7"
test> hmac_sha2_512.tests.ex1 =
ex' Sha2_512
"0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b"
"Hi There"
"87aa7cdea5ef619d4ff0b4241a1d6cb02379f4e2ce4ec2787ad0b30545e17cdedaa833b7d6b8a702038b274eaea3f4e4be9d914eeb61f1702e696c203a126854"
test> hmac_sha2_256.tests.ex2 =
ex' Sha2_256
"4a656665"
"what do ya want for nothing?"
"5bdcc146bf60754e6a042426089575c75a003f089d2739839dec58b964ec3843"
test> hmac_sha2_512.tests.ex2 =
ex' Sha2_512
"4a656665"
"what do ya want for nothing?"
"164b7a7bfcf819e2e395fbe73b56e0a387bd64222e831fd610270cd7ea2505549758bf75c05a994a6d034f65f8f0e6fdcaeab1a34d4a6b4b636e070a38bce737"
```
```ucm
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`:
ex' : HashAlgorithm
-> Text
-> Text
-> Text
-> [Result]
hmac_sha2_256.tests.ex1 : [Result]
hmac_sha2_256.tests.ex2 : [Result]
hmac_sha2_512.tests.ex1 : [Result]
hmac_sha2_512.tests.ex2 : [Result]
Now evaluating any watch expressions (lines starting with
`>`)... Ctrl+C cancels.
6 | ex' Sha2_256
✅ Passed Passed.
12 | ex' Sha2_512
✅ Passed Passed.
18 | ex' Sha2_256
✅ Passed Passed.
24 | ex' Sha2_512
✅ Passed Passed.
```
```ucm
.scratch> test
Cached test results (`help testcache` to learn more)
◉ blake2s_256.tests.ex1 Passed.
◉ sha2_256.tests.ex2 Passed.
◉ hex.tests.ex1 Passed.
◉ hmac_sha2_256.tests.ex1 Passed.
◉ sha2_256.tests.ex3 Passed.
◉ sha3_512.tests.ex2 Passed.
◉ blake2b_512.tests.ex1 Passed.
◉ sha3_512.tests.ex1 Passed.
◉ sha3_256.tests.ex2 Passed.
◉ sha3_512.tests.ex3 Passed.
◉ sha2_512.tests.ex1 Passed.
◉ sha2_256.tests.ex4 Passed.
◉ blake2b_512.tests.ex3 Passed.
◉ sha3_256.tests.ex1 Passed.
◉ hmac_sha2_512.tests.ex1 Passed.
◉ sha2_512.tests.ex4 Passed.
◉ hmac_sha2_256.tests.ex2 Passed.
◉ sha3_256.tests.ex4 Passed.
◉ sha3_256.tests.ex3 Passed.
◉ sha3_512.tests.ex4 Passed.
◉ hmac_sha2_512.tests.ex2 Passed.
◉ sha2_256.tests.ex1 Passed.
◉ sha2_512.tests.ex3 Passed.
◉ blake2b_512.tests.ex2 Passed.
◉ sha2_512.tests.ex2 Passed.
✅ 25 test(s) passing
Tip: Use view blake2s_256.tests.ex1 to view the source of a
test.
```

48
unison-src/parser-tests/GenerateErrors.hs Normal file
View File

@ -0,0 +1,48 @@
{- For every file foo.u in the current directory write the parse error to foo.message.txt -}
module GenerateErrors where
import qualified Data.Text as Text
import Data.Text.IO ( readFile )
import Prelude hiding ( readFile )
import System.Directory ( listDirectory, getCurrentDirectory )
import System.FilePath ( takeExtension, dropExtension )
import System.IO ( putStrLn )
import qualified Unison.Builtin as B
import Unison.Parser ( Err )
import qualified Unison.Parsers as P
import Unison.PrintError ( prettyParseError )
import Unison.Symbol ( Symbol )
import qualified Unison.Util.ColorText as Color
import Unison.Var ( Var )
unisonFilesInDir :: FilePath -> IO [String]
unisonFilesInDir p = do
files <- listDirectory p
pure $ filter ((==) ".u" . takeExtension) files
unisonFilesInCurrDir :: IO [String]
unisonFilesInCurrDir = getCurrentDirectory >>= unisonFilesInDir
errorFileName :: String -> String
errorFileName n = dropExtension n ++ ".message.txt"
emitAsPlainTextTo :: Var v => String -> Err v -> FilePath -> IO ()
emitAsPlainTextTo src e f = writeFile f plainErr
where plainErr = Color.toPlain $ prettyParseError src e
printError :: Var v => String -> Err v -> IO ()
printError src e = putStrLn $ B.showParseError src e
processFile :: FilePath -> IO ()
processFile f = do
content <- Text.unpack <$> readFile f
let res = P.parseFile f content B.names
case res of
Left err -> do
emitAsPlainTextTo content (err :: Err Symbol) (errorFileName f)
printError content err
Right _ -> putStrLn $
"Error: " ++ f ++ " parses successfully but none of the files in this directory should parse"
main :: IO ()
main = unisonFilesInCurrDir >>= mapM_ processFile

Some files were not shown because too many files have changed in this diff Show More