
  0 | module System.Posix.File.FileDesc
  1 | 
  2 | import Data.C.Ptr
  3 | import Derive.Prelude
  4 | 
  5 | %default total
  6 | %language ElabReflection
  7 | 
  8 | ||| A wrapper around a file descriptor.
  9 | public export
 10 | record Fd where
 11 |   constructor MkFd
 12 |   fd : Bits32
 13 | 
 14 | %name Fd fd
 15 | 
 16 | %runElab derive "Fd" [Show,Eq,Ord]
 17 | 
 18 | public export
 19 | 0 FileDesc : Type -> Type
 20 | FileDesc a = Cast a Fd
 21 | 
 22 | export %inline
 23 | Cast Bits32 Fd where cast = MkFd
 24 | 
 25 | export %inline
 26 | fileDesc : FileDesc a => a -> Bits32
 27 | fileDesc = fd . cast
 28 | 
 29 | public export %inline
 30 | SizeOf Fd where
 31 |   sizeof_ = sizeof Bits32
 32 | 
 33 | export %inline
 34 | Deref Fd where
 35 |   deref p = MkFd <$> deref p
 36 | 
 37 | export %inline
 38 | SetPtr Fd where
 39 |   setPtr p = setPtr p . fd
 40 | 
 41 | ||| Standard input and output file descriptors
 42 | public export
 43 | data StdIO : Type where
 44 |   Stdin  : StdIO
 45 |   Stdout : StdIO
 46 |   Stderr : StdIO
 47 | 
 48 | %runElab derive "StdIO" [Show,Eq,Ord]
 49 | 
 50 | export %inline
 51 | Cast StdIO Fd where
 52 |   cast = MkFd . cast . conIndexStdIO
 53 |