1 | module Goop.Types.Uuid
3 | import Data.List.Quantifiers
4 | import Derive.Prelude
5 | import Decidable.Equality
6 | import Generics.Derive
8 | import Goop.Types.BitsN
10 | %language ElabReflection
11 | %prefix_record_projections off
12 | %hide Generics.Derive.Show
13 | %hide Generics.Derive.Eq
14 | %hide Generics.Derive.Ord
24 | namespace VersionError
26 | data VersionError : Type where
27 | UnusedVersion : VersionError
28 | ReservedVersion : BitsN 4 -> VersionError
29 | %runElab derive "VersionError" [Show]
33 | data UuidError : Type where
34 | Version : VersionError -> UuidError
35 | %runElab derive "UuidError" [Show]
52 | %name Uuid.Version
ver, ver2, ver3
53 | %runElab derive "Version" [Generic, DecEq, Eq, Ord, Show]
56 | versionToBits : Version -> BitsN 4
57 | versionToBits V1 = 0b0001
58 | versionToBits V2 = 0b0010
59 | versionToBits V3 = 0b0011
60 | versionToBits V4 = 0b0100
61 | versionToBits V5 = 0b0101
62 | versionToBits V6 = 0b0110
63 | versionToBits V7 = 0b0111
64 | versionToBits V8 = 0b1000
67 | bitsToVersion : BitsN 4 -> Either VersionError Version
68 | bitsToVersion 0b0000 = Left UnusedVersion
69 | bitsToVersion 0b0001 = Right V1
70 | bitsToVersion 0b0010 = Right V2
71 | bitsToVersion 0b0011 = Right V3
72 | bitsToVersion 0b0100 = Right V4
73 | bitsToVersion 0b0101 = Right V5
74 | bitsToVersion 0b0110 = Right V6
75 | bitsToVersion 0b0111 = Right V7
76 | bitsToVersion 0b1000 = Right V8
77 | bitsToVersion x = Left $
ReservedVersion x
80 | fieldLengths : Version -> List Nat
81 | fieldLengths V1 = [32, 16, 4, 12, 2, 14, 48]
82 | fieldLengths V2 = [48, 4, 76]
83 | fieldLengths V3 = [48, 4, 12, 2, 62]
84 | fieldLengths V4 = [48, 4, 12, 2, 62]
85 | fieldLengths V5 = [48, 4, 12, 2, 62]
86 | fieldLengths V6 = [32, 16, 4, 12, 2, 14, 48]
87 | fieldLengths V7 = [48, 4, 12, 2, 62]
88 | fieldLengths V8 = [48, 4, 12, 2, 62]
91 | fieldLengthsSum : (ver : Version) -> 128 = sumLengths (fieldLengths ver)
92 | fieldLengthsSum V1 = Refl
93 | fieldLengthsSum V2 = Refl
94 | fieldLengthsSum V3 = Refl
95 | fieldLengthsSum V4 = Refl
96 | fieldLengthsSum V5 = Refl
97 | fieldLengthsSum V6 = Refl
98 | fieldLengthsSum V7 = Refl
99 | fieldLengthsSum V8 = Refl
116 | data Uuid : Version -> Type where
117 | UuidV1 : (time_low : BitsN 32) -> (time_mid : BitsN 16) -> (time_high : BitsN 12)
118 | -> (clock_seq : BitsN 14) -> (node : BitsN 48)
121 | UuidV2 : (high : BitsN 48) -> (low : BitsN 76) -> Uuid V2
122 | UuidV3 : (md5_high : BitsN 48) -> (md5_mid : BitsN 12) -> (md5_low : BitsN 62) -> Uuid V3
123 | UuidV4 : (random_a : BitsN 48) -> (random_b : BitsN 12) -> (random_c : BitsN 62) -> Uuid V4
124 | UuidV5 : (sha1_high : BitsN 48) -> (sha1_mid : BitsN 12) -> (sha1_low : BitsN 62) -> Uuid V5
125 | UuidV6 : (time_high : BitsN 32) -> (time_mid : BitsN 16) -> (time_low : BitsN 12)
126 | -> (clock_seq : BitsN 14) -> (node : BitsN 48)
128 | UuidV7 : (unix_ts_ms : BitsN 48) -> (rand_a : BitsN 12) -> (rand_b : BitsN 62) -> Uuid V7
129 | UuidV8 : (custom_a : BitsN 48) -> (custom_b : BitsN 12) -> (custom_c : BitsN 62) -> Uuid V8
131 | %name Uuid
uuid, uuid2, uuid3
132 | %runElab derive "Uuid" [Eq, Ord, Show]
136 | version : Uuid ver -> Version
137 | version (UuidV1 _ _ _ _ _) = V1
138 | version (UuidV2 _ _) = V2
139 | version (UuidV3 _ _ _) = V3
140 | version (UuidV4 _ _ _) = V4
141 | version (UuidV5 _ _ _) = V5
142 | version (UuidV6 _ _ _ _ _) = V6
143 | version (UuidV7 _ _ _) = V7
144 | version (UuidV8 _ _ _) = V8
147 | versionCorrect : (uuid : Uuid ver) -> version uuid = ver
148 | versionCorrect (UuidV1 _ _ _ _ _) = Refl
149 | versionCorrect (UuidV2 _ _) = Refl
150 | versionCorrect (UuidV3 _ _ _) = Refl
151 | versionCorrect (UuidV4 _ _ _) = Refl
152 | versionCorrect (UuidV5 _ _ _) = Refl
153 | versionCorrect (UuidV6 _ _ _ _ _) = Refl
154 | versionCorrect (UuidV7 _ _ _) = Refl
155 | versionCorrect (UuidV8 _ _ _) = Refl
159 | uuidToFields : (uuid : Uuid ver) -> All BitsN (fieldLengths (version uuid))
160 | uuidToFields (UuidV1 time_low time_mid time_high clock_seq node) =
161 | [time_low, time_mid, versionToBits V1, time_high, RFCVar, clock_seq, node]
162 | uuidToFields (UuidV2 high low) =
163 | [high, versionToBits V2, low]
164 | uuidToFields (UuidV3 md5_high md5_mid md5_low) =
165 | [md5_high, versionToBits V3, md5_mid, RFCVar, md5_low]
166 | uuidToFields (UuidV4 random_a random_b random_c) =
167 | [random_a, versionToBits V4, random_b, RFCVar, random_c]
168 | uuidToFields (UuidV5 sha1_high sha1_mid sha1_low) =
169 | [sha1_high, versionToBits V5, sha1_mid, RFCVar, sha1_low]
170 | uuidToFields (UuidV6 time_high time_mid time_low clock_seq node) =
171 | [time_high, time_mid, versionToBits V6, time_low, RFCVar, clock_seq, node]
172 | uuidToFields (UuidV7 unix_ts_ms rand_a rand_b) =
173 | [unix_ts_ms, versionToBits V7, rand_a, RFCVar, rand_b]
174 | uuidToFields (UuidV8 custom_a custom_b custom_c) =
175 | [custom_a, versionToBits V8, custom_b, RFCVar, custom_c]
179 | uuidToInteger : Uuid ver -> BitsN 128
180 | uuidToInteger uuid = rewrite fieldLengthsSum (version uuid) in concat (uuidToFields uuid)
184 | FormattedUuidFields : List Nat
185 | FormattedUuidFields = [4 * 8, 2 * 8, 2 * 8, 2 * 8, 6 * 8]
187 | Interpolation (Uuid ver) where
189 | let [first, second, third, forth, fifth] = splits FormattedUuidFields (uuidToInteger x)
190 | in "\{first}-\{second}-\{third}-\{forth}-\{fifth}"
192 | namespace Versioned
195 | record VersionedUuid where
196 | constructor MkVerUuid
198 | uuid : Uuid version
200 | %name VersionedUuid
uuid, uuid2, uuid3
201 | %runElab derive "VersionedUuid" [Show]
203 | Eq VersionedUuid where
204 | (==) (MkVerUuid version_x uuid_x) (MkVerUuid version_y uuid_y) =
205 | case decEq version_x version_y of
206 | Yes Refl => uuid_x == uuid_y
209 | Ord VersionedUuid where
210 | compare (MkVerUuid version_x uuid_x) (MkVerUuid version_y uuid_y) =
211 | case decEq version_x version_y of
212 | Yes Refl => compare uuid_x uuid_y
213 | No _ => compare version_x version_y
215 | Interpolation VersionedUuid where
216 | interpolate x = interpolate x.uuid