1.1 --- a/src/HOL/IsaMakefile Mon Jul 26 11:09:45 2010 +0200
1.2 +++ b/src/HOL/IsaMakefile Mon Jul 26 11:10:35 2010 +0200
1.3 @@ -398,20 +398,19 @@
1.4 $(OUT)/HOL-Library: $(OUT)/HOL Library/HOL_Library_ROOT.ML \
1.5 $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \
1.6 Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \
1.7 - Library/AssocList.thy \
1.8 - Library/BigO.thy Library/Binomial.thy Library/Bit.thy \
1.9 - Library/Boolean_Algebra.thy Library/Cardinality.thy \
1.10 + Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \
1.11 + Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \
1.12 Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
1.13 - Library/Code_Integer.thy Library/ContNotDenum.thy \
1.14 - Library/Continuity.thy Library/Convex.thy Library/Countable.thy \
1.15 - Library/Diagonalize.thy Library/Dlist.thy Library/Efficient_Nat.thy \
1.16 - Library/Enum.thy Library/Eval_Witness.thy Library/Executable_Set.thy \
1.17 - Library/Float.thy Library/Formal_Power_Series.thy \
1.18 - Library/Fraction_Field.thy Library/FrechetDeriv.thy Library/Fset.thy \
1.19 - Library/FuncSet.thy Library/Fundamental_Theorem_Algebra.thy \
1.20 - Library/Glbs.thy Library/Indicator_Function.thy \
1.21 - Library/Infinite_Set.thy Library/Inner_Product.thy \
1.22 - Library/Kleene_Algebra.thy \
1.23 + Library/Code_Integer.thy Library/Code_Natural.thy \
1.24 + Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy \
1.25 + Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \
1.26 + Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy \
1.27 + Library/Executable_Set.thy Library/Float.thy \
1.28 + Library/Formal_Power_Series.thy Library/Fraction_Field.thy \
1.29 + Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy \
1.30 + Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \
1.31 + Library/Indicator_Function.thy Library/Infinite_Set.thy \
1.32 + Library/Inner_Product.thy Library/Kleene_Algebra.thy \
1.33 Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \
1.34 Library/Lattice_Syntax.thy Library/Library.thy \
1.35 Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \
2.1 --- a/src/HOL/Library/Code_Integer.thy Mon Jul 26 11:09:45 2010 +0200
2.2 +++ b/src/HOL/Library/Code_Integer.thy Mon Jul 26 11:10:35 2010 +0200
2.3 @@ -5,7 +5,7 @@
2.4 header {* Pretty integer literals for code generation *}
2.5
2.6 theory Code_Integer
2.7 -imports Main
2.8 +imports Main Code_Natural
2.9 begin
2.10
2.11 text {*
2.12 @@ -14,142 +14,6 @@
2.13 operations for abstract integer operations.
2.14 *}
2.15
2.16 -text {*
2.17 - Preliminary: alternative representation of @{typ code_numeral}
2.18 - for @{text Haskell} and @{text Scala}.
2.19 -*}
2.20 -
2.21 -code_include Haskell "Natural" {*
2.22 -newtype Natural = Natural Integer deriving (Eq, Show, Read);
2.23 -
2.24 -instance Num Natural where {
2.25 - fromInteger k = Natural (if k >= 0 then k else 0);
2.26 - Natural n + Natural m = Natural (n + m);
2.27 - Natural n - Natural m = fromInteger (n - m);
2.28 - Natural n * Natural m = Natural (n * m);
2.29 - abs n = n;
2.30 - signum _ = 1;
2.31 - negate n = error "negate Natural";
2.32 -};
2.33 -
2.34 -instance Ord Natural where {
2.35 - Natural n <= Natural m = n <= m;
2.36 - Natural n < Natural m = n < m;
2.37 -};
2.38 -
2.39 -instance Real Natural where {
2.40 - toRational (Natural n) = toRational n;
2.41 -};
2.42 -
2.43 -instance Enum Natural where {
2.44 - toEnum k = fromInteger (toEnum k);
2.45 - fromEnum (Natural n) = fromEnum n;
2.46 -};
2.47 -
2.48 -instance Integral Natural where {
2.49 - toInteger (Natural n) = n;
2.50 - divMod n m = quotRem n m;
2.51 - quotRem (Natural n) (Natural m)
2.52 - | (m == 0) = (0, Natural n)
2.53 - | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
2.54 -};
2.55 -*}
2.56 -
2.57 -code_reserved Haskell Natural
2.58 -
2.59 -code_include Scala "Natural" {*
2.60 -import scala.Math
2.61 -
2.62 -object Natural {
2.63 -
2.64 - def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
2.65 - def apply(numeral: Int): Natural = Natural(BigInt(numeral))
2.66 - def apply(numeral: String): Natural = Natural(BigInt(numeral))
2.67 -
2.68 -}
2.69 -
2.70 -class Natural private(private val value: BigInt) {
2.71 -
2.72 - override def hashCode(): Int = this.value.hashCode()
2.73 -
2.74 - override def equals(that: Any): Boolean = that match {
2.75 - case that: Natural => this equals that
2.76 - case _ => false
2.77 - }
2.78 -
2.79 - override def toString(): String = this.value.toString
2.80 -
2.81 - def equals(that: Natural): Boolean = this.value == that.value
2.82 -
2.83 - def as_BigInt: BigInt = this.value
2.84 - def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
2.85 - this.value.intValue
2.86 - else this.value.intValue
2.87 -
2.88 - def +(that: Natural): Natural = new Natural(this.value + that.value)
2.89 - def -(that: Natural): Natural = Natural(this.value - that.value)
2.90 - def *(that: Natural): Natural = new Natural(this.value * that.value)
2.91 -
2.92 - def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
2.93 - else {
2.94 - val (k, l) = this.value /% that.value
2.95 - (new Natural(k), new Natural(l))
2.96 - }
2.97 -
2.98 - def <=(that: Natural): Boolean = this.value <= that.value
2.99 -
2.100 - def <(that: Natural): Boolean = this.value < that.value
2.101 -
2.102 -}
2.103 -*}
2.104 -
2.105 -code_reserved Scala Natural
2.106 -
2.107 -code_type code_numeral
2.108 - (Haskell "Natural.Natural")
2.109 - (Scala "Natural")
2.110 -
2.111 -setup {*
2.112 - fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
2.113 - false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
2.114 -*}
2.115 -
2.116 -code_instance code_numeral :: eq
2.117 - (Haskell -)
2.118 -
2.119 -code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
2.120 - (Haskell infixl 6 "+")
2.121 - (Scala infixl 7 "+")
2.122 -
2.123 -code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
2.124 - (Haskell infixl 6 "-")
2.125 - (Scala infixl 7 "-")
2.126 -
2.127 -code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
2.128 - (Haskell infixl 7 "*")
2.129 - (Scala infixl 8 "*")
2.130 -
2.131 -code_const div_mod_code_numeral
2.132 - (Haskell "divMod")
2.133 - (Scala infixl 8 "/%")
2.134 -
2.135 -code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
2.136 - (Haskell infixl 4 "==")
2.137 - (Scala infixl 5 "==")
2.138 -
2.139 -code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
2.140 - (Haskell infix 4 "<=")
2.141 - (Scala infixl 4 "<=")
2.142 -
2.143 -code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
2.144 - (Haskell infix 4 "<")
2.145 - (Scala infixl 4 "<")
2.146 -
2.147 -text {*
2.148 - Setup for @{typ int} proper.
2.149 -*}
2.150 -
2.151 -
2.152 code_type int
2.153 (SML "IntInf.int")
2.154 (OCaml "Big'_int.big'_int")
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Library/Code_Natural.thy Mon Jul 26 11:10:35 2010 +0200
3.3 @@ -0,0 +1,145 @@
3.4 +(* Title: HOL/Library/Code_Natural.thy
3.5 + Author: Florian Haftmann, TU Muenchen
3.6 +*)
3.7 +
3.8 +theory Code_Natural
3.9 +imports Main
3.10 +begin
3.11 +
3.12 +section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *}
3.13 +
3.14 +code_include Haskell "Natural"
3.15 +{*import Data.Array.ST;
3.16 +
3.17 +newtype Natural = Natural Integer deriving (Eq, Show, Read);
3.18 +
3.19 +instance Num Natural where {
3.20 + fromInteger k = Natural (if k >= 0 then k else 0);
3.21 + Natural n + Natural m = Natural (n + m);
3.22 + Natural n - Natural m = fromInteger (n - m);
3.23 + Natural n * Natural m = Natural (n * m);
3.24 + abs n = n;
3.25 + signum _ = 1;
3.26 + negate n = error "negate Natural";
3.27 +};
3.28 +
3.29 +instance Ord Natural where {
3.30 + Natural n <= Natural m = n <= m;
3.31 + Natural n < Natural m = n < m;
3.32 +};
3.33 +
3.34 +instance Ix Natural where {
3.35 + range (Natural n, Natural m) = map Natural (range (n, m));
3.36 + index (Natural n, Natural m) (Natural q) = index (n, m) q;
3.37 + inRange (Natural n, Natural m) (Natural q) = inRange (n, m) q;
3.38 + rangeSize (Natural n, Natural m) = rangeSize (n, m);
3.39 +};
3.40 +
3.41 +instance Real Natural where {
3.42 + toRational (Natural n) = toRational n;
3.43 +};
3.44 +
3.45 +instance Enum Natural where {
3.46 + toEnum k = fromInteger (toEnum k);
3.47 + fromEnum (Natural n) = fromEnum n;
3.48 +};
3.49 +
3.50 +instance Integral Natural where {
3.51 + toInteger (Natural n) = n;
3.52 + divMod n m = quotRem n m;
3.53 + quotRem (Natural n) (Natural m)
3.54 + | (m == 0) = (0, Natural n)
3.55 + | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
3.56 +};*}
3.57 +
3.58 +code_reserved Haskell Natural
3.59 +
3.60 +code_include Scala "Natural" {*
3.61 +import scala.Math
3.62 +
3.63 +object Natural {
3.64 +
3.65 + def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
3.66 + def apply(numeral: Int): Natural = Natural(BigInt(numeral))
3.67 + def apply(numeral: String): Natural = Natural(BigInt(numeral))
3.68 +
3.69 +}
3.70 +
3.71 +class Natural private(private val value: BigInt) {
3.72 +
3.73 + override def hashCode(): Int = this.value.hashCode()
3.74 +
3.75 + override def equals(that: Any): Boolean = that match {
3.76 + case that: Natural => this equals that
3.77 + case _ => false
3.78 + }
3.79 +
3.80 + override def toString(): String = this.value.toString
3.81 +
3.82 + def equals(that: Natural): Boolean = this.value == that.value
3.83 +
3.84 + def as_BigInt: BigInt = this.value
3.85 + def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
3.86 + this.value.intValue
3.87 + else error("Int value out of range: " + this.value.toString)
3.88 +
3.89 + def +(that: Natural): Natural = new Natural(this.value + that.value)
3.90 + def -(that: Natural): Natural = Natural(this.value - that.value)
3.91 + def *(that: Natural): Natural = new Natural(this.value * that.value)
3.92 +
3.93 + def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
3.94 + else {
3.95 + val (k, l) = this.value /% that.value
3.96 + (new Natural(k), new Natural(l))
3.97 + }
3.98 +
3.99 + def <=(that: Natural): Boolean = this.value <= that.value
3.100 +
3.101 + def <(that: Natural): Boolean = this.value < that.value
3.102 +
3.103 +}
3.104 +*}
3.105 +
3.106 +code_reserved Scala Natural
3.107 +
3.108 +code_type code_numeral
3.109 + (Haskell "Natural.Natural")
3.110 + (Scala "Natural")
3.111 +
3.112 +setup {*
3.113 + fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
3.114 + false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
3.115 +*}
3.116 +
3.117 +code_instance code_numeral :: eq
3.118 + (Haskell -)
3.119 +
3.120 +code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
3.121 + (Haskell infixl 6 "+")
3.122 + (Scala infixl 7 "+")
3.123 +
3.124 +code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
3.125 + (Haskell infixl 6 "-")
3.126 + (Scala infixl 7 "-")
3.127 +
3.128 +code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
3.129 + (Haskell infixl 7 "*")
3.130 + (Scala infixl 8 "*")
3.131 +
3.132 +code_const div_mod_code_numeral
3.133 + (Haskell "divMod")
3.134 + (Scala infixl 8 "/%")
3.135 +
3.136 +code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
3.137 + (Haskell infixl 4 "==")
3.138 + (Scala infixl 5 "==")
3.139 +
3.140 +code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
3.141 + (Haskell infix 4 "<=")
3.142 + (Scala infixl 4 "<=")
3.143 +
3.144 +code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
3.145 + (Haskell infix 4 "<")
3.146 + (Scala infixl 4 "<")
3.147 +
3.148 +end