0 | module FS.Core

  2 | import public Data.Linear.ELift1

  3 | import public FS.Scope

  5 | import Control.Monad.Elin

  7 | import Data.Linear.Deferred

  8 | import Data.Linear.Ref1

  9 | import Data.Maybe

 10 | import Data.SortedMap

 11 | import Debug.Trace

 12 | import IO.Async

 14 | %default total

 18 | data Action :

 19 |      (f  : List Type -> Type -> Type)

 20 |   -> (es : List Type)

 21 |   -> (r  : Type)

 22 |   -> Type where

 23 |   Eval    : (act : f es r) -> Action f es r

 24 |   Acquire : f es r -> (r -> f [] ()) -> Action f es r

 25 |   Close   : Scope f -> Result es r -> Action f es r

 82 | data Pull :

 83 |        (f : List Type -> Type -> Type) -- effect type

 84 |     -> (o : Type)                      -- output type

 85 |     -> (es : List Type)                -- possible errors

 86 |     -> (r : Type)                      -- result type

 87 |     -> Type where

 89 |   ||| Constructor for producing value of type `r`

 90 |   Val    : (res : r) -> Pull f o es r

 92 |   ||| Constructor for failing with an exception

 93 |   Err    : HSum es -> Pull f o es r

 95 |   ||| Constructor for producing a chunk of output values

 96 |   Cons   : (val : o) -> Inf (Pull f o es r) -> Pull f o es r

 98 |   ||| Wraps an arbitrary effectful computation in a `Pull`

 99 |   Act    : (act : Action f es r) -> Pull f o es r

101 |   ||| Unwraps the given child `Pull` until it either produces

103 |   Uncons : Pull f o es r -> Pull f q es (Either r (o, Pull f o es r))

105 |   ||| Attempts to evaluate the underlying `Pull`, returning any error

108 |   Att    : Pull f o es r -> Pull f o fs (Result es r)

110 |   ||| Sequencing of `Pull`s via monadic bind `(>>=)`.

111 |   Bind   : Pull f o es r -> (r -> Pull f o es t) -> Pull f o es t

113 |   ||| Runs the given `Pull` in a new child scope. The optional second argument

115 |   OScope : Interrupt f -> Pull f o es r -> Pull f o es r

117 |   ||| Internal: A pull for returning the current scope

118 |   GScope : Pull f o es (Scope f)

120 |   ||| Internal: Forces the given pull to be evaluated in the given scope.

126 |   IScope : Scope f -> (close : Bool) -> Pull f o es r -> Pull f o es r

128 |   ||| Continues with the second pull in case the first is interrupted.

129 |   OnIntr : Pull f o es r -> Lazy (Pull f o es r) -> Pull f o es r

132 | public export

133 | 0 Stream : (List Type -> Type -> Type) -> List Type -> Type -> Type

134 | Stream f es o = Pull f o es ()

137 | public export

138 | 0 EmptyPull : (List Type -> Type -> Type) -> List Type -> Type -> Type

139 | EmptyPull f = Pull f Void

142 | public export

143 | 0 EmptyStream : (List Type -> Type -> Type) -> List Type -> Type

144 | EmptyStream f es = Stream f es Void

148 | public export

149 | record StepLeg f es o where

150 |   constructor SL

151 |   out   : o

152 |   pull  : Pull f o es ()

153 |   scope : Scope f

160 | export %inline

161 | exec : f es r -> Pull f o es r

162 | exec = Act . Eval

166 | export %inline

167 | acquire : (acq : f es r) -> (release : r -> f [] ()) -> Pull f o es r

168 | acquire acq rel = Act $ Acquire acq rel

171 | export %inline %tcinline

172 | cons : o -> Inf (Pull f o es r) -> Pull f o es r

173 | cons = Cons

176 | export %inline

177 | emit : o -> Stream f es o

178 | emit v = cons v (Val ())

182 | export %inline

183 | uncons : Pull f o es r -> Pull f q es (Either r (o, Pull f o es r))

184 | uncons = Uncons

190 | export %inline

191 | scope : Pull f o es (Scope f)

192 | scope = GScope

195 | export %inline

196 | newScope : Pull f o es r -> Pull f o es r

197 | newScope = OScope None

203 | export %inline

204 | inScope : Scope f -> Pull f o es r -> Pull f o es r

205 | inScope p = IScope p False

209 | export %inline

210 | att : Pull f o es r -> Pull f o fs (Result es r)

211 | att = Att

213 | peek : Deferred World (Result es ()) -> Stream (Async e) es o

214 | peek x =

215 |   Bind (Act $ Eval $ lift1 $ peekDeferred1 x) $ \case

