
  0 | module UUID
  1 | 
  2 | import Data.Bits
  3 | import Data.Vect
  4 | 
  5 | ||| A UUID.
  6 | |||
  7 | ||| Implemented as a wrapper around a foreign object.
  8 | public export
  9 | record UUID where
 10 |   constructor MkUUID
 11 |   ptr : GCAnyPtr
 12 | 
 13 | repr : Vect 16 Bits8 -> String
 14 | repr xs =
 15 |   case map (\x => aux (x `shiftR` 4) ++ aux (0x0f .&. x)) xs of
 16 |         [x00, x01, x02, x03, x04, x05, x06, x07, x08, x09, x10, x11, x12, x13, x14, x15] =>
 17 |           "\{x00}\{x01}\{x02}\{x03}-\{x04}\{x05}-\{x06}\{x07}" ++
 18 |             "-\{x08}\{x09}-\{x10}\{x11}\{x12}\{x13}\{x14}\{x15}"
 19 | 
 20 |   where
 21 |   aux : Bits8 -> String
 22 |   aux = \case
 23 |     0x0a => "a"
 24 |     0x0b => "b"
 25 |     0x0c => "c"
 26 |     0x0d => "d"
 27 |     0x0e => "e"
 28 |     0x0f => "f"
 29 |     x    => show x
 30 | 
 31 | public export
 32 | interface Ord UUID => UUIDGen where
 33 |   ||| A UUID from a byte vector, if the byte vector forms a valid UUID.
 34 |   export
 35 |   fromBytes : Vect 16 Bits8 -> Maybe UUID
 36 |   fromBytes = parse . repr
 37 | 
 38 |   ||| A UUID as a byte vector.
 39 |   export
 40 |   toBytes : UUID -> Vect 16 Bits8
 41 | 
 42 |   ||| UUID version 1.
 43 |   |||
 44 |   ||| Uses the current time and the local ethernet MAC address.
 45 |   |||
 46 |   ||| If the `Bool` is `False`, it is guaranteed that two concurrently running processes did not
 47 |   ||| obtain the same UUID. `True` does not necessarily guarantee the converse.
 48 |   export
 49 |   uuid1 : IO (UUID, Bool)
 50 | 
 51 |   ||| UUID version 3.
 52 |   |||
 53 |   ||| Deterministic UUID created by MD5 hashing `namespace'` and `name`.
 54 |   export
 55 |   uuid3 : (namespace' : Vect 16 Bits8) -> (name : String) -> UUID
 56 | 
 57 |   ||| UUID version 4.
 58 |   |||
 59 |   ||| Generates a UUID using high-quality randomness.
 60 |   |||
 61 |   ||| **Note**: For C, If none of libc `getRandom`, /dev/urandom or /dev/random are available,
 62 |   ||| a pseudo-random generator will be substituted, which may compromise UUID uniqueness.
 63 |   export
 64 |   uuid4 : IO UUID
 65 | 
 66 |   ||| UUID version 5.
 67 |   |||
 68 |   ||| Deterministic UUID created by SHA1 hashing `namespace'` and `name`.
 69 |   export
 70 |   uuid5 : (namespace' : Vect 16 Bits8) -> (name : String) -> UUID
 71 | 
 72 |   ||| Try to parse a UUID string (e.g. "1b4e28ba-2fa1-11d2-883f-b9a761bde3fb") as a UUID.
 73 |   export
 74 |   parse : String -> Maybe UUID
 75 | 
 76 |   ||| Convert a UUID to string format.
 77 |   export
 78 |   unparse : UUID -> String
 79 |