1 (* Title: HOL/Library/Code_Natural.thy
2 Author: Florian Haftmann, TU Muenchen
9 section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
11 code_include Haskell "Natural"
12 {*import Data.Array.ST;
14 newtype Natural = Natural Integer deriving (Eq, Show, Read);
16 instance Num Natural where {
17 fromInteger k = Natural (if k >= 0 then k else 0);
18 Natural n + Natural m = Natural (n + m);
19 Natural n - Natural m = fromInteger (n - m);
20 Natural n * Natural m = Natural (n * m);
23 negate n = error "negate Natural";
26 instance Ord Natural where {
27 Natural n <= Natural m = n <= m;
28 Natural n < Natural m = n < m;
31 instance Ix Natural where {
32 range (Natural n, Natural m) = map Natural (range (n, m));
33 index (Natural n, Natural m) (Natural q) = index (n, m) q;
34 inRange (Natural n, Natural m) (Natural q) = inRange (n, m) q;
35 rangeSize (Natural n, Natural m) = rangeSize (n, m);
38 instance Real Natural where {
39 toRational (Natural n) = toRational n;
42 instance Enum Natural where {
43 toEnum k = fromInteger (toEnum k);
44 fromEnum (Natural n) = fromEnum n;
47 instance Integral Natural where {
48 toInteger (Natural n) = n;
49 divMod n m = quotRem n m;
50 quotRem (Natural n) (Natural m)
51 | (m == 0) = (0, Natural n)
52 | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
55 code_reserved Haskell Natural
57 code_include Scala "Natural" {*
62 def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
63 def apply(numeral: Int): Natural = Natural(BigInt(numeral))
64 def apply(numeral: String): Natural = Natural(BigInt(numeral))
68 class Natural private(private val value: BigInt) {
70 override def hashCode(): Int = this.value.hashCode()
72 override def equals(that: Any): Boolean = that match {
73 case that: Natural => this equals that
77 override def toString(): String = this.value.toString
79 def equals(that: Natural): Boolean = this.value == that.value
81 def as_BigInt: BigInt = this.value
82 def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
84 else error("Int value out of range: " + this.value.toString)
86 def +(that: Natural): Natural = new Natural(this.value + that.value)
87 def -(that: Natural): Natural = Natural(this.value - that.value)
88 def *(that: Natural): Natural = new Natural(this.value * that.value)
90 def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
92 val (k, l) = this.value /% that.value
93 (new Natural(k), new Natural(l))
96 def <=(that: Natural): Boolean = this.value <= that.value
98 def <(that: Natural): Boolean = this.value < that.value
103 code_reserved Scala Natural
105 code_type code_numeral
106 (Haskell "Natural.Natural")
110 fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
111 false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
114 code_instance code_numeral :: eq
117 code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
118 (Haskell infixl 6 "+")
121 code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
122 (Haskell infixl 6 "-")
125 code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
126 (Haskell infixl 7 "*")
129 code_const div_mod_code_numeral
131 (Scala infixl 8 "/%")
133 code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
134 (Haskell infixl 4 "==")
135 (Scala infixl 5 "==")
137 code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
138 (Haskell infix 4 "<=")
139 (Scala infixl 4 "<=")
141 code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
142 (Haskell infix 4 "<")