Move test_examplefiles to new tests/lexers scheme.examplefiles

1 files changed, 2606 insertions, 0 deletions

diff --git a/tests/lexers/silver/example.txt b/tests/lexers/silver/example.txt
new file mode 100644
index 00000000..e44d4a38
--- /dev/null
+++ b/tests/lexers/silver/example.txt
@@ -0,0 +1,2606 @@
+---input---
+domain Option__Node {
+    unique function Option__Node__Some(): Option__Node
+    unique function Option__Node__None(): Option__Node
+
+    function variantOfOptionNode(self: Ref): Option__Node
+
+    function isOptionNode(self: Ref): Bool
+
+    axiom ax_variantOfOptionNodeChoices {
+        forall x: Ref :: { variantOfOptionNode(x) }
+            (variantOfOptionNode(x) == Option__Node__Some() || variantOfOptionNode(x) == Option__Node__None())
+    }
+
+    axiom ax_isCounterState {
+        forall x: Ref ::  { variantOfOptionNode(x) }
+            isOptionNode(x) == (variantOfOptionNode(x) == Option__Node__Some() ||
+                variantOfOptionNode(x) == Option__Node__None())
+    }
+}
+
+predicate validOption(this: Ref) {
+    isOptionNode(this) &&
+    variantOfOptionNode(this) == Option__Node__Some() ==> (
+        acc(this.Option__Node__Some__1, write) &&
+        acc(validNode(this.Option__Node__Some__1))
+    )
+}
+
+field Option__Node__Some__1: Ref
+
+field Node__v: Int
+field Node__next: Ref
+
+predicate validNode(this: Ref) {
+    acc(this.Node__v) &&
+    acc(this.Node__next) &&
+    acc(validOption(this.Node__next))
+}
+
+
+function length(this: Ref): Int
+    requires acc(validNode(this), write)
+    ensures result >= 1
+{
+    (unfolding acc(validNode(this), write) in
+        unfolding acc(validOption(this.Node__next)) in
+        (variantOfOptionNode(this.Node__next) == Option__Node__None()) ? 
+            1 : 1 + length(this.Node__next.Option__Node__Some__1)
+    )
+}
+
+function itemAt(this: Ref, i: Int): Int
+    requires acc(validNode(this), write)
+    requires 0 <= i && i < length(this)
+{
+    unfolding acc(validNode(this), write) in unfolding acc(validOption(this.Node__next)) in (
+        (i == 0) ?
+            this.Node__v:
+            (variantOfOptionNode(this.Node__next) == Option__Node__Some()) ? 
+                itemAt(this.Node__next.Option__Node__Some__1, i-1) : this.Node__v
+    )
+}
+
+function sum(this$1: Ref): Int
+    requires acc(validNode(this$1), write)
+{
+    (unfolding acc(validNode(this$1), write) in unfolding acc(validOption(this$1.Node__next)) in 
+        (variantOfOptionNode(this$1.Node__next) == Option__Node__None()) ? this$1.Node__v : this$1.Node__v + sum(this$1.Node__next.Option__Node__Some__1))
+}
+
+method append(this: Ref, val: Int)
+    requires acc(validNode(this), write)
+    ensures acc(validNode(this), write) /* POST1 */
+    ensures length(this) == (old(length(this)) + 1) /* POST2 */
+    ensures (forall i: Int :: (0 <= i && i < old(length(this))) ==> (itemAt(this, i) == old(itemAt(this, i)))) /* POST3 */
+    ensures itemAt(this, length(this) - 1) == val /* POST4 */
+    ensures true ==> true
+{
+    var tmp_node: Ref
+    var tmp_option: Ref
+
+    unfold acc(validNode(this), write)
+    unfold acc(validOption(this.Node__next), write)
+
+    if (variantOfOptionNode(this.Node__next) == Option__Node__None()) {
+        tmp_node := new(Node__next, Node__v)
+        tmp_node.Node__next := null
+        tmp_node.Node__v := val
+
+        assume variantOfOptionNode(tmp_node.Node__next) == Option__Node__None()
+        fold acc(validOption(tmp_node.Node__next))
+        fold acc(validNode(tmp_node), write)
+
+        tmp_option := new(Option__Node__Some__1)
+        tmp_option.Option__Node__Some__1 := tmp_node
+        assume variantOfOptionNode(tmp_option) == Option__Node__Some()
+        fold acc(validOption(tmp_option))
+
+        this.Node__next := tmp_option
+
+ 
+        unfold validOption(tmp_option)
+        assert length(tmp_node) == 1 /* TODO: Required by Silicon, POST2 fails otherwise */
+        assert itemAt(tmp_node, 0) == val /* TODO: Required by Silicon, POST4 fails otherwise */
+        fold validOption(tmp_option)
+    } else {
+        append(this.Node__next.Option__Node__Some__1, val)
+        fold acc(validOption(this.Node__next), write)
+    }
+
+    fold acc(validNode(this), write)
+}
+
+method prepend(tail: Ref, val: Int) returns (res: Ref)
+    requires acc(validNode(tail))
+    ensures acc(validNode(res))
+    //ensures acc(validNode(tail))
+    ensures length(res) == old(length(tail)) + 1
+
+    ensures (forall i: Int :: (1 <= i && i < length(res)) ==> (itemAt(res, i) == old(itemAt(tail, i-1)))) /* POST3 */
+    ensures itemAt(res, 0) == val
+{
+    var tmp_option: Ref
+
+    res := new(Node__v, Node__next)
+    res.Node__v := val
+
+    tmp_option := new(Option__Node__Some__1)
+    tmp_option.Option__Node__Some__1 := tail
+    assume variantOfOptionNode(tmp_option) == Option__Node__Some()
+
+    res.Node__next := tmp_option
+
+    assert acc(validNode(tail))
+    fold acc(validOption(res.Node__next))
+    fold acc(validNode(res))
+}
+
+method length_iter(list: Ref) returns (len: Int)
+    requires acc(validNode(list), write)
+    ensures old(length(list)) == len
+    // TODO we have to preserve this property
+    // ensures acc(validNode(list))
+{
+    var curr: Ref := list
+    var tmp: Ref := list
+
+    len := 1
+
+    unfold acc(validNode(curr))
+    unfold acc(validOption(curr.Node__next))
+    while(variantOfOptionNode(curr.Node__next) == Option__Node__Some())
+        invariant acc(curr.Node__v)
+        invariant acc(curr.Node__next)
+        invariant (variantOfOptionNode(curr.Node__next) == Option__Node__Some() ==> (
+            acc(curr.Node__next.Option__Node__Some__1, write) &&
+            acc(validNode(curr.Node__next.Option__Node__Some__1))
+        ))
+        invariant (variantOfOptionNode(curr.Node__next) == Option__Node__Some() ==> len + length(curr.Node__next.Option__Node__Some__1) == old(length(list)))
+        invariant (variantOfOptionNode(curr.Node__next) == Option__Node__None() ==> len == old(length(list)))
+    {
+        assert acc(validNode(curr.Node__next.Option__Node__Some__1))
+        len := len + 1
+        tmp := curr
+        curr := curr.Node__next.Option__Node__Some__1
+        unfold acc(validNode(curr))
+        unfold acc(validOption(curr.Node__next))
+    }
+}
+
+method t1()
+{
+    var l: Ref
+
+    l := new(Node__v, Node__next)
+    l.Node__next := null
+    l.Node__v := 1
+    assume variantOfOptionNode(l.Node__next) == Option__Node__None()
+
+    fold validOption(l.Node__next)
+    fold validNode(l)
+
+    assert length(l) == 1
+    assert itemAt(l, 0) == 1
+
+    append(l, 7)
+    assert itemAt(l, 1) == 7
+    assert itemAt(l, 0) == 1
+    assert length(l) == 2
+
+    l := prepend(l, 10)
+    assert itemAt(l, 2) == 7
+    assert itemAt(l, 1) == 1
+    assert itemAt(l, 0) == 10
+    assert length(l) == 3
+
+    //assert sum(l) == 18
+}
+
+method t2(l: Ref) returns (res: Ref)
+    requires acc(validNode(l), write)
+    ensures acc(validNode(res), write)
+    ensures length(res) > old(length(l))
+{
+    res := prepend(l, 10)
+}
+
+---tokens---
+'domain'      Keyword
+' '           Text
+'Option__Node' Name
+' '           Text
+'{'           Punctuation
+'\n'          Text
+
+'    '        Text
+'unique'      Keyword
+' '           Text
+'function'    Keyword
+' '           Text
+'Option__Node__Some' Name
+'('           Punctuation
+')'           Punctuation
+':'           Operator
+' '           Text
+'Option__Node' Name
+'\n'          Text
+
+'    '        Text
+'unique'      Keyword
+' '           Text
+'function'    Keyword
+' '           Text
+'Option__Node__None' Name
+'('           Punctuation
+')'           Punctuation
+':'           Operator
+' '           Text
+'Option__Node' Name
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'function'    Keyword
+' '           Text
+'variantOfOptionNode' Name
+'('           Punctuation
+'self'        Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+')'           Punctuation
+':'           Operator
+' '           Text
+'Option__Node' Name
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'function'    Keyword
+' '           Text
+'isOptionNode' Name
+'('           Punctuation
+'self'        Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+')'           Punctuation
+':'           Operator
+' '           Text
+'Bool'        Keyword.Type
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'axiom'       Keyword
+' '           Text
+'ax_variantOfOptionNodeChoices' Name
+' '           Text
+'{'           Punctuation
+'\n'          Text
+
+'        '    Text
+'forall'      Keyword
+' '           Text
+'x'           Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+' '           Text
+':'           Operator
+':'           Operator
+' '           Text
+'{ variantOfOptionNode(x) }' Generic.Emph
+'\n'          Text
+
+'            ' Text
+'('           Punctuation
+'variantOfOptionNode' Name
+'('           Punctuation
+'x'           Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__Some' Name
+'('           Punctuation
+')'           Punctuation
+' '           Text
+'|'           Operator
+'|'           Operator
+' '           Text
+'variantOfOptionNode' Name
+'('           Punctuation
+'x'           Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__None' Name
+'('           Punctuation
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'}'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'axiom'       Keyword
+' '           Text
+'ax_isCounterState' Name
+' '           Text
+'{'           Punctuation
+'\n'          Text
+
+'        '    Text
+'forall'      Keyword
+' '           Text
+'x'           Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+' '           Text
+':'           Operator
+':'           Operator
+'  '          Text
+'{ variantOfOptionNode(x) }' Generic.Emph
+'\n'          Text
+
+'            ' Text
+'isOptionNode' Name
+'('           Punctuation
+'x'           Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'('           Punctuation
+'variantOfOptionNode' Name
+'('           Punctuation
+'x'           Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__Some' Name
+'('           Punctuation
+')'           Punctuation
+' '           Text
+'|'           Operator
+'|'           Operator
+'\n'          Text
+
+'                ' Text
+'variantOfOptionNode' Name
+'('           Punctuation
+'x'           Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__None' Name
+'('           Punctuation
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'}'           Punctuation
+'\n'          Text
+
+'}'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'predicate'   Keyword
+' '           Text
+'validOption' Name
+'('           Punctuation
+'this'        Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+')'           Punctuation
+' '           Text
+'{'           Punctuation
+'\n'          Text
+
+'    '        Text
+'isOptionNode' Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+' '           Text
+'&'           Operator
+'&'           Operator
+'\n'          Text
+
+'    '        Text
+'variantOfOptionNode' Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__Some' Name
+'('           Punctuation
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+'>'           Operator
+' '           Text
+'('           Punctuation
+'\n'          Text
+
+'        '    Text
+'acc'         Keyword
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Option__Node__Some__1' Name
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+' '           Text
+'&'           Operator
+'&'           Operator
+'\n'          Text
+
+'        '    Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Option__Node__Some__1' Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+')'           Punctuation
+'\n'          Text
+
+'}'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'field'       Keyword
+' '           Text
+'Option__Node__Some__1' Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+'\n'          Text
+
+'\n'          Text
+
+'field'       Keyword
+' '           Text
+'Node__v'     Name
+':'           Operator
+' '           Text
+'Int'         Keyword.Type
+'\n'          Text
+
+'field'       Keyword
+' '           Text
+'Node__next'  Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+'\n'          Text
+
+'\n'          Text
+
+'predicate'   Keyword
+' '           Text
+'validNode'   Name
+'('           Punctuation
+'this'        Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+')'           Punctuation
+' '           Text
+'{'           Punctuation
+'\n'          Text
+
+'    '        Text
+'acc'         Keyword
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Node__v'     Name
+')'           Punctuation
+' '           Text
+'&'           Operator
+'&'           Operator
+'\n'          Text
+
+'    '        Text
+'acc'         Keyword
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+' '           Text
+'&'           Operator
+'&'           Operator
+'\n'          Text
+
+'    '        Text
+'acc'         Keyword
+'('           Punctuation
+'validOption' Name
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'}'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'\n'          Text
+
+'function'    Keyword
+' '           Text
+'length'      Name
+'('           Punctuation
+'this'        Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+')'           Punctuation
+':'           Operator
+' '           Text
+'Int'         Keyword.Type
+'\n'          Text
+
+'    '        Text
+'requires'    Name.Decorator
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'ensures'     Name.Decorator
+' '           Text
+'result'      Keyword
+' '           Text
+'>'           Operator
+'='           Operator
+' '           Text
+'1'           Literal.Number.Integer
+'\n'          Text
+
+'{'           Punctuation
+'\n'          Text
+
+'    '        Text
+'('           Punctuation
+'unfolding'   Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+' '           Text
+'in'          Keyword
+'\n'          Text
+
+'        '    Text
+'unfolding'   Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validOption' Name
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'in'          Keyword
+'\n'          Text
+
+'        '    Text
+'('           Punctuation
+'variantOfOptionNode' Name
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__None' Name
+'('           Punctuation
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'?'           Operator
+' \n            ' Text
+'1'           Literal.Number.Integer
+' '           Text
+':'           Operator
+' '           Text
+'1'           Literal.Number.Integer
+' '           Text
+'+'           Operator
+' '           Text
+'length'      Name
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Node__next'  Name
+'.'           Punctuation
+'Option__Node__Some__1' Name
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+')'           Punctuation
+'\n'          Text
+
+'}'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'function'    Keyword
+' '           Text
+'itemAt'      Name
+'('           Punctuation
+'this'        Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+','           Punctuation
+' '           Text
+'i'           Name
+':'           Operator
+' '           Text
+'Int'         Keyword.Type
+')'           Punctuation
+':'           Operator
+' '           Text
+'Int'         Keyword.Type
+'\n'          Text
+
+'    '        Text
+'requires'    Name.Decorator
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'requires'    Name.Decorator
+' '           Text
+'0'           Literal.Number.Integer
+' '           Text
+'<'           Operator
+'='           Operator
+' '           Text
+'i'           Name
+' '           Text
+'&'           Operator
+'&'           Operator
+' '           Text
+'i'           Name
+' '           Text
+'<'           Operator
+' '           Text
+'length'      Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+'\n'          Text
+
+'{'           Punctuation
+'\n'          Text
+
+'    '        Text
+'unfolding'   Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+' '           Text
+'in'          Keyword
+' '           Text
+'unfolding'   Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validOption' Name
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'in'          Keyword
+' '           Text
+'('           Punctuation
+'\n'          Text
+
+'        '    Text
+'('           Punctuation
+'i'           Name
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'0'           Literal.Number.Integer
+')'           Punctuation
+' '           Text
+'?'           Operator
+'\n'          Text
+
+'            ' Text
+'this'        Name
+'.'           Punctuation
+'Node__v'     Name
+':'           Operator
+'\n'          Text
+
+'            ' Text
+'('           Punctuation
+'variantOfOptionNode' Name
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__Some' Name
+'('           Punctuation
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'?'           Operator
+' \n                ' Text
+'itemAt'      Name
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Node__next'  Name
+'.'           Punctuation
+'Option__Node__Some__1' Name
+','           Punctuation
+' '           Text
+'i'           Name
+'-'           Operator
+'1'           Literal.Number.Integer
+')'           Punctuation
+' '           Text
+':'           Operator
+' '           Text
+'this'        Name
+'.'           Punctuation
+'Node__v'     Name
+'\n'          Text
+
+'    '        Text
+')'           Punctuation
+'\n'          Text
+
+'}'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'function'    Keyword
+' '           Text
+'sum'         Name
+'('           Punctuation
+'this'        Name
+'$1'          Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+')'           Punctuation
+':'           Operator
+' '           Text
+'Int'         Keyword.Type
+'\n'          Text
+
+'    '        Text
+'requires'    Name.Decorator
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'this'        Name
+'$1'          Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+'\n'          Text
+
+'{'           Punctuation
+'\n'          Text
+
+'    '        Text
+'('           Punctuation
+'unfolding'   Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'this'        Name
+'$1'          Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+' '           Text
+'in'          Keyword
+' '           Text
+'unfolding'   Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validOption' Name
+'('           Punctuation
+'this'        Name
+'$1'          Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'in'          Keyword
+' \n        ' Text
+'('           Punctuation
+'variantOfOptionNode' Name
+'('           Punctuation
+'this'        Name
+'$1'          Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__None' Name
+'('           Punctuation
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'?'           Operator
+' '           Text
+'this'        Name
+'$1'          Name
+'.'           Punctuation
+'Node__v'     Name
+' '           Text
+':'           Operator
+' '           Text
+'this'        Name
+'$1'          Name
+'.'           Punctuation
+'Node__v'     Name
+' '           Text
+'+'           Operator
+' '           Text
+'sum'         Name
+'('           Punctuation
+'this'        Name
+'$1'          Name
+'.'           Punctuation
+'Node__next'  Name
+'.'           Punctuation
+'Option__Node__Some__1' Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'}'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'method'      Keyword
+' '           Text
+'append'      Name
+'('           Punctuation
+'this'        Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+','           Punctuation
+' '           Text
+'val'         Name
+':'           Operator
+' '           Text
+'Int'         Keyword.Type
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'requires'    Name.Decorator
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'ensures'     Name.Decorator
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+' '           Text
+'/*'          Comment.Multiline
+' POST1 '     Comment.Multiline
+'*/'          Comment.Multiline
+'\n'          Text
+
+'    '        Text
+'ensures'     Name.Decorator
+' '           Text
+'length'      Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'('           Punctuation
+'old'         Keyword
+'('           Punctuation
+'length'      Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'+'           Operator
+' '           Text
+'1'           Literal.Number.Integer
+')'           Punctuation
+' '           Text
+'/*'          Comment.Multiline
+' POST2 '     Comment.Multiline
+'*/'          Comment.Multiline
+'\n'          Text
+
+'    '        Text
+'ensures'     Name.Decorator
+' '           Text
+'('           Punctuation
+'forall'      Keyword
+' '           Text
+'i'           Name
+':'           Operator
+' '           Text
+'Int'         Keyword.Type
+' '           Text
+':'           Operator
+':'           Operator
+' '           Text
+'('           Punctuation
+'0'           Literal.Number.Integer
+' '           Text
+'<'           Operator
+'='           Operator
+' '           Text
+'i'           Name
+' '           Text
+'&'           Operator
+'&'           Operator
+' '           Text
+'i'           Name
+' '           Text
+'<'           Operator
+' '           Text
+'old'         Keyword
+'('           Punctuation
+'length'      Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+'>'           Operator
+' '           Text
+'('           Punctuation
+'itemAt'      Name
+'('           Punctuation
+'this'        Name
+','           Punctuation
+' '           Text
+'i'           Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'old'         Keyword
+'('           Punctuation
+'itemAt'      Name
+'('           Punctuation
+'this'        Name
+','           Punctuation
+' '           Text
+'i'           Name
+')'           Punctuation
+')'           Punctuation
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'/*'          Comment.Multiline
+' POST3 '     Comment.Multiline
+'*/'          Comment.Multiline
+'\n'          Text
+
+'    '        Text
+'ensures'     Name.Decorator
+' '           Text
+'itemAt'      Name
+'('           Punctuation
+'this'        Name
+','           Punctuation
+' '           Text
+'length'      Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+' '           Text
+'-'           Operator
+' '           Text
+'1'           Literal.Number.Integer
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'val'         Name
+' '           Text
+'/*'          Comment.Multiline
+' POST4 '     Comment.Multiline
+'*/'          Comment.Multiline
+'\n'          Text
+
+'    '        Text
+'ensures'     Name.Decorator
+' '           Text
+'true'        Keyword
+' '           Text
+'='           Operator
+'='           Operator
+'>'           Operator
+' '           Text
+'true'        Keyword
+'\n'          Text
+
+'{'           Punctuation
+'\n'          Text
+
+'    '        Text
+'var'         Keyword
+' '           Text
+'tmp_node'    Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+'\n'          Text
+
+'    '        Text
+'var'         Keyword
+' '           Text
+'tmp_option'  Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'unfold'      Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'unfold'      Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validOption' Name
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'if'          Keyword
+' '           Text
+'('           Punctuation
+'variantOfOptionNode' Name
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__None' Name
+'('           Punctuation
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'{'           Punctuation
+'\n'          Text
+
+'        '    Text
+'tmp_node'    Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'new'         Keyword
+'('           Punctuation
+'Node__next'  Name
+','           Punctuation
+' '           Text
+'Node__v'     Name
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'tmp_node'    Name
+'.'           Punctuation
+'Node__next'  Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'null'        Keyword
+'\n'          Text
+
+'        '    Text
+'tmp_node'    Name
+'.'           Punctuation
+'Node__v'     Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'val'         Name
+'\n'          Text
+
+'\n'          Text
+
+'        '    Text
+'assume'      Keyword
+' '           Text
+'variantOfOptionNode' Name
+'('           Punctuation
+'tmp_node'    Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__None' Name
+'('           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'fold'        Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validOption' Name
+'('           Punctuation
+'tmp_node'    Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'fold'        Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'tmp_node'    Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'        '    Text
+'tmp_option'  Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'new'         Keyword
+'('           Punctuation
+'Option__Node__Some__1' Name
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'tmp_option'  Name
+'.'           Punctuation
+'Option__Node__Some__1' Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'tmp_node'    Name
+'\n'          Text
+
+'        '    Text
+'assume'      Keyword
+' '           Text
+'variantOfOptionNode' Name
+'('           Punctuation
+'tmp_option'  Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__Some' Name
+'('           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'fold'        Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validOption' Name
+'('           Punctuation
+'tmp_option'  Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'        '    Text
+'this'        Name
+'.'           Punctuation
+'Node__next'  Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'tmp_option'  Name
+'\n'          Text
+
+'\n'          Text
+
+' \n        ' Text
+'unfold'      Keyword
+' '           Text
+'validOption' Name
+'('           Punctuation
+'tmp_option'  Name
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'assert'      Keyword
+' '           Text
+'length'      Name
+'('           Punctuation
+'tmp_node'    Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'1'           Literal.Number.Integer
+' '           Text
+'/*'          Comment.Multiline
+' TODO: Required by Silicon, POST2 fails otherwise ' Comment.Multiline
+'*/'          Comment.Multiline
+'\n'          Text
+
+'        '    Text
+'assert'      Keyword
+' '           Text
+'itemAt'      Name
+'('           Punctuation
+'tmp_node'    Name
+','           Punctuation
+' '           Text
+'0'           Literal.Number.Integer
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'val'         Name
+' '           Text
+'/*'          Comment.Multiline
+' TODO: Required by Silicon, POST4 fails otherwise ' Comment.Multiline
+'*/'          Comment.Multiline
+'\n'          Text
+
+'        '    Text
+'fold'        Keyword
+' '           Text
+'validOption' Name
+'('           Punctuation
+'tmp_option'  Name
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'}'           Punctuation
+' '           Text
+'else'        Keyword
+' '           Text
+'{'           Punctuation
+'\n'          Text
+
+'        '    Text
+'append'      Name
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Node__next'  Name
+'.'           Punctuation
+'Option__Node__Some__1' Name
+','           Punctuation
+' '           Text
+'val'         Name
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'fold'        Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validOption' Name
+'('           Punctuation
+'this'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'}'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'fold'        Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'this'        Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+'\n'          Text
+
+'}'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'method'      Keyword
+' '           Text
+'prepend'     Name
+'('           Punctuation
+'tail'        Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+','           Punctuation
+' '           Text
+'val'         Name
+':'           Operator
+' '           Text
+'Int'         Keyword.Type
+')'           Punctuation
+' '           Text
+'returns'     Keyword
+' '           Text
+'('           Punctuation
+'res'         Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'requires'    Name.Decorator
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'tail'        Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'ensures'     Name.Decorator
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'res'         Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'//ensures acc(validNode(tail))\n' Comment.Single
+
+'    '        Text
+'ensures'     Name.Decorator
+' '           Text
+'length'      Name
+'('           Punctuation
+'res'         Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'old'         Keyword
+'('           Punctuation
+'length'      Name
+'('           Punctuation
+'tail'        Name
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'+'           Operator
+' '           Text
+'1'           Literal.Number.Integer
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'ensures'     Name.Decorator
+' '           Text
+'('           Punctuation
+'forall'      Keyword
+' '           Text
+'i'           Name
+':'           Operator
+' '           Text
+'Int'         Keyword.Type
+' '           Text
+':'           Operator
+':'           Operator
+' '           Text
+'('           Punctuation
+'1'           Literal.Number.Integer
+' '           Text
+'<'           Operator
+'='           Operator
+' '           Text
+'i'           Name
+' '           Text
+'&'           Operator
+'&'           Operator
+' '           Text
+'i'           Name
+' '           Text
+'<'           Operator
+' '           Text
+'length'      Name
+'('           Punctuation
+'res'         Name
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+'>'           Operator
+' '           Text
+'('           Punctuation
+'itemAt'      Name
+'('           Punctuation
+'res'         Name
+','           Punctuation
+' '           Text
+'i'           Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'old'         Keyword
+'('           Punctuation
+'itemAt'      Name
+'('           Punctuation
+'tail'        Name
+','           Punctuation
+' '           Text
+'i'           Name
+'-'           Operator
+'1'           Literal.Number.Integer
+')'           Punctuation
+')'           Punctuation
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'/*'          Comment.Multiline
+' POST3 '     Comment.Multiline
+'*/'          Comment.Multiline
+'\n'          Text
+
+'    '        Text
+'ensures'     Name.Decorator
+' '           Text
+'itemAt'      Name
+'('           Punctuation
+'res'         Name
+','           Punctuation
+' '           Text
+'0'           Literal.Number.Integer
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'val'         Name
+'\n'          Text
+
+'{'           Punctuation
+'\n'          Text
+
+'    '        Text
+'var'         Keyword
+' '           Text
+'tmp_option'  Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'res'         Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'new'         Keyword
+'('           Punctuation
+'Node__v'     Name
+','           Punctuation
+' '           Text
+'Node__next'  Name
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'res'         Name
+'.'           Punctuation
+'Node__v'     Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'val'         Name
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'tmp_option'  Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'new'         Keyword
+'('           Punctuation
+'Option__Node__Some__1' Name
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'tmp_option'  Name
+'.'           Punctuation
+'Option__Node__Some__1' Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'tail'        Name
+'\n'          Text
+
+'    '        Text
+'assume'      Keyword
+' '           Text
+'variantOfOptionNode' Name
+'('           Punctuation
+'tmp_option'  Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__Some' Name
+'('           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'res'         Name
+'.'           Punctuation
+'Node__next'  Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'tmp_option'  Name
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'assert'      Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'tail'        Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'fold'        Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validOption' Name
+'('           Punctuation
+'res'         Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'fold'        Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'res'         Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'}'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'method'      Keyword
+' '           Text
+'length_iter' Name
+'('           Punctuation
+'list'        Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+')'           Punctuation
+' '           Text
+'returns'     Keyword
+' '           Text
+'('           Punctuation
+'len'         Name
+':'           Operator
+' '           Text
+'Int'         Keyword.Type
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'requires'    Name.Decorator
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'list'        Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'ensures'     Name.Decorator
+' '           Text
+'old'         Keyword
+'('           Punctuation
+'length'      Name
+'('           Punctuation
+'list'        Name
+')'           Punctuation
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'len'         Name
+'\n'          Text
+
+'    '        Text
+'// TODO we have to preserve this property\n' Comment.Single
+
+'    '        Text
+'// ensures acc(validNode(list))\n' Comment.Single
+
+'{'           Punctuation
+'\n'          Text
+
+'    '        Text
+'var'         Keyword
+' '           Text
+'curr'        Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'list'        Name
+'\n'          Text
+
+'    '        Text
+'var'         Keyword
+' '           Text
+'tmp'         Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'list'        Name
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'len'         Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'1'           Literal.Number.Integer
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'unfold'      Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'curr'        Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'unfold'      Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validOption' Name
+'('           Punctuation
+'curr'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'while'       Keyword
+'('           Punctuation
+'variantOfOptionNode' Name
+'('           Punctuation
+'curr'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__Some' Name
+'('           Punctuation
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'invariant'   Name.Decorator
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'curr'        Name
+'.'           Punctuation
+'Node__v'     Name
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'invariant'   Name.Decorator
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'curr'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'invariant'   Name.Decorator
+' '           Text
+'('           Punctuation
+'variantOfOptionNode' Name
+'('           Punctuation
+'curr'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__Some' Name
+'('           Punctuation
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+'>'           Operator
+' '           Text
+'('           Punctuation
+'\n'          Text
+
+'            ' Text
+'acc'         Keyword
+'('           Punctuation
+'curr'        Name
+'.'           Punctuation
+'Node__next'  Name
+'.'           Punctuation
+'Option__Node__Some__1' Name
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+' '           Text
+'&'           Operator
+'&'           Operator
+'\n'          Text
+
+'            ' Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'curr'        Name
+'.'           Punctuation
+'Node__next'  Name
+'.'           Punctuation
+'Option__Node__Some__1' Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'invariant'   Name.Decorator
+' '           Text
+'('           Punctuation
+'variantOfOptionNode' Name
+'('           Punctuation
+'curr'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__Some' Name
+'('           Punctuation
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+'>'           Operator
+' '           Text
+'len'         Name
+' '           Text
+'+'           Operator
+' '           Text
+'length'      Name
+'('           Punctuation
+'curr'        Name
+'.'           Punctuation
+'Node__next'  Name
+'.'           Punctuation
+'Option__Node__Some__1' Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'old'         Keyword
+'('           Punctuation
+'length'      Name
+'('           Punctuation
+'list'        Name
+')'           Punctuation
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'invariant'   Name.Decorator
+' '           Text
+'('           Punctuation
+'variantOfOptionNode' Name
+'('           Punctuation
+'curr'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__None' Name
+'('           Punctuation
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+'>'           Operator
+' '           Text
+'len'         Name
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'old'         Keyword
+'('           Punctuation
+'length'      Name
+'('           Punctuation
+'list'        Name
+')'           Punctuation
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'{'           Punctuation
+'\n'          Text
+
+'        '    Text
+'assert'      Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'curr'        Name
+'.'           Punctuation
+'Node__next'  Name
+'.'           Punctuation
+'Option__Node__Some__1' Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'len'         Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'len'         Name
+' '           Text
+'+'           Operator
+' '           Text
+'1'           Literal.Number.Integer
+'\n'          Text
+
+'        '    Text
+'tmp'         Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'curr'        Name
+'\n'          Text
+
+'        '    Text
+'curr'        Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'curr'        Name
+'.'           Punctuation
+'Node__next'  Name
+'.'           Punctuation
+'Option__Node__Some__1' Name
+'\n'          Text
+
+'        '    Text
+'unfold'      Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'curr'        Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'        '    Text
+'unfold'      Keyword
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validOption' Name
+'('           Punctuation
+'curr'        Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'}'           Punctuation
+'\n'          Text
+
+'}'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'method'      Keyword
+' '           Text
+'t1'          Name
+'('           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'{'           Punctuation
+'\n'          Text
+
+'    '        Text
+'var'         Keyword
+' '           Text
+'l'           Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'l'           Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'new'         Keyword
+'('           Punctuation
+'Node__v'     Name
+','           Punctuation
+' '           Text
+'Node__next'  Name
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'l'           Name
+'.'           Punctuation
+'Node__next'  Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'null'        Keyword
+'\n'          Text
+
+'    '        Text
+'l'           Name
+'.'           Punctuation
+'Node__v'     Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'1'           Literal.Number.Integer
+'\n'          Text
+
+'    '        Text
+'assume'      Keyword
+' '           Text
+'variantOfOptionNode' Name
+'('           Punctuation
+'l'           Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'Option__Node__None' Name
+'('           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'fold'        Keyword
+' '           Text
+'validOption' Name
+'('           Punctuation
+'l'           Name
+'.'           Punctuation
+'Node__next'  Name
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'fold'        Keyword
+' '           Text
+'validNode'   Name
+'('           Punctuation
+'l'           Name
+')'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'assert'      Keyword
+' '           Text
+'length'      Name
+'('           Punctuation
+'l'           Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'1'           Literal.Number.Integer
+'\n'          Text
+
+'    '        Text
+'assert'      Keyword
+' '           Text
+'itemAt'      Name
+'('           Punctuation
+'l'           Name
+','           Punctuation
+' '           Text
+'0'           Literal.Number.Integer
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'1'           Literal.Number.Integer
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'append'      Name
+'('           Punctuation
+'l'           Name
+','           Punctuation
+' '           Text
+'7'           Literal.Number.Integer
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'assert'      Keyword
+' '           Text
+'itemAt'      Name
+'('           Punctuation
+'l'           Name
+','           Punctuation
+' '           Text
+'1'           Literal.Number.Integer
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'7'           Literal.Number.Integer
+'\n'          Text
+
+'    '        Text
+'assert'      Keyword
+' '           Text
+'itemAt'      Name
+'('           Punctuation
+'l'           Name
+','           Punctuation
+' '           Text
+'0'           Literal.Number.Integer
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'1'           Literal.Number.Integer
+'\n'          Text
+
+'    '        Text
+'assert'      Keyword
+' '           Text
+'length'      Name
+'('           Punctuation
+'l'           Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'2'           Literal.Number.Integer
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'l'           Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'prepend'     Name
+'('           Punctuation
+'l'           Name
+','           Punctuation
+' '           Text
+'10'          Literal.Number.Integer
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'assert'      Keyword
+' '           Text
+'itemAt'      Name
+'('           Punctuation
+'l'           Name
+','           Punctuation
+' '           Text
+'2'           Literal.Number.Integer
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'7'           Literal.Number.Integer
+'\n'          Text
+
+'    '        Text
+'assert'      Keyword
+' '           Text
+'itemAt'      Name
+'('           Punctuation
+'l'           Name
+','           Punctuation
+' '           Text
+'1'           Literal.Number.Integer
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'1'           Literal.Number.Integer
+'\n'          Text
+
+'    '        Text
+'assert'      Keyword
+' '           Text
+'itemAt'      Name
+'('           Punctuation
+'l'           Name
+','           Punctuation
+' '           Text
+'0'           Literal.Number.Integer
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'10'          Literal.Number.Integer
+'\n'          Text
+
+'    '        Text
+'assert'      Keyword
+' '           Text
+'length'      Name
+'('           Punctuation
+'l'           Name
+')'           Punctuation
+' '           Text
+'='           Operator
+'='           Operator
+' '           Text
+'3'           Literal.Number.Integer
+'\n'          Text
+
+'\n'          Text
+
+'    '        Text
+'//assert sum(l) == 18\n' Comment.Single
+
+'}'           Punctuation
+'\n'          Text
+
+'\n'          Text
+
+'method'      Keyword
+' '           Text
+'t2'          Name
+'('           Punctuation
+'l'           Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+')'           Punctuation
+' '           Text
+'returns'     Keyword
+' '           Text
+'('           Punctuation
+'res'         Name
+':'           Operator
+' '           Text
+'Ref'         Keyword.Type
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'requires'    Name.Decorator
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'l'           Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'ensures'     Name.Decorator
+' '           Text
+'acc'         Keyword
+'('           Punctuation
+'validNode'   Name
+'('           Punctuation
+'res'         Name
+')'           Punctuation
+','           Punctuation
+' '           Text
+'write'       Keyword
+')'           Punctuation
+'\n'          Text
+
+'    '        Text
+'ensures'     Name.Decorator
+' '           Text
+'length'      Name
+'('           Punctuation
+'res'         Name
+')'           Punctuation
+' '           Text
+'>'           Operator
+' '           Text
+'old'         Keyword
+'('           Punctuation
+'length'      Name
+'('           Punctuation
+'l'           Name
+')'           Punctuation
+')'           Punctuation
+'\n'          Text
+
+'{'           Punctuation
+'\n'          Text
+
+'    '        Text
+'res'         Name
+' '           Text
+':'           Operator
+'='           Operator
+' '           Text
+'prepend'     Name
+'('           Punctuation
+'l'           Name
+','           Punctuation
+' '           Text
+'10'          Literal.Number.Integer
+')'           Punctuation
+'\n'          Text
+
+'}'           Punctuation
+'\n'          Text