module Apps.Sudoku.Serializer;
import Apps.Sudoku.Grid open;
import Apps.Sudoku.Extra open;
import Apps.Sudoku.Validator open;
import Data.ByteString open;
import Anoma.Prelude open;
import Stdlib.Trait.Partial open;
--- Encode a Sudoku ;Grid; to a ;ByteString;
encode : Grid -> ByteString := flatten ∘ gridRows;
--- Compute the largest ;Nat; that is less than or equal to the input ;Nat;.
floorSquareRoot : Nat -> Nat
| zero := zero
| n :=
let
terminating
go (a : Nat) : Nat :=
let
b : Nat := div (a + div n a) 2;
in if (a > b) (go b) a;
in go n;
--- Partial function that computes a square root. If the input ;Nat; is not a
--- square number then fail.
checkSquareRoot {{Partial}} (n : Nat) : Nat :=
let
root : Nat := floorSquareRoot n;
in if (root * root == n) root (fail "checkSquareRoot: not a square number");
--- Decode a Sudoku ;Grid; from a ;ByteString;
decode {{Partial}} (bs : ByteString) : Grid :=
let
gridWidth : Nat := checkSquareRoot (length bs);
subGridWidth : Nat := checkSquareRoot gridWidth;
rows : List (List Nat) := chunksOf gridWidth bs;
split {A : Type} : List A -> List (List A) := chunksOf subGridWidth;
pack : List (List Nat) -> List (List (List (List Nat))) :=
split ∘ map split;
unpack : List (List (List (List Nat))) -> List (List Nat) :=
map flatten ∘ flatten;
subGrids : List (List Nat) -> List (List Nat) :=
unpack ∘ map transpose ∘ pack;
decodeSubGrid : List Nat -> SubGrid := subGrid ∘ chunksOf subGridWidth;
in grid (chunksOf subGridWidth (map decodeSubGrid (subGrids rows)));
--- Count the number of filled squares in a serialized ;Grid;
filledSquares (proposal : ByteString) : Nat :=
length (filter (square in proposal) entryFilled? square);
--- Count the number of unfilled squares in a serialized ;Grid;
emptySquares (proposal : ByteString) : Nat :=
length (filter (square in proposal) not (entryFilled? square));
Last modified on 2023-12-07 10:36 UTC