---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
