You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
.> view base.Abort.toOptional
base.Abort.toOptional : '{g, Abort} a ->{g} Optional a
base.Abort.toOptional a = handle !a with toOptional.handler
base.Abort.toOptional.handler
.> view base.Abort.toOptional.handler
base.Abort.toOptional.handler : Request {Abort} a -> Optional a
base.Abort.toOptional.handler = cases
{ a } -> Some a
{abort -> _} -> None
base.Ask
.> view base.Ask
ability base.Ask a where ask : {base.Ask a} a
base.Ask.ask
.> view base.Ask.ask
ability base.Ask a where ask : {base.Ask a} a
base.Ask.provide
.> view base.Ask.provide
base.Ask.provide : a -> '{g, Ask a} r ->{g} r
base.Ask.provide a asker =
handle !asker with provide.handler a
base.Ask.provide.handler
.> view base.Ask.provide.handler
base.Ask.provide.handler : a -> Request {Ask a} r -> r
base.Ask.provide.handler a =
h = cases
{ r } -> r
{ask -> resume} -> handle resume a with h
h
.> view base.Char.ascii.isPunct
base.Char.ascii.isPunct : Char -> Boolean
base.Char.ascii.isPunct c =
if (c == ?\s) || (isAlphaNum c) then false else isPrint c
.> view base.Char.ascii.lowerUpperDiff
base.Char.ascii.lowerUpperDiff : Int
base.Char.ascii.lowerUpperDiff =
use Int -
toInt (toNat ?a) - toInt (toNat ?A)
base.Char.ascii.tests.propUpperLower
.> view base.Char.ascii.tests.propUpperLower
base.Char.ascii.tests.propUpperLower : [Result]
base.Char.ascii.tests.propUpperLower =
go _ =
use ascii toLower toUpper
c = fromNat !nat
if isUpper c then expect (toUpper (toLower c) == c)
else
if isLower c then expect (toLower (toUpper c) == c)
else expect ((toUpper c == c) && (toLower c == c))
runs 128 go
.> view base.Char.ascii.toLower
base.Char.ascii.toLower : Char -> Char
base.Char.ascii.toLower c =
if isUpper c then
use Int +
fromNat (truncate0 (toInt (toNat c) + lowerUpperDiff))
else c
base.Char.ascii.toUpper
.> view base.Char.ascii.toUpper
base.Char.ascii.toUpper : Char -> Char
base.Char.ascii.toUpper c =
if isLower c then
use Int -
fromNat (truncate0 (toInt (toNat c) - lowerUpperDiff))
else c
base.Char.fromNat
.> view base.Char.fromNat
-- base.Char.fromNat is built-in.
base.Char.inRange
.> view base.Char.inRange
base.Char.inRange : Char -> Char -> Char -> Boolean
base.Char.inRange lo hi c =
code = toNat c
(toNat lo <= code) && (code <= toNat hi)
base.Char.toNat
.> view base.Char.toNat
-- base.Char.toNat is built-in.
base.CopyrightHolder
.> view base.CopyrightHolder
unique type base.CopyrightHolder = CopyrightHolder GUID Text
base.CopyrightHolder.CopyrightHolder
.> view base.CopyrightHolder.CopyrightHolder
unique type base.CopyrightHolder = CopyrightHolder GUID Text
.> view base.Doc.Blob
unique type base.Doc
= Link Link
| Source Link
| Blob Text
| Join [base.Doc]
| Signature Term
| Evaluate Term
base.Doc.Evaluate
.> view base.Doc.Evaluate
unique type base.Doc
= Link Link
| Source Link
| Blob Text
| Join [base.Doc]
| Signature Term
| Evaluate Term
base.Doc.Join
.> view base.Doc.Join
unique type base.Doc
= Link Link
| Source Link
| Blob Text
| Join [base.Doc]
| Signature Term
| Evaluate Term
base.Doc.Link
.> view base.Doc.Link
unique type base.Doc
= Link Link
| Source Link
| Blob Text
| Join [base.Doc]
| Signature Term
| Evaluate Term
base.Doc.Signature
.> view base.Doc.Signature
unique type base.Doc
= Link Link
| Source Link
| Blob Text
| Join [base.Doc]
| Signature Term
| Evaluate Term
base.Doc.Source
.> view base.Doc.Source
unique type base.Doc
= Link Link
| Source Link
| Blob Text
| Join [base.Doc]
| Signature Term
| Evaluate Term
base.Doc.example
.> view base.Doc.example
base.Doc.example : Term -> Doc
base.Doc.example e =
source = Source (Term e)
value = Evaluate e
Join
[Blob "\n", source, Blob "\n\nOutput: ", value, Blob ""]
base.Either
.> view base.Either
type base.Either a b = Left a | Right b
base.Either.Left
.> view base.Either.Left
type base.Either a b = Left a | Right b
base.Either.Right
.> view base.Either.Right
type base.Either a b = Left a | Right b
base.Either.mapLeft
.> view base.Either.mapLeft
base.Either.mapLeft : (a ->{π} b) -> Either a z ->{π} Either b z
base.Either.mapLeft f = cases
Left l -> Left (f l)
Right r -> Right r
base.Either.mapLeft.tests.ex1
.> view base.Either.mapLeft.tests.ex1
base.Either.mapLeft.tests.ex1 : [Result]
base.Either.mapLeft.tests.ex1 =
check
let
input = [Left 2, Left 5, Right "Hiya"]
actual = List.map (mapLeft Nat.toText) input
expected = [Left "2", Left "5", Right "Hiya"]
assert
(actual == expected)
("Not equal!", actual, expected)
true
base.Either.mapRight
.> view base.Either.mapRight
base.Either.mapRight :
(a ->{π} b) -> Either e a ->{π} Either e b
base.Either.mapRight f = cases
Left l -> Left l
Right a -> Right (f a)
base.Either.mapRight.tests.ex1
.> view base.Either.mapRight.tests.ex1
base.Either.mapRight.tests.ex1 : [Result]
base.Either.mapRight.tests.ex1 =
check
let
input =
[Left 2, Left 5, Right "Hiya", Right "Bye", Left 10]
actual =
use Text ++
List.map (mapRight (s -> s ++ "!")) input
expected =
[Left 2, Left 5, Right "Hiya!", Right "Bye!", Left 10]
assert
(actual == expected)
("Not equal!", actual, expected)
true
base.Either.toException
.> view base.Either.toException
base.Either.toException : Either e a ->{Exception e} a
base.Either.toException = cases
Left e -> raise e
Right a -> a
base.Exception
.> view base.Exception
ability base.Exception e where
raise : e ->{base.Exception e} a
base.Exception.raise
.> view base.Exception.raise
ability base.Exception e where
raise : e ->{base.Exception e} a
.> view base.Exception.toEither
base.Exception.toEither : '{g, Exception e} a ->{g} Either e a
base.Exception.toEither a = handle !a with toEither.handler
base.Exception.toEither.handler
.> view base.Exception.toEither.handler
base.Exception.toEither.handler :
Request {Exception e} a -> Either e a
base.Exception.toEither.handler = cases
{ a } -> Right a
{raise e -> _} -> Left e
base.Float
.> view base.Float
-- base.Float is built-in.
base.Float.*
.> view base.Float.*
-- base.Float.* is built-in.
base.Float.+
.> view base.Float.+
-- base.Float.+ is built-in.
base.Float.-
.> view base.Float.-
-- base.Float.- is built-in.
base.Float./
.> view base.Float./
-- base.Float./ is built-in.
base.Float.abs
.> view base.Float.abs
-- base.Float.abs is built-in.
base.Float.acos
.> view base.Float.acos
-- base.Float.acos is built-in.
base.Float.acosh
.> view base.Float.acosh
-- base.Float.acosh is built-in.
base.Float.asin
.> view base.Float.asin
-- base.Float.asin is built-in.
base.Float.asinh
.> view base.Float.asinh
-- base.Float.asinh is built-in.
base.Float.atan
.> view base.Float.atan
-- base.Float.atan is built-in.
base.Float.atan2
.> view base.Float.atan2
-- base.Float.atan2 is built-in.
base.Float.atanh
.> view base.Float.atanh
-- base.Float.atanh is built-in.
base.Float.ceiling
.> view base.Float.ceiling
-- base.Float.ceiling is built-in.
base.Float.cos
.> view base.Float.cos
-- base.Float.cos is built-in.
base.Float.cosh
.> view base.Float.cosh
-- base.Float.cosh is built-in.
base.Float.eq
.> view base.Float.eq
-- base.Float.eq is built-in.
base.Float.exp
.> view base.Float.exp
-- base.Float.exp is built-in.
base.Float.floor
.> view base.Float.floor
-- base.Float.floor is built-in.
base.Float.fromText
.> view base.Float.fromText
-- base.Float.fromText is built-in.
base.Float.gt
.> view base.Float.gt
-- base.Float.gt is built-in.
base.Float.gteq
.> view base.Float.gteq
-- base.Float.gteq is built-in.
base.Float.log
.> view base.Float.log
-- base.Float.log is built-in.
base.Float.logBase
.> view base.Float.logBase
-- base.Float.logBase is built-in.
base.Float.lt
.> view base.Float.lt
-- base.Float.lt is built-in.
base.Float.lteq
.> view base.Float.lteq
-- base.Float.lteq is built-in.
base.Float.max
.> view base.Float.max
-- base.Float.max is built-in.
base.Float.min
.> view base.Float.min
-- base.Float.min is built-in.
base.Float.pow
.> view base.Float.pow
-- base.Float.pow is built-in.
base.Float.round
.> view base.Float.round
-- base.Float.round is built-in.
base.Float.sin
.> view base.Float.sin
-- base.Float.sin is built-in.
base.Float.sinh
.> view base.Float.sinh
-- base.Float.sinh is built-in.
base.Float.sqrt
.> view base.Float.sqrt
-- base.Float.sqrt is built-in.
base.Float.tan
.> view base.Float.tan
-- base.Float.tan is built-in.
base.Float.tanh
.> view base.Float.tanh
-- base.Float.tanh is built-in.
base.Float.toText
.> view base.Float.toText
-- base.Float.toText is built-in.
base.Float.truncate
.> view base.Float.truncate
-- base.Float.truncate is built-in.
base.Function.curry
.> view base.Function.curry
base.Function.curry : ((a, b) ->{e} c) -> a -> b ->{e} c
base.Function.curry f a b = f (a, b)
base.Function.fix
.> view base.Function.fix
base.Function.fix : ('{e} a ->{e} a) ->{e} a
base.Function.fix f =
x = '(f x)
!x
.> view base.Function.fix.examples.factorial.explicitRecursion
base.Function.fix.examples.factorial.explicitRecursion : Nat
base.Function.fix.examples.factorial.explicitRecursion =
fac n =
if n <= 1 then 1
else
use Nat *
n * fac (Nat.decrement n)
fac 7
base.Function.fix.examples.factorial.fixpoint
.> view base.Function.fix.examples.factorial.fixpoint
base.Function.fix.examples.factorial.fixpoint : Nat
base.Function.fix.examples.factorial.fixpoint =
fix
(rec n ->
(if n <= 1 then 1
else
use Nat *
n * !rec (Nat.decrement n))) 7
base.Function.flatMap
.> view base.Function.flatMap
base.Function.flatMap :
(a -> r ->{e} b) -> (r ->{e} a) -> r ->{e} b
base.Function.flatMap f x r = f (x r) r
base.Function.flip
.> view base.Function.flip
base.Function.flip : (a ->{e} b ->{e} c) -> b -> a ->{e} c
base.Function.flip f b a = f a b
base.Function.on
.> view base.Function.on
base.Function.on :
(b ->{e} b ->{e} c) -> (a ->{e} b) -> a -> a ->{e} c
base.Function.on b u x y = b (u x) (u y)
.> view base.Function.uncurry
base.Function.uncurry : (a ->{e} b ->{e} c) -> (a, b) ->{e} c
base.Function.uncurry f = cases (a, b) -> f a b
base.GUID
.> view base.GUID
unique type base.GUID = GUID Bytes
base.GUID.GUID
.> view base.GUID.GUID
unique type base.GUID = GUID Bytes
base.Heap
.> view base.Heap
type base.Heap k v = Heap Nat k v [base.Heap k v]
base.Heap.Heap
.> view base.Heap.Heap
type base.Heap k v = Heap Nat k v [base.Heap k v]
base.Heap.children
.> view base.Heap.children
base.Heap.children : Heap k v -> [Heap k v]
base.Heap.children = cases Heap _ _ _ cs -> cs
base.Heap.fromKeys
.> view base.Heap.fromKeys
base.Heap.fromKeys : [a] -> Optional (Heap a a)
base.Heap.fromKeys as =
Heap.fromList (List.map (a -> (a, a)) as)
base.Heap.fromList
.> view base.Heap.fromList
base.Heap.fromList : [(k, v)] -> Optional (Heap k v)
base.Heap.fromList kvs =
op a b =
match a with
None -> b
Some a ->
match b with
None -> Some a
Some b -> Some (Heap.union a b)
single = cases (k, v) -> Some (Heap.singleton k v)
foldb single op None kvs
base.Heap.max
.> view base.Heap.max
base.Heap.max : Heap k v -> (k, v)
base.Heap.max = cases Heap _ k v _ -> (k, v)
base.Heap.maxKey
.> view base.Heap.maxKey
base.Heap.maxKey : Heap k v -> k
base.Heap.maxKey = cases Heap _ k _ _ -> k
base.Heap.pop
.> view base.Heap.pop
base.Heap.pop : Heap k v -> Optional (Heap k v)
base.Heap.pop h =
go h subs =
use List size
if size subs == 0 then h
else
use Heap union
if size subs == 1 then union h (unsafeAt 0 subs)
else
union
(union h (unsafeAt 0 subs))
(go (unsafeAt 1 subs) (List.drop 2 subs))
match List.uncons (children h) with
None -> None
Some (s0, subs) -> Some (go s0 subs)
base.Heap.singleton
.> view base.Heap.singleton
base.Heap.singleton : k -> v -> Heap k v
base.Heap.singleton k v = Heap 1 k v []
base.Heap.size
.> view base.Heap.size
base.Heap.size : Heap k v -> Nat
base.Heap.size = cases Heap n _ _ _ -> n
base.Heap.sort
.> view base.Heap.sort
base.Heap.sort : [a] -> [a]
base.Heap.sort as = sortDescending as |> reverse
base.Heap.sortDescending
.> view base.Heap.sortDescending
base.Heap.sortDescending : [a] -> [a]
base.Heap.sortDescending as =
step = cases
None -> None
Some h -> Some (Heap.max h, pop h)
unfold (fromKeys as) step |> List.map at1
base.Heap.union
.> view base.Heap.union
base.Heap.union : Heap k v -> Heap k v -> Heap k v
base.Heap.union h1 h2 =
match (h1, h2) with
(Heap n k1 v1 hs1, Heap m k2 v2 hs2) ->
use Nat +
if k1 >= k2 then Heap (n + m) k1 v1 (h2 +: hs1)
else Heap (n + m) k2 v2 (h1 +: hs2)
base.Int
.> view base.Int
-- base.Int is built-in.
base.Int.*
.> view base.Int.*
-- base.Int.* is built-in.
base.Int.+
.> view base.Int.+
-- base.Int.+ is built-in.
base.Int.-
.> view base.Int.-
-- base.Int.- is built-in.
base.Int./
.> view base.Int./
-- base.Int./ is built-in.
base.Int.and
.> view base.Int.and
-- base.Int.and is built-in.
base.Int.complement
.> view base.Int.complement
-- base.Int.complement is built-in.
base.Int.decrement
.> view base.Int.decrement
base.Int.decrement : Int -> Int
base.Int.decrement n =
use Int -
n - +1
base.Int.decrement.test
.> view base.Int.decrement.test
base.Int.decrement.test : [Result]
base.Int.decrement.test =
use Int +
forAll 100 Domain.ints (n -> Int.decrement n + +1 == n)
base.Int.eq
.> view base.Int.eq
-- base.Int.eq is built-in.
base.Int.fromText
.> view base.Int.fromText
-- base.Int.fromText is built-in.
base.Int.gt
.> view base.Int.gt
-- base.Int.gt is built-in.
base.Int.gteq
.> view base.Int.gteq
-- base.Int.gteq is built-in.
base.Int.inRange
.> view base.Int.inRange
base.Int.inRange : Int -> Int -> Int -> Boolean
base.Int.inRange fromInclusive toExclusive x =
(x >= fromInclusive) && (x < toExclusive)
base.Int.inRange.test
.> view base.Int.inRange.test
base.Int.inRange.test : [Result]
base.Int.inRange.test =
runs
100
'let
x = !int
y = !int
z = !int
match sort [x, y, z] with
[x, y, z] -> expect ((Int.inRange x z y) || (z == y))
base.Int.increment
.> view base.Int.increment
-- base.Int.increment is built-in.
base.Int.isEven
.> view base.Int.isEven
-- base.Int.isEven is built-in.
base.Int.isOdd
.> view base.Int.isOdd
-- base.Int.isOdd is built-in.
base.Int.leadingZeros
.> view base.Int.leadingZeros
-- base.Int.leadingZeros is built-in.
base.Int.lt
.> view base.Int.lt
-- base.Int.lt is built-in.
base.Int.lteq
.> view base.Int.lteq
-- base.Int.lteq is built-in.
base.Int.maxInt
.> view base.Int.maxInt
base.Int.maxInt : Int
base.Int.maxInt = +9223372036854775807
base.Int.minInt
.> view base.Int.minInt
base.Int.minInt : Int
base.Int.minInt = -9223372036854775808
base.Int.mod
.> view base.Int.mod
-- base.Int.mod is built-in.
base.Int.negate
.> view base.Int.negate
-- base.Int.negate is built-in.
base.Int.or
.> view base.Int.or
-- base.Int.or is built-in.
base.Int.pow
.> view base.Int.pow
-- base.Int.pow is built-in.
base.Int.range
.> view base.Int.range
base.Int.range : Int -> Int -> [Int]
base.Int.range start stopExclusive =
f : Int -> Optional (Int, Int)
f i =
if i < stopExclusive then
use Int +
Some (i, i + +1)
else None
unfold start f
base.Int.shiftLeft
.> view base.Int.shiftLeft
-- base.Int.shiftLeft is built-in.
base.Int.shiftRight
.> view base.Int.shiftRight
-- base.Int.shiftRight is built-in.
base.Int.signum
.> view base.Int.signum
-- base.Int.signum is built-in.
base.Int.toFloat
.> view base.Int.toFloat
-- base.Int.toFloat is built-in.
base.Int.toText
.> view base.Int.toText
-- base.Int.toText is built-in.
base.Int.trailingZeros
.> view base.Int.trailingZeros
-- base.Int.trailingZeros is built-in.
base.Int.truncate0
.> view base.Int.truncate0
-- base.Int.truncate0 is built-in.
base.Int.xor
.> view base.Int.xor
-- base.Int.xor is built-in.
base.IsPropagated
.> view base.IsPropagated
unique type base.IsPropagated = IsPropagated
base.IsPropagated.IsPropagated
.> view base.IsPropagated.IsPropagated
unique type base.IsPropagated = IsPropagated
base.IsTest
.> view base.IsTest
unique type base.IsTest = IsTest
base.IsTest.IsTest
.> view base.IsTest.IsTest
unique type base.IsTest = IsTest
.> view base.LicenseType
unique type base.LicenseType = LicenseType Doc
base.LicenseType.LicenseType
.> view base.LicenseType.LicenseType
unique type base.LicenseType = LicenseType Doc
base.Link
.> view base.Link
unique type base.Link = Term Term | Type Type
base.Link.Term
.> view base.Link.Term
unique type base.Link = Term Term | Type Type
-- base.Link.Term is built-in.
base.Link.Term
.> view base.Link.Term
unique type base.Link = Term Term | Type Type
-- base.Link.Term is built-in.
base.Link.Type
.> view base.Link.Type
unique type base.Link = Term Term | Type Type
-- base.Link.Type is built-in.
base.Link.Type
.> view base.Link.Type
unique type base.Link = Term Term | Type Type
-- base.Link.Type is built-in.
base.List
.> view base.List
-- base.List is built-in.
base.List.++
.> view base.List.++
-- base.List.++ is built-in.
base.List.+:
.> view base.List.+:
-- base.List.+: is built-in.
base.List.:+
.> view base.List.:+
-- base.List.:+ is built-in.
base.List.Nonempty
.> view base.List.Nonempty
type base.List.Nonempty a = Nonempty a [a]
base.List.Nonempty.++
.> view base.List.Nonempty.++
(base.List.Nonempty.++) : Nonempty a -> Nonempty a -> Nonempty a
(base.List.Nonempty.++) = cases
Nonempty x xs ->
cases
Nonempty y ys ->
use List ++
Nonempty x (xs :+ y ++ ys)
base.List.Nonempty.+|
.> view base.List.Nonempty.+|
(base.List.Nonempty.+|) : a -> [a] -> Nonempty a
(base.List.Nonempty.+|) = Nonempty
base.List.Nonempty.Nonempty
.> view base.List.Nonempty.Nonempty
type base.List.Nonempty a = Nonempty a [a]
base.List.Nonempty.append
.> view base.List.Nonempty.append
(base.List.Nonempty.++) : Nonempty a -> Nonempty a -> Nonempty a
(base.List.Nonempty.++) = cases
Nonempty x xs ->
cases
Nonempty y ys ->
use List ++
Nonempty x (xs :+ y ++ ys)
base.List.Nonempty.append.tests.associative
.> view base.List.Nonempty.append.tests.associative
base.List.Nonempty.append.tests.associative : [Result]
base.List.Nonempty.append.tests.associative =
use Nonempty ++
runs
100 'let
x = !(atLeastOne nat)
y = !(atLeastOne nat)
z = !(atLeastOne nat)
expect (x ++ (y ++ z) == (x ++ y ++ z))
base.List.Nonempty.append.tests.homomorphism
.> view base.List.Nonempty.append.tests.homomorphism
base.List.Nonempty.append.tests.homomorphism : [Result]
base.List.Nonempty.append.tests.homomorphism =
use List size
use Nat +
use Nonempty ++ toList
runs
100
'let
x = !(atLeastOne nat)
y = !(atLeastOne nat)
expect
( size (toList x)
+ size (toList y)
== size (toList (x ++ y)))
base.List.Nonempty.cons
.> view base.List.Nonempty.cons
base.List.Nonempty.cons : a -> Nonempty a -> Nonempty a
base.List.Nonempty.cons a = (Nonempty a) Nonempty.toList
.> view base.List.Nonempty.flatMap
base.List.Nonempty.flatMap :
(a ->{e} Nonempty b) -> Nonempty a ->{e} Nonempty b
base.List.Nonempty.flatMap f = cases
Nonempty a as ->
match List.flatMap ( Nonempty.toList f) as with
x +: xs ->
use Nonempty ++
f a ++ Nonempty x xs
[] -> f a
.> view base.List.Nonempty.foldMap
base.List.Nonempty.foldMap :
(b ->{e} b ->{e} b) -> (a ->{e} b) -> Nonempty a ->{e} b
base.List.Nonempty.foldMap semigroup f = cases
Nonempty a as ->
List.foldl (acc x -> semigroup acc (f x)) (f a) as
base.List.Nonempty.foldMap.examples.ex1
.> view base.List.Nonempty.foldMap.examples.ex1
base.List.Nonempty.foldMap.examples.ex1 : Text
base.List.Nonempty.foldMap.examples.ex1 =
use Text ++
foldMap (++) Nat.toText (1 +| [2, 3])
base.List.Nonempty.foldMap.test
.> view base.List.Nonempty.foldMap.test
base.List.Nonempty.foldMap.test : [Result]
base.List.Nonempty.foldMap.test =
use Nat toText
use Text ++
runs
100
'let
x = !nat
y = !nat
z = !nat
f = foldMap (++) toText
expect
((( f (x +| [y, z])
== (toText x ++ toText y ++ toText z))
&&
(f (x +| [y]) == (toText x ++ toText y)))
&&
(f (Nonempty.singleton x) == toText x))
base.List.Nonempty.foldl
.> view base.List.Nonempty.foldl
base.List.Nonempty.foldl :
(a ->{e} a ->{e} a) -> Nonempty a ->{e} a
base.List.Nonempty.foldl f = cases
Nonempty a as -> List.foldl f a as
base.List.Nonempty.foldl.test
.> view base.List.Nonempty.foldl.test
base.List.Nonempty.foldl.test : [Result]
base.List.Nonempty.foldl.test =
use Nat drop
use Nonempty foldl
runs
100
'let
x = !nat
y = !nat
z = !nat
expect
(((foldl drop (x +| [y, z]) == drop (drop x y) z)
&&
(foldl drop (x +| [y]) == drop x y))
&&
(foldl drop (Nonempty.singleton x) == x))
base.List.Nonempty.foldr
.> view base.List.Nonempty.foldr
base.List.Nonempty.foldr :
(a ->{e} a ->{e} a) -> Nonempty a ->{e} a
base.List.Nonempty.foldr f as =
List.foldr f (Nonempty.last as) (Nonempty.init as)
base.List.Nonempty.foldr.test
.> view base.List.Nonempty.foldr.test
base.List.Nonempty.foldr.test : [Result]
base.List.Nonempty.foldr.test =
use Nat drop
use Nonempty foldr
runs
100
'let
x = !nat
y = !nat
z = !nat
expect
(((foldr drop (x +| [y, z]) == drop x (drop y z))
&&
(foldr drop (x +| [y]) == drop x y))
&&
(foldr drop (Nonempty.singleton x) == x))
base.List.Nonempty.head
.> view base.List.Nonempty.head
base.List.Nonempty.head : Nonempty a -> a
base.List.Nonempty.head = cases Nonempty a _ -> a
base.List.Nonempty.head.test
.> view base.List.Nonempty.head.test
base.List.Nonempty.head.test : [Result]
base.List.Nonempty.head.test =
runs
100 'let
a = !nat
as = !(listOf nat)
expect (Nonempty.head (Nonempty a as) == a)
base.List.Nonempty.init
.> view base.List.Nonempty.init
base.List.Nonempty.init : Nonempty a -> [a]
base.List.Nonempty.init = cases
Nonempty a [] -> []
Nonempty a (xs :+ _) -> a +: xs
base.List.Nonempty.init.test
.> view base.List.Nonempty.init.test
base.List.Nonempty.init.test : [Result]
base.List.Nonempty.init.test =
runs
100 'let
a = !nat
as = !(listOf nat)
expect (Nonempty.init (as |+ a) == as)
base.List.Nonempty.join
.> view base.List.Nonempty.join
base.List.Nonempty.join : Nonempty (Nonempty a) -> Nonempty a
base.List.Nonempty.join = cases
Nonempty (Nonempty a as) nels ->
use List ++
Nonempty a (as ++ List.flatMap Nonempty.toList nels)
.> view base.List.Nonempty.last
base.List.Nonempty.last : Nonempty a -> a
base.List.Nonempty.last = cases
Nonempty a [] -> a
Nonempty a (xs :+ x) -> x
base.List.Nonempty.last.test
.> view base.List.Nonempty.last.test
base.List.Nonempty.last.test : [Result]
base.List.Nonempty.last.test =
runs
100 'let
a = !nat
as = !(listOf nat)
expect (Nonempty.last (as |+ a) == a)
base.List.Nonempty.map
.> view base.List.Nonempty.map
base.List.Nonempty.map :
(a ->{e} b) -> Nonempty a ->{e} Nonempty b
base.List.Nonempty.map f = cases
Nonempty a as -> Nonempty (f a) (List.map f as)
.> view base.List.Nonempty.scanl
base.List.Nonempty.scanl :
(a ->{e} a ->{e} a) -> Nonempty a ->{e} Nonempty a
base.List.Nonempty.scanl f = cases
Nonempty x xs -> List.scanl f x xs
.> view base.List.Nonempty.scanl.test
base.List.Nonempty.scanl.test : [Result]
base.List.Nonempty.scanl.test =
use Int -
runs
100
'let
x = !int
y = !int
z = !int
expect
( Nonempty.scanl (-) (Nonempty x [y, z])
== Nonempty x [x - y, x - y - z])
base.List.Nonempty.scanr
.> view base.List.Nonempty.scanr
base.List.Nonempty.scanr :
(a ->{e} a ->{e} a) -> Nonempty a ->{e} Nonempty a
base.List.Nonempty.scanr f = cases
Nonempty x (ys :+ y) -> List.scanr f y (x +: ys)
xs -> xs
.> view base.List.Nonempty.snoc
base.List.Nonempty.snoc : Nonempty a -> a -> Nonempty a
base.List.Nonempty.snoc = cases
Nonempty head middle ->
last -> Nonempty head (middle :+ last)
base.List.Nonempty.tail
.> view base.List.Nonempty.tail
base.List.Nonempty.tail : Nonempty a -> [a]
base.List.Nonempty.tail = cases Nonempty _ as -> as
base.List.Nonempty.tail.test
.> view base.List.Nonempty.tail.test
base.List.Nonempty.tail.test : [Result]
base.List.Nonempty.tail.test =
runs
100 'let
a = !nat
as = !(listOf nat)
expect (Nonempty.tail (Nonempty a as) == as)
base.List.Nonempty.toList
.> view base.List.Nonempty.toList
base.List.Nonempty.toList : Nonempty a -> [a]
base.List.Nonempty.toList = cases Nonempty a as -> a +: as
base.List.Nonempty.|+
.> view base.List.Nonempty.|+
(base.List.Nonempty.|+) : [a] -> a -> Nonempty a
(base.List.Nonempty.|+) = cases
[] -> a -> Nonempty a []
x +: xs -> a -> Nonempty x (xs :+ a)
.> view base.List.all.tests.homomorphism
base.List.all.tests.homomorphism : [Result]
base.List.all.tests.homomorphism =
use List ++
runs
100
'(laws.homomorphism
(listOf gen.boolean) (List.all id) (++) (a b -> a && b))
.> view base.List.any.tests.deMorgan
base.List.any.tests.deMorgan : [Result]
base.List.any.tests.deMorgan =
runs
100 'let
bs = !(listOf gen.boolean)
expect (any id bs == not (List.all not bs))
base.List.any.tests.homomorphism
.> view base.List.any.tests.homomorphism
base.List.any.tests.homomorphism : [Result]
base.List.any.tests.homomorphism =
use List ++
runs
100
'(laws.homomorphism
(listOf gen.boolean) (any id) (++) (a b -> a || b))
.> view base.List.cons
-- base.List.+: is built-in.
base.List.contains
.> view base.List.contains
base.List.contains : a -> [a] -> Boolean
base.List.contains a as = isSome <| indexOf a as
base.List.contains.tests.prop1
.> view base.List.contains.tests.prop1
base.List.contains.tests.prop1 : [Result]
base.List.contains.tests.prop1 =
go _ =
use List ++
a = !(listOf nat)
b = !nat
c = !(listOf nat)
expect (elem b (a :+ b ++ c))
runs 100 go
base.List.deleteAt
.> view base.List.deleteAt
base.List.deleteAt : Nat -> [a] -> [a]
base.List.deleteAt n as =
use List ++
use Nat +
slice 0 n as ++ slice (n + 1) (List.size as) as
.> view base.List.distinct
base.List.distinct : [a] -> [a]
base.List.distinct as =
go i seen acc =
match List.at i as with
None -> acc
Some a ->
use Nat +
if Set.contains a seen then go (i + 1) seen acc
else go (i + 1) (Set.insert a seen) (acc :+ a)
go 0 Set.empty []
base.List.drop
.> view base.List.drop
-- base.List.drop is built-in.
.> view base.List.filter
base.List.filter : (a ->{π} Boolean) -> [a] ->{π} [a]
base.List.filter pred as =
List.foldl
(acc a -> (if pred a then acc :+ a else acc)) [] as
.> view base.List.filterMap
base.List.filterMap : (a ->{π} Optional b) -> [a] ->{π} [b]
base.List.filterMap f =
List.flatMap
(e ->
(match f e with
None -> []
Some v -> [v]))
.> view base.List.foldb
base.List.foldb : (a -> b) -> (b -> b -> b) -> b -> [a] -> b
base.List.foldb f op z as =
use List size
if size as == 0 then z
else
if size as == 1 then f (unsafeAt 0 as)
else
match halve as with
(left, right) ->
use base.List foldb
op (foldb f op z left) (foldb f op z right)
base.List.foldl
.> view base.List.foldl
base.List.foldl : (b ->{π} a ->{π} b) -> b -> [a] ->{π} b
base.List.foldl f b as =
go b i =
match List.at i as with
None -> b
Some a ->
use Nat +
go (f b a) (i + 1)
go b 0
base.List.foldr
.> view base.List.foldr
base.List.foldr : (a ->{e} b ->{e} b) -> b -> [a] ->{e} b
base.List.foldr f b as =
go b i =
next = Nat.decrement i
match List.at next as with
Some a | next == 0 -> f a b
Some a -> go (f a b) next
None -> b
go b (List.size as)
.> view base.List.groupBy
base.List.groupBy :
(a ->{e} a ->{e} Boolean) -> [a] ->{e} [Nonempty a]
base.List.groupBy p' = cases
[] -> []
x' +: xs' ->
go p z = cases
[] -> ([], [])
x +: xs ->
match go p x xs with
(ys, zs) ->
if p z x then (x +: ys, zs)
else ([], x +| ys +: zs)
match go p' x' xs' with (ys', zs') -> x' +| ys' +: zs'
.> view base.List.intercalate.tests.size
base.List.intercalate.tests.size : [Result]
base.List.intercalate.tests.size =
go _ =
use List size
expect
let
l = !(listOf nat)
v = !(listOf (listOf nat))
i = intercalate l v
actual = size i
expected =
use Nat * + -
size (List.join v)
+ (size l * truncate0 (size v - 1))
if not (expected == actual) then
bug ("Not equal!", expected, actual, l, v)
else true
runs 100 go
base.List.intersperse
.> view base.List.intersperse
base.List.intersperse : a -> [a] -> [a]
base.List.intersperse sep ls =
prependToAll : a -> [a] -> [a]
prependToAll sep = cases
[] -> []
a +: as ->
use List ++
[sep, a] ++ prependToAll sep as
match ls with
[] -> []
a +: as -> a +: prependToAll sep as
.> view base.List.isInfixOf.tests.prop1
base.List.isInfixOf.tests.prop1 : [Result]
base.List.isInfixOf.tests.prop1 =
go _ =
use List ++
a = !(listOf nat)
b = !(listOf nat)
c = !(listOf nat)
expect (isInfixOf b (a ++ b ++ c))
runs 100 go
base.List.isPrefixOf
.> view base.List.isPrefixOf
base.List.isPrefixOf : [a] -> [a] -> Boolean
base.List.isPrefixOf prefix list =
match prefix with
p +: ps ->
match list with
x +: xs -> (p == x) && (base.List.isPrefixOf ps xs)
[] -> false
[] -> true
base.List.isPrefixOf.tests.prop1
.> view base.List.isPrefixOf.tests.prop1
base.List.isPrefixOf.tests.prop1 : [Result]
base.List.isPrefixOf.tests.prop1 =
go _ =
use List ++
a = !(listOf nat)
b = !(listOf nat)
expect (isPrefixOf a (a ++ b))
runs 100 go
base.List.isPrefixOf.tests.prop2
.> view base.List.isPrefixOf.tests.prop2
base.List.isPrefixOf.tests.prop2 : [Result]
base.List.isPrefixOf.tests.prop2 =
go _ =
use List ++ size
use Universal !=
a = !(listOf nat)
b = !(listOf nat)
c = !(listOf nat)
expect
((size a != size b)
||
(a == b == isPrefixOf a (b ++ c)))
runs 100 go
base.List.isSuffixOf
.> view base.List.isSuffixOf
base.List.isSuffixOf : [a] -> [a] -> Boolean
base.List.isSuffixOf suffix list =
match suffix with
ss :+ s ->
match list with
xs :+ x -> (s == x) && (base.List.isSuffixOf ss xs)
[] -> false
[] -> true
base.List.isSuffixOf.tests.prop1
.> view base.List.isSuffixOf.tests.prop1
base.List.isSuffixOf.tests.prop1 : [Result]
base.List.isSuffixOf.tests.prop1 =
go _ =
use List ++
a = !(listOf nat)
b = !(listOf nat)
expect (isSuffixOf b (a ++ b))
runs 100 go
base.List.isSuffixOf.tests.prop2
.> view base.List.isSuffixOf.tests.prop2
base.List.isSuffixOf.tests.prop2 : [Result]
base.List.isSuffixOf.tests.prop2 =
go _ =
use List ++ size
use Universal !=
a = !(listOf nat)
b = !(listOf nat)
c = !(listOf nat)
expect
((size b != size c)
||
(b == c == isSuffixOf c (a ++ b)))
runs 100 go
base.List.join
.> view base.List.join
base.List.join : [[a]] -> [a]
base.List.join =
use List ++
List.foldl (++) []
base.List.join.tests.associative
.> view base.List.join.tests.associative
base.List.join.tests.associative : [Result]
base.List.join.tests.associative =
use List join
runs
100 'let
x = !(listOf (listOf (listOf nat)))
expect (join (join x) == join (List.map join x))
base.List.join.tests.homomorphism
.> view base.List.join.tests.homomorphism
base.List.join.tests.homomorphism : [Result]
base.List.join.tests.homomorphism =
use List ++
runs
100 'let
x = !(listOf nat)
y = !(listOf nat)
expect (List.join [x, y] == (x ++ y))
base.List.join.tests.unit
.> view base.List.join.tests.unit
base.List.join.tests.unit : [Result]
base.List.join.tests.unit =
use List join
runs
100 'let
x = !(listOf nat)
expect (join [x] == join (List.map (a -> [a]) x))
.> view base.List.lefts.tests.ex1
base.List.lefts.tests.ex1 : [Result]
base.List.lefts.tests.ex1 =
check
let
actual =
lefts
[ Left 2,
Right "Hello",
Left 10,
Right "Hello again" ]
expected = [2, 10]
assert
(actual == expected)
("Not equal!", actual, expected)
true
base.List.map
.> view base.List.map
base.List.map : (a ->{π} b) -> [a] ->{π} [b]
base.List.map f a =
go i as acc =
match List.at i as with
None -> acc
Some a ->
use Nat +
go (i + 1) as (acc :+ f a)
go 0 a []
base.List.mapIndexed
.> view base.List.mapIndexed
base.List.mapIndexed : (Nat ->{π} a ->{π} b) -> [a] ->{π} [b]
base.List.mapIndexed f xs =
at2
(List.foldl
(acc e ->
(match acc with
(c, res) ->
use Nat +
(c + 1, res :+ f c e))) (0, []) xs)
.> view base.List.maximum
base.List.maximum : [a] -> Optional a
base.List.maximum list =
go x = cases
[] -> Some x
y +: ys | y > x -> go y ys
_ +: ys -> go x ys
match list with
x +: xs -> go x xs
[] -> None
.> view base.List.minimum
base.List.minimum : [a] -> Optional a
base.List.minimum list =
go x = cases
[] -> Some x
y +: ys | y < x -> go y ys
_ +: ys -> go x ys
match list with
x +: xs -> go x xs
[] -> None
.> view base.List.nonEmptySubsequences
base.List.nonEmptySubsequences : [a] -> [Nonempty a]
base.List.nonEmptySubsequences list =
f : a -> Nonempty a -> [Nonempty a] -> [Nonempty a]
f x ys r = ys +: (Nonempty.cons x ys +: r)
match list with
[] -> []
x +: xs ->
Nonempty.singleton x
+: List.foldr
(f x) [] (base.List.nonEmptySubsequences xs)
.> view base.List.powerslice.tests.prop1
base.List.powerslice.tests.prop1 : [Result]
base.List.powerslice.tests.prop1 =
go _ =
use List ++
a = !(listOf nat)
b = !(listOf nat)
c = !(listOf nat)
expect (elem b (powerslice (a ++ b ++ c)))
runs 100 go
.> view base.List.range
base.List.range : Nat -> Nat -> [Nat]
base.List.range start stopExclusive =
f i =
if i < stopExclusive then
use Nat +
Some (i, i + 1)
else None
unfold start f
.> view base.List.replace
base.List.replace : Nat -> a -> [a] -> [a]
base.List.replace i a as =
use List ++
use Nat +
List.take i as ++ [a] ++ List.drop (i + 1) as
base.List.replicate
.> view base.List.replicate
base.List.replicate : Nat -> '{e} a ->{e} [a]
base.List.replicate n op =
unfold
n
(n -> (if n == 0 then None else Some (!op, Nat.drop n 1)))
base.List.replicate.test
.> view base.List.replicate.test
base.List.replicate.test : [Result]
base.List.replicate.test =
runs
100 'let
n = !nat
h = cases
{ask -> k} -> handle !k with h
{ a } -> a
units : [()]
units = handle replicate n 'ask with h
expect (List.size units == n)
base.List.reverse
.> view base.List.reverse
base.List.reverse : [a] -> [a]
base.List.reverse as = List.foldl (acc a -> a +: acc) [] as
.> view base.List.rights.tests.ex1
base.List.rights.tests.ex1 : [Result]
base.List.rights.tests.ex1 =
check
let
actual =
rights
[ Left 2,
Right "Hello",
Left 10,
Right "Hello again" ]
expected = ["Hello", "Hello again"]
assert
(actual == expected)
("Not equal!", actual, expected)
true
base.List.scanl
.> view base.List.scanl
base.List.scanl :
(b ->{e} a ->{e} b) -> b -> [a] ->{e} Nonempty b
base.List.scanl f initial values =
go acc f q = cases
[] -> acc
x +: xs ->
next = f q x
go (Nonempty.snoc acc next) f next xs
go (Nonempty.singleton initial) f initial values
.> view base.List.scanl.examples.ex5
base.List.scanl.examples.ex5 : Nonempty Nat
base.List.scanl.examples.ex5 =
use Nat * +
List.scanl (x y -> 2 * x + y) 4 [1, 2, 3]
base.List.scanl.test
.> view base.List.scanl.test
base.List.scanl.test : [Result]
base.List.scanl.test =
use Nat +
runs
100
'let
xs = !(listOf nat)
expect
( List.scanl (x y -> y + 1) 0 xs
== (0 +| List.map (x -> x + 1) xs))
base.List.scanr
.> view base.List.scanr
base.List.scanr :
(a ->{e} b ->{e} b) -> b -> [a] ->{e} Nonempty b
base.List.scanr f initial values =
go : Nonempty b -> (a ->{e} b ->{e} b) -> b -> [a] -> Nonempty b
go acc f q = cases
[] -> acc
xs :+ x ->
next = f x q
go (Nonempty.cons next acc) f (f x q) xs
go (Nonempty.singleton initial) f initial values
.> view base.List.split
base.List.split : (a ->{e} Boolean) -> [a] ->{e} [[a]]
base.List.split f = cases
[] -> [[]]
x +: xs | f x -> [] +: base.List.split f xs
x +: xs ->
match base.List.split f xs with y +: ys -> x +: y +: ys
.> view base.List.stripPrefix
base.List.stripPrefix : [a] -> [a] -> Optional [a]
base.List.stripPrefix prefix list =
match splitAt (List.size prefix) list with
(p, s) -> if p == prefix then Some s else None
.> view base.List.tails
base.List.tails : [a] -> [[a]]
base.List.tails l =
l +: (match l with
[] -> []
_ +: xs -> base.List.tails xs)
base.List.take
.> view base.List.take
-- base.List.take is built-in.
base.List.takeWhile
.> view base.List.takeWhile
base.List.takeWhile : (a ->{e} Boolean) -> [a] ->{e} [a]
base.List.takeWhile f xs =
go acc = cases
x +: xs | f x -> go (acc :+ x) xs
_ -> acc
go [] xs
.> view base.List.uncons
base.List.uncons : [a] -> Optional (a, [a])
base.List.uncons as =
match List.at 0 as with
None -> None
Some a -> Some (a, List.drop 1 as)
base.List.unfold
.> view base.List.unfold
base.List.unfold : s -> (s ->{π} Optional (a, s)) ->{π} [a]
base.List.unfold s0 f =
go f s acc =
match f s with
None -> acc
Some (a, s) -> go f s (acc :+ a)
go f s0 []
base.List.unsafeAt
.> view base.List.unsafeAt
base.List.unsafeAt : Nat -> [a] -> a
base.List.unsafeAt n as =
match List.at n as with
Some a -> a
None -> watch "oh noes" (base.List.unsafeAt n as)
base.List.unsnoc
.> view base.List.unsnoc
base.List.unsnoc : [a] -> Optional ([a], a)
base.List.unsnoc as =
i = List.size (List.drop 1 as)
match List.at i as with
None -> None
Some a -> Some (List.take i as, a)
base.List.zip
.> view base.List.zip
base.List.zip : [a] -> [b] -> [(a, b)]
base.List.zip as bs =
go acc i =
use List at
match (at i as, at i bs) with
(None, _) -> acc
(_, None) -> acc
(Some a, Some b) ->
use Nat +
go (acc :+ (a, b)) (i + 1)
go [] 0
base.List.zipWith
.> view base.List.zipWith
base.List.zipWith : (a ->{π} b ->{π} c) -> [a] -> [b] ->{π} [c]
base.List.zipWith f a b =
go acc as bs =
match (as, bs) with
(ah +: at, bh +: bt) -> go (acc :+ f ah bh) at bt
_ -> acc
go [] a b
base.List.zipWith.tests.edge1
.> view base.List.zipWith.tests.edge1
base.List.zipWith.tests.edge1 : [Result]
base.List.zipWith.tests.edge1 =
check
let
actual =
use Nat +
zipWith (+) [1, 5, 10] []
expected = []
if not (actual == expected) then
bug ("Not equal!", actual, expected)
else true
base.List.zipWith.tests.edge2
.> view base.List.zipWith.tests.edge2
base.List.zipWith.tests.edge2 : [Result]
base.List.zipWith.tests.edge2 =
check
let
actual =
use Nat +
zipWith (+) [] []
expected = []
if not (actual == expected) then
bug ("Not equal!", actual, expected)
else true
.> view base.Map.Map
type base.Map k v = Map [k] [v]
base.Map.contains
.> view base.Map.contains
base.Map.contains : k -> Map k v -> Boolean
base.Map.contains k = cases
Map ks _ ->
match anyIndexOf k ks with
None -> false
_ -> true
base.Map.delete
.> view base.Map.delete
base.Map.delete : k -> Map k v -> Map k v
base.Map.delete k = cases
Map ks vs ->
i = lubIndexOf k ks
Map (deleteAt i ks) (deleteAt i vs)
base.Map.delete.test
.> view base.Map.delete.test
base.Map.delete.test : [Result]
base.Map.delete.test =
runs
100
'let
k = !nat
expect
(not (Map.contains k (Map.delete k !(mapOf nat nat))))
base.Map.empty
.> view base.Map.empty
base.Map.empty : Map k v
base.Map.empty = Map [] []
base.Map.fromList
.> view base.Map.fromList
base.Map.fromList : [(k, v)] -> Map k v
base.Map.fromList kvs =
go acc i =
match List.at i kvs with
None -> acc
Some (k, v) ->
use Nat +
go (Map.insert k v acc) (i + 1)
go Map.empty 0
base.Map.insert
.> view base.Map.insert
base.Map.insert : k -> v -> Map k v -> Map k v
base.Map.insert k v = cases
Map ks vs ->
i = lubIndexOf k ks
match List.at i ks with
Some k' ->
if k == k' then Map ks (replace i v vs)
else
use List insert
Map (insert i k ks) (insert i v vs)
None -> Map (ks :+ k) (vs :+ v)
base.Map.intersect
.> view base.Map.intersect
base.Map.intersect : Map k v -> Map k v -> Map k v
base.Map.intersect = intersectWith (_ v -> v)
base.Map.intersectWith
.> view base.Map.intersectWith
base.Map.intersectWith :
(v -> v -> v2) -> Map k v -> Map k v -> Map k v2
base.Map.intersectWith f m1 m2 =
match (m1, m2) with
(Map k1 v1, Map k2 v2) ->
go i j ko vo =
use List at
match (at i k1, at j k2) with
(None, _) -> Map ko vo
(_, None) -> Map ko vo
(Some kx, Some ky) ->
if kx == ky then
use Nat +
go
(i + 1)
(j + 1)
(ko :+ kx)
(vo :+ f (unsafeAt i v1) (unsafeAt j v2))
else
if kx < ky then
i' = lubIndexOf' ky i k1
go i' j ko vo
else
j' = lubIndexOf' kx j k2
go i j' ko vo
go 0 0 [] []
base.Map.keys
.> view base.Map.keys
base.Map.keys : Map k v -> [k]
base.Map.keys = cases Map ks _ -> ks
base.Map.lookup
.> view base.Map.lookup
base.Map.lookup : k -> Map k v -> Optional v
base.Map.lookup k = cases
Map ks vs ->
match anyIndexOf k ks with
None -> None
Some i -> List.at i vs
base.Map.map
.> view base.Map.map
base.Map.map : (v ->{π} v2) -> Map k v ->{π} Map k v2
base.Map.map f m = Map (keys m) (List.map f (values m))
base.Map.mapKeys
.> view base.Map.mapKeys
base.Map.mapKeys : (k ->{π} k2) -> Map k v ->{π} Map k2 v
base.Map.mapKeys f m = Map (List.map f (keys m)) (values m)
base.Map.singleton
.> view base.Map.singleton
base.Map.singleton : k -> v -> Map k v
base.Map.singleton k v = Map [k] [v]
base.Map.size
.> view base.Map.size
base.Map.size : Map k v -> Nat
base.Map.size s = List.size (keys s)
base.Map.toList
.> view base.Map.toList
base.Map.toList : Map k v -> [(k, v)]
base.Map.toList m = zip (keys m) (values m)
base.Map.union
.> view base.Map.union
base.Map.union : Map k v -> Map k v -> Map k v
base.Map.union = Map.unionWith (_ v -> v)
base.Map.unionWith
.> view base.Map.unionWith
base.Map.unionWith :
(v ->{π} v ->{π} v) -> Map k v -> Map k v ->{π} Map k v
base.Map.unionWith f m1 m2 =
match (m1, m2) with
(Map k1 v1, Map k2 v2) ->
go i j ko vo =
use List ++ at drop
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) ->
if kx == ky then
use Nat +
go
(i + 1)
(j + 1)
(ko :+ kx)
(vo :+ 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 [] []
base.Map.values
.> view base.Map.values
base.Map.values : Map k v -> [v]
base.Map.values = cases Map _ vs -> vs
base.Multimap.insert
.> view base.Multimap.insert
base.Multimap.insert : k -> v -> Map k [v] -> Map k [v]
base.Multimap.insert k v m =
use Map insert
match Map.lookup k m with
None -> insert k [v] m
Some vs -> insert k (vs :+ v) m
base.Multimap.lookup
.> view base.Multimap.lookup
base.Multimap.lookup : k -> Map k [v] -> [v]
base.Multimap.lookup k m = orDefault [] (Map.lookup k m)
base.Nat
.> view base.Nat
-- base.Nat is built-in.
base.Nat.*
.> view base.Nat.*
-- base.Nat.* is built-in.
base.Nat.+
.> view base.Nat.+
-- base.Nat.+ is built-in.
base.Nat.-
.> view base.Nat.-
(base.Nat.-) : Nat -> Nat -> Int
(base.Nat.-) = sub
base.Nat./
.> view base.Nat./
-- base.Nat./ is built-in.
base.Nat.and
.> view base.Nat.and
-- base.Nat.and is built-in.
base.Nat.complement
.> view base.Nat.complement
-- base.Nat.complement is built-in.
base.Nat.decrement
.> view base.Nat.decrement
base.Nat.decrement : Nat -> Nat
base.Nat.decrement n = Nat.drop n 1
.> view base.Nat.inRange.test
base.Nat.inRange.test : [Result]
base.Nat.inRange.test =
runs
100
'let
x = !nat
y = !nat
z = !nat
match sort [x, y, z] with
[x, y, z] -> expect ((Nat.inRange x z y) || (z == y))
base.Nat.increment
.> view base.Nat.increment
-- base.Nat.increment is built-in.
base.Nat.isEven
.> view base.Nat.isEven
-- base.Nat.isEven is built-in.
base.Nat.isOdd
.> view base.Nat.isOdd
-- base.Nat.isOdd is built-in.
base.Nat.leadingZeros
.> view base.Nat.leadingZeros
-- base.Nat.leadingZeros is built-in.
base.Nat.lt
.> view base.Nat.lt
-- base.Nat.lt is built-in.
base.Nat.lteq
.> view base.Nat.lteq
-- base.Nat.lteq is built-in.
.> view base.Nat.shiftLeft
-- base.Nat.shiftLeft is built-in.
base.Nat.shiftRight
.> view base.Nat.shiftRight
-- base.Nat.shiftRight is built-in.
base.Nat.sub
.> view base.Nat.sub
-- base.Nat.sub is built-in.
base.Nat.toFloat
.> view base.Nat.toFloat
-- base.Nat.toFloat is built-in.
base.Nat.toInt
.> view base.Nat.toInt
-- base.Nat.toInt is built-in.
base.Nat.toText
.> view base.Nat.toText
-- base.Nat.toText is built-in.
base.Nat.trailingZeros
.> view base.Nat.trailingZeros
-- base.Nat.trailingZeros is built-in.
base.Nat.xor
.> view base.Nat.xor
-- base.Nat.xor is built-in.
base.Optional
.> view base.Optional
type base.Optional a = None | Some a
base.Optional.None
.> view base.Optional.None
type base.Optional a = None | Some a
base.Optional.Some
.> view base.Optional.Some
type base.Optional a = None | Some a
base.Optional.flatMap
.> view base.Optional.flatMap
base.Optional.flatMap :
(a ->{π} Optional b) -> Optional a ->{π} Optional b
base.Optional.flatMap f = cases
None -> None
Some a -> f a
.> view base.Optional.isSome
base.Optional.isSome : Optional a -> Boolean
base.Optional.isSome = cases
Some a -> true
None -> false
base.Optional.map
.> view base.Optional.map
base.Optional.map : (a ->{π} b) -> Optional a ->{π} Optional b
base.Optional.map f = cases
None -> None
Some a -> Some (f a)
base.Optional.map2
.> view base.Optional.map2
base.Optional.map2 :
(a ->{π} b ->{π} c)
-> Optional a
-> Optional b
->{π} Optional c
base.Optional.map2 f oa ob =
Optional.flatMap (a -> Optional.map (f a) ob) oa
base.Optional.orDefault
.> view base.Optional.orDefault
base.Optional.orDefault : a -> Optional a -> a
base.Optional.orDefault a = cases
None -> a
Some a -> a
base.Optional.orElse
.> view base.Optional.orElse
base.Optional.orElse : Optional a -> Optional a -> Optional a
base.Optional.orElse a b =
match a with
None -> b
Some _ -> a
base.Optional.toAbort
.> view base.Optional.toAbort
base.Optional.toAbort : Optional a ->{Abort} a
base.Optional.toAbort = cases
None -> abort
Some a -> a
base.Ordering
.> view base.Ordering
unique type base.Ordering = Less | Equal | Greater
base.Ordering.Equal
.> view base.Ordering.Equal
unique type base.Ordering = Less | Equal | Greater
base.Ordering.Greater
.> view base.Ordering.Greater
unique type base.Ordering = Less | Equal | Greater
base.Ordering.Less
.> view base.Ordering.Less
unique type base.Ordering = Less | Equal | Greater
base.Ordering.andThen
.> view base.Ordering.andThen
base.Ordering.andThen : Ordering -> Ordering -> Ordering
base.Ordering.andThen x y =
match x with
Equal -> y
x -> x
base.Ordering.andThen.example.ex1
.> view base.Ordering.andThen.example.ex1
base.Ordering.andThen.example.ex1 : Ordering
base.Ordering.andThen.example.ex1 =
x = [5, 6, 7]
y = [5, 9, 7, 6]
Ordering.andThen
(compareOn List.head x y) (compareOn List.last x y)
base.Request
.> view base.Request
-- base.Request is built-in.
base.Search.anyIndexOf
.> view base.Search.anyIndexOf
base.Search.anyIndexOf : a -> [a] -> Optional Nat
base.Search.anyIndexOf a s =
ao = Some a
exact (i -> compare ao (List.at i s)) 0 (List.size s)
.> view base.Search.elem.tests.positive
base.List.contains.tests.prop1 : [Result]
base.List.contains.tests.prop1 =
go _ =
use List ++
a = !(listOf nat)
b = !nat
c = !(listOf nat)
expect (elem b (a :+ b ++ c))
runs 100 go
base.Search.exact
.> view base.Search.exact
base.Search.exact :
(Nat ->{π} Int) -> Nat -> Nat ->{π} Optional Nat
base.Search.exact hit bot top =
if bot >= top then None
else
use Nat +
use base.Search exact
mid =
use Nat /
bot + top / 2
match hit mid with
+0 -> Some mid
-1 -> exact hit bot mid
+1 -> exact hit (mid + 1) top
base.Search.indexOf
.> view base.Search.indexOf
base.Search.indexOf : a -> [a] -> Optional Nat
base.Search.indexOf a as =
go : Nat -> [a] -> Optional Nat
go index = cases
[] -> None
head +: tail | head == a -> Some index
_ +: tail ->
use Nat +
go (index + 1) tail
go 0 as
.> view base.Search.lub
base.Search.lub : (Nat ->{π} Int) -> Nat -> Nat ->{π} Nat
base.Search.lub hit bot top =
if bot >= top then top
else
use Nat +
use base.Search lub
mid =
use Nat /
bot + top / 2
match hit mid with
+0 -> mid
-1 -> lub hit bot mid
+1 -> lub hit (mid + 1) top
base.Search.lubIndexOf
.> view base.Search.lubIndexOf
base.Search.lubIndexOf : a -> [a] -> Nat
base.Search.lubIndexOf a s = lubIndexOf' a 0 s
base.Search.lubIndexOf'
.> view base.Search.lubIndexOf'
base.Search.lubIndexOf' : a -> Nat -> [a] -> Nat
base.Search.lubIndexOf' a start s =
ao = Some a
lub (i -> compare ao (List.at i s)) start (List.size s)
.> view base.Search.notElem
base.Search.notElem : a -> [a] -> Boolean
base.Search.notElem a as = not <| elem a as
base.Set
.> view base.Set
type base.Set a = Set (Map a ())
base.Set.Set
.> view base.Set.Set
type base.Set a = Set (Map a ())
base.Set.contains
.> view base.Set.contains
base.Set.contains : k -> Set k -> Boolean
base.Set.contains k = cases Set m -> Map.contains k m
base.Set.delete
.> view base.Set.delete
base.Set.delete : k -> Set k -> Set k
base.Set.delete k s = Set (Map.delete k (underlying s))
base.Set.delete.test
.> view base.Set.delete.test
base.Set.delete.test : [Result]
base.Set.delete.test =
runs
100 'let
xs = !(setOf nat)
x = !nat
expect (not (Set.contains x (Set.delete x xs)))
base.Set.empty
.> view base.Set.empty
base.Set.empty : Set k
base.Set.empty = Set Map.empty
base.Set.flatMap
.> view base.Set.flatMap
base.Set.flatMap : (a ->{e} Set b) -> Set a ->{e} Set b
base.Set.flatMap f as =
Set.foldl (b a -> Set.union b (f a)) Set.empty as
base.Set.flatMap.tests.associative
.> view base.Set.flatMap.tests.associative
base.Set.flatMap.tests.associative : [Result]
base.Set.flatMap.tests.associative =
use Map lookup
use Set empty
runs
100
'let
xs = !(setOf nat)
ys = !(mapOf nat (setOf nat))
zs = !(mapOf nat (setOf nat))
f x = orDefault empty (lookup x ys)
g y = orDefault empty (lookup y zs)
r =
use Set flatMap
flatMap f (flatMap g xs)
== flatMap (x -> flatMap f (g x)) xs
expect r
base.Set.flatMap.tests.unit
.> view base.Set.flatMap.tests.unit
base.Set.flatMap.tests.unit : [Result]
base.Set.flatMap.tests.unit =
use Set flatMap singleton
runs
100 'let
n = !nat
xs = !(setOf nat)
ys = !(mapOf nat (setOf nat))
f x = orDefault Set.empty (Map.lookup x ys)
left = flatMap f (singleton n) == f n
right = flatMap singleton xs == xs
expect (left && right)
base.Set.flatten
.> view base.Set.flatten
base.Set.flatten : Set (Set b) -> Set b
base.Set.flatten = Set.flatMap id
.> view base.Set.fromList
base.Set.fromList : [k] -> Set k
base.Set.fromList ks =
Set (Map.fromList (List.map (k -> (k, ())) ks))
base.Set.insert
.> view base.Set.insert
base.Set.insert : k -> Set k -> Set k
base.Set.insert k = cases Set s -> Set (!(Map.insert k) s)
base.Set.intersect
.> view base.Set.intersect
base.Set.intersect : Set k -> Set k -> Set k
base.Set.intersect s1 s2 =
Set (Map.intersect (underlying s1) (underlying s2))
base.Set.map
.> view base.Set.map
base.Set.map : (a ->{e} b) -> Set a ->{e} Set b
base.Set.map f s = Set (Map.mapKeys f (underlying s))
base.Set.map.test
.> view base.Set.map.test
base.Set.map.test : [Result]
base.Set.map.test =
use Set map
runs
100 'let
ks = !(setOf nat)
f x =
use Nat *
x * 2
g x =
use Nat +
x + 2
expect (map ( f g) ks == map f (map g ks))
base.Set.singleton
.> view base.Set.singleton
base.Set.singleton : a -> Set a
base.Set.singleton a = Set.insert a Set.empty
base.Set.singleton.test
.> view base.Set.singleton.test
base.Set.singleton.test : [Result]
base.Set.singleton.test =
check
let
s = Set.singleton 0
(Set.contains 0 s) && (Set.size s == 1)
base.Set.size
.> view base.Set.size
base.Set.size : Set k -> Nat
base.Set.size s = Map.size (underlying s)
base.Set.toList
.> view base.Set.toList
base.Set.toList : Set k -> [k]
base.Set.toList = cases Set (Map ks _) -> ks
base.Set.toMap
.> view base.Set.toMap
base.Set.toMap : (k ->{π} v) -> Set k ->{π} Map k v
base.Set.toMap f = cases
Set (Map ks vs) -> Map ks (List.map f ks)
base.Set.underlying
.> view base.Set.underlying
base.Set.underlying : Set k -> Map k ()
base.Set.underlying = cases Set s -> s
base.Set.union
.> view base.Set.union
base.Set.union : Set k -> Set k -> Set k
base.Set.union s1 s2 =
Set (Map.union (underlying s1) (underlying s2))
base.Set.unions
.> view base.Set.unions
base.Set.unions : [Set a] -> Set a
base.Set.unions = List.foldl Set.union Set.empty
.> view base.Store.local
base.Store.local : a -> '{g, Store a} v ->{g, Store a} v
base.Store.local a op =
old = get
put a
res = !op
put old
res
base.Store.local.examples.ex1
.> view base.Store.local.examples.ex1
base.Store.local.examples.ex1 : (Nat, Nat, Nat)
base.Store.local.examples.ex1 =
withInitialValue
1 'let
before = get
during = local 2 'get
after = get
(before, during, after)
.> view base.Store.put
ability base.Store a where
put : a ->{base.Store a} ()
get : {base.Store a} a
base.Store.put.examples.ex1
.> view base.Store.put.examples.ex1
base.Store.put.examples.ex1 : Nat
base.Store.put.examples.ex1 =
withInitialValue
10 'let
put 15
get
base.Store.withInitialValue
.> view base.Store.withInitialValue
base.Store.withInitialValue : a -> '{g, Store a} v ->{g} v
base.Store.withInitialValue init thunk =
handle !thunk with withInitialValue.handler init
base.Store.withInitialValue.handler
.> view base.Store.withInitialValue.handler
base.Store.withInitialValue.handler :
a -> Request (Store a) v -> v
base.Store.withInitialValue.handler init = cases
{ v } -> v
{get -> k} ->
handle k init
with base.Store.withInitialValue.handler init
{put v -> k} ->
handle !k with base.Store.withInitialValue.handler v
base.Store.withInitialValue.laws.law1
.> view base.Store.withInitialValue.laws.law1
base.Store.withInitialValue.laws.law1 : a ->{Store a} Test
base.Store.withInitialValue.laws.law1 v =
expect
(v == let
put v
get)
.> view base.Stream
ability base.Stream e where emit : e ->{base.Stream e} ()
base.Stream.emit
.> view base.Stream.emit
ability base.Stream e where emit : e ->{base.Stream e} ()
base.Stream.range
.> view base.Stream.range
base.Stream.range : Nat -> Nat ->{Stream Nat} ()
base.Stream.range n m =
if n >= m then ()
else
use Nat +
emit n
base.Stream.range (n + 1) m
.> view base.Stream.toList
base.Stream.toList : '{e, Stream a} () ->{e} [a]
base.Stream.toList s = handle !s with toList.handler
base.Stream.toList.handler
.> view base.Stream.toList.handler
base.Stream.toList.handler : Request {Stream a} () -> [a]
base.Stream.toList.handler =
h : [a] -> Request {Stream a} () -> [a]
h acc = cases
{emit e -> resume} ->
handle !resume
with
use List ++
h (acc ++ [e])
{ u } -> acc
h []
base.Test.Result
.> view base.Test.Result
unique type base.Test.Result = Result.Fail Text | Ok Text
base.Test.Result.Fail
.> view base.Test.Result.Fail
unique type base.Test.Result = Result.Fail Text | Ok Text
base.Test.Result.Ok
.> view base.Test.Result.Ok
unique type base.Test.Result = Result.Fail Text | Ok Text
base.Text
.> view base.Text
-- base.Text is built-in.
base.Text.!=
.> view base.Text.!=
-- base.Text.!= is built-in.
base.Text.++
.> view base.Text.++
-- base.Text.++ is built-in.
base.Text.drop
.> view base.Text.drop
-- base.Text.drop is built-in.
base.Text.empty
.> view base.Text.empty
-- base.Text.empty is built-in.
base.Text.eq
.> view base.Text.eq
-- base.Text.eq is built-in.
base.Text.fromCharList
.> view base.Text.fromCharList
-- base.Text.fromCharList is built-in.
base.Text.gt
.> view base.Text.gt
-- base.Text.gt is built-in.
base.Text.gteq
.> view base.Text.gteq
-- base.Text.gteq is built-in.
base.Text.lt
.> view base.Text.lt
-- base.Text.lt is built-in.
base.Text.lteq
.> view base.Text.lteq
-- base.Text.lteq is built-in.
base.Text.size
.> view base.Text.size
-- base.Text.size is built-in.
base.Text.split
.> view base.Text.split
base.Text.split : Char -> Text -> [Text]
base.Text.split separator text =
go acc rest =
match indexOf separator rest with
None -> acc :+ fromCharList rest
Some n ->
use Nat +
go
(acc :+ fromCharList (List.take n rest))
(List.drop (n + 1) rest)
if text == "" then [] else go [] (toCharList text)
.> view base.Text.take
-- base.Text.take is built-in.
base.Text.toCharList
.> view base.Text.toCharList
-- base.Text.toCharList is built-in.
base.Text.uncons
.> view base.Text.uncons
-- base.Text.uncons is built-in.
base.Text.unsnoc
.> view base.Text.unsnoc
-- base.Text.unsnoc is built-in.
base.Trie
.> view base.Trie
type base.Trie k v = Trie (Optional v) (Map k (base.Trie k v))
base.Trie.Trie
.> view base.Trie.Trie
type base.Trie k v = Trie (Optional v) (Map k (base.Trie k v))
base.Trie.empty
.> view base.Trie.empty
base.Trie.empty : Trie k v
base.Trie.empty = Trie None Map.empty
base.Trie.head
.> view base.Trie.head
base.Trie.head : Trie k v -> Optional v
base.Trie.head = cases Trie head _ -> head
base.Trie.head.modify
.> view base.Trie.head.modify
base.Trie.head.modify :
(Optional v ->{π} Optional v) -> Trie k v ->{π} Trie k v
base.Trie.head.modify f = cases
Trie head tail -> Trie (f head) tail
base.Trie.head.set
.> view base.Trie.head.set
base.Trie.head.set : Optional v -> Trie k v -> Trie k v
base.Trie.head.set head1 = cases
Trie _ tail -> Trie head1 tail
base.Trie.insert
.> view base.Trie.insert
base.Trie.insert : [k] -> v -> Trie k v -> Trie k v
base.Trie.insert path v t =
Trie.unionWith const (Trie.singleton path v) t
base.Trie.lookup
.> view base.Trie.lookup
base.Trie.lookup : [k] -> Trie k v -> Optional v
base.Trie.lookup path t =
match path with
[] -> Trie.head t
p +: ps ->
Optional.flatMap
(base.Trie.lookup ps) (Map.lookup p (Trie.tail t))
base.Trie.map
.> view base.Trie.map
base.Trie.map : (v1 -> v2) -> Trie k v1 -> Trie k v2
base.Trie.map f t =
Trie
(Optional.map f (Trie.head t))
(Map.map (base.Trie.map f) (Trie.tail t))
base.Trie.mapKeys
.> view base.Trie.mapKeys
base.Trie.mapKeys : (k1 -> k2) -> Trie k1 v -> Trie k2 v
base.Trie.mapKeys f t =
Trie
(Trie.head t)
(Map.mapKeys
f (Map.map (base.Trie.mapKeys f) (Trie.tail t)))
base.Trie.singleton
.> view base.Trie.singleton
base.Trie.singleton : [k] -> v -> Trie k v
base.Trie.singleton path v =
match path with
[] -> Trie (Some v) Map.empty
k +: ks ->
Trie None (Map.fromList [(k, base.Trie.singleton ks v)])
base.Trie.tail
.> view base.Trie.tail
base.Trie.tail : Trie k v -> Map k (Trie k v)
base.Trie.tail = cases Trie _ tail -> tail
base.Trie.tail.modify
.> view base.Trie.tail.modify
base.Trie.tail.modify :
(Map k111 (Trie k111 v) ->{π} Map k (Trie k v))
-> Trie k111 v
->{π} Trie k v
base.Trie.tail.modify f = cases
Trie head tail -> Trie head (f tail)
base.Trie.tail.set
.> view base.Trie.tail.set
base.Trie.tail.set :
Map k (Trie k v) -> Trie k111 v -> Trie k v
base.Trie.tail.set tail1 = cases
Trie head _ -> Trie head tail1
base.Trie.union
.> view base.Trie.union
base.Trie.union : Trie k v ->{π} Trie k v ->{π} Trie k v
base.Trie.union = Trie.unionWith const
base.Trie.unionWith
.> view base.Trie.unionWith
base.Trie.unionWith :
(v -> v -> v) -> Trie k v -> Trie k v -> Trie k v
base.Trie.unionWith f t1 t2 =
use Trie head tail
h1 = head t1
h2 = head t2
Trie
(orElse (orElse (map2 f h1 h2) h1) h2)
(Map.unionWith (base.Trie.unionWith f) (tail t1) (tail t2))
base.Tuple
.> view base.Tuple
type base.Tuple a b = Cons a b
base.Tuple.Cons
.> view base.Tuple.Cons
type base.Tuple a b = Cons a b
base.Tuple.at1
.> view base.Tuple.at1
base.Tuple.at1 : Tuple a b -> a
base.Tuple.at1 = cases Cons a _ -> a
.> view base.Tuple.pair
base.Tuple.pair : a -> b -> (a, b)
base.Tuple.pair a b = (a, b)
base.Tuple.tests.ex1
.> view base.Tuple.tests.ex1
base.Tuple.tests.ex1 : [Result]
base.Tuple.tests.ex1 =
check
let
tuple : (Text, Nat, Text)
tuple = ("Hello", 3, "Tuple")
actual =
use Text ++
at1 tuple ++ Nat.toText (at2 tuple) ++ at3 tuple
expected = "Hello3Tuple"
actual == expected
base.Tuple.tests.ex2
.> view base.Tuple.tests.ex2
base.Tuple.tests.ex2 : [Result]
base.Tuple.tests.ex2 =
check
let
pythagoras : (Nat, Nat, Nat)
pythagoras = (3, 4, 5)
square n =
use Nat *
n * n
match pythagoras with
(a, b, c) ->
use Nat +
square a + square b == square c
base.Unit
.> view base.Unit
type base.Unit = Unit
base.Unit.Unit
.> view base.Unit.Unit
type base.Unit = Unit
base.Universal.!=
.> view base.Universal.!=
(base.Universal.!=) : a -> a -> Boolean
a base.Universal.!= b = not (a == b)
base.Universal.<
.> view base.Universal.<
-- base.Universal.< is built-in.
base.Universal.<=
.> view base.Universal.<=
-- base.Universal.<= is built-in.
base.Universal.==
.> view base.Universal.==
-- base.Universal.== is built-in.
base.Universal.>
.> view base.Universal.>
-- base.Universal.> is built-in.
base.Universal.>=
.> view base.Universal.>=
-- base.Universal.>= is built-in.
base.Universal.compare
.> view base.Universal.compare
-- base.Universal.compare is built-in.
base.Universal.compareOn
.> view base.Universal.compareOn
base.Universal.compareOn : (a ->{e} x) -> a -> a ->{e} Ordering
base.Universal.compareOn p x y = on ordering p x y
base.Universal.max
.> view base.Universal.max
base.Universal.max : a -> a -> a
base.Universal.max a b = if a > b then a else b
base.Universal.max.tests.absorption
.> view base.Universal.max.tests.absorption
base.Universal.max.tests.absorption : [Result]
base.Universal.max.tests.absorption =
use Universal min
runs 100 '(laws.absorption int min min)
.> view base.Universal.min.tests.partialOrder
base.Universal.min.tests.partialOrder : [Result]
base.Universal.min.tests.partialOrder =
runs
100 'let
x = !int
y = !int
expect (x <= y == (Universal.min x y == x))
base.Universal.ordering
.> view base.Universal.ordering
base.Universal.ordering : a -> a -> Ordering
base.Universal.ordering x y =
c = compare x y
if c < +0 then Less else if c == +0 then Equal else Greater
base.Universal.ordering.doc.snippet1
.> view base.Universal.ordering.doc.snippet1
base.Universal.ordering.doc.snippet1 : Doc
base.Universal.ordering.doc.snippet1 =
[: @Less means the first object is below the second, @Equal means they are the same, and @Greater means the second object is below the first.
Examples:
@ordering 1 2
> @Less
@ordering 2 1
> @Greater
@ordering 4 4
> @Equal
:]
base.Void
.> view base.Void
type base.Void =
base.Weighted
.> view base.Weighted
type base.Weighted a
= Weight Nat 'base.Weighted a
| Yield a (base.Weighted a)
| Weighted.Fail
base.Weighted.<|>
.> view base.Weighted.<|>
(base.Weighted.<|>) : Weighted a -> Weighted a -> Weighted a
m base.Weighted.<|> n =
use Weighted Fail
use base.Weighted <|>
match (m, n) with
(Fail, n) -> n
(Yield x m, n) -> Yield x (m <|> n)
(Weight w m, Fail) -> Weight w m
(Weight w m, Yield x n) -> Yield x (Weight w m <|> n)
(Weight w m, Weight w' n) ->
use Nat drop
if w < w' then Weight w '(!m <|> Weight (drop w' w) n)
else
if w == w' then Weight w '(!m <|> !n)
else Weight w '(Weight (drop w w') m <|> !n)
base.Weighted.Fail
.> view base.Weighted.Fail
type base.Weighted a
= Weight Nat 'base.Weighted a
| Yield a (base.Weighted a)
| Weighted.Fail
base.Weighted.Weight
.> view base.Weighted.Weight
type base.Weighted a
= Weight Nat 'base.Weighted a
| Yield a (base.Weighted a)
| Weighted.Fail
base.Weighted.Yield
.> view base.Weighted.Yield
type base.Weighted a
= Weight Nat 'base.Weighted a
| Yield a (base.Weighted a)
| Weighted.Fail
base.Weighted.append
.> view base.Weighted.append
base.Weighted.append : Weighted a -> Weighted a -> Weighted a
base.Weighted.append w1 w2 =
use base.Weighted append
match w1 with
Weight n k -> Weight n '(append !k w2)
Yield a k -> Yield a (append k w2)
Weighted.Fail -> w2
.> view base.Weighted.flatMap
base.Weighted.flatMap :
(a -> Weighted b) -> Weighted a -> Weighted b
base.Weighted.flatMap f = cases
Weighted.Fail -> Weighted.Fail
Yield x m -> f x <|> base.Weighted.flatMap f m
Weight w m -> Weight w '(base.Weighted.flatMap f !m)
base.Weighted.fromList
.> view base.Weighted.fromList
base.Weighted.fromList : [a] -> Weighted a
base.Weighted.fromList = cases
[] -> Weighted.Fail
a +: as -> yield a <|> weight 1 '(base.Weighted.fromList as)
base.Weighted.ints
.> view base.Weighted.ints
base.Weighted.ints : Weighted Int
base.Weighted.ints =
go n =
yield n
<|> weight
1
'(go
(if n > +0 then negate n
else Int.increment (negate n)))
List.foldl
(a n -> a <|> yield n)
Weighted.Fail
[+0, +1, -1, maxInt, minInt]
<|> go +2
base.Weighted.lists
.> view base.Weighted.lists
base.Weighted.lists : Weighted a -> Weighted [a]
base.Weighted.lists w =
yield []
<|> weight 1 '(mergeWith (+:) w (base.Weighted.lists w))
base.Weighted.map
.> view base.Weighted.map
base.Weighted.map : (a ->{e} b) -> Weighted a ->{e} Weighted b
base.Weighted.map f = cases
Weighted.Fail -> Weighted.Fail
Yield x w -> Yield (f x) (base.Weighted.map f w)
Weight a w -> weight a '(base.Weighted.map f !w)
base.Weighted.mergeWith
.> view base.Weighted.mergeWith
base.Weighted.mergeWith :
(a ->{π} b ->{π} c)
-> Weighted a
-> Weighted b
->{π} Weighted c
base.Weighted.mergeWith f as bs =
Weighted.flatMap (a -> Weighted.map (b -> f a b) bs) as
base.Weighted.nats
.> view base.Weighted.nats
base.Weighted.nats : Weighted Nat
base.Weighted.nats =
go n =
use Nat +
yield n <|> weight 1 '(go (n + 1))
go 0
base.Weighted.sample
.> view base.Weighted.sample
base.Weighted.sample : Nat -> Weighted a -> [a]
base.Weighted.sample n wsa =
if n > 0 then
use base.Weighted sample
match wsa with
Weighted.Fail -> []
Yield a ms -> a +: sample (Nat.drop n 1) ms
Weight _ w -> sample n !w
else []
base.Weighted.weight
.> view base.Weighted.weight
base.Weighted.weight :
Nat ->{e} '{e} Weighted a ->{e} Weighted a
base.Weighted.weight w ws = Weight w ws
base.Weighted.yield
.> view base.Weighted.yield
base.Weighted.yield : a -> Weighted a
base.Weighted.yield a = Yield a Weighted.Fail
base.Year
.> view base.Year
unique type base.Year = Year Nat
base.Year.Year
.> view base.Year.Year
unique type base.Year = Year Nat
.> view base.io.bracket
base.io.bracket :
'{IO} a -> (a ->{IO} b) -> (a ->{IO} c) ->{IO} c
base.io.bracket acquire release what =
rethrow (bracket_ acquire release what)
.> view base.metadata.licenseTypes.bsd2
base.metadata.licenseTypes.bsd2 : LicenseType
base.metadata.licenseTypes.bsd2 =
LicenseType
[:
Redistribution and use in source and binary forms, with or
without modification, are permitted provided that the following
conditions are met:
1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above
copyright notice, this list of conditions and the following
disclaimer in the documentation and/or other materials provided
with the distribution.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT
NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT
SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE
GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
:]
base.metadata.licenseTypes.bsd3
.> view base.metadata.licenseTypes.bsd3
base.metadata.licenseTypes.bsd3 : LicenseType
base.metadata.licenseTypes.bsd3 =
LicenseType
[:
Redistribution and use in source and binary forms, with or
without modification, are permitted provided that the following
conditions are met:
1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above
copyright notice, this list of conditions and the following
disclaimer in the documentation and/or other materials provided
with the distribution.
3. Neither the name of the copyright holder nor the names of
its contributors may be used to endorse or promote products
derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT
NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT
SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE
GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
:]
base.metadata.licenseTypes.mit
.> view base.metadata.licenseTypes.mit
base.metadata.licenseTypes.mit : LicenseType
base.metadata.licenseTypes.mit =
LicenseType
[:
Permission is hereby granted, free of charge, to any person
obtaining a copy of this software and associated documentation
files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify,
merge, publish, distribute, sublicense, and/or sell copies
of the Software, and to permit persons to whom the Software
is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall
be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE
FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.
:]
.> view base.prs.pr1.note1
base.prs.pr1.note1 : Doc
base.prs.pr1.note1 =
[:
This PR syncs base to incorporate all the latest additions to
`.builtin`, including support for assigning authorship and licensing
information to definitions:
```
@[source] Author
@[source] License
```
There are various `@LicenseType` values in the `licenseTypes`
namespace, for instance:
```
@[source] mit
```
Most of the code in base is MIT-licensed, see `@unisoncomputing2020`.
Also see the `metadata.authors` namespace which has the contributors
to this codebase (for instance, `@aryairani`).
:]
base.repeat
.> view base.repeat
base.repeat : Nat -> '{e} a ->{e} ()
base.repeat n op =
if n == 0 then ()
else
!op
base.repeat (Nat.drop n 1) op
base.test.===
.> view base.test.===
(base.test.===) : a -> a -> Boolean
actual base.test.=== expected =
assert
(actual == expected)
("The values being compared are not equal",
actual,
expected)
true
base.test.Gen
.> view base.test.Gen
ability base.test.Gen where
Gen.sample : Weighted a ->{base.test.Gen} a
.> view base.test.Gen.sample
ability base.test.Gen where
Gen.sample : Weighted a ->{base.test.Gen} a
base.test.Gen.toWeighted
.> view base.test.Gen.toWeighted
base.test.Gen.toWeighted : '{e, Gen} a ->{e} Weighted a
base.test.Gen.toWeighted g =
go = cases
{ a } -> yield a
{Gen.sample w -> k} ->
Weighted.flatMap (a -> (handle k a with go)) w
handle !g with go
base.test.Test
.> view base.test.Test
type base.test.Test = Test (Scope -> Report)
base.test.assert
.> view base.test.assert
base.test.assert : Boolean -> e -> a -> a
base.test.assert b e a = if b then a else bug e
base.test.assertEquals
.> view base.test.assertEquals
(base.test.===) : a -> a -> Boolean
actual base.test.=== expected =
assert
(actual == expected)
("The values being compared are not equal",
actual,
expected)
true
base.test.both
.> view base.test.both
base.test.both : Test -> Test -> Test
base.test.both a b =
match (a, b) with
(Test k1, Test k2) ->
Test
(scope ->
r1 = k1 scope
r2 = k2 scope
Report.combine r1 r2)
base.test.cost
.> view base.test.cost
base.test.cost : Nat -> '{Gen} a -> '{Gen} a
base.test.cost n g _ = weight n '(toWeighted g) |> Gen.sample
base.test.expect
.> view base.test.expect
base.test.expect : Boolean -> Test
base.test.expect b = if b then passed else fail
base.test.fail
.> view base.test.fail
base.test.fail : Test
base.test.fail = finished Failed
base.test.failWith
.> view base.test.failWith
base.test.failWith : Text -> Test
base.test.failWith m = label m fail
.> view base.test.gen.atLeastOne
base.test.gen.atLeastOne : '{Gen} a -> '{Gen} Nonempty a
base.test.gen.atLeastOne g =
'let
a = !g
as = !(listOf g)
Nonempty a as
.> view base.test.gen.either
base.test.gen.either : '{Gen} a -> '{Gen} b -> '{Gen} Either a b
base.test.gen.either a b = pick ['(Left !a), '(Right !b)]
base.test.gen.either.test
.> view base.test.gen.either.test
base.test.gen.either.test : [Result]
base.test.gen.either.test =
use Set fromList
g = either gen.boolean (oneOf [0, 1])
actual = fromList (test.sample 10 g)
expected =
fromList [Left false, Right 0, Left true, Right 1]
check (expected == actual)
.> view base.test.gen.mapOf
base.test.gen.mapOf : '{Gen} k -> '{Gen} v -> '{Gen} Map k v
base.test.gen.mapOf k v =
'(Map.fromList !(listOf (pairOf k v)))
.> view base.test.internals.v1.Domain.ints
base.test.internals.v1.Domain.ints : Domain Int
base.test.internals.v1.Domain.ints =
go n =
yield n
<|> weight
1
'(go
(if n > +0 then negate n
else Int.increment (negate n)))
Large
( List.foldl
(a n -> a <|> yield n)
Weighted.Fail
[+0, +1, -1, maxInt, minInt]
<|> go +2)
base.test.internals.v1.Domain.lift2
.> view base.test.internals.v1.Domain.lift2
base.test.internals.v1.Domain.lift2 :
(a ->{π} b ->{π} c) -> Domain a -> Domain b ->{π} Domain c
base.test.internals.v1.Domain.lift2 f da db =
use List size
use Nat +
wa = weighted da
wb = weighted db
wc = mergeWith (a1 a2 -> f a1 a2) wa wb
match (da, db) with
(Small as, Small bs) | size as + size bs < smallSize ->
Small (Weighted.sample smallSize wc)
_ ->
Large wc
.> view base.test.internals.v1.Domain.listsOf
base.test.internals.v1.Domain.listsOf : Domain a -> Domain [a]
base.test.internals.v1.Domain.listsOf d =
Large
(Weighted.lists
(match d with
Small as -> Weighted.fromList as
Large w -> w))
base.test.internals.v1.Domain.map
.> view base.test.internals.v1.Domain.map
base.test.internals.v1.Domain.map :
(a ->{π} b) -> Domain a ->{π} Domain b
base.test.internals.v1.Domain.map f = cases
Large w -> Large (Weighted.map f w)
Small as -> Small (List.map f as)
.> view base.test.internals.v1.Domain.pairs
base.test.internals.v1.Domain.pairs :
Domain a -> Domain (a, a)
base.test.internals.v1.Domain.pairs d =
lift2 (a b -> (a, b)) d d
base.test.internals.v1.Domain.sample
.> view base.test.internals.v1.Domain.sample
base.test.internals.v1.Domain.sample : Nat -> Domain a -> [a]
base.test.internals.v1.Domain.sample n = cases
Large w -> Weighted.sample n w
Small xs -> List.take n xs
.> view base.test.internals.v1.Domain.tuples
base.test.internals.v1.Domain.tuples :
Domain a -> Domain b -> Domain (Tuple a b)
base.test.internals.v1.Domain.tuples = lift2 (a b -> Cons a b)
base.test.internals.v1.Domain.weighted
.> view base.test.internals.v1.Domain.weighted
base.test.internals.v1.Domain.weighted : Domain a -> Weighted a
base.test.internals.v1.Domain.weighted = cases
Small as -> Weighted.fromList as
Large w -> w
base.test.internals.v1.Scope.cons
.> view base.test.internals.v1.Scope.cons
base.test.internals.v1.Scope.cons : Text -> Scope -> Scope
base.test.internals.v1.Scope.cons n =
foldScope ( Scope ((+:) n))
base.test.internals.v1.Status.combine
.> view base.test.internals.v1.Status.combine
base.test.internals.v1.Status.combine :
Status -> Status -> Status
base.test.internals.v1.Status.combine s1 s2 =
use Success combine
match (s1, s2) with
(_, Pending) -> Pending
(Pending, _) -> Pending
(Failed, _) -> Failed
(_, Failed) -> Failed
(Unexpected a, Unexpected b) -> Unexpected (combine a b)
(Unexpected a, _) -> Unexpected a
(_, Unexpected b) -> Unexpected b
(Expected a, Expected b) -> Expected (combine a b)
base.test.internals.v1.Status.pending
.> view base.test.internals.v1.Status.pending
base.test.internals.v1.Status.pending : Status -> Status
base.test.internals.v1.Status.pending = cases
Failed -> Pending
Expected s -> Unexpected s
Unexpected s -> Pending
Pending -> Pending
base.test.internals.v1.Success.combine
.> view base.test.internals.v1.Success.combine
base.test.internals.v1.Success.combine :
Success -> Success -> Success
base.test.internals.v1.Success.combine s1 s2 =
match (s1, s2) with
(Passed n, Passed m) ->
use Nat +
Passed (n + m)
(Passed n, Proved) -> Passed n
(Proved, Passed n) -> Passed n
(Proved, Proved) -> Proved
base.test.internals.v1.Test.Report
.> view base.test.internals.v1.Test.Report
type base.test.internals.v1.Test.Report
= Report (Trie Text Status)
base.test.internals.v1.Test.Report.Report
.> view base.test.internals.v1.Test.Report.Report
type base.test.internals.v1.Test.Report
= Report (Trie Text Status)
.> view base.test.internals.v1.Test.Report.toCLIResult
base.test.internals.v1.Test.Report.toCLIResult :
Report -> [Result]
base.test.internals.v1.Test.Report.toCLIResult r =
use Text ++
descend scope = cases
(k, t) ->
use Text !=
go ((if scope != "" then scope ++ "." else "") ++ k) t
convert : Text -> Status -> Result
convert scope = cases
Failed -> Result.Fail scope
Expected (Passed n) ->
Ok (scope ++ " : Passed " ++ Nat.toText n ++ " tests.")
Expected Proved -> Ok (scope ++ " : Proved.")
go : Text -> Trie Text Status -> [Result]
go scope t =
rest = List.flatMap (descend scope) (Map.toList (Trie.tail t))
match Trie.head t with
Some status -> convert scope status +: rest
None -> rest
match r with Report t -> go "" t
base.test.internals.v1.Test.Scope
.> view base.test.internals.v1.Test.Scope
unique type base.test.internals.v1.Test.Scope = Scope [Text]
base.test.internals.v1.Test.Scope.Scope
.> view base.test.internals.v1.Test.Scope.Scope
unique type base.test.internals.v1.Test.Scope = Scope [Text]
.> view base.test.internals.v1.Test.check'
base.test.internals.v1.Test.check' : Boolean -> Test
base.test.internals.v1.Test.check' b =
if b then prove else fail
base.test.internals.v1.Test.failed
.> view base.test.internals.v1.Test.failed
base.test.fail : Test
base.test.fail = finished Failed
base.test.internals.v1.Test.failedWith
.> view base.test.internals.v1.Test.failedWith
base.test.failWith : Text -> Test
base.test.failWith m = label m fail
base.test.internals.v1.Test.finished
.> view base.test.internals.v1.Test.finished
base.test.internals.v1.Test.finished : Status -> Test
base.test.internals.v1.Test.finished st =
Test ( Report (foldScope (sc -> Trie.singleton sc st)))
base.test.internals.v1.Test.forAll
.> view base.test.internals.v1.Test.forAll
base.test.internals.v1.Test.forAll :
Nat -> Domain a -> (a ->{π} Boolean) ->{π} [Result]
base.test.internals.v1.Test.forAll n d p = run (forAll' n d p)
base.test.internals.v1.Test.forAll'
.> view base.test.internals.v1.Test.forAll'
base.test.internals.v1.Test.forAll' :
Nat -> Domain a -> (a ->{π} Boolean) ->{π} Test
base.test.internals.v1.Test.forAll' maxSize domain property =
check xs s =
List.map
(cases
(c, i) ->
if property c then finished (Expected s)
else
use Text ++
label
("test case " ++ Nat.toText i) (finished Failed))
(indexed xs)
foldb id both prove
<| (match domain with
Small xs -> check (List.take maxSize xs) Proved
Large _ ->
check (Domain.sample maxSize domain) (Passed 1))
base.test.internals.v1.Test.label
.> view base.test.internals.v1.Test.label
base.test.label : Text -> Test -> Test
base.test.label n = cases
Test k -> Test (scope -> k <| Scope.cons n scope)
base.test.internals.v1.Test.modifyScope
.> view base.test.internals.v1.Test.modifyScope
base.test.internals.v1.Test.modifyScope :
(Scope -> Scope) -> Test -> Test
base.test.internals.v1.Test.modifyScope f = cases
Test k -> Test ( k f)
base.test.internals.v1.Test.modifyStatus
.> view base.test.internals.v1.Test.modifyStatus
base.test.internals.v1.Test.modifyStatus :
(Status -> Status) -> Test -> Test
base.test.internals.v1.Test.modifyStatus f = cases
Test k -> Test ( (foldReport ( Report (Trie.map f))) k)
.> view base.test.internals.v1.Test.provedWith
base.test.proveWith : Text -> Test
base.test.proveWith m = label m prove
base.test.internals.v1.Test.report
.> view base.test.internals.v1.Test.report
base.test.internals.v1.Test.report : Test -> Report
base.test.internals.v1.Test.report = cases
Test k -> k (Scope [])
.> view base.test.internals.v1.foldReport
base.test.internals.v1.foldReport :
(Trie Text Status ->{π} r) -> Report ->{π} r
base.test.internals.v1.foldReport k = cases Report t -> k t
base.test.internals.v1.foldScope
.> view base.test.internals.v1.foldScope
base.test.internals.v1.foldScope :
([Text] ->{π} r) -> Scope ->{π} r
base.test.internals.v1.foldScope k = cases Scope ss -> k ss
base.test.internals.v1.foldStatus
.> view base.test.internals.v1.foldStatus
base.test.internals.v1.foldStatus :
r
-> (Success ->{π} r)
-> (Success ->{π} r)
-> r
-> Status
->{π} r
base.test.internals.v1.foldStatus
failed expected unexpected pending = cases
Failed -> failed
Expected s -> expected s
Unexpected s -> unexpected s
Pending -> pending
base.test.internals.v1.foldSuccess
.> view base.test.internals.v1.foldSuccess
base.test.internals.v1.foldSuccess :
(Nat ->{π} r) -> r -> Success ->{π} r
base.test.internals.v1.foldSuccess passed proved = cases
Passed n -> passed n
Proved -> proved
base.test.label
.> view base.test.label
base.test.label : Text -> Test -> Test
base.test.label n = cases
Test k -> Test (scope -> k <| Scope.cons n scope)
base.test.laws.absorption
.> view base.test.laws.absorption
base.test.laws.absorption :
'{Gen} a
-> (a ->{e} a ->{e} a)
-> (a ->{e} a ->{e} a)
->{e, Gen} Test
base.test.laws.absorption gen f g =
x = !gen
y = !gen
expect ((f x (g x y) == x) && (g x (f x y) == x))
base.test.laws.associative
.> view base.test.laws.associative
base.test.laws.associative :
'{Gen} a -> (a ->{e} a ->{e} a) ->{e, Gen} Test
base.test.laws.associative gen f =
x = !gen
y = !gen
z = !gen
expect (f x (f y z) == f (f x y) z)
base.test.laws.commutative
.> view base.test.laws.commutative
base.test.laws.commutative :
'{Gen} a -> (a ->{e} a ->{e} b) ->{e, Gen} Test
base.test.laws.commutative gen f =
x = !gen
y = !gen
expect (f x y == f y x)
base.test.laws.distributive
.> view base.test.laws.distributive
base.test.laws.distributive :
'{Gen} a
-> (a ->{e} a ->{e} a)
-> (a ->{e} a ->{e} a)
->{e, Gen} Test
base.test.laws.distributive gen f g =
x = !gen
y = !gen
z = !gen
expect (f x (g y z) == g (f x y) (f x z))
base.test.laws.homomorphism
.> view base.test.laws.homomorphism
base.test.laws.homomorphism :
'{Gen} a
-> (a ->{e} b)
-> (a ->{e} a ->{e} a)
-> (b ->{e} b ->{e} b)
->{e, Gen} Test
base.test.laws.homomorphism gen f p q =
a = !gen
b = !gen
expect (f (p a b) == q (f a) (f b))
base.test.laws.idempotence
.> view base.test.laws.idempotence
base.test.laws.idempotence :
'{Gen} a -> (a ->{e} a ->{e} a) ->{e, Gen} Test
base.test.laws.idempotence gen f =
x = !gen
expect (f x x == x)
base.test.laws.lattice
.> view base.test.laws.lattice
base.test.laws.lattice :
'{Gen} a
-> (a ->{e} a ->{e} a)
-> (a ->{e} a ->{e} a)
->{e, Gen} Test
base.test.laws.lattice gen meet join =
use laws associative commutative
both
(both
(both
(both
(laws.absorption gen meet join)
(associative gen meet))
(associative gen join))
(commutative gen meet))
(commutative gen join)
.> view base.until
base.until : (a ->{e} Boolean) -> '{e} a ->{e} a
base.until pred op =
r = !op
if pred r then r else base.until pred op
base.until.test
.> view base.until.test
base.until.test : [Result]
base.until.test =
use withInitialValue handler
go n _ =
new =
use Nat +
get + 1
put new
new == n
t3 =
handle expect ((until id (go 3)) && (get == 3))
with handler 0
t1 =
handle expect ((until id (go 1)) && (get == 1))
with handler 0
run (both t1 t3)
base.while
.> view base.while
base.while : (a ->{e} Boolean) -> '{e} a ->{e} a
base.while pred op = until ( not pred) op
base.while.test
.> view base.while.test
base.while.test : [Result]
base.while.test =
use withInitialValue handler
go n _ =
new =
use Nat +
get + 1
put new
new < n
t3 =
handle expect ((not (while id (go 3))) && (get == 3))
with handler 0
t1 =
handle expect ((not (while id (go 1))) && (get == 1))
with handler 0
run (both t1 t3)
base.|>
.> view base.|>
(base.|>) : a -> (a ->{π} b) ->{π} b
a base.|> f = f a