216 |     Nothing => Val ()

217 |     Just (Left err) => Err err

218 |     Just (Right _)  => Val ()

223 | interruptOn :

224 |      Deferred World (Result es ())

225 |   -> Stream (Async e) es o

226 |   -> Stream (Async e) es o

227 | interruptOn def p = OnIntr (OScope (I def) p) (peek def)

232 | interruptOnAny :

233 |      Deferred World a

234 |   -> Stream (Async e) es o

235 |   -> Stream (Async e) es o

236 | interruptOnAny def p = OnIntr (OScope (I def) p) (Val ())

245 | export %inline

246 | MErr (Pull f o) where

247 |   fail        = Err

248 |   succeed     = Val

249 |   bind        = Bind

250 |   attempt     = Att

251 |   mapImpl f p = Bind p (Val . f)

252 |   appImpl f p = Bind f (`mapImpl` p)

256 | export %inline

257 | ELift1 s f => ELift1 s (Pull f o) where

258 |   elift1 = exec . elift1

260 | export %inline

261 | Semigroup (Stream f es o) where

262 |   x <+> y = x >> y

264 | export %inline

265 | Monoid (Stream f es o) where

266 |   neutral = pure ()

268 | export %inline

269 | HasIO (f es) => HasIO (Pull f o es) where

270 |   liftIO = exec . liftIO

279 | data Item :

280 |      (f     : List Type -> Type -> Type)

281 |   -> (o,p   : Type)

282 |   -> (es,fs : List Type)

283 |   -> (x,y   : Type)

284 |   -> Type where

285 |   -- the continuation of a monadic bind on the stack

286 |   B : (x -> Pull f o es y) -> Item f o o es es x y

288 |   -- `Att` (error handling) on the stack

289 |   A : Item f o o es fs r (Result es r)

291 |   -- Handling of output (`Uncons`)

292 |   U : Item f o p es es r (Either r (o, Pull f o es r))

294 |   -- Changing the current evaluation scope (resource management)

295 |   -- `cl` signifies whether the current scope should be closed and

296 |   -- its resources cleaned up.

297 |   S : Scope f -> (cl : Bool) -> Item f o o es es x x

299 |   -- Resumption to use if the current pull has been interrupted.

300 |   I : Lazy (Pull f o es r) -> Item f o o es es r r

303 | data Stack :

304 |      (f     : List Type -> Type -> Type)

305 |   -> (o     : Type)

306 |   -> (es,fs : List Type)

307 |   -> (x,y   : Type)

308 |   -> Type where

309 |   Nil  : Stack f Void es es x x

310 |   (::) : Item f o p es fs x y -> Stack f p fs gs y z -> Stack f o es gs x z

314 | data View :

315 |      (f  : List Type -> Type -> Type)

316 |   -> (es : List Type)

317 |   -> (r  : Type)

318 |   -> Type where

319 |   VV : Scope f -> Outcome es r -> View f es r

320 |   VA : Scope f -> Action f es x -> Stack f o es fs x y -> View f fs y

328 | record URes (f : List Type -> Type -> Type) (fs : List Type) (y : Type) where

329 |   constructor UR

330 |   {0 out, res  : Type}

331 |   {0 errs : List Type}

332 |   scope : Scope f

333 |   cur   : Pull f out errs res

334 |   stck  : Stack f out errs fs res y

339 | traceOutput :

340 |      Scope f

341 |   -> o

342 |   -> Pull f o es x

343 |   -> Stack f o es fs x y

344 |   -> URes f fs y

345 | traceOutput sc v p []        = UR sc p []

346 | traceOutput sc v p (i :: is) =

347 |   case i of

348 |     B g       => traceOutput sc v (Bind p g) is

349 |     A         => traceOutput sc v (Att p) is

350 |     U         => UR sc (Val $ Right (v, p)) is

351 |     S prev cl => traceOutput prev v (IScope sc cl p) is

352 |     I q       => traceOutput sc v (OnIntr p q) is

354 | parameters {0 f      : List Type -> Type -> Type}

355 |            {auto tgt : Target s f}

356 |            (ref      : Ref s (ScopeST f))

358 |   -- Tail-recursively unfolds a `Pull` placing all continuations on

359 |   -- the call stack until we either arrive at a final result or at

360 |   -- an effectful computation (`Action`).

361 |   covering

362 |   view :

363 |        Scope f

364 |     -> Pull f o es x

365 |     -> Stack f o es fs x y

366 |     -> F1 s (View f fs y)

367 |   view sc p st t =

368 |     case p of

369 |       Bind q g => case q of

