{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}

module Type.Data.Num.Decimal.Proof (
    Digits(Digits),
    UnaryNat(UnaryNat), unaryNat,
    UnaryPos(UnaryPos), unaryPos,
    ) where

import qualified Type.Data.Num.Decimal.Digit.Proof as DigitProof
import qualified Type.Data.Num.Decimal.Digit as Digit
import qualified Type.Data.Num.Decimal.Number as Dec
import qualified Type.Data.Num.Unary.Literal as UnaryLit
import qualified Type.Data.Num.Unary.Proof as UnaryProof
import qualified Type.Data.Num.Unary as Unary

import Type.Data.Num.Decimal.Number (Pos, (:>), Natural, Positive, )


data UnaryNat n = Unary.Natural (Dec.ToUnary n) => UnaryNat

unaryNat :: (Natural n) => UnaryNat n
unaryNat :: UnaryNat n
unaryNat = UnaryNat Zero
-> (forall x xs. (Pos x, Digits xs) => UnaryNat (Pos x xs))
-> UnaryNat n
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f n
Dec.switchNat UnaryNat Zero
forall n. Natural (ToUnary n) => UnaryNat n
UnaryNat (UnaryPos (Pos x xs) -> UnaryNat (Pos x xs)
forall n. UnaryPos n -> UnaryNat n
unaryUnPos UnaryPos (Pos x xs)
forall x xs. (Pos x, Digits xs) => UnaryPos (Pos x xs)
unaryPosPos)

unaryUnPos :: UnaryPos n -> UnaryNat n
unaryUnPos :: UnaryPos n -> UnaryNat n
unaryUnPos UnaryPos n
UnaryPos = UnaryNat n
forall n. Natural (ToUnary n) => UnaryNat n
UnaryNat


data UnaryPos n = Unary.Positive (Dec.ToUnary n) => UnaryPos

unaryPos :: (Positive n) => UnaryPos n
unaryPos :: UnaryPos n
unaryPos = (forall x xs. (Pos x, Digits xs) => UnaryPos (Pos x xs))
-> UnaryPos n
forall n (f :: * -> *).
Positive n =>
(forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f n
Dec.switchPos forall x xs. (Pos x, Digits xs) => UnaryPos (Pos x xs)
unaryPosPos

unaryPosPos :: (Digit.Pos x, Dec.Digits xs) => UnaryPos (Pos x xs)
unaryPosPos :: UnaryPos (Pos x xs)
unaryPosPos =
    (UnaryPos x -> Digits xs -> UnaryPos (Pos x xs))
-> UnaryPos (Pos x xs)
forall x xs.
(Pos x, Digits xs) =>
(UnaryPos x -> Digits xs -> UnaryPos (Pos x xs))
-> UnaryPos (Pos x xs)
withUnaryPosPos ((UnaryPos x -> Digits xs -> UnaryPos (Pos x xs))
 -> UnaryPos (Pos x xs))
-> (UnaryPos x -> Digits xs -> UnaryPos (Pos x xs))
-> UnaryPos (Pos x xs)
forall a b. (a -> b) -> a -> b
$ \UnaryPos x
x Digits xs
xs ->
        case Pos (ToUnary x) -> Digits xs -> Pos (ToUnaryAcc (ToUnary x) xs)
forall m xs. Pos m -> Digits xs -> Pos (ToUnaryAcc m xs)
toUnaryAcc (UnaryPos x -> Pos (ToUnary x)
forall x. UnaryPos x -> Pos (ToUnary x)
digitUnaryPos UnaryPos x
x) Digits xs
xs of
            Pos (ToUnaryAcc (ToUnary x) xs)
UnaryProof.Pos -> UnaryPos (Pos x xs)
forall n. Positive (ToUnary n) => UnaryPos n
UnaryPos


withUnaryPosPos ::
    (Digit.Pos x, Dec.Digits xs) =>
    (DigitProof.UnaryPos x -> Digits xs ->
     UnaryPos (Pos x xs)) ->
    UnaryPos (Pos x xs)
withUnaryPosPos :: (UnaryPos x -> Digits xs -> UnaryPos (Pos x xs))
-> UnaryPos (Pos x xs)
withUnaryPosPos UnaryPos x -> Digits xs -> UnaryPos (Pos x xs)
f =
    UnaryPos x -> Digits xs -> UnaryPos (Pos x xs)
f UnaryPos x
forall d. Pos d => UnaryPos d
DigitProof.unaryPos Digits xs
forall xs. Digits xs => Digits xs
Digits

digitUnaryPos ::
    DigitProof.UnaryPos x -> UnaryProof.Pos (Digit.ToUnary x)
digitUnaryPos :: UnaryPos x -> Pos (ToUnary x)
digitUnaryPos UnaryPos x
DigitProof.UnaryPos = Pos (ToUnary x)
forall x. Positive x => Pos x
UnaryProof.Pos


data Digits xs = (Dec.Digits xs) => Digits

newtype
    ToUnaryAcc m xs =
        ToUnaryAcc {ToUnaryAcc m xs -> Pos m -> Digits xs -> Pos (ToUnaryAcc m xs)
runToUnaryAcc ::
            UnaryProof.Pos m -> Digits xs ->
            UnaryProof.Pos (Dec.ToUnaryAcc m xs)}

toUnaryAcc ::
    UnaryProof.Pos m -> Digits xs ->
    UnaryProof.Pos (Dec.ToUnaryAcc m xs)
toUnaryAcc :: Pos m -> Digits xs -> Pos (ToUnaryAcc m xs)
toUnaryAcc Pos m
m y :: Digits xs
y@Digits xs
Digits =
    ToUnaryAcc m xs -> Pos m -> Digits xs -> Pos (ToUnaryAcc m xs)
forall m xs.
ToUnaryAcc m xs -> Pos m -> Digits xs -> Pos (ToUnaryAcc m xs)
runToUnaryAcc
        (ToUnaryAcc m EndDesc
-> (forall xh xl. (C xh, Digits xl) => ToUnaryAcc m (xh :> xl))
-> ToUnaryAcc m xs
forall xs (f :: * -> *).
Digits xs =>
f EndDesc
-> (forall xh xl. (C xh, Digits xl) => f (xh :> xl)) -> f xs
Dec.switchDigits
            ((Pos m -> Digits EndDesc -> Pos (ToUnaryAcc m EndDesc))
-> ToUnaryAcc m EndDesc
forall m xs.
(Pos m -> Digits xs -> Pos (ToUnaryAcc m xs)) -> ToUnaryAcc m xs
ToUnaryAcc ((Pos m -> Digits EndDesc -> Pos (ToUnaryAcc m EndDesc))
 -> ToUnaryAcc m EndDesc)
-> (Pos m -> Digits EndDesc -> Pos (ToUnaryAcc m EndDesc))
-> ToUnaryAcc m EndDesc
forall a b. (a -> b) -> a -> b
$ \ Pos m
UnaryProof.Pos Digits EndDesc
_ -> Pos (ToUnaryAcc m EndDesc)
forall x. Positive x => Pos x
UnaryProof.Pos)
            ((Pos m -> Digits (xh :> xl) -> Pos (ToUnaryAcc m (xh :> xl)))
-> ToUnaryAcc m (xh :> xl)
forall m xs.
(Pos m -> Digits xs -> Pos (ToUnaryAcc m xs)) -> ToUnaryAcc m xs
ToUnaryAcc ((Pos m -> Digits (xh :> xl) -> Pos (ToUnaryAcc m (xh :> xl)))
 -> ToUnaryAcc m (xh :> xl))
-> (Pos m -> Digits (xh :> xl) -> Pos (ToUnaryAcc m (xh :> xl)))
-> ToUnaryAcc m (xh :> xl)
forall a b. (a -> b) -> a -> b
$ \ Pos m
acc Digits (xh :> xl)
xt ->
                Pos
  (ToUnary xh
   :+: (m
        :+: (m
             :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: m))))))))))
