dhall-1.3.0: Prelude/List/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  }
        ]   : List { index : Natural, value : Bool }
    ,   [   { index = +0, value = False }
        ,   { index = +1, value = False }
        ]   : List { index : Natural, value : Bool }
    ,   [   { index = +0, value = True  }
        ,   { index = +1, value = True  }
        ,   { index = +2, value = True  }
        ,   { index = +3, value = True  }
        ]   : List { index : Natural, value : Bool }
    ]   : List (List { index : Natural, value : Bool })
)
=   [   { 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  }
    ]   : List { index : Natural, value : Bool }

./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