src/HOL/Library/Code_Natural.thy
 author haftmann Fri Aug 27 19:34:23 2010 +0200 (2010-08-27 ago) changeset 38857 97775f3e8722 parent 38810 361119ea62ee child 38968 e55deaa22fff permissions -rw-r--r--
renamed class/constant eq to equal; tuned some instantiations
 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 ``` haftmann@31203 ` 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@38774 ` 59` ```{*import scala.Math ``` haftmann@37958 ` 60` haftmann@38771 ` 61` ```object Nat { ``` haftmann@37958 ` 62` haftmann@38771 ` 63` ``` def apply(numeral: BigInt): Nat = new Nat(numeral max 0) ``` haftmann@38771 ` 64` ``` def apply(numeral: Int): Nat = Nat(BigInt(numeral)) ``` haftmann@38771 ` 65` ``` def apply(numeral: String): Nat = Nat(BigInt(numeral)) ``` haftmann@37958 ` 66` haftmann@37958 ` 67` ```} ``` haftmann@37958 ` 68` haftmann@38771 ` 69` ```class Nat private(private val value: BigInt) { ``` haftmann@37958 ` 70` haftmann@37958 ` 71` ``` override def hashCode(): Int = this.value.hashCode() ``` haftmann@37958 ` 72` haftmann@37958 ` 73` ``` override def equals(that: Any): Boolean = that match { ``` haftmann@38771 ` 74` ``` case that: Nat => this equals that ``` haftmann@37958 ` 75` ``` case _ => false ``` haftmann@37958 ` 76` ``` } ``` haftmann@37958 ` 77` haftmann@37958 ` 78` ``` override def toString(): String = this.value.toString ``` haftmann@37958 ` 79` haftmann@38771 ` 80` ``` def equals(that: Nat): Boolean = this.value == that.value ``` haftmann@37958 ` 81` haftmann@37958 ` 82` ``` def as_BigInt: BigInt = this.value ``` haftmann@37958 ` 83` ``` def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue) ``` haftmann@37958 ` 84` ``` this.value.intValue ``` haftmann@37968 ` 85` ``` else error("Int value out of range: " + this.value.toString) ``` haftmann@37958 ` 86` haftmann@38771 ` 87` ``` def +(that: Nat): Nat = new Nat(this.value + that.value) ``` haftmann@38771 ` 88` ``` def -(that: Nat): Nat = Nat(this.value - that.value) ``` haftmann@38771 ` 89` ``` def *(that: Nat): Nat = new Nat(this.value * that.value) ``` haftmann@37958 ` 90` haftmann@38771 ` 91` ``` def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this) ``` haftmann@37958 ` 92` ``` else { ``` haftmann@37958 ` 93` ``` val (k, l) = this.value /% that.value ``` haftmann@38771 ` 94` ``` (new Nat(k), new Nat(l)) ``` haftmann@37958 ` 95` ``` } ``` haftmann@37958 ` 96` haftmann@38771 ` 97` ``` def <=(that: Nat): Boolean = this.value <= that.value ``` haftmann@37958 ` 98` haftmann@38771 ` 99` ``` def <(that: Nat): Boolean = this.value < that.value ``` haftmann@37958 ` 100` haftmann@37958 ` 101` ```} ``` haftmann@37958 ` 102` ```*} ``` haftmann@37958 ` 103` haftmann@37958 ` 104` ```code_reserved Scala Natural ``` haftmann@37958 ` 105` haftmann@37958 ` 106` ```code_type code_numeral ``` haftmann@37958 ` 107` ``` (Haskell "Natural.Natural") ``` haftmann@38771 ` 108` ``` (Scala "Natural.Nat") ``` haftmann@37958 ` 109` haftmann@37958 ` 110` ```setup {* ``` haftmann@37958 ` 111` ``` fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} ``` haftmann@37958 ` 112` ``` false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"] ``` haftmann@37958 ` 113` ```*} ``` haftmann@37958 ` 114` haftmann@38857 ` 115` ```code_instance code_numeral :: equal ``` haftmann@37958 ` 116` ``` (Haskell -) ``` haftmann@37958 ` 117` haftmann@37958 ` 118` ```code_const "op + \ code_numeral \ code_numeral \ code_numeral" ``` haftmann@37958 ` 119` ``` (Haskell infixl 6 "+") ``` haftmann@37958 ` 120` ``` (Scala infixl 7 "+") ``` haftmann@37958 ` 121` haftmann@37958 ` 122` ```code_const "op - \ code_numeral \ code_numeral \ code_numeral" ``` haftmann@37958 ` 123` ``` (Haskell infixl 6 "-") ``` haftmann@37958 ` 124` ``` (Scala infixl 7 "-") ``` haftmann@37958 ` 125` haftmann@37958 ` 126` ```code_const "op * \ code_numeral \ code_numeral \ code_numeral" ``` haftmann@37958 ` 127` ``` (Haskell infixl 7 "*") ``` haftmann@37958 ` 128` ``` (Scala infixl 8 "*") ``` haftmann@37958 ` 129` haftmann@37958 ` 130` ```code_const div_mod_code_numeral ``` haftmann@37958 ` 131` ``` (Haskell "divMod") ``` haftmann@37958 ` 132` ``` (Scala infixl 8 "/%") ``` haftmann@37958 ` 133` haftmann@38857 ` 134` ```code_const "HOL.equal \ code_numeral \ code_numeral \ bool" ``` haftmann@37958 ` 135` ``` (Haskell infixl 4 "==") ``` haftmann@37958 ` 136` ``` (Scala infixl 5 "==") ``` haftmann@37958 ` 137` haftmann@37958 ` 138` ```code_const "op \ \ code_numeral \ code_numeral \ bool" ``` haftmann@37958 ` 139` ``` (Haskell infix 4 "<=") ``` haftmann@37958 ` 140` ``` (Scala infixl 4 "<=") ``` haftmann@37958 ` 141` haftmann@37958 ` 142` ```code_const "op < \ code_numeral \ code_numeral \ bool" ``` haftmann@37958 ` 143` ``` (Haskell infix 4 "<") ``` haftmann@37958 ` 144` ``` (Scala infixl 4 "<") ``` haftmann@37958 ` 145` haftmann@37968 ` 146` ```end ```