60 lines
2 KiB
Text
60 lines
2 KiB
Text
λ(nix : ../NixPrelude.dhall) →
|
|
let Any = ../Any/Type.dhall
|
|
|
|
let lessThan =
|
|
https://prelude.dhall-lang.org/Natural/lessThan.dhall
|
|
sha256:3381b66749290769badf8855d8a3f4af62e8de52d1364d838a9d1e20c94fa70c
|
|
|
|
let greaterThanEqual =
|
|
https://prelude.dhall-lang.org/Natural/greaterThanEqual.dhall
|
|
sha256:30ebfab0febd7aa0ccccfdf3dc36ee6d50f0117f35dd4a9b034750b7e885a1a4
|
|
|
|
let subtract =
|
|
https://prelude.dhall-lang.org/Natural/subtract.dhall
|
|
sha256:b9277ac637d09142a3a3ac79137ef5955c42f8b33b6746d59db2c9d75ccdd745
|
|
|
|
let Any/toAny = ../Any/toAny.dhall nix
|
|
|
|
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
|
|
|
|
let divide = ./divide.dhall nix
|
|
|
|
let throwIfNot = ../Misc/throwIfNot.dhall nix
|
|
|
|
let toBaseDigits
|
|
: Natural → Natural → List Natural
|
|
= λ(base : Natural) →
|
|
λ(i : Natural) →
|
|
let FunctionType = λ(x : Type) → x → Natural → List Natural
|
|
|
|
let function =
|
|
λ(function : FunctionType Any) →
|
|
let functionArgs =
|
|
Any/toTypeUnchecked
|
|
(FunctionType (FunctionType Any))
|
|
(Any/toAny (FunctionType Any) function)
|
|
function
|
|
|
|
in λ(i : Natural) →
|
|
if lessThan i base
|
|
then [ i ]
|
|
else let r = subtract i (divide i base * base)
|
|
|
|
let q = divide (subtract i r) base
|
|
|
|
in [ r ] # functionArgs q
|
|
|
|
let functionErased =
|
|
Any/toTypeUnchecked
|
|
(FunctionType Any)
|
|
(Any/toAny (FunctionType (FunctionType Any)) function)
|
|
|
|
let go = function functionErased
|
|
|
|
in throwIfNot
|
|
(greaterThanEqual base 2)
|
|
"Base must be 2 or greater"
|
|
(List Natural)
|
|
(List/reverse Natural (go i))
|
|
|
|
in toBaseDigits
|