author | haftmann |
Mon, 26 Jul 2010 11:10:35 +0200 | |
changeset 37968 | 52fdcb76c0af |
parent 37958 | 9728342bcd56 |
child 38053 | 9102e859dc0b |
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 |
|
37968 | 8 |
imports Main Code_Natural |
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 |
||
17 |
code_type int |
|
18 |
(SML "IntInf.int") |
|
19 |
(OCaml "Big'_int.big'_int") |
|
20 |
(Haskell "Integer") |
|
34899 | 21 |
(Scala "BigInt") |
24999 | 22 |
|
23 |
code_instance int :: eq |
|
24 |
(Haskell -) |
|
25 |
||
26 |
setup {* |
|
25928 | 27 |
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
|
28 |
true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] |
24999 | 29 |
*} |
30 |
||
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
31 |
code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1" |
24999 | 32 |
(SML "raise/ Fail/ \"Pls\"" |
33 |
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
|
34 |
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
|
35 |
and "!((_);/ raise/ Fail/ \"Bit1\")") |
24999 | 36 |
(OCaml "failwith/ \"Pls\"" |
37 |
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
|
38 |
and "!((_);/ failwith/ \"Bit0\")" |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
39 |
and "!((_);/ failwith/ \"Bit1\")") |
24999 | 40 |
(Haskell "error/ \"Pls\"" |
41 |
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
|
42 |
and "error/ \"Bit0\"" |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26009
diff
changeset
|
43 |
and "error/ \"Bit1\"") |
34899 | 44 |
(Scala "!error(\"Pls\")" |
45 |
and "!error(\"Min\")" |
|
46 |
and "!error(\"Bit0\")" |
|
47 |
and "!error(\"Bit1\")") |
|
48 |
||
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
49 |
code_const Int.pred |
24999 | 50 |
(SML "IntInf.- ((_), 1)") |
51 |
(OCaml "Big'_int.pred'_big'_int") |
|
52 |
(Haskell "!(_/ -/ 1)") |
|
34899 | 53 |
(Scala "!(_/ -/ 1)") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
54 |
(Eval "!(_/ -/ 1)") |
24999 | 55 |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25767
diff
changeset
|
56 |
code_const Int.succ |
24999 | 57 |
(SML "IntInf.+ ((_), 1)") |
58 |
(OCaml "Big'_int.succ'_big'_int") |
|
59 |
(Haskell "!(_/ +/ 1)") |
|
34899 | 60 |
(Scala "!(_/ +/ 1)") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
61 |
(Eval "!(_/ +/ 1)") |
24999 | 62 |
|
63 |
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
64 |
(SML "IntInf.+ ((_), (_))") |
|
65 |
(OCaml "Big'_int.add'_big'_int") |
|
66 |
(Haskell infixl 6 "+") |
|
34899 | 67 |
(Scala infixl 7 "+") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
68 |
(Eval infixl 8 "+") |
24999 | 69 |
|
70 |
code_const "uminus \<Colon> int \<Rightarrow> int" |
|
71 |
(SML "IntInf.~") |
|
72 |
(OCaml "Big'_int.minus'_big'_int") |
|
73 |
(Haskell "negate") |
|
34899 | 74 |
(Scala "!(- _)") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
75 |
(Eval "~/ _") |
24999 | 76 |
|
77 |
code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
78 |
(SML "IntInf.- ((_), (_))") |
|
79 |
(OCaml "Big'_int.sub'_big'_int") |
|
80 |
(Haskell infixl 6 "-") |
|
34899 | 81 |
(Scala infixl 7 "-") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
82 |
(Eval infixl 8 "-") |
24999 | 83 |
|
84 |
code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
|
85 |
(SML "IntInf.* ((_), (_))") |
|
86 |
(OCaml "Big'_int.mult'_big'_int") |
|
87 |
(Haskell infixl 7 "*") |
|
34899 | 88 |
(Scala infixl 8 "*") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
89 |
(Eval infixl 9 "*") |
24999 | 90 |
|
29936 | 91 |
code_const pdivmod |
34899 | 92 |
(SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") |
93 |
(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
|
94 |
(Haskell "divMod/ (abs _)/ (abs _)") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
95 |
(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
|
96 |
(Eval "Integer.div'_mod/ (abs _)/ (abs _)") |
29936 | 97 |
|
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28228
diff
changeset
|
98 |
code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
24999 | 99 |
(SML "!((_ : IntInf.int) = _)") |
100 |
(OCaml "Big'_int.eq'_big'_int") |
|
101 |
(Haskell infixl 4 "==") |
|
34899 | 102 |
(Scala infixl 5 "==") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
103 |
(Eval infixl 6 "=") |
24999 | 104 |
|
105 |
code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
106 |
(SML "IntInf.<= ((_), (_))") |
|
107 |
(OCaml "Big'_int.le'_big'_int") |
|
108 |
(Haskell infix 4 "<=") |
|
34899 | 109 |
(Scala infixl 4 "<=") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
110 |
(Eval infixl 6 "<=") |
24999 | 111 |
|
112 |
code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
|
113 |
(SML "IntInf.< ((_), (_))") |
|
114 |
(OCaml "Big'_int.lt'_big'_int") |
|
115 |
(Haskell infix 4 "<") |
|
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
116 |
(Scala infixl 4 "<") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
117 |
(Eval infixl 6 "<") |
24999 | 118 |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
119 |
code_const Code_Numeral.int_of |
31192 | 120 |
(SML "IntInf.fromInt") |
31377 | 121 |
(OCaml "_") |
37958
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
122 |
(Haskell "toInteger") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
123 |
(Scala "!_.as'_BigInt") |
9728342bcd56
another refinement chapter in the neverending numeral story
haftmann
parents:
37947
diff
changeset
|
124 |
(Eval "_") |
24999 | 125 |
|
28228 | 126 |
text {* Evaluation *} |
127 |
||
32657 | 128 |
code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term" |
31192 | 129 |
(Eval "HOLogic.mk'_number/ HOLogic.intT") |
28228 | 130 |
|
24999 | 131 |
end |