370 |         -- This is here for reasons of efficiency: If a `Bind` wraps

371 |         -- a pure value, the value can be passed to the continuation

372 |         -- directly. Otherwise, the continuation is put on the stack.

373 |         Val v => view sc (g v) st t

374 |         _     => view sc q (B g::st) t

376 |       -- We arrived at a terminal (a result), and it's time to

377 |       -- pass it to the head of the stack (if any).

378 |       Val v => case st of

379 |         h::tl => case h of

380 |           -- monadic bind: we pass result `v` to continuation `fun`

381 |           -- and continue from there

382 |           B fun  => view sc (fun v) tl t

384 |           -- `Uncons`: We arrived at the pull's end, so we pass

385 |           -- the result wrapped in a `Left` (see the type of `Uncons`)

386 |           U      => view sc (Val $ Left v) tl t

388 |           -- error handling: there was no error so we wrap the result

389 |           -- in a `Right`.

390 |           A      => view sc (Val $ Right v) tl t

392 |           -- Scope handling. In case the current scope needs to be

393 |           -- closed, we arrived at an effectful computation and return

394 |           -- it as our result. Otherwise, we just continue with the

395 |           -- new scope.

396 |           S s2 b => case b of

397 |             True  => VA s2 (Close sc $ Right v) tl # t

398 |             False => view s2 p tl t

400 |           -- Interrupt handling. We were not interrupted, so we just

401 |           -- continue.

402 |           I _    => view sc p tl t

403 |         []    => VV sc (Succeeded v) # t

405 |       -- An error occured. Let's try and handle it.

406 |       Err v => case st of

407 |         h::tl => case h of

408 |           -- We can't continue with the bind, so we drop it and look

409 |           -- if there is an error handler further down the stack.

410 |           B _    => view sc (Err v) tl t

412 |           -- We can't continue with the `Uncons`, so we drop it and look

413 |           -- if there is an error handler further down the stack.

414 |           U      => view sc (Err v) tl t

416 |           -- We found an error handler, so we wrap the error in a `Left`

417 |           -- and continue regularily.

418 |           A      => view sc (Val $ Left v) tl t

420 |           -- Scope handling. In case the current scope needs to be

421 |           -- closed, we arrived at an effectful computation and return

422 |           -- it as our result. Otherwise, we just continue with the

423 |           -- new scope.

424 |           S s2 b => case b of

425 |             True  => VA s2 (Close sc $ Left v) tl # t

426 |             False => view s2 (Err v) tl t

428 |           -- Interrupt handling. We were not interrupted, so we just

429 |           -- continue.

430 |           I _    => view sc p tl t

431 |         []    => VV sc (Error v) # t

433 |       -- Some output was produced. The only way this can be handled

434 |       -- is by an `Uncons` wrapper, which by now should be on the

435 |       -- stack. We try to find and continue from there. This will

436 |       -- reassemble parts of the wrapping pull, so we might go

437 |       -- back and forth on the stack for some time (until all

438 |       -- output has been consumed, or consumption is aborted)

439 |       Cons v q =>

440 |        let UR sc2 p2 st2 := traceOutput sc v q st

441 |         in view sc2 (IScope sc False p2) st2 t

443 |       -- An effectful computation. We have to stop here and pass control

444 |       -- to `loop`

445 |       Act x => VA sc x st # t

447 |       -- We are looking for some output, so we put an uncons handler

448 |       -- `U` on the stack.

449 |       Uncons q => view sc q (U :: st) t

451 |       -- Error handling. We put the corresponding item onto the stack

452 |       -- and continue.

453 |       Att q    => view sc q (A::st) t

455 |       -- Pull `q` should be run in a new scope. We open a new scope

456 |       -- and put a note on the stack that the scope should be closed

457 |       -- when `q` is done.

458 |       OScope i q =>

459 |         let s2 # t := openScope ref i sc t

460 |          in view s2 q (S sc True :: st) t

462 |       -- Pull `q` should be run in the given scope. We put a note

463 |       -- on the stack that the current scope `sc` should be used

464 |       -- and `s2` closed (if `b` is `True`) once `q` is done.

465 |       IScope s2 b q => view s2 q (S sc b :: st) t

467 |       -- We have been asked for the current scope so we wrap it

468 |       -- in a `Val` and continue.

469 |       GScope   => view sc (Val sc) st t

471 |       -- An interrupt handler should be put on the stack: `q1`

472 |       -- will be evaluated and `q2` should be used in its stead in

473 |       -- case it has been interrupted.

474 |       OnIntr q1 q2 => view sc q1 (I q2 :: st) t

476 |   -- This is invoked if evaluation of the pull has been interrupted

