Skip to content

Instantly share code, notes, and snippets.

@JadenGeller

JadenGeller/Spiral.idr

Last active October 7, 2017 05:39
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save JadenGeller/566a0c75ae1effc944af325b9a30d570 to your computer and use it in GitHub Desktop.
Save JadenGeller/566a0c75ae1effc944af325b9a30d570 to your computer and use it in GitHub Desktop.
Download ZIP
Idris Spiral
Raw
Spiral.idr
import Data.Vect
Matrix : Nat -> Nat -> Type -> Type
Matrix r c a = Vect r (Vect c a)
unrotate : Matrix r c a -> Matrix c r a
unrotate = reverse . transpose
spiral : Matrix r c a -> Vect (r * c) a
spiral {r=Z} [] = []
spiral {r=S r'} {c} (row :: rows) = let rest : Vect (r' * c) a = rewrite multCommutative r' c
in spiral (unrotate rows)
in row ++ rest
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment