shifted

{-
Combine a `List` of `List`s, offsetting the `index` of each element by the
number of elements in preceding lists

Examples:

```
./shifted
Bool
[   [   { index = 0, value = True  }
    ,   { index = 1, value = True  }
    ,   { index = 2, value = True  }
    ]
,   [   { index = 0, value = False }
    ,   { index = 1, value = False }
    ]
,   [   { index = 0, value = True  }
    ,   { index = 1, value = True  }
    ,   { index = 2, value = True  }
    ,   { index = 3, value = True  }
    ]
]
=   [   { index = 0, value = True  }
    ,   { index = 1, value = True  }
    ,   { index = 2, value = True  }
    ,   { index = 3, value = False }
    ,   { index = 4, value = False }
    ,   { index = 5, value = True  }
    ,   { index = 6, value = True  }
    ,   { index = 7, value = True  }
    ,   { index = 8, value = True  }
    ]

./shifted Bool ([] : List (List { index : Natural, value : Bool }))
= [] : List { index : Natural, value : Bool }
```
-}
    let shifted
        :   ∀(a : Type)
          → List (List { index : Natural, value : a })
          → List { index : Natural, value : a }
        =   λ(a : Type)
          → λ(kvss : List (List { index : Natural, value : a }))
          → List/build
            { index : Natural, value : a }
            (   λ(list : Type)
              → λ(cons : { index : Natural, value : a } → list → list)
              → λ(nil : list)
              →     let result =
                          List/fold
                          (List { index : Natural, value : a })
                          kvss
                          { count : Natural, diff : Natural → list }
                          (   λ(kvs : List { index : Natural, value : a })
                            → λ(y : { count : Natural, diff : Natural → list })
                            →     let length =
                                        List/length
                                        { index : Natural, value : a }
                                        kvs
                              
                              in  { count = y.count + length
                                  , diff  =
                                        λ(n : Natural)
                                      → List/fold
                                        { index : Natural, value : a }
                                        kvs
                                        list
                                        (   λ ( kvOld
                                              : { index : Natural, value : a }
                                              )
                                          → λ(z : list)
                                          →     let kvNew =
                                                      { index = kvOld.index + n
                                                      , value = kvOld.value
                                                      }
                                            
                                            in  cons kvNew z
                                        )
                                        (y.diff (n + length))
                                  }
                          )
                          { count = 0, diff = λ(_ : Natural) → nil }
                
                in  result.diff 0
            )

in  shifted