module UVMHS.Core.Classes.Arithmetic where

import UVMHS.Core.Init

import UVMHS.Core.Classes.Order
import UVMHS.Core.Classes.Functors

infixl 5 +,-
infixl 6 ×,⨵,/,⌿,÷
infixl 7 ^

class Zero a where zero ∷ a
class Plus a where (+) ∷ a → a → a
class Minus a where (-) ∷ a → a → a
class One a where one ∷ a
class Times a where (×) ∷ a → a → a
class Divide a where (/) ∷ a → a → a
class DivMod a where {(⌿) ∷ a → a → a;(÷) ∷ a → a → a}
class Pon a where (^^) ∷ a → ℕ → a
class Pow a where (^) ∷ a → a → a
class Root a where root ∷ a → a
class Log a where log ∷ a → a
class Efn a where efn ∷ a → a
class Sin a where sin ∷ a → a
class Cos a where cos ∷ a → a

class (Zero a,Plus a) ⇒ Additive a
class (Additive a,One a,Times a) ⇒ Multiplicative a

succ ∷ (One a,Plus a) ⇒ a → a
succ :: forall a. (One a, Plus a) => a -> a
succ a
x = a
x a -> a -> a
forall a. Plus a => a -> a -> a
+ a
forall a. One a => a
one

pred ∷ (One a,Minus a) ⇒ a → a
pred :: forall a. (One a, Minus a) => a -> a
pred a
x = a
x a -> a -> a
forall a. Minus a => a -> a -> a
- a
forall a. One a => a
one

even ∷ (Eq a,Additive a,One a,DivMod a) ⇒ a → 𝔹
even :: forall a. (Eq a, Additive a, One a, DivMod a) => a -> 𝔹
even a
x = a
x a -> a -> a
forall a. DivMod a => a -> a -> a
÷ (a
forall a. One a => a
one a -> a -> a
forall a. Plus a => a -> a -> a
+ a
forall a. One a => a
one) a -> a -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ a
forall a. Zero a => a
zero

odd ∷ (Eq a,Additive a,One a,DivMod a) ⇒ a → 𝔹
odd :: forall a. (Eq a, Additive a, One a, DivMod a) => a -> 𝔹
odd a
x = a
x a -> a -> a
forall a. DivMod a => a -> a -> a
÷ (a
forall a. One a => a
one a -> a -> a
forall a. Plus a => a -> a -> a
+ a
forall a. One a => a
one) a -> a -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≢ a
forall a. Zero a => a
zero

neg ∷ (Zero a,Minus a) ⇒ a → a
neg :: forall a. (Zero a, Minus a) => a -> a
neg a
x = a
forall a. Zero a => a
zero a -> a -> a
forall a. Minus a => a -> a -> a
- a
x

(⨵) ∷ (Functor f,Multiplicative a) ⇒ a → f a → f a
a
x ⨵ :: forall (f :: * -> *) a.
(Functor f, Multiplicative a) =>
a -> f a -> f a
⨵ f a
xs = (a -> a) -> f a -> f a
forall a b. (a -> b) -> f a -> f b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (a
x a -> a -> a
forall a. Times a => a -> a -> a
×) f a
xs

(⨴ ) ∷ (Functor f,Multiplicative a) ⇒ f a → a → f a
f a
xs ⨴ :: forall (f :: * -> *) a.
(Functor f, Multiplicative a) =>
f a -> a -> f a
⨴ a
x = (a -> a) -> f a -> f a
forall a b. (a -> b) -> f a -> f b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (a -> a -> a
forall a. Times a => a -> a -> a
× a
x) f a
xs

class ToNat   a where nat   ∷ a → ℕ
class ToNat64 a where nat64 ∷ a → ℕ64
class ToNat32 a where nat32 ∷ a → ℕ32
class ToNat16 a where nat16 ∷ a → ℕ16
class ToNat8  a where nat8  ∷ a → ℕ8

class ToNatO   a where natO   ∷ a → 𝑂 ℕ
class ToNatO64 a where natO64 ∷ a → 𝑂 ℕ64
class ToNatO32 a where natO32 ∷ a → 𝑂 ℕ32
class ToNatO16 a where natO16 ∷ a → 𝑂 ℕ16
class ToNatO8  a where natO8  ∷ a → 𝑂 ℕ8

