src/HOL/Library/Efficient_Nat.thy
author wenzelm
Sat, 12 Jan 2013 14:53:56 +0100
changeset 50843 1465521b92a1
parent 50023 28f3263d4d1b
permissions -rw-r--r--
removed unused/non-portable bash_output_fifo;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Library/Efficient_Nat.thy
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
     2
    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     3
*)
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     4
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
     5
header {* Implementation of natural numbers by target-language integers *}
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     6
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     7
theory Efficient_Nat
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents: 48568
diff changeset
     8
imports Code_Binary_Nat Code_Integer Main
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
     9
begin
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    10
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    11
text {*
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    12
  The efficiency of the generated code for natural numbers can be improved
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
    13
  drastically by implementing natural numbers by target-language
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
    14
  integers.  To do this, just include this theory.
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    15
*}
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
    16
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
    17
subsection {* Target language fundamentals *}
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
    18
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
    19
text {*
25967
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    20
  For ML, we map @{typ nat} to target language integers, where we
34899
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    21
  ensure that values are always non-negative.
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
    22
*}
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
    23
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
    24
code_type nat
27496
f56684dd75a5 fix: using IntInf.int for SML
haftmann
parents: 27368
diff changeset
    25
  (SML "IntInf.int")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
    26
  (OCaml "Big'_int.big'_int")
37958
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
    27
  (Eval "int")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
    28
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
    29
text {*
45185
3a0c63c0ed48 removing old code generator setup for efficient natural numbers; cleaned typo
bulwahn
parents: 43653
diff changeset
    30
  For Haskell and Scala we define our own @{typ nat} type.  The reason
34899
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    31
  is that we have to distinguish type class instances for @{typ nat}
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    32
  and @{typ int}.
25967
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    33
*}
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    34
38774
567b94f8bb6e tuned includes
haftmann
parents: 38771
diff changeset
    35
code_include Haskell "Nat"
567b94f8bb6e tuned includes
haftmann
parents: 38771
diff changeset
    36
{*newtype Nat = Nat Integer deriving (Eq, Show, Read);
25967
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    37
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    38
instance Num Nat where {
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    39
  fromInteger k = Nat (if k >= 0 then k else 0);
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    40
  Nat n + Nat m = Nat (n + m);
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    41
  Nat n - Nat m = fromInteger (n - m);
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    42
  Nat n * Nat m = Nat (n * m);
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    43
  abs n = n;
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    44
  signum _ = 1;
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    45
  negate n = error "negate Nat";
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    46
};
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    47
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    48
instance Ord Nat where {
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    49
  Nat n <= Nat m = n <= m;
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    50
  Nat n < Nat m = n < m;
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    51
};
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    52
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    53
instance Real Nat where {
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    54
  toRational (Nat n) = toRational n;
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    55
};
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    56
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    57
instance Enum Nat where {
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    58
  toEnum k = fromInteger (toEnum k);
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    59
  fromEnum (Nat n) = fromEnum n;
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    60
};
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    61
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    62
instance Integral Nat where {
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    63
  toInteger (Nat n) = n;
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    64
  divMod n m = quotRem n m;
37958
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
    65
  quotRem (Nat n) (Nat m)
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
    66
    | (m == 0) = (0, Nat n)
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
    67
    | otherwise = (Nat k, Nat l) where (k, l) = quotRem n m;
25967
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    68
};
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    69
*}
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    70
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    71
code_reserved Haskell Nat
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
    72
38774
567b94f8bb6e tuned includes
haftmann
parents: 38771
diff changeset
    73
