# HG changeset patch # User haftmann # Date 1280135470 -7200 # Node ID 278367fa09f3737c7ded35600e5718ccd72939d8 # Parent 61887e5b3d1d3630c77ae760b6f5767be21f8c13# Parent f36980b37af56e4ec421bf695aa76433807cb024 merged diff -r 61887e5b3d1d -r 278367fa09f3 src/HOL/Imperative_HOL/Array.thy --- a/src/HOL/Imperative_HOL/Array.thy Sun Jul 25 15:43:53 2010 +0200 +++ b/src/HOL/Imperative_HOL/Array.thy Mon Jul 26 11:11:10 2010 +0200 @@ -484,13 +484,11 @@ code_type array (Scala "!collection.mutable.ArraySeq[_]") code_const Array (Scala "!error(\"bare Array\")") -code_const Array.new' (Scala "('_: Unit)/ => / collection.mutable.ArraySeq.fill((_))((_))") -code_const Array.make' (Scala "('_: Unit)/ =>/ collection.mutable.ArraySeq.tabulate((_))((_))") -code_const Array.len' (Scala "('_: Unit)/ =>/ _.length") -code_const Array.nth' (Scala "('_: Unit)/ =>/ _((_))") -code_const Array.upd' (Scala "('_: Unit)/ =>/ _.update((_),/ (_))") -code_const Array.freeze (Scala "('_: Unit)/ =>/ _.toList") - -code_reserved Scala Array +code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))") +code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))") +code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))") +code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))") +code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))") +code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))") end diff -r 61887e5b3d1d -r 278367fa09f3 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Sun Jul 25 15:43:53 2010 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jul 26 11:11:10 2010 +0200 @@ -5,7 +5,7 @@ header {* A monad with a polymorphic heap and primitive reasoning infrastructure *} theory Heap_Monad -imports Heap Monad_Syntax +imports Heap Monad_Syntax Code_Natural begin subsection {* The monad *} @@ -430,31 +430,33 @@ import qualified Data.STRef; import qualified Data.Array.ST; +import Natural; + type RealWorld = Control.Monad.ST.RealWorld; type ST s a = Control.Monad.ST.ST s a; type STRef s a = Data.STRef.STRef s a; -type STArray s a = Data.Array.ST.STArray s Integer a; +type STArray s a = Data.Array.ST.STArray s Natural a; newSTRef = Data.STRef.newSTRef; readSTRef = Data.STRef.readSTRef; writeSTRef = Data.STRef.writeSTRef; -newArray :: Integer -> a -> ST s (STArray s a); +newArray :: Natural -> a -> ST s (STArray s a); newArray k = Data.Array.ST.newArray (0, k); newListArray :: [a] -> ST s (STArray s a); -newListArray xs = Data.Array.ST.newListArray (0, toInteger (length xs)) xs; +newListArray xs = Data.Array.ST.newListArray (0, (fromInteger . toInteger . length) xs) xs; -newFunArray :: Integer -> (Integer -> a) -> ST s (STArray s a); +newFunArray :: Natural -> (Natural -> a) -> ST s (STArray s a); newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]); -lengthArray :: STArray s a -> ST s Integer; +lengthArray :: STArray s a -> ST s Natural; lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a); -readArray :: STArray s a -> Integer -> ST s a; +readArray :: STArray s a -> Natural -> ST s a; readArray = Data.Array.ST.readArray; -writeArray :: STArray s a -> Integer -> a -> ST s (); +writeArray :: STArray s a -> Natural -> a -> ST s (); writeArray = Data.Array.ST.writeArray;*} code_reserved Haskell Heap @@ -470,7 +472,10 @@ subsubsection {* Scala *} code_include Scala "Heap" -{*def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) () +{*import collection.mutable.ArraySeq +import Natural._ + +def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) () class Ref[A](x: A) { var value = x @@ -478,13 +483,20 @@ object Ref { def apply[A](x: A): Ref[A] = new Ref[A](x) + def lookup[A](r: Ref[A]): A = r.value + def update[A](r: Ref[A], x: A): Unit = { r.value = x } } -def lookup[A](r: Ref[A]): A = r.value +object Array { + def alloc[A](n: Natural)(x: A): ArraySeq[A] = ArraySeq.fill(n.as_Int)(x) + def make[A](n: Natural)(f: Natural => A): ArraySeq[A] = ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k))) + def len[A](a: ArraySeq[A]): Natural = Natural(a.length) + def nth[A](a: ArraySeq[A], n: Natural): A = a(n.as_Int) + def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit = a.update(n.as_Int, x) + def freeze[A](a: ArraySeq[A]): List[A] = a.toList +}*} -def update[A](r: Ref[A], x: A): Unit = { r.value = x }*} - -code_reserved Scala Heap +code_reserved Scala bind Ref Array code_type Heap (Scala "Unit/ =>/ _") code_const bind (Scala "bind") diff -r 61887e5b3d1d -r 278367fa09f3 src/HOL/Imperative_HOL/Imperative_HOL_ex.thy --- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Sun Jul 25 15:43:53 2010 +0200 +++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Mon Jul 26 11:11:10 2010 +0200 @@ -14,6 +14,6 @@ Array.upd, Array.map_entry, Array.swap, Array.freeze, ref, Ref.lookup, Ref.update, Ref.change)" -export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? (*Scala?*) +export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? end diff -r 61887e5b3d1d -r 278367fa09f3 src/HOL/Imperative_HOL/Ref.thy --- a/src/HOL/Imperative_HOL/Ref.thy Sun Jul 25 15:43:53 2010 +0200 +++ b/src/HOL/Imperative_HOL/Ref.thy Mon Jul 26 11:11:10 2010 +0200 @@ -299,8 +299,7 @@ code_type ref (Scala "!Ref[_]") code_const Ref (Scala "!error(\"bare Ref\")") code_const ref (Scala "('_: Unit)/ =>/ Ref((_))") -code_const Ref.lookup (Scala "('_: Unit)/ =>/ lookup((_))") -code_const Ref.update (Scala "('_: Unit)/ =>/ update((_), (_))") +code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))") +code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))") end - diff -r 61887e5b3d1d -r 278367fa09f3 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Sun Jul 25 15:43:53 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Jul 26 11:11:10 2010 +0200 @@ -655,6 +655,6 @@ ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *} -export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? (*Scala?*) +export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? end diff -r 61887e5b3d1d -r 278367fa09f3 src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Sun Jul 25 15:43:53 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Mon Jul 26 11:11:10 2010 +0200 @@ -5,7 +5,7 @@ header {* An imperative in-place reversal on arrays *} theory Imperative_Reverse -imports Imperative_HOL Subarray +imports Subarray Imperative_HOL begin fun swap :: "'a\heap array \ nat \ nat \ unit Heap" where @@ -110,6 +110,6 @@ subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims) (drule sym[of "List.length (Array.get h a)"], simp) -export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? (*Scala?*) +export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? end diff -r 61887e5b3d1d -r 278367fa09f3 src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Sun Jul 25 15:43:53 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Jul 26 11:11:10 2010 +0200 @@ -1014,6 +1014,6 @@ ML {* @{code test_2} () *} ML {* @{code test_3} () *} -export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? (*Scala?*) +export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? end diff -r 61887e5b3d1d -r 278367fa09f3 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun Jul 25 15:43:53 2010 +0200 +++ b/src/HOL/IsaMakefile Mon Jul 26 11:11:10 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 61887e5b3d1d -r 278367fa09f3 src/HOL/Library/Code_Integer.thy --- a/src/HOL/Library/Code_Integer.thy Sun Jul 25 15:43:53 2010 +0200 +++ b/src/HOL/Library/Code_Integer.thy Mon Jul 26 11:11:10 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 61887e5b3d1d -r 278367fa09f3 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:11:10 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 diff -r 61887e5b3d1d -r 278367fa09f3 src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Sun Jul 25 15:43:53 2010 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Mon Jul 26 11:11:10 2010 +0200 @@ -307,7 +307,7 @@ 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 + else error("Int value out of range: " + this.value.toString) def +(that: Nat): Nat = new Nat(this.value + that.value) def -(that: Nat): Nat = Nat(this.value - that.value)