
  0 | -- Note: This module is automatically generated when Idris builds
  1 | -- the library and the constants will be replaced with values
  2 | -- matching the system this is generated on.
  3 | --
  4 | -- The placeholders are here so that it works with tools like the LSP
  5 | -- without first compiling the library. They were generated on an x86_64
  6 | -- GNU/Linux system with GCC. If you are on a similar system, your numbers
  7 | -- might very well be identical.
  8 | module System.Posix.Pthreads.Types
  9 | 
 10 | import Data.C.Integer
 11 | import Derive.Finite
 12 | import Derive.Prelude
 13 | 
 14 | %default total
 15 | %language ElabReflection
 16 | 
 17 | public export
 18 | data MutexType : Type where
 19 |   MUTEX_NORMAL     : MutexType
 20 |   MUTEX_RECURSIVE  : MutexType
 21 |   MUTEX_ERRORCHECK : MutexType
 22 | 
 23 | %runElab derive "MutexType" [Show,Eq,Ord,Finite]
 24 | 
 25 | public export
 26 | data CancelType : Type where
 27 |   CANCEL_DEFERRED     : CancelType
 28 |   CANCEL_ASYNCHRONOUS : CancelType
 29 | 
 30 | %runElab derive "CancelType" [Show,Eq,Ord,Finite]
 31 | 
 32 | public export
 33 | data CancelState : Type where
 34 |   CANCEL_ENABLE  : CancelState
 35 |   CANCEL_DISABLE : CancelState
 36 | 
 37 | %runElab derive "CancelState" [Show,Eq,Ord,Finite]
 38 | 
 39 | 
 40 | public export
 41 | mutexCode : MutexType -> Bits8
 42 | mutexCode MUTEX_NORMAL = 0
 43 | mutexCode MUTEX_RECURSIVE = 1
 44 | mutexCode MUTEX_ERRORCHECK = 2
 45 | 
 46 | public export
 47 | cancelType : CancelType -> Bits8
 48 | cancelType CANCEL_DEFERRED = 0
 49 | cancelType CANCEL_ASYNCHRONOUS = 1
 50 | 
 51 | public export
 52 | cancelState : CancelState -> Bits8
 53 | cancelState CANCEL_ENABLE = 0
 54 | cancelState CANCEL_DISABLE = 1
 55 | 
 56 | public export %inline
 57 | pthread_t_size : Bits32
 58 | pthread_t_size = 8
 59 | 
 60 | public export %inline
 61 | mutex_t_size : Bits32
 62 | mutex_t_size = 40
 63 | 
 64 | public export %inline
 65 | cond_t_size : Bits32
 66 | cond_t_size = 48
 67 |