# HG changeset patch # User haftmann # Date 1280135435 -7200 # Node ID 52fdcb76c0afb519c763722fbe96223e9d2d4c36 # Parent 3e174df3f965214eae07da13b7d19d9451e8c107 added Code_Natural.thy diff -r 3e174df3f965 -r 52fdcb76c0af src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Jul 26 11:09:45 2010 +0200 +++ b/src/HOL/IsaMakefile Mon Jul 26 11:10:35 2010 +0200 @@ -398,20 +398,19 @@ $(OUT)/HOL-Library: $(OUT)/HOL Library/HOL_Library_ROOT.ML \ $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \ Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \ - Library/AssocList.thy \ - Library/BigO.thy Library/Binomial.thy Library/Bit.thy \ - Library/Boolean_Algebra.thy Library/Cardinality.thy \ + Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \ + Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \ Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \ - Library/Code_Integer.thy Library/ContNotDenum.thy \ - Library/Continuity.thy Library/Convex.thy Library/Countable.thy \ - Library/Diagonalize.thy Library/Dlist.thy Library/Efficient_Nat.thy \ - Library/Enum.thy Library/Eval_Witness.thy Library/Executable_Set.thy \ - Library/Float.thy Library/Formal_Power_Series.thy \ - Library/Fraction_Field.thy Library/FrechetDeriv.thy Library/Fset.thy \ - Library/FuncSet.thy Library/Fundamental_Theorem_Algebra.thy \ - Library/Glbs.thy Library/Indicator_Function.thy \ - Library/Infinite_Set.thy Library/Inner_Product.thy \ - Library/Kleene_Algebra.thy \ + Library/Code_Integer.thy Library/Code_Natural.thy \ + Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy \ + Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \ + Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy \ + Library/Executable_Set.thy Library/Float.thy \ + Library/Formal_Power_Series.thy Library/Fraction_Field.thy \ + Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy \ + Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \ + Library/Indicator_Function.thy Library/Infinite_Set.thy \ + Library/Inner_Product.thy Library/Kleene_Algebra.thy \ Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \ Library/Lattice_Syntax.thy Library/Library.thy \ Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \ diff -r 3e174df3f965 -r 52fdcb76c0af src/HOL/Library/Code_Integer.thy --- a/src/HOL/Library/Code_Integer.thy Mon Jul 26 11:09:45 2010 +0200 +++ b/src/HOL/Library/Code_Integer.thy Mon Jul 26 11:10:35 2010 +0200 @@ -5,7 +5,7 @@ header {* Pretty integer literals for code generation *} theory Code_Integer -imports Main +imports Main Code_Natural begin text {* @@ -14,142 +14,6 @@ operations for abstract integer operations. *} -text {* - Preliminary: alternative representation of @{typ code_numeral} - for @{text Haskell} and @{text Scala}. -*} - -code_include Haskell "Natural" {* -newtype Natural = Natural Integer deriving (Eq, Show, Read); - -instance Num Natural where { - fromInteger k = Natural (if k >= 0 then k else 0); - Natural n + Natural m = Natural (n + m); - Natural n - Natural m = fromInteger (n - m); - Natural n * Natural m = Natural (n * m); - abs n = n; - signum _ = 1; - negate n = error "negate Natural"; -}; - -instance Ord Natural where { - Natural n <= Natural m = n <= m; - Natural n < Natural m = n < m; -}; - -instance Real Natural where { - toRational (Natural n) = toRational n; -}; - -instance Enum Natural where { - toEnum k = fromInteger (toEnum k); - fromEnum (Natural n) = fromEnum n; -}; - -instance Integral Natural where { - toInteger (Natural n) = n; - divMod n m = quotRem n m; - quotRem (Natural n) (Natural m) - | (m == 0) = (0, Natural n) - | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m; -}; -*} - -code_reserved Haskell Natural - -code_include Scala "Natural" {* -import scala.Math - -object Natural { - - def apply(numeral: BigInt): Natural = new Natural(numeral max 0) - def apply(numeral: Int): Natural = Natural(BigInt(numeral)) - def apply(numeral: String): Natural = Natural(BigInt(numeral)) - -} - -class Natural private(private val value: BigInt) { - - override def hashCode(): Int = this.value.hashCode() - - override def equals(that: Any): Boolean = that match { - case that: Natural => this equals that - case _ => false - } - - override def toString(): String = this.value.toString - - def equals(that: Natural): Boolean = this.value == that.value - - def as_BigInt: BigInt = this.value - def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue) - this.value.intValue - else this.value.intValue - - def +(that: Natural): Natural = new Natural(this.value + that.value) - def -(that: Natural): Natural = Natural(this.value - that.value) - def *(that: Natural): Natural = new Natural(this.value * that.value) - - def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this) - else { - val (k, l) = this.value /% that.value - (new Natural(k), new Natural(l)) - } - - def <=(that: Natural): Boolean = this.value <= that.value - - def <(that: Natural): Boolean = this.value < that.value - -} -*} - -code_reserved Scala Natural - -code_type code_numeral - (Haskell "Natural.Natural") - (Scala "Natural") - -setup {* - fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} - false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"] -*} - -code_instance code_numeral :: eq - (Haskell -) - -code_const "op + \ code_numeral \ code_numeral \ code_numeral" - (Haskell infixl 6 "+") - (Scala infixl 7 "+") - -code_const "op - \ code_numeral \ code_numeral \ code_numeral" - (Haskell infixl 6 "-") - (Scala infixl 7 "-") - -code_const "op * \ code_numeral \ code_numeral \ code_numeral" - (Haskell infixl 7 "*") - (Scala infixl 8 "*") - -code_const div_mod_code_numeral - (Haskell "divMod") - (Scala infixl 8 "/%") - -code_const "eq_class.eq \ code_numeral \ code_numeral \ bool" - (Haskell infixl 4 "==") - (Scala infixl 5 "==") - -code_const "op \ \ code_numeral \ code_numeral \ bool" - (Haskell infix 4 "<=") - (Scala infixl 4 "<=") - -code_const "op < \ code_numeral \ code_numeral \ bool" - (Haskell infix 4 "<") - (Scala infixl 4 "<") - -text {* - Setup for @{typ int} proper. -*} - - code_type int (SML "IntInf.int") (OCaml "Big'_int.big'_int") diff -r 3e174df3f965 -r 52fdcb76c0af src/HOL/Library/Code_Natural.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Code_Natural.thy Mon Jul 26 11:10:35 2010 +0200 @@ -0,0 +1,145 @@ +(* Title: HOL/Library/Code_Natural.thy + Author: Florian Haftmann, TU Muenchen +*) + +theory Code_Natural +imports Main +begin + +section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *} + +code_include Haskell "Natural" +{*import Data.Array.ST; + +newtype Natural = Natural Integer deriving (Eq, Show, Read); + +instance Num Natural where { + fromInteger k = Natural (if k >= 0 then k else 0); + Natural n + Natural m = Natural (n + m); + Natural n - Natural m = fromInteger (n - m); + Natural n * Natural m = Natural (n * m); + abs n = n; + signum _ = 1; + negate n = error "negate Natural"; +}; + +instance Ord Natural where { + Natural n <= Natural m = n <= m; + Natural n < Natural m = n < m; +}; + +instance Ix Natural where { + range (Natural n, Natural m) = map Natural (range (n, m)); + index (Natural n, Natural m) (Natural q) = index (n, m) q; + inRange (Natural n, Natural m) (Natural q) = inRange (n, m) q; + rangeSize (Natural n, Natural m) = rangeSize (n, m); +}; + +instance Real Natural where { + toRational (Natural n) = toRational n; +}; + +instance Enum Natural where { + toEnum k = fromInteger (toEnum k); + fromEnum (Natural n) = fromEnum n; +}; + +instance Integral Natural where { + toInteger (Natural n) = n; + divMod n m = quotRem n m; + quotRem (Natural n) (Natural m) + | (m == 0) = (0, Natural n) + | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m; +};*} + +code_reserved Haskell Natural + +code_include Scala "Natural" {* +import scala.Math + +object Natural { + + def apply(numeral: BigInt): Natural = new Natural(numeral max 0) + def apply(numeral: Int): Natural = Natural(BigInt(numeral)) + def apply(numeral: String): Natural = Natural(BigInt(numeral)) + +} + +class Natural private(private val value: BigInt) { + + override def hashCode(): Int = this.value.hashCode() + + override def equals(that: Any): Boolean = that match { + case that: Natural => this equals that + case _ => false + } + + override def toString(): String = this.value.toString + + def equals(that: Natural): Boolean = this.value == that.value + + def as_BigInt: BigInt = this.value + def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue) + this.value.intValue + else error("Int value out of range: " + this.value.toString) + + def +(that: Natural): Natural = new Natural(this.value + that.value) + def -(that: Natural): Natural = Natural(this.value - that.value) + def *(that: Natural): Natural = new Natural(this.value * that.value) + + def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this) + else { + val (k, l) = this.value /% that.value + (new Natural(k), new Natural(l)) + } + + def <=(that: Natural): Boolean = this.value <= that.value + + def <(that: Natural): Boolean = this.value < that.value + +} +*} + +code_reserved Scala Natural + +code_type code_numeral + (Haskell "Natural.Natural") + (Scala "Natural") + +setup {* + fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} + false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"] +*} + +code_instance code_numeral :: eq + (Haskell -) + +code_const "op + \ code_numeral \ code_numeral \ code_numeral" + (Haskell infixl 6 "+") + (Scala infixl 7 "+") + +code_const "op - \ code_numeral \ code_numeral \ code_numeral" + (Haskell infixl 6 "-") + (Scala infixl 7 "-") + +code_const "op * \ code_numeral \ code_numeral \ code_numeral" + (Haskell infixl 7 "*") + (Scala infixl 8 "*") + +code_const div_mod_code_numeral + (Haskell "divMod") + (Scala infixl 8 "/%") + +code_const "eq_class.eq \ code_numeral \ code_numeral \ bool" + (Haskell infixl 4 "==") + (Scala infixl 5 "==") + +code_const "op \ \ code_numeral \ code_numeral \ bool" + (Haskell infix 4 "<=") + (Scala infixl 4 "<=") + +code_const "op < \ code_numeral \ code_numeral \ bool" + (Haskell infix 4 "<") + (Scala infixl 4 "<") + +end