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