tricu

A lazy functional language based on Tree Calculus
Log | Files | Refs | README | LICENSE

copy.tri (3322B)

      1 !import base as B
      2 !import io as IO
      3 !import handlers as H
      4 !export cancelledCopy
      5 !export copy
      6 !export handledCopy
      7 !export borrowedCopy
      8 !export transferredCopy
      9 !export joinedOnExitCopy
     10 !export handledChildCopy
     11 
     12 pump reader writer = IO.copyStream reader writer
     13 
     14 copy source destination = IO.io <| IO.scope (owner : do IO.onOk
     15   reader <- IO.openReader owner source
     16   writer <- IO.openWriter owner destination
     17   pump reader writer)
     18 
     19 -- A captured service supplies the implementation, while the caller requests
     20 -- policy-level work. The host scope, not handler removal, owns both resources.
     21 service reader writer "run" _ = H.liftIO (pump reader writer)
     22 service _ _ operation argument = H.forward "copy" operation argument
     23 handledCopy source destination = IO.io <| IO.scope (owner : do IO.onOk
     24   reader <- IO.openReader owner source
     25   writer <- IO.openWriter owner destination
     26   H.runIO (H.handle "copy" (service reader writer) (H.request "copy" "run" t)))
     27 
     28 
     29 joinCopy spawned = case spawned of
     30   [task ticket] = IO.require (IO.join ticket) (outcome : case outcome of
     31     ["completed" value] = IO.pure value
     32     ["failed" diagnostic cleanup] = IO.fail [diagnostic cleanup]
     33     ["cancelled" reason cleanup] = IO.fail [reason cleanup]
     34     _ = IO.fail "Invalid task outcome")
     35   _ = IO.fail "Invalid spawn reply"
     36 
     37 borrowedCopy source destination = IO.io <| IO.scope (owner : do IO.require
     38   reader <- IO.openReader owner source
     39   writer <- IO.openWriter owner destination
     40   spawned <- IO.spawn 0 1 [] (_ : pump reader writer)
     41   joinCopy spawned)
     42 
     43 transferredPump [reader writer] = pump reader writer
     44 transferredPump _ = IO.fail "Invalid transferred handles"
     45 transferredCopy source destination = IO.io <| IO.scope (owner : do IO.require
     46   reader <- IO.openReader owner source
     47   writer <- IO.openWriter owner destination
     48   spawned <- IO.spawn 0 1 [reader writer] transferredPump
     49   joinCopy spawned)
     50 
     51 -- No ticket and no explicit join: scope return still waits for complete copying.
     52 joinedOnExitCopy source destination = IO.io <| IO.scope (owner : do IO.require
     53   reader <- IO.openReader owner source
     54   writer <- IO.openWriter owner destination
     55   IO.spawn 0 0 [] (_ : pump reader writer)
     56   IO.pure (B.ok t t))
     57 
     58 handledChildCopy source destination = IO.io <| IO.scope (owner : do IO.require
     59   reader <- IO.openReader owner source
     60   writer <- IO.openWriter owner destination
     61   H.runIO (H.handle "copy" (service reader writer) (do H.bind
     62     reply <- H.spawn 0 1 [] (_ : H.request "copy" "run" t)
     63     H.liftIO (IO.require (IO.pure reply) joinCopy))))
     64 
     65 -- Cancellation after one acknowledged chunk is not rollback. The supervisor
     66 -- observes the outcome only after the transferred handles have been released.
     67 cancelPump [reader writer] = IO.require (IO.readSome reader 4096) (reply : case reply of
     68   ("eof", t) = IO.cancelled "requested"
     69   ("data", bytes) = IO.require (IO.writeAll writer bytes) (_ : IO.cancelled "requested")
     70   _ = IO.fail "Invalid read reply")
     71 cancelPump _ = IO.fail "Invalid transferred handles"
     72 cancelledCopy source destination = IO.io <| IO.scope (owner : do IO.require
     73   reader <- IO.openReader owner source
     74   writer <- IO.openWriter owner destination
     75   spawned <- IO.spawn 1 1 [reader writer] cancelPump
     76   case spawned of
     77     [task ticket] = IO.require (IO.join ticket) IO.pure
     78     _ = IO.fail "Invalid spawn reply")