(*
* Example of using dimensions as units. This doesn't do any automatic conversion between
* different units of the same dimension, but given the perils of floating-point arithmetic,
* that's probably just as well.
*)
(* Declare a new dimension "FT" *)
indexconstant FT : dim
(* Declare a value to introduce FT *)
primitive val FT : real[FT] = "1.0"
val metersPerFoot : real[M / FT]
val metersPerFoot = (0.3048 * M) / FT
val fromFeet : real[FT] -> real[M]
fun fromFeet ft = ft * metersPerFoot
val toFeet : real[M] -> real[FT]
fun toFeet m = m / metersPerFoot
val readDistance : real[NODIM] -> string -> real[M]
fun readDistance number units =
case units of
"m" => number * M
| "ft" => fromFeet (number * FT)
| _ => raise BadInput ("unknown distance unit: "^units)
val metersToString : real[M] -> string
fun metersToString number =
Real.toString (number / M) ^ " m"
val _ = print ("1000.0 ft = " ^ metersToString (readDistance 1000.0 "ft") ^ "\n")
val _ = print ("10.0 m = " ^ metersToString (readDistance 10.0 "m") ^ "\n")