pyramid.idr

module Main

forLoop : List a -> (a -> IO ()) -> IO ()
forLoop [] f = return ()
forLoop (x :: xs) f = do f x
                         forLoop xs f

syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)

spaces : Nat -> String
spaces Z = ""
spaces (S k) = strCons ' ' (spaces k)

charAt : String -> Nat -> Char
charAt s Z = strHead s
charAt s (S k) = charAt (strTail s) k

modulo : Nat -> (n : Nat) -> Fin n
modulo Z (S b) = fZ {k=b}
modulo (S k) (S b) = if k >= b
  then modulo ((S k) - (S b)) (S b)
  else fS (modulo k b)

brickAt : String -> Nat -> Char
brickAt bricks idx = index boundedIdx sized
  where
    unpacked : List Char
    unpacked = unpack bricks
    len : Nat
    len = length unpacked
    sized : Vect (length unpacked) Char
    sized = fromList unpacked
    boundedIdx : Fin len
    boundedIdx = modulo idx len

row : Nat -> String -> Nat -> String
row height bricks i = (spaces width) ++ lefts ++ rights
  where
    width : Nat
    width = (height - i)

    lefts : String
    lefts = pack (map (brickAt bricks) (reverse [1..i]))

    rights: String
    rights = pack (map (brickAt bricks) [0..i])

pyramid : String -> Nat -> IO ()
pyramid bricks height =
  do for i in [0..height]:
    putStrLn $ row height bricks i

main : IO ()
main = do
  putStr "Bricks: "
  bricks <- getLine
  putStr "Height: "
  heightStr <- getLine
  let height : Integer = cast heightStr
  pyramid (trim bricks) (fromInteger height)