1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Code_Natural.thy	Mon Jul 26 11:10:35 2010 +0200
     1.3 @@ -0,0 +1,145 @@
     1.4 +(*  Title:      HOL/Library/Code_Natural.thy
     1.5 +    Author:     Florian Haftmann, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +theory Code_Natural
     1.9 +imports Main
    1.10 +begin
    1.11 +
    1.12 +section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
    1.13 +
    1.14 +code_include Haskell "Natural"
    1.15 +{*import Data.Array.ST;
    1.16 +
    1.17 +newtype Natural = Natural Integer deriving (Eq, Show, Read);
    1.18 +
    1.19 +instance Num Natural where {
    1.20 +  fromInteger k = Natural (if k >= 0 then k else 0);
    1.21 +  Natural n + Natural m = Natural (n + m);
    1.22 +  Natural n - Natural m = fromInteger (n - m);
    1.23 +  Natural n * Natural m = Natural (n * m);
    1.24 +  abs n = n;
    1.25 +  signum _ = 1;
    1.26 +  negate n = error "negate Natural";
    1.27 +};
    1.28 +
    1.29 +instance Ord Natural where {
    1.30 +  Natural n <= Natural m = n <= m;
    1.31 +  Natural n < Natural m = n < m;
    1.32 +};
    1.33 +
    1.34 +instance Ix Natural where {
    1.35 +  range (Natural n, Natural m) = map Natural (range (n, m));
    1.36 +  index (Natural n, Natural m) (Natural q) = index (n, m) q;
    1.37 +  inRange (Natural n, Natural m) (Natural q) = inRange (n, m) q;
    1.38 +  rangeSize (Natural n, Natural m) = rangeSize (n, m);
    1.39 +};
    1.40 +
    1.41 +instance Real Natural where {
    1.42 +  toRational (Natural n) = toRational n;
    1.43 +};
    1.44 +
    1.45 +instance Enum Natural where {
    1.46 +  toEnum k = fromInteger (toEnum k);
    1.47 +  fromEnum (Natural n) = fromEnum n;
    1.48 +};
    1.49 +
    1.50 +instance Integral Natural where {
    1.51 +  toInteger (Natural n) = n;
    1.52 +  divMod n m = quotRem n m;
    1.53 +  quotRem (Natural n) (Natural m)
    1.54 +    | (m == 0) = (0, Natural n)
    1.55 +    | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
    1.56 +};*}
    1.57 +
    1.58 +code_reserved Haskell Natural
    1.59 +
    1.60 +code_include Scala "Natural" {*
    1.61 +import scala.Math
    1.62 +
    1.63 +object Natural {
    1.64 +
    1.65 +  def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
    1.66 +  def apply(numeral: Int): Natural = Natural(BigInt(numeral))
    1.67 +  def apply(numeral: String): Natural = Natural(BigInt(numeral))
    1.68 +
    1.69 +}
    1.70 +
    1.71 +class Natural private(private val value: BigInt) {
    1.72 +
    1.73 +  override def hashCode(): Int = this.value.hashCode()
    1.74 +
    1.75 +  override def equals(that: Any): Boolean = that match {
    1.76 +    case that: Natural => this equals that
    1.77 +    case _ => false
    1.78 +  }
    1.79 +
    1.80 +  override def toString(): String = this.value.toString
    1.81 +
    1.82 +  def equals(that: Natural): Boolean = this.value == that.value
    1.83 +
    1.84 +  def as_BigInt: BigInt = this.value
    1.85 +  def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
    1.86 +      this.value.intValue
    1.87 +    else error("Int value out of range: " + this.value.toString)
    1.88 +
    1.89 +  def +(that: Natural): Natural = new Natural(this.value + that.value)
    1.90 +  def -(that: Natural): Natural = Natural(this.value - that.value)
    1.91 +  def *(that: Natural): Natural = new Natural(this.value * that.value)
    1.92 +
    1.93 +  def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
    1.94 +    else {
    1.95 +      val (k, l) = this.value /% that.value
    1.96 +      (new Natural(k), new Natural(l))
    1.97 +    }
    1.98 +
    1.99 +  def <=(that: Natural): Boolean = this.value <= that.value
   1.100 +
   1.101 +  def <(that: Natural): Boolean = this.value < that.value
   1.102 +
   1.103 +}
   1.104 +*}
   1.105 +
   1.106 +code_reserved Scala Natural
   1.107 +
   1.108 +code_type code_numeral
   1.109 +  (Haskell "Natural.Natural")
   1.110 +  (Scala "Natural")
   1.111 +
   1.112 +setup {*
   1.113 +  fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
   1.114 +    false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
   1.115 +*}
   1.116 +
   1.117 +code_instance code_numeral :: eq
   1.118 +  (Haskell -)
   1.119 +
   1.120 +code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   1.121 +  (Haskell infixl 6 "+")
   1.122 +  (Scala infixl 7 "+")
   1.123 +
   1.124 +code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   1.125 +  (Haskell infixl 6 "-")
   1.126 +  (Scala infixl 7 "-")
   1.127 +
   1.128 +code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   1.129 +  (Haskell infixl 7 "*")
   1.130 +  (Scala infixl 8 "*")
   1.131 +
   1.132 +code_const div_mod_code_numeral
   1.133 +  (Haskell "divMod")
   1.134 +  (Scala infixl 8 "/%")
   1.135 +
   1.136 +code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   1.137 +  (Haskell infixl 4 "==")
   1.138 +  (Scala infixl 5 "==")
   1.139 +
   1.140 +code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   1.141 +  (Haskell infix 4 "<=")
   1.142 +  (Scala infixl 4 "<=")
   1.143 +
   1.144 +code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   1.145 +  (Haskell infix 4 "<")
   1.146 +  (Scala infixl 4 "<")
   1.147 +
   1.148 +end