import "foo.tdf"
import "foo.txt"
import "foo.txt"

domain Foo[T] {
    axiom named { forall x: Int:: {lookup(x)} len(lookup(x)) == foobar(x) }
    axiom { forall x: Int :: {lookup(x)} {len(lookup(x))} len(lookup(x)) == foobar(x) } // anonymous
}

// this is a comment

/* This is also
 * another multi-line comment
 * With a string "string" and
 * an import "foo.bar" inside */

// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

import "empty.sil"

method test1(xs: Seq[Ref]) {
  inhale forall i: Int :: 0 <= i && i < |xs| ==> xs[i].f != 0
}

function $(n: Ref, m: Ref): Node

domain Foo[T] {
    function enc(arg: T): Foo[T]
    function dec(arg: Foo[T]): T

    axiom ax_Dec {
        forall arg: T ::
            dec( enc(arg) ) == arg
    }

    axiom ax_Enc {
        forall arg: Foo[T] ::
        { enc( dec(arg) ), foo(bar, i) }
            {  dec(arg) }
                enc( dec(arg) ) == arg
    }
}

function myFunc(arg: Int): Int
    requires true || false
    ensures arg <= 0 ==> result == -1
    ensures arg > 0  ==> result == arg
{
    arg > 0 ? arg : myFunc(arg - 1)
}

field value: Int
field next: Ref

predicate list(xs: Ref) {
    acc(xs.value) && acc(xs.next)
    && ( list(xs.next) )
}

define myPureMacro(abc) abc

define myStmtMacro(abc) {
    inhale abc
    exhale abc
}

method smokeTest() {

    inhale false; exhale false
    assume false; assert false

    //magic wands
    var s: Set[Int]
    assert s setminus s != s

}

//:: special comment
/*
        gfdgfd
*/

method testHighlights() returns ( res: Set[Seq[Multiset[Foo[Int]]]] )
    requires true
    ensures false
{
    var a: Int; var b: Bool; var c: Ref; var d: Rational; var e: Perm
    var x: Seq[Int]; var y: Set[Int]; var z: Multiset[Int]
    var t1: Set[Int] := Set(a, 1, 2)
    var t2: Seq[Int] := Seq(a, a, a)
    var t3: Multiset[Int] := Multiset(a, a, 0, 0, 0)

    assert myFunc(331) > -2

    myStmtMacro( myFunc(331) == -331 )

    while ( true )
        invariant true
    {
        var aa: Ref
        aa := null
        var bb: Int
        bb := 33
    }

    if ( true ) {
        assert true
    } elseif ( false ) {
        assert false
    } else {
        assert true
    }

    //forperm r: Ref :: true
    //exists
    //forall
    assert ! false
    assert 0  +321 - 0 -321 == 0
}

field f:Int

method test02(x: Ref)
  requires acc(x.f, write)
  ensures acc(x.f, write)
{
  define A true
  define B acc(x.f, write)

  package A --* B
  wand w := A --* B

  //apply w

    label my_lbl

    goto my_lbl

    fresh x

    var p: Perm

    var r: Ref; r := new (*)

    constraining ( p ) {
        exhale acc(x.f, p)
    }

    assert 0 == ( let a == (11 + 22) in a+a )
}