38 and "!((_);/ failwith/ \"Bit1\")") |
41 and "!((_);/ failwith/ \"Bit1\")") |
39 (Haskell "error/ \"Pls\"" |
42 (Haskell "error/ \"Pls\"" |
40 and "error/ \"Min\"" |
43 and "error/ \"Min\"" |
41 and "error/ \"Bit0\"" |
44 and "error/ \"Bit0\"" |
42 and "error/ \"Bit1\"") |
45 and "error/ \"Bit1\"") |
|
46 (Scala "!error(\"Pls\")" |
|
47 and "!error(\"Min\")" |
|
48 and "!error(\"Bit0\")" |
|
49 and "!error(\"Bit1\")") |
|
50 |
43 |
51 |
44 code_const Int.pred |
52 code_const Int.pred |
45 (SML "IntInf.- ((_), 1)") |
53 (SML "IntInf.- ((_), 1)") |
46 (OCaml "Big'_int.pred'_big'_int") |
54 (OCaml "Big'_int.pred'_big'_int") |
47 (Haskell "!(_/ -/ 1)") |
55 (Haskell "!(_/ -/ 1)") |
|
56 (Scala "!(_/ -/ 1)") |
48 |
57 |
49 code_const Int.succ |
58 code_const Int.succ |
50 (SML "IntInf.+ ((_), 1)") |
59 (SML "IntInf.+ ((_), 1)") |
51 (OCaml "Big'_int.succ'_big'_int") |
60 (OCaml "Big'_int.succ'_big'_int") |
52 (Haskell "!(_/ +/ 1)") |
61 (Haskell "!(_/ +/ 1)") |
|
62 (Scala "!(_/ +/ 1)") |
53 |
63 |
54 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
64 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
55 (SML "IntInf.+ ((_), (_))") |
65 (SML "IntInf.+ ((_), (_))") |
56 (OCaml "Big'_int.add'_big'_int") |
66 (OCaml "Big'_int.add'_big'_int") |
57 (Haskell infixl 6 "+") |
67 (Haskell infixl 6 "+") |
|
68 (Scala infixl 7 "+") |
58 |
69 |
59 code_const "uminus \<Colon> int \<Rightarrow> int" |
70 code_const "uminus \<Colon> int \<Rightarrow> int" |
60 (SML "IntInf.~") |
71 (SML "IntInf.~") |
61 (OCaml "Big'_int.minus'_big'_int") |
72 (OCaml "Big'_int.minus'_big'_int") |
62 (Haskell "negate") |
73 (Haskell "negate") |
|
74 (Scala "!(- _)") |
63 |
75 |
64 code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
76 code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
65 (SML "IntInf.- ((_), (_))") |
77 (SML "IntInf.- ((_), (_))") |
66 (OCaml "Big'_int.sub'_big'_int") |
78 (OCaml "Big'_int.sub'_big'_int") |
67 (Haskell infixl 6 "-") |
79 (Haskell infixl 6 "-") |
|
80 (Scala infixl 7 "-") |
68 |
81 |
69 code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
82 code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int" |
70 (SML "IntInf.* ((_), (_))") |
83 (SML "IntInf.* ((_), (_))") |
71 (OCaml "Big'_int.mult'_big'_int") |
84 (OCaml "Big'_int.mult'_big'_int") |
72 (Haskell infixl 7 "*") |
85 (Haskell infixl 7 "*") |
|
86 (Scala infixl 8 "*") |
73 |
87 |
74 code_const pdivmod |
88 code_const pdivmod |
75 (SML "(fn k => fn l =>/ IntInf.divMod/ (IntInf.abs k,/ IntInf.abs l))") |
89 (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") |
76 (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))") |
90 (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") |
77 (Haskell "(\\k l ->/ divMod/ (abs k)/ (abs l))") |
91 (Haskell "divMod/ (abs _)/ (abs _))") |
|
92 (Scala "!(_.abs '/% _.abs)") |
78 |
93 |
79 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
94 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
80 (SML "!((_ : IntInf.int) = _)") |
95 (SML "!((_ : IntInf.int) = _)") |
81 (OCaml "Big'_int.eq'_big'_int") |
96 (OCaml "Big'_int.eq'_big'_int") |
82 (Haskell infixl 4 "==") |
97 (Haskell infixl 4 "==") |
|
98 (Scala infixl 5 "==") |
83 |
99 |
84 code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
100 code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
85 (SML "IntInf.<= ((_), (_))") |
101 (SML "IntInf.<= ((_), (_))") |
86 (OCaml "Big'_int.le'_big'_int") |
102 (OCaml "Big'_int.le'_big'_int") |
87 (Haskell infix 4 "<=") |
103 (Haskell infix 4 "<=") |
|
104 (Scala infixl 4 "<=") |
88 |
105 |
89 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
106 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool" |
90 (SML "IntInf.< ((_), (_))") |
107 (SML "IntInf.< ((_), (_))") |
91 (OCaml "Big'_int.lt'_big'_int") |
108 (OCaml "Big'_int.lt'_big'_int") |
92 (Haskell infix 4 "<") |
109 (Haskell infix 4 "<") |
|
110 (Scala infixl 4 "<=") |
93 |
111 |
94 code_const Code_Numeral.int_of |
112 code_const Code_Numeral.int_of |
95 (SML "IntInf.fromInt") |
113 (SML "IntInf.fromInt") |
96 (OCaml "_") |
114 (OCaml "_") |
97 (Haskell "toEnum") |
115 (Haskell "toEnum") |
|
116 (Scala "!BigInt(_)") |
98 |
117 |
99 code_reserved SML IntInf |
118 code_reserved SML IntInf |
|
119 code_reserved Scala BigInt |
100 |
120 |
101 text {* Evaluation *} |
121 text {* Evaluation *} |
102 |
122 |
103 code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term" |
123 code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term" |
104 (Eval "HOLogic.mk'_number/ HOLogic.intT") |
124 (Eval "HOLogic.mk'_number/ HOLogic.intT") |