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