
haftmann@23854: (*  Title:      HOL/Library/Efficient_Nat.thy
haftmann@25931:     Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
haftmann@23854: *)
haftmann@23854: 
haftmann@25931: header {* Implementation of natural numbers by target-language integers *}
haftmann@23854: 
haftmann@23854: theory Efficient_Nat
huffman@47108: imports Code_Nat Code_Integer Main
haftmann@23854: begin
haftmann@23854: 
haftmann@23854: text {*
huffman@47108:   The efficiency of the generated code for natural numbers can be improved
haftmann@25931:   drastically by implementing natural numbers by target-language
haftmann@25931:   integers.  To do this, just include this theory.
haftmann@23854: *}
haftmann@23854: 
huffman@47108: subsection {* Target language fundamentals *}
haftmann@25931: 
haftmann@25931: text {*
haftmann@25967:   For ML, we map @{typ nat} to target language integers, where we
haftmann@34899:   ensure that values are always non-negative.
haftmann@25931: *}
haftmann@25931: 
haftmann@25931: code_type nat
haftmann@27496:   (SML "IntInf.int")
haftmann@25931:   (OCaml "Big'_int.big'_int")
haftmann@37958:   (Eval "int")
haftmann@25931: 
haftmann@25931: text {*
bulwahn@45185:   For Haskell and Scala we define our own @{typ nat} type.  The reason
haftmann@34899:   is that we have to distinguish type class instances for @{typ nat}
haftmann@34899:   and @{typ int}.
haftmann@25967: *}
haftmann@25967: 
haftmann@38774: code_include Haskell "Nat"
haftmann@38774: {*newtype Nat = Nat Integer deriving (Eq, Show, Read);
haftmann@25967: 
haftmann@25967: instance Num Nat where {
haftmann@25967:   fromInteger k = Nat (if k >= 0 then k else 0);
haftmann@25967:   Nat n + Nat m = Nat (n + m);
haftmann@25967:   Nat n - Nat m = fromInteger (n - m);
haftmann@25967:   Nat n * Nat m = Nat (n * m);
haftmann@25967:   abs n = n;
haftmann@25967:   signum _ = 1;
haftmann@25967:   negate n = error "negate Nat";
haftmann@25967: };
haftmann@25967: 
haftmann@25967: instance Ord Nat where {
haftmann@25967:   Nat n <= Nat m = n <= m;
haftmann@25967:   Nat n < Nat m = n < m;
haftmann@25967: };
haftmann@25967: 
haftmann@25967: instance Real Nat where {
haftmann@25967:   toRational (Nat n) = toRational n;
haftmann@25967: };
haftmann@25967: 
haftmann@25967: instance Enum Nat where {
haftmann@25967:   toEnum k = fromInteger (toEnum k);
haftmann@25967:   fromEnum (Nat n) = fromEnum n;
haftmann@25967: };
haftmann@25967: 
haftmann@25967: instance Integral Nat where {
haftmann@25967:   toInteger (Nat n) = n;
haftmann@25967:   divMod n m = quotRem n m;
haftmann@37958:   quotRem (Nat n) (Nat m)
haftmann@37958:     | (m == 0) = (0, Nat n)
haftmann@37958:     | otherwise = (Nat k, Nat l) where (k, l) = quotRem n m;
haftmann@25967: };
haftmann@25967: *}
haftmann@25967: 
haftmann@25967: code_reserved Haskell Nat
haftmann@25967: 
haftmann@38774: code_include Scala "Nat"
haftmann@38968: {*object Nat {
haftmann@34899: 
haftmann@34899:   def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
haftmann@34899:   def apply(numeral: Int): Nat = Nat(BigInt(numeral))
haftmann@34899:   def apply(numeral: String): Nat = Nat(BigInt(numeral))
haftmann@34899: 
haftmann@34899: }
haftmann@34899: 
haftmann@34899: class Nat private(private val value: BigInt) {
haftmann@34899: 
haftmann@34899:   override def hashCode(): Int = this.value.hashCode()
haftmann@34899: 
haftmann@34899:   override def equals(that: Any): Boolean = that match {
haftmann@34899:     case that: Nat => this equals that
haftmann@34899:     case _ => false
haftmann@34899:   }
haftmann@34899: 
haftmann@34899:   override def toString(): String = this.value.toString
haftmann@34899: 
haftmann@34899:   def equals(that: Nat): Boolean = this.value == that.value
haftmann@34899: 
haftmann@34899:   def as_BigInt: BigInt = this.value
haftmann@39781:   def as_Int: Int = if (this.value >= scala.Int.MinValue && this.value <= scala.Int.MaxValue)
haftmann@34944:       this.value.intValue
haftmann@37969:     else error("Int value out of range: " + this.value.toString)
haftmann@34899: 
haftmann@34899:   def +(that: Nat): Nat = new Nat(this.value + that.value)
haftmann@37223:   def -(that: Nat): Nat = Nat(this.value - that.value)
haftmann@34899:   def *(that: Nat): Nat = new Nat(this.value * that.value)
haftmann@34899: 
haftmann@34899:   def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
haftmann@34899:     else {
haftmann@34899:       val (k, l) = this.value /% that.value
haftmann@34899:       (new Nat(k), new Nat(l))
haftmann@34899:     }
haftmann@34899: 
haftmann@34899:   def <=(that: Nat): Boolean = this.value <= that.value
haftmann@34899: 
haftmann@34899:   def <(that: Nat): Boolean = this.value < that.value
haftmann@34899: 
haftmann@34899: }
haftmann@34899: *}
haftmann@34899: 
haftmann@34899: code_reserved Scala Nat
haftmann@34899: 
haftmann@25967: code_type nat
haftmann@29793:   (Haskell "Nat.Nat")
haftmann@38968:   (Scala "Nat")
haftmann@25967: 
haftmann@38857: code_instance nat :: equal
haftmann@25967:   (Haskell -)
haftmann@25967: 
haftmann@25931: setup {*
huffman@47108:   fold (Numeral.add_code @{const_name nat_of_num}
haftmann@37958:     false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell", "Scala"]
haftmann@25931: *}
haftmann@25931: 
huffman@47108: code_const "0::nat"
huffman@47108:   (SML "0")
huffman@47108:   (OCaml "Big'_int.zero'_big'_int")
huffman@47108:   (Haskell "0")
huffman@47108:   (Scala "Nat(0)")
huffman@47108: 
huffman@47108: 
huffman@47108: subsection {* Conversions *}
huffman@47108: 
haftmann@25931: text {*
haftmann@25931:   Since natural numbers are implemented
huffman@47108:   using integers in ML, the coercion function @{term "int"} of type
haftmann@25931:   @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
haftmann@37388:   For the @{const nat} function for converting an integer to a natural
huffman@47108:   number, we give a specific implementation using an ML expression that
haftmann@25931:   returns its input value, provided that it is non-negative, and otherwise
haftmann@25931:   returns @{text "0"}.
haftmann@25931: *}
haftmann@25931: 
haftmann@32073: definition int :: "nat \<Rightarrow> int" where
huffman@47108:   [code_abbrev]: "int = of_nat"
haftmann@32073: 
haftmann@25931: code_const int
haftmann@25931:   (SML "_")
haftmann@25931:   (OCaml "_")
haftmann@25931: 
haftmann@25967: code_const nat
haftmann@43653:   (SML "IntInf.max/ (0,/ _)")
haftmann@25967:   (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
huffman@47108:   (Eval "Integer.max/ 0")
haftmann@25967: 
haftmann@35689: text {* For Haskell and Scala, things are slightly different again. *}
haftmann@25967: 
haftmann@25967: code_const int and nat
haftmann@48431:   (Haskell "Prelude.toInteger" and "Prelude.fromInteger")
haftmann@38968:   (Scala "!_.as'_BigInt" and "Nat")
haftmann@25931: 
huffman@47108: text {* Alternativ implementation for @{const of_nat} *}
huffman@47108: 
huffman@47108: lemma [code]:
huffman@47108:   "of_nat n = (if n = 0 then 0 else
huffman@47108:      let
huffman@47108:        (q, m) = divmod_nat n 2;
huffman@47108:        q' = 2 * of_nat q
huffman@47108:      in if m = 0 then q' else q' + 1)"
huffman@47108: proof -
huffman@47108:   from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
huffman@47108:   show ?thesis
huffman@47108:     apply (simp add: Let_def divmod_nat_div_mod mod_2_not_eq_zero_eq_one_nat
huffman@47108:       of_nat_mult
huffman@47108:       of_nat_add [symmetric])
huffman@47108:     apply (auto simp add: of_nat_mult)
huffman@47108:     apply (simp add: * of_nat_mult add_commute mult_commute)
huffman@47108:     done
huffman@47108: qed
huffman@47108: 
huffman@47108: text {* Conversion from and to code numerals *}
haftmann@25931: 
haftmann@31205: code_const Code_Numeral.of_nat
haftmann@25967:   (SML "IntInf.toInt")
haftmann@31377:   (OCaml "_")
haftmann@48431:   (Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)")
haftmann@38968:   (Scala "!Natural(_.as'_BigInt)")
haftmann@37958:   (Eval "_")
haftmann@25967: 
haftmann@31205: code_const Code_Numeral.nat_of
haftmann@25931:   (SML "IntInf.fromInt")
haftmann@31377:   (OCaml "_")
haftmann@48431:   (Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)")
haftmann@38968:   (Scala "!Nat(_.as'_BigInt)")
haftmann@37958:   (Eval "_")
haftmann@25931: 
huffman@47108: 
huffman@47108: subsection {* Target language arithmetic *}
haftmann@25931: 
huffman@47108: code_const "plus \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
huffman@47108:   (SML "IntInf.+/ ((_),/ (_))")
haftmann@25931:   (OCaml "Big'_int.add'_big'_int")
haftmann@25931:   (Haskell infixl 6 "+")
haftmann@34899:   (Scala infixl 7 "+")
haftmann@37958:   (Eval infixl 8 "+")
haftmann@34899: 
huffman@47108: code_const "minus \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
huffman@47108:   (SML "IntInf.max/ (0, IntInf.-/ ((_),/ (_)))")
huffman@47108:   (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)")
haftmann@34899:   (Haskell infixl 6 "-")
haftmann@34899:   (Scala infixl 7 "-")
huffman@47108:   (Eval "Integer.max/ 0/ (_ -/ _)")
haftmann@25931: 
huffman@47108: code_const Code_Nat.dup
huffman@47108:   (SML "IntInf.*/ (2,/ (_))")
huffman@47108:   (OCaml "Big'_int.mult'_big'_int/ 2")
huffman@47108:   (Haskell "!(2 * _)")
huffman@47108:   (Scala "!(2 * _)")
huffman@47108:   (Eval "!(2 * _)")
huffman@47108: 
huffman@47108: code_const Code_Nat.sub
huffman@47108:   (SML "!(raise/ Fail/ \"sub\")")
huffman@47108:   (OCaml "failwith/ \"sub\"")
huffman@47108:   (Haskell "error/ \"sub\"")
haftmann@48073:   (Scala "!sys.error(\"sub\")")
huffman@47108: 
huffman@47108: code_const "times \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
huffman@47108:   (SML "IntInf.*/ ((_),/ (_))")
haftmann@25931:   (OCaml "Big'_int.mult'_big'_int")
haftmann@25931:   (Haskell infixl 7 "*")
haftmann@34899:   (Scala infixl 8 "*")
haftmann@37958:   (Eval infixl 9 "*")
haftmann@25931: 
haftmann@37958: code_const divmod_nat
haftmann@26009:   (SML "IntInf.divMod/ ((_),/ (_))")
haftmann@26009:   (OCaml "Big'_int.quomod'_big'_int")
haftmann@26009:   (Haskell "divMod")
haftmann@34899:   (Scala infixl 8 "/%")
haftmann@37958:   (Eval "Integer.div'_mod")
haftmann@25931: 
haftmann@38857: code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
haftmann@25931:   (SML "!((_ : IntInf.int) = _)")
haftmann@25931:   (OCaml "Big'_int.eq'_big'_int")
haftmann@39272:   (Haskell infix 4 "==")
haftmann@34899:   (Scala infixl 5 "==")
haftmann@37958:   (Eval infixl 6 "=")
haftmann@25931: 
huffman@47108: code_const "less_eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
huffman@47108:   (SML "IntInf.<=/ ((_),/ (_))")
haftmann@25931:   (OCaml "Big'_int.le'_big'_int")
haftmann@25931:   (Haskell infix 4 "<=")
haftmann@34899:   (Scala infixl 4 "<=")
haftmann@37958:   (Eval infixl 6 "<=")
haftmann@25931: 
huffman@47108: code_const "less \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
huffman@47108:   (SML "IntInf.</ ((_),/ (_))")
haftmann@25931:   (OCaml "Big'_int.lt'_big'_int")
haftmann@25931:   (Haskell infix 4 "<")
haftmann@34899:   (Scala infixl 4 "<")
haftmann@37958:   (Eval infixl 6 "<")
haftmann@25931: 
huffman@47108: code_const Num.num_of_nat
huffman@47108:   (SML "!(raise/ Fail/ \"num'_of'_nat\")")
huffman@47108:   (OCaml "failwith/ \"num'_of'_nat\"")
huffman@47108:   (Haskell "error/ \"num'_of'_nat\"")
haftmann@48073:   (Scala "!sys.error(\"num'_of'_nat\")")
haftmann@25931: 
huffman@47108: 
huffman@47108: subsection {* Evaluation *}
haftmann@28228: 
haftmann@28562: lemma [code, code del]:
haftmann@32657:   "(Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term) = Code_Evaluation.term_of" ..
haftmann@28228: 
haftmann@32657: code_const "Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term"
haftmann@28228:   (SML "HOLogic.mk'_number/ HOLogic.natT")
haftmann@28228: 
huffman@47108: text {*
haftmann@48568:   Evaluation with @{text "Quickcheck_Narrowing"} does not work yet,
haftmann@48568:   since a couple of questions how to perform evaluations in Haskell are not that
haftmann@48568:   clear yet.  Therefore, we simply deactivate the narrowing-based quickcheck
haftmann@48568:   from here on.
bulwahn@45793: *}
bulwahn@45793: 
bulwahn@45793: declare [[quickcheck_narrowing_active = false]] 
haftmann@28228: 
haftmann@23854: 
haftmann@23854: code_modulename SML
haftmann@33364:   Efficient_Nat Arith
haftmann@23854: 
haftmann@23854: code_modulename OCaml
haftmann@33364:   Efficient_Nat Arith
haftmann@23854: 
haftmann@23854: code_modulename Haskell
haftmann@33364:   Efficient_Nat Arith
haftmann@23854: 
huffman@47108: hide_const (open) int
haftmann@23854: 
haftmann@23854: end




