src/HOL/Library/Code_Natural.thy
 author Christian Sternagel Thu Aug 30 15:44:03 2012 +0900 (2012-08-30) changeset 49093 fdc301f592c4 parent 47108 2a1953f0d20d permissions -rw-r--r--
 haftmann@37968 ` 1` ```(* Title: HOL/Library/Code_Natural.thy ``` haftmann@24999 ` 2` ``` Author: Florian Haftmann, TU Muenchen ``` haftmann@24999 ` 3` ```*) ``` haftmann@24999 ` 4` haftmann@37968 ` 5` ```theory Code_Natural ``` huffman@46547 ` 6` ```imports "../Main" ``` haftmann@24999 ` 7` ```begin ``` haftmann@24999 ` 8` haftmann@37968 ` 9` ```section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *} ``` haftmann@24999 ` 10` haftmann@37968 ` 11` ```code_include Haskell "Natural" ``` haftmann@38810 ` 12` ```{*import Data.Array.ST; ``` haftmann@38810 ` 13` haftmann@38810 ` 14` ```newtype Natural = Natural Integer deriving (Eq, Show, Read); ``` haftmann@37958 ` 15` haftmann@37958 ` 16` ```instance Num Natural where { ``` haftmann@37958 ` 17` ``` fromInteger k = Natural (if k >= 0 then k else 0); ``` haftmann@37958 ` 18` ``` Natural n + Natural m = Natural (n + m); ``` haftmann@37958 ` 19` ``` Natural n - Natural m = fromInteger (n - m); ``` haftmann@37958 ` 20` ``` Natural n * Natural m = Natural (n * m); ``` haftmann@37958 ` 21` ``` abs n = n; ``` haftmann@37958 ` 22` ``` signum _ = 1; ``` haftmann@37958 ` 23` ``` negate n = error "negate Natural"; ``` haftmann@37958 ` 24` ```}; ``` haftmann@37958 ` 25` haftmann@37958 ` 26` ```instance Ord Natural where { ``` haftmann@37958 ` 27` ``` Natural n <= Natural m = n <= m; ``` haftmann@37958 ` 28` ``` Natural n < Natural m = n < m; ``` haftmann@37958 ` 29` ```}; ``` haftmann@37958 ` 30` haftmann@37968 ` 31` ```instance Ix Natural where { ``` haftmann@37968 ` 32` ``` range (Natural n, Natural m) = map Natural (range (n, m)); ``` haftmann@37968 ` 33` ``` index (Natural n, Natural m) (Natural q) = index (n, m) q; ``` haftmann@37968 ` 34` ``` inRange (Natural n, Natural m) (Natural q) = inRange (n, m) q; ``` haftmann@37968 ` 35` ``` rangeSize (Natural n, Natural m) = rangeSize (n, m); ``` haftmann@37968 ` 36` ```}; ``` haftmann@37968 ` 37` haftmann@37958 ` 38` ```instance Real Natural where { ``` haftmann@37958 ` 39` ``` toRational (Natural n) = toRational n; ``` haftmann@37958 ` 40` ```}; ``` haftmann@37958 ` 41` haftmann@37958 ` 42` ```instance Enum Natural where { ``` haftmann@37958 ` 43` ``` toEnum k = fromInteger (toEnum k); ``` haftmann@37958 ` 44` ``` fromEnum (Natural n) = fromEnum n; ``` haftmann@37958 ` 45` ```}; ``` haftmann@37958 ` 46` haftmann@37958 ` 47` ```instance Integral Natural where { ``` haftmann@37958 ` 48` ``` toInteger (Natural n) = n; ``` haftmann@37958 ` 49` ``` divMod n m = quotRem n m; ``` haftmann@37958 ` 50` ``` quotRem (Natural n) (Natural m) ``` haftmann@37958 ` 51` ``` | (m == 0) = (0, Natural n) ``` haftmann@37958 ` 52` ``` | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m; ``` haftmann@37968 ` 53` ```};*} ``` haftmann@37958 ` 54` haftmann@38810 ` 55` haftmann@37958 ` 56` ```code_reserved Haskell Natural ``` haftmann@37958 ` 57` haftmann@38774 ` 58` ```code_include Scala "Natural" ``` haftmann@38968 ` 59` ```{*object Natural { ``` haftmann@37958 ` 60` haftmann@38968 ` 61` ``` def apply(numeral: BigInt): Natural = new Natural(numeral max 0) ``` haftmann@38968 ` 62` ``` def apply(numeral: Int): Natural = Natural(BigInt(numeral)) ``` haftmann@38968 ` 63` ``` def apply(numeral: String): Natural = Natural(BigInt(numeral)) ``` haftmann@37958 ` 64` haftmann@37958 ` 65` ```} ``` haftmann@37958 ` 66` haftmann@38968 ` 67` ```class Natural private(private val value: BigInt) { ``` haftmann@37958 ` 68` haftmann@37958 ` 69` ``` override def hashCode(): Int = this.value.hashCode() ``` haftmann@37958 ` 70` haftmann@37958 ` 71` ``` override def equals(that: Any): Boolean = that match { ``` haftmann@38968 ` 72` ``` case that: Natural => this equals that ``` haftmann@37958 ` 73` ``` case _ => false ``` haftmann@37958 ` 74` ``` } ``` haftmann@37958 ` 75` haftmann@37958 ` 76` ``` override def toString(): String = this.value.toString ``` haftmann@37958 ` 77` haftmann@38968 ` 78` ``` def equals(that: Natural): Boolean = this.value == that.value ``` haftmann@37958 ` 79` haftmann@37958 ` 80` ``` def as_BigInt: BigInt = this.value ``` haftmann@39781 ` 81` ``` def as_Int: Int = if (this.value >= scala.Int.MinValue && this.value <= scala.Int.MaxValue) ``` haftmann@37958 ` 82` ``` this.value.intValue ``` haftmann@37968 ` 83` ``` else error("Int value out of range: " + this.value.toString) ``` haftmann@37958 ` 84` haftmann@38968 ` 85` ``` def +(that: Natural): Natural = new Natural(this.value + that.value) ``` haftmann@38968 ` 86` ``` def -(that: Natural): Natural = Natural(this.value - that.value) ``` haftmann@38968 ` 87` ``` def *(that: Natural): Natural = new Natural(this.value * that.value) ``` haftmann@37958 ` 88` haftmann@38968 ` 89` ``` def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this) ``` haftmann@37958 ` 90` ``` else { ``` haftmann@37958 ` 91` ``` val (k, l) = this.value /% that.value ``` haftmann@38968 ` 92` ``` (new Natural(k), new Natural(l)) ``` haftmann@37958 ` 93` ``` } ``` haftmann@37958 ` 94` haftmann@38968 ` 95` ``` def <=(that: Natural): Boolean = this.value <= that.value ``` haftmann@37958 ` 96` haftmann@38968 ` 97` ``` def <(that: Natural): Boolean = this.value < that.value ``` haftmann@37958 ` 98` haftmann@37958 ` 99` ```} ``` haftmann@37958 ` 100` ```*} ``` haftmann@37958 ` 101` haftmann@37958 ` 102` ```code_reserved Scala Natural ``` haftmann@37958 ` 103` haftmann@37958 ` 104` ```code_type code_numeral ``` haftmann@37958 ` 105` ``` (Haskell "Natural.Natural") ``` haftmann@38968 ` 106` ``` (Scala "Natural") ``` haftmann@37958 ` 107` haftmann@37958 ` 108` ```setup {* ``` huffman@47108 ` 109` ``` fold (Numeral.add_code @{const_name Code_Numeral.Num} ``` haftmann@37958 ` 110` ``` false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"] ``` haftmann@37958 ` 111` ```*} ``` haftmann@37958 ` 112` haftmann@38857 ` 113` ```code_instance code_numeral :: equal ``` haftmann@37958 ` 114` ``` (Haskell -) ``` haftmann@37958 ` 115` huffman@47108 ` 116` ```code_const "0::code_numeral" ``` huffman@47108 ` 117` ``` (Haskell "0") ``` huffman@47108 ` 118` ``` (Scala "Natural(0)") ``` huffman@47108 ` 119` huffman@47108 ` 120` ```code_const "plus \ code_numeral \ code_numeral \ code_numeral" ``` haftmann@37958 ` 121` ``` (Haskell infixl 6 "+") ``` haftmann@37958 ` 122` ``` (Scala infixl 7 "+") ``` haftmann@37958 ` 123` huffman@47108 ` 124` ```code_const "minus \ code_numeral \ code_numeral \ code_numeral" ``` haftmann@37958 ` 125` ``` (Haskell infixl 6 "-") ``` haftmann@37958 ` 126` ``` (Scala infixl 7 "-") ``` haftmann@37958 ` 127` huffman@47108 ` 128` ```code_const "times \ code_numeral \ code_numeral \ code_numeral" ``` haftmann@37958 ` 129` ``` (Haskell infixl 7 "*") ``` haftmann@37958 ` 130` ``` (Scala infixl 8 "*") ``` haftmann@37958 ` 131` huffman@46547 ` 132` ```code_const Code_Numeral.div_mod ``` haftmann@37958 ` 133` ``` (Haskell "divMod") ``` haftmann@37958 ` 134` ``` (Scala infixl 8 "/%") ``` haftmann@37958 ` 135` haftmann@38857 ` 136` ```code_const "HOL.equal \ code_numeral \ code_numeral \ bool" ``` haftmann@39272 ` 137` ``` (Haskell infix 4 "==") ``` haftmann@37958 ` 138` ``` (Scala infixl 5 "==") ``` haftmann@37958 ` 139` huffman@47108 ` 140` ```code_const "less_eq \ code_numeral \ code_numeral \ bool" ``` haftmann@37958 ` 141` ``` (Haskell infix 4 "<=") ``` haftmann@37958 ` 142` ``` (Scala infixl 4 "<=") ``` haftmann@37958 ` 143` huffman@47108 ` 144` ```code_const "less \ code_numeral \ code_numeral \ bool" ``` haftmann@37958 ` 145` ``` (Haskell infix 4 "<") ``` haftmann@37958 ` 146` ``` (Scala infixl 4 "<") ``` haftmann@37958 ` 147` haftmann@37968 ` 148` ```end ```