1/* Title: Pure/General/value.scala 2 Author: Makarius 3 4Plain values, represented as string. 5*/ 6 7package isabelle 8 9 10object Value 11{ 12 object Boolean 13 { 14 def apply(x: scala.Boolean): java.lang.String = x.toString 15 def unapply(s: java.lang.String): Option[scala.Boolean] = 16 s match { 17 case "true" => Some(true) 18 case "false" => Some(false) 19 case _ => None 20 } 21 def parse(s: java.lang.String): scala.Boolean = 22 unapply(s) getOrElse error("Bad boolean: " + quote(s)) 23 } 24 25 object Nat 26 { 27 def unapply(s: java.lang.String): Option[scala.Int] = 28 s match { 29 case Int(n) if n >= 0 => Some(n) 30 case _ => None 31 } 32 def parse(s: java.lang.String): scala.Int = 33 unapply(s) getOrElse error("Bad natural number: " + quote(s)) 34 } 35 36 object Int 37 { 38 def apply(x: scala.Int): java.lang.String = Library.signed_string_of_int(x) 39 def unapply(s: java.lang.String): Option[scala.Int] = 40 try { Some(Integer.parseInt(s)) } 41 catch { case _: NumberFormatException => None } 42 def parse(s: java.lang.String): scala.Int = 43 unapply(s) getOrElse error("Bad integer: " + quote(s)) 44 } 45 46 object Long 47 { 48 def apply(x: scala.Long): java.lang.String = Library.signed_string_of_long(x) 49 def unapply(s: java.lang.String): Option[scala.Long] = 50 try { Some(java.lang.Long.parseLong(s)) } 51 catch { case _: NumberFormatException => None } 52 def parse(s: java.lang.String): scala.Long = 53 unapply(s) getOrElse error("Bad integer: " + quote(s)) 54 } 55 56 object Double 57 { 58 def apply(x: scala.Double): java.lang.String = x.toString 59 def unapply(s: java.lang.String): Option[scala.Double] = 60 try { Some(java.lang.Double.parseDouble(s)) } 61 catch { case _: NumberFormatException => None } 62 def parse(s: java.lang.String): scala.Double = 63 unapply(s) getOrElse error("Bad real: " + quote(s)) 64 } 65 66 object Seconds 67 { 68 def apply(t: Time): java.lang.String = 69 { 70 val s = t.seconds 71 if (s.toInt.toDouble == s) s.toInt.toString else t.toString 72 } 73 def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds(_)) 74 def parse(s: java.lang.String): Time = 75 unapply(s) getOrElse error("Bad real (for seconds): " + quote(s)) 76 } 77} 78