natΩ ∷ (ToNatO a,STACK) ⇒ a → ℕ
natΩ :: forall a. (ToNatO a, STACK) => a -> ℕ
natΩ a
x = case a -> 𝑂 ℕ
forall a. ToNatO a => a -> 𝑂 ℕ
natO a
x of {𝑂 ℕ
None → 𝕊 -> ℕ
forall a. STACK => 𝕊 -> a
error 𝕊
"failed natΩ conversion";Some ℕ
n → ℕ
n}
natΩ64 ∷ (ToNatO64 a,STACK) ⇒ a → ℕ64
natΩ64 :: forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 a
x = case a -> 𝑂 ℕ64
forall a. ToNatO64 a => a -> 𝑂 ℕ64
natO64 a
x of {𝑂 ℕ64
None → 𝕊 -> ℕ64
forall a. STACK => 𝕊 -> a
error 𝕊
"failed natΩ64 conversion";Some ℕ64
n → ℕ64
n}
natΩ32 ∷ (ToNatO32 a,STACK) ⇒ a → ℕ32
natΩ32 :: forall a. (ToNatO32 a, STACK) => a -> ℕ32
natΩ32 a
x = case a -> 𝑂 ℕ32
forall a. ToNatO32 a => a -> 𝑂 ℕ32
natO32 a
x of {𝑂 ℕ32
None → 𝕊 -> ℕ32
forall a. STACK => 𝕊 -> a
error 𝕊
"failed natΩ32 conversion";Some ℕ32
n → ℕ32
n}
natΩ16 ∷ (ToNatO16 a,STACK) ⇒ a → ℕ16
natΩ16 :: forall a. (ToNatO16 a, STACK) => a -> ℕ16
natΩ16 a
x = case a -> 𝑂 ℕ16
forall a. ToNatO16 a => a -> 𝑂 ℕ16
natO16 a
x of {𝑂 ℕ16
None → 𝕊 -> ℕ16
forall a. STACK => 𝕊 -> a
error 𝕊
"failed natΩ16 conversion";Some ℕ16
n → ℕ16
n}
natΩ8 ∷ (ToNatO8 a,STACK) ⇒ a → ℕ8
natΩ8 :: forall a. (ToNatO8 a, STACK) => a -> ℕ8
natΩ8 a
x = case a -> 𝑂 ℕ8
forall a. ToNatO8 a => a -> 𝑂 ℕ8
natO8 a
x of {𝑂 ℕ8
None → 𝕊 -> ℕ8
forall a. STACK => 𝕊 -> a
error 𝕊
"failed natΩ8 conversion";Some ℕ8
n → ℕ8
n}

class ToInt   a where int   ∷ a → ℤ
class ToInt64 a where int64 ∷ a → ℤ64
class ToInt32 a where int32 ∷ a → ℤ32
class ToInt16 a where int16 ∷ a → ℤ16
class ToInt8  a where int8  ∷ a → ℤ8

class ToIntO   a where intO   ∷ a → 𝑂 ℤ
class ToIntO64 a where intO64 ∷ a → 𝑂 ℤ64
class ToIntO32 a where intO32 ∷ a → 𝑂 ℤ32
class ToIntO16 a where intO16 ∷ a → 𝑂 ℤ16
class ToIntO8  a where intO8  ∷ a → 𝑂 ℤ8

intΩ ∷ (ToIntO a,STACK) ⇒ a → ℤ
intΩ :: forall a. (ToIntO a, STACK) => a -> ℤ
intΩ a
x = case a -> 𝑂 ℤ
forall a. ToIntO a => a -> 𝑂 ℤ
intO a
x of {𝑂 ℤ
None → 𝕊 -> ℤ
forall a. STACK => 𝕊 -> a
error 𝕊
"failed intΩ6";Some ℤ
n → ℤ
n}
intΩ64 ∷ (ToIntO64 a,STACK) ⇒ a → ℤ64
intΩ64 :: forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 a
x = case a -> 𝑂 ℤ64
forall a. ToIntO64 a => a -> 𝑂 ℤ64
intO64 a
x of {𝑂 ℤ64
None → 𝕊 -> ℤ64
forall a. STACK => 𝕊 -> a
error 𝕊
"failed intΩ64 conversion";Some ℤ64
n → ℤ64
n}
intΩ32 ∷ (ToIntO32 a,STACK) ⇒ a → ℤ32
intΩ32 :: forall a. (ToIntO32 a, STACK) => a -> ℤ32
intΩ32 a
x = case a -> 𝑂 ℤ32
forall a. ToIntO32 a => a -> 𝑂 ℤ32
intO32 a
x of {𝑂 ℤ32
None → 𝕊 -> ℤ32
forall a. STACK => 𝕊 -> a
error 𝕊
"failed intΩ32 conversion";Some ℤ32
n → ℤ32
n}
intΩ16 ∷ (ToIntO16 a,STACK) ⇒ a → ℤ16
intΩ16 :: forall a. (ToIntO16 a, STACK) => a -> ℤ16
intΩ16 a
x = case a -> 𝑂 ℤ16
forall a. ToIntO16 a => a -> 𝑂 ℤ16
intO16 a
x of {𝑂 ℤ16
None → 𝕊 -> ℤ16
forall a. STACK => 𝕊 -> a
error 𝕊
"failed intΩ16 conversion";Some ℤ16
n → ℤ16
n}
intΩ8 ∷ (ToIntO8 a,STACK) ⇒ a → ℤ8
intΩ8 :: forall a. (ToIntO8 a, STACK) => a -> ℤ8
intΩ8 a
x = case a -> 𝑂 ℤ8
forall a. ToIntO8 a => a -> 𝑂 ℤ8
intO8 a
x of {𝑂 ℤ8
None → 𝕊 -> ℤ8
forall a. STACK => 𝕊 -> a
error 𝕊
"failed intΩ8 conversion";Some ℤ8
n → ℤ8
n}

class ToRational a where rat ∷ a → ℚ
class ToRationalO a where ratO ∷ a → 𝑂 ℚ

class ToRationalᴾ a where ratᴾ ∷ a → ℚᴾ
class ToRationalᴾO a where ratᴾO ∷ a → 𝑂 ℚᴾ

class ToDouble a where dbl ∷ a → 𝔻
class ToDoubleO a where dblO ∷ a → 𝑂 𝔻

class ToDoubleᴾ a where dblᴾ ∷ a → 𝔻ᴾ
class ToDoubleᴾO a where dblᴾO ∷ a → 𝑂 𝔻ᴾ

class ToNumber a where num ∷ a → ℝ

class ToNumberᴾ a where numᴾ ∷ a → ℝᴾ
class ToNumberᴾO a where numᴾO ∷ a → 𝑂 ℝᴾ

ratΩ ∷ (ToRationalO a,STACK) ⇒ a → ℚ
ratΩ :: forall a. (ToRationalO a, STACK) => a -> ℚ
ratΩ a
x = case a -> 𝑂 ℚ
forall a. ToRationalO a => a -> 𝑂 ℚ
ratO a
x of {𝑂 ℚ
None → 𝕊 -> ℚ
forall a. STACK => 𝕊 -> a
error 𝕊
"failed ratΩ conversion";Some ℚ
n → ℚ
n}

ratᴾΩ ∷ (ToRationalᴾO a,STACK) ⇒ a → ℚᴾ
ratᴾΩ :: forall a. (ToRationalᴾO a, STACK) => a -> ℚᴾ
ratᴾΩ a
x = case a -> 𝑂 ℚᴾ
forall a. ToRationalᴾO a => a -> 𝑂 ℚᴾ
ratᴾO a
x of {𝑂 ℚᴾ
None → 𝕊 -> ℚᴾ
forall a. STACK => 𝕊 -> a
error 𝕊
"failed ratᴾΩ conversion";Some ℚᴾ
n → ℚᴾ
n}

dblΩ ∷ (ToDoubleO a,STACK) ⇒ a → 𝔻
dblΩ :: forall a. (ToDoubleO a, STACK) => a -> 𝔻
dblΩ a
x = case a -> 𝑂 𝔻
forall a. ToDoubleO a => a -> 𝑂 𝔻
dblO a
x of {𝑂 𝔻
None → 𝕊 -> 𝔻
forall a. STACK => 𝕊 -> a
error 𝕊
"failed dblΩ conversion";Some 𝔻
n → 𝔻
n}

dblᴾΩ ∷ (ToDoubleᴾO a,STACK) ⇒ a → 𝔻ᴾ
dblᴾΩ :: forall a. (ToDoubleᴾO a, STACK) => a -> 𝔻ᴾ
dblᴾΩ a
x = case a -> 𝑂 𝔻ᴾ
forall a. ToDoubleᴾO a => a -> 𝑂 𝔻ᴾ
dblᴾO a
x of {𝑂 𝔻ᴾ
None → 𝕊 -> 𝔻ᴾ
forall a. STACK => 𝕊 -> a
error 𝕊
"failed dblᴾΩ conversion";Some 𝔻ᴾ
n → 𝔻ᴾ
n}

numᴾΩ ∷ (ToNumberᴾO a,STACK) ⇒ a → ℝᴾ
numᴾΩ :: forall a. (ToNumberᴾO a, STACK) => a -> ℝᴾ
numᴾΩ a
x = case a -> 𝑂 ℝᴾ
forall a. ToNumberᴾO a => a -> 𝑂 ℝᴾ
numᴾO a
x of {𝑂 ℝᴾ
None → 𝕊 -> ℝᴾ
forall a. STACK => 𝕊 -> a
error 𝕊
"failed numᴾΩ conversion";Some ℝᴾ
n → ℝᴾ
n}