Update documentation of revised dataspacePatterns.prs language

src/protocols/syndicate/dataspacePatterns.md

@@ -19,7 +19,7 @@ corresponds to a (possibly-nested) [binding pattern](#binding) in the overall pa
 Consider the pattern:
 
 ```preserves
-<arr [<lit 1> <bind <arr [<bind <_>> <_>]>> <_>]>
+<arr {0:<lit 1> 1:<bind <arr {0:<bind <_>> 1:<_>}>> 2:<_>}>
 ```
 
 Each of the following values yields different results when matched against it:
@@ -29,10 +29,10 @@ Each of the following values yields different results when matched against it:
  - `[1 [2 3] 4]` succeeds, yielding a binding sequence `[[2 3] 2]`, because the outer `bind`
    captures the whole `[2 3]` array, and the inner (nested) `bind` captures the `2`.
 
- - `[1 [2] 5]` fails, because `[2]` has fewer than the expected two elements.
+ - `[1 [2] 5]` fails, because `[2]` lacks an element at index 1.
 
  - However, `[1 [2 3 4] 5]` succeeds, yielding a binding sequence `[[2 3 4] 2]`, because
-   `[2 3 4]` has *at least* the expected two elements.
+   `[2 3 4]` has *at least* the expected two elements at indexes 0 and 1.
 
  - `[1 [<x> <y>] []]` succeeds, yielding a binding sequence `[[<x> <y>] <x>]`. Each discard
    pattern (`<_>`) ignores the specific input it is given.
@@ -89,28 +89,34 @@ Each *compound pattern* first checks the type of its input: a `rec` pattern fail
 given a Record, an `arr` demands a Sequence and a `dict` only matches a Dictionary.
 
 ```preserves-schema
-DCompound = <rec @label any @fields [Pattern ...]>
-          / <arr @items [Pattern ...]>
+DCompound = <rec @label any @fields { int: Pattern ...:... }>
+          / <arr @items { int: Pattern ...:... }>
           / <dict @entries { any: Pattern ...:... }> .
 ```
 
 If the type check fails, the pattern match fails. Otherwise, matching continues:
 
  - `rec` patterns compare the label of the input Record against the `label` field in the
-   pattern; unless they match literally and exactly, the overall match fails. Otherwise, if the
-   number of fields in the input is smaller than the number expected in the pattern, the match
-   fails. Otherwise, matching proceeds structurally recursively at each field specified in
-   the pattern. The pattern ignores fields present in the input but not mentioned in the pattern.
+   pattern; unless they match literally and exactly, the overall match fails. Otherwise,
+   subpatterns in `fields` are considered in increasing order of key. Each key in `fields` is
+   the index of an input record field to examine. Each subpattern is matched against the
+   corresponding field in the input, failing if no such field exists. The overall pattern thus
+   ignores any position in the input record for which no subpattern exists.
 
- - `arr` patterns fail if the number of subpatterns exceeds the number of items in the
-   input Sequence. Otherwise, matching proceeds structurally recursively at each item specified
-   in the pattern. The pattern ignores items present in the input but not mentioned in the pattern.
+ - `arr` patterns are similar, except without the need for a label check. Subpatterns in
+   `items` are processed in order of key. Each key is interpreted as an element index. Excess
+   or unexamined input elements are ignored.
 
  - `dict` patterns consider each of the key/subpattern pairs in `entries` in turn, according to
    the Preserves order of the keys.[^dict-pattern-ordering] If any given key from the pattern
    is not present in the input value, matching fails. Otherwise, matching proceeds recursively.
    The pattern ignores keys in the input value that are not mentioned in the pattern.
 
+These rules treat Record, Sequence and Dictionary values similarly: matching will succeed if
+such values have *more* than the structure and information required of them by a given pattern,
+but not if they have less. This allows for protocol extension: for example, records with
+"extra" fields will continue to match.
+
 ---
 
 [^efficient-indexing]: Most implementations of Syndicated Actor Model dataspaces use an