@@ -27,6 +27,7 @@ elaboration, and core language is forthcoming.
2727 - [ Overlap formats] ( #overlap-formats )
2828 - [ Number formats] ( #number-formats )
2929 - [ Array formats] ( #array-formats )
30+ - [ Map formats] ( #map-formats )
3031 - [ Repeat formats] ( #repeat-formats )
3132 - [ Limit formats] ( #limit-formats )
3233 - [ Stream position formats] ( #stream-position-formats )
@@ -505,22 +506,62 @@ of the host [array types](#array-types).
505506| ` array32 len format ` | ` Array32 len (Repr format) ` |
506507| ` array64 len format ` | ` Array64 len (Repr format) ` |
507508
509+ ### Map formats
510+
511+ There are four array map formats, corresponding to the four [ array types] ( #arrays ) .
512+ These allow mapping a supplied function over the elements of an array in order
513+ to parse another array:
514+
515+ - ` array8_map : fun (len : U8) -> fun (A : Type) -> (A -> Format) -> Array8 len A -> Format `
516+ - ` array16_map : fun (len : U16) -> fun (A : Type) -> (A -> Format) -> Array16 len A -> Format `
517+ - ` array32_map : fun (len : U32) -> fun (A : Type) -> (A -> Format) -> Array32 len A -> Format `
518+ - ` array64_map : fun (len : U64) -> fun (A : Type) -> (A -> Format) -> Array64 len A -> Format `
519+
520+ #### Representation of map formats
521+
522+ The [ representation] ( #format-representations ) of the array map formats preserve the
523+ lengths, and use the representation of the map function as the element types
524+ of the host [ array types] ( #array-types ) .
525+
526+ | format | ` Repr ` format |
527+ | ----------------------------------| -----------------------------|
528+ | ` array8_map len A map_fn array ` | ` Array8 len (Repr map_fn) ` |
529+ | ` array16_map len A map_fn array ` | ` Array16 len (Repr map_fn) ` |
530+ | ` array32_map len A map_fn array ` | ` Array32 len (Repr map_fn) ` |
531+ | ` array64_map len A map_fn array ` | ` Array64 len (Repr map_fn) ` |
532+
508533### Repeat formats
509534
510535The ` repeat_until_end ` format repeats parsing the given format until the end of
511536the current binary stream is reached:
512537
513538- ` repeat_until_end : Format -> Format `
514539
540+ There are four repeat until full formats that parse and replicate a format until
541+ a given length is reached:
542+
543+ - ` repeat_until_full8 : U8 -> fun (A : Format) -> (Repr A -> U8) -> Format `
544+ - ` repeat_until_full16 : U16 -> fun (A : Format) -> (Repr A -> U16) -> Format `
545+ - ` repeat_until_full32 : U32 -> fun (A : Format) -> (Repr A -> U32) -> Format `
546+ - ` repeat_until_full64 : U64 -> fun (A : Format) -> (Repr A -> U64) -> Format `
547+
548+ The supplied function can be used to replicate a single parsed format multiple
549+ times into the final array.
550+
515551#### Representation of repeat formats
516552
517- Because the repeat format does not have a predefined length, it is
553+ Because the repeat until end format does not have a predefined length, it is
518554[ represented] ( #format-representations ) as a dynamically sized
519- [ array type] ( #array-types ) :
555+ [ array type] ( #array-types ) . The repeat until full format preserves the length
556+ in its [ representation] ( #format-representations ) :
520557
521- | format | ` Repr ` format |
522- | ------------------------- | --------------------- |
523- | ` repeat_until_end format ` | ` Array (Repr format) ` |
558+ | format | ` Repr ` format |
559+ | -------------------------------------| -----------------------------|
560+ | ` repeat_until_end format ` | ` Array (Repr format) ` |
561+ | ` repeat_until_full8 len replicate ` | ` Array8 len (Repr format) ` |
562+ | ` repeat_until_full16 len replicate ` | ` Array16 len (Repr format) ` |
563+ | ` repeat_until_full32 len replicate ` | ` Array32 len (Repr format) ` |
564+ | ` repeat_until_full64 len replicate ` | ` Array64 len (Repr format) ` |
524565
525566### Limit formats
526567
@@ -595,11 +636,18 @@ embedded in the resulting parsed output.
595636
596637- ` succeed : fun (A : Type) -> A -> Format `
597638
639+ The ` or_succeed ` accepts a boolean condition value. If the condition value is
640+ ` true ` then the format is used, otherwise the default value is used, consuming
641+ no input:
642+
643+ - ` or_succeed : Bool -> fun (A : Format) -> Repr A -> Format `
644+
598645#### Representation of succeed formats
599646
600- | format | ` Repr ` format |
601- | ------------- | ------------- |
602- | ` succeed A a ` | ` A ` |
647+ | format | ` Repr ` format |
648+ | ----------------------------------| ---------------|
649+ | ` succeed A a ` | ` A ` |
650+ | ` or_succeed cond format default ` | ` Repr format ` |
603651
604652### Fail format
605653
@@ -845,6 +893,7 @@ A number of operations are defined for the numeric types:
845893- ` u16_and : U16 -> U16 -> U16 `
846894- ` u16_or : U16 -> U16 -> U16 `
847895- ` u16_xor : U16 -> U16 -> U16 `
896+ - ` u16_from_u8 : U8 -> U16 `
848897
849898- ` u32_eq : U32 -> U32 -> Bool `
850899- ` u32_neq : U32 -> U32 -> Bool `
0 commit comments