namespace http://cds.omdoc.org/physics❚

theory Quantities : ur:?LF =
   include examples?Real❙

   // the type of dimensions, e.g., time, length ❙
   dim : type❙
   scalar: dim❙
   mult_dim   : dim ⟶ dim ⟶ dim             ❘# 1 * 2❙
   inv_dim    : dim ⟶ dim                   ❘# 1 ⁻ prec 10❙

   div_dim    : dim ⟶ dim ⟶ dim ❘= [d,e] d*e⁻ ❘# 1 / 2❙
   square_dim : dim ⟶ dim❘= [d] d*d        ❘# 1 ² prec 10❙
   cube_dim   : dim ⟶ dim❘= [d] d*d*d      ❘# 1 ³ prec 10❙

   eq_dim     : dim ⟶ dim ⟶ type               ❘# 1 = 2 prec -10❘role Eq❙
   assoc      : {d:dim,e:dim,f:dim} d*(e*f)=(d*e)*f❙
   comm       : {d:dim,e:dim} d*e=e*d❙
   mult_scalar_right : {d} d*scalar = d        ❘role Simplify❙
   mult_scalar_left  : {d} scalar*d = d        ❘role Simplify❙
   mult_inv_right    : {d:dim} d*d⁻ = scalar   ❘role Simplify❙
   mult_inv_left     : {d:dim} d⁻*d = scalar   ❘role Simplify❙
   inv_mult   : {d:dim,e:dim} (d*e)⁻ = d⁻*e⁻   ❘role Simplify❙
   inv_inv    : {d} d⁻⁻ = d                    ❘role Simplify❙
   

   // the type of quantities of a certain dimension, e.g., 10 s, 100 m ❙
   quantity : dim ⟶ type❘# $ 1❙
   eq_quant : {d} $d ⟶ $d ⟶ type               ❘# 2 == 3 prec -10❘role Eq❙
   
   // the type of units of a dimension, e.g., second, meter
      units are functions that map real numbers to quantities ❙
   unit : dim ⟶ type❘ = [d] real ⟶ $d❙
   // takes a real number and a unit and makes the quantity
      e.g., 10'meter❙
   makeQuantity : {d} real ⟶ unit d ⟶ $ d❘ = [d,r,u] u r❘# 2 ' 3 prec 50❙
   
   // addition and subtraction quantities ❙
   add_quant : {d} $d ⟶ $d ⟶ $d  ❘# 2 ++ 3❙
   sub_quant : {d} $d ⟶ $d ⟶ $d  ❘# 2 -- 3❙
   
   add_quant_same_unit : {d,u: unit d, p, q} p'u ++ q'u == (p + q)'u❘ // role Simplify❙
   sub_quant_same_unit : {d,u: unit d, p, q} p'u -- q'u == (p - q)'u❘ // role Simplify❙

   // multiplication and division of dimensions, quantities, and units (should be imported from elsewhere) ❙
   mult_quant : {d,e} $d ⟶ $e ⟶ $(d * e)  ❘# 3 ** 4❙
   div_quant  : {d,e} $d ⟶ $e ⟶ $(d / e)  ❘# 3 // 4❙
   mult_unit  : {d,e} unit d ⟶ unit e ⟶ unit(d * e)  ❘# 3 ** 4❘
              = [d,e,u,v] [r] (r'u) ** (r'v)❙
   div_unit   : {d,e} unit d ⟶ unit e ⟶ unit(d / e)  ❘# 3 // 4❘
              = [d,e,u,v] [r] (r'u) // (r'v)❙

   mult_scalar : {d} real ⟶ $ d ⟶ $ d❘# 2 @ 3❙
   multiples_of: {d} $ d ⟶ unit d ❘= [d,q] [r] r @ q❘# multiples_of 2❙
❚

theory Dimensions : ur:?LF =
   include ?Quantities❙
   length : dim❙
   time   : dim❙
   mass   : dim❙
   temperature : dim❙

   area   : dim❘= length ²❙
   volume : dim❘ = length ³❙
   velocity : dim❘= length / time❙
   acceleration : dim❘ = length * time⁻²❙
   force : dim❘= mass * acceleration❙
   pressure : dim❘= force * length⁻²❙

❚

theory Prefixes : ur:?LF =
   include ?Dimensions❙
   // TODO ❙
   milli : {d} unit d ⟶ unit d❘ // = [d,u] [r] (r / 1000) ' u❘# milli 2❙
   centi : {d} unit d ⟶ unit d❘ // = [d,u] [r] (r / 100) ' u❘# centi 2❙
   deci  : {d} unit d ⟶ unit d❘ // = [d,u] [r] (r / 10) ' u❘# deci 2❙
❚
   
theory Units : ur:?LF =
   include ?Dimensions❙

   meter  : $ length❙
   second : $ time❙
   gramm  : $ mass❙

   meters  : unit length❘ = multiples_of meter❙
   seconds : unit time❘   = multiples_of second❙
   gramms  : unit mass❘   = multiples_of gramm❙
   
   kelvin  : $temperature❙
   kelvins : unit temperature❘ = multiples_of kelvin❙
❚

theory DerivedUnits : ur:?LF =
   include ?Prefixes❙
   include ?Units❙
   
   litre  : $ volume❘ // = (1 ' deci meters) ** (1 ' deci meters) ** (1 ' deci meters)❙
   litres : unit volume❘ = multiples_of litre❙
❚

theory CookingUnit : ur:?LF =
   include ?DerivedUnits❙
   
   tablespoon : $ volume❙
   teaspoon   : $ volume❙
   cup        : $ volume❙
   
   tablespoons : unit volume❘ = multiples_of (15 ' milli litres)❙
   teaspoons   : unit volume❘ = multiples_of (5 ' milli litres)❙
   
   cups        : unit volume❘ = multiples_of (250 ' milli litres)❙
❚

theory TimeUnits : ur:?LF =
   include ?Units❙
   minutes : unit time❘ = multiples_of (60 ' seconds)❙
   hours   : unit time❘ = multiples_of (60 ' minutes)❙
❚

theory TemperatureUnits : ur:?LF =
   include ?Units❙
   celsius    : unit temperature❘ //  = [r] (r+273+(15/100)) ' kelvins ❘ # 1 °C❙
   fahrenheit : unit temperature❘ //  = [r] (r-32)*5/9 °C  ❘ # 1 °F❙
❚