mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-11 10:35:57 +03:00
fixes tests and transcripts
This commit is contained in:
parent
5da63ec4f1
commit
ac2bc29849
@ -295,9 +295,9 @@ constructorName ref cid =
|
|||||||
source :: Text
|
source :: Text
|
||||||
source = fromString [r|
|
source = fromString [r|
|
||||||
|
|
||||||
type Either a b = Left a | Right b
|
structural type Either a b = Left a | Right b
|
||||||
|
|
||||||
type Optional a = None | Some a
|
structural type Optional a = None | Some a
|
||||||
|
|
||||||
unique[b28d929d0a73d2c18eac86341a3bb9399f8550c11b5f35eabb2751e6803ccc20] type
|
unique[b28d929d0a73d2c18eac86341a3bb9399f8550c11b5f35eabb2751e6803ccc20] type
|
||||||
IsPropagated = IsPropagated
|
IsPropagated = IsPropagated
|
||||||
@ -462,7 +462,7 @@ unique[d7b2ced8c08b2c6e54050d1f5acedef3395f293d] type Pretty.Annotated w txt
|
|||||||
| Indent w (Pretty.Annotated w txt) (Pretty.Annotated w txt) (Pretty.Annotated w txt)
|
| Indent w (Pretty.Annotated w txt) (Pretty.Annotated w txt) (Pretty.Annotated w txt)
|
||||||
| Append w [Pretty.Annotated w txt]
|
| Append w [Pretty.Annotated w txt]
|
||||||
|
|
||||||
type Pretty txt = Pretty (Pretty.Annotated () txt)
|
structural type Pretty txt = Pretty (Pretty.Annotated () txt)
|
||||||
|
|
||||||
Pretty.get = cases Pretty p -> p
|
Pretty.get = cases Pretty p -> p
|
||||||
|
|
||||||
|
@ -38,23 +38,23 @@ test = scope "datadeclaration" $
|
|||||||
file :: UnisonFile Symbol Ann
|
file :: UnisonFile Symbol Ann
|
||||||
file = flip unsafeParseFile Common.parsingEnv $ [r|
|
file = flip unsafeParseFile Common.parsingEnv $ [r|
|
||||||
|
|
||||||
type Bool = True | False
|
structural type Bool = True | False
|
||||||
type Bool' = False | True
|
structural type Bool' = False | True
|
||||||
|
|
||||||
type Option a = Some a | None
|
structural type Option a = Some a | None
|
||||||
type Option' b = Nothing | Just b
|
structural type Option' b = Nothing | Just b
|
||||||
|
|
||||||
type List a = Nil | Cons a (List a)
|
structural type List a = Nil | Cons a (List a)
|
||||||
type List' b = Prepend b (List' b) | Empty
|
structural type List' b = Prepend b (List' b) | Empty
|
||||||
type SnocList a = Snil | Snoc (List a) a
|
structural type SnocList a = Snil | Snoc (List a) a
|
||||||
|
|
||||||
type ATree a = Tree a (List (ATree a)) | Leaf (Option a)
|
structural type ATree a = Tree a (List (ATree a)) | Leaf (Option a)
|
||||||
|
|
||||||
type Ping a = Ping a (Pong a)
|
structural type Ping a = Ping a (Pong a)
|
||||||
type Pong a = Pnong | Pong (Ping a)
|
structural type Pong a = Pnong | Pong (Ping a)
|
||||||
|
|
||||||
type Long' a = Long' (Ling' a) | Lnong
|
structural type Long' a = Long' (Ling' a) | Lnong
|
||||||
type Ling' a = Ling' a (Long' a)
|
structural type Ling' a = Ling' a (Long' a)
|
||||||
|]
|
|]
|
||||||
|
|
||||||
|
|
||||||
|
@ -18,25 +18,25 @@ module Unison.Test.FileParser where
|
|||||||
test1 = scope "test1" . tests . map parses $
|
test1 = scope "test1" . tests . map parses $
|
||||||
[
|
[
|
||||||
-- , "type () = ()\n()"
|
-- , "type () = ()\n()"
|
||||||
"type Pair a b = Pair a b\n"
|
"structural type Pair a b = Pair a b\n"
|
||||||
, "type Optional a = Just a | Nothing\n"
|
, "structural type Optional a = Just a | Nothing\n"
|
||||||
, unlines
|
, unlines
|
||||||
["type Optional2 a"
|
["structural type Optional2 a"
|
||||||
," = Just a"
|
," = Just a"
|
||||||
," | Nothing\n"]
|
," | Nothing\n"]
|
||||||
------ -- ,unlines
|
------ -- ,unlines
|
||||||
------ -- ["type Optional a b c where"
|
------ -- ["structural type Optional a b c where"
|
||||||
------ -- ," Just : a -> Optional a"
|
------ -- ," Just : a -> Optional a"
|
||||||
------ -- ," Nothing : Optional Int"]
|
------ -- ," Nothing : Optional Int"]
|
||||||
------ -- , unlines
|
------ -- , unlines
|
||||||
------ -- ["type Optional"
|
------ -- ["structural type Optional"
|
||||||
------ -- ," a"
|
------ -- ," a"
|
||||||
------ -- ," b"
|
------ -- ," b"
|
||||||
------ -- ," c where"
|
------ -- ," c where"
|
||||||
------ -- ," Just : a -> Optional a"
|
------ -- ," Just : a -> Optional a"
|
||||||
------ -- ," Nothing : Optional Int"]
|
------ -- ," Nothing : Optional Int"]
|
||||||
, unlines -- NB: this currently fails because we don't have type AST or parser for effect types yet
|
, unlines -- NB: this currently fails because we don't have type AST or parser for effect types yet
|
||||||
["ability State s where"
|
["structural ability State s where"
|
||||||
," get : {State s} s"
|
," get : {State s} s"
|
||||||
," set : s -> {State s} ()"
|
," set : s -> {State s} ()"
|
||||||
]
|
]
|
||||||
|
@ -249,7 +249,7 @@ test = scope "gitsync22" . tests $
|
|||||||
-- simplest-author
|
-- simplest-author
|
||||||
(\repo -> [i|
|
(\repo -> [i|
|
||||||
```unison
|
```unison
|
||||||
type Foo = Foo
|
structural type Foo = Foo
|
||||||
```
|
```
|
||||||
```ucm
|
```ucm
|
||||||
.myLib> debug.file
|
.myLib> debug.file
|
||||||
@ -322,8 +322,8 @@ test = scope "gitsync22" . tests $
|
|||||||
.> builtins.merge
|
.> builtins.merge
|
||||||
```
|
```
|
||||||
```unison
|
```unison
|
||||||
type A = A Nat
|
structural type A = A Nat
|
||||||
type B = B Int
|
structural type B = B Int
|
||||||
x = 3
|
x = 3
|
||||||
y = 4
|
y = 4
|
||||||
```
|
```
|
||||||
|
@ -32,7 +32,7 @@ test = scope "> extractor" . tests $
|
|||||||
, n "> match 3 with 3 | 3 -> 3" Err.matchBody
|
, n "> match 3 with 3 | 3 -> 3" Err.matchBody
|
||||||
, y "> 1 1" Err.applyingNonFunction
|
, y "> 1 1" Err.applyingNonFunction
|
||||||
, y "> 1 Int.+ 1" Err.applyingFunction
|
, y "> 1 Int.+ 1" Err.applyingFunction
|
||||||
, y ( "ability Abort where\n" ++
|
, y ( "structural ability Abort where\n" ++
|
||||||
" abort : {Abort} a\n" ++
|
" abort : {Abort} a\n" ++
|
||||||
"\n" ++
|
"\n" ++
|
||||||
"xyz : t -> Request Abort t -> t\n" ++
|
"xyz : t -> Request Abort t -> t\n" ++
|
||||||
|
@ -154,7 +154,7 @@ List.diagonal =
|
|||||||
-- -- Use binary search to do lookups and find insertion points
|
-- -- Use binary search to do lookups and find insertion points
|
||||||
-- -- This relies on the underlying sequence having efficient
|
-- -- This relies on the underlying sequence having efficient
|
||||||
-- -- slicing and concatenation
|
-- -- slicing and concatenation
|
||||||
type Map k v = Map [k] [v]
|
structural type Map k v = Map [k] [v]
|
||||||
|
|
||||||
-- use Map Map
|
-- use Map Map
|
||||||
|
|
||||||
@ -314,7 +314,7 @@ Multimap.insert k v m = match Map.lookup k m with
|
|||||||
Multimap.lookup : k -> Map k [v] -> [v]
|
Multimap.lookup : k -> Map k [v] -> [v]
|
||||||
Multimap.lookup k m = Optional.orDefault [] (Map.lookup k m)
|
Multimap.lookup k m = Optional.orDefault [] (Map.lookup k m)
|
||||||
|
|
||||||
type Set a = Set (Map a ())
|
structural type Set a = Set (Map a ())
|
||||||
|
|
||||||
Set.empty : Set k
|
Set.empty : Set k
|
||||||
Set.empty = Set Map.empty
|
Set.empty = Set Map.empty
|
||||||
@ -346,7 +346,7 @@ Set.size s = Map.size (underlying s)
|
|||||||
Set.intersect : Set k -> Set k -> Set k
|
Set.intersect : Set k -> Set k -> Set k
|
||||||
Set.intersect s1 s2 = Set (Map.intersect (underlying s1) (underlying s2))
|
Set.intersect s1 s2 = Set (Map.intersect (underlying s1) (underlying s2))
|
||||||
|
|
||||||
type Heap k v = Heap Nat k v [Heap k v]
|
structural type Heap k v = Heap Nat k v [Heap k v]
|
||||||
|
|
||||||
Heap.singleton : k -> v -> Heap k v
|
Heap.singleton : k -> v -> Heap k v
|
||||||
Heap.singleton k v = Heap 1 k v []
|
Heap.singleton k v = Heap 1 k v []
|
||||||
|
@ -3,4 +3,3 @@ increment n = n + 1
|
|||||||
|
|
||||||
> x = 1 + 40
|
> x = 1 + 40
|
||||||
> increment x
|
> increment x
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
type X = S Text | I Nat
|
structural type X = S Text | I Nat
|
||||||
|
|
||||||
foo : a -> b -> c -> X
|
foo : a -> b -> c -> X
|
||||||
foo x y z = X.S ""
|
foo x y z = X.S ""
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--Abort
|
--Abort
|
||||||
ability Abort where
|
structural ability Abort where
|
||||||
Abort : forall a . () -> {Abort} a
|
Abort : forall a . () -> {Abort} a
|
||||||
|
|
||||||
bork = u -> 1 + (Abort.Abort ())
|
bork = u -> 1 + (Abort.Abort ())
|
||||||
|
@ -1,9 +1,9 @@
|
|||||||
type Optional a = Some a | None
|
structural type Optional a = Some a | None
|
||||||
|
|
||||||
ability Abort where
|
structural ability Abort where
|
||||||
Abort : forall a . () -> {Abort} a
|
Abort : forall a . () -> {Abort} a
|
||||||
|
|
||||||
ability Abort2 where
|
structural ability Abort2 where
|
||||||
Abort2 : forall a . () -> {Abort2} a
|
Abort2 : forall a . () -> {Abort2} a
|
||||||
Abort2' : forall a . () -> {Abort2} a
|
Abort2' : forall a . () -> {Abort2} a
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
type Foo a b = Foo a b
|
structural type Foo a b = Foo a b
|
||||||
use Foo Foo
|
use Foo Foo
|
||||||
use Optional Some
|
use Optional Some
|
||||||
setA : Foo a b -> Optional a -> Foo a b
|
setA : Foo a b -> Optional a -> Foo a b
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
ability Abort where
|
structural ability Abort where
|
||||||
Abort : forall a . () -> {Abort} a
|
Abort : forall a . () -> {Abort} a
|
||||||
|
|
||||||
foo n = if n >= 1000 then n else !Abort.Abort
|
foo n = if n >= 1000 then n else !Abort.Abort
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
ability T where
|
structural ability T where
|
||||||
a : Unknown -> {T} ()
|
a : Unknown -> {T} ()
|
||||||
|
|
||||||
--b : Unknown
|
--b : Unknown
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--handle inference
|
--handle inference
|
||||||
ability State s where
|
structural ability State s where
|
||||||
get : ∀ s . () -> {State s} s
|
get : ∀ s . () -> {State s} s
|
||||||
set : ∀ s . s -> {State s} ()
|
set : ∀ s . s -> {State s} ()
|
||||||
state : ∀ a s . s -> Request (State s) a -> a
|
state : ∀ a s . s -> Request (State s) a -> a
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--State3 ability
|
--State3 ability
|
||||||
ability State se2 where
|
structural ability State se2 where
|
||||||
put : ∀ se . se -> {State se} ()
|
put : ∀ se . se -> {State se} ()
|
||||||
get : ∀ se . () -> {State se} se
|
get : ∀ se . () -> {State se} se
|
||||||
|
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--IO ability
|
--IO ability
|
||||||
ability IO where
|
structural ability IO where
|
||||||
launchMissiles : () -> {IO} ()
|
launchMissiles : () -> {IO} ()
|
||||||
-- binding is not guarded by a lambda, it only can access
|
-- binding is not guarded by a lambda, it only can access
|
||||||
-- ambient abilities (which will be empty)
|
-- ambient abilities (which will be empty)
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
--IO/State1 ability
|
--IO/State1 ability
|
||||||
ability IO where
|
structural ability IO where
|
||||||
launchMissiles : {IO} ()
|
launchMissiles : {IO} ()
|
||||||
ability State se2 where
|
structural ability State se2 where
|
||||||
put : ∀ se . se -> {State se} ()
|
put : ∀ se . se -> {State se} ()
|
||||||
get : ∀ se . () -> {State se} se
|
get : ∀ se . () -> {State se} se
|
||||||
foo : () -> {IO} ()
|
foo : () -> {IO} ()
|
||||||
|
@ -1,8 +1,8 @@
|
|||||||
--map/traverse
|
--map/traverse
|
||||||
ability Noop where
|
structural ability Noop where
|
||||||
noop : a -> {Noop} a
|
noop : a -> {Noop} a
|
||||||
|
|
||||||
type List a = Nil | Cons a (List a)
|
structural type List a = Nil | Cons a (List a)
|
||||||
|
|
||||||
map : (a ->{} b) -> List a -> List b
|
map : (a ->{} b) -> List a -> List b
|
||||||
map f = cases
|
map f = cases
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
type Foo = Foo
|
structural type Foo = Foo
|
||||||
type Bar = Bar
|
structural type Bar = Bar
|
||||||
|
|
||||||
x : Foo
|
x : Foo
|
||||||
x = Bar.Bar
|
x = Bar.Bar
|
||||||
|
@ -5,9 +5,9 @@
|
|||||||
-- 27 | let
|
-- 27 | let
|
||||||
--
|
--
|
||||||
|
|
||||||
type Optional a = None | Some a
|
structural type Optional a = None | Some a
|
||||||
|
|
||||||
ability State s where
|
structural ability State s where
|
||||||
put : s -> {State s} ()
|
put : s -> {State s} ()
|
||||||
get : {State s} s
|
get : {State s} s
|
||||||
|
|
||||||
|
@ -11,7 +11,7 @@
|
|||||||
--
|
--
|
||||||
-- Verbiage could be improved, but also the `()` location should
|
-- Verbiage could be improved, but also the `()` location should
|
||||||
-- point to line 22, the `k ()` call.
|
-- point to line 22, the `k ()` call.
|
||||||
ability Ask foo where
|
structural ability Ask foo where
|
||||||
ask : () -> {Ask a} a
|
ask : () -> {Ask a} a
|
||||||
|
|
||||||
supply : Text -> Request (Ask Text) a -> a
|
supply : Text -> Request (Ask Text) a -> a
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--mismatched case result types
|
--mismatched case result types
|
||||||
type Optional a = None | Some a
|
structural type Optional a = None | Some a
|
||||||
match Optional.Some 3 with
|
match Optional.Some 3 with
|
||||||
x -> 1
|
x -> 1
|
||||||
y -> "boo"
|
y -> "boo"
|
||||||
|
@ -10,7 +10,7 @@
|
|||||||
--
|
--
|
||||||
-- even though this program doesn't use guards!
|
-- even though this program doesn't use guards!
|
||||||
|
|
||||||
ability Ask a where
|
structural ability Ask a where
|
||||||
ask : {Ask a} a
|
ask : {Ask a} a
|
||||||
|
|
||||||
supply : Text -> Request (Ask Text) a -> a
|
supply : Text -> Request (Ask Text) a -> a
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
-- board piece
|
-- board piece
|
||||||
type P = X | O | E
|
structural type P = X | O | E
|
||||||
|
|
||||||
type Board = Board P P
|
structural type Board = Board P P
|
||||||
|
|
||||||
use Board.Board
|
use Board.Board
|
||||||
use P O X E
|
use P O X E
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
type Foo0 = Foo0
|
structural type Foo0 = Foo0
|
||||||
type Foo1 a = Foo1 a
|
structural type Foo1 a = Foo1 a
|
||||||
type Foo2 a b = Foo2 a b
|
structural type Foo2 a b = Foo2 a b
|
||||||
type Foo3 a b c = Foo3 a b c
|
structural type Foo3 a b c = Foo3 a b c
|
||||||
|
|
||||||
use Foo0 Foo0
|
use Foo0 Foo0
|
||||||
use Foo1 Foo1
|
use Foo1 Foo1
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--State4 ability
|
--State4 ability
|
||||||
ability State se2 where
|
structural ability State se2 where
|
||||||
put : ∀ se . se -> {State se} ()
|
put : ∀ se . se -> {State se} ()
|
||||||
get : ∀ se . () -> {State se} se
|
get : ∀ se . () -> {State se} se
|
||||||
-- binding is not guarded by a lambda, it only can access
|
-- binding is not guarded by a lambda, it only can access
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
ability State s where
|
structural ability State s where
|
||||||
get : () -> {State s} s
|
get : () -> {State s} s
|
||||||
set : s -> {State s} ()
|
set : s -> {State s} ()
|
||||||
|
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--mismatched case result types
|
--mismatched case result types
|
||||||
type Optional a = None | Some a
|
structural type Optional a = None | Some a
|
||||||
match Optional.Some 3 with
|
match Optional.Some 3 with
|
||||||
x -> 1
|
x -> 1
|
||||||
y -> "boo"
|
y -> "boo"
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--Type.apply
|
--Type.apply
|
||||||
type List a = Nil | Cons a (List a)
|
structural type List a = Nil | Cons a (List a)
|
||||||
map : ∀ a b . (a -> b) -> List a -> List b
|
map : ∀ a b . (a -> b) -> List a -> List b
|
||||||
map f = cases
|
map f = cases
|
||||||
List.Nil -> List.Nil
|
List.Nil -> List.Nil
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
type Optional a = Some a | None
|
structural type Optional a = Some a | None
|
||||||
app' : Optional Int
|
app' : Optional Int
|
||||||
app' = 3
|
app' = 3
|
||||||
()
|
()
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
ability Abort where
|
structural ability Abort where
|
||||||
Abort : forall a . () -> {Abort} a
|
Abort : forall a . () -> {Abort} a
|
||||||
|
|
||||||
ability Abort2 where
|
structural ability Abort2 where
|
||||||
Abort2 : forall a . () -> {Abort2} a
|
Abort2 : forall a . () -> {Abort2} a
|
||||||
Abort2' : forall a . () -> {Abort2} a
|
Abort2' : forall a . () -> {Abort2} a
|
||||||
|
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
ability Abort where
|
structural ability Abort where
|
||||||
Abort : forall a . () -> {Abort} a
|
Abort : forall a . () -> {Abort} a
|
||||||
|
|
||||||
ability Abort2 where
|
structural ability Abort2 where
|
||||||
Abort2 : forall a . () -> {Abort2} a
|
Abort2 : forall a . () -> {Abort2} a
|
||||||
|
|
||||||
ability' : Nat -> { Abort } Int
|
ability' : Nat -> { Abort } Int
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
type Optional a = Some a | None
|
structural type Optional a = Some a | None
|
||||||
y : (Optional Int)
|
y : (Optional Int)
|
||||||
y = 3
|
y = 3
|
||||||
()
|
()
|
@ -1,4 +1,4 @@
|
|||||||
type Optional a = Some a | None
|
structural type Optional a = Some a | None
|
||||||
z' : (Optional Int, Optional Text, Optional Float)
|
z' : (Optional Int, Optional Text, Optional Float)
|
||||||
z' = (None, 3)
|
z' = (None, 3)
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
type Optional a = Some a | None
|
structural type Optional a = Some a | None
|
||||||
z : (Optional Int, Optional Text, Optional Float)
|
z : (Optional Int, Optional Text, Optional Float)
|
||||||
z = 3
|
z = 3
|
||||||
()
|
()
|
@ -1,5 +1,5 @@
|
|||||||
--Abort
|
--Abort
|
||||||
ability Abort where
|
structural ability Abort where
|
||||||
Abort : forall a . () -> {Abort} a
|
Abort : forall a . () -> {Abort} a
|
||||||
|
|
||||||
use Nat +
|
use Nat +
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
|
|
||||||
ability Ask a where
|
structural ability Ask a where
|
||||||
ask : {Ask a} a
|
ask : {Ask a} a
|
||||||
|
|
||||||
supply : Text -> Request (Ask Text) a -> a
|
supply : Text -> Request (Ask Text) a -> a
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
ability Either a b where
|
structural ability Either a b where
|
||||||
left : a -> {Either a b} ()
|
left : a -> {Either a b} ()
|
||||||
right : b -> {Either a b} ()
|
right : b -> {Either a b} ()
|
||||||
|
|
||||||
type Either a b = Left a | Right b
|
structural type Either a b = Left a | Right b
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
|
|
||||||
type Any = Any (∀ r . (∀ a . a -> r) -> r)
|
structural type Any = Any (∀ r . (∀ a . a -> r) -> r)
|
||||||
|
|
||||||
-- also typechecks as expected
|
-- also typechecks as expected
|
||||||
any : a -> Any
|
any : a -> Any
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
type Choice = First | Second
|
structural type Choice = First | Second
|
||||||
type Wrapper = Wrapper Choice
|
structural type Wrapper = Wrapper Choice
|
||||||
|
|
||||||
broken = match Wrapper.Wrapper Choice.Second with
|
broken = match Wrapper.Wrapper Choice.Second with
|
||||||
Wrapper.Wrapper Choice.First -> true
|
Wrapper.Wrapper Choice.First -> true
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
type Optional a = None | Some a
|
structural type Optional a = None | Some a
|
||||||
|
|
||||||
Optional.isEmpty : Optional a -> Boolean
|
Optional.isEmpty : Optional a -> Boolean
|
||||||
Optional.isEmpty = cases
|
Optional.isEmpty = cases
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
ability Emit a where
|
structural ability Emit a where
|
||||||
emit : a ->{Emit a} ()
|
emit : a ->{Emit a} ()
|
||||||
|
|
||||||
type Stream a = Stream ('{Emit a} ())
|
structural type Stream a = Stream ('{Emit a} ())
|
||||||
|
|
||||||
use Stream Stream
|
use Stream Stream
|
||||||
use Optional None Some
|
use Optional None Some
|
||||||
|
@ -1,5 +1,4 @@
|
|||||||
|
structural ability Foo where
|
||||||
ability Foo where
|
|
||||||
foo : {Foo} Text
|
foo : {Foo} Text
|
||||||
|
|
||||||
x = 'let
|
x = 'let
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--Abort
|
--Abort
|
||||||
ability Abort where
|
structural ability Abort where
|
||||||
Abort : forall a . () -> {Abort} a
|
Abort : forall a . () -> {Abort} a
|
||||||
eff : forall a b . (a -> b) -> b -> Request Abort a -> b
|
eff : forall a b . (a -> b) -> b -> Request Abort a -> b
|
||||||
eff f z = cases
|
eff f z = cases
|
||||||
|
@ -1,14 +1,14 @@
|
|||||||
--Ask inferred
|
--Ask inferred
|
||||||
|
|
||||||
ability Ask a where
|
structural ability Ask a where
|
||||||
ask : {Ask a} a
|
ask : {Ask a} a
|
||||||
|
|
||||||
ability AskU where
|
structural ability AskU where
|
||||||
ask : {AskU} Nat
|
ask : {AskU} Nat
|
||||||
|
|
||||||
use Nat +
|
use Nat +
|
||||||
|
|
||||||
ability AskT where
|
structural ability AskT where
|
||||||
ask : {AskT} Text
|
ask : {AskT} Text
|
||||||
|
|
||||||
x = '(Ask.ask + 1)
|
x = '(Ask.ask + 1)
|
||||||
|
@ -1,9 +1,9 @@
|
|||||||
use Universal <
|
use Universal <
|
||||||
|
|
||||||
type Future a = Future ('{Remote} a)
|
structural type Future a = Future ('{Remote} a)
|
||||||
|
|
||||||
-- A simple distributed computation ability
|
-- A simple distributed computation ability
|
||||||
ability Remote where
|
structural ability Remote where
|
||||||
|
|
||||||
-- Spawn a new node
|
-- Spawn a new node
|
||||||
spawn : {Remote} Node
|
spawn : {Remote} Node
|
||||||
@ -16,7 +16,7 @@ ability Remote where
|
|||||||
-- await the result of the computation
|
-- await the result of the computation
|
||||||
fork : '{Remote} a ->{Remote} Future a
|
fork : '{Remote} a ->{Remote} Future a
|
||||||
|
|
||||||
type Node = Node Nat -- more realistic would be perhaps a (Hostname, PublicKey) pair
|
structural type Node = Node Nat -- more realistic would be perhaps a (Hostname, PublicKey) pair
|
||||||
|
|
||||||
force : Future a ->{Remote} a
|
force : Future a ->{Remote} a
|
||||||
force = cases Future.Future r -> !r
|
force = cases Future.Future r -> !r
|
||||||
@ -51,7 +51,7 @@ List.map f as =
|
|||||||
Some a -> go f (acc `snoc` f a) as (i + 1)
|
Some a -> go f (acc `snoc` f a) as (i + 1)
|
||||||
go f [] as 0
|
go f [] as 0
|
||||||
|
|
||||||
type Monoid a = Monoid (a -> a -> a) a
|
structural type Monoid a = Monoid (a -> a -> a) a
|
||||||
|
|
||||||
Monoid.zero = cases Monoid.Monoid op z -> z
|
Monoid.zero = cases Monoid.Monoid op z -> z
|
||||||
Monoid.op = cases Monoid.Monoid op z -> op
|
Monoid.op = cases Monoid.Monoid op z -> op
|
||||||
|
@ -1,8 +1,8 @@
|
|||||||
ability State s where
|
structural ability State s where
|
||||||
get : {State s} s
|
get : {State s} s
|
||||||
set : s -> {State s} ()
|
set : s -> {State s} ()
|
||||||
|
|
||||||
ability Console where
|
structural ability Console where
|
||||||
read : {Console} (Optional Text)
|
read : {Console} (Optional Text)
|
||||||
write : Text -> {Console} ()
|
write : Text -> {Console} ()
|
||||||
|
|
||||||
|
@ -1,11 +1,11 @@
|
|||||||
-- This confusingly gives an error that
|
-- This confusingly gives an error that
|
||||||
-- it doesn't know what `Console.simulate` is.
|
-- it doesn't know what `Console.simulate` is.
|
||||||
|
|
||||||
ability State s where
|
structural ability State s where
|
||||||
get : {State s} s
|
get : {State s} s
|
||||||
set : s -> {State s} ()
|
set : s -> {State s} ()
|
||||||
|
|
||||||
ability Console where
|
structural ability Console where
|
||||||
read : {Console} (Optional Text)
|
read : {Console} (Optional Text)
|
||||||
write : Text -> {Console} ()
|
write : Text -> {Console} ()
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
--data references builtins
|
--data references builtins
|
||||||
type StringOrInt = S Text | I Nat
|
structural type StringOrInt = S Text | I Nat
|
||||||
> [StringOrInt.S "YO", StringOrInt.I 1]
|
> [StringOrInt.S "YO", StringOrInt.I 1]
|
||||||
|
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
|
|
||||||
type Foo a = Foo a
|
structural type Foo a = Foo a
|
||||||
|
|
||||||
(+) = (Nat.+)
|
(+) = (Nat.+)
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
ability T where
|
structural ability T where
|
||||||
foo : {T} ()
|
foo : {T} ()
|
||||||
|
|
||||||
-- parses fine
|
-- parses fine
|
||||||
|
@ -2,7 +2,7 @@
|
|||||||
blah : a -> a -> a
|
blah : a -> a -> a
|
||||||
blah a a2 = a2
|
blah a a2 = a2
|
||||||
|
|
||||||
ability Foo where
|
structural ability Foo where
|
||||||
foo : {Foo} Text
|
foo : {Foo} Text
|
||||||
|
|
||||||
-- previously this didn't work as first argument was pure
|
-- previously this didn't work as first argument was pure
|
||||||
|
@ -2,7 +2,7 @@
|
|||||||
woot : a -> a -> a
|
woot : a -> a -> a
|
||||||
woot a a2 = a
|
woot a a2 = a
|
||||||
|
|
||||||
ability Hi where
|
structural ability Hi where
|
||||||
hi : Float ->{Hi} Int
|
hi : Float ->{Hi} Int
|
||||||
|
|
||||||
> woot Float.floor Hi.hi
|
> woot Float.floor Hi.hi
|
||||||
|
@ -4,5 +4,5 @@ eff f z = cases
|
|||||||
{ Abort.Abort _ -> k } -> z
|
{ Abort.Abort _ -> k } -> z
|
||||||
{ a } -> f a
|
{ a } -> f a
|
||||||
|
|
||||||
ability Abort where
|
structural ability Abort where
|
||||||
Abort : forall a . () -> {Abort} a
|
Abort : forall a . () -> {Abort} a
|
||||||
|
@ -8,7 +8,7 @@
|
|||||||
-- This file won't typecheck unless the definitions get
|
-- This file won't typecheck unless the definitions get
|
||||||
-- the correct inferred types.
|
-- the correct inferred types.
|
||||||
|
|
||||||
ability Zonk where
|
structural ability Zonk where
|
||||||
zonk : Nat
|
zonk : Nat
|
||||||
|
|
||||||
-- should be inferred as:
|
-- should be inferred as:
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
|
|
||||||
ability G a where
|
structural ability G a where
|
||||||
get : a
|
get : a
|
||||||
|
|
||||||
f x y =
|
f x y =
|
||||||
|
@ -4,7 +4,7 @@ a |> f = f a
|
|||||||
|
|
||||||
ex1 = "bob" |> (Text.++) "hi, "
|
ex1 = "bob" |> (Text.++) "hi, "
|
||||||
|
|
||||||
type Woot = Woot Text Int Nat
|
structural type Woot = Woot Text Int Nat
|
||||||
|
|
||||||
ex2 = match 0 |> Woot "Zonk" +10 with
|
ex2 = match 0 |> Woot "Zonk" +10 with
|
||||||
Woot.Woot _ i _ -> i
|
Woot.Woot _ i _ -> i
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
type MonoidRec a = {
|
structural type MonoidRec a = {
|
||||||
combine : a -> a -> a,
|
combine : a -> a -> a,
|
||||||
empty : a
|
empty : a
|
||||||
}
|
}
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
ability Woot where woot : {Woot} Text
|
structural ability Woot where woot : {Woot} Text
|
||||||
|
|
||||||
force : '{e} a ->{e} a
|
force : '{e} a ->{e} a
|
||||||
force a = !a
|
force a = !a
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
type Foo = Foo Boolean Boolean
|
structural type Foo = Foo Boolean Boolean
|
||||||
|
|
||||||
f : Foo -> Boolean
|
f : Foo -> Boolean
|
||||||
f = cases
|
f = cases
|
||||||
|
@ -15,11 +15,11 @@ replicate n x =
|
|||||||
!x
|
!x
|
||||||
replicate (n `drop` 1) x
|
replicate (n `drop` 1) x
|
||||||
|
|
||||||
ability State a where
|
structural ability State a where
|
||||||
get : {State a} a
|
get : {State a} a
|
||||||
put : a -> {State a} ()
|
put : a -> {State a} ()
|
||||||
|
|
||||||
ability Writer w where
|
structural ability Writer w where
|
||||||
tell : w -> {Writer w} ()
|
tell : w -> {Writer w} ()
|
||||||
|
|
||||||
stateHandler : s -> Request {State s} a -> (s, a)
|
stateHandler : s -> Request {State s} a -> (s, a)
|
||||||
|
@ -1,10 +1,10 @@
|
|||||||
|
|
||||||
use Universal == <
|
use Universal == <
|
||||||
|
|
||||||
type Future a = Future ('{Remote} a)
|
structural type Future a = Future ('{Remote} a)
|
||||||
|
|
||||||
-- A simple distributed computation ability
|
-- A simple distributed computation ability
|
||||||
ability Remote where
|
structural ability Remote where
|
||||||
|
|
||||||
-- Spawn a new node
|
-- Spawn a new node
|
||||||
spawn : {Remote} Node
|
spawn : {Remote} Node
|
||||||
@ -17,7 +17,7 @@ ability Remote where
|
|||||||
-- await the result of the computation
|
-- await the result of the computation
|
||||||
fork : '{Remote} a ->{Remote} Future a
|
fork : '{Remote} a ->{Remote} Future a
|
||||||
|
|
||||||
type Node = Node Nat -- more realistic would be perhaps a (Hostname, PublicKey) pair
|
structural type Node = Node Nat -- more realistic would be perhaps a (Hostname, PublicKey) pair
|
||||||
|
|
||||||
force : Future a ->{Remote} a
|
force : Future a ->{Remote} a
|
||||||
force = cases Future.Future r -> !r
|
force = cases Future.Future r -> !r
|
||||||
|
@ -2,4 +2,3 @@ id : a -> a
|
|||||||
id x = x
|
id x = x
|
||||||
|
|
||||||
> id
|
> id
|
||||||
|
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--IO/State2 ability
|
--IO/State2 ability
|
||||||
ability IO where
|
structural ability IO where
|
||||||
launchMissiles : {IO} ()
|
launchMissiles : {IO} ()
|
||||||
|
|
||||||
foo : Int -> {IO} Int
|
foo : Int -> {IO} Int
|
||||||
@ -12,10 +12,10 @@ foo unit =
|
|||||||
+42
|
+42
|
||||||
+43
|
+43
|
||||||
|
|
||||||
type Optional a =
|
structural type Optional a =
|
||||||
Some a | None
|
Some a | None
|
||||||
|
|
||||||
ability State se2 where
|
structural ability State se2 where
|
||||||
put : ∀ se . se -> {State se} ()
|
put : ∀ se . se -> {State se} ()
|
||||||
get : ∀ se . {State se} se
|
get : ∀ se . {State se} se
|
||||||
|
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--IO3 ability
|
--IO3 ability
|
||||||
ability IO where
|
structural ability IO where
|
||||||
launchMissiles : () -> {IO} ()
|
launchMissiles : () -> {IO} ()
|
||||||
-- binding IS guarded, so its body can access whatever abilities
|
-- binding IS guarded, so its body can access whatever abilities
|
||||||
-- are declared by the type of the binding
|
-- are declared by the type of the binding
|
||||||
|
@ -1,11 +1,11 @@
|
|||||||
--map/traverse
|
--map/traverse
|
||||||
ability Noop where
|
structural ability Noop where
|
||||||
noop : ∀ a . a -> {Noop} a
|
noop : ∀ a . a -> {Noop} a
|
||||||
|
|
||||||
ability Noop2 where
|
structural ability Noop2 where
|
||||||
noop2 : ∀ a . a -> a -> {Noop2} a
|
noop2 : ∀ a . a -> a -> {Noop2} a
|
||||||
|
|
||||||
type List a = Nil | Cons a (List a)
|
structural type List a = Nil | Cons a (List a)
|
||||||
|
|
||||||
map : ∀ a b e . (a -> {e} b) -> List a -> {e} (List b)
|
map : ∀ a b e . (a -> {e} b) -> List a -> {e} (List b)
|
||||||
map f = cases
|
map f = cases
|
||||||
|
@ -1,11 +1,11 @@
|
|||||||
--map/traverse
|
--map/traverse
|
||||||
ability Noop where
|
structural ability Noop where
|
||||||
noop : a -> {Noop} a
|
noop : a -> {Noop} a
|
||||||
|
|
||||||
ability Noop2 where
|
structural ability Noop2 where
|
||||||
noop2 : a -> a -> {Noop2} a
|
noop2 : a -> a -> {Noop2} a
|
||||||
|
|
||||||
type List a = Nil | Cons a (List a)
|
structural type List a = Nil | Cons a (List a)
|
||||||
|
|
||||||
map : (a -> b) -> List a -> List b
|
map : (a -> b) -> List a -> List b
|
||||||
map f = cases
|
map f = cases
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
|
|
||||||
-- ABILITIES
|
-- ABILITIES
|
||||||
|
|
||||||
ability A where
|
structural ability A where
|
||||||
woot : {A} Nat
|
woot : {A} Nat
|
||||||
|
|
||||||
unA = cases
|
unA = cases
|
||||||
@ -15,7 +15,7 @@ a1 = handle
|
|||||||
x
|
x
|
||||||
with unA
|
with unA
|
||||||
|
|
||||||
ability B where
|
structural ability B where
|
||||||
zing : {B} Int
|
zing : {B} Int
|
||||||
|
|
||||||
abh = cases
|
abh = cases
|
||||||
@ -43,7 +43,7 @@ ab2 =
|
|||||||
with nh
|
with nh
|
||||||
with abh
|
with abh
|
||||||
|
|
||||||
ability C where
|
structural ability C where
|
||||||
n : Nat
|
n : Nat
|
||||||
i : Int
|
i : Int
|
||||||
|
|
||||||
|
@ -2,7 +2,7 @@
|
|||||||
-- Now check exact and underapply cases for constructors
|
-- Now check exact and underapply cases for constructors
|
||||||
-- (overapply of a constructor is always a type error)
|
-- (overapply of a constructor is always a type error)
|
||||||
|
|
||||||
type Woot = Woot Nat Nat Nat Nat
|
structural type Woot = Woot Nat Nat Nat Nat
|
||||||
|
|
||||||
toSeq : Woot -> [Nat]
|
toSeq : Woot -> [Nat]
|
||||||
toSeq = cases
|
toSeq = cases
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
|
|
||||||
ability SpaceAttack where
|
structural ability SpaceAttack where
|
||||||
launchMissiles : Text -> ()
|
launchMissiles : Text -> ()
|
||||||
|
|
||||||
-- should typecheck fine, as the `launchMissiles "saturn"`
|
-- should typecheck fine, as the `launchMissiles "saturn"`
|
||||||
|
@ -2,7 +2,7 @@
|
|||||||
-- A corner case in the runtime is when a function is being overapplied and
|
-- A corner case in the runtime is when a function is being overapplied and
|
||||||
-- the exactly applied function requests an ability (and returns a new function)
|
-- the exactly applied function requests an ability (and returns a new function)
|
||||||
|
|
||||||
ability Zing where
|
structural ability Zing where
|
||||||
zing : Nat -> {Zing} (Nat -> Nat)
|
zing : Nat -> {Zing} (Nat -> Nat)
|
||||||
zing2 : Nat -> Nat ->{Zing} (Nat -> Nat -> [Nat])
|
zing2 : Nat -> Nat ->{Zing} (Nat -> Nat -> [Nat])
|
||||||
|
|
||||||
|
@ -1,8 +1,8 @@
|
|||||||
ability State s where
|
structural ability State s where
|
||||||
get : {State s} s
|
get : {State s} s
|
||||||
set : s -> {State s} ()
|
set : s -> {State s} ()
|
||||||
|
|
||||||
ability Console where
|
structural ability Console where
|
||||||
read : {Console} (Optional Text)
|
read : {Console} (Optional Text)
|
||||||
write : Text -> {Console} ()
|
write : Text -> {Console} ()
|
||||||
|
|
||||||
|
@ -1,8 +1,8 @@
|
|||||||
type Foo0 = Foo0
|
structural type Foo0 = Foo0
|
||||||
type Foo1 a = Foo1 a
|
structural type Foo1 a = Foo1 a
|
||||||
type Foo2 a b = Foo2 a b
|
structural type Foo2 a b = Foo2 a b
|
||||||
type Foo3 a b c = Foo3 a b c
|
structural type Foo3 a b c = Foo3 a b c
|
||||||
type List a = Nil | Cons a (List a)
|
structural type List a = Nil | Cons a (List a)
|
||||||
|
|
||||||
use Foo0 Foo0
|
use Foo0 Foo0
|
||||||
use Foo1 Foo1
|
use Foo1 Foo1
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
type Foo0 = Foo0
|
structural type Foo0 = Foo0
|
||||||
type Foo1 a = Foo1 a
|
structural type Foo1 a = Foo1 a
|
||||||
type Foo2 a b = Foo2 a b
|
structural type Foo2 a b = Foo2 a b
|
||||||
type Foo3 a b c = Foo3 a b c
|
structural type Foo3 a b c = Foo3 a b c
|
||||||
|
|
||||||
use Foo0 Foo0
|
use Foo0 Foo0
|
||||||
use Foo1 Foo1
|
use Foo1 Foo1
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
type Value = String Text
|
structural type Value = String Text
|
||||||
| Bool Boolean
|
| Bool Boolean
|
||||||
|
|
||||||
f : Value -> Nat
|
f : Value -> Nat
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--r1
|
--r1
|
||||||
type Optional a = None | Some a
|
structural type Optional a = None | Some a
|
||||||
r1 : Nat
|
r1 : Nat
|
||||||
r1 = match Optional.Some 3 with
|
r1 = match Optional.Some 3 with
|
||||||
x -> 1
|
x -> 1
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
type Optional a = None | Some a
|
structural type Optional a = None | Some a
|
||||||
r2 : Nat
|
r2 : Nat
|
||||||
r2 = match Optional.Some true with
|
r2 = match Optional.Some true with
|
||||||
Optional.Some true -> 1
|
Optional.Some true -> 1
|
||||||
|
@ -21,10 +21,10 @@ rainbow x =
|
|||||||
d = (Ask.ask : Int)
|
d = (Ask.ask : Int)
|
||||||
+42
|
+42
|
||||||
|
|
||||||
ability Ask a where
|
structural ability Ask a where
|
||||||
ask : {Ask a} a
|
ask : {Ask a} a
|
||||||
|
|
||||||
type Either a b = Left a | Right b
|
structural type Either a b = Left a | Right b
|
||||||
|
|
||||||
unique ability Zang where
|
unique ability Zang where
|
||||||
zang : {Zang} Nat
|
zang : {Zang} Nat
|
||||||
|
@ -1,9 +1,9 @@
|
|||||||
|
|
||||||
type Point x y = { x : x, y : y }
|
structural type Point x y = { x : x, y : y }
|
||||||
|
|
||||||
type Point2 = { point2 : Nat, f : Nat }
|
structural type Point2 = { point2 : Nat, f : Nat }
|
||||||
|
|
||||||
type Monoid a = { zero : a, plus : a -> a -> a }
|
structural type Monoid a = { zero : a, plus : a -> a -> a }
|
||||||
|
|
||||||
> Point.x.set 10 (Point 0 0)
|
> Point.x.set 10 (Point 0 0)
|
||||||
> Point.x (Point 10 0)
|
> Point.x (Point 10 0)
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
type X a = X [a]
|
structural type X a = X [a]
|
||||||
|
|
||||||
f : X a -> a
|
f : X a -> a
|
||||||
f = cases
|
f = cases
|
||||||
|
@ -1,10 +1,10 @@
|
|||||||
|
|
||||||
use Universal == <
|
use Universal == <
|
||||||
|
|
||||||
type Future a = Future ('{Remote} a)
|
structural type Future a = Future ('{Remote} a)
|
||||||
|
|
||||||
-- A simple distributed computation ability
|
-- A simple distributed computation ability
|
||||||
ability Remote where
|
structural ability Remote where
|
||||||
|
|
||||||
-- Spawn a new node
|
-- Spawn a new node
|
||||||
spawn : {Remote} Node
|
spawn : {Remote} Node
|
||||||
@ -17,7 +17,7 @@ ability Remote where
|
|||||||
-- await the result of the computation
|
-- await the result of the computation
|
||||||
fork : '{Remote} a ->{Remote} Future a
|
fork : '{Remote} a ->{Remote} Future a
|
||||||
|
|
||||||
type Node = Node Nat -- more realistic would be perhaps a (Hostname, PublicKey) pair
|
structural type Node = Node Nat -- more realistic would be perhaps a (Hostname, PublicKey) pair
|
||||||
|
|
||||||
force : Future a ->{Remote} a
|
force : Future a ->{Remote} a
|
||||||
force = cases Future.Future r -> !r
|
force = cases Future.Future r -> !r
|
||||||
@ -50,7 +50,7 @@ List.map f as =
|
|||||||
Some a -> go f (acc `snoc` f a) as (i + 1)
|
Some a -> go f (acc `snoc` f a) as (i + 1)
|
||||||
go f [] as 0
|
go f [] as 0
|
||||||
|
|
||||||
type Monoid a = Monoid (a -> a -> a) a
|
structural type Monoid a = Monoid (a -> a -> a) a
|
||||||
|
|
||||||
Monoid.zero = cases Monoid.Monoid op z -> z
|
Monoid.zero = cases Monoid.Monoid op z -> z
|
||||||
Monoid.op = cases Monoid.Monoid op z -> op
|
Monoid.op = cases Monoid.Monoid op z -> op
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
ability Woot where
|
structural ability Woot where
|
||||||
woot : {Woot} Nat
|
woot : {Woot} Nat
|
||||||
|
|
||||||
wha : ((a ->{Woot} a) -> a ->{Woot} a) -> Nat
|
wha : ((a ->{Woot} a) -> a ->{Woot} a) -> Nat
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--State1 ability
|
--State1 ability
|
||||||
ability State se2 where
|
structural ability State se2 where
|
||||||
put : ∀ se . se -> {State se} ()
|
put : ∀ se . se -> {State se} ()
|
||||||
get : ∀ se . () -> {State se} se
|
get : ∀ se . () -> {State se} se
|
||||||
|
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--State1a ability
|
--State1a ability
|
||||||
ability State se2 where
|
structural ability State se2 where
|
||||||
put : ∀ se . se -> {State se} ()
|
put : ∀ se . se -> {State se} ()
|
||||||
get : ∀ se . {State se} se
|
get : ∀ se . {State se} se
|
||||||
id : Int -> Int
|
id : Int -> Int
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--State2 ability
|
--State2 ability
|
||||||
ability State se2 where
|
structural ability State se2 where
|
||||||
put : ∀ se . se -> {State se} ()
|
put : ∀ se . se -> {State se} ()
|
||||||
get : ∀ se . () -> {State se} se
|
get : ∀ se . () -> {State se} se
|
||||||
state : ∀ s a . s -> Request (State s) a -> (s, a)
|
state : ∀ s a . s -> Request (State s) a -> (s, a)
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--State2 ability
|
--State2 ability
|
||||||
ability State s where
|
structural ability State s where
|
||||||
put : s -> {State s} ()
|
put : s -> {State s} ()
|
||||||
|
|
||||||
state : s -> Request (State s) a -> a
|
state : s -> Request (State s) a -> a
|
||||||
|
@ -1,8 +1,8 @@
|
|||||||
--State2 ability
|
--State2 ability
|
||||||
|
|
||||||
type Optional a = None | Some a
|
structural type Optional a = None | Some a
|
||||||
|
|
||||||
ability State s where
|
structural ability State s where
|
||||||
put : s -> {State s} ()
|
put : s -> {State s} ()
|
||||||
get : {State s} s
|
get : {State s} s
|
||||||
|
|
||||||
|
@ -1,8 +1,8 @@
|
|||||||
--State2 ability
|
--State2 ability
|
||||||
|
|
||||||
type Optional a = None | Some a
|
structural type Optional a = None | Some a
|
||||||
|
|
||||||
ability State s where
|
structural ability State s where
|
||||||
put : s -> {State s} ()
|
put : s -> {State s} ()
|
||||||
get : {State s} s
|
get : {State s} s
|
||||||
|
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--State2 ability
|
--State2 ability
|
||||||
ability State s where
|
structural ability State s where
|
||||||
put : s -> {State s} ()
|
put : s -> {State s} ()
|
||||||
|
|
||||||
state : s -> Request (State s) a -> s
|
state : s -> Request (State s) a -> s
|
||||||
|
@ -1,8 +1,8 @@
|
|||||||
--State2 ability
|
--State2 ability
|
||||||
|
|
||||||
type Optional a = None | Some a
|
structural type Optional a = None | Some a
|
||||||
|
|
||||||
ability State s where
|
structural ability State s where
|
||||||
put : s -> {State s} ()
|
put : s -> {State s} ()
|
||||||
get : {State s} s
|
get : {State s} s
|
||||||
|
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
--State3 ability
|
--State3 ability
|
||||||
ability State se2 where
|
structural ability State se2 where
|
||||||
put : ∀ se . se -> {State se} ()
|
put : ∀ se . se -> {State se} ()
|
||||||
get : ∀ se . () -> {State se} se
|
get : ∀ se . () -> {State se} se
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
ability State s where
|
structural ability State s where
|
||||||
put : s -> {State s} ()
|
put : s -> {State s} ()
|
||||||
get : {State s} s
|
get : {State s} s
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
ability State s where
|
structural ability State s where
|
||||||
put : s -> {State s} ()
|
put : s -> {State s} ()
|
||||||
get : {State s} s
|
get : {State s} s
|
||||||
|
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
ability Emit a where
|
structural ability Emit a where
|
||||||
emit : a ->{Emit a} ()
|
emit : a ->{Emit a} ()
|
||||||
|
|
||||||
type Stream e a r = Stream ('{e, Emit a} r)
|
structural type Stream e a r = Stream ('{e, Emit a} r)
|
||||||
|
|
||||||
use Stream Stream
|
use Stream Stream
|
||||||
use Optional None Some
|
use Optional None Some
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
ability Emit a where
|
structural ability Emit a where
|
||||||
emit : a ->{Emit a} ()
|
emit : a ->{Emit a} ()
|
||||||
|
|
||||||
type Stream e a r = Stream ('{e, Emit a} r)
|
structural type Stream e a r = Stream ('{e, Emit a} r)
|
||||||
|
|
||||||
use Stream Stream
|
use Stream Stream
|
||||||
use Optional None Some
|
use Optional None Some
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
ability Emit a where
|
structural ability Emit a where
|
||||||
emit : a ->{Emit a} ()
|
emit : a ->{Emit a} ()
|
||||||
|
|
||||||
type Stream e a r = Stream ('{e, Emit a} r)
|
structural type Stream e a r = Stream ('{e, Emit a} r)
|
||||||
|
|
||||||
use Stream Stream
|
use Stream Stream
|
||||||
use Optional None Some
|
use Optional None Some
|
||||||
@ -50,7 +50,7 @@ namespace Stream where
|
|||||||
run : Stream e a r ->{e, Emit a} r
|
run : Stream e a r ->{e, Emit a} r
|
||||||
run = cases Stream c -> !c
|
run = cases Stream c -> !c
|
||||||
|
|
||||||
ability Abort where
|
structural ability Abort where
|
||||||
abort : {Abort} a
|
abort : {Abort} a
|
||||||
|
|
||||||
---
|
---
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
-- board piece
|
-- board piece
|
||||||
type P = X | O | E
|
structural type P = X | O | E
|
||||||
|
|
||||||
type Board = Board P P P P P P P P P
|
structural type Board = Board P P P P P P P P P
|
||||||
|
|
||||||
use Board Board
|
use Board Board
|
||||||
use P O X E
|
use P O X E
|
||||||
|
@ -1,6 +1,6 @@
|
|||||||
-- board piece
|
-- board piece
|
||||||
|
|
||||||
type Board = Board Nat Nat Nat
|
structural type Board = Board Nat Nat Nat
|
||||||
|
|
||||||
use Board Board
|
use Board Board
|
||||||
|
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
-- board piece
|
-- board piece
|
||||||
type P = X | O | E
|
structural type P = X | O | E
|
||||||
|
|
||||||
type Board = Board P P P P P P P P P
|
structural type Board = Board P P P P P P P P P
|
||||||
|
|
||||||
use Board Board
|
use Board Board
|
||||||
use P O X E
|
use P O X E
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
-- board piece
|
-- board piece
|
||||||
type P = X | O | E
|
structural type P = X | O | E
|
||||||
|
|
||||||
type Board = Board P P P P P P P P P
|
structural type Board = Board P P P P P P P P P
|
||||||
|
|
||||||
use Board Board
|
use Board Board
|
||||||
use P O X E
|
use P O X E
|
||||||
|
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue
Block a user