diff options
Diffstat (limited to 'web/spiderweb/src/larch/lists.web')
-rw-r--r-- | web/spiderweb/src/larch/lists.web | 56 |
1 files changed, 56 insertions, 0 deletions
diff --git a/web/spiderweb/src/larch/lists.web b/web/spiderweb/src/larch/lists.web new file mode 100644 index 0000000000..8a1f2bca27 --- /dev/null +++ b/web/spiderweb/src/larch/lists.web @@ -0,0 +1,56 @@ +@*Theory of sequences. +The theory of sequences is built on the theory of stacks. +The stack theory provides most of the machinery needed for the elementary +operations on lists: |insert|, |head|, |tail|, and |is_empty|. +The sequence trait includes +additional machinery that allows easy specification of concatenation. +@c +sequence: trait + imports Stack_theory with [nil for empty_stack, + cons for push, first for top, rest for pop] + introduces + enter: C,E -> C % adds e to back of c + last: C -> E + prefix: C -> C % c with last deleted + #.[#]:C, Card -> E % indexed selection (starts at 1) + append: C,C -> C % concatenation + + constrains [C] so that C is generated by [new, insert] + C is generated by [new, enter] + C is partitioned by [first, rest, isEmpty] + C is partitioned by [last, prefix, isEmpty] + + for all [e:E] + last(enter(new,e)) = e + prefix(enter(new,e)) = new + + for all [c:C, e:E] + not isEmpty(enter(c,e)) + last(enter(c,e)) = e + prefix(enter(c,e)) = stk + + for all [c:C, e, e1: E] + insert(new,e) = enter(new,e) + insert(enter(c,e),e1) = enter(insert(c,e1),e) + + for all [c:C, i:Card] + c.[1] = first(c) + c.[i+1] = rest(c).[i] + + for all [c,c1:C, e:E] + append(c,new) = c + append(c,insert(c1,e)) = insert(append(c,c1), e) + + implies + converts [insert, first, last, rest, prefix], + [enter, first, last, rest, prefix], + [append], + [isEmpty], + [size], + [#.[#]] + + + exempts last(new), prefix(new), first(new), rest(new) +% for all [c:C], c(0) + +@*Index.
\ No newline at end of file |