cc2.scala

object CC {
  def connectedComponent(board: Board, color: Cell, toVisit: List[Point], component: List[Point] = List[Point]()): List[Point] = {
    require(board.isValid &&
      board.isValidPoints(toVisit) &&
      board.isValidPoints(component) &&
      isComponent(board, addValidElements(board, component, toVisit), color)
    )
    if (toVisit.isEmpty)
      component
    else if (component.contains(toVisit.head))
      connectedComponent(board, color, toVisit.tail, component)
    else {
      val p = toVisit.head
      val newComponent = addToComponent(board, component, p, color)
      val newNeighbors = board.sameColorNeighborPoints(p, color)
      val newToVisit = addValidElements(board, toVisit.tail, newNeighbors)
      connectedComponent(board, color, newToVisit, newComponent)
    }
  } ensuring { res =>
    isComponent(board, res, color)
  }
  def isComponent(board: Board, lst: List[Point], color: Cell): Boolean = {
    require(board.isValid)
    if (lst.isEmpty) true
    else
      board.isValidPoints(lst)
    // lst.forall(a => lst.forall(b => board.isConnected(PlacedCell(a, color), PlacedCell(b, color))))
  }
  def addToComponent(board: Board, lst: List[Point], e: Point, color: Cell): List[Point] = {
    require(
      board.isValid &&
        isComponent(board, lst, color) &&
        board.isValidPoints(lst) &&
        board.insideBoard(e)
    )

    e :: lst
  } ensuring { res =>
    isComponent(board, res, color) && res.content == (e :: lst).content
  }

  def addValidElements(board: Board, a: List[Point], b: List[Point]): List[Point] = {
    require(
      board.isValid &&
        board.isValidPoints(a) &&
        board.isValidPoints(b)
    )
    if (a.isEmpty) b
    else addValidElements(board, a.tail, a.head :: b)
  } ensuring { res =>
    board.isValidPoints(res) && res.content == (a ++ b).content
  }
}