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