author | haftmann |
Sat, 24 Jul 2010 18:08:41 +0200 | |
changeset 37958 | 9728342bcd56 |
parent 37947 | 844977c7abeb |
child 37968 | 52fdcb76c0af |
permissions | -rw-r--r-- |
24999 | 1 |
(* Title: HOL/Library/Code_Integer.thy |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Pretty integer literals for code generation *} |
|
6 |
||
7 |
theory Code_Integer |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31192
diff
changeset
|
8 |
imports Main |
24999 | 9 |
begin |
10 |
||
11 |
text {* |
|
12 |
HOL numeral expressions are mapped to integer literals |
|
13 |
in target languages, using predefined target language |
|
14 |
operations for abstract integer operations. |
|
15 |
*} |
|
16 |
||
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
17 |
text {* |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
18 |
Preliminary: alternative representation of @{typ code_numeral} |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
19 |
for @{text Haskell} and @{text Scala}. |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
20 |
*} |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
21 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
22 |
code_include Haskell "Natural" {* |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
23 |
newtype Natural = Natural Integer deriving (Eq, Show, Read); |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
24 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
25 |
instance Num Natural where { |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
26 |
fromInteger k = Natural (if k >= 0 then k else 0); |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
27 |
Natural n + Natural m = Natural (n + m); |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
28 |
Natural n - Natural m = fromInteger (n - m); |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
29 |
Natural n * Natural m = Natural (n * m); |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
30 |
abs n = n; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
31 |
signum _ = 1; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
32 |
negate n = error "negate Natural"; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
33 |
}; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
34 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
35 |
instance Ord Natural where { |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
36 |
Natural n <= Natural m = n <= m; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
37 |
Natural n < Natural m = n < m; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
38 |
}; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
39 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
40 |
instance Real Natural where { |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
41 |
toRational (Natural n) = toRational n; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
42 |
}; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
43 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
44 |
instance Enum Natural where { |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
45 |
toEnum k = fromInteger (toEnum k); |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
46 |
fromEnum (Natural n) = fromEnum n; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
47 |
}; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
48 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
49 |
instance Integral Natural where { |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
50 |
toInteger (Natural n) = n; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
51 |
divMod n m = quotRem n m; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
52 |
quotRem (Natural n) (Natural m) |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
53 |
| (m == 0) = (0, Natural n) |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
54 |
| otherwise = (Natural k, Natural l) where (k, l) = quotRem n m; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
55 |
}; |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
56 |
*} |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
57 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
58 |
code_reserved Haskell Natural |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
59 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
60 |
code_include Scala "Natural" {* |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
61 |
import scala.Math |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
62 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
63 |
object Natural { |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
64 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
65 |
def apply(numeral: BigInt): Natural = new Natural(numeral max 0) |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
66 |
def apply(numeral: Int): Natural = Natural(BigInt(numeral)) |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
67 |
def apply(numeral: String): Natural = Natural(BigInt(numeral)) |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
68 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
69 |
} |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
70 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
71 |
class Natural private(private val value: BigInt) { |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
72 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
73 |
override def hashCode(): Int = this.value.hashCode() |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
74 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
75 |
override def equals(that: Any): Boolean = that match { |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
76 |
case that: Natural => this equals that |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
77 |
case _ => false |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
78 |
} |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
79 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
80 |
override def toString(): String = this.value.toString |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
81 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
82 |
def equals(that: Natural): Boolean = this.value == that.value |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
83 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
84 |
def as_BigInt: BigInt = this.value |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
85 |
def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue) |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
86 |
this.value.intValue |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
87 |
else this.value.intValue |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
88 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
89 |
def +(that: Natural): Natural = new Natural(this.value + that.value) |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
90 |
def -(that: Natural): Natural = Natural(this.value - that.value) |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
91 |
def *(that: Natural): Natural = new Natural(this.value * that.value) |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
92 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
93 |
def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this) |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
94 |
else { |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
95 |
val (k, l) = this.value /% that.value |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
96 |
(new Natural(k), new Natural(l)) |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
97 |
} |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
98 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
99 |
def <=(that: Natural): Boolean = this.value <= that.value |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
100 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
101 |
def <(that: Natural): Boolean = this.value < that.value |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
102 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
103 |
} |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
104 |
*} |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
105 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
106 |
code_reserved Scala Natural |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
107 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
108 |
code_type code_numeral |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
109 |
(Haskell "Natural.Natural") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
110 |
(Scala "Natural") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
111 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
112 |
setup {* |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
113 |
fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
114 |
false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"] |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
115 |
*} |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
116 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
117 |
code_instance code_numeral :: eq |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
118 |
(Haskell -) |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
119 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
120 |
code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
121 |
(Haskell infixl 6 "+") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
122 |
(Scala infixl 7 "+") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
123 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
124 |
code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
125 |
(Haskell infixl 6 "-") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
126 |
(Scala infixl 7 "-") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
127 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
128 |
code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
129 |
(Haskell infixl 7 "*") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
130 |
(Scala infixl 8 "*") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
131 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
132 |
code_const div_mod_code_numeral |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
133 |
(Haskell "divMod") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
134 |
(Scala infixl 8 "/%") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
135 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
136 |
code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool" |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
137 |
(Haskell infixl 4 "==") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
138 |
(Scala infixl 5 "==") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
139 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
140 |
code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool" |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
141 |
(Haskell infix 4 "<=") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
142 |
(Scala infixl 4 "<=") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
143 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
144 |
code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool" |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
145 |
(Haskell infix 4 "<") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
146 |
(Scala infixl 4 "<") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
147 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
148 |
text {* |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
149 |
Setup for @{typ int} proper. |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
150 |
*} |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
151 |
|
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
152 |
|
24999 | 153 |
code_type int |
154 |
(SML "IntInf.int") |
|
155 |
(OCaml "Big'_int.big'_int") |
|
156 |
(Haskell "Integer") |
|
34899 | 157 |
(Scala "BigInt") |
24999 | 158 |
|
159 |
code_instance int :: eq |
|
160 |
(Haskell -) |
|
161 |
||
162 |
setup {* |
|
25928 | 163 |
fold (Numeral.add_code @{const_name number_int_inst.number_of_int} |
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34899
diff
changeset
|
164 |
true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] |
24999 | 165 |
*} |
166 |
||
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
167 |
code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1" |
24999 | 168 |
(SML "raise/ Fail/ \"Pls\"" |
169 |
and "raise/ Fail/ \"Min\"" |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
170 |
and "!((_);/ raise/ Fail/ \"Bit0\")" |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
171 |
and "!((_);/ raise/ Fail/ \"Bit1\")") |
24999 | 172 |
(OCaml "failwith/ \"Pls\"" |
173 |
and "failwith/ \"Min\"" |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
174 |
and "!((_);/ failwith/ \"Bit0\")" |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
175 |
and "!((_);/ failwith/ \"Bit1\")") |
24999 | 176 |
(Haskell "error/ \"Pls\"" |
177 |
and "error/ \"Min\"" |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
178 |
and "error/ \"Bit0\"" |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
179 |
and "error/ \"Bit1\"") |
34899 | 180 |
(Scala "!error(\"Pls\")" |
181 |
and "!error(\"Min\")" |
|
182 |
and "!error(\"Bit0\")" |
|
183 |
and "!error(\"Bit1\")") |
|
184 |
||
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
185 |
code_const Int.pred |
24999 | 186 |
(SML "IntInf.- ((_), 1)") |
187 |
(OCaml "Big'_int.pred'_big'_int") |
|
188 |
(Haskell "!(_/ -/ 1)") |
|
34899 | 189 |
(Scala "!(_/ -/ 1)") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
190 |
(Eval "!(_/ -/ 1)") |
24999 | 191 |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
192 |
code_const Int.succ |
24999 | 193 |
(SML "IntInf.+ ((_), 1)") |
194 |
(OCaml "Big'_int.succ'_big'_int") |
|
195 |
(Haskell "!(_/ +/ 1)") |
|
34899 | 196 |
(Scala "!(_/ +/ 1)") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
197 |
(Eval "!(_/ +/ 1)") |
24999 | 198 |
|
199 |
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
200 |
(SML "IntInf.+ ((_), (_))") |
|
201 |
(OCaml "Big'_int.add'_big'_int") |
|
202 |
(Haskell infixl 6 "+") |
|
34899 | 203 |
(Scala infixl 7 "+") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
204 |
(Eval infixl 8 "+") |
24999 | 205 |
|
206 |
code_const "uminus \<Colon> int \<Rightarrow> int" |
|
207 |
(SML "IntInf.~") |
|
208 |
(OCaml "Big'_int.minus'_big'_int") |
|
209 |
(Haskell "negate") |
|
34899 | 210 |
(Scala "!(- _)") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
211 |
(Eval "~/ _") |
24999 | 212 |
|
213 |
code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
214 |
(SML "IntInf.- ((_), (_))") |
|
215 |
(OCaml "Big'_int.sub'_big'_int") |
|
216 |
(Haskell infixl 6 "-") |
|
34899 | 217 |
(Scala infixl 7 "-") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
218 |
(Eval infixl 8 "-") |
24999 | 219 |
|
220 |
code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
221 |
(SML "IntInf.* ((_), (_))") |
|
222 |
(OCaml "Big'_int.mult'_big'_int") |
|
223 |
(Haskell infixl 7 "*") |
|
34899 | 224 |
(Scala infixl 8 "*") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
225 |
(Eval infixl 9 "*") |
24999 | 226 |
|
29936 | 227 |
code_const pdivmod |
34899 | 228 |
(SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") |
229 |
(OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") |
|
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34899
diff
changeset
|
230 |
(Haskell "divMod/ (abs _)/ (abs _)") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
231 |
(Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
232 |
(Eval "Integer.div'_mod/ (abs _)/ (abs _)") |
29936 | 233 |
|
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28228
diff
changeset
|
234 |
code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
24999 | 235 |
(SML "!((_ : IntInf.int) = _)") |
236 |
(OCaml "Big'_int.eq'_big'_int") |
|
237 |
(Haskell infixl 4 "==") |
|
34899 | 238 |
(Scala infixl 5 "==") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
239 |
(Eval infixl 6 "=") |
24999 | 240 |
|
241 |
code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
242 |
(SML "IntInf.<= ((_), (_))") |
|
243 |
(OCaml "Big'_int.le'_big'_int") |
|
244 |
(Haskell infix 4 "<=") |
|
34899 | 245 |
(Scala infixl 4 "<=") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
246 |
(Eval infixl 6 "<=") |
24999 | 247 |
|
248 |
code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
249 |
(SML "IntInf.< ((_), (_))") |
|
250 |
(OCaml "Big'_int.lt'_big'_int") |
|
251 |
(Haskell infix 4 "<") |
|
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
252 |
(Scala infixl 4 "<") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
253 |
(Eval infixl 6 "<") |
24999 | 254 |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
255 |
code_const Code_Numeral.int_of |
31192 | 256 |
(SML "IntInf.fromInt") |
31377 | 257 |
(OCaml "_") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
258 |
(Haskell "toInteger") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
259 |
(Scala "!_.as'_BigInt") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
260 |
(Eval "_") |
24999 | 261 |
|
28228 | 262 |
text {* Evaluation *} |
263 |
||
32657 | 264 |
code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term" |
31192 | 265 |
(Eval "HOLogic.mk'_number/ HOLogic.intT") |
28228 | 266 |
|
24999 | 267 |
end |