summaryrefslogtreecommitdiff
path: root/web/spiderweb/src/larch/lists.web
diff options
context:
space:
mode:
Diffstat (limited to 'web/spiderweb/src/larch/lists.web')
-rw-r--r--web/spiderweb/src/larch/lists.web56
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