vecs.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

import Data.Bitraversable (bisequence)
import Data.Kind (Type)
import Data.Type.Equality ((:~:) (..))
import Numeric.Natural (Natural)

-- peano naturals
data Nat = Zero | Succ Nat

-- get type information from terms
-- every term in SNat corresponds to *exactly* one type from Nat
-- called singletons
data SNat (n :: Nat) where
  SZero :: SNat Zero
  SSucc :: SNat n -> SNat (Succ n)

-- lists that know their length
data Vec a (n :: Nat) where
  -- the empty list has length zero
  Nil :: Vec a Zero
  -- consing to a list increases its length by one
  (:::) :: a -> Vec a n -> Vec a (Succ n)

-- so we can chain conses like normal lists
infixr 5 :::

-- so we can print Vecs
deriving instance Show a => Show (Vec a n)

-- a nxm sized image with pixels of type a
type Image a n m = Vec (Vec a m) n

-- create a vector with the given size and the given elements
-- analoguous to replicate, but with type info
replicateV :: SNat n -> a -> Vec a n
replicateV SZero _ = Nil
replicateV (SSucc n) x = x ::: replicateV n x

-- an example way to make an image
-- create an entirely black image of the given dimensions
black :: SNat n -> SNat m -> Image Float n m
black n m = replicateV n $ replicateV m 0

type Rgb = (Float, Float, Float)

-- witness of < for peano naturals
-- this also happens to be a singleton for n, so we can use it as such
data (<) n m where
  -- zero < 1 + anything
  LZero :: Zero < Succ m
  -- if n <= m then 1 + n < 1 + m
  LSucc :: n < m -> Succ n < Succ m

-- safe indexing, to be used in e.g. floodFill
-- notice that we don't need a match for
-- index LZero Nil
-- because the compiler can check that it's impossible:
-- if (n < m) is actually LZero, that means that
-- n == Zero, m == Succ m'
-- so our Vec a m is actually Vec a (Succ m')
-- meaning that it necessarily has the form (x ::: _)
-- (because that's the only constructor of Vec that fits)
-- same reasoning is valid for why we don't need a (LSucc _) Nil match
index :: n < m -> Vec a m -> a
index LZero (x ::: _) = x
index (LSucc p) (_ ::: xs) = index p xs

-- we can't call this function unless the given coordinates are "inside" our image
-- we don't need to also give SNat n0 and SNat m0, because we can "abuse" the fact
-- that each term in (<) uniquely determines a natural number (LZero is 0, LSucc is +1)
floodFill ::
  Rgb ->
  n0 < n1 ->
  m0 < m1 ->
  Image Rgb n1 m1 ->
  Image Rgb n1 m1
floodFill = error "implement algorithm for flood filling.."

two = SSucc $ SSucc SZero

three = SSucc two

main :: IO ()
main = do
  MkSNat n <- toSomeSNat <$> readLn @Natural
  MkSNat m <- toSomeSNat <$> readLn @Natural
  xss <- read @[[Rgb]] <$> readFile "pesho.kartinka"
  case toSomeImage xss of
    Nothing -> putStrLn "Не всичките редове на картинката са с равна дължина!"
    Just (MkImage xss') -> do
      case decideInside n m xss' of
        Nothing -> putStrLn "Въведените координати не са валидни!"
        Just (nIn, mIn) -> do
          let xss'' = floodFill (0, 0, 0) nIn mIn xss'
          writeFile "pesho.kartinka.nova" $ show $ map forgetLength $ forgetLength xss''

data SomeSNat where
  MkSNat :: SNat n -> SomeSNat

toSomeSNat :: Natural -> SomeSNat
toSomeSNat 0 = MkSNat SZero
toSomeSNat n = case toSomeSNat (n - 1) of MkSNat n' -> MkSNat $ SSucc n'

withSomeSNat :: Natural -> (forall n. SNat n -> r) -> r
withSomeSNat n f = case toSomeSNat n of MkSNat n' -> f n'

data SomeVec a where
  MkVec :: Vec a n -> SomeVec a

toSomeVec :: [a] -> SomeVec a
toSomeVec [] = MkVec Nil
toSomeVec (x : xs) = case toSomeVec xs of MkVec van -> MkVec $ x ::: van

withSomeVec :: [a] -> (forall n. Vec a n -> r) -> r
withSomeVec xs f = case toSomeVec xs of MkVec xs' -> f xs'

data SomeImage a where
  MkImage :: Image a n m -> SomeImage a

class NatSing (snat :: Nat -> Type) where
  toSNat :: snat n -> SNat n

instance NatSing SNat where
  toSNat = id

instance NatSing (Vec a) where
  toSNat = forgetElems

decideNatEq :: (NatSing sn, NatSing sm) => sn n -> sm m -> Maybe (n :~: m)
decideNatEq sn sm = decideNatEq' (toSNat sn) (toSNat sm)
  where
    decideNatEq' :: SNat n -> SNat m -> Maybe (n :~: m)
    decideNatEq' SZero SZero = Just Refl
    decideNatEq' (SSucc n) (SSucc m) =
      case decideNatEq' n m of
        Just Refl -> Just Refl
        Nothing -> Nothing
    decideNatEq' _ _ = Nothing

forgetElems :: Vec a n -> SNat n
forgetElems Nil = SZero
forgetElems (_ ::: xs) = SSucc $ forgetElems xs

vecMap :: (a -> b) -> Vec a n -> Vec b n
vecMap _ Nil = Nil
vecMap f (x ::: xs) = f x ::: vecMap f xs

toSomeImage :: [[a]] -> Maybe (SomeImage a)
toSomeImage [] = Just $ MkImage Nil
toSomeImage (xs : xss) =
  withSomeVec xs \xs' -> do
    xss' <- go (forgetElems xs') xss
    Just $ withSomeVec (xs' : xss') MkImage
  where
    go :: SNat n -> [[a]] -> Maybe [Vec a n]
    go _ [] = Just []
    go sn (ys : yss) =
      withSomeVec ys \ys' -> do
        yss' <- go sn yss
        Refl <- decideNatEq sn ys'
        Just $ ys' : yss'

withSomeImage :: [[a]] -> (forall n m. Image a n m -> r) -> Maybe r
withSomeImage xss f = (\(MkImage xss') -> f xss') <$> toSomeImage xss

forgetLength :: Vec a n -> [a]
forgetLength Nil = []
forgetLength (x ::: xs) = x : forgetLength xs

decideLt :: (NatSing sn0, NatSing sn1) => sn0 n -> sn1 m -> Maybe (n < m)
decideLt sn sm = decideLt' (toSNat sn) (toSNat sm)
  where
    decideLt' :: SNat n -> SNat m -> Maybe (n < m)
    decideLt' _ SZero = Nothing
    decideLt' SZero (SSucc _) = Just LZero
    decideLt' (SSucc n) (SSucc m) = LSucc <$> decideLt' n m

decideInside :: SNat n -> SNat m -> Image a n1 m1 -> Maybe (n < n1, m < m1)
decideInside _ _ Nil = Nothing
decideInside n m img@(xs ::: _) = bisequence (decideLt n img, decideLt m xs)