process.tri (1992B)
1 !import io_v2 as IO 2 !export pipeline 3 !export normalExit 4 !export raw 5 6 -- Child stdout/stderr are drained concurrently while the parent pumps stdin. 7 -- All three streams use bounded chunks; output is written to files, not collected. 8 -- Executable and argv are caller supplied; using a shell requires naming one. 9 copy reader writer = IO.require (IO.copyStream reader writer) IO.pure 10 completed ticket = IO.require (IO.join ticket) (outcome : case outcome of 11 ["completed" value] = IO.pure value 12 _ = IO.fail outcome) 13 waitCopy [_ ticket] = completed ticket 14 waitCopy _ = IO.fail "Invalid copy task reply" 15 pump owner source destination errors spawned = case spawned of 16 [task ticket input output error] = do IO.require 17 reader <- IO.openReader owner source 18 writer <- IO.openWriter owner destination 19 errorWriter <- IO.openWriter owner errors 20 stdoutTask <- IO.spawn 0 1 [] (_ : copy output writer) 21 stderrTask <- IO.spawn 0 1 [] (_ : copy error errorWriter) 22 IO.bind (copy reader input) (_ : do IO.require 23 IO.close input 24 IO.bind (waitCopy stdoutTask) (_ : IO.bind (waitCopy stderrTask) (_ : completed ticket))) 25 _ = IO.fail "Invalid process reply" 26 pipeline [executable arguments directory environment grace source destination errors] = IO.io (IO.scope (owner : 27 IO.require (IO.spawnProcess executable arguments directory environment grace) 28 (pump owner source destination errors))) 29 pipeline _ = IO.io (IO.fail "Invalid pipeline arguments") 30 normalExit [executable arguments] = IO.io (IO.scope (_ : 31 IO.require (IO.spawnProcess executable arguments ["inherit"] ["inherit"] 20) 32 (spawned : case spawned of 33 [_ _ input _ _] = IO.require (IO.close input) (_ : IO.pure 42) 34 _ = IO.fail "Invalid process reply"))) 35 normalExit _ = IO.io (IO.fail "Invalid process arguments") 36 raw [executable arguments directory environment grace] = IO.io 37 (IO.spawnProcess executable arguments directory environment grace) 38 raw _ = IO.io (IO.fail "Invalid raw arguments")