@@ -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