equal
deleted
inserted
replaced
23 code_instance int :: eq |
23 code_instance int :: eq |
24 (Haskell -) |
24 (Haskell -) |
25 |
25 |
26 setup {* |
26 setup {* |
27 fold (Numeral.add_code @{const_name number_int_inst.number_of_int} |
27 fold (Numeral.add_code @{const_name number_int_inst.number_of_int} |
28 true true Code_Printer.str) ["SML", "OCaml", "Haskell", "Scala"] |
28 true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"] |
29 #> Numeral.add_code @{const_name number_int_inst.number_of_int} |
29 #> Numeral.add_code @{const_name number_int_inst.number_of_int} |
30 true true (fn s => (Pretty.block o map Code_Printer.str) ["BigInt", s]) "Scala" |
30 true Code_Printer.literal_numeral "Scala" |
31 *} |
31 *} |
32 |
32 |
33 code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1" |
33 code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1" |
34 (SML "raise/ Fail/ \"Pls\"" |
34 (SML "raise/ Fail/ \"Pls\"" |
35 and "raise/ Fail/ \"Min\"" |
35 and "raise/ Fail/ \"Min\"" |
86 (Scala infixl 8 "*") |
86 (Scala infixl 8 "*") |
87 |
87 |
88 code_const pdivmod |
88 code_const pdivmod |
89 (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") |
89 (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") |
90 (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") |
90 (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") |
91 (Haskell "divMod/ (abs _)/ (abs _))") |
91 (Haskell "divMod/ (abs _)/ (abs _)") |
92 (Scala "!(_.abs '/% _.abs)") |
92 (Scala "!(_.abs '/% _.abs)") |
93 |
93 |
94 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
94 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
95 (SML "!((_ : IntInf.int) = _)") |
95 (SML "!((_ : IntInf.int) = _)") |
96 (OCaml "Big'_int.eq'_big'_int") |
96 (OCaml "Big'_int.eq'_big'_int") |
111 |
111 |
112 code_const Code_Numeral.int_of |
112 code_const Code_Numeral.int_of |
113 (SML "IntInf.fromInt") |
113 (SML "IntInf.fromInt") |
114 (OCaml "_") |
114 (OCaml "_") |
115 (Haskell "toEnum") |
115 (Haskell "toEnum") |
116 (Scala "!BigInt(_)") |
116 (Scala "!BigInt((_))") |
117 |
|
118 code_reserved SML IntInf |
|
119 code_reserved Scala BigInt |
|
120 |
117 |
121 text {* Evaluation *} |
118 text {* Evaluation *} |
122 |
119 |
123 code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term" |
120 code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term" |
124 (Eval "HOLogic.mk'_number/ HOLogic.intT") |
121 (Eval "HOLogic.mk'_number/ HOLogic.intT") |