Extended Exercise: Full Solution
As promised, here is the full DaeDaLus PNG specification:
1import Daedalus
2
3-- Utilities
4
5def Length = BEUInt32
6def Crc = BEUInt32
7
8def FLAG = $[0 .. 1]
9
10def NullChar = $[0]
11def NonNullChar = $[1 .. 255]
12
13def OMany (omin:maybe (uint 64)) (omax:maybe (uint 64)) P =
14 case omin of
15 nothing -> case omax of
16 nothing -> Many P
17 just max -> Many (..max) P
18 just min -> case omax of
19 nothing -> Many (min..) P
20 just max -> Many (min..max) P
21
22def NTString (omin:maybe (uint 64)) (omax:maybe (uint 64)) =
23 block
24 $$ = OMany omin omax NonNullChar
25 NullChar
26
27def RGB =
28 block
29 red = UInt8
30 green = UInt8
31 blue = UInt8
32
33def UTCTime =
34 block
35 year = BEUInt16
36 month = $[1 .. 12]
37 day = $[1 .. 31]
38 hour = $[0 .. 23]
39 minute = $[0 .. 59]
40 second = $[0 .. 60]
41
42-- Chunks / PNG
43
44bitdata ChunkType where
45 plte = { 80 : uint 8 ; 76 : uint 8 ; 84 : uint 8 ; 69 : uint 8 }
46 idat = { 73 : uint 8 ; 68 : uint 8 ; 65 : uint 8 ; 84 : uint 8 }
47 trns = { 116 : uint 8 ; 82 : uint 8 ; 78 : uint 8 ; 83 : uint 8 }
48 chrm = { 99 : uint 8 ; 72 : uint 8 ; 82 : uint 8 ; 77 : uint 8 }
49 gama = { 103 : uint 8 ; 65 : uint 8 ; 77 : uint 8 ; 65 : uint 8 }
50 iccp = { 105 : uint 8 ; 67 : uint 8 ; 67 : uint 8 ; 80 : uint 8 }
51 sbit = { 115 : uint 8 ; 66 : uint 8 ; 73 : uint 8 ; 84 : uint 8 }
52 srgb = { 115 : uint 8 ; 82 : uint 8 ; 71 : uint 8 ; 66 : uint 8 }
53 text = { 116 : uint 8 ; 69 : uint 8 ; 88 : uint 8 ; 116 : uint 8 }
54 itxt = { 105 : uint 8 ; 84 : uint 8 ; 88 : uint 8 ; 116 : uint 8 }
55 ztxt = { 122 : uint 8 ; 84 : uint 8 ; 88 : uint 8 ; 116 : uint 8 }
56 bkgd = { 98 : uint 8 ; 75 : uint 8 ; 71 : uint 8 ; 68 : uint 8 }
57 hist = { 104 : uint 8 ; 73 : uint 8 ; 83 : uint 8 ; 84 : uint 8 }
58 phys = { 112 : uint 8 ; 72 : uint 8 ; 89 : uint 8 ; 115 : uint 8 }
59 splt = { 115 : uint 8 ; 80 : uint 8 ; 76 : uint 8 ; 84 : uint 8 }
60 time = { 116 : uint 8 ; 73 : uint 8 ; 77 : uint 8 ; 69 : uint 8 }
61
62def ChunkData sig (type : ChunkType) =
63 case type of
64 plte -> {| plte_data = PLTEChunkData |}
65 idat -> {| idat_data = IDATChunkData |}
66 trns -> {| trns_data = TRNSChunkData sig |}
67 chrm -> {| chrm_data = CHRMChunkData |}
68 gama -> {| gama_data = GAMAChunkData |}
69 iccp -> {| iccp_data = ICCPChunkData |}
70 sbit -> {| sbit_data = SBITChunkData sig |}
71 srgb -> {| srgb_data = SRGBChunkData |}
72 text -> {| text_data = TEXTChunkData |}
73 itxt -> {| itxt_data = ITXTChunkData |}
74 ztxt -> {| ztxt_data = ZTXTChunkData |}
75 bkgd -> {| bkgd_data = BKGDChunkData sig |}
76 hist -> {| hist_data = HISTChunkData |}
77 phys -> {| phys_data = PHYSChunkData |}
78 splt -> {| splt_data = SPLTChunkData |}
79 time -> {| time_data = TIMEChunkData |}
80
81def PLTEChunkData = Many (1..256) RGB
82
83def IDATChunkData = Many UInt8
84
85def TRNSChunkData sig =
86 case sig.colour_type of
87 0 -> {| trns_colour_type_0 = TRNSData0 |}
88 2 -> {| trns_colour_type_2 = TRNSData2 |}
89 3 -> {| trns_colour_type_3 = TRNSData3 |}
90 _ -> Fail "tRNS chunk shall not appear for other colour types"
91
92def TRNSData0 =
93 block
94 grey_sample_value = BEUInt16
95
96def TRNSData2 =
97 block
98 red_sample_value = BEUInt16
99 blue_sample_value = BEUInt16
100 green_sample_value = BEUInt16
101
102def TRNSData3 =
103 block
104 alpha_for_palette = Many UInt8
105
106def CHRMChunkData =
107 block
108 white_point_x = BEUInt32
109 white_point_y = BEUInt32
110 red_x = BEUInt32
111 red_y = BEUInt32
112 green_x = BEUInt32
113 green_y = BEUInt32
114 blue_x = BEUInt32
115 blue_y = BEUInt32
116
117def GAMAChunkData =
118 block
119 image_gamma = BEUInt32
120
121def ICCPChunkData =
122 block
123 profile_name = NTString (just 1) (just 79)
124 compression_method = UInt8
125 compressed_profile = Many UInt8
126
127def SBITChunkData sig =
128 case sig.colour_type of
129 0 -> {| sbit_colour_type_0 = SBITData0 |}
130 2 -> {| sbit_colour_type_2 = SBITData2or3 |}
131 3 -> {| sbit_colour_type_3 = SBITData2or3 |}
132 4 -> {| sbit_colour_type_4 = SBITData4 |}
133 6 -> {| sbit_colour_type_6 = SBITData6 |}
134
135def SBITData0 =
136 block
137 significant_greyscale_bits = UInt8
138
139def SBITData2or3 =
140 block
141 significant_red_bits = UInt8
142 significant_green_bits = UInt8
143 significant_blue_bits = UInt8
144
145def SBITData4 =
146 block
147 significant_greyscale_bits = UInt8
148 significant_alpha_bits = UInt8
149
150def SBITData6 =
151 block
152 significant_red_bits = UInt8
153 significant_green_bits = UInt8
154 significant_blue_bits = UInt8
155 significant_alpha_bits = UInt8
156
157def SRGBChunkData =
158 block
159 rendering_intent = $[0 .. 3]
160
161def TEXTChunkData =
162 block
163 keyword = NTString (just 1) (just 79)
164 text_string = Many UInt8
165
166def ZTXTChunkData =
167 block
168 keyword = NTString (just 1) (just 79)
169 compression_method = UInt8
170 compressed_text_datastream = Many UInt8
171
172def ITXTChunkData =
173 block
174 keyword = NTString (just 1) (just 79)
175 compression_flag = FLAG
176 compression_method = UInt8
177 language_tag = NTString nothing nothing
178 translated_keyword = NTString nothing nothing
179 text = Many UInt8
180
181def BKGDChunkData sig =
182 case sig.colour_type of
183 0 -> {| bkgd_colour_type_0 = BKGDData0or4 |}
184 4 -> {| bkgd_colour_type_4 = BKGDData0or4 |}
185 2 -> {| bkgd_colour_type_2 = BKGDData2or6 |}
186 6 -> {| bkgd_colour_type_6 = BKGDData2or6 |}
187 3 -> {| bkgd_colour_type_3 = BKGDData3 |}
188
189def BKGDData0or4 =
190 block
191 greyscale = BEUInt16
192
193def BKGDData2or6 =
194 block
195 red = BEUInt16
196 green = BEUInt16
197 blue = BEUInt16
198
199def BKGDData3 =
200 block
201 palette_index = UInt8
202
203def HISTChunkData =
204 block
205 frequencies = Many BEUInt16
206
207def PHYSChunkData =
208 block
209 pixels_per_unit_x_axis = BEUInt32
210 pixels_per_unit_y_axis = BEUInt32
211 unit_specifier = FLAG
212
213def SPLTChunkData =
214 block
215 palette_name = NTString (just 1) (just 79)
216 sample_depth = $[ 8 ] <| $[ 16 ]
217 Many (SPLTSample sample_depth)
218
219def SPLTSample (depth : uint 8) =
220 case depth of
221 8 -> {| splt_sample_depth_8 = SPLTSample8 |}
222 16 -> {| splt_sample_depth_16 = SPLTSample16 |}
223
224def SPLTSample8 =
225 block
226 red = UInt8
227 green = UInt8
228 blue = UInt8
229 alpha = UInt8
230 frequency = BEUInt16
231
232def SPLTSample16 =
233 block
234 red = BEUInt16
235 green = BEUInt16
236 blue = BEUInt16
237 alpha = BEUInt16
238 frequency = BEUInt16
239
240def TIMEChunkData = UTCTime
241
242def PNGChunk sig =
243 block
244 let len = Length as uint 64
245 type = BEUInt32 as? ChunkType
246 data = Chunk len (ChunkData sig type)
247 crc = Crc
248
249def IHDRChunk =
250 block
251 Match [ 0; 0; 0; 13]
252 Match [ 73; 72; 68; 82]
253 width = BEUInt32
254 height = BEUInt32
255 bit_depth = UInt8
256 colour_type = UInt8
257 compression_method = UInt8
258 filter_method = UInt8
259 interlace_method = UInt8
260 crc = Crc
261
262def IENDChunk =
263 block
264 Match [0; 0; 0; 0]
265 Match [73; 69; 78; 68]
266 crc = Crc
267
268def PNGHeader =
269 Match [ 137; 80; 78; 71; 13; 10; 26; 10]
270
271def Main =
272 block
273 PNGHeader
274 signature = IHDRChunk
275 chunks = Many (PNGChunk signature)
276 IENDChunk
277 END