Skip to content

Generic domain function application needs trivial type variable map with uninsightful error message #733

Open
@nilscrm

Description

@nilscrm

If one wants to create a simple generic domain to represent an option type, one could use this (simplified) example:

domain Option[T]  {

  function none_val(): Option[T]

  function some_of(x: T): Option[T]

  axiom {
    (forall x: T :: { some_of(x) } some_of(x) != none_val())
  }
}

This works perfectly fine in VS Code, however, when one want to implement this in Silver, troubles can occur.
The generic function call some_of(x) can be modeled as

vpr.DomainFuncApp(someOf, Seq(vpr.LocalVar("x", T)()), Map.empty)()

This code, however, throws an exception:

java.lang.Exception: Internal error in type system - unexpected non-ground type <T>

It is non-obvious from this error that the actual problem is the empty type variable map. Even in the generic case where you want to keep the generic type T a type variable map from T to T needs to be specified like this:

vpr.DomainFuncApp(someOf, Seq(vpr.LocalVar("x", T)()), Map(T -> T))()

Two possible solution might be to either have a default value for the type variable map or to make the error message clearer.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions