Read simple glyph flags

[wezm]

I've forged ahead with some ideas in order to make it possible to read the contours of simple glyphs. I've added the following primitives:

• u16_from_u8 — does what it says
  • I haven't added all the other permutations of safe conversions like this. Open to suggestions here.
• or_succeed — read a format if the supplied Bool is true, else succeed with the supplied default value.
• repeat_until_full — perhaps the most controversial inclusion.
  • repeat_until_full : U16 -> fun (A : Format) -> (Repr A -> U16) -> Format
  • Repr: Array16 len (Repr format)
  • Takes a length, format, and a function that returns how many times to add (Repr format) to the array.
• array_map — map a function over the elements of an existing array to read another array

[brendanzab]

Hum. Yeah we might actually. We don’t directly match on the value (which is what would usually make you reach for force), but it seems like ElimEnv::fun_app doesn’t force the value before matching itself. Not sure if it’s common to force in eliminator helpers like fun_app… might need to take a look at the elaboration-zoo. 🤔

Even if ElimEnv::fun_app did, because we don’t have mutable flexvars at the moment, it’s probably good for performance to force once before iterating.

[brendanzab]

Think it could be worth documenting this parameter with env.name("max_len")

[brendanzab]

Probably would recommend putting let flag_repeat = fun (f : Repr flag) => u16_from_u8 f.repeat + (1 : U16) in a local let binding seeing as it doesn't close over anything useful. This would avoid it showing up in the parsed output.

[brendanzab]

This looks suspicious. Is the idea that each element of the array can produce a different format? If so this isn’t really represented in the definition of Repr... and we don’t have a heterogeneous array type to properly model this (where the types of the elements could be different).

Relatedly, there‘s also a type error in Repr map_fn. The type signature of map_fn is A -> Format, but Repr expects an argument of Format. Sorry if I didn’t catch this!

Alas I don’t have any ideas that come to mind as yet, other than constrained formats to constrain the array*_map formats, and map format to let you map each element format to ensure they have a common representation:

array8_map : fun (len : U8) (A : Type) (B : Type) -> (A -> Format [Repr = B]) -> Array8 len A -> Format

Repr (array8_map len A B map_fn array) = Array8 len B

map : fun (f : Format) (B : Type) -> (Repr f -> B) -> Format

Repr (map f B fn) = B

[mikeday]

It feels like map is something that happens to parsed arrays to produce other parsed arrays, rather than being a format itself 🤔

[wezm]

Is the idea that each element of the array can produce a different format?

To be honest I'm not sure. My grasp on this whole thing is tenuous at best—each time I think I have a handle on it is escapes my grasp. In the motivating example the key thing is this function:

let read_coord = fun (is_short : Repr flag -> Bool) => fun (is_same : Repr flag -> Bool) => fun (f : Repr flag) => {
    coord <- match (is_short f) {
        true => u8,
        false => match (is_same f) {
            true => succeed S16 0,
            false => s16be,
        }
    }
},

In order to read a coordinate you need to take the corresponding flag for that coordinate and based on the bits that are set in it you will read 0, 1, or 2 bytes from the input. In my perhaps broken mental model this was the same format, the same function is used to read all values.

[brendanzab]

It feels like map is something that happens to parsed arrays to produce other parsed arrays, rather than being a format itself 🤔

Yeah the the naming is probably a bit off at any rate - I think this is more like… traverse from Haskell land? I think?

traverse : (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)

traverse : fun {len} {A, B} -> (A -> FormatOf B) -> Array len A -> FormatOf B

where:

• f is FormatOf
• t is Array len