-> Digits xl
-> Pos
     (ToUnaryAcc
        (ToUnary xh
         :+: (m
              :+: (m
                   :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: m))))))))))
        xl)
forall m xs. Pos m -> Digits xs -> Pos (ToUnaryAcc m xs)
toUnaryAcc
                    (Pos m
-> Nat (ToUnary xh) -> Pos U10 -> Pos (ToUnary xh :+: (m :*: U10))
forall m x. Pos m -> Nat x -> Pos U10 -> Pos (x :+: (m :*: U10))
unaryAcc Pos m
acc (Nat xh -> Nat (ToUnary xh)
forall d. Nat d -> Nat (ToUnary d)
DigitProof.unaryNatImpl (Digits (xh :> xl) -> Nat xh
forall x xs. C x => Digits (x :> xs) -> Nat x
headDigits Digits (xh :> xl)
xt))
                        Pos U10
forall x. Positive x => Pos x
UnaryProof.Pos)
                    (Digits (xh :> xl) -> Digits xl
forall xs x. Digits xs => Digits (x :> xs) -> Digits xs
tailDigits Digits (xh :> xl)
xt)))
        Pos m
m Digits xs
y


headDigits :: (Digit.C x) => Digits (x :> xs) -> DigitProof.Nat x
headDigits :: Digits (x :> xs) -> Nat x
headDigits Digits (x :> xs)
Digits = Nat x
forall d. C d => Nat d
DigitProof.Nat

tailDigits :: Dec.Digits xs => Digits (x :> xs) -> Digits xs
tailDigits :: Digits (x :> xs) -> Digits xs
tailDigits Digits (x :> xs)
Digits = Digits xs
forall xs. Digits xs => Digits xs
Digits


unaryAcc ::
    UnaryProof.Pos m -> UnaryProof.Nat x -> UnaryProof.Pos UnaryLit.U10 ->
    UnaryProof.Pos (x Unary.:+: (m Unary.:*: UnaryLit.U10))
unaryAcc :: Pos m -> Nat x -> Pos U10 -> Pos (x :+: (m :*: U10))
unaryAcc Pos m
m Nat x
x Pos U10
ten =
    Nat x
-> Pos
     (m
      :+: (m
           :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: m)))))))))
-> Pos
     (x
      :+: (m
           :+: (m
                :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: m))))))))))
forall x y. Nat x -> Pos y -> Pos (x :+: y)
UnaryProof.addPosR Nat x
x (Pos
   (m
    :+: (m
         :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: m)))))))))
 -> Pos
      (x
       :+: (m
            :+: (m
                 :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: m)))))))))))
-> Pos
     (m
      :+: (m
           :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: m)))))))))
-> Pos
     (x
      :+: (m
           :+: (m
                :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: (m :+: m))))))))))
forall a b. (a -> b) -> a -> b
$ Pos m -> Pos U10 -> Pos (m :*: U10)
forall x y. Pos x -> Pos y -> Pos (x :*: y)
UnaryProof.mulPos Pos m
m Pos U10
ten