on master help sign in
Remove prim_io_bind and prim_io_return from run__IO.
65d10f2Matus Tejiscak
libs/prelude/IO.idr+3−6
@@ -132,16 +132,13 @@ io_return : a -> IO a
132io_return x = MkIO (\w => prim_io_return x)
132io_return x = MkIO (\w => prim_io_return x)
133
133
134liftPrimIO : (World -> PrimIO a) -> IO a
134liftPrimIO : (World -> PrimIO a) -> IO a
135−liftPrimIO f = MkIO (\w => prim_io_bind (f w)
135+liftPrimIO = MkIO
136− (\x => prim_io_return x))
137
136
138run__IO : IO () -> PrimIO ()
137run__IO : IO () -> PrimIO ()
139−run__IO (MkIO f) = prim_io_bind (f TheWorld)
138+run__IO (MkIO f) = f TheWorld
140− (\ b => prim_io_return b)
141
139
142run__provider : IO a -> PrimIO a
140run__provider : IO a -> PrimIO a
143−run__provider (MkIO f) = prim_io_bind (f TheWorld)
141+run__provider (MkIO f) = f TheWorld
144− (\ b => prim_io_return b)
145
142
146-- io_bind v (\v' => io_return v')
143-- io_bind v (\v' => io_return v')
147
144
src/Idris/Erasure.hs+2−2
@@ -174,7 +174,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
174 [ [(sUN "main" `sNS` ["Main"], Result)]
174 [ [(sUN "main" `sNS` ["Main"], Result)]
175 , [(sUN "run__IO", Result), (sUN "run__IO", Arg 0)]
175 , [(sUN "run__IO", Result), (sUN "run__IO", Arg 0)]
176
176
177− -- MkIO is presumably read by run__IO
177+ -- MkIO is presumably read by run__IO,
178 -- but this cannot be observed in the source code of programs.
178 -- but this cannot be observed in the source code of programs.
179 , it "MkIO" [1]
179 , it "MkIO" [1]
180 , it "prim__IO" [1]
180 , it "prim__IO" [1]
@@ -184,7 +184,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
184 , mn "__MkPair" [0,1]
184 , mn "__MkPair" [0,1]
185 , it "prim_fork" [0]
185 , it "prim_fork" [0]
186
186
187− -- believe_me only uses its third argument
187+ -- believe_me is a primitive but it only uses its third argument
188 -- it is special-cased in usedNames above
188 -- it is special-cased in usedNames above
189 , it "prim__believe_me" [2]
189 , it "prim__believe_me" [2]
190
190