module Apps.Sudoku.Grid;

import Anoma.Prelude open;
import Data.ByteString open;
import Apps.Sudoku.Extra open;

--- A Sudoku subgrid
type SubGrid := subGrid : List (List Nat) -> SubGrid;

subGridEntries : SubGrid -> List Nat
  | (subGrid rows) := flatten rows;

--- The rows of ;SubGrid;s that comprise a Sudoku grid.
type Grid := grid : List (List SubGrid) -> Grid;

gridEntries : Grid -> List Nat
  | (grid sgs) := flatten (concatMap (map subGridEntries) sgs);

gridRows : Grid -> List (List Nat)
  | (grid rows) :=
    let
      combineSubGridRows (rs1 : List (List Nat)) (sg : SubGrid)
        : List (List Nat) := case sg of {subGrid rs2 := zipWith (++) rs1 rs2};
      combineRows : List SubGrid -> List (List Nat)
        | nil := nil
        | (subGrid rs :: sgs) :=
          for (acc := rs) (sg in sgs)
            combineSubGridRows acc sg;
    in concatMap combineRows rows;

instance
gridEq : Eq Grid := mkEq λ {g1 g2 := gridRows g1 == gridRows g2};

prettyGrid : Grid -> String
  | g@(grid (sg@(subGrid (r :: _) :: _) :: _)) :=
    let
      subGridWidth : Nat := length r;
      numSubGrids : Nat := length sg;
      showSquare : Nat -> String
        | zero := "   "
        | n := " " ++str Show.show n ++str " ";
      showSplitRow : List Nat -> String := concatStr ∘ map showSquare;
      showRow (subGridWith : Nat) (xs : List Nat) : String :=
        concatStr (surround "|" (map showSplitRow (chunksOf subGridWidth xs)));
      showRowChunk (subGridWidth : Nat) (xs : List (List Nat)) : String :=
        unlines (map (showRow subGridWidth) xs);
    in case gridRows g of {
         | nil := ""
         | xs@(x :: _) :=
           let
             oneSquareWidth : Nat := 3;
             borderOneSubgrid : String :=
               concatStr (replicate (oneSquareWidth * subGridWidth) "-")
                 ++str "+";
             border : String :=
               "+" ++str concatStr (replicate numSubGrids borderOneSubgrid);
           in unlines
             (surround
               border
               (map (showRowChunk subGridWidth) (chunksOf subGridWidth xs)))
       }
  | _ := "";