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