module Logic.Square;

import Stdlib.Prelude open;
import Logic.Symbol open;
import Logic.Extra open;

--- A square is each of the holes in a board
type Square :=
  | --- An empty square has a ;Nat; that uniquely identifies it
    empty : Nat → Square
  | --- An occupied square has a ;Symbol; in it
    occupied : Symbol → Square;

--- Equality for ;Square;s
==Square : Square → Square → Bool
  | (empty m) (empty n) := m == n
  | (occupied s) (occupied t) := ==Symbol s t
  | _ _ := false;

--- Textual representation of a ;Square;
showSquare : Square → String
  | (empty n) := " " ++str natToString n ++str " "
  | (occupied s) := " " ++str showSymbol s ++str " ";

replace (player : Symbol) (k : Nat) : Square → Square
  | (empty n) := ite (n == k) (occupied player) (empty n)
  | s := s;