--- 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;

import Stdlib.Prelude open;

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

--- Produce a singleton List
singleton {A} (value : A) : List A := value :: nil;

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

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

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

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

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

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