// This problem set is about practing with loops, so we're going to impose an
// extra rule: no method that we ask you to write should execute a recursive
// call, whether in a method or a function.  You'll want to make use of
// recursive functions in *specifying* and *proving* methods, but those
// functions should only appear in ghost code, present only for verification
// purposes.

// As usual, check out a few definitions we'll appeal to below.  The file also
// proves some lemmas that we found useful in our solution, but you aren't
// required to use them.
include "pset09_definitions.dfy"

module Pset9 {
  import opened Defs

  // Write and verify a loop-based list reverse.
  method ReverseLoop<X>(xs: List<X>) returns (ys: List<X>)
    ensures ys == Reverse(xs)

  // Write and verify a method for splitting a list into two others, alternating
  // placement of original elements in each.  Consulting the definition of Zip
  // in pset09_definitions.dfy is actually the easiest way to see the fully
  // rigorous requirements.
  method Split<X>(ws: List<X>) returns (xs: List<X>, ys: List<X>)
    requires Length(ws) % 2 == 0
    ensures ws == Zip(xs, ys)
    ensures Length(xs) == Length(ys)

  // This function finds the position within a sequence that contains a
  // particular value.  Add loop annotations to make it pass verification.
  method FindExistingElement0<X(==)>(s: seq<X>, key: X) returns (i: int)
    requires exists j :: 0 <= j < |s| && s[j] == key
    ensures 0 <= i < |s| && s[i] == key
  {
    i := 0;
    while true
    {
      if s[i] == key {
        return i;
      }
      i := i + 1;
    }
  }

  // This variant achieves a simpler postcondition by requiring that the
  // sequence is duplicate-free.  Add loop annotations to make it pass
  // verification.
  method FindExistingElement1<X(==)>(s: seq<X>, key: X, ghost j: int) returns (i: int)
    requires forall m, n :: 0 <= m < n < |s| ==> s[m] != s[n] // s has no duplicates
    requires 0 <= j < |s| && s[j] == key
    ensures i == j
  {
    i := 0;
    while true
    {
      if s[i] == key {
        return i;
      }
      i := i + 1;
    }
  }

  // Implement and verify this checker for whether repeatedly applying 'f' to
  // 'start' eventually takes us back around to a duplicate value, before we run
  // out of elements of 's'.
  method ComputeIsClosed<X>(f: X -> X, start: X, s: set<X>) returns (closed: bool)
    ensures closed == IsClosed(f, start, s)
}