code_include Scala "Nat"
38968
e55deaa22fff do not print object frame around Scala includes -- this is in the responsibility of the user
haftmann
parents: 38857
diff changeset
    74
{*object Nat {
34899
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    75
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    76
  def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    77
  def apply(numeral: Int): Nat = Nat(BigInt(numeral))
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    78
  def apply(numeral: String): Nat = Nat(BigInt(numeral))
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    79
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    80
}
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    81
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    82
class Nat private(private val value: BigInt) {
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    83
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    84
  override def hashCode(): Int = this.value.hashCode()
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    85
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    86
  override def equals(that: Any): Boolean = that match {
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    87
    case that: Nat => this equals that
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    88
    case _ => false
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    89
  }
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    90
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    91
  override def toString(): String = this.value.toString
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    92
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    93
  def equals(that: Nat): Boolean = this.value == that.value
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    94
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    95
  def as_BigInt: BigInt = this.value
39781
2053638a2bf2 scala is reserved identifier
haftmann
parents: 39302
diff changeset
    96
  def as_Int: Int = if (this.value >= scala.Int.MinValue && this.value <= scala.Int.MaxValue)
34944
970e1466028d code literals: distinguish numeral classes by different entries
haftmann
parents: 34902
diff changeset
    97
      this.value.intValue
37969
3bf1fffcdd48 corrected range check once more
haftmann
parents: 37958
diff changeset
    98
    else error("Int value out of range: " + this.value.toString)
34899
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
    99
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   100
  def +(that: Nat): Nat = new Nat(this.value + that.value)
37223
5226259b6fa2 corrected implementation
haftmann
parents: 37050
diff changeset
   101
  def -(that: Nat): Nat = Nat(this.value - that.value)
34899
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   102
  def *(that: Nat): Nat = new Nat(this.value * that.value)
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   103
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   104
  def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   105
    else {
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   106
      val (k, l) = this.value /% that.value
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   107
      (new Nat(k), new Nat(l))
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   108
    }
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   109
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   110
  def <=(that: Nat): Boolean = this.value <= that.value
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   111
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   112
  def <(that: Nat): Boolean = this.value < that.value
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   113
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   114
}
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   115
*}
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   116
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   117
code_reserved Scala Nat
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   118
25967
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
   119
code_type nat
29793
86cac1fab613 changed name space policy for Haskell includes
haftmann
parents: 29657
diff changeset
   120
  (Haskell "Nat.Nat")
38968
e55deaa22fff do not print object frame around Scala includes -- this is in the responsibility of the user
haftmann
parents: 38857
diff changeset
   121
  (Scala "Nat")
25967
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
   122
38857
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 38774
diff changeset
   123
