0 | {-
  1 | UUID: UUIDs for Idris2
  2 |
  3 | Copyright (C) 2026  Joel Berkeley
  4 |
  5 | This program is free software: you can redistribute it and/or modify
  6 | it under the terms of the GNU Affero General Public License as published
  7 | by the Free Software Foundation, either version 3 of the License, or
  8 | (at your option) any later version.
  9 |
 10 | This program is distributed in the hope that it will be useful,
 11 | but WITHOUT ANY WARRANTY; without even the implied warranty of
 12 | MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 13 | GNU Affero General Public License for more details.
 14 |
 15 | You should have received a copy of the GNU Affero General Public License
 16 | along with this program.  If not, see <https://www.gnu.org/licenses/>.
 17 | -}
 18 | ||| Come get your UUIDs.
 19 | module UUID
 20 |
 21 | import Data.Vect
 22 | import System.FFI
 23 |
 24 | import UUID.Support.C
 25 |
 26 | export
 27 | record UUID where
 28 |   constructor MkUUID
 29 |   ptr : GCAnyPtr
 30 |
 31 | compare' : UUID -> UUID -> Ordering
 32 | compare' = flip compare 0 .: prim__uuidCompare `on` ptr
 33 |
 34 | export Eq UUID where x == y = compare' x y == EQ
 35 | export Ord UUID where compare = compare'
 36 |
 37 | allocUUID : IO GCAnyPtr
 38 | allocUUID = onCollectAny !(malloc $ cast sizeOfUUID_t) free
 39 |
 40 | enumerate : Vect n a -> Vect n (Nat, a)
 41 | enumerate = aux 0
 42 |   where
 43 |   aux : Nat -> Vect m a -> Vect m (Nat, a)
 44 |   aux k [] = []
 45 |   aux k (x :: xs) = (k, x) :: aux (S k) xs
 46 |
 47 | ||| A UUID from a byte vector.
 48 | export
 49 | fromBytes : Vect 16 Bits8 -> UUID
 50 | fromBytes bytes =
 51 |   unsafePerformIO $ do
 52 |     uuid <- allocUUID
 53 |     traverse_ (\(i, x) => primIO $ prim__uuidSetByte uuid (cast i) x) $ enumerate bytes
 54 |     pure $ MkUUID uuid
 55 |
 56 | ||| UUID version 1.
 57 | |||
 58 | ||| Uses the current time and the local ethernet MAC address.
 59 | |||
 60 | ||| If the `Bool` is `True`, it is possible that two concurrently running processes obtained the
 61 | ||| same UUID.
 62 | export
 63 | uuid1 : IO (UUID, Bool)
 64 | uuid1 = do
 65 |   uuid <- allocUUID
 66 |   ok <- primIO $ prim__uuidGenerateTimeSafe uuid
 67 |   pure (MkUUID uuid, ok == 0)
 68 |
 69 | ||| UUID version 3.
 70 | |||
 71 | ||| Deterministic UUID created by MD5 hashing `namespace'` and `name`.
 72 | export
 73 | uuid3 : (namespace' : UUID) -> (name : String) -> UUID
 74 | uuid3 ns name = unsafePerformIO $ do
 75 |   uuid <- allocUUID
 76 |   primIO $ prim__uuidGenerateMD5 uuid ns.ptr name (cast $ length name)
 77 |   pure $ MkUUID uuid
 78 |
 79 | ||| UUID version 4.
 80 | |||
 81 | ||| Generates a UUID using high-quality randomness.
 82 | |||
 83 | ||| **Note**: If none of libc `getRandom`, /dev/urandom or /dev/random are available,
 84 | ||| a pseudo-random generator will be substituted, which may compromise UUID uniqueness.
 85 | export
 86 | uuid4 : IO UUID
 87 | uuid4 = do
 88 |   uuid <- allocUUID
 89 |   primIO $ prim__uuidGenerateRandom uuid
 90 |   pure $ MkUUID uuid
 91 |
 92 | ||| UUID version 5.
 93 | |||
 94 | ||| Deterministic UUID created by SHA1 hashing `namespace'` and `name`.
 95 | export
 96 | uuid5 : (namespace' : UUID) -> (name : String) -> UUID
 97 | uuid5 ns name = unsafePerformIO $ do
 98 |   uuid <- allocUUID
 99 |   primIO $ prim__uuidGenerateSHA1 uuid ns.ptr name (cast $ length name)
100 |   pure $ MkUUID uuid
101 |
102 | ||| Try to parse a UUID string (e.g. "1b4e28ba-2fa1-11d2-883f-b9a761bde3fb") as a UUID.
103 | export
104 | parse : String -> Maybe UUID
105 | parse str = unsafePerformIO $ do
106 |   uuid <- allocUUID
107 |   ok <- primIO $ prim__uuidParse str uuid
108 |   pure $ if ok == 0 then Just (MkUUID uuid) else Nothing
109 |
110 | ||| Convert a UUID to string format.
111 | export
112 | unparse : UUID -> String
113 | unparse uuid = unsafePerformIO $ primIO $ prim__uuidUnparse uuid.ptr
114 |