equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Pretty integer literals for code generation *} |
6 header {* Pretty integer literals for code generation *} |
7 |
7 |
8 theory Pretty_Int |
8 theory Pretty_Int |
9 imports IntArith |
9 imports IntArith ML_Int |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text {* |
13 HOL numeral expressions are mapped to integer literals |
13 HOL numeral expressions are mapped to integer literals |
14 in target languages, using predefined target language |
14 in target languages, using predefined target language |
86 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
86 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
87 (SML "IntInf.< ((_), (_))") |
87 (SML "IntInf.< ((_), (_))") |
88 (OCaml "Big'_int.lt'_big'_int") |
88 (OCaml "Big'_int.lt'_big'_int") |
89 (Haskell infix 4 "<") |
89 (Haskell infix 4 "<") |
90 |
90 |
|
91 code_const ml_int_of_int and int_of_ml_int |
|
92 (SML "IntInf.toInt" and "IntInf.fromInt") |
|
93 (OCaml "Big'_int.int'_of'_big'_int" and "Big'_int.big'_int'_of'_int") |
|
94 (Haskell "_" and "_") |
|
95 |
91 code_reserved SML IntInf |
96 code_reserved SML IntInf |
92 code_reserved OCaml Big_int |
97 code_reserved OCaml Big_int |
93 |
98 |
94 end |
99 end |