code_instance nat :: equal
25967
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
   124
  (Haskell -)
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
   125
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   126
setup {*
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   127
  fold (Numeral.add_code @{const_name nat_of_num}
37958
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
   128
    false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell", "Scala"]
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   129
*}
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   130
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   131
code_const "0::nat"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   132
  (SML "0")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   133
  (OCaml "Big'_int.zero'_big'_int")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   134
  (Haskell "0")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   135
  (Scala "Nat(0)")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   136
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   137
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   138
subsection {* Conversions *}
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   139
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   140
text {*
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   141
  Since natural numbers are implemented
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   142
  using integers in ML, the coercion function @{term "int"} of type
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   143
  @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 37223
diff changeset
   144
  For the @{const nat} function for converting an integer to a natural
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   145
  number, we give a specific implementation using an ML expression that
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   146
  returns its input value, provided that it is non-negative, and otherwise
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   147
  returns @{text "0"}.
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   148
*}
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   149
32073
0a83608e21f1 additional preprocessor rule
haftmann
parents: 32069
diff changeset
   150
definition int :: "nat \<Rightarrow> int" where
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   151
  [code_abbrev]: "int = of_nat"
32073
0a83608e21f1 additional preprocessor rule
haftmann
parents: 32069
diff changeset
   152
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   153
code_const int
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   154
  (SML "_")
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   155
  (OCaml "_")
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   156
25967
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
   157
code_const nat
43653
905f17258bca tuned typo
haftmann
parents: 43324
diff changeset
   158
  (SML "IntInf.max/ (0,/ _)")
25967
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
   159
  (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   160
  (Eval "Integer.max/ 0")
25967
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
   161
35689
c3bef0c972d7 fixed typo
haftmann
parents: 35625
diff changeset
   162
text {* For Haskell and Scala, things are slightly different again. *}
25967
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
   163
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
   164
code_const int and nat
48431
6efff142bb54 restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
haftmann
parents: 48073
diff changeset
   165
  (Haskell "Prelude.toInteger" and "Prelude.fromInteger")
38968
e55deaa22fff do not print object frame around Scala includes -- this is in the responsibility of the user
haftmann
parents: 38857
diff changeset
   166
  (Scala "!_.as'_BigInt" and "Nat")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   167
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   168
text {* Alternativ implementation for @{const of_nat} *}
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   169
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   170
lemma [code]:
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   171
  "of_nat n = (if n = 0 then 0 else
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   172
     let
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   173
       (q, m) = divmod_nat n 2;
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   174
       q' = 2 * of_nat q
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   175
     in if m = 0 then q' else q' + 1)"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   176
proof -
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   177
  from mod_div_equality have *: "of_nat n = of_nat (n div 2 * 2 + n mod 2)" by simp
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   178
  show ?thesis
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   179
    apply (simp add: Let_def divmod_nat_div_mod mod_2_not_eq_zero_eq_one_nat
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   180
      of_nat_mult
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   181
      of_nat_add [symmetric])
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   182
    apply (auto simp add: of_nat_mult)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   183
    apply (simp add: * of_nat_mult add_commute mult_commute)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   184
    done
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   185
qed
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   186
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   187
text {* Conversion from and to code numerals *}
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   188
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
   189
code_const Code_Numeral.of_nat
25967
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
   190
  (SML "IntInf.toInt")
31377
a48f9ef9de15 OCaml builtin intergers are elusive; avoid
haftmann
parents: 31295
diff changeset
   191
  (OCaml "_")
48431
6efff142bb54 restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
haftmann
parents: 48073
diff changeset
   192
  (Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)")
38968
e55deaa22fff do not print object frame around Scala includes -- this is in the responsibility of the user
haftmann
parents: 38857
diff changeset
   193
  (Scala "!Natural(_.as'_BigInt)")
37958
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
   194
  (Eval "_")
25967
dd602eb20f3f fixed and tuned
haftmann
parents: 25931
diff changeset
   195
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
   196
code_const Code_Numeral.nat_of
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   197
  (SML "IntInf.fromInt")
31377
a48f9ef9de15 OCaml builtin intergers are elusive; avoid
haftmann
parents: 31295
diff changeset
   198
  (OCaml "_")
48431
6efff142bb54 restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
haftmann
parents: 48073
diff changeset
   199
  (Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)")
38968
e55deaa22fff do not print object frame around Scala includes -- this is in the responsibility of the user
haftmann
parents: 38857
diff changeset
   200
  (Scala "!Nat(_.as'_BigInt)")
37958
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
   201
  (Eval "_")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   202
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   203
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   204
subsection {* Target language arithmetic *}
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   205
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   206
code_const "plus \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   207
  (SML "IntInf.+/ ((_),/ (_))")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   208
  (OCaml "Big'_int.add'_big'_int")
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   209
  (Haskell infixl 6 "+")
34899
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   210
  (Scala infixl 7 "+")
37958
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
   211
  (Eval infixl 8 "+")
34899
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   212
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   213
code_const "minus \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   214
  (SML "IntInf.max/ (0, IntInf.-/ ((_),/ (_)))")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   215
  (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)")
34899
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   216
  (Haskell infixl 6 "-")
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   217
  (Scala infixl 7 "-")
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   218
  (Eval "Integer.max/ 0/ (_ -/ _)")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   219
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents: 48568
diff changeset
   220
code_const Code_Binary_Nat.dup
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   221
  (SML "IntInf.*/ (2,/ (_))")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   222
  (OCaml "Big'_int.mult'_big'_int/ 2")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   223
  (Haskell "!(2 * _)")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   224
  (Scala "!(2 * _)")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   225
  (Eval "!(2 * _)")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   226
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents: 48568
diff changeset
   227
code_const Code_Binary_Nat.sub
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   228
  (SML "!(raise/ Fail/ \"sub\")")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   229
  (OCaml "failwith/ \"sub\"")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   230
  (Haskell "error/ \"sub\"")
48073
1b609a7837ef prefer sys.error over plain error in Scala to avoid deprecation warning
haftmann
parents: 47108
diff changeset
   231
  (Scala "!sys.error(\"sub\")")
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   232
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   233
code_const "times \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   234
  (SML "IntInf.*/ ((_),/ (_))")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   235
  (OCaml "Big'_int.mult'_big'_int")
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   236
  (Haskell infixl 7 "*")
34899
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   237
  (Scala infixl 8 "*")
37958
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
   238
  (Eval infixl 9 "*")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   239
37958
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
   240
code_const divmod_nat
26009
b6a64fe38634 treating division by zero properly
haftmann
parents: 25967
diff changeset
   241
  (SML "IntInf.divMod/ ((_),/ (_))")
b6a64fe38634 treating division by zero properly
haftmann
parents: 25967
diff changeset
   242
  (OCaml "Big'_int.quomod'_big'_int")
b6a64fe38634 treating division by zero properly
haftmann
parents: 25967
diff changeset
   243
  (Haskell "divMod")
34899
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   244
  (Scala infixl 8 "/%")
37958
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
   245
  (Eval "Integer.div'_mod")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   246
38857
97775f3e8722 renamed class/constant eq to equal; tuned some instantiations
haftmann
parents: 38774
diff changeset
   247
code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   248
  (SML "!((_ : IntInf.int) = _)")
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   249
  (OCaml "Big'_int.eq'_big'_int")
39272
0b61951d2682 Haskell == is infix, not infixl
haftmann
parents: 39198
diff changeset
   250
  (Haskell infix 4 "==")
34899
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   251
  (Scala infixl 5 "==")
37958
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
   252
  (Eval infixl 6 "=")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   253
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   254
code_const "less_eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   255
  (SML "IntInf.<=/ ((_),/ (_))")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   256
  (OCaml "Big'_int.le'_big'_int")
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   257
  (Haskell infix 4 "<=")
34899
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   258
  (Scala infixl 4 "<=")
37958
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
   259
  (Eval infixl 6 "<=")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   260
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   261
code_const "less \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   262
  (SML "IntInf.</ ((_),/ (_))")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   263
  (OCaml "Big'_int.lt'_big'_int")
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   264
  (Haskell infix 4 "<")
34899
8674bb6f727b added Scala setup
haftmann
parents: 34893
diff changeset
   265
  (Scala infixl 4 "<")
37958
9728342bcd56 another refinement chapter in the neverending numeral story
haftmann
parents: 37947
diff changeset
   266
  (Eval infixl 6 "<")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   267
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   268
code_const Num.num_of_nat
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   269
  (SML "!(raise/ Fail/ \"num'_of'_nat\")")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   270
  (OCaml "failwith/ \"num'_of'_nat\"")
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   271
  (Haskell "error/ \"num'_of'_nat\"")
48073
1b609a7837ef prefer sys.error over plain error in Scala to avoid deprecation warning
haftmann
parents: 47108
diff changeset
   272
  (Scala "!sys.error(\"num'_of'_nat\")")
25931
b1d1ab3e5a2e streamlined and improved
haftmann
parents: 25919
diff changeset
   273
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   274
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   275
subsection {* Evaluation *}
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents: 27673
diff changeset
   276
28562
4e74209f113e `code func` now just `code`
haftmann
parents: 28522
diff changeset
   277
lemma [code, code del]:
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32348
diff changeset
   278
  "(Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term) = Code_Evaluation.term_of" ..
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents: 27673
diff changeset
   279
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32348
diff changeset
   280
code_const "Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term"
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents: 27673
diff changeset
   281
  (SML "HOLogic.mk'_number/ HOLogic.natT")
7ebe8dc06cbb evaluation using code generator
haftmann
parents: 27673
diff changeset
   282
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   283
text {*
48568
084cd758a8ab evaluation: allow multiple code modules
haftmann
parents: 48431
diff changeset
   284
  Evaluation with @{text "Quickcheck_Narrowing"} does not work yet,
084cd758a8ab evaluation: allow multiple code modules
haftmann
parents: 48431
diff changeset
   285
  since a couple of questions how to perform evaluations in Haskell are not that
084cd758a8ab evaluation: allow multiple code modules
haftmann
parents: 48431
diff changeset
   286
  clear yet.  Therefore, we simply deactivate the narrowing-based quickcheck
084cd758a8ab evaluation: allow multiple code modules
haftmann
parents: 48431
diff changeset
   287
  from here on.
45793
331ebffe0593 deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
bulwahn
parents: 45185
diff changeset
   288
*}
331ebffe0593 deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
bulwahn
parents: 45185
diff changeset
   289
331ebffe0593 deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
bulwahn
parents: 45185
diff changeset
   290
declare [[quickcheck_narrowing_active = false]] 
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents: 27673
diff changeset
   291
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   292
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   293
code_modulename SML
33364
2bd12592c5e8 tuned code setup
haftmann
parents: 33343
diff changeset
   294
  Efficient_Nat Arith
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   295
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   296
code_modulename OCaml
33364
2bd12592c5e8 tuned code setup
haftmann
parents: 33343
diff changeset
   297
  Efficient_Nat Arith
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   298
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   299
code_modulename Haskell
33364
2bd12592c5e8 tuned code setup
haftmann
parents: 33343
diff changeset
   300
  Efficient_Nat Arith
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   301
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   302
hide_const (open) int
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   303
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents:
diff changeset
   304
end
50023
28f3263d4d1b refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents: 48568
diff changeset
   305