-- -*- idris-interpreter-flags: ("-p" "contrib") -*-

import Data.ZZ
import Data.Vect

data CountChange : ZZ -> Vect n ZZ -> Type where
     C1  : CountChange 0 k        -- 1 way
     C0a : CountChange (NegS a) k -- 0 ways
     C0b : CountChange a []       -- 0 ways
     CC  : CountChange (a - (head k)) k -> CountChange a (tail k) -> CountChange a k -- x + y ways

count : CountChange x y -> Nat
count C1       = 1
count C0a      = 0
count C0b      = 0
count (CC x y) = count x + count y

cc_2_by_1 : CountChange 2 [1]
cc_2_by_1 = CC (CC C1 C0b) C0b

cc_2_by_2_1 : CountChange 2 [2,1]
cc_2_by_2_1 = CC C1 (CC (CC C1 C0b) C0b)

cc_11_by_50_25_10_5_1 : CountChange 11 [50,25,10,5,1] 
cc_11_by_50_25_10_5_1 = ?try_it
{- ex 1.14 'tree', generated by 'C-c-a'
cc_11_by_50_25_10_5_1 = CC
                          C0a
                          (CC
                            C0a
                            (CC
                              (CC
                                C0a
                                (CC
                                  C0a
                                  (CC
                                    C1
                                    C0b
                                  )
                                )
                              )
                              (CC
                                (CC
                                  (CC
                                    C0a
                                    (CC
                                      C1
                                      C0b
                                    )
                                  )
                                  (CC
                                    (CC
                                      (CC
                                        (CC
                                          (CC
                                            (CC
                                              C1
                                              C0b
                                            )
                                            C0b
                                          )
                                          C0b
                                        )
                                        C0b
                                      )
                                      C0b
                                    )
                                    C0b
                                  )
                                )
                                (CC
                                  (CC
                                    (CC
                                      (CC
                                        (CC
                                          (CC
                                            (CC
                                              (CC
                                                (CC
                                                  (CC
                                                    (CC
                                                      C1
                                                      C0b
                                                    )
                                                    C0b
                                                  )
                                                  C0b
                                                )
                                                C0b
                                              )
                                              C0b
                                            )
                                            C0b
                                          )
                                          C0b
                                        )
                                        C0b
                                      )
                                      C0b
                                    )
                                    C0b
                                  )
                                  C0b
                                )
                              )
                            )
                          )
-}
