/// m12 check: property-based testing built from the course's own parts.
/// A generator of test data is nothing new: it is a `Random<'a>` from Random.fs (`seed -> (value, nextSeed)`).
module Snake.Check

open Snake.Model
open Snake.Random

/// What `forAll` reports: every value passed, or the first one that did not.
type CheckResult<'a> =
    | Passed of runs: int
    | Failed of run: int * seed: uint32 * value: 'a

/// One of the elements of the non-empty list `xs`: the one at index `intBelow (List.length xs)`.
let elementOf (xs: 'a list) : Random<'a> =
    Random.intBelow (List.length xs) |> Random.map (fun i -> List.item i xs)

/// `n` values drawn from `gen`, one after another; the seed is threaded from each draw to the next.
let rec listOf (n: int) (gen: Random<'a>) : Random<'a list> =
    if n <= 0 then
        Random.pure []
    else
        gen |> Random.bind (fun a -> listOf (n - 1) gen |> Random.map (fun rest -> a :: rest))

// Ticks appear three times so that the snake moves more often than it turns.
let private actionPool: Action list =
    [ Tick; Tick; Tick; Turn Up; Turn Down; Turn Left; Turn Right ]

/// A generator of `n` random actions (given).
let genActions (n: int) : Random<Action list> = listOf n (elementOf actionPool)

/// Check `prop` on `runs` values drawn from `gen`, starting from `seed`; stop at the first value that fails.
/// Recursion carries the seed: no counter, no loop variable. `go` calls itself last, so it runs in constant stack.
let forAll (runs: int) (seed: uint32) (prop: 'a -> bool) (gen: Random<'a>) : CheckResult<'a> =
    let rec go (i: int) (s: uint32) : CheckResult<'a> =
        if i >= runs then
            Passed runs
        else
            let value, next = Random.run s gen
            if prop value then go (i + 1) next else Failed(i, s, value)

    go 0 seed

/// Every list that is `xs` with exactly one element removed, in the order of the removed index.
let removals (xs: 'a list) : 'a list list = xs |> List.mapi (fun i _ -> List.removeAt i xs)

/// Keep removing one element for as long as the list still fails; the result is 1-minimal.
let rec minimize (fails: 'a list -> bool) (xs: 'a list) : 'a list =
    match List.tryFind fails (removals xs) with
    | Some smaller -> minimize fails smaller
    | None -> xs

let private neighbours (a: Point, b: Point) : bool = abs (a.X - b.X) + abs (a.Y - b.Y) = 1

let rec private allDifferent (ps: Point list) : bool =
    match ps with
    | [] -> true
    | p :: rest -> not (Util.contains rest p (=)) && allDifferent rest

// Each invariant: its name, and a predicate that is true when the state is fine.
// `Option.forall` is true for `None`: no apple breaks nothing.
let private invariants: (string * (GameState -> bool)) list =
    [ "snake-not-empty", (fun s -> not (List.isEmpty s.Snake))
      "snake-in-bounds", (fun s -> s.Snake |> List.forall (Rules.inBounds s))
      "snake-no-overlap", (fun s -> allDifferent s.Snake)
      "snake-connected", (fun s -> s.Snake |> List.pairwise |> List.forall neighbours)
      "apple-in-bounds", (fun s -> s.Apple |> Option.forall (Rules.inBounds s))
      "apple-not-on-snake", (fun s -> s.Apple |> Option.forall (fun a -> not (Util.contains s.Snake a (=))))
      "turn-not-reversed", (fun s -> s.NextDir <> opposite s.Dir)
      "queued-not-reversed", (fun s -> s.Queued |> Option.forall (fun q -> q <> opposite s.NextDir)) ]

/// The names of the invariants that `state` breaks, in the order of the table above.
let violations (state: GameState) : string list =
    invariants |> List.filter (fun (_, holds) -> not (holds state)) |> List.map fst

/// The numbers of states between consecutive moves of the snake's head.
let moveGaps (states: GameState list) : int list =
    let moved =
        states
        |> List.pairwise
        |> List.indexed
        |> List.filter (fun (_, (before, after)) -> List.tryHead after.Snake <> List.tryHead before.Snake)
        |> List.map (fun (i, _) -> i + 1)

    moved |> List.pairwise |> List.map (fun (a, b) -> b - a)

// ---- random states (Exercise 12.6) and a second implementation of the step as an oracle (Exercise 12.7)

let private directions: Direction list = [ Up; Down; Left; Right ]

// The direction the head moved in to get from the second cell to the first (`Right` for a one-cell snake).
let private headingOf (snake: Point list) : Direction =
    match snake with
    | head :: second :: _ -> directions |> List.find (fun d -> Rules.move second d = head)
    | _ -> Right

/// A random snake, head first: a random head, then a random walk that never leaves the board or crosses itself.
let genSnake (width: int) (height: int) (maxLen: int) : Random<Point list> =
    // Extend `snake` at its tail by up to `left` more cells, each a random free in-bounds neighbour of the last cell.
    let rec grow (snake: Point list) (left: int) : Random<Point list> =
        if left <= 0 then
            Random.pure snake
        else
            let last = List.last snake

            let options =
                directions
                |> List.map (Rules.move last)
                |> List.filter (fun p ->
                    p.X >= 0 && p.X < width && p.Y >= 0 && p.Y < height && not (Util.contains snake p (=)))

            if List.isEmpty options then
                Random.pure snake
            else
                elementOf options |> Random.bind (fun p -> grow (snake @ [ p ]) (left - 1))

    Random.intBelow width
    |> Random.bind (fun x -> Random.intBelow height |> Random.bind (fun y -> grow [ { X = x; Y = y } ] (maxLen - 1)))

/// A random sane Playing state on a `width` x `height` board (given).
let genState (width: int) (height: int) : Random<GameState> =
    Random.intBelow (width * height)
    |> Random.bind (fun n ->
        genSnake width height (n + 1)
        |> Random.bind (fun snake ->
            let dir = headingOf snake

            let state =
                { Width = width
                  Height = height
                  Snake = snake
                  Dir = dir
                  NextDir = dir
                  Apple = None
                  Seed = 0u
                  Score = 0
                  Status = Playing
                  Frame = 0
                  Queued = None }

            let free = Spawn.freeCells state

            elementOf (directions |> List.filter (fun d -> d <> opposite dir))
            |> Random.bind (fun nextDir ->
                Random.intBelow 2
                |> Random.bind (fun coin ->
                    (if coin = 0 || List.isEmpty free then Random.pure None else elementOf free |> Random.map Some)
                    |> Random.map (fun apple -> { state with NextDir = nextDir; Apple = apple })))))

/// The step of m03, written from the rules instead of from `advance`: build the snake the step would give,
/// then ask `violations` whether that snake is on the board and does not overlap itself.
let advanceSpec (state: GameState) : GameState =
    if state.Status <> Playing then
        state
    else
        let head = Rules.move (List.head state.Snake) state.NextDir
        let eating = state.Apple = Some head
        let snake = head :: (if eating then state.Snake else Util.dropLast state.Snake)

        let broken =
            violations { state with Snake = snake }
            |> List.exists (fun v -> v = "snake-in-bounds" || v = "snake-no-overlap")

        if broken then
            { state with Dir = state.NextDir; Status = GameOver }
        else
            { state with
                Snake = snake
                Dir = state.NextDir
                Apple = if eating then None else state.Apple
                Score = state.Score + (if eating then 1 else 0) }