allows domains to implement an interface

src/main/scala/viper/gobra/frontend/info/implementation/property/Implements.scala

@@ -113,6 +113,7 @@ trait Implements { this: TypeInfoImpl =>
         case ut: Type.OptionT => go(ut.elem)
         case ut: Type.AdtT =>
           ut.clauses.forall(_.fields.forall(f => go(f._2)))
+        case _: Type.DomainT => true
         case ut: GhostCollectionType => go(ut.elem)
         case _: Type.InterfaceT => true
         case _ => false

src/test/resources/regressions/features/domains/implements-interface-fail01.gobra

@@ -0,0 +1,36 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// this testcase checks that a ghost value of a type implementing an interface
+// cannot be passed to a non-ghost context
+
+package ImplementsInterfaceFail01
+
+ghost type intPair domain {
+    func fst(intPair) int
+    func snd(intPair) int
+    func pair(int, int) intPair
+
+    axiom {
+      forall p intPair :: {fst(p)}{snd(p)} p == pair(fst(p),snd(p))
+    } // pair
+
+    axiom {
+      forall l, r int :: {pair(l,r)} l == fst(pair(l,r)) && r == snd(pair(l,r))
+    }
+}
+
+// the following clause should be permitted by the type-checker:
+intPair implements any
+
+func test() {
+    x := pair(1,2)
+    //:: ExpectedOutput(type_error)
+    assert equal(x, x) // fails as `equal` is actual
+}
+
+decreases
+requires isComparable(a)
+pure func equal(a, b any) bool {
+    return a == b
+}

src/test/resources/regressions/features/domains/implements-interface-simple01.gobra

@@ -0,0 +1,37 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// this testcase checks whether a domain can implement an interface
+
+package ImplementsInterfaceSimple01
+
+ghost type intPair domain {
+    func fst(intPair) int
+    func snd(intPair) int
+    func pair(int, int) intPair
+
+    axiom {
+      forall p intPair :: {fst(p)}{snd(p)} p == pair(fst(p),snd(p))
+    } // pair
+
+    axiom {
+      forall l, r int :: {pair(l,r)} l == fst(pair(l,r)) && r == snd(pair(l,r))
+    }
+}
+
+// the following clause should be permitted by the type-checker:
+intPair implements any
+
+func test() {
+    x := pair(1,2)
+    assert equal(x, x) // succeeds as `equal` is ghost
+    //:: ExpectedOutput(assert_error:assertion_error)
+    assert false
+}
+
+ghost
+decreases
+requires isComparable(a)
+pure func equal(a, b any) bool {
+    return a == b
+}

src/test/resources/regressions/features/domains/implements-interface-simple02.gobra

@@ -0,0 +1,53 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// this testcase checks whether a domain can implement a non-empty interface
+
+package ImplementsInterfaceSimple01
+
+ghost type intPair domain {
+    func fst(intPair) int
+    func snd(intPair) int
+    func pair(int, int) intPair
+
+    axiom {
+      forall p intPair :: {fst(p)}{snd(p)} p == pair(fst(p),snd(p))
+    } // pair
+
+    axiom {
+      forall l, r int :: {pair(l,r)} l == fst(pair(l,r)) && r == snd(pair(l,r))
+    }
+}
+
+type Equality interface {
+    ghost
+    pure hash() int
+
+    ghost
+    isEqual(other Equality) bool
+}
+
+// the following clause should be permitted by the type-checker as intPair implements the interface:
+intPair implements Equality
+
+ghost
+decreases
+pure func (i intPair) hash() int {
+    return 42 // best implementation of a hash function
+}
+
+ghost
+decreases
+func (i intPair) isEqual(other Equality) bool {
+    if typeOf(other) == intPair {
+        return fst(i) == fst(other.(intPair)) && snd(i) == snd(other.(intPair))
+    }
+    return false
+}
+
+func test() {
+    x := pair(1,2)
+    assert x.hash() == 42
+    //:: ExpectedOutput(assert_error:assertion_error)
+    assert false
+}