author | haftmann |
Tue, 05 Jun 2012 07:10:51 +0200 | |
changeset 48073 | 1b609a7837ef |
parent 47108 | 2a1953f0d20d |
child 48431 | 6efff142bb54 |
permissions | -rw-r--r-- |
23854 | 1 |
(* Title: HOL/Library/Efficient_Nat.thy |
25931 | 2 |
Author: Stefan Berghofer, Florian Haftmann, TU Muenchen |
23854 | 3 |
*) |
4 |
||
25931 | 5 |
header {* Implementation of natural numbers by target-language integers *} |
23854 | 6 |
|
7 |
theory Efficient_Nat |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
8 |
imports Code_Nat Code_Integer Main |
23854 | 9 |
begin |
10 |
||
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 | 13 |
drastically by implementing natural numbers by target-language |
14 |
integers. To do this, just include this theory. |
|
23854 | 15 |
*} |
16 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
17 |
subsection {* Target language fundamentals *} |
25931 | 18 |
|
19 |
text {* |
|
25967 | 20 |
For ML, we map @{typ nat} to target language integers, where we |
34899 | 21 |
ensure that values are always non-negative. |
25931 | 22 |
*} |
23 |
||
24 |
code_type nat |
|
27496 | 25 |
(SML "IntInf.int") |
25931 | 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 | 28 |
|
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 | 31 |
is that we have to distinguish type class instances for @{typ nat} |
32 |
and @{typ int}. |
|
25967 | 33 |
*} |
34 |
||
38774 | 35 |
code_include Haskell "Nat" |
36 |
{*newtype Nat = Nat Integer deriving (Eq, Show, Read); |
|
25967 | 37 |
|
38 |
instance Num Nat where { |
|
39 |
fromInteger k = Nat (if k >= 0 then k else 0); |
|
40 |
Nat n + Nat m = Nat (n + m); |
|
41 |
Nat n - Nat m = fromInteger (n - m); |
|
42 |
Nat n * Nat m = Nat (n * m); |
|
43 |
abs n = n; |
|
44 |
signum _ = 1; |
|
45 |
negate n = error "negate Nat"; |
|
46 |
}; |
|
47 |
||
48 |
instance Ord Nat where { |
|
49 |
Nat n <= Nat m = n <= m; |
|
50 |
Nat n < Nat m = n < m; |
|
51 |
}; |
|
52 |
||
53 |
instance Real Nat where { |
|
54 |
toRational (Nat n) = toRational n; |
|
55 |
}; |
|
56 |
||
57 |
instance Enum Nat where { |
|
58 |
toEnum k = fromInteger (toEnum k); |
|
59 |
fromEnum (Nat n) = fromEnum n; |
|
60 |
}; |
|
61 |
||
62 |
instance Integral Nat where { |
|
63 |
toInteger (Nat n) = n; |
|
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 | 68 |
}; |
69 |
*} |
|
70 |
||
71 |
code_reserved Haskell Nat |
|
72 |
||
38774 | 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 | 75 |
|
76 |
def apply(numeral: BigInt): Nat = new Nat(numeral max 0) |
|
77 |
def apply(numeral: Int): Nat = Nat(BigInt(numeral)) |
|
78 |
def apply(numeral: String): Nat = Nat(BigInt(numeral)) |
|
79 |
||
80 |
} |
|
81 |
||
82 |
class Nat private(private val value: BigInt) { |
|
83 |
||
84 |
override def hashCode(): Int = this.value.hashCode() |
|
85 |
||
86 |
override def equals(that: Any): Boolean = that match { |
|
87 |
case that: Nat => this equals that |
|
88 |
case _ => false |
|
89 |
} |
|
90 |
||
91 |
override def toString(): String = this.value.toString |
|
92 |
||
93 |
def equals(that: Nat): Boolean = this.value == that.value |
|
94 |
||
95 |
def as_BigInt: BigInt = this.value |
|
39781 | 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 | 98 |
else error("Int value out of range: " + this.value.toString) |
34899 | 99 |
|
100 |
def +(that: Nat): Nat = new Nat(this.value + that.value) |
|
37223 | 101 |
def -(that: Nat): Nat = Nat(this.value - that.value) |
34899 | 102 |
def *(that: Nat): Nat = new Nat(this.value * that.value) |
103 |
||
104 |
def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this) |
|
105 |
else { |
|
106 |
val (k, l) = this.value /% that.value |
|
107 |
(new Nat(k), new Nat(l)) |
|
108 |
} |
|
109 |
||
110 |
def <=(that: Nat): Boolean = this.value <= that.value |
|
111 |
||
112 |
def <(that: Nat): Boolean = this.value < that.value |
|
113 |
||
114 |
} |
|
115 |
*} |
|
116 |
||
117 |
code_reserved Scala Nat |
|
118 |
||
25967 | 119 |
code_type nat |
29793 | 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 | 122 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38774
diff
changeset
|
123 |
code_instance nat :: equal |
25967 | 124 |
(Haskell -) |
125 |
||
25931 | 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 | 129 |
*} |
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 | 140 |
text {* |
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 | 143 |
@{typ "nat \<Rightarrow> int"} is simply implemented by the identity function. |
37388 | 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 | 146 |
returns its input value, provided that it is non-negative, and otherwise |
147 |
returns @{text "0"}. |
|
148 |
*} |
|
149 |
||
32073 | 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 | 152 |
|
25931 | 153 |
code_const int |
154 |
(SML "_") |
|
155 |
(OCaml "_") |
|
156 |
||
25967 | 157 |
code_const nat |
43653 | 158 |
(SML "IntInf.max/ (0,/ _)") |
25967 | 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 | 161 |
|
35689 | 162 |
text {* For Haskell and Scala, things are slightly different again. *} |
25967 | 163 |
|
164 |
code_const int and nat |
|
165 |
(Haskell "toInteger" and "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 | 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 | 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 | 190 |
(SML "IntInf.toInt") |
31377 | 191 |
(OCaml "_") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
192 |
(Haskell "!(fromInteger/ ./ 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 | 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 | 197 |
(SML "IntInf.fromInt") |
31377 | 198 |
(OCaml "_") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
199 |
(Haskell "!(fromInteger/ ./ 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 | 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 | 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 | 208 |
(OCaml "Big'_int.add'_big'_int") |
209 |
(Haskell infixl 6 "+") |
|
34899 | 210 |
(Scala infixl 7 "+") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
211 |
(Eval infixl 8 "+") |
34899 | 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 | 216 |
(Haskell infixl 6 "-") |
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 | 219 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
220 |
code_const Code_Nat.dup |
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 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
227 |
code_const Code_Nat.sub |
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 | 235 |
(OCaml "Big'_int.mult'_big'_int") |
236 |
(Haskell infixl 7 "*") |
|
34899 | 237 |
(Scala infixl 8 "*") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
238 |
(Eval infixl 9 "*") |
25931 | 239 |
|
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
240 |
code_const divmod_nat |
26009 | 241 |
(SML "IntInf.divMod/ ((_),/ (_))") |
242 |
(OCaml "Big'_int.quomod'_big'_int") |
|
243 |
(Haskell "divMod") |
|
34899 | 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 | 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 | 248 |
(SML "!((_ : IntInf.int) = _)") |
249 |
(OCaml "Big'_int.eq'_big'_int") |
|
39272 | 250 |
(Haskell infix 4 "==") |
34899 | 251 |
(Scala infixl 5 "==") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
252 |
(Eval infixl 6 "=") |
25931 | 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 | 256 |
(OCaml "Big'_int.le'_big'_int") |
257 |
(Haskell infix 4 "<=") |
|
34899 | 258 |
(Scala infixl 4 "<=") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
259 |
(Eval infixl 6 "<=") |
25931 | 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 | 263 |
(OCaml "Big'_int.lt'_big'_int") |
264 |
(Haskell infix 4 "<") |
|
34899 | 265 |
(Scala infixl 4 "<") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
266 |
(Eval infixl 6 "<") |
25931 | 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 | 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 | 276 |
|
28562 | 277 |
lemma [code, code del]: |
32657 | 278 |
"(Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term) = Code_Evaluation.term_of" .. |
28228 | 279 |
|
32657 | 280 |
code_const "Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term" |
28228 | 281 |
(SML "HOLogic.mk'_number/ HOLogic.natT") |
282 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
283 |
text {* |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
284 |
FIXME -- Evaluation with @{text "Quickcheck_Narrowing"} does not work, as |
45793
331ebffe0593
deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
bulwahn
parents:
45185
diff
changeset
|
285 |
@{text "code_module"} is very aggressive leading to bad Haskell code. |
331ebffe0593
deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
bulwahn
parents:
45185
diff
changeset
|
286 |
Therefore, we simply deactivate the narrowing-based quickcheck from here on. |
331ebffe0593
deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
bulwahn
parents:
45185
diff
changeset
|
287 |
*} |
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 |
declare [[quickcheck_narrowing_active = false]] |
28228 | 290 |
|
23854 | 291 |
|
292 |
code_modulename SML |
|
33364 | 293 |
Efficient_Nat Arith |
23854 | 294 |
|
295 |
code_modulename OCaml |
|
33364 | 296 |
Efficient_Nat Arith |
23854 | 297 |
|
298 |
code_modulename Haskell |
|
33364 | 299 |
Efficient_Nat Arith |
23854 | 300 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
301 |
hide_const (open) int |
23854 | 302 |
|
303 |
end |