module Quox.NatExtra

import public Data.Nat
import Data.Nat.Division
import Data.SnocList
import Data.Vect

%default total


public export
data LTE' : Nat -> Nat -> Type where
  LTERefl  : LTE' n n
  LTESuccR : LTE' m n -> LTE' m (S n)
%builtin Natural LTE'

public export %hint
lteZero' : {n : Nat} -> LTE' 0 n
lteZero' {n = 0}   = LTERefl
lteZero' {n = S n} = LTESuccR lteZero'

public export %hint
lteSucc' : LTE' m n -> LTE' (S m) (S n)
lteSucc' LTERefl      = LTERefl
lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p

public export
fromLte : {n : Nat} -> LTE m n -> LTE' m n
fromLte LTEZero     = lteZero'
fromLte (LTESucc p) = lteSucc' $ fromLte p

public export
toLte : {n : Nat} -> m `LTE'` n -> m `LTE` n
toLte LTERefl      = reflexive
toLte (LTESuccR p) = lteSuccRight (toLte p)


private
0 baseNZ : n `GTE` 2 => NonZero n
baseNZ @{LTESucc _} = SIsNonZero

parameters {base : Nat} {auto 0 _ : base `GTE` 2} (chars : Vect base Char)
  private
  showAtBase' : List Char -> Nat -> List Char
  showAtBase' acc 0 = acc
  showAtBase' acc k =
    let dig = natToFinLT (modNatNZ k base baseNZ) @{boundModNatNZ {}} in
    showAtBase' (index dig chars :: acc)
                (assert_smaller k $ divNatNZ k base baseNZ)

  export
  showAtBase : Nat -> String
  showAtBase = pack . showAtBase' []

export
showHex : Nat -> String
showHex = showAtBase $ fromList $ unpack "0123456789ABCDEF"


n2i = natToInteger
i2n = fromInteger {ty = Nat}

private partial %inline
divNatViaInteger : (m, n : Nat) -> Nat
divNatViaInteger m n = i2n $ n2i m `div` n2i n
%transform "divNat" divNat = divNatViaInteger

private %inline
divNatViaIntegerNZ : (m, n : Nat) -> (0 _ : NonZero n) -> Nat
divNatViaIntegerNZ m n _ = assert_total divNatViaInteger m n
%transform "divNat" divNatNZ = divNatViaIntegerNZ

private partial %inline
modNatViaInteger : (m, n : Nat) -> Nat
modNatViaInteger m n = i2n $ n2i m `mod` n2i n
%transform "modNat" modNat = modNatViaInteger

private %inline
modNatViaIntegerNZ : (m, n : Nat) -> (0 _ : NonZero n) -> Nat
modNatViaIntegerNZ m n _ = assert_total modNatViaInteger m n
%transform "modNat" modNatNZ = modNatViaIntegerNZ


public export
data ViewLsb : Nat -> Type where
  Lsb0 : (n : Nat) -> ViewLsb (2 * n)
  Lsb1 : (n : Nat) -> ViewLsb (S (2 * n))

private
viewLsb' : (m, d : Nat) -> (0 _ : m `LT` 2) -> ViewLsb (m + 2 * d)
viewLsb' 0 d p = Lsb0 d
viewLsb' 1 d p = Lsb1 d
viewLsb' (S (S _)) _ (LTESucc p) = void $ absurd p

export
viewLsb : (n : Nat) -> ViewLsb n
viewLsb n =
  let nz = the (NonZero 2) %search in
  rewrite DivisionTheorem n 2 nz nz in
  rewrite multCommutative (divNatNZ n 2 nz) 2 in
  viewLsb' (modNatNZ n 2 nz) (divNatNZ n 2 nz) (boundModNatNZ n 2 nz)