'module' Keyword.Namespace ' ' Text.Whitespace 'examples' Name '/' Operator 'systems' Name '/' Operator 'views' Name '\n' Text.Whitespace '\n' Text.Whitespace '/*\n * Model of views in object-oriented programming.\n *\n * Two object references, called the view and the backing,\n * are related by a view mechanism when changes to the\n * backing are automatically propagated to the view. Note\n * that the state of a view need not be a projection of the\n * state of the backing; the keySet method of Map, for\n * example, produces two view relationships, and for the\n * one in which the map is modified by changes to the key\n * set, the value of the new map cannot be determined from\n * the key set. Note that in the iterator view mechanism,\n * the iterator is by this definition the backing object,\n * since changes are propagated from iterator to collection\n * and not vice versa. Oddly, a reference may be a view of\n * more than one backing: there can be two iterators on the\n * same collection, eg. A reference cannot be a view under\n * more than one view type.\n *\n * A reference is made dirty when it is a backing for a view\n * with which it is no longer related by the view invariant.\n * This usually happens when a view is modified, either\n * directly or via another backing. For example, changing a\n * collection directly when it has an iterator invalidates\n * it, as does changing the collection through one iterator\n * when there are others.\n *\n * More work is needed if we want to model more closely the\n * failure of an iterator when its collection is invalidated.\n *\n * As a terminological convention, when there are two\n * complementary view relationships, we will give them types\n * t and t". For example, KeySetView propagates from map to\n * set, and KeySetView" propagates from set to map.\n *\n * author: Daniel Jackson\n */' Comment.Multiline '\n' Text.Whitespace '\n' Text.Whitespace 'open' Keyword.Namespace ' ' Text.Whitespace 'util' Name '/' Operator 'ordering' Name '[' Operator 'State' Name ']' Operator ' ' Text.Whitespace 'as' Keyword ' ' Text.Whitespace 'so' Name '\n' Text.Whitespace 'open' Keyword.Namespace ' ' Text.Whitespace 'util' Name '/' Operator 'relation' Name ' ' Text.Whitespace 'as' Keyword ' ' Text.Whitespace 'rel' Name '\n' Text.Whitespace '\n' Text.Whitespace 'sig' Keyword.Declaration ' ' Text.Whitespace 'Ref' Name ' ' Text.Whitespace '{' Operator '}' Operator '\n' Text.Whitespace 'sig' Keyword.Declaration ' ' Text.Whitespace 'Object' Name ' ' Text.Whitespace '{' Operator '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace '-- t->b->v in views when v is view of type t of backing b' Comment.Single '\n' Text.Whitespace '-- dirty contains refs that have been invalidated' Comment.Single '\n' Text.Whitespace 'sig' Keyword.Declaration ' ' Text.Whitespace 'State' Name ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'refs' Name ':' Punctuation ' ' Text.Whitespace 'set' Keyword ' ' Text.Whitespace 'Ref' Name ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 'obj' Name ':' Punctuation ' ' Text.Whitespace 'refs' Name ' ' Text.Whitespace '->' Operator ' ' Text.Whitespace 'one' Keyword ' ' Text.Whitespace 'Object' Name ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 'views' Name ':' Punctuation ' ' Text.Whitespace 'ViewType' Name ' ' Text.Whitespace '->' Operator ' ' Text.Whitespace 'refs' Name ' ' Text.Whitespace '->' Operator ' ' Text.Whitespace 'refs' Name ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 'dirty' Name ':' Punctuation ' ' Text.Whitespace 'set' Keyword ' ' Text.Whitespace 'refs' Name '\n' Text.Whitespace '-- , anyviews: Ref -> Ref -- for visualization' Comment.Single '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace '-- {anyviews = ViewType.views}' Comment.Single '\n' Text.Whitespace '\n' Text.Whitespace 'sig' Keyword.Declaration ' ' Text.Whitespace 'Map' Name ' ' Text.Whitespace 'extends' Keyword ' ' Text.Whitespace 'Object' Name ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'keys' Name ':' Punctuation ' ' Text.Whitespace 'set' Keyword ' ' Text.Whitespace 'Ref' Name ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 'map' Name ':' Punctuation ' ' Text.Whitespace 'keys' Name ' ' Text.Whitespace '->' Operator ' ' Text.Whitespace 'one' Keyword ' ' Text.Whitespace 'Ref' Name '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '{' Operator 'all' Keyword ' ' Text.Whitespace 's' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ' ' Text.Whitespace '|' Operator ' ' Text.Whitespace 'keys' Name ' ' Text.Whitespace '+' Operator ' ' Text.Whitespace 'Ref' Name '.' Operator 'map' Name ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 's' Name '.' Operator 'refs' Name '}' Operator '\n' Text.Whitespace 'sig' Keyword.Declaration ' ' Text.Whitespace 'MapRef' Name ' ' Text.Whitespace 'extends' Keyword ' ' Text.Whitespace 'Ref' Name ' ' Text.Whitespace '{' Operator '}' Operator '\n' Text.Whitespace 'fact' Keyword ' ' Text.Whitespace '{' Operator 'State' Name '.' Operator 'obj' Name '[' Operator 'MapRef' Name ']' Operator ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'Map' Name '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace 'sig' Keyword.Declaration ' ' Text.Whitespace 'Iterator' Name ' ' Text.Whitespace 'extends' Keyword ' ' Text.Whitespace 'Object' Name ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'left' Name ',' Punctuation ' ' Text.Whitespace 'done' Name ':' Punctuation ' ' Text.Whitespace 'set' Keyword ' ' Text.Whitespace 'Ref' Name ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 'lastRef' Name ':' Punctuation ' ' Text.Whitespace 'lone' Keyword ' ' Text.Whitespace 'done' Name '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '{' Operator 'all' Keyword ' ' Text.Whitespace 's' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ' ' Text.Whitespace '|' Operator ' ' Text.Whitespace 'done' Name ' ' Text.Whitespace '+' Operator ' ' Text.Whitespace 'left' Name ' ' Text.Whitespace '+' Operator ' ' Text.Whitespace 'lastRef' Name ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 's' Name '.' Operator 'refs' Name '}' Operator '\n' Text.Whitespace 'sig' Keyword.Declaration ' ' Text.Whitespace 'IteratorRef' Name ' ' Text.Whitespace 'extends' Keyword ' ' Text.Whitespace 'Ref' Name ' ' Text.Whitespace '{' Operator '}' Operator '\n' Text.Whitespace 'fact' Keyword ' ' Text.Whitespace '{' Operator 'State' Name '.' Operator 'obj' Name '[' Operator 'IteratorRef' Name ']' Operator ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'Iterator' Name '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace 'sig' Keyword.Declaration ' ' Text.Whitespace 'Set' Name ' ' Text.Whitespace 'extends' Keyword ' ' Text.Whitespace 'Object' Name ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'elts' Name ':' Punctuation ' ' Text.Whitespace 'set' Keyword ' ' Text.Whitespace 'Ref' Name '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '{' Operator 'all' Keyword ' ' Text.Whitespace 's' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ' ' Text.Whitespace '|' Operator ' ' Text.Whitespace 'elts' Name ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 's' Name '.' Operator 'refs' Name '}' Operator '\n' Text.Whitespace 'sig' Keyword.Declaration ' ' Text.Whitespace 'SetRef' Name ' ' Text.Whitespace 'extends' Keyword ' ' Text.Whitespace 'Ref' Name ' ' Text.Whitespace '{' Operator '}' Operator '\n' Text.Whitespace 'fact' Keyword ' ' Text.Whitespace '{' Operator 'State' Name '.' Operator 'obj' Name '[' Operator 'SetRef' Name ']' Operator ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'Set' Name '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace 'abstract' Keyword ' ' Text.Whitespace 'sig' Keyword.Declaration ' ' Text.Whitespace 'ViewType' Name ' ' Text.Whitespace '{' Operator '}' Operator '\n' Text.Whitespace 'one' Keyword ' ' Text.Whitespace 'sig' Keyword.Declaration ' ' Text.Whitespace 'KeySetView' Name ',' Punctuation ' ' Text.Whitespace 'KeySetView"' Name ',' Punctuation ' ' Text.Whitespace 'IteratorView' Name ' ' Text.Whitespace 'extends' Keyword ' ' Text.Whitespace 'ViewType' Name ' ' Text.Whitespace '{' Operator '}' Operator '\n' Text.Whitespace 'fact' Keyword ' ' Text.Whitespace 'ViewTypes' Name ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'State' Name '.' Operator 'views' Name '[' Operator 'KeySetView' Name ']' Operator ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'MapRef' Name ' ' Text.Whitespace '->' Operator ' ' Text.Whitespace 'SetRef' Name '\n' Text.Whitespace ' ' Text.Whitespace 'State' Name '.' Operator 'views' Name '[' Operator 'KeySetView"' Name ']' Operator ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'SetRef' Name ' ' Text.Whitespace '->' Operator ' ' Text.Whitespace 'MapRef' Name '\n' Text.Whitespace ' ' Text.Whitespace 'State' Name '.' Operator 'views' Name '[' Operator 'IteratorView' Name ']' Operator ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'IteratorRef' Name ' ' Text.Whitespace '->' Operator ' ' Text.Whitespace 'SetRef' Name '\n' Text.Whitespace ' ' Text.Whitespace 'all' Keyword ' ' Text.Whitespace 's' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ' ' Text.Whitespace '|' Operator ' ' Text.Whitespace 's' Name '.' Operator 'views' Name '[' Operator 'KeySetView' Name ']' Operator ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace '~' Operator '(' Operator 's' Name '.' Operator 'views' Name '[' Operator 'KeySetView"' Name ']' Operator ')' Operator '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace "/**\n * mods is refs modified directly or by view mechanism\n * doesn't handle possibility of modifying an object and its view at once?\n * should we limit frame conds to non-dirty refs?\n */" Comment.Multiline '\n' Text.Whitespace 'pred' Keyword ' ' Text.Whitespace 'modifies' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ',' Punctuation ' ' Text.Whitespace 'rs' Name ':' Punctuation ' ' Text.Whitespace 'set' Keyword ' ' Text.Whitespace 'Ref' Name ']' Operator ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'let' Keyword ' ' Text.Whitespace 'vr' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pre' Name '.' Operator 'views' Name '[' Operator 'ViewType' Name ']' Operator ',' Punctuation ' ' Text.Whitespace 'mods' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'rs' Name '.' Operator '*' Operator 'vr' Name ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'all' Keyword ' ' Text.Whitespace 'r' Name ':' Punctuation ' ' Text.Whitespace 'pre' Name '.' Operator 'refs' Name ' ' Text.Whitespace '-' Operator ' ' Text.Whitespace 'mods' Name ' ' Text.Whitespace '|' Operator ' ' Text.Whitespace 'pre' Name '.' Operator 'obj' Name '[' Operator 'r' Name ']' Operator ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'post' Name '.' Operator 'obj' Name '[' Operator 'r' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'all' Keyword ' ' Text.Whitespace 'b' Name ':' Punctuation ' ' Text.Whitespace 'mods' Name ',' Punctuation ' ' Text.Whitespace 'v' Name ':' Punctuation ' ' Text.Whitespace 'pre' Name '.' Operator 'refs' Name ',' Punctuation ' ' Text.Whitespace 't' Name ':' Punctuation ' ' Text.Whitespace 'ViewType' Name ' ' Text.Whitespace '|' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'b' Name '->' Operator 'v' Name ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'pre' Name '.' Operator 'views' Name '[' Operator 't' Name ']' Operator ' ' Text.Whitespace '=' Operator '>' Operator ' ' Text.Whitespace 'viewFrame' Name ' ' Text.Whitespace '[' Operator 't' Name ',' Punctuation ' ' Text.Whitespace 'pre' Name '.' Operator 'obj' Name '[' Operator 'v' Name ']' Operator ',' Punctuation ' ' Text.Whitespace 'post' Name '.' Operator 'obj' Name '[' Operator 'v' Name ']' Operator ',' Punctuation ' ' Text.Whitespace 'post' Name '.' Operator 'obj' Name '[' Operator 'b' Name ']' Operator ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'post' Name '.' Operator 'dirty' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pre' Name '.' Operator 'dirty' Name ' ' Text.Whitespace '+' Operator '\n' Text.Whitespace ' ' Text.Whitespace '{' Operator 'b' Name ':' Punctuation ' ' Text.Whitespace 'pre' Name '.' Operator 'refs' Name ' ' Text.Whitespace '|' Operator ' ' Text.Whitespace 'some' Keyword ' ' Text.Whitespace 'v' Name ':' Punctuation ' ' Text.Whitespace 'Ref' Name ',' Punctuation ' ' Text.Whitespace 't' Name ':' Punctuation ' ' Text.Whitespace 'ViewType' Name ' ' Text.Whitespace '|' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'b' Name '->' Operator 'v' Name ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'pre' Name '.' Operator 'views' Name '[' Operator 't' Name ']' Operator ' ' Text.Whitespace '&&' Operator ' ' Text.Whitespace '!' Operator 'viewFrame' Name ' ' Text.Whitespace '[' Operator 't' Name ',' Punctuation ' ' Text.Whitespace 'pre' Name '.' Operator 'obj' Name '[' Operator 'v' Name ']' Operator ',' Punctuation ' ' Text.Whitespace 'post' Name '.' Operator 'obj' Name '[' Operator 'v' Name ']' Operator ',' Punctuation ' ' Text.Whitespace 'post' Name '.' Operator 'obj' Name '[' Operator 'b' Name ']' Operator ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace 'pred' Keyword ' ' Text.Whitespace 'allocates' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ',' Punctuation ' ' Text.Whitespace 'rs' Name ':' Punctuation ' ' Text.Whitespace 'set' Keyword ' ' Text.Whitespace 'Ref' Name ']' Operator ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'no' Keyword ' ' Text.Whitespace 'rs' Name ' ' Text.Whitespace '&' Operator ' ' Text.Whitespace 'pre' Name '.' Operator 'refs' Name '\n' Text.Whitespace ' ' Text.Whitespace 'post' Name '.' Operator 'refs' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pre' Name '.' Operator 'refs' Name ' ' Text.Whitespace '+' Operator ' ' Text.Whitespace 'rs' Name '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace '/** \n * models frame condition that limits change to view object from v to v" when backing object changes to b"\n */' Comment.Multiline '\n' Text.Whitespace 'pred' Keyword ' ' Text.Whitespace 'viewFrame' Name ' ' Text.Whitespace '[' Operator 't' Name ':' Punctuation ' ' Text.Whitespace 'ViewType' Name ',' Punctuation ' ' Text.Whitespace 'v' Name ',' Punctuation ' ' Text.Whitespace 'v"' Name ',' Punctuation ' ' Text.Whitespace 'b"' Name ':' Punctuation ' ' Text.Whitespace 'Object' Name ']' Operator ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 't' Name ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'KeySetView' Name ' ' Text.Whitespace '=' Operator '>' Operator ' ' Text.Whitespace 'v"' Name '.' Operator 'elts' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'dom' Name ' ' Text.Whitespace '[' Operator 'b"' Name '.' Operator 'map' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 't' Name ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'KeySetView"' Name ' ' Text.Whitespace '=' Operator '>' Operator ' ' Text.Whitespace 'b"' Name '.' Operator 'elts' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'dom' Name ' ' Text.Whitespace '[' Operator 'v"' Name '.' Operator 'map' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 't' Name ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'KeySetView"' Name ' ' Text.Whitespace '=' Operator '>' Operator ' ' Text.Whitespace '(' Operator 'b"' Name '.' Operator 'elts' Name ')' Operator ' ' Text.Whitespace '<' Operator ':' Punctuation ' ' Text.Whitespace '(' Operator 'v' Name '.' Operator 'map' Name ')' Operator ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace '(' Operator 'b"' Name '.' Operator 'elts' Name ')' Operator ' ' Text.Whitespace '<' Operator ':' Punctuation ' ' Text.Whitespace '(' Operator 'v"' Name '.' Operator 'map' Name ')' Operator '\n' Text.Whitespace ' ' Text.Whitespace 't' Name ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'IteratorView' Name ' ' Text.Whitespace '=' Operator '>' Operator ' ' Text.Whitespace 'v"' Name '.' Operator 'elts' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'b"' Name '.' Operator 'left' Name ' ' Text.Whitespace '+' Operator ' ' Text.Whitespace 'b"' Name '.' Operator 'done' Name '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace 'pred' Keyword ' ' Text.Whitespace 'MapRef' Name '.' Operator 'keySet' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ',' Punctuation ' ' Text.Whitespace 'setRefs' Name ':' Punctuation ' ' Text.Whitespace 'SetRef' Name ']' Operator ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'post' Name '.' Operator 'obj' Name '[' Operator 'setRefs' Name ']' Operator '.' Operator 'elts' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'dom' Name ' ' Text.Whitespace '[' Operator 'pre' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator '.' Operator 'map' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'modifies' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ',' Punctuation ' ' Text.Whitespace 'none' Keyword.Constant ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'allocates' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ',' Punctuation ' ' Text.Whitespace 'setRefs' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'post' Name '.' Operator 'views' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pre' Name '.' Operator 'views' Name ' ' Text.Whitespace '+' Operator ' ' Text.Whitespace 'KeySetView' Name '->' Operator 'this' Keyword '->' Operator 'setRefs' Name ' ' Text.Whitespace '+' Operator ' ' Text.Whitespace 'KeySetView"' Name '->' Operator 'setRefs' Name '->' Operator 'this' Keyword '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace 'pred' Keyword ' ' Text.Whitespace 'MapRef' Name '.' Operator 'put' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ',' Punctuation ' ' Text.Whitespace 'k' Name ',' Punctuation ' ' Text.Whitespace 'v' Name ':' Punctuation ' ' Text.Whitespace 'Ref' Name ']' Operator ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'post' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator '.' Operator 'map' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pre' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator '.' Operator 'map' Name ' ' Text.Whitespace '++' Operator ' ' Text.Whitespace 'k' Name '->' Operator 'v' Name '\n' Text.Whitespace ' ' Text.Whitespace 'modifies' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ',' Punctuation ' ' Text.Whitespace 'this' Keyword ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'allocates' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ',' Punctuation ' ' Text.Whitespace 'none' Keyword.Constant ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'post' Name '.' Operator 'views' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pre' Name '.' Operator 'views' Name '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace 'pred' Keyword ' ' Text.Whitespace 'SetRef' Name '.' Operator 'iterator' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ',' Punctuation ' ' Text.Whitespace 'iterRef' Name ':' Punctuation ' ' Text.Whitespace 'IteratorRef' Name ']' Operator ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'let' Keyword ' ' Text.Whitespace 'i' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'post' Name '.' Operator 'obj' Name '[' Operator 'iterRef' Name ']' Operator ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'i' Name '.' Operator 'left' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pre' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator '.' Operator 'elts' Name '\n' Text.Whitespace ' ' Text.Whitespace 'no' Keyword ' ' Text.Whitespace 'i' Name '.' Operator 'done' Name ' ' Text.Whitespace '+' Operator ' ' Text.Whitespace 'i' Name '.' Operator 'lastRef' Name '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'modifies' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation 'post' Name ',' Punctuation 'none' Keyword.Constant ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'allocates' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ',' Punctuation ' ' Text.Whitespace 'iterRef' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'post' Name '.' Operator 'views' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pre' Name '.' Operator 'views' Name ' ' Text.Whitespace '+' Operator ' ' Text.Whitespace 'IteratorView' Name '->' Operator 'iterRef' Name '->' Operator 'this' Keyword '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace 'pred' Keyword ' ' Text.Whitespace 'IteratorRef' Name '.' Operator 'remove' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ']' Operator ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'let' Keyword ' ' Text.Whitespace 'i' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pre' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator ',' Punctuation ' ' Text.Whitespace 'i"' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'post' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'i"' Name '.' Operator 'left' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'i' Name '.' Operator 'left' Name '\n' Text.Whitespace ' ' Text.Whitespace 'i"' Name '.' Operator 'done' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'i' Name '.' Operator 'done' Name ' ' Text.Whitespace '-' Operator ' ' Text.Whitespace 'i' Name '.' Operator 'lastRef' Name '\n' Text.Whitespace ' ' Text.Whitespace 'no' Keyword ' ' Text.Whitespace 'i"' Name '.' Operator 'lastRef' Name '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'modifies' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation 'post' Name ',' Punctuation 'this' Keyword ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'allocates' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ',' Punctuation ' ' Text.Whitespace 'none' Keyword.Constant ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'pre' Name '.' Operator 'views' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'post' Name '.' Operator 'views' Name '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace 'pred' Keyword ' ' Text.Whitespace 'IteratorRef' Name '.' Operator 'next' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ',' Punctuation ' ' Text.Whitespace 'ref' Name ':' Punctuation ' ' Text.Whitespace 'Ref' Name ']' Operator ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'let' Keyword ' ' Text.Whitespace 'i' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'pre' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator ',' Punctuation ' ' Text.Whitespace 'i"' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'post' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'ref' Name ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'i' Name '.' Operator 'left' Name '\n' Text.Whitespace ' ' Text.Whitespace 'i"' Name '.' Operator 'left' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'i' Name '.' Operator 'left' Name ' ' Text.Whitespace '-' Operator ' ' Text.Whitespace 'ref' Name '\n' Text.Whitespace ' ' Text.Whitespace 'i"' Name '.' Operator 'done' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'i' Name '.' Operator 'done' Name ' ' Text.Whitespace '+' Operator ' ' Text.Whitespace 'ref' Name '\n' Text.Whitespace ' ' Text.Whitespace 'i"' Name '.' Operator 'lastRef' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'ref' Name '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'modifies' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ',' Punctuation ' ' Text.Whitespace 'this' Keyword ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'allocates' Name ' ' Text.Whitespace '[' Operator 'pre' Name ',' Punctuation ' ' Text.Whitespace 'post' Name ',' Punctuation ' ' Text.Whitespace 'none' Keyword.Constant ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'pre' Name '.' Operator 'views' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace 'post' Name '.' Operator 'views' Name '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace 'pred' Keyword ' ' Text.Whitespace 'IteratorRef' Name '.' Operator 'hasNext' Name ' ' Text.Whitespace '[' Operator 's' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ']' Operator ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'some' Keyword ' ' Text.Whitespace 's' Name '.' Operator 'obj' Name '[' Operator 'this' Keyword ']' Operator '.' Operator 'left' Name '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace 'assert' Keyword ' ' Text.Whitespace 'zippishOK' Name ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'all' Keyword '\n' Text.Whitespace ' ' Text.Whitespace 'ks' Name ',' Punctuation ' ' Text.Whitespace 'vs' Name ':' Punctuation ' ' Text.Whitespace 'SetRef' Name ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 'm' Name ':' Punctuation ' ' Text.Whitespace 'MapRef' Name ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 'ki' Name ',' Punctuation ' ' Text.Whitespace 'vi' Name ':' Punctuation ' ' Text.Whitespace 'IteratorRef' Name ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 'k' Name ',' Punctuation ' ' Text.Whitespace 'v' Name ':' Punctuation ' ' Text.Whitespace 'Ref' Name ' ' Text.Whitespace '|' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'let' Keyword ' ' Text.Whitespace 's0' Name '=' Operator 'so' Name '/' Operator 'first' Name ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 's1' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's0' Name ']' Operator ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 's2' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's1' Name ']' Operator ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 's3' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's2' Name ']' Operator ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 's4' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's3' Name ']' Operator ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 's5' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's4' Name ']' Operator ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 's6' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's5' Name ']' Operator ',' Punctuation '\n' Text.Whitespace ' ' Text.Whitespace 's7' Name '=' Operator 'so' Name '/' Operator 'next' Name '[' Operator 's6' Name ']' Operator ' ' Text.Whitespace '|' Operator '\n' Text.Whitespace ' ' Text.Whitespace '(' Operator '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'precondition' Name ' ' Text.Whitespace '[' Operator 's0' Name ',' Punctuation ' ' Text.Whitespace 'ks' Name ',' Punctuation ' ' Text.Whitespace 'vs' Name ',' Punctuation ' ' Text.Whitespace 'm' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'no' Keyword ' ' Text.Whitespace 's0' Name '.' Operator 'dirty' Name '\n' Text.Whitespace ' ' Text.Whitespace 'ks' Name '.' Operator 'iterator' Name ' ' Text.Whitespace '[' Operator 's0' Name ',' Punctuation ' ' Text.Whitespace 's1' Name ',' Punctuation ' ' Text.Whitespace 'ki' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'vs' Name '.' Operator 'iterator' Name ' ' Text.Whitespace '[' Operator 's1' Name ',' Punctuation ' ' Text.Whitespace 's2' Name ',' Punctuation ' ' Text.Whitespace 'vi' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'ki' Name '.' Operator 'hasNext' Name ' ' Text.Whitespace '[' Operator 's2' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'vi' Name '.' Operator 'hasNext' Name ' ' Text.Whitespace '[' Operator 's2' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'ki' Name '.' Operator 'this' Keyword '/' Operator 'next' Name ' ' Text.Whitespace '[' Operator 's2' Name ',' Punctuation ' ' Text.Whitespace 's3' Name ',' Punctuation ' ' Text.Whitespace 'k' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'vi' Name '.' Operator 'this' Keyword '/' Operator 'next' Name ' ' Text.Whitespace '[' Operator 's3' Name ',' Punctuation ' ' Text.Whitespace 's4' Name ',' Punctuation ' ' Text.Whitespace 'v' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'm' Name '.' Operator 'put' Name ' ' Text.Whitespace '[' Operator 's4' Name ',' Punctuation ' ' Text.Whitespace 's5' Name ',' Punctuation ' ' Text.Whitespace 'k' Name ',' Punctuation ' ' Text.Whitespace 'v' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'ki' Name '.' Operator 'remove' Name ' ' Text.Whitespace '[' Operator 's5' Name ',' Punctuation ' ' Text.Whitespace 's6' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'vi' Name '.' Operator 'remove' Name ' ' Text.Whitespace '[' Operator 's6' Name ',' Punctuation ' ' Text.Whitespace 's7' Name ']' Operator '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator ' ' Text.Whitespace '=' Operator '>' Operator ' ' Text.Whitespace 'no' Keyword ' ' Text.Whitespace 'State' Name '.' Operator 'dirty' Name ')' Operator '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace 'pred' Keyword ' ' Text.Whitespace 'precondition' Name ' ' Text.Whitespace '[' Operator 'pre' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ',' Punctuation ' ' Text.Whitespace 'ks' Name ',' Punctuation ' ' Text.Whitespace 'vs' Name ',' Punctuation ' ' Text.Whitespace 'm' Name ':' Punctuation ' ' Text.Whitespace 'Ref' Name ']' Operator ' ' Text.Whitespace '{' Operator '\n' Text.Whitespace ' ' Text.Whitespace '// all these conditions and other errors discovered in scope of 6 but 8,3' Comment.Single '\n' Text.Whitespace ' ' Text.Whitespace '// in initial state, must have view invariants hold' Comment.Single '\n' Text.Whitespace ' ' Text.Whitespace '(' Operator 'all' Keyword ' ' Text.Whitespace 't' Name ':' Punctuation ' ' Text.Whitespace 'ViewType' Name ',' Punctuation ' ' Text.Whitespace 'b' Name ',' Punctuation ' ' Text.Whitespace 'v' Name ':' Punctuation ' ' Text.Whitespace 'pre' Name '.' Operator 'refs' Name ' ' Text.Whitespace '|' Operator '\n' Text.Whitespace ' ' Text.Whitespace 'b' Name '->' Operator 'v' Name ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace 'pre' Name '.' Operator 'views' Name '[' Operator 't' Name ']' Operator ' ' Text.Whitespace '=' Operator '>' Operator ' ' Text.Whitespace 'viewFrame' Name ' ' Text.Whitespace '[' Operator 't' Name ',' Punctuation ' ' Text.Whitespace 'pre' Name '.' Operator 'obj' Name '[' Operator 'v' Name ']' Operator ',' Punctuation ' ' Text.Whitespace 'pre' Name '.' Operator 'obj' Name '[' Operator 'v' Name ']' Operator ',' Punctuation ' ' Text.Whitespace 'pre' Name '.' Operator 'obj' Name '[' Operator 'b' Name ']' Operator ']' Operator ')' Operator '\n' Text.Whitespace ' ' Text.Whitespace '// sets are not aliases' Comment.Single '\n' Text.Whitespace '-- ks != vs' Comment.Single '\n' Text.Whitespace ' ' Text.Whitespace '// sets are not views of map' Comment.Single '\n' Text.Whitespace '-- no (ks+vs)->m & ViewType.pre.views' Comment.Single '\n' Text.Whitespace ' ' Text.Whitespace '// no iterator currently on either set' Comment.Single '\n' Text.Whitespace '-- no Ref->(ks+vs) & ViewType.pre.views' Comment.Single '\n' Text.Whitespace ' ' Text.Whitespace '}' Operator '\n' Text.Whitespace '\n' Text.Whitespace 'check' Keyword ' ' Text.Whitespace 'zippishOK' Name ' ' Text.Whitespace 'for' Keyword ' ' Text.Whitespace '6' Literal.Number.Integer ' ' Text.Whitespace 'but' Keyword ' ' Text.Whitespace '8' Literal.Number.Integer ' ' Text.Whitespace 'State' Name ',' Punctuation ' ' Text.Whitespace '3' Literal.Number.Integer ' ' Text.Whitespace 'ViewType' Name ' ' Text.Whitespace 'expect' Keyword ' ' Text.Whitespace '1' Literal.Number.Integer '\n' Text.Whitespace '\n' Text.Whitespace '/** \n * experiment with controlling heap size\n */' Comment.Multiline '\n' Text.Whitespace 'fact' Keyword ' ' Text.Whitespace '{' Operator 'all' Keyword ' ' Text.Whitespace 's' Name ':' Punctuation ' ' Text.Whitespace 'State' Name ' ' Text.Whitespace '|' Operator ' ' Text.Whitespace '#' Operator 's' Name '.' Operator 'obj' Name ' ' Text.Whitespace '<' Operator ' ' Text.Whitespace '5' Literal.Number.Integer '}' Operator '\n' Text.Whitespace