[SOLVED] Dafny: Generic method on a base type and a subset type?

Dafny: Generic method on a base type and a subset type?

Can I define a generic method on a base type and subset type?

For example, we might later use the generic function by having

T0 be the sets of integers, and
T1 be the non-empty sets of integers

I image something like:

method MergeAndTouch<T0, T1>(Touch: (T1,T1)->bool, Plus: (T0,T0)->T0, unit: T0, xs: seq<T1>, a: T1)
  requires T0 >= T1 // NOT ALLOWED
  requires Reflexive(Touch)
  requires Symmetric(Touch)
  requires IsAssociative(Plus)
  requires IsUnital(Plus, unit)
  requires forall i:T1, j:T1 :: Touch(Plus(i, j), i) && Touch(Plus(i, j), j)
  requires forall i:nat, j:nat :: i < j < |xs| ==> !Touch(xs[i], xs[j])
{
// code goes here
}

I need this to exclude things like the empty set from the generic Touch while still having things like the empty set as the unit for operations such as FoldLeft.

Solution

In this case subset language feature can be used. This is how it will look like

ghost function NonEmptySetExample<T(00)>() : (r: set<T>)
{
    var t : T :| true ; {t}
}

type NonEmptySet<T(00)> = s : set<T> |  s != {} 
     ghost witness NonEmptySetExample<T>()

You can use set methods (in here) on NonEmptySet.

ghost function Test<T(00)>(t: NonEmptySet<T>) : T 
{
    var x : T :| x in t; x
}

Additionally you can define method taking set as argument and call with NonEmptySet

method TypeMethod<T>(s: set<T>) 
{
}

method CallTypeMethodOnSubSet<T(00)>(t: NonEmptySet<T>)
{
   TypeMethod(t);
}

Note: T(00) means type parameter itself is non empty.