a dependently typed nonogram solver algorithm (wip)

nono.idr

module nono

import Data.Vect

mutual
    data Descriptor : Nat -> Type where
        Nil : Descriptor n
        (::) : (k : Nat) -> (d : Descriptor n) -> Descriptor (k + n + isNotEmpty d)

    isNotEmpty : Descriptor n -> Nat
    isNotEmpty [] = 0
    isNotEmpty (_::_) = 1

record Puzzle (n : Nat) (m: Nat) where
    constructor MkPuzzle
    rows : Vect n (Descriptor m)
    columns : Vect m (Descriptor n)

Board : (n, m : Nat) -> Type
Board n m = Vect n (Vect m Bool)

row : Fin n -> Board n m -> Vect m Bool
row = index

column : Fin m -> Board n m -> Vect n Bool
column = map . index

data Chunks : Vect n Bool -> Type where
    End : Chunks []
    Filled : (k : Nat) -> Chunks xs -> Chunks (replicate k True ++ xs)
    Blank : Chunks xs -> Chunks (False :: xs)

chunks : (xs : Vect n Bool) -> Chunks xs
chunks [] = End
chunks (False :: xs) = Blank (chunks xs)
chunks (True :: xs) = 
    case chunks xs of
        (Filled k cs) => Filled (S k) cs
        cs => Filled 1 cs

data Matches : Chunks xs -> Descriptor n -> Type where
    Done : Matches End []
    Skip : Matches cs d -> Matches (Blank cs) d
    Chunk : Matches cs d -> Matches (Filled k cs) (k :: d)

endCantMatchSome : Matches End (k :: d) -> Void
endCantMatchSome Done impossible
endCantMatchSome (Skip _) impossible
endCantMatchSome (Chunk _) impossible

filledCantMatchNone : Matches (Filled k x) [] -> Void
filledCantMatchNone Done impossible
filledCantMatchNone (Skip _) impossible
filledCantMatchNone (Chunk _) impossible

matchChunks : (cs : Chunks xs) -> (d : Descriptor n) -> Dec (Matches cs d)
matchChunks End [] = Yes Done
matchChunks End (k :: d) = No endCantMatchSome
matchChunks (Blank x) d = 
    case matchChunks x d of
        (Yes prf) => Yes (Skip prf)
        (No contra) => No (\(Skip prf) => contra prf)
matchChunks (Filled k x) [] = No filledCantMatchNone
matchChunks (Filled k x) (j :: d) with (decEq k j)
  matchChunks (Filled j x) (j :: d) | (Yes Refl) = 
    case matchChunks x d of
        (Yes prf) => Yes (Chunk prf)
        (No contra) => No (\(Chunk prf) => contra prf)
  matchChunks (Filled k x) (j :: d) | (No contra) = No (\(Chunk prf) => contra Refl)
    
matches : (xs : Vect n Bool) -> (d : Descriptor n) -> Dec (Matches (chunks xs) d)
matches xs d = matchChunks (chunks xs) d

data Solves : (b : Board n m) -> (p : Puzzle n m) -> Type where
    Solution : 
        (rowsMatch : (i : Fin n) -> Matches (chunks (row i b)) (index i (rows p))) ->
        (columnsMatch : (i : Fin m) -> Matches (chunks (column i b)) (index i (columns p))) ->
        Solves b p

unwrap : {P : Fin n -> Type} -> ((i : Fin n) -> Dec (P i)) -> Dec ((i : Fin n) -> (P i))
unwrap {n = Z} f = Yes (\x => absurd x)
unwrap {n = (S k)} {P=P} f = 
    case unwrap {P = P . FS} (\x => f (FS x)) of
        (Yes prfS) => 
            case f FZ of
                (Yes prfZ) => Yes (\x => 
                    case x of 
                        FZ => prfZ
                        (FS i) => prfS i)
                (No contra) => No (\g => contra (g FZ))
        (No contra) => No (\g => contra (\x => g (FS x)))

decSolves : (b : Board n m) -> (p : Puzzle n m) -> Dec (b `Solves` p)
decSolves b p = 
    case decRowsMatch of
        (Yes prf1) => 
        case decColumnsMatch of
            (Yes prf2) => Yes (Solution prf1 prf2)
            (No contra) => No (\(Solution _ prf) => contra prf)
        (No contra) => No (\(Solution prf _) => contra prf)
where
    rowMatches : (i : Fin n) -> Dec (Matches (chunks (row i b)) (index i (rows p)))
    rowMatches i = matches (row i b) (index i (rows p))
    columnMatches : (i : Fin m) -> Dec ( Matches (chunks (column i b)) (index i (columns p)))
    columnMatches i = matches (column i b) (index i (columns p))
    decRowsMatch : Dec ((i : Fin n) -> Matches (chunks (row i b)) (index i (rows p)))
    decRowsMatch = unwrap rowMatches {P = \i => Matches (chunks (row i b)) (index i (rows p))}
    decColumnsMatch : Dec ((i : Fin m) -> Matches (chunks (column i b)) (index i (columns p)))
    decColumnsMatch = unwrap columnMatches {P = \i =>  Matches (chunks (column i b)) (index i (columns p))}