Theory SI_Pretty

section ‹ Parsing and Pretty Printing of SI Units ›

theory SI_Pretty
  imports SI
begin

subsection ‹ Syntactic SI Units ›

text ‹ The following syntactic representation can apply at both the type and value level. ›

nonterminal si

syntax
  "_si_metre"    :: "si" ("m")
  "_si_kilogram" :: "si" ("kg")
  "_si_second"   :: "si" ("s")
  "_si_ampere"   :: "si" ("A")
  "_si_kelvin"   :: "si" ("K")
  "_si_mole"     :: "si" ("mol")
  "_si_candela"  :: "si" ("cd")

  "_si_square"      :: "si ⇒ si" ("(_)⇧2" [999] 999)
  "_si_cube"        :: "si ⇒ si" ("(_)⇧3" [999] 999)
  "_si_quart"       :: "si ⇒ si" ("(_)⇧4" [999] 999)

  "_si_inverse"     :: "si ⇒ si" ("(_⇧-⇧1)" [999] 999)
  "_si_invsquare"   :: "si ⇒ si" ("(_)⇧-⇧2" [999] 999)
  "_si_invcube"     :: "si ⇒ si" ("(_)⇧-⇧3" [999] 999)
  "_si_invquart"    :: "si ⇒ si" ("(_)⇧-⇧4" [999] 999)

  "_si_times"    :: "si ⇒ si ⇒ si" (infixl "⋅" 70)

subsection ‹ Type Notation ›

text ‹ Pretty notation for SI units at the type level. ›

no_type_notation SIUnitT ("_[_]" [999,0] 999)

syntax
  "_si_unit"        :: "type ⇒ si ⇒ type" ("_[_]" [999,0] 999)
  "_si_print"       :: "type ⇒ si" ("SIPRINT'(_')")

translations
  (type) "'a[SIPRINT('d)]" == (type) "'a['d, SI]"
  (si) "SIPRINT('d)⇧2" == (si) "SIPRINT('d⇧2)"
  (si) "SIPRINT('d)⇧3" == (si) "SIPRINT('d⇧3)"
  (si) "SIPRINT('d)⇧4" == (si) "SIPRINT('d⇧4)"
  (si) "SIPRINT('d)⇧-⇧1" == (si) "SIPRINT('d⇧-⇧1)"
  (si) "SIPRINT('d)⇧-⇧2" == (si) "SIPRINT('d⇧-⇧2)"
  (si) "SIPRINT('d)⇧-⇧3" == (si) "SIPRINT('d⇧-⇧3)"
  (si) "SIPRINT('d)⇧-⇧4" == (si) "SIPRINT('d⇧-⇧4)"
  (si) "SIPRINT('d⇩1) ⋅ SIPRINT('d⇩2)" == (si) "SIPRINT('d⇩1 ⋅ 'd⇩2)"
  (si) "m"   == (si) "SIPRINT(L)"
  (si) "kg"  == (si) "SIPRINT(M)"
  (si) "s"   == (si) "SIPRINT(T)"
  (si) "A"   == (si) "SIPRINT(I)"
  (si) "K"   == (si) "SIPRINT(Θ)"
  (si) "mol" == (si) "SIPRINT(N)"
  (si) "cd"  == (si) "SIPRINT(J)"

  "_si_invsquare x" <= "_si_inverse (_si_square x)"
  "_si_invcube x" <= "_si_inverse (_si_cube x)"
  "_si_invquart x" <= "_si_inverse (_si_quart x)"

  "_si_invsquare x" <= "_si_square (_si_inverse x)"
  "_si_invcube x" <= "_si_cube (_si_inverse  x)"
  "_si_invquart x" <= "_si_quart (_si_inverse x)"

typ "real[m⋅s⇧-⇧2]"
typ "real[m⋅s⇧-⇧2⋅A⇧2]"
term "5 *⇩Q joule"

subsection ‹ Value Notations ›

text ‹ Pretty notation for SI units at the type level. Currently, it is not possible to support
  prefixes, as this would require a more sophisticated cartouche parser. ›

definition "SIQ n u = n *⇩Q u"

syntax
  "_si_term"        :: "si ⇒ logic" ("SI'(_')")
  "_siq_term"       :: "logic ⇒ si ⇒ logic" ("SI[_, _]")
  "_siq_print"      :: "logic ⇒ si"

translations
  "_siq_term n u" => "CONST SIQ n (_si_term u)"
  "_siq_term n (_siq_print u)" <= "CONST SIQ n u"
  "_si_term (_si_times x y)" == "(_si_term x) ❙⋅ (_si_term y)"
  "_si_term (_si_inverse x)" == "(_si_term x)⇧-⇧𝟭"
  "_si_term (_si_square x)" == "(_si_term x)⇧𝟮"
  "_si_term (_si_cube x)" == "(_si_term x)⇧𝟮"
  "SI(m)"   => "CONST metre"
  "SI(kg)"  => "CONST kilogram"
  "SI(s)"   => "CONST second"
  "SI(A)"   => "CONST ampere"
  "SI(K)"   => "CONST kelvin"
  "SI(mol)" => "CONST mole"
  "SI(cd)"  => "CONST candela"

  "_si_inverse (_siq_print x)" <= "_siq_print (x⇧-⇧𝟭)"
  "_si_invsquare (_siq_print x)" <= "_siq_print (x⇧-⇧𝟮)"
  "_si_invcube (_siq_print x)" <= "_siq_print (x⇧-⇧𝟯)"
  "_si_invquart (_siq_print x)" <= "_siq_print (x⇧-⇧𝟰)"

  "_si_square (_siq_print x)" <= "_siq_print (x⇧𝟮)"
  "_si_cube (_siq_print x)" <= "_siq_print (x⇧𝟯)"
  "_si_quart (_siq_print x)" <= "_siq_print (x⇧𝟰)"
  "_si_times (_siq_print x) (_siq_print y)" <= "_siq_print (x ❙⋅ y)"

  "_si_metre" <= "_siq_print (CONST metre)"
  "_si_kilogram" <= "_siq_print (CONST kilogram)"
  "_si_second" <= "_siq_print (CONST second)"
  "_si_ampere" <= "_siq_print (CONST ampere)"
  "_si_kelvin" <= "_siq_print (CONST kelvin)"
  "_si_mole" <= "_siq_print (CONST mole)"
  "_si_candela" <= "_siq_print (CONST candela)"

term "SI[5, m⇧2]"
term "SI[22, m⋅s⇧-⇧1]"

end