git.iko.soy/Idris-dev
on master help sign in
Remove prim_io_bind and prim_io_return from run__IO.
commit65d10f28601bf082d3a353938680f126bf2dc337 authorMatus Tejiscak <ziman@functor.sk> dateThu 20 Feb 2014, 13:59 (13 years ago) parentb5f219e
2 files changed+5−8
compare with master
unifiedsplit
libs/prelude/IO.idr+3−6 src/Idris/Erasure.hs+2−2
libs/prelude/IO.idr+3−6
@@ -132,16 +132,13 @@ io_return : a -> IO a
132132io_return x = MkIO (\w => prim_io_return x)
133133
134134liftPrimIO : (World -> PrimIO a) -> IO a
135−liftPrimIO f = MkIO (\w => prim_io_bind (f w)
136− (\x => prim_io_return x))
135+liftPrimIO = MkIO
137136
138137run__IO : IO () -> PrimIO ()
139−run__IO (MkIO f) = prim_io_bind (f TheWorld)
140− (\ b => prim_io_return b)
138+run__IO (MkIO f) = f TheWorld
141139
142140run__provider : IO a -> PrimIO a
143−run__provider (MkIO f) = prim_io_bind (f TheWorld)
144− (\ b => prim_io_return b)
141+run__provider (MkIO f) = f TheWorld
145142
146143-- io_bind v (\v' => io_return v')
147144
src/Idris/Erasure.hs+2−2
@@ -174,7 +174,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
174174 [ [(sUN "main" `sNS` ["Main"], Result)]
175175 , [(sUN "run__IO", Result), (sUN "run__IO", Arg 0)]
176176
177− -- MkIO is presumably read by run__IO
177+ -- MkIO is presumably read by run__IO,
178178 -- but this cannot be observed in the source code of programs.
179179 , it "MkIO" [1]
180180 , it "prim__IO" [1]
@@ -184,7 +184,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
184184 , mn "__MkPair" [0,1]
185185 , it "prim_fork" [0]
186186
187− -- believe_me only uses its third argument
187+ -- believe_me is a primitive but it only uses its third argument
188188 -- it is special-cased in usedNames above
189189 , it "prim__believe_me" [2]
190190