mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-21 15:28:15 +03:00
fix pretty-printing of handle blocks and fix tests broken by handle-with syntax
This commit is contained in:
parent
df7193c4fe
commit
ec87a60254
@ -195,12 +195,22 @@ pretty0
|
||||
elideFQN im $ PrettyPrintEnv.termName n (Referent.Con ref i CT.Data)
|
||||
Request' ref i -> styleHashQualified'' (fmt S.Request) $
|
||||
elideFQN im $ PrettyPrintEnv.termName n (Referent.Con ref i CT.Effect)
|
||||
Handle' h body -> let (imBody, usesBody) = calcImports im body
|
||||
(imH, usesH) = calcImports im h in
|
||||
paren (p >= 2)
|
||||
$ (fmt S.ControlKeyword "handle" `PP.hang` usesBody [pretty0 n (ac 2 Block imBody doc) body])
|
||||
<> PP.softbreak
|
||||
<> (fmt S.ControlKeyword "with" `PP.hang` usesH [pretty0 n (ac 2 Block imH doc) h])
|
||||
Handle' h body -> paren (p >= 2) $
|
||||
if height > 0 then PP.lines [
|
||||
(fmt S.ControlKeyword "handle") `PP.hang` pb,
|
||||
(fmt S.ControlKeyword "with") `PP.hang` ph
|
||||
]
|
||||
else PP.spaced [
|
||||
(fmt S.ControlKeyword "handle") `PP.hang` pb
|
||||
<> PP.softbreak
|
||||
<> (fmt S.ControlKeyword "with") `PP.hang` ph
|
||||
]
|
||||
where
|
||||
height = PP.preferredHeight pb `max` PP.preferredHeight ph
|
||||
pb = pblock body
|
||||
ph = pblock h
|
||||
pblock tm = let (im', uses) = calcImports im tm
|
||||
in uses $ [pretty0 n (ac 0 Block im' doc) tm]
|
||||
App' x (Constructor' DD.UnitRef 0) ->
|
||||
paren (p >= 11) $ (fmt S.DelayForceChar $ l "!") <> pretty0 n (ac 11 Normal im doc) x
|
||||
LamNamed' v x | (Var.name v) == "()" ->
|
||||
|
@ -82,13 +82,15 @@ test1 = scope "termparser" . tests . map parses $
|
||||
" x + 1 )"
|
||||
--
|
||||
-- Handlers
|
||||
,"handle foo in \n" ++
|
||||
, "handle\n" ++
|
||||
" x = 23 + 42\n" ++
|
||||
" x + foo 8 102.0 +4"
|
||||
, "handle foo in \n" ++
|
||||
" x + foo 8 102.0 +4\n" ++
|
||||
"with foo"
|
||||
, "handle\n" ++
|
||||
" x = 1\n" ++
|
||||
" x"
|
||||
, "handle foo in x"
|
||||
" x\n" ++
|
||||
"with foo"
|
||||
, "handle x with foo"
|
||||
|
||||
-- Patterns
|
||||
, "case x of x -> x"
|
||||
|
@ -124,7 +124,7 @@ test = scope "termprinter" . tests $
|
||||
, tc "List.empty"
|
||||
, tc "None"
|
||||
, tc "Optional.None"
|
||||
, tc "handle foo in bar"
|
||||
, tc "handle foo with bar"
|
||||
, tc "Cons 1 1"
|
||||
, tc "let\n\
|
||||
\ x = 1\n\
|
||||
@ -160,13 +160,13 @@ test = scope "termprinter" . tests $
|
||||
, pending $ tc "case e of { () -> k } -> z" -- TODO doesn't parse since 'many leaf' expected before the "-> k"
|
||||
-- need an actual effect constructor to test this with
|
||||
, tc "if a then if b then c else d else e"
|
||||
, tc "handle foo in (handle bar in baz)"
|
||||
, tc "handle handle foo with bar with baz"
|
||||
, tcBreaks 16 "case (if a then\n\
|
||||
\ b\n\
|
||||
\else c) of\n\
|
||||
\ 112 -> x" -- dodgy layout. note #517 and #518
|
||||
, tc "handle Pair 1 1 in bar"
|
||||
, tc "handle x -> foo in bar"
|
||||
, tc "handle bar with Pair 1 1"
|
||||
, tc "handle bar with x -> foo"
|
||||
, tcDiffRtt True "let\n\
|
||||
\ x = (1 : Int)\n\
|
||||
\ (x : Int)"
|
||||
@ -248,12 +248,13 @@ test = scope "termprinter" . tests $
|
||||
\ baz.f : Int -> Int\n\
|
||||
\ baz.f x = x\n\
|
||||
\ 13"
|
||||
, pending $ tcBreaks 90 "handle foo in\n\
|
||||
, tcBreaks 90 "handle\n\
|
||||
\ a = 5\n\
|
||||
\ b =\n\
|
||||
\ c = 3\n\
|
||||
\ true\n\
|
||||
\ false" -- TODO comes back out with line breaks around foo
|
||||
\ false\n\
|
||||
\with foo"
|
||||
, tcBreaks 50 "case x of\n\
|
||||
\ true ->\n\
|
||||
\ d = 1\n\
|
||||
@ -419,28 +420,24 @@ test = scope "termprinter" . tests $
|
||||
\else\n\
|
||||
\ use A X.c YY.c\n\
|
||||
\ g X.c X.c YY.c YY.c"
|
||||
, tcBreaks 20 "handle bar in\n\
|
||||
\ (if foo then\n\
|
||||
, tcBreaks 20 "handle\n\
|
||||
\ if foo then\n\
|
||||
\ use A.X c\n\
|
||||
\ f c c\n\
|
||||
\ else\n\
|
||||
\ use A.Y c\n\
|
||||
\ g c c)" -- questionable parentheses, issue #517
|
||||
\ g c c\n\
|
||||
\with bar"
|
||||
, tcBreaks 28 "if foo then\n\
|
||||
\ f (x : (∀ t. Pair t t))\n\
|
||||
\else\n\
|
||||
\ f (x : (∀ t. Pair t t))"
|
||||
, tcDiffRtt False "handle foo in\n\
|
||||
\ use A x\n\
|
||||
\ (if f x x then\n\
|
||||
\ x\n\
|
||||
\ else y)" -- missing break before 'then', issue #518; surplus parentheses #517
|
||||
"handle foo\n\
|
||||
\in\n\
|
||||
\ use A x\n\
|
||||
\ (if f x x then\n\
|
||||
\ x\n\
|
||||
\ else y)" 15 -- parser doesn't like 'in' beginning a line
|
||||
, tcBreaks 15 "handle\n\
|
||||
\ use A x\n\
|
||||
\ if f x x then\n\
|
||||
\ x\n\
|
||||
\ else y\n\
|
||||
\with foo" -- missing break before 'then', issue #518
|
||||
, tcBreaks 20 "case x of\n\
|
||||
\ () ->\n\
|
||||
\ use A y\n\
|
||||
@ -450,9 +447,10 @@ test = scope "termprinter" . tests $
|
||||
\ f x x\n\
|
||||
\ c = g x x\n\
|
||||
\ h x x"
|
||||
, tcBreaks 15 "handle foo in\n\
|
||||
, tcBreaks 15 "handle\n\
|
||||
\ use A x\n\
|
||||
\ f x x"
|
||||
\ f x x\n\
|
||||
\with foo"
|
||||
, tcBreaks 15 "let\n\
|
||||
\ c =\n\
|
||||
\ use A x\n\
|
||||
@ -466,11 +464,12 @@ test = scope "termprinter" . tests $
|
||||
\ a =\n\
|
||||
\ use A B.x\n\
|
||||
\ f B.x B.x\n\
|
||||
\ handle foo in\n\
|
||||
\ handle\n\
|
||||
\ q =\n\
|
||||
\ use A.B.D x\n\
|
||||
\ h x x\n\
|
||||
\ foo\n\
|
||||
\ with foo\n\
|
||||
\ bar\n\
|
||||
\ _ ->\n\
|
||||
\ b =\n\
|
||||
@ -479,9 +478,10 @@ test = scope "termprinter" . tests $
|
||||
\ bar"
|
||||
, tcBreaks 20 "let\n\
|
||||
\ a =\n\
|
||||
\ handle foo in\n\
|
||||
\ handle\n\
|
||||
\ use A x\n\
|
||||
\ f x x\n\
|
||||
\ with foo\n\
|
||||
\ bar"
|
||||
, tcBreaks 16 "let\n\
|
||||
\ a =\n\
|
||||
|
@ -40,7 +40,7 @@ test = scope "> extractor" . tests $
|
||||
"xyz default abort = case abort of\n" ++
|
||||
" {a} -> 3\n" ++
|
||||
" {Abort.abort -> k} ->\n" ++
|
||||
" handle xyz default in k 100\n"
|
||||
" handle k 100 with xyz default\n"
|
||||
) Err.matchBody
|
||||
]
|
||||
where y, n :: String -> ErrorExtractor Symbol Ann a -> Test ()
|
||||
|
@ -6,8 +6,8 @@ eff f z e = case e of
|
||||
{ Abort.Abort _ -> k } -> z
|
||||
{ a } -> f a
|
||||
-- heff : Nat
|
||||
heff = handle eff (x -> x Nat.+ 2) 1 in Abort.Abort ()
|
||||
heff = handle Abort.Abort () with eff (x -> x Nat.+ 2) 1
|
||||
hudy : Nat
|
||||
hudy = handle eff (x -> x Nat.+ 2) 1 in 42
|
||||
hudy = handle 42 with eff (x -> x Nat.+ 2) 1
|
||||
bork : () -> {Abort} Nat
|
||||
bork = u -> 1 Nat.+ (Abort.Abort ())
|
||||
|
@ -32,10 +32,10 @@ Remote.runLocal : '{Remote} a -> a
|
||||
Remote.runLocal r =
|
||||
step nid r = case r of
|
||||
{a} -> a
|
||||
{Remote.fork t -> k} -> handle (step nid) in k (Future.fromThunk t)
|
||||
{Remote.spawn -> k} -> handle (step (Node.increment nid)) in k nid
|
||||
{Remote.at _ t -> k} -> handle (step nid) in k !t
|
||||
handle (step (Node.Node 0)) in !r
|
||||
{Remote.fork t -> k} -> handle k (Future.fromThunk t) with step nid
|
||||
{Remote.spawn -> k} -> handle k nid with step (Node.increment nid)
|
||||
{Remote.at _ t -> k} -> handle k !t with step nid
|
||||
handle !r with step (Node.Node 0)
|
||||
|
||||
Remote.forkAt : Node -> '{Remote} a ->{Remote} (Future a)
|
||||
Remote.forkAt node r = Remote.fork '(Remote.at node r)
|
||||
|
@ -15,8 +15,8 @@ namespace Console where
|
||||
|
||||
state : s -> Request (State s) a -> a
|
||||
state s c = case c of
|
||||
{State.get -> k} -> handle state s in k s
|
||||
{State.set s' -> k} -> handle state s' in k ()
|
||||
{State.get -> k} -> handle k s with state s
|
||||
{State.set s' -> k} -> handle k () with state s'
|
||||
{a} -> a
|
||||
|
||||
simulate : Request Console d -> {State ([Text], [Text])} d
|
||||
@ -29,24 +29,26 @@ namespace Console where
|
||||
-- this really should typecheck but doesn't for some reason
|
||||
-- error is that `simulate` doesn't check against `Request Console c -> r`,
|
||||
-- but seems like that `r` should get instantiated as `{State (..)} c`.
|
||||
handle simulate in k (at 0 ins)
|
||||
handle k (at 0 ins) with simulate
|
||||
{Console.write t -> k} ->
|
||||
io = State.get
|
||||
ins = fst io
|
||||
outs = snd io
|
||||
-- same deal here
|
||||
handle simulate in k (State.set (ins, cons t outs))
|
||||
handle k (State.set (ins, cons t outs)) with simulate
|
||||
{a} -> a
|
||||
|
||||
(++) = (Text.++)
|
||||
|
||||
x = handle Console.state ([],[]) in
|
||||
handle Console.simulate in
|
||||
x = handle
|
||||
handle
|
||||
use Console read write
|
||||
use Optional Some None
|
||||
write "What's your name?"
|
||||
case read of
|
||||
Some name -> write ("Hello" ++ name)
|
||||
None -> write "Fine, be that way."
|
||||
with Console.simulate
|
||||
with Console.state ([],[])
|
||||
|
||||
> x
|
||||
|
@ -19,24 +19,27 @@ namespace Console where
|
||||
|
||||
simulate : Request Console a -> {State ([Text], [Text])} a
|
||||
simulate c = case c of
|
||||
{Console.read -> k} -> handle simulate in
|
||||
io = State.get
|
||||
ins = fst io
|
||||
outs = snd io
|
||||
State.set (drop 1 ins, outs)
|
||||
k (at 0 ins)
|
||||
{Console.write t -> k} -> handle simulate in
|
||||
io = State.get
|
||||
ins = fst io
|
||||
outs = snd io
|
||||
State.set (ins, outs ++ [t])
|
||||
k ()
|
||||
{Console.read -> k} -> handle
|
||||
io = State.get
|
||||
ins = fst io
|
||||
outs = snd io
|
||||
State.set (drop 1 ins, outs)
|
||||
k (at 0 ins)
|
||||
with simulate
|
||||
|
||||
e = 'let handle simulate in
|
||||
use Console read write
|
||||
use Optional Some None
|
||||
write "What's your name?"
|
||||
case read of
|
||||
Some name -> write ("Hello" ++ name)
|
||||
None -> write "Fine, be that way."
|
||||
{Console.write t -> k} -> handle
|
||||
io = State.get
|
||||
ins = fst io
|
||||
outs = snd io
|
||||
State.set (ins, outs ++ [t])
|
||||
k ()
|
||||
with simulate
|
||||
|
||||
e = 'let handle
|
||||
use Console read write
|
||||
use Optional Some None
|
||||
write "What's your name?"
|
||||
case read of
|
||||
Some name -> write ("Hello" ++ name)
|
||||
None -> write "Fine, be that way."
|
||||
with simulate
|
||||
|
@ -1,9 +1,11 @@
|
||||
use State get put
|
||||
use Writer tell
|
||||
|
||||
> handle stateHandler "hello" in
|
||||
handle writerHandler [] in
|
||||
replicate 5 main
|
||||
> handle
|
||||
handle replicate 5 main
|
||||
with writerHandler []
|
||||
with stateHandler "hello"
|
||||
|
||||
|
||||
main = '(tell get)
|
||||
|
||||
@ -22,11 +24,11 @@ ability Writer w where
|
||||
|
||||
stateHandler : s -> Request {State s} a -> (s, a)
|
||||
stateHandler s x = case x of
|
||||
{ State.get -> k } -> handle stateHandler s in k s
|
||||
{ State.put s -> k } -> handle stateHandler s in k ()
|
||||
{ State.get -> k } -> handle k s with stateHandler s
|
||||
{ State.put s -> k } -> handle k () with stateHandler s
|
||||
{ a } -> (s, a)
|
||||
|
||||
writerHandler : [w] -> Request {Writer w} a -> ([w], a)
|
||||
writerHandler ww x = case x of
|
||||
{ Writer.tell w -> k } -> handle writerHandler (ww `snoc` w) in k ()
|
||||
{ Writer.tell w -> k } -> handle k () with writerHandler (ww `snoc` w)
|
||||
{ a } -> (ww, a)
|
||||
|
@ -31,10 +31,10 @@ Remote.runLocal r =
|
||||
use Future Future
|
||||
step nid r = case r of
|
||||
{a} -> a
|
||||
{Remote.fork t -> k} -> handle (step nid) in k (Future t)
|
||||
{Remote.spawn -> k} -> handle (step (Node.increment nid)) in k nid
|
||||
{Remote.at _ t -> k} -> handle (step nid) in k !t
|
||||
handle (step (Node.Node 0)) in !r
|
||||
{Remote.fork t -> k} -> handle k (Future t) with step nid
|
||||
{Remote.spawn -> k} -> handle k nid with step (Node.increment nid)
|
||||
{Remote.at _ t -> k} -> handle k !t with step nid
|
||||
handle !r with step (Node.Node 0)
|
||||
|
||||
Remote.forkAt : Node -> '{Remote} a ->{Remote} (Future a)
|
||||
Remote.forkAt node r = Remote.fork '(Remote.at node r)
|
||||
|
@ -6,13 +6,13 @@ ability A where
|
||||
|
||||
unA w = case w of
|
||||
{a} -> a
|
||||
{A.woot -> k} -> handle unA in k 10
|
||||
{A.woot -> k} -> handle k 10 with unA
|
||||
|
||||
-- This verifies that the continuation captures local variables
|
||||
a1 = handle unA in
|
||||
x = 42
|
||||
y = A.woot
|
||||
x
|
||||
a1 = handle
|
||||
x = 42
|
||||
y = A.woot
|
||||
x
|
||||
with unA
|
||||
|
||||
> a1 -- should be 42
|
||||
|
||||
|
@ -8,31 +8,33 @@ ability Zing where
|
||||
|
||||
unzing z = case z of
|
||||
{a} -> a
|
||||
{Zing.zing n -> k} -> handle unzing in k (x -> x `drop` n)
|
||||
{Zing.zing2 n1 n2 -> k} -> handle unzing in k (n3 n4 -> [n1, n2, n3, n4])
|
||||
{Zing.zing n -> k} -> handle k (x -> x `drop` n) with unzing
|
||||
{Zing.zing2 n1 n2 -> k} -> handle k (n3 n4 -> [n1, n2, n3, n4]) with unzing
|
||||
|
||||
exacth = handle unzing in
|
||||
exacth = handle
|
||||
f = Zing.zing 3
|
||||
f 20 + 1
|
||||
with unzing
|
||||
|
||||
overapplyh = handle unzing in
|
||||
overapplyh = handle
|
||||
Zing.zing 3 20 + 1
|
||||
with unzing
|
||||
|
||||
-- SEQUENCES with abilities
|
||||
|
||||
sequence1 = handle unzing in [Zing.zing 1 4]
|
||||
sequence2 = handle unzing in [Zing.zing 1 4, Zing.zing 1 4]
|
||||
sequence3 = handle unzing in [Zing.zing 1 4, Zing.zing 2 4, Zing.zing 3 4, Zing.zing 4 4]
|
||||
sequence1 = handle [Zing.zing 1 4] with unzing
|
||||
sequence2 = handle [Zing.zing 1 4, Zing.zing 1 4] with unzing
|
||||
sequence3 = handle [Zing.zing 1 4, Zing.zing 2 4, Zing.zing 3 4, Zing.zing 4 4] with unzing
|
||||
|
||||
-- Overapply of requests
|
||||
|
||||
overapplyh2 = handle unzing in Zing.zing2 1 2 3 4
|
||||
overapplyh2 = handle Zing.zing2 1 2 3 4 with unzing
|
||||
|
||||
overapplyh3a = handle unzing in Zing.zing2 1 2 3 4 ++ [5]
|
||||
overapplyh3a = handle Zing.zing2 1 2 3 4 ++ [5] with unzing
|
||||
|
||||
overapplyh3b = handle unzing in Zing.zing2 1 2 3 4 ++ [5, Zing.zing 2 8]
|
||||
overapplyh3b = handle Zing.zing2 1 2 3 4 ++ [5, Zing.zing 2 8] with unzing
|
||||
|
||||
overapplyh3c = handle unzing in Zing.zing2 1 2 3 4 ++ [5, Zing.zing 2 7 + 1]
|
||||
overapplyh3c = handle Zing.zing2 1 2 3 4 ++ [5, Zing.zing 2 7 + 1] with unzing
|
||||
|
||||
> (exacth,
|
||||
overapplyh,
|
||||
|
@ -9,8 +9,8 @@ ability Console where
|
||||
namespace Console where
|
||||
state : s -> Request (State s) a -> a
|
||||
state s c = case c of
|
||||
{State.get -> k} -> handle state s in k s
|
||||
{State.set s' -> k} -> handle state s' in k ()
|
||||
{State.get -> k} -> handle k s with state s
|
||||
{State.set s' -> k} -> handle k () with state s'
|
||||
{a} -> a
|
||||
|
||||
multiHandler : s -> [w] -> Nat -> Request {State s, Console} a -> ()
|
||||
|
@ -31,10 +31,10 @@ Remote.runLocal r =
|
||||
use Future Future
|
||||
step nid r = case r of
|
||||
{a} -> a
|
||||
{Remote.fork t -> k} -> handle (step nid) in k (Future t)
|
||||
{Remote.spawn -> k} -> handle (step (Node.increment nid)) in k nid
|
||||
{Remote.at _ t -> k} -> handle (step nid) in k !t
|
||||
handle (step (Node.Node 0)) in !r
|
||||
{Remote.fork t -> k} -> handle k (Future t) with step nid
|
||||
{Remote.spawn -> k} -> handle k nid with step (Node.increment nid)
|
||||
{Remote.at _ t -> k} -> handle k !t with step nid
|
||||
handle !r with step (Node.Node 0)
|
||||
|
||||
Remote.forkAt : Node -> '{Remote} a ->{Remote} (Future a)
|
||||
Remote.forkAt node r = Remote.fork '(Remote.at node r)
|
||||
|
@ -5,8 +5,8 @@ ability State se2 where
|
||||
|
||||
-- state : ∀ s a . s -> Request (State s) a -> (s, a)
|
||||
state woot eff = case eff of
|
||||
{ State.put snew -> k } -> handle (state snew) in k ()
|
||||
{ State.get () -> k } -> handle state woot in k woot
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ State.get () -> k } -> handle k woot with state woot
|
||||
{ a } -> (woot, a)
|
||||
|
||||
blah : ∀ s a . s -> Request (State s) a -> (s, a)
|
||||
|
@ -4,8 +4,8 @@ ability State se2 where
|
||||
get : ∀ se . () -> {State se} se
|
||||
state : ∀ s a . s -> Request (State s) a -> (s, a)
|
||||
state woot eff = case eff of
|
||||
{ State.get () -> k } -> handle (state woot) in (k woot)
|
||||
{ State.put snew -> k } -> handle (state snew) in (k ())
|
||||
{ State.get () -> k } -> handle k woot with state woot
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> (woot, a)
|
||||
|
||||
> ()
|
||||
|
@ -4,13 +4,14 @@ ability State s where
|
||||
|
||||
state : s -> Request (State s) a -> a
|
||||
state s eff = case eff of
|
||||
{ State.put snew -> k } -> handle (state snew) in k ()
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> a
|
||||
|
||||
ex : Text
|
||||
ex = handle (state 10) in
|
||||
ex = handle
|
||||
State.put (11 + 1)
|
||||
State.put (5 + 5)
|
||||
"hello"
|
||||
with state 10
|
||||
|
||||
> ex
|
||||
|
@ -8,8 +8,8 @@ ability State s where
|
||||
|
||||
state : s -> Request (State s) a -> (s, a)
|
||||
state s eff = case eff of
|
||||
{ State.get -> k } -> handle (state s) in k s
|
||||
{ State.put snew -> k } -> handle (state snew) in k ()
|
||||
{ State.get -> k } -> handle k s with state s
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> (s, a)
|
||||
|
||||
modify : (s ->{} s) ->{State s} ()
|
||||
@ -30,11 +30,12 @@ first p = case p of (a,_) -> a
|
||||
ex : Text
|
||||
ex =
|
||||
result : (Nat, Text)
|
||||
result = handle (state 10) in
|
||||
State.put (11 + 1)
|
||||
x = State.get
|
||||
State.put (5 + 5)
|
||||
"hello"
|
||||
result = handle
|
||||
State.put (11 + 1)
|
||||
x = State.get
|
||||
State.put (5 + 5)
|
||||
"hello"
|
||||
with state 10
|
||||
|
||||
second result
|
||||
|
||||
@ -47,5 +48,3 @@ modify2 f =
|
||||
State.put s2
|
||||
|
||||
---
|
||||
|
||||
|
||||
|
@ -4,11 +4,12 @@ ability State s where
|
||||
|
||||
state : s -> Request (State s) a -> s
|
||||
state s eff = case eff of
|
||||
{ State.put snew -> k } -> handle (state snew) in k ()
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> s
|
||||
|
||||
> handle (state 10) in
|
||||
> handle
|
||||
State.put (11 + 1)
|
||||
State.put (5 + 15)
|
||||
()
|
||||
with state 10
|
||||
-- should be 20
|
||||
|
@ -8,8 +8,8 @@ ability State s where
|
||||
|
||||
state : s -> Request (State s) a -> (s, a)
|
||||
state s eff = case eff of
|
||||
{ State.get -> k } -> handle (state s) in k s
|
||||
{ State.put snew -> k } -> handle (state snew) in k ()
|
||||
{ State.get -> k } -> handle k s with state s
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> (s, a)
|
||||
|
||||
modify : (s ->{} s) -> {State s} ()
|
||||
@ -26,14 +26,14 @@ first p = case p of (a,_) -> a
|
||||
|
||||
ex : Nat
|
||||
ex =
|
||||
result = handle (state 10) in
|
||||
result = handle
|
||||
State.put (11 + 1)
|
||||
State.put (5 + 15)
|
||||
()
|
||||
with state 10
|
||||
|
||||
first result
|
||||
|
||||
-- should return `20`, but actually returns `12`
|
||||
-- seems like only one `put` is actually being run
|
||||
> ex
|
||||
|
||||
|
@ -5,24 +5,24 @@ ability State se2 where
|
||||
|
||||
state : ∀ s a . s -> Request (State s) a -> (s, a)
|
||||
state woot eff = case eff of
|
||||
{ State.get () -> k } -> handle (state woot) in (k woot)
|
||||
{ State.put snew -> k } -> handle (state snew) in (k ())
|
||||
{ State.get () -> k } -> handle k woot with state woot
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> (woot, a)
|
||||
|
||||
ex1 : (Nat, Nat)
|
||||
ex1 = handle (state 42) in State.get ()
|
||||
ex1 = handle State.get () with state 42
|
||||
|
||||
ex1a : (Nat, Nat)
|
||||
ex1a = handle (state 42) in 49
|
||||
ex1a = handle 49 with state 42
|
||||
|
||||
ex1b = handle (x -> 10) in 0
|
||||
ex1b = handle 0 with x -> 10
|
||||
|
||||
ex1c : Nat
|
||||
ex1c = handle (x -> 10) in 0
|
||||
ex1c = handle 0 with x -> 10
|
||||
|
||||
ex1d = handle (state 42) in 49
|
||||
ex1d = handle 49 with state 42
|
||||
|
||||
ex2 = handle (state 42) in State.get ()
|
||||
ex2 = handle State.get () with state 42
|
||||
|
||||
ex3 : (Nat, Nat)
|
||||
ex3 = ex2
|
||||
|
@ -4,8 +4,8 @@ ability State s where
|
||||
|
||||
state : s -> Request (State s) a -> s
|
||||
state s eff = case eff of
|
||||
{ State.get -> k } -> handle (state s) in k s
|
||||
{ State.put snew -> k } -> handle (state snew) in k ()
|
||||
{ State.get -> k } -> handle k s with state s
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> s
|
||||
|
||||
modify : (s ->{} s) -> {State s} ()
|
||||
@ -15,11 +15,12 @@ increment : '{State Nat} ()
|
||||
increment = '(modify ((+) 1))
|
||||
|
||||
ex : Nat
|
||||
ex = handle (state 10) in
|
||||
ex = handle
|
||||
State.put (11 + 1)
|
||||
!increment
|
||||
!increment
|
||||
!increment
|
||||
State.get -- should be 15, amirite??
|
||||
with state 10
|
||||
|
||||
> ex
|
||||
|
@ -4,8 +4,8 @@ ability State s where
|
||||
|
||||
state : s -> Request (State s) a -> s
|
||||
state s eff = case eff of
|
||||
{ State.get -> k } -> handle (state s) in k s
|
||||
{ State.put snew -> k } -> handle (state snew) in k ()
|
||||
{ State.get -> k } -> handle k s with state s
|
||||
{ State.put snew -> k } -> handle k () with state snew
|
||||
{ a } -> s
|
||||
|
||||
modify : (s ->{} s) -> {State s} ()
|
||||
@ -15,11 +15,12 @@ increment : '{State Nat} ()
|
||||
increment = '(modify ((+) 1))
|
||||
|
||||
ex : Nat
|
||||
ex = handle (state 10) in
|
||||
ex = handle
|
||||
State.put (11 + 1)
|
||||
-- !increment
|
||||
-- !increment
|
||||
-- !increment
|
||||
State.get -- should be 15, amirite??
|
||||
with state 10
|
||||
|
||||
> ex
|
||||
|
@ -35,9 +35,9 @@ namespace Stream where
|
||||
if n Nat.== 0 then ()
|
||||
else
|
||||
Emit.emit a
|
||||
handle step (n `drop` 1) in k ()
|
||||
handle k () with step (n `drop` 1)
|
||||
{r} -> ()
|
||||
Stream ' handle step n in run s
|
||||
Stream ' handle run s with step n
|
||||
|
||||
-- map : (a -> b) -> Stream {e} a r -> Stream {e} b r
|
||||
map f s =
|
||||
@ -45,15 +45,15 @@ namespace Stream where
|
||||
{r} -> r
|
||||
{Emit.emit a -> k} ->
|
||||
Emit.emit (f a)
|
||||
handle step in k ()
|
||||
Stream ' handle step in run s
|
||||
handle k () with step
|
||||
Stream ' handle run s with step
|
||||
|
||||
-- toSeq : Stream {e} a r ->{e} [a]
|
||||
toSeq s =
|
||||
step acc e = case e of
|
||||
{Emit.emit a -> k} -> handle step (acc `snoc` a) in k ()
|
||||
{Emit.emit a -> k} -> handle k () with step (acc `snoc` a)
|
||||
{_} -> acc
|
||||
handle step [] in run s
|
||||
handle run s with step []
|
||||
|
||||
fromSeq : [a] -> Stream e a ()
|
||||
fromSeq a =
|
||||
|
Loading…
Reference in New Issue
Block a user