mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-17 13:27:30 +03:00
unique introduces a layout block, removed effect
keyword (and updated tests) and nicer "file typechecked" message
This commit is contained in:
parent
1a5b34f137
commit
086b01efbb
@ -215,19 +215,17 @@ notifyUser dir o = case o of
|
||||
-- Console.clearScreen
|
||||
-- Console.setCursorPosition 0 0
|
||||
Typechecked sourceName ppe uf -> do
|
||||
Console.setTitle "Unison ☺︎"
|
||||
Console.setTitle "Unison ✅"
|
||||
let terms = sortOn fst [ (HQ.fromVar v, typ) | (v, _, typ) <- join $ UF.topLevelComponents uf ]
|
||||
typeDecls =
|
||||
[ (HQ.fromVar v, Left e) | (v, (_,e)) <- Map.toList (UF.effectDeclarations' uf) ] ++
|
||||
[ (HQ.fromVar v, Right d) | (v, (_,d)) <- Map.toList (UF.dataDeclarations' uf) ]
|
||||
if UF.nonEmpty uf then putPrettyLn' . ("\n" <>) . P.okCallout . P.nonEmpty $ [
|
||||
if UF.nonEmpty uf then putPrettyLn' . ("\n" <>) . P.okCallout . P.sep "\n\n" $ [
|
||||
P.wrap $ "I found and" <> P.bold "typechecked" <> "these definitions in "
|
||||
<> P.group (P.text sourceName <> ":"),
|
||||
"",
|
||||
P.lines $
|
||||
(uncurry DeclPrinter.prettyDeclHeader <$> typeDecls) ++
|
||||
TypePrinter.prettySignatures' ppe terms,
|
||||
"",
|
||||
<> P.group (P.text sourceName <> ":"),
|
||||
P.indentN 2 . P.sepNonEmpty "\n\n" $ [
|
||||
P.lines (fmap (uncurry DeclPrinter.prettyDeclHeader) typeDecls),
|
||||
P.lines (TypePrinter.prettySignatures' ppe terms) ],
|
||||
P.wrap "Now evaluating any watch expressions (lines starting with `>`)..." ]
|
||||
else when (null $ UF.watchComponents uf) $ putPrettyLn' . P.wrap $
|
||||
"I loaded " <> P.text sourceName <> " and didn't find anything."
|
||||
|
@ -144,7 +144,7 @@ declarations = do
|
||||
|
||||
modifier :: Var v => P v (L.Token DD.Modifier)
|
||||
modifier = do
|
||||
o <- optional (exactWordyId "unique")
|
||||
o <- optional (openBlockWith "unique")
|
||||
case o of
|
||||
Nothing -> fmap (const DD.Structural) <$> P.lookAhead anyToken
|
||||
Just tok -> do
|
||||
@ -162,7 +162,7 @@ declaration = do
|
||||
|
||||
dataDeclaration :: forall v . Var v => L.Token DD.Modifier -> P v (v, DataDeclaration' v Ann)
|
||||
dataDeclaration mod = do
|
||||
_ <- openBlockWith "type"
|
||||
_ <- fmap void (reserved "type") <|> openBlockWith "type"
|
||||
(name, typeArgs) <- (,) <$> prefixVar <*> many prefixVar
|
||||
let typeArgVs = L.payload <$> typeArgs
|
||||
eq <- reserved "="
|
||||
@ -193,13 +193,13 @@ dataDeclaration mod = do
|
||||
|
||||
effectDeclaration :: Var v => L.Token DD.Modifier -> P v (v, EffectDeclaration' v Ann)
|
||||
effectDeclaration mod = do
|
||||
_ <- reserved "effect" <|> reserved "ability"
|
||||
_ <- fmap void (reserved "ability") <|> openBlockWith "ability"
|
||||
name <- prefixVar
|
||||
typeArgs <- many prefixVar
|
||||
let typeArgVs = L.payload <$> typeArgs
|
||||
blockStart <- openBlockWith "where"
|
||||
constructors <- sepBy semi (constructor name)
|
||||
_ <- closeBlock
|
||||
_ <- closeBlock <* closeBlock -- `ability` opens a block, as does `where`
|
||||
let closingAnn = last $ ann blockStart : ((\(_,_,t) -> ann t) <$> constructors)
|
||||
pure (L.payload name, DD.mkEffectDecl' (L.payload mod) (ann mod <> closingAnn) typeArgVs constructors)
|
||||
where
|
||||
|
@ -185,8 +185,8 @@ reorder ts = join . sortWith f . stanzas $ ts
|
||||
f [] = 3 :: Int
|
||||
f (t : _) = case payload $ headToken t of
|
||||
Open "type" -> 0
|
||||
Reserved "effect" -> 0
|
||||
Reserved "ability" -> 0
|
||||
Open "unique" -> 0
|
||||
Open "ability" -> 0
|
||||
Reserved "use" -> 1
|
||||
_ -> 3 :: Int
|
||||
|
||||
@ -331,7 +331,8 @@ lexer0 scope rem =
|
||||
let end = inc pos
|
||||
in case topBlockName l of
|
||||
-- '=' does not open a layout block if within a type declaration
|
||||
Just "type" -> Token (Reserved "=") pos end : goWhitespace l end rem
|
||||
Just "type" -> Token (Reserved "=") pos end : goWhitespace l end rem
|
||||
Just "unique" -> Token (Reserved "=") pos end : goWhitespace l end rem
|
||||
Just _ -> Token (Open "=") pos end : pushLayout "=" l end rem
|
||||
Nothing -> Token (Err LayoutError) pos pos : recover l pos rem
|
||||
'-' : '>' : (rem @ (c : _))
|
||||
@ -367,7 +368,17 @@ lexer0 scope rem =
|
||||
(matchKeyword -> Just (kw,rem)) ->
|
||||
let end = incBy kw pos in
|
||||
case kw of
|
||||
kw@"type" ->
|
||||
-- `unique type` lexes as [Open "unique", Reserved "type"]
|
||||
-- `type` lexes as [Open "type"]
|
||||
-- `unique ability` lexes as [Open "unique", Reserved "ability"]
|
||||
-- `ability` lexes as [Open "ability"]
|
||||
kw@"unique" ->
|
||||
Token (Open kw) pos end
|
||||
: goWhitespace ((kw, column $ inc pos) : l) end rem
|
||||
kw@"ability" | topBlockName l /= Just "unique" ->
|
||||
Token (Open kw) pos end
|
||||
: goWhitespace ((kw, column $ inc pos) : l) end rem
|
||||
kw@"type" | topBlockName l /= Just "unique" ->
|
||||
Token (Open kw) pos end
|
||||
: goWhitespace ((kw, column $ inc pos) : l) end rem
|
||||
kw | Set.member kw layoutKeywords ->
|
||||
@ -516,10 +527,10 @@ symbolyIdChars = Set.fromList "!$%^&*-=+<>.~\\/|:;"
|
||||
keywords :: Set String
|
||||
keywords = Set.fromList [
|
||||
"if", "then", "else", "forall", "∀",
|
||||
"handle", "in",
|
||||
"handle", "in", "unique",
|
||||
"where", "use",
|
||||
"and", "or", "true", "false",
|
||||
"type", "effect", "ability", "alias",
|
||||
"type", "ability", "alias",
|
||||
"let", "namespace", "case", "of"]
|
||||
|
||||
-- These keywords introduce a layout block
|
||||
|
@ -50,6 +50,7 @@ module Unison.Util.Pretty (
|
||||
renderUnbroken,
|
||||
rightPad,
|
||||
sep,
|
||||
sepNonEmpty,
|
||||
sepSpaced,
|
||||
shown,
|
||||
softbreak,
|
||||
@ -246,6 +247,9 @@ sepSpaced between = sep (between <> softbreak)
|
||||
sep :: (Foldable f, IsString s) => Pretty s -> f (Pretty s) -> Pretty s
|
||||
sep between = intercalateMap between id
|
||||
|
||||
sepNonEmpty :: (Foldable f, IsString s) => Pretty s -> f (Pretty s) -> Pretty s
|
||||
sepNonEmpty between ps = sep between (nonEmpty ps)
|
||||
|
||||
nonEmpty :: (Foldable f, IsString s) => f (Pretty s) -> [Pretty s]
|
||||
nonEmpty (toList -> l) = case l of
|
||||
(out -> Empty) : t -> nonEmpty t
|
||||
|
@ -39,7 +39,7 @@ module Unison.Test.FileParser where
|
||||
------ -- ," Just : a -> Optional a"
|
||||
------ -- ," Nothing : Optional Int"]
|
||||
, unlines -- NB: this currently fails because we don't have type AST or parser for effect types yet
|
||||
["effect State s where"
|
||||
["ability State s where"
|
||||
," get : {State s} s"
|
||||
," set : s -> {State s} ()"
|
||||
]
|
||||
|
@ -1,5 +1,5 @@
|
||||
--Abort
|
||||
effect Abort where
|
||||
ability Abort where
|
||||
Abort : forall a . () -> {Abort} a
|
||||
|
||||
bork = u -> 1 + (Abort.Abort ())
|
||||
|
@ -1,9 +1,9 @@
|
||||
type Optional a = Some a | None
|
||||
|
||||
effect Abort where
|
||||
ability Abort where
|
||||
Abort : forall a . () -> {Abort} a
|
||||
|
||||
effect Abort2 where
|
||||
ability Abort2 where
|
||||
Abort2 : forall a . () -> {Abort2} a
|
||||
Abort2' : forall a . () -> {Abort2} a
|
||||
|
||||
@ -16,8 +16,8 @@ app' = 3
|
||||
arrow : Int -> Int -> Int
|
||||
arrow a = 3
|
||||
|
||||
effect' : Nat -> { Abort } Int
|
||||
effect' n = Abort2.Abort2 ()
|
||||
ability' : Nat -> { Abort } Int
|
||||
ability' n = Abort2.Abort2 ()
|
||||
|
||||
id : forall a . a -> a
|
||||
id x = 3
|
||||
|
@ -1,8 +1,8 @@
|
||||
effect State s where
|
||||
ability State s where
|
||||
get : Nat -> {State s} s
|
||||
set : s -> {State s} ()
|
||||
|
||||
effect Console where
|
||||
ability Console where
|
||||
read : () -> {Console} (Optional Text)
|
||||
write : Text -> {Console} ()
|
||||
|
||||
|
@ -1,8 +1,8 @@
|
||||
effect State s where
|
||||
ability State s where
|
||||
get : {State s} s
|
||||
set : s -> {State s} ()
|
||||
|
||||
effect Console where
|
||||
ability Console where
|
||||
read : {Console} (Optional Text)
|
||||
write : Text -> {Console} ()
|
||||
|
||||
|
@ -1,4 +1,4 @@
|
||||
effect Abort where
|
||||
ability Abort where
|
||||
Abort : forall a . () -> {Abort} a
|
||||
|
||||
foo n = if n >= 1000 then n else !Abort.Abort
|
||||
@ -9,4 +9,4 @@ bar f i = f i
|
||||
bar foo 3
|
||||
|
||||
-- as of 3935b366383fe8184f96cfe714c31ca04234cf27, this typechecks (unexpected)
|
||||
-- and then bombs in the runtime because the Abort effect isn't handled.
|
||||
-- and then bombs in the runtime because the Abort ability isn't handled.
|
||||
|
@ -15,6 +15,6 @@ CallStack (from HasCallStack):
|
||||
-- Typechecker emits a helpful error about b's use of an unknown type, but not a's.
|
||||
--
|
||||
-- Error for b:
|
||||
-- typechecker.tests/effect_unknown_type.u FAILURE I don't know about the type Unknown. Make sure it's imported and spelled correctly:
|
||||
-- typechecker.tests/ability_unknown_type.u FAILURE I don't know about the type Unknown. Make sure it's imported and spelled correctly:
|
||||
--
|
||||
-- 22 | b : Unknown
|
||||
|
@ -1,5 +1,5 @@
|
||||
--handle inference
|
||||
effect State s where
|
||||
ability State s where
|
||||
get : ∀ s . () -> {State s} s
|
||||
set : ∀ s . s -> {State s} ()
|
||||
state : ∀ a s . s -> Effect (State s) a -> a
|
||||
|
@ -1,5 +1,5 @@
|
||||
--State3 effect
|
||||
effect State se2 where
|
||||
--State3 ability
|
||||
ability State se2 where
|
||||
put : ∀ se . se -> {State se} ()
|
||||
get : ∀ se . () -> {State se} se
|
||||
|
||||
|
@ -1,5 +1,5 @@
|
||||
--IO effect
|
||||
effect IO where
|
||||
--IO ability
|
||||
ability IO where
|
||||
launchMissiles : () -> {IO} ()
|
||||
-- binding is not guarded by a lambda, it only can access
|
||||
-- ambient abilities (which will be empty)
|
||||
|
@ -1,7 +1,7 @@
|
||||
--IO/State1 effect
|
||||
effect IO where
|
||||
--IO/State1 ability
|
||||
ability IO where
|
||||
launchMissiles : {IO} ()
|
||||
effect State se2 where
|
||||
ability State se2 where
|
||||
put : ∀ se . se -> {State se} ()
|
||||
get : ∀ se . () -> {State se} se
|
||||
foo : () -> {IO} ()
|
||||
|
@ -1,6 +1,6 @@
|
||||
|
||||
-- A simple distributed computation effect
|
||||
effect Remote n where
|
||||
-- A simple distributed computation ability
|
||||
ability Remote n where
|
||||
|
||||
-- Spawn a new node, of type `n`
|
||||
spawn : {Remote n} n
|
||||
|
@ -1,5 +1,5 @@
|
||||
--map/traverse
|
||||
effect Noop where
|
||||
ability Noop where
|
||||
noop : a -> {Noop} a
|
||||
|
||||
type List a = Nil | Cons a (List a)
|
||||
|
@ -8,7 +8,7 @@ reduce2 a0 f s = case at 0 s of
|
||||
-- as of commit a48fa3b, we get the following error
|
||||
|
||||
--The expression at Line 18, columns 40-41 (in red below) is requesting
|
||||
-- {𝛆3} effects, but this location only has access to
|
||||
-- {𝛆3} abilitys, but this location only has access to
|
||||
-- {}
|
||||
--
|
||||
-- 18 | Optional.Some a1 -> reduce (f a0 a1) f (drop 1 s)
|
||||
@ -17,7 +17,7 @@ reduce2 a0 f s = case at 0 s of
|
||||
-- AbilityCheckFailure: ambient={} requested={𝛆3}
|
||||
|
||||
-- The problem is that I've accidentally called `reduce` instead of `reduce2`,
|
||||
-- which TDNRs to `Stream.reduce`, which doesn't allow effects, and `f` isn't
|
||||
-- which TDNRs to `Stream.reduce`, which doesn't allow abilitys, and `f` isn't
|
||||
-- restricted to be pure.
|
||||
|
||||
-- I'd like to know:
|
||||
|
@ -4,11 +4,11 @@
|
||||
-- expecting : or the rest of infixApp
|
||||
-- 51 | ()
|
||||
|
||||
effect State s where
|
||||
ability State s where
|
||||
get : {State s} s
|
||||
set : s -> {State s} ()
|
||||
|
||||
effect Console where
|
||||
ability Console where
|
||||
read : {Console} (Optional Text)
|
||||
write : Text -> {Console} ()
|
||||
|
||||
|
@ -7,7 +7,7 @@
|
||||
|
||||
type Optional a = None | Some a
|
||||
|
||||
effect State s where
|
||||
ability State s where
|
||||
put : s -> {State s} ()
|
||||
get : {State s} s
|
||||
|
||||
|
@ -11,7 +11,7 @@
|
||||
--
|
||||
-- Verbiage could be improved, but also the `()` location should
|
||||
-- point to line 22, the `k ()` call.
|
||||
effect Ask foo where
|
||||
ability Ask foo where
|
||||
ask : () -> {Ask a} a
|
||||
|
||||
supply : Text -> Effect (Ask Text) a -> a
|
||||
|
@ -10,7 +10,7 @@
|
||||
--
|
||||
-- even though this program doesn't use guards!
|
||||
|
||||
effect Ask a where
|
||||
ability Ask a where
|
||||
ask : {Ask a} a
|
||||
|
||||
supply : Text -> Effect (Ask Text) a -> a
|
||||
|
@ -1,5 +1,5 @@
|
||||
--State4 effect
|
||||
effect State se2 where
|
||||
--State4 ability
|
||||
ability State se2 where
|
||||
put : ∀ se . se -> {State se} ()
|
||||
get : ∀ se . () -> {State se} se
|
||||
-- binding is not guarded by a lambda, it only can access
|
||||
|
@ -1,4 +1,4 @@
|
||||
effect State s where
|
||||
ability State s where
|
||||
get : () -> {State s} s
|
||||
set : s -> {State s} ()
|
||||
|
||||
|
@ -1,11 +1,11 @@
|
||||
effect Abort where
|
||||
ability Abort where
|
||||
Abort : forall a . () -> {Abort} a
|
||||
|
||||
effect Abort2 where
|
||||
ability Abort2 where
|
||||
Abort2 : forall a . () -> {Abort2} a
|
||||
Abort2' : forall a . () -> {Abort2} a
|
||||
|
||||
effect' : Nat -> { Abort } Int
|
||||
effect' n = Abort2.Abort2 ()
|
||||
ability' : Nat -> { Abort } Int
|
||||
ability' n = Abort2.Abort2 ()
|
||||
|
||||
()
|
||||
|
@ -1,11 +1,11 @@
|
||||
effect Abort where
|
||||
ability Abort where
|
||||
Abort : forall a . () -> {Abort} a
|
||||
|
||||
effect Abort2 where
|
||||
ability Abort2 where
|
||||
Abort2 : forall a . () -> {Abort2} a
|
||||
|
||||
effect' : Nat -> { Abort } Int
|
||||
effect' n = Abort2.Abort2 ()
|
||||
ability' : Nat -> { Abort } Int
|
||||
ability' n = Abort2.Abort2 ()
|
||||
|
||||
()
|
||||
|
||||
|
@ -1,5 +1,5 @@
|
||||
--Abort
|
||||
effect Abort where
|
||||
ability Abort where
|
||||
Abort : forall a . () -> {Abort} a
|
||||
|
||||
use Nat +
|
||||
|
@ -1,5 +1,5 @@
|
||||
|
||||
effect Ask a where
|
||||
ability Ask a where
|
||||
ask : {Ask a} a
|
||||
|
||||
supply : Text -> Effect (Ask Text) a -> a
|
||||
|
@ -1,5 +1,5 @@
|
||||
--Abort
|
||||
effect Abort where
|
||||
ability Abort where
|
||||
Abort : forall a . () -> {Abort} a
|
||||
eff : forall a b . (a -> b) -> b -> Effect Abort a -> b
|
||||
eff f z e = case e of
|
||||
|
@ -1,14 +1,14 @@
|
||||
--Ask inferred
|
||||
|
||||
effect Ask a where
|
||||
ability Ask a where
|
||||
ask : {Ask a} a
|
||||
|
||||
effect AskU where
|
||||
ability AskU where
|
||||
ask : {AskU} Nat
|
||||
|
||||
use Nat +
|
||||
|
||||
effect AskT where
|
||||
ability AskT where
|
||||
ask : {AskT} Text
|
||||
|
||||
x = '(Ask.ask + 1)
|
||||
|
@ -1,8 +1,8 @@
|
||||
effect State s where
|
||||
ability State s where
|
||||
get : {State s} s
|
||||
set : s -> {State s} ()
|
||||
|
||||
effect Console where
|
||||
ability Console where
|
||||
read : {Console} (Optional Text)
|
||||
write : Text -> {Console} ()
|
||||
|
||||
|
@ -1,11 +1,11 @@
|
||||
-- This confusingly gives an error that
|
||||
-- it doesn't know what `Console.simulate` is.
|
||||
|
||||
effect State s where
|
||||
ability State s where
|
||||
get : {State s} s
|
||||
set : s -> {State s} ()
|
||||
|
||||
effect Console where
|
||||
ability Console where
|
||||
read : {Console} (Optional Text)
|
||||
write : Text -> {Console} ()
|
||||
|
||||
|
@ -1,4 +1,4 @@
|
||||
effect T where
|
||||
ability T where
|
||||
foo : {T} ()
|
||||
|
||||
-- parses fine
|
||||
|
@ -2,7 +2,7 @@
|
||||
blah : a -> a -> a
|
||||
blah a a2 = a2
|
||||
|
||||
effect Foo where
|
||||
ability Foo where
|
||||
foo : {Foo} Text
|
||||
|
||||
-- previously this didn't work as first argument was pure
|
||||
|
@ -4,7 +4,7 @@ eff f z e = case e of
|
||||
{ Abort.Abort _ -> k } -> z
|
||||
{ a } -> f a
|
||||
|
||||
effect Abort where
|
||||
ability Abort where
|
||||
Abort : forall a . () -> {Abort} a
|
||||
|
||||
|
||||
|
@ -3,4 +3,4 @@
|
||||
|
||||
-- /Users/arya/unison/unison-src/tests/empty-above-the-fold.u:1:1:
|
||||
-- unexpected end of input
|
||||
-- expecting ability, effect, or use
|
||||
-- expecting ability, ability, or use
|
||||
|
@ -1,4 +1,4 @@
|
||||
effect Woot where woot : {Woot} Text
|
||||
ability Woot where woot : {Woot} Text
|
||||
|
||||
force : '{e} a ->{e} a
|
||||
force a = !a
|
||||
|
@ -13,11 +13,11 @@ replicate n x =
|
||||
!x
|
||||
replicate (n `drop` 1) x
|
||||
|
||||
effect State a where
|
||||
ability State a where
|
||||
get : {State a} a
|
||||
put : a -> {State a} ()
|
||||
|
||||
effect Writer w where
|
||||
ability Writer w where
|
||||
tell : w -> {Writer w} ()
|
||||
|
||||
stateHandler : s -> Effect {State s} a -> (s, a)
|
||||
|
@ -1,5 +1,5 @@
|
||||
--IO/State2 effect
|
||||
effect IO where
|
||||
--IO/State2 ability
|
||||
ability IO where
|
||||
launchMissiles : {IO} ()
|
||||
|
||||
foo : () -> {IO} ()
|
||||
@ -14,7 +14,7 @@ foo unit =
|
||||
type Optional a =
|
||||
Some a | None
|
||||
|
||||
effect State se2 where
|
||||
ability State se2 where
|
||||
put : ∀ se . se -> {State se} ()
|
||||
get : ∀ se . {State se} se
|
||||
|
||||
|
@ -1,5 +1,5 @@
|
||||
--IO3 effect
|
||||
effect IO where
|
||||
--IO3 ability
|
||||
ability IO where
|
||||
launchMissiles : () -> {IO} ()
|
||||
-- binding IS guarded, so its body can access whatever abilities
|
||||
-- are declared by the type of the binding
|
||||
|
@ -1,8 +1,8 @@
|
||||
--map/traverse
|
||||
effect Noop where
|
||||
ability Noop where
|
||||
noop : ∀ a . a -> {Noop} a
|
||||
|
||||
effect Noop2 where
|
||||
ability Noop2 where
|
||||
noop2 : ∀ a . a -> a -> {Noop2} a
|
||||
|
||||
type List a = Nil | Cons a (List a)
|
||||
@ -21,11 +21,11 @@ ex = (c 1 (c 2 (c 3 z)))
|
||||
pureMap : List Text
|
||||
pureMap = map (a -> "hello") ex
|
||||
|
||||
-- `map` is effect polymorphic
|
||||
-- `map` is ability polymorphic
|
||||
zappy : () -> {Noop} (List Nat)
|
||||
zappy u = map (zap -> (Noop.noop (zap Nat.+ 1))) ex
|
||||
|
||||
-- mixing multiple effects in a call to `map` works fine
|
||||
-- mixing multiple abilitys in a call to `map` works fine
|
||||
zappy2 : () -> {Noop, Noop2} (List Nat)
|
||||
zappy2 u = map (zap -> Noop.noop (zap Nat.+ Noop2.noop2 2 7)) ex
|
||||
|
||||
|
@ -1,8 +1,8 @@
|
||||
--map/traverse
|
||||
effect Noop where
|
||||
ability Noop where
|
||||
noop : a -> {Noop} a
|
||||
|
||||
effect Noop2 where
|
||||
ability Noop2 where
|
||||
noop2 : a -> a -> {Noop2} a
|
||||
|
||||
type List a = Nil | Cons a (List a)
|
||||
@ -22,11 +22,11 @@ ex = (c 1 (c 2 (c 3 z)))
|
||||
pureMap : List Text
|
||||
pureMap = map (a -> "hello") ex
|
||||
|
||||
-- `map` is effect polymorphic
|
||||
-- `map` is ability polymorphic
|
||||
zappy : '{Noop} (List Nat)
|
||||
zappy = 'let map (zap -> Noop.noop (zap Nat.+ 1)) ex
|
||||
|
||||
-- mixing multiple effects in a call to `map` works fine
|
||||
-- mixing multiple abilitys in a call to `map` works fine
|
||||
zappy2 : '{Noop, Noop2} (List Nat)
|
||||
zappy2 = 'let
|
||||
map (zap -> Noop.noop (zap Nat.+ Noop2.noop2 2 7)) ex
|
||||
|
@ -1,8 +1,8 @@
|
||||
effect State s where
|
||||
ability State s where
|
||||
get : {State s} s
|
||||
set : s -> {State s} ()
|
||||
|
||||
effect Console where
|
||||
ability Console where
|
||||
read : {Console} (Optional Text)
|
||||
write : Text -> {Console} ()
|
||||
|
||||
|
@ -1,5 +1,5 @@
|
||||
--State1 effect
|
||||
effect State se2 where
|
||||
--State1 ability
|
||||
ability State se2 where
|
||||
put : ∀ se . se -> {State se} ()
|
||||
get : ∀ se . () -> {State se} se
|
||||
|
||||
|
@ -1,5 +1,5 @@
|
||||
--State1a effect
|
||||
effect State se2 where
|
||||
--State1a ability
|
||||
ability State se2 where
|
||||
put : ∀ se . se -> {State se} ()
|
||||
get : ∀ se . {State se} se
|
||||
id : Int -> Int
|
||||
|
@ -1,5 +1,5 @@
|
||||
--State2 effect
|
||||
effect State se2 where
|
||||
--State2 ability
|
||||
ability State se2 where
|
||||
put : ∀ se . se -> {State se} ()
|
||||
get : ∀ se . () -> {State se} se
|
||||
state : ∀ s a . s -> Effect (State s) a -> (s, a)
|
||||
|
@ -1,5 +1,5 @@
|
||||
--State2 effect
|
||||
effect State s where
|
||||
--State2 ability
|
||||
ability State s where
|
||||
put : s -> {State s} ()
|
||||
|
||||
state : s -> Effect (State s) a -> a
|
||||
|
@ -1,8 +1,8 @@
|
||||
--State2 effect
|
||||
--State2 ability
|
||||
|
||||
type Optional a = None | Some a
|
||||
|
||||
effect State s where
|
||||
ability State s where
|
||||
put : s -> {State s} ()
|
||||
get : {State s} s
|
||||
|
||||
|
@ -1,8 +1,8 @@
|
||||
--State2 effect
|
||||
--State2 ability
|
||||
|
||||
type Optional a = None | Some a
|
||||
|
||||
effect State s where
|
||||
ability State s where
|
||||
put : s -> {State s} ()
|
||||
get : {State s} s
|
||||
|
||||
|
@ -1,5 +1,5 @@
|
||||
--State2 effect
|
||||
effect State s where
|
||||
--State2 ability
|
||||
ability State s where
|
||||
put : s -> {State s} ()
|
||||
|
||||
state : s -> Effect (State s) a -> s
|
||||
|
@ -1,8 +1,8 @@
|
||||
--State2 effect
|
||||
--State2 ability
|
||||
|
||||
type Optional a = None | Some a
|
||||
|
||||
effect State s where
|
||||
ability State s where
|
||||
put : s -> {State s} ()
|
||||
get : {State s} s
|
||||
|
||||
|
@ -1,5 +1,5 @@
|
||||
--State3 effect
|
||||
effect State se2 where
|
||||
--State3 ability
|
||||
ability State se2 where
|
||||
put : ∀ se . se -> {State se} ()
|
||||
get : ∀ se . () -> {State se} se
|
||||
|
||||
|
@ -1,4 +1,4 @@
|
||||
effect State s where
|
||||
ability State s where
|
||||
put : s -> {State s} ()
|
||||
get : {State s} s
|
||||
|
||||
|
@ -1,4 +1,4 @@
|
||||
effect State s where
|
||||
ability State s where
|
||||
put : s -> {State s} ()
|
||||
get : {State s} s
|
||||
|
||||
|
28
unison-src/tests/unique.u
Normal file
28
unison-src/tests/unique.u
Normal file
@ -0,0 +1,28 @@
|
||||
|
||||
unique ability Zing where zing : {Zang} Nat
|
||||
|
||||
unique[asdlfkjasdflkj] ability Zang where
|
||||
zang : {Zing} Nat
|
||||
|
||||
unique
|
||||
ability Blarg where
|
||||
oog : {Blarg} Text
|
||||
|
||||
unique type Bool = T | F
|
||||
|
||||
unique[sdalfkjsdf] type BetterBool = Ya | Nah
|
||||
|
||||
unique[asdflkajsdf] type Day
|
||||
= Sun | Mon | Tue | Wed | Thu | Fri | Sat
|
||||
|
||||
id x = x
|
||||
|
||||
unique type Day2
|
||||
= Sun
|
||||
| Mon
|
||||
| Tue
|
||||
| Wed
|
||||
| Thu
|
||||
| Fri
|
||||
| Sat
|
||||
|
Loading…
Reference in New Issue
Block a user