Module
Typelevel.Arithmetic.Add
- Package
- purescript-typelevel-arithmetic
- Repository
- sigma-andex/purescript-typelevel-arithmetic
#AddSingle Source
class AddSingle :: Symbol -> Symbol -> Symbol -> Symbol -> Symbol -> Constraint
class AddSingle (augend :: Symbol) (addend :: Symbol) (carryPrevious :: Symbol) (carryNext :: Symbol) (sum :: Symbol) | augend addend carryPrevious -> carryNext sum, augend carryPrevious sum -> addend carryNext, addend carryPrevious sum -> augend carryNext
Class for internal use only. See Add
instead.
Typeclass for adding two single digits.
Instances
AddSingle "0" "0" "0" "0" "0"
AddSingle "1" "0" "0" "0" "1"
AddSingle "2" "0" "0" "0" "2"
AddSingle "3" "0" "0" "0" "3"
AddSingle "4" "0" "0" "0" "4"
AddSingle "5" "0" "0" "0" "5"
AddSingle "6" "0" "0" "0" "6"
AddSingle "7" "0" "0" "0" "7"
AddSingle "8" "0" "0" "0" "8"
AddSingle "9" "0" "0" "0" "9"
AddSingle "0" "1" "0" "0" "1"
AddSingle "1" "1" "0" "0" "2"
AddSingle "2" "1" "0" "0" "3"
AddSingle "3" "1" "0" "0" "4"
AddSingle "4" "1" "0" "0" "5"
AddSingle "5" "1" "0" "0" "6"
AddSingle "6" "1" "0" "0" "7"
AddSingle "7" "1" "0" "0" "8"
AddSingle "8" "1" "0" "0" "9"
AddSingle "9" "1" "0" "1" "0"
AddSingle "0" "2" "0" "0" "2"
AddSingle "1" "2" "0" "0" "3"
AddSingle "2" "2" "0" "0" "4"
AddSingle "3" "2" "0" "0" "5"
AddSingle "4" "2" "0" "0" "6"
AddSingle "5" "2" "0" "0" "7"
AddSingle "6" "2" "0" "0" "8"
AddSingle "7" "2" "0" "0" "9"
AddSingle "8" "2" "0" "1" "0"
AddSingle "9" "2" "0" "1" "1"
AddSingle "0" "3" "0" "0" "3"
AddSingle "1" "3" "0" "0" "4"
AddSingle "2" "3" "0" "0" "5"
AddSingle "3" "3" "0" "0" "6"
AddSingle "4" "3" "0" "0" "7"
AddSingle "5" "3" "0" "0" "8"
AddSingle "6" "3" "0" "0" "9"
AddSingle "7" "3" "0" "1" "0"
AddSingle "8" "3" "0" "1" "1"
AddSingle "9" "3" "0" "1" "2"
AddSingle "0" "4" "0" "0" "4"
AddSingle "1" "4" "0" "0" "5"
AddSingle "2" "4" "0" "0" "6"
AddSingle "3" "4" "0" "0" "7"
AddSingle "4" "4" "0" "0" "8"
AddSingle "5" "4" "0" "0" "9"
AddSingle "6" "4" "0" "1" "0"
AddSingle "7" "4" "0" "1" "1"
AddSingle "8" "4" "0" "1" "2"
AddSingle "9" "4" "0" "1" "3"
AddSingle "0" "5" "0" "0" "5"
AddSingle "1" "5" "0" "0" "6"
AddSingle "2" "5" "0" "0" "7"
AddSingle "3" "5" "0" "0" "8"
AddSingle "4" "5" "0" "0" "9"
AddSingle "5" "5" "0" "1" "0"
AddSingle "6" "5" "0" "1" "1"
AddSingle "7" "5" "0" "1" "2"
AddSingle "8" "5" "0" "1" "3"
AddSingle "9" "5" "0" "1" "4"
AddSingle "0" "6" "0" "0" "6"
AddSingle "1" "6" "0" "0" "7"
AddSingle "2" "6" "0" "0" "8"
AddSingle "3" "6" "0" "0" "9"
AddSingle "4" "6" "0" "1" "0"
AddSingle "5" "6" "0" "1" "1"
AddSingle "6" "6" "0" "1" "2"
AddSingle "7" "6" "0" "1" "3"
AddSingle "8" "6" "0" "1" "4"
AddSingle "9" "6" "0" "1" "5"
AddSingle "0" "7" "0" "0" "7"
AddSingle "1" "7" "0" "0" "8"
AddSingle "2" "7" "0" "0" "9"
AddSingle "3" "7" "0" "1" "0"
AddSingle "4" "7" "0" "1" "1"
AddSingle "5" "7" "0" "1" "2"
AddSingle "6" "7" "0" "1" "3"
AddSingle "7" "7" "0" "1" "4"
AddSingle "8" "7" "0" "1" "5"
AddSingle "9" "7" "0" "1" "6"
AddSingle "0" "8" "0" "0" "8"
AddSingle "1" "8" "0" "0" "9"
AddSingle "2" "8" "0" "1" "0"
AddSingle "3" "8" "0" "1" "1"
AddSingle "4" "8" "0" "1" "2"
AddSingle "5" "8" "0" "1" "3"
AddSingle "6" "8" "0" "1" "4"
AddSingle "7" "8" "0" "1" "5"
AddSingle "8" "8" "0" "1" "6"
AddSingle "9" "8" "0" "1" "7"
AddSingle "0" "9" "0" "0" "9"
AddSingle "1" "9" "0" "1" "0"
AddSingle "2" "9" "0" "1" "1"
AddSingle "3" "9" "0" "1" "2"
AddSingle "4" "9" "0" "1" "3"
AddSingle "5" "9" "0" "1" "4"
AddSingle "6" "9" "0" "1" "5"
AddSingle "7" "9" "0" "1" "6"
AddSingle "8" "9" "0" "1" "7"
AddSingle "9" "9" "0" "1" "8"
AddSingle "0" "0" "1" "0" "1"
AddSingle "1" "0" "1" "0" "2"
AddSingle "2" "0" "1" "0" "3"
AddSingle "3" "0" "1" "0" "4"
AddSingle "4" "0" "1" "0" "5"
AddSingle "5" "0" "1" "0" "6"
AddSingle "6" "0" "1" "0" "7"
AddSingle "7" "0" "1" "0" "8"
AddSingle "8" "0" "1" "0" "9"
AddSingle "9" "0" "1" "1" "0"
AddSingle "0" "1" "1" "0" "2"
AddSingle "1" "1" "1" "0" "3"
AddSingle "2" "1" "1" "0" "4"
AddSingle "3" "1" "1" "0" "5"
AddSingle "4" "1" "1" "0" "6"
AddSingle "5" "1" "1" "0" "7"
AddSingle "6" "1" "1" "0" "8"
AddSingle "7" "1" "1" "0" "9"
AddSingle "8" "1" "1" "1" "0"
AddSingle "9" "1" "1" "1" "1"
AddSingle "0" "2" "1" "0" "3"
AddSingle "1" "2" "1" "0" "4"
AddSingle "2" "2" "1" "0" "5"
AddSingle "3" "2" "1" "0" "6"
AddSingle "4" "2" "1" "0" "7"
AddSingle "5" "2" "1" "0" "8"
AddSingle "6" "2" "1" "0" "9"
AddSingle "7" "2" "1" "1" "0"
AddSingle "8" "2" "1" "1" "1"
AddSingle "9" "2" "1" "1" "2"
AddSingle "0" "3" "1" "0" "4"
AddSingle "1" "3" "1" "0" "5"
AddSingle "2" "3" "1" "0" "6"
AddSingle "3" "3" "1" "0" "7"
AddSingle "4" "3" "1" "0" "8"
AddSingle "5" "3" "1" "0" "9"
AddSingle "6" "3" "1" "1" "0"
AddSingle "7" "3" "1" "1" "1"
AddSingle "8" "3" "1" "1" "2"
AddSingle "9" "3" "1" "1" "3"
AddSingle "0" "4" "1" "0" "5"
AddSingle "1" "4" "1" "0" "6"
AddSingle "2" "4" "1" "0" "7"
AddSingle "3" "4" "1" "0" "8"
AddSingle "4" "4" "1" "0" "9"
AddSingle "5" "4" "1" "1" "0"
AddSingle "6" "4" "1" "1" "1"
AddSingle "7" "4" "1" "1" "2"
AddSingle "8" "4" "1" "1" "3"
AddSingle "9" "4" "1" "1" "4"
AddSingle "0" "5" "1" "0" "6"
AddSingle "1" "5" "1" "0" "7"
AddSingle "2" "5" "1" "0" "8"
AddSingle "3" "5" "1" "0" "9"
AddSingle "4" "5" "1" "1" "0"
AddSingle "5" "5" "1" "1" "1"
AddSingle "6" "5" "1" "1" "2"
AddSingle "7" "5" "1" "1" "3"
AddSingle "8" "5" "1" "1" "4"
AddSingle "9" "5" "1" "1" "5"
AddSingle "0" "6" "1" "0" "7"
AddSingle "1" "6" "1" "0" "8"
AddSingle "2" "6" "1" "0" "9"
AddSingle "3" "6" "1" "1" "0"
AddSingle "4" "6" "1" "1" "1"
AddSingle "5" "6" "1" "1" "2"
AddSingle "6" "6" "1" "1" "3"
AddSingle "7" "6" "1" "1" "4"
AddSingle "8" "6" "1" "1" "5"
AddSingle "9" "6" "1" "1" "6"
AddSingle "0" "7" "1" "0" "8"
AddSingle "1" "7" "1" "0" "9"
AddSingle "2" "7" "1" "1" "0"
AddSingle "3" "7" "1" "1" "1"
AddSingle "4" "7" "1" "1" "2"
AddSingle "5" "7" "1" "1" "3"
AddSingle "6" "7" "1" "1" "4"
AddSingle "7" "7" "1" "1" "5"
AddSingle "8" "7" "1" "1" "6"
AddSingle "9" "7" "1" "1" "7"
AddSingle "0" "8" "1" "0" "9"
AddSingle "1" "8" "1" "1" "0"
AddSingle "2" "8" "1" "1" "1"
AddSingle "3" "8" "1" "1" "2"
AddSingle "4" "8" "1" "1" "3"
AddSingle "5" "8" "1" "1" "4"
AddSingle "6" "8" "1" "1" "5"
AddSingle "7" "8" "1" "1" "6"
AddSingle "8" "8" "1" "1" "7"
AddSingle "9" "8" "1" "1" "8"
AddSingle "0" "9" "1" "1" "0"
AddSingle "1" "9" "1" "1" "1"
AddSingle "2" "9" "1" "1" "2"
AddSingle "3" "9" "1" "1" "3"
AddSingle "4" "9" "1" "1" "4"
AddSingle "5" "9" "1" "1" "5"
AddSingle "6" "9" "1" "1" "6"
AddSingle "7" "9" "1" "1" "7"
AddSingle "8" "9" "1" "1" "8"
AddSingle "9" "9" "1" "1" "9"
#Add Source
class Add :: Symbol -> Symbol -> Symbol -> Symbol -> Constraint
class Add (augend :: Symbol) (addend :: Symbol) (carry :: Symbol) (sum :: Symbol) | augend addend -> carry sum, augend sum -> addend carry, addend sum -> augend carry
Typeclass for adding two typelevel numbers represented as symbols
Note: Currently, the terms have to be equal length.
Use the PadZeroes
typeclass to align the terms.
Use Trim
to remove any excessive zeroes after the calculation.
Example usage:
add ∷
∀ augend addend sum carry result.
Add augend addend carry sum ⇒
Cons carry sum result ⇒
Proxy augend → Proxy addend → Proxy result
add _ _ = Proxy
result ∷ Proxy "0579"
result = add (term ∷ _ "123") (term ∷ _ "456")
Instances
#PadZeroesHelper Source
class PadZeroesHelper :: Symbol -> Symbol -> Symbol -> Symbol -> Symbol -> Symbol -> Constraint
class PadZeroesHelper (leftIn :: Symbol) (rightIn :: Symbol) (leftTemp :: Symbol) (rightTemp :: Symbol) (leftOut :: Symbol) (rightOut :: Symbol) | leftIn rightIn leftTemp rightTemp -> leftOut rightOut
Typeclass for internal use only. See PadZeroes
instead.
Instances
PadZeroesHelper leftIn rightIn "" "" leftIn rightIn
(Cons head tail leftTemp, PadZeroesHelper leftIn rightIn tail "" leftIn leftOutPrev, Cons "0" leftOutPrev leftOut) => PadZeroesHelper leftIn rightIn leftTemp "" leftIn leftOut
(Cons head tail rightTemp, PadZeroesHelper leftIn rightIn "" tail leftOutPrev rightIn, Cons "0" leftOutPrev leftOut) => PadZeroesHelper leftIn rightIn "" rightTemp leftOut rightIn
(Cons leftHead leftTail leftTemp, Cons rightHead rightTail rightTemp, PadZeroesHelper leftIn rightIn leftTail rightTail leftOut rightOut) => PadZeroesHelper leftIn rightIn leftTemp rightTemp leftOut rightOut
#PadZeroes Source
class PadZeroes :: Symbol -> Symbol -> Symbol -> Symbol -> Constraint
class PadZeroes (leftIn :: Symbol) (rightIn :: Symbol) (leftOut :: Symbol) (rightOut :: Symbol) | leftIn rightIn -> leftOut rightOut
Typeclass to align two symbols by padding the shorter one with zeroes.
Instances
(PadZeroesHelper leftIn rightIn leftIn rightIn leftOut rightOut) => PadZeroes leftIn rightIn leftOut rightOut
#TrimHelper Source
class TrimHelper :: Symbol -> Symbol -> Symbol -> Constraint
class TrimHelper (inHead :: Symbol) (inTail :: Symbol) (out :: Symbol) | inHead inTail -> out
Typeclass for internal use only. See Trim
instead.
Instances
TrimHelper "0" "" "0"
(Cons inTailHead inTailTail inTail, TrimHelper inTailHead inTailTail out) => TrimHelper "0" inTail out
(Cons inHead inTail out) => TrimHelper inHead inTail out