--- Pascal's triangle is the arrangement of binomial coefficients in a triangular array.
--- The rows of the triangle are staggered so that each number can be computed as the
--- sum of the numbers to the left and right in the previous row.
--- The function ;pascal; produces the triangle to a given depth.
module PascalsTriangle;

open import Stdlib.Prelude;

--- Return a list of repeated applications of a given function
scanIterate : {A : Type} → Nat → (A → A) → A → List A;
scanIterate zero _ _ := nil;
scanIterate (suc n) f a := a :: scanIterate n f (f a);

--- Produce a singleton List
singleton : {A : Type} → A → List A;
singleton a := a :: nil;

--- Concatenates a list of strings
--- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a" :: "b" :: nil;
concat : List String → String;
concat := foldl (++str) "";

intercalate : String → List String → String;
intercalate sep xs := concat (intersperse sep xs);

showList : List Nat → String;
showList xs := "[" ++str intercalate "," (map natToString xs) ++str "]";

--- Compute the next row of Pascal's triangle
pascalNextRow : List Nat → List Nat;
pascalNextRow row :=
  zipWith (+) (singleton zero ++ row) (row ++ singleton zero);

--- Produce Pascal's triangle to a given depth
pascal : Nat → List (List Nat);
pascal rows := scanIterate rows pascalNextRow (singleton 1);

main : IO;
main := printStringLn (unlines (map showList (pascal 10)));