{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ScopedTypeVariables #-}
module TypeLevel.Number.Int (
ZZ
, Dn
, D0
, D1
, IntT(..)
, SomeInt
, withInt
, intT
, module TypeLevel.Number.Classes
) where
import Data.Typeable (Typeable)
import Language.Haskell.TH
import TypeLevel.Number.Classes
import TypeLevel.Number.Int.Types
import TypeLevel.Util
splitToTrits :: Integer -> [Int]
splitToTrits :: Integer -> [Int]
splitToTrits 0 = []
splitToTrits x :: Integer
x | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = 0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: Integer -> [Int]
splitToTrits Integer
rest
| Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 1 = 1 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: Integer -> [Int]
splitToTrits Integer
rest
| Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 2 = -1 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: Integer -> [Int]
splitToTrits (Integer
rest Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1)
where
(rest :: Integer
rest,n :: Integer
n) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
x 3
splitToTrits _ = [Char] -> [Int]
forall a. HasCallStack => [Char] -> a
error "Internal error"
intT :: Integer -> TypeQ
intT :: Integer -> TypeQ
intT = (TypeQ -> TypeQ -> TypeQ) -> TypeQ -> [TypeQ] -> TypeQ
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TypeQ -> TypeQ -> TypeQ
appT (Name -> TypeQ
conT ''ZZ) ([TypeQ] -> TypeQ) -> (Integer -> [TypeQ]) -> Integer -> TypeQ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> TypeQ) -> [Int] -> [TypeQ]
forall a b. (a -> b) -> [a] -> [b]
map Int -> TypeQ
forall a. (Eq a, Num a, Show a) => a -> TypeQ
con ([Int] -> [TypeQ]) -> (Integer -> [Int]) -> Integer -> [TypeQ]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> [Int]
splitToTrits
where
con :: a -> TypeQ
con (-1) = Name -> TypeQ
conT ''Dn
con 0 = Name -> TypeQ
conT ''D0
con 1 = Name -> TypeQ
conT ''D1
con x :: a
x = [Char] -> TypeQ
forall a. HasCallStack => [Char] -> a
error ([Char] -> TypeQ) -> [Char] -> TypeQ
forall a b. (a -> b) -> a -> b
$ "Strange trit: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
x
class IntT n where
toInt :: Integral i => n -> i
instance IntT ZZ where toInt :: ZZ -> i
toInt _ = 0
instance IntT (D1 ZZ) where toInt :: D1 ZZ -> i
toInt _ = 1
instance IntT (Dn ZZ) where toInt :: Dn ZZ -> i
toInt _ = -1
instance IntT (Dn n) => IntT (Dn (Dn n)) where toInt :: Dn (Dn n) -> i
toInt n :: Dn (Dn n)
n = -1 i -> i -> i
forall a. Num a => a -> a -> a
+ 3 i -> i -> i
forall a. Num a => a -> a -> a
* Dn (Dn n) -> i
forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
toInt' Dn (Dn n)
n
instance IntT (Dn n) => IntT (D0 (Dn n)) where toInt :: D0 (Dn n) -> i
toInt n :: D0 (Dn n)
n = 0 i -> i -> i
forall a. Num a => a -> a -> a
+ 3 i -> i -> i
forall a. Num a => a -> a -> a
* D0 (Dn n) -> i
forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
toInt' D0 (Dn n)
n
instance IntT (Dn n) => IntT (D1 (Dn n)) where toInt :: D1 (Dn n) -> i
toInt n :: D1 (Dn n)
n = 1 i -> i -> i
forall a. Num a => a -> a -> a
+ 3 i -> i -> i
forall a. Num a => a -> a -> a
* D1 (Dn n) -> i
forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
toInt' D1 (Dn n)
n
instance IntT (D0 n) => IntT (Dn (D0 n)) where toInt :: Dn (D0 n) -> i
toInt n :: Dn (D0 n)
n = -1 i -> i -> i
forall a. Num a => a -> a -> a
+ 3 i -> i -> i
forall a. Num a => a -> a -> a
* Dn (D0 n) -> i
forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
toInt' Dn (D0 n)
n
instance IntT (D0 n) => IntT (D0 (D0 n)) where toInt :: D0 (D0 n) -> i
toInt n :: D0 (D0 n)
n = 0 i -> i -> i
forall a. Num a => a -> a -> a
+ 3 i -> i -> i
forall a. Num a => a -> a -> a
* D0 (D0 n) -> i
forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
toInt' D0 (D0 n)
n
instance IntT (D0 n) => IntT (D1 (D0 n)) where toInt :: D1 (D0 n) -> i
toInt n :: D1 (D0 n)
n = 1 i -> i -> i
forall a. Num a => a -> a -> a
+ 3 i -> i -> i
forall a. Num a => a -> a -> a
* D1 (D0 n) -> i
forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
toInt' D1 (D0 n)
n
instance IntT (D1 n) => IntT (Dn (D1 n)) where toInt :: Dn (D1 n) -> i
toInt n :: Dn (D1 n)
n = -1 i -> i -> i
forall a. Num a => a -> a -> a
+ 3 i -> i -> i
forall a. Num a => a -> a -> a
* Dn (D1 n) -> i
forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
toInt' Dn (D1 n)
n
instance IntT (D1 n) => IntT (D0 (D1 n)) where toInt :: D0 (D1 n) -> i
toInt n :: D0 (D1 n)
n = 0 i -> i -> i
forall a. Num a => a -> a -> a
+ 3 i -> i -> i
forall a. Num a => a -> a -> a
* D0 (D1 n) -> i
forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
toInt' D0 (D1 n)
n
instance IntT (D1 n) => IntT (D1 (D1 n)) where toInt :: D1 (D1 n) -> i
toInt n :: D1 (D1 n)
n = 1 i -> i -> i
forall a. Num a => a -> a -> a
+ 3 i -> i -> i
forall a. Num a => a -> a -> a
* D1 (D1 n) -> i
forall n i (t :: * -> *). (IntT n, Integral i) => t n -> i
toInt' D1 (D1 n)
n
toInt' :: (IntT n, Integral i) => t n -> i
toInt' :: t n -> i
toInt' = n -> i
forall n i. (IntT n, Integral i) => n -> i
toInt (n -> i) -> (t n -> n) -> t n -> i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t n -> n
forall (t :: * -> *) a. t a -> a
cdr
instance Show ZZ where show :: ZZ -> [Char]
show _ = "[0:Z]"
instance IntT (Dn n) => Show (Dn n) where show :: Dn n -> [Char]
show n :: Dn n
n = "["[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++Integer -> [Char]
forall a. Show a => a -> [Char]
show (Dn n -> Integer
forall n i. (IntT n, Integral i) => n -> i
toInt Dn n
n :: Integer)[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++":Z]"
instance IntT (D0 n) => Show (D0 n) where show :: D0 n -> [Char]
show n :: D0 n
n = "["[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++Integer -> [Char]
forall a. Show a => a -> [Char]
show (D0 n -> Integer
forall n i. (IntT n, Integral i) => n -> i
toInt D0 n
n :: Integer)[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++":Z]"
instance IntT (D1 n) => Show (D1 n) where show :: D1 n -> [Char]
show n :: D1 n
n = "["[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++Integer -> [Char]
forall a. Show a => a -> [Char]
show (D1 n -> Integer
forall n i. (IntT n, Integral i) => n -> i
toInt D1 n
n :: Integer)[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++":Z]"
data SomeInt where
SomeInt :: IntT n => n -> SomeInt
deriving Typeable
instance Show SomeInt where
showsPrec :: Int -> SomeInt -> [Char] -> [Char]
showsPrec d :: Int
d (SomeInt n :: n
n) = Bool -> ([Char] -> [Char]) -> [Char] -> [Char]
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 10) (([Char] -> [Char]) -> [Char] -> [Char])
-> ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$
[Char] -> [Char] -> [Char]
showString "withInt SomeInt " ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> [Char] -> [Char]
forall a. Show a => a -> [Char] -> [Char]
shows (n -> Integer
forall n i. (IntT n, Integral i) => n -> i
toInt n
n :: Integer)
withInt :: forall i a. (Integral i) => (forall n. IntT n => n -> a) -> i -> a
withInt :: (forall n. IntT n => n -> a) -> i -> a
withInt f :: forall n. IntT n => n -> a
f i0 :: i
i0
| i
i0 i -> i -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = ZZ -> a
forall n. IntT n => n -> a
f (ZZ
forall a. HasCallStack => a
undefined :: ZZ)
| Bool
otherwise = Integer
-> (forall n m. (IntT n, n ~ Dn m) => n -> a)
-> (forall n m. (IntT n, n ~ D0 m) => n -> a)
-> (forall n m. (IntT n, n ~ D1 m) => n -> a)
-> a
cont (i -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral i
i0) forall n. IntT n => n -> a
forall n m. (IntT n, n ~ Dn m) => n -> a
f forall n. IntT n => n -> a
forall n m. (IntT n, n ~ D0 m) => n -> a
f forall n. IntT n => n -> a
forall n m. (IntT n, n ~ D1 m) => n -> a
f
where
cont :: Integer -> (forall n m. (IntT n, n ~ Dn m) => n -> a)
-> (forall n m. (IntT n, n ~ D0 m) => n -> a)
-> (forall n m. (IntT n, n ~ D1 m) => n -> a) -> a
cont :: Integer
-> (forall n m. (IntT n, n ~ Dn m) => n -> a)
-> (forall n m. (IntT n, n ~ D0 m) => n -> a)
-> (forall n m. (IntT n, n ~ D1 m) => n -> a)
-> a
cont (-1) kN :: forall n m. (IntT n, n ~ Dn m) => n -> a
kN _ _ = Dn ZZ -> a
forall n m. (IntT n, n ~ Dn m) => n -> a
kN (Dn ZZ
forall a. HasCallStack => a
undefined :: Dn ZZ)
cont 1 _ _ k1 :: forall n m. (IntT n, n ~ D1 m) => n -> a
k1 = D1 ZZ -> a
forall n m. (IntT n, n ~ D1 m) => n -> a
k1 (D1 ZZ
forall a. HasCallStack => a
undefined :: D1 ZZ)
cont i :: Integer
i kN :: forall n m. (IntT n, n ~ Dn m) => n -> a
kN k0 :: forall n m. (IntT n, n ~ D0 m) => n -> a
k0 k1 :: forall n m. (IntT n, n ~ D1 m) => n -> a
k1 = Integer
-> (forall n m. (IntT n, n ~ Dn m) => n -> a)
-> (forall n m. (IntT n, n ~ D0 m) => n -> a)
-> (forall n m. (IntT n, n ~ D1 m) => n -> a)
-> a
cont Integer
i' forall n m. (IntT n, n ~ Dn m) => n -> a
kN' forall n m. (IntT n, n ~ D0 m) => n -> a
k0' forall n m. (IntT n, n ~ D1 m) => n -> a
k1'
where
(i' :: Integer
i',bit :: Integer
bit) = case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
i 3 of
(x :: Integer
x,2) -> (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+1,-1)
x :: (Integer, Integer)
x -> (Integer, Integer)
x
kN' :: forall n m. (IntT n, n ~ Dn m) => n -> a
kN' :: n -> a
kN' _ | Integer
bit Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== -1 = Dn n -> a
forall n m. (IntT n, n ~ Dn m) => n -> a
kN (Dn n
forall a. HasCallStack => a
undefined :: Dn n)
| Integer
bit Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = D0 n -> a
forall n m. (IntT n, n ~ D0 m) => n -> a
k0 (D0 n
forall a. HasCallStack => a
undefined :: D0 n)
| Bool
otherwise = D1 n -> a
forall n m. (IntT n, n ~ D1 m) => n -> a
k1 (D1 n
forall a. HasCallStack => a
undefined :: D1 n)
k0' :: forall n m. (IntT n, n ~ D0 m) => n -> a
k0' :: n -> a
k0' _ | Integer
bit Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== -1 = Dn n -> a
forall n m. (IntT n, n ~ Dn m) => n -> a
kN (Dn n
forall a. HasCallStack => a
undefined :: Dn n)
| Integer
bit Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = D0 n -> a
forall n m. (IntT n, n ~ D0 m) => n -> a
k0 (D0 n
forall a. HasCallStack => a
undefined :: D0 n)
| Bool
otherwise = D1 n -> a
forall n m. (IntT n, n ~ D1 m) => n -> a
k1 (D1 n
forall a. HasCallStack => a
undefined :: D1 n)
k1' :: forall n m. (IntT n, n ~ D1 m) => n -> a
k1' :: n -> a
k1' _ | Integer
bit Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== -1 = Dn n -> a
forall n m. (IntT n, n ~ Dn m) => n -> a
kN (Dn n
forall a. HasCallStack => a
undefined :: Dn n)
| Integer
bit Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = D0 n -> a
forall n m. (IntT n, n ~ D0 m) => n -> a
k0 (D0 n
forall a. HasCallStack => a
undefined :: D0 n)
| Bool
otherwise = D1 n -> a
forall n m. (IntT n, n ~ D1 m) => n -> a
k1 (D1 n
forall a. HasCallStack => a
undefined :: D1 n)
type family AddBit n :: *
type instance AddBit ZZ = ZZ
type instance AddBit (Dn a) = D0 (Dn a)
type instance AddBit (D0 a) = D0 (D0 a)
type instance AddBit (D1 a) = D0 (D1 a)
type instance Normalized ZZ = ZZ
type instance Normalized (Dn n) = Dn (Normalized n)
type instance Normalized (D0 n) = AddBit (Normalized n)
type instance Normalized (D1 n) = D1 (Normalized n)
type instance Next ZZ = D1 ZZ
type instance Next (Dn n) = Normalized (D0 n)
type instance Next (D0 n) = D1 n
type instance Next (D1 n) = Normalized (Dn (Next n))
type instance Prev ZZ = Dn ZZ
type instance Prev (Dn n) = Normalized (D1 (Prev n))
type instance Prev (D0 n) = Dn n
type instance Prev (D1 n) = Normalized (D0 n)
type instance Negate ZZ = ZZ
type instance Negate (Dn n) = D1 (Negate n)
type instance Negate (D0 n) = D0 (Negate n)
type instance Negate (D1 n) = Dn (Negate n)
type family Add' n m carry :: *
data CarryN
data Carry0
data Carry1
type instance Add' ZZ ZZ Carry0 = ZZ
type instance Add' ZZ (Dn n) Carry0 = (Dn n)
type instance Add' ZZ (D0 n) Carry0 = (D0 n)
type instance Add' ZZ (D1 n) Carry0 = (D1 n)
type instance Add' (Dn n) ZZ Carry0 = (Dn n)
type instance Add' (D0 n) ZZ Carry0 = (D0 n)
type instance Add' (D1 n) ZZ Carry0 = (D1 n)
type instance Add' ZZ ZZ CarryN = Dn ZZ
type instance Add' ZZ (Dn n) CarryN = Prev (Dn n)
type instance Add' ZZ (D0 n) CarryN = (Dn n)
type instance Add' ZZ (D1 n) CarryN = (D0 n)
type instance Add' (Dn n) ZZ CarryN = Prev (Dn n)
type instance Add' (D0 n) ZZ CarryN = (Dn n)
type instance Add' (D1 n) ZZ CarryN = (D0 n)
type instance Add' ZZ ZZ Carry1 = D1 ZZ
type instance Add' ZZ (Dn n) Carry1 = (D0 n)
type instance Add' ZZ (D0 n) Carry1 = (D1 n)
type instance Add' ZZ (D1 n) Carry1 = Next (D1 n)
type instance Add' (Dn n) ZZ Carry1 = (D0 n)
type instance Add' (D0 n) ZZ Carry1 = (D1 n)
type instance Add' (D1 n) ZZ Carry1 = Next (D1 n)
type instance Add' (Dn n) (Dn m) Carry0 = D1 (Add' n m CarryN)
type instance Add' (D0 n) (Dn m) Carry0 = Dn (Add' n m Carry0)
type instance Add' (D1 n) (Dn m) Carry0 = D0 (Add' n m Carry0)
type instance Add' (Dn n) (D0 m) Carry0 = Dn (Add' n m Carry0)
type instance Add' (D0 n) (D0 m) Carry0 = D0 (Add' n m Carry0)
type instance Add' (D1 n) (D0 m) Carry0 = D1 (Add' n m Carry0)
type instance Add' (Dn n) (D1 m) Carry0 = D0 (Add' n m Carry0)
type instance Add' (D0 n) (D1 m) Carry0 = D1 (Add' n m Carry0)
type instance Add' (D1 n) (D1 m) Carry0 = Dn (Add' n m Carry1)
type instance Add' (Dn n) (Dn m) CarryN = D0 (Add' n m CarryN)
type instance Add' (D0 n) (Dn m) CarryN = D1 (Add' n m CarryN)
type instance Add' (D1 n) (Dn m) CarryN = Dn (Add' n m Carry0)
type instance Add' (Dn n) (D0 m) CarryN = D1 (Add' n m CarryN)
type instance Add' (D0 n) (D0 m) CarryN = Dn (Add' n m Carry0)
type instance Add' (D1 n) (D0 m) CarryN = D0 (Add' n m Carry0)
type instance Add' (Dn n) (D1 m) CarryN = Dn (Add' n m Carry0)
type instance Add' (D0 n) (D1 m) CarryN = D0 (Add' n m Carry0)
type instance Add' (D1 n) (D1 m) CarryN = D1 (Add' n m Carry0)
type instance Add' (Dn n) (Dn m) Carry1 = Dn (Add' n m Carry0)
type instance Add' (D0 n) (Dn m) Carry1 = D0 (Add' n m Carry0)
type instance Add' (D1 n) (Dn m) Carry1 = D1 (Add' n m Carry0)
type instance Add' (Dn n) (D0 m) Carry1 = D0 (Add' n m Carry0)
type instance Add' (D0 n) (D0 m) Carry1 = D1 (Add' n m Carry0)
type instance Add' (D1 n) (D0 m) Carry1 = Dn (Add' n m Carry1)
type instance Add' (Dn n) (D1 m) Carry1 = D1 (Add' n m Carry0)
type instance Add' (D0 n) (D1 m) Carry1 = Dn (Add' n m Carry1)
type instance Add' (D1 n) (D1 m) Carry1 = D0 (Add' n m Carry1)
type instance Add ZZ ZZ = ZZ
type instance Add ZZ (Dn n) = Normalized (Dn n)
type instance Add ZZ (D0 n) = Normalized (D0 n)
type instance Add ZZ (D1 n) = Normalized (D1 n)
type instance Add (Dn n) ZZ = Normalized (Dn n)
type instance Add (D0 n) ZZ = Normalized (D0 n)
type instance Add (D1 n) ZZ = Normalized (D1 n)
type instance Add (Dn n) (Dn m) = Normalized (Add' (Dn n) (Dn m) Carry0)
type instance Add (D0 n) (Dn m) = Normalized (Add' (D0 n) (Dn m) Carry0)
type instance Add (D1 n) (Dn m) = Normalized (Add' (D1 n) (Dn m) Carry0)
type instance Add (Dn n) (D0 m) = Normalized (Add' (Dn n) (D0 m) Carry0)
type instance Add (D0 n) (D0 m) = Normalized (Add' (D0 n) (D0 m) Carry0)
type instance Add (D1 n) (D0 m) = Normalized (Add' (D1 n) (D0 m) Carry0)
type instance Add (Dn n) (D1 m) = Normalized (Add' (Dn n) (D1 m) Carry0)
type instance Add (D0 n) (D1 m) = Normalized (Add' (D0 n) (D1 m) Carry0)
type instance Add (D1 n) (D1 m) = Normalized (Add' (D1 n) (D1 m) Carry0)
type instance Sub ZZ ZZ = ZZ
type instance Sub ZZ (Dn n) = Negate (Dn n)
type instance Sub ZZ (D0 n) = Negate (D0 n)
type instance Sub ZZ (D1 n) = Negate (D1 n)
type instance Sub (Dn n) ZZ = (Dn n)
type instance Sub (D0 n) ZZ = (D0 n)
type instance Sub (D1 n) ZZ = (D1 n)
type instance Sub (Dn n) (Dn m) = Add (Dn n) (Negate (Dn m))
type instance Sub (D0 n) (Dn m) = Add (D0 n) (Negate (Dn m))
type instance Sub (D1 n) (Dn m) = Add (D1 n) (Negate (Dn m))
type instance Sub (Dn n) (D0 m) = Add (Dn n) (Negate (D0 m))
type instance Sub (D0 n) (D0 m) = Add (D0 n) (Negate (D0 m))
type instance Sub (D1 n) (D0 m) = Add (D1 n) (Negate (D0 m))
type instance Sub (Dn n) (D1 m) = Add (Dn n) (Negate (D1 m))
type instance Sub (D0 n) (D1 m) = Add (D0 n) (Negate (D1 m))
type instance Sub (D1 n) (D1 m) = Add (D1 n) (Negate (D1 m))
type instance Mul n ZZ = ZZ
type instance Mul n (Dn m) = Normalized (Add' (Negate n) (D0 (Mul n m)) Carry0)
type instance Mul n (D0 m) = Normalized (D0 (Mul n m))
type instance Mul n (D1 m) = Normalized (Add' n (D0 (Mul n m)) Carry0)