477 |   -- by an external event. We look on the stack for an interrupt handler

478 |   -- (item `I`) or - if none is found - terminate with `Canceled`.

479 |   covering

480 |   interrupted : Scope f -> Stack f o es fs x y -> f [] (Outcome fs y)

482 |   -- main run loop: Keeps invoking `view`, executing the actions

483 |   -- it gets back until a result is found or evaluation of the

484 |   -- pull interrupted by an external event.

485 |   covering

486 |   loop : Scope f -> Pull f o es x -> Stack f o es fs x y -> f [] (Outcome fs y)

487 |   loop sc p st = Prelude.do

488 |     -- We check if the current scope has been interrupted

489 |     -- If that'e the case, we search for an interrupt handler by

490 |     -- passing control to `interrupted`

491 |     False <- isInterrupted sc.interrupt | True => interrupted sc st

493 |     -- We unfold the current pull until we either arrive at a final

494 |     -- result or get an effectful computation we must run in order

495 |     -- to continue

496 |     v     <- lift1 (view sc p st)

497 |     case v of

498 |       VA sc2 act st2 => case act of

499 |         -- Effect `act` should be run in monad `f`. This might

500 |         -- be something long-running (waiting on a timer, listening

501 |         -- on a socket) so it should be possible to interrupt this.

502 |         -- TODO: Some (short-running) effects do not require the

503 |         --       overhead from making them interruptible. We should

504 |         --       consider adding a boolean flag to the `Eval` constructor.

505 |         --       The reason this is not already there: It will complicate

506 |         --       the API that's based on evaluating effects.

507 |         Eval act => raceInterrupt sc.interrupt act >>= \case

508 |           Succeeded v => loop sc2 (Val v) st2

509 |           Error     v => loop sc2 (Err v) st2

510 |           Canceled    => interrupted sc2 st2

512 |         -- We should acquire a resource that should be later released

513 |         -- See the notes above about interrupting effects.

514 |         -- TODO: This currently does not take cancellation (of `Async`)

515 |         --       into account and should be fixed.

516 |         Acquire act release => raceInterrupt sc.interrupt act >>= \case

517 |           Succeeded v => addHook sc2 (release v) >> loop sc2 (Val v) st2

518 |           Error x     => loop sc2 (Err x) st2

519 |           Canceled    => interrupted sc2 st2

521 |         -- Scope `old` has come to an end and should be closed, thus

522 |         -- releasing all resources that have been aqcuired within.

523 |         Close old res => Prelude.do

524 |           close ref True old.id

525 |           case res of

526 |             Right v => loop sc2 (Val v) st2

527 |             Left  v => loop sc2 (Err v) st2

529 |       -- We are done! Yay!

530 |       VV sc v => pure v

532 |   -- Implementation of `interrupted`

533 |   interrupted sc []      = pure Canceled

534 |   interrupted sc (h::tl) =

535 |     case h of

536 |       -- Of course we keep closing scopes and releasing resources!

537 |       S sc2 True  => close ref True sc.id >> interrupted sc2 tl

539 |       -- Nothing to do except switching to a different scope.

540 |       S sc2 False => interrupted sc2 tl

542 |       -- We arrived at an interrupt handler and can continue with

543 |       -- the replacement pull `q`.

544 |       I q         => loop sc q tl

546 |       -- In all other cases, there is nothing to do. Note: We don't

547 |       -- use a catch-all pattern here to make sure we don't miss any

548 |       -- data constructors that might be introduced at a later point.

549 |       B _         => interrupted sc tl

550 |       U           => interrupted sc tl

551 |       A           => interrupted sc tl

553 | parameters {auto mcn : MCancel f}

554 |            {auto tgt : Target s f}

556 |   ||| Runs a `Pull` to completion, eventually producing

563 |   export covering

564 |   pull : Pull f Void es r -> f [] (Outcome es r)

565 |   pull p =

566 |     bracket newScope

567 |       (\(S i rt as ir ref) => loop ref (S i rt as ir ref) p [])

568 |       (\(S i rt as ir ref) => close ref False i)

570 |   ||| Like `pull` but without the possibility of failure. Returns `neutral`

572 |   export covering

573 |   mpull : Monoid r => Pull f Void [] r -> f [] r

574 |   mpull p =

575 |     pull p >>= \case

576 |       Succeeded res => pure res

577 |       Canceled      => pure neutral

578 |       Error x impossible

583 | export covering

584 | pullIn : Scope f -> Pull f Void es r -> f [] (Outcome es r)

585 | pullIn (S i rt as ir ref) p = loop ref (S i rt as ir ref) p []