/* SI Prelude */
//: SI Units
type normal Second  :: Unit; //Unit is the Kind of SI Unit types.
type normal Metre   :: Unit; //Kinds do not need to be declared before use.
type normal Gram    :: Unit;
type normal Ampere  :: Unit;
type normal Kelvin  :: Unit;
type normal Mole    :: Unit;
type normal Candela :: Unit;

//: Imperial & Misc. Units
type Feet :: Unit;
forall u:Feet::Unit. Feet => Metre  = 0.3048*u :: Unit;
forall u:Metre::Unit. Metre => Feet  = u/0.3048 :: Unit;

type Yard :: Unit;
forall u:Yard::Unit. Yard => Metre  = 0.9144*u :: Unit;
forall u:Metre::Unit. Metre => Yard  = u/0.9144 :: Unit;

type Mile :: Unit;
forall u:Mile::Unit. Mile => Metre  = 1609.34*u :: Unit;
forall u:Metre::Unit. Metre => Mile  = u/1609.34 :: Unit;

type Minute :: Unit;
forall u:Minute::Unit. Minute => Second  = 60*u :: Unit;
forall u:Second::Unit. Second => Minute  = u/60 :: Unit;

type Hour :: Unit;
forall u:Hour::Unit. Hour => Second  = 3600*u :: Unit;
forall u:Second::Unit. Second => Hour  = u/3600 :: Unit;

//: Dimensionless Units
type normal Radian    :: Unit;
type normal Steradian :: Unit;

//: SI Derived Units (source: https://www.ece.utoronto.ca/canadian-metric-association/si-derived-units/)
type Hertz: ()/Second :: Unit;
type Newton: Metre*Kilo<Gram>/Second*Second :: Unit;
type Pascal: Kilo<Gram>/Metre*Second*Second :: Unit;
type Joule: Kilo<Gram>*Metre*Metre/Second*Second :: Unit;
type Watt: Kilo<Gram>*Metre*Metre/Second*Second*Second :: Unit;
type Coulomb: Ampere*Second :: Unit; //The constant value of a Coulomb is no longer exactly 1 Ampere Second but the Unit remains unchanged
type Volt: Kilo<Gram>*Metre*Metre/Ampere*Second*Second*Second :: Unit;
type Ohm: Kilo<Gram>*Metre*Metre/Ampere*Ampere*Second*Second*Second :: Unit;
type Siemens: Ampere*Ampere*Second*Second*Second/Kilo<Gram>*Metre*Metre :: Unit;
type Farad: Ampere*Ampere*Second*Second*Second*Second/Kilo<Gram>*Metre*Metre :: Unit;
type Tesla: Kilo<Gram>/Ampere*Second*Second :: Unit;
type Weber: Kilo<Gram>*Metre*Metre/Ampere*Second*Second :: Unit;
type Henry: Kilo<Gram>*Metre*Metre/Ampere*Ampere*Second*Second :: Unit;
type Lumen: Candela*Steradian :: Unit;
type Lux: Candela*Steradian/Metre*Metre :: Unit;
type Becquerel: ()/Second :: Unit;
type Gray: Metre*Metre/Second*Second :: Unit;
type Sievert: Metre*Metre/Second*Second :: Unit;
type SquareMetre: Metre*Metre :: Unit;
type CubicMetre: Metre*Metre*Metre :: Unit;
type Speed: Metre/Second :: Unit;
type Acceleration: Metre/Second*Second :: Unit;
type Jerk: Metre/Second*Second*Second :: Unit;
type Wavenumber: ()/Metre :: Unit;
type Density: Kilo<Gram>/Metre*Metre*Metre :: Unit;
type SurfaceDensity: Kilo<Gram>/Metre*Metre :: Unit;
type SpecificVolume: Metre*Metre*Metre/Kilo<Gram> :: Unit;
type CurrentDensity: Ampere/Metre*Metre :: Unit;
type MagneticFieldStrength: Ampere/Metre :: Unit;
type Concentration: Mole/Metre*Metre*Metre :: Unit;
type MassConcentration: Kilo<Gram>/Metre*Metre*Metre :: Unit;
type Luminance: Candela/Metre*Metre :: Unit;
type RefractiveIndex :: Unit;
type RelativePermeability :: Unit;

//: SI Metric Prefixes
type Yotta<U::Unit> :: Unit;
type Zetta<U::Unit> :: Unit;
type Exa<U::Unit> :: Unit;
type Peta<U::Unit> :: Unit;
type Tera<U::Unit> :: Unit;
type Giga<U::Unit> :: Unit;
type Mega<U::Unit> :: Unit;
type Kilo<U::Unit> :: Unit;
type Hecto<U::Unit> :: Unit;
type Deca<U::Unit> :: Unit;

type Deci<U::Unit> :: Unit;
type Centi<U::Unit> :: Unit;
type Milli<U::Unit> :: Unit;
type Micro<U::Unit> :: Unit;
type Nano<U::Unit> :: Unit;
type Pico<U::Unit> :: Unit;
type Femto<U::Unit> :: Unit;
type Atto<U::Unit> :: Unit;
type Zepto<U::Unit> :: Unit;
type Yocto<U::Unit> :: Unit;

//: SI Metric Prefixes, boxing
forall u:U::Unit. U => Yotta<U> = 1000000000000000000000000 * u :: Unit;
forall u:U::Unit. U => Zetta<U> = 1000000000000000000000 * u :: Unit;
forall u:U::Unit. U => Exa<U>   = 1000000000000000000 * u :: Unit;
forall u:U::Unit. U => Peta<U>  = 1000000000000000 * u :: Unit;
forall u:U::Unit. U => Tera<U>  = 1000000000000 * u :: Unit;
forall u:U::Unit. U => Giga<U>  = 1000000000 * u :: Unit;
forall u:U::Unit. U => Mega<U>  = 1000000 * u :: Unit;
forall u:U::Unit. U => Kilo<U>  = 1000 * u :: Unit;
forall u:U::Unit. U => Hecto<U> = 100 * u :: Unit;
forall u:U::Unit. U => Deca<U>  = 10 * u :: Unit;

forall u:U::Unit. U => Deci<U>  = u / 10 :: Unit;
forall u:U::Unit. U => Centi<U> = u / 100 :: Unit;
forall u:U::Unit. U => Milli<U> = u / 1000 :: Unit;
forall u:U::Unit. U => Micro<U> = u / 1000000 :: Unit;
forall u:U::Unit. U => Nano<U>  = u / 1000000000 :: Unit;
forall u:U::Unit. U => Pico<U>  = u / 1000000000000 :: Unit;
forall u:U::Unit. U => Femto<U> = u / 1000000000000000 :: Unit;
forall u:U::Unit. U => Atto<U>  = u / 1000000000000000000 :: Unit;
forall u:U::Unit. U => Zepto<U> = u / 1000000000000000000000 :: Unit;
forall u:U::Unit. U => Yocto<U> = u / 1000000000000000000000000 :: Unit;

//: SI Metric Prefixes, unboxing
forall u:Yotta<U>::Unit. Yotta<U> => U = u / 1000000000000000000000000 :: Unit;
forall u:Zetta<U>::Unit. Zetta<U> => U = u / 1000000000000000000000 :: Unit;
forall u:Exa<U>::Unit.   Exa<U>   => U = u / 1000000000000000000 :: Unit;
forall u:Peta<U>::Unit.  Peta<U>  => U = u / 1000000000000000 :: Unit;
forall u:Tera<U>::Unit.  Tera<U>  => U = u / 1000000000000 :: Unit;
forall u:Giga<U>::Unit.  Giga<U>  => U = u / 1000000000 :: Unit;
forall u:Mega<U>::Unit.  Mega<U>  => U = u / 1000000 :: Unit;
forall u:Kilo<U>::Unit.  Kilo<U>  => U = u / 1000 :: Unit;
forall u:Hecto<U>::Unit. Hecto<U> => U = u / 100 :: Unit;
forall u:Deca<U>::Unit.  Deca<U>  => U = u / 10 :: Unit;

forall u:Deci<U>::Unit.  Deci<U>  => U = 10 * u :: Unit;
forall u:Centi<U>::Unit. Centi<U> => U = 100 * u :: Unit;
forall u:Milli<U>::Unit. Milli<U> => U = 1000 * u :: Unit;
forall u:Micro<U>::Unit. Micro<U> => U = 1000000 * u :: Unit;
forall u:Nano<U>::Unit.  Nano<U>  => U = 1000000000 * u :: Unit;
forall u:Pico<U>::Unit.  Pico<U>  => U = 1000000000000 * u :: Unit;
forall u:Femto<U>::Unit. Femto<U> => U = 1000000000000000 * u :: Unit;
forall u:Atto<U>::Unit.  Atto<U>  => U = 1000000000000000000 * u :: Unit;
forall u:Zepto<U>::Unit. Zepto<U> => U = 1000000000000000000000 * u :: Unit;
forall u:Yocto<U>::Unit. Yocto<U> => U = 1000000000000000000000000 * u :: Unit;

//: SI Constants
let si_c: Metre/Second = 299_792_458;      //speed of light in vacuum
let si_h: Joule*Second = 6.626_070_15e-34; //Planck constant
let si_e: Coulomb = 1.602_176_634e-19;     //elementary charge
let si_k: Joule/Kelvin = 1.380_649e-23;    //Boltzmann constant
let si_k_cd: Lumen/Watt = 683;             //luminous efficacy of a defined visible radiation
let si_n_A: ()/Mole = 6.022_140_76e23;     //Avogadro constant
let si_deltavCs: Hertz = 9_192_631_770;    //caesium hyperfine frequency

//: Unit Math
let pos(x:X::Unit)             :X   ::Unit; //pos
let neg(x:X::Unit)             :X   ::Unit; //neg
let $"+"(x:X::Unit, y:X::Unit) :X   ::Unit; //add
let $"-"(x:X::Unit, y:X::Unit) :X   ::Unit; //sub
let $"*"(x:X::Unit, y:Y::Unit) :X*Y ::Unit; //mul
let $"*"(x:Number, y:Y::Unit)  :Y   ::Unit; //mul constant
let $"*"(x:X::Unit, y:Number)  :X   ::Unit; //mul constant
let $"/"(x:X::Unit, y:Y::Unit) :X/Y ::Unit; //div
let $"/"(x:Number, y:Y::Unit)  :()/Y::Unit; //div constant
let $"/"(x:X::Unit, y:Number)  :X   ::Unit; //div constant