// tip enumerare
datatype Dow = Mon | Tue | Wed | Thu | Fri | Sat | Sun
{
  function asIndex() : int
  {
    match this
    {
    case Mon => 0
    case Tue => 1
    case Wed => 2
    case Thu => 3
    case Fri => 4
    case Sat => 5
    case Sun => 6
    }
  }
}

method testMe(dow : Dow)
{
  var r := dow.asIndex();
}

// datatype MaybeDow = Nothing | Just(dow : Dow)

datatype Maybe<T> = Nothing | Just(t : T)

function toDowMaybe(index : int) : Maybe<Dow>
{
  match index {
    case 0 => Just(Mon)
    case 1 => Just(Tue)
    case 2 => Just(Wed)
    case 3 => Just(Thu)
    case 4 => Just(Fri)
    case 5 => Just(Sat)
    case 6 => Just(Sun)
    case _ => Nothing
  }
}

function toIndex(dow : Dow) : int
{
  match dow {
    case Mon => 0
    case Tue => 1
    case Wed => 2
    case Thu => 3
    case Fri => 4
    case Sat => 5
    case Sun => 6
  }
}

predicate isWeekend(dow : Dow)
{
  match dow {
    case Sat => true
    case Sun => true
    case _ => false
  }
}

predicate isWeekend1(dow : Dow)
{
  dow.Sat? || dow.Sun?
}

function toDow(index : int) : Dow
  requires 0 <= index < 7
{
  match index {
    case 0 => Mon
    case 1 => Tue
    case 2 => Wed
    case 3 => Thu
    case 4 => Fri
    case 5 => Sat
    case 6 => Sun
  }
}

method Main()
{
  //var r := toDow(8);
  var r := toDow(6);
  print r;
}