equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Pretty integer literals for code generation *} |
5 header {* Pretty integer literals for code generation *} |
6 |
6 |
7 theory Code_Integer |
7 theory Code_Integer |
8 imports Main |
8 imports Main Code_Index |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 HOL numeral expressions are mapped to integer literals |
12 HOL numeral expressions are mapped to integer literals |
13 in target languages, using predefined target language |
13 in target languages, using predefined target language |
89 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
89 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
90 (SML "IntInf.< ((_), (_))") |
90 (SML "IntInf.< ((_), (_))") |
91 (OCaml "Big'_int.lt'_big'_int") |
91 (OCaml "Big'_int.lt'_big'_int") |
92 (Haskell infix 4 "<") |
92 (Haskell infix 4 "<") |
93 |
93 |
|
94 code_const Code_Index.int_of |
|
95 (SML "IntInf.fromInt") |
|
96 (OCaml "Big'_int.big'_int'_of'_int") |
|
97 (Haskell "toEnum") |
|
98 |
94 code_reserved SML IntInf |
99 code_reserved SML IntInf |
95 code_reserved OCaml Big_int |
100 code_reserved OCaml Big_int |
96 |
101 |
97 text {* Evaluation *} |
102 text {* Evaluation *} |
98 |
103 |
99 lemma [code, code del]: |
|
100 "(Code_Eval.term_of \<Colon> int \<Rightarrow> term) = Code_Eval.term_of" .. |
|
101 |
|
102 code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term" |
104 code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term" |
103 (SML "HOLogic.mk'_number/ HOLogic.intT") |
105 (Eval "HOLogic.mk'_number/ HOLogic.intT") |
104 |
106 |
105 end |
107 end |