@@ -27,6 +27,7 @@ elaboration, and core language is forthcoming.
27
27
- [ Overlap formats] ( #overlap-formats )
28
28
- [ Number formats] ( #number-formats )
29
29
- [ Array formats] ( #array-formats )
30
+ - [ Map formats] ( #map-formats )
30
31
- [ Repeat formats] ( #repeat-formats )
31
32
- [ Limit formats] ( #limit-formats )
32
33
- [ Stream position formats] ( #stream-position-formats )
@@ -505,22 +506,62 @@ of the host [array types](#array-types).
505
506
| ` array32 len format ` | ` Array32 len (Repr format) ` |
506
507
| ` array64 len format ` | ` Array64 len (Repr format) ` |
507
508
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
+
508
533
### Repeat formats
509
534
510
535
The ` repeat_until_end ` format repeats parsing the given format until the end of
511
536
the current binary stream is reached:
512
537
513
538
- ` repeat_until_end : Format -> Format `
514
539
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
+
515
551
#### Representation of repeat formats
516
552
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
518
554
[ 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 ) :
520
557
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) ` |
524
565
525
566
### Limit formats
526
567
@@ -595,11 +636,18 @@ embedded in the resulting parsed output.
595
636
596
637
- ` succeed : fun (A : Type) -> A -> Format `
597
638
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
+
598
645
#### Representation of succeed formats
599
646
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 ` |
603
651
604
652
### Fail format
605
653
@@ -845,6 +893,7 @@ A number of operations are defined for the numeric types:
845
893
- ` u16_and : U16 -> U16 -> U16 `
846
894
- ` u16_or : U16 -> U16 -> U16 `
847
895
- ` u16_xor : U16 -> U16 -> U16 `
896
+ - ` u16_from_u8 : U8 -> U16 `
848
897
849
898
- ` u32_eq : U32 -> U32 -> Bool `
850
899
- ` u32_neq : U32 -> U32 -> Bool `
0 commit comments