lemma integer_of_num [code]: "integer_of_num Num.One = 1" "integer_of_num (Num.Bit0 n) = (let k = integer_of_num n in k + k)" "integer_of_num (Num.Bit1 n) = (let k = integer_of_num n in k + k + 1)" by (simp_all only: integer_of_num_def numeral.simps Let_def)
instantiation integer :: linordered_euclidean_semiring_division begin
definition divmod_integer :: "num ==> num ==> integer × integer" where
divmod_integer'_def: "divmod_integer m n = (numeral m div numeral n, numeral m mod numeral n)"
definition divmod_step_integer :: "integer ==> integer × integer ==> integer × integer" where "divmod_step_integer l qr = (let (q, r) = qr in if ∣l∣≤∣r∣ then (2 * q + 1, r - l) else (2 * q, r))"
instanceby standard
(auto simp add: divmod_integer'_def divmod_step_integer_def integer_less_eq_iff)
end
lemma integer_of_nat_0: "integer_of_nat 0 = 0" by transfer simp
lemma integer_of_nat_1: "integer_of_nat 1 = 1" by transfer simp
lemma integer_of_nat_numeral: "integer_of_nat (numeral n) = numeral n" by transfer simp
subsection‹Code theorems for target language integers›
lift_definition sub :: "num ==> num ==> integer" is"λm n. numeral m - numeral n :: int"
.
lemma sub_code [code]: "sub Num.One Num.One = 0" "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)" "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)" "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)" "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" by (transfer; simp add: dbl_def dbl_inc_def dbl_dec_def)+
text‹Implementations›
lemma one_integer_code [code, code_unfold]: "1 = Pos Num.One" by simp
lemma plus_integer_code [code]: "k + 0 = (k::integer)" "0 + l = (l::integer)" "Pos m + Pos n = Pos (m + n)" "Pos m + Neg n = sub m n" "Neg m + Pos n = sub n m" "Neg m + Neg n = Neg (m + n)" by (transfer, simp)+
lemma uminus_integer_code [code]: "uminus 0 = (0::integer)" "uminus (Pos m) = Neg m" "uminus (Neg m) = Pos m" by simp_all
lemma minus_integer_code [code]: "k - 0 = (k::integer)" "0 - l = uminus (l::integer)" "Pos m - Pos n = sub m n" "Pos m - Neg n = Pos (m + n)" "Neg m - Pos n = Neg (m + n)" "Neg m - Neg n = sub n m" by (transfer, simp)+
lemma abs_integer_code [code]: "∣k∣ = (if (k::integer) < 0 then - k else k)" by simp
lemma sgn_integer_code [code]: "sgn k = (if k = 0 then 0 else if (k::integer) < 0 then - 1 else 1)" by simp
lemma times_integer_code [code]: "k * 0 = (0::integer)" "0 * l = (0::integer)" "Pos m * Pos n = Pos (m * n)" "Pos m * Neg n = Neg (m * n)" "Neg m * Pos n = Neg (m * n)" "Neg m * Neg n = Pos (m * n)" by simp_all
definition divmod_integer :: "integer ==> integer ==> integer × integer" where "divmod_integer k l = (k div l, k mod l)"
lemma fst_divmod_integer [simp]: "fst (divmod_integer k l) = k div l" by (simp add: divmod_integer_def)
lemma snd_divmod_integer [simp]: "snd (divmod_integer k l) = k mod l" by (simp add: divmod_integer_def)
definition divmod_abs :: "integer ==> integer ==> integer × integer" where "divmod_abs k l = (∣k∣ div ∣l∣, ∣k∣ mod ∣l∣)"
lemma fst_divmod_abs [simp]: "fst (divmod_abs k l) = ∣k∣ div ∣l∣" by (simp add: divmod_abs_def)
lemma snd_divmod_abs [simp]: "snd (divmod_abs k l) = ∣k∣ mod ∣l∣" by (simp add: divmod_abs_def)
lemma divmod_integer_eq_cases: "divmod_integer k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else (apsnd ∘ times ∘ sgn) l (if sgn k = sgn l then divmod_abs k l else (let (r, s) = divmod_abs k l in if s = 0 then (- r, 0) else (- r - 1, ∣l∣ - s))))" proof - have *: "sgn k = sgn l ⟷ k = 0 ∧ l = 0 ∨ 0 < l ∧ 0 < k ∨ l < 0 ∧ k < 0"for k l :: int by (auto simp add: sgn_if) have **: "- k = l * q ⟷ k = - (l * q)"for k l q :: int by auto show ?thesis by (simp add: divmod_integer_def divmod_abs_def)
(transfer, auto simp add: * ** not_less zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right) qed
lemma divmod_integer_code [code]: 🍋‹contributor ‹René Thiemann›\›🍋‹contributor ‹Akihisa Yamada›\› "divmod_integer k l = (if k = 0 then (0, 0) else if l > 0 then (if k > 0 then divmod_abs k l else case divmod_abs k l of (r, s) ==> if s = 0 then (- r, 0) else (- r - 1, l - s)) else if l = 0 then (0, k) else apsnd uminus (if k < 0 then divmod_abs k l else case divmod_abs k l of (r, s) ==> if s = 0 then (- r, 0) else (- r - 1, - l - s)))" by (cases l "0 :: integer" rule: linorder_cases)
(auto split: prod.splits simp add: divmod_integer_eq_cases)
lemma div_integer_code [code]: "k div l = fst (divmod_integer k l)" by simp
lemma mod_integer_code [code]: "k mod l = snd (divmod_integer k l)" by simp
context includes bit_operations_syntax begin
lemma and_integer_code [code]: ‹0 AND k = 0› ‹k AND 0 = 0› ‹Neg Num.One AND k = k› ‹k AND Neg Num.One = k› ‹Pos Num.One AND Pos Num.One = Pos Num.One› ‹Pos Num.One AND Pos (Num.Bit0 n) = 0› ‹Pos (Num.Bit0 m) AND Pos Num.One = 0› ‹Pos Num.One AND Pos (Num.Bit1 n) = Pos Num.One› ‹Pos (Num.Bit1 m) AND Pos Num.One = Pos Num.One› ‹Pos (Num.Bit0 m) AND Pos (Num.Bit0 n) = dup (Pos m AND Pos n)› ‹Pos (Num.Bit0 m) AND Pos (Num.Bit1 n) = dup (Pos m AND Pos n)› ‹Pos (Num.Bit1 m) AND Pos (Num.Bit0 n) = dup (Pos m AND Pos n)› ‹Pos (Num.Bit1 m) AND Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m AND Pos n)› ‹Pos m AND Neg (num.Bit0 n) = (case and_not_num m (Num.BitM n) of None ==> 0 | Some n' ==> Pos n')› ‹Neg (num.Bit0 m) AND Pos n = (case and_not_num n (Num.BitM m) of None ==> 0 | Some n' ==> Pos n')› ‹Pos m AND Neg (num.Bit1 n) = (case and_not_num m (Num.Bit0 n) of None ==> 0 | Some n' ==> Pos n')› ‹Neg (num.Bit1 m) AND Pos n = (case and_not_num n (Num.Bit0 m) of None ==> 0 | Some n' ==> Pos n')› ‹Neg m AND Neg n = NOT (sub m Num.One OR sub n Num.One)› for k :: integer by (transfer; simp)+
lemma or_integer_code [code]: ‹0 OR k = k› ‹k OR 0 = k› ‹Neg Num.One OR k = Neg Num.One› ‹k OR Neg Num.One = Neg Num.One› ‹Pos Num.One OR Pos Num.One = Pos Num.One› ‹Pos Num.One OR Pos (Num.Bit0 n) = Pos (Num.Bit1 n)› ‹Pos (Num.Bit0 m) OR Pos Num.One = Pos (Num.Bit1 m)› ‹Pos Num.One OR Pos (Num.Bit1 n) = Pos (Num.Bit1 n)› ‹Pos (Num.Bit1 m) OR Pos Num.One = Pos (Num.Bit1 m)› ‹Pos (Num.Bit0 m) OR Pos (Num.Bit0 n) = dup (Pos m OR Pos n)› ‹Pos (Num.Bit0 m) OR Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m OR Pos n)› ‹Pos (Num.Bit1 m) OR Pos (Num.Bit0 n) = Pos Num.One + dup (Pos m OR Pos n)› ‹Pos (Num.Bit1 m) OR Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m OR Pos n)› ‹Pos m OR Neg (num.Bit0 n) = Neg (or_not_num_neg m (Num.BitM n))› ‹Neg (num.Bit0 m) OR Pos n = Neg (or_not_num_neg n (Num.BitM m))› ‹Pos m OR Neg (num.Bit1 n) = Neg (or_not_num_neg m (Num.Bit0 n))› ‹Neg (num.Bit1 m) OR Pos n = Neg (or_not_num_neg n (Num.Bit0 m))› ‹Neg m OR Neg n = NOT (sub m Num.One AND sub n Num.One)› for k :: integer by (transfer; simp)+
lemma xor_integer_code [code]: ‹0 XOR k = k› ‹k XOR 0 = k› ‹Neg Num.One XOR k = NOT k› ‹k XOR Neg Num.One = NOT k› ‹Neg m XOR k = NOT (sub m num.One XOR k)› ‹k XOR Neg n = NOT (k XOR (sub n num.One))› ‹Pos Num.One XOR Pos Num.One = 0› ‹Pos Num.One XOR Pos (Num.Bit0 n) = Pos (Num.Bit1 n)› ‹Pos (Num.Bit0 m) XOR Pos Num.One = Pos (Num.Bit1 m)› ‹Pos Num.One XOR Pos (Num.Bit1 n) = Pos (Num.Bit0 n)› ‹Pos (Num.Bit1 m) XOR Pos Num.One = Pos (Num.Bit0 m)› ‹Pos (Num.Bit0 m) XOR Pos (Num.Bit0 n) = dup (Pos m XOR Pos n)› ‹Pos (Num.Bit0 m) XOR Pos (Num.Bit1 n) = Pos Num.One + dup (Pos m XOR Pos n)› ‹Pos (Num.Bit1 m) XOR Pos (Num.Bit0 n) = Pos Num.One + dup (Pos m XOR Pos n)› ‹Pos (Num.Bit1 m) XOR Pos (Num.Bit1 n) = dup (Pos m XOR Pos n)› for k :: integer by (transfer; simp)+
lemma [code]: ‹NOT k = - k - 1›for k :: integer by (fact not_eq_complement)
lemma [code]: ‹bit k n ⟷ k AND push_bit n 1 ≠ (0 :: integer)› by (simp add: and_exp_eq_0_iff_not_bit)
lemma [code]: ‹mask n = push_bit n 1 - (1 :: integer)› by (simp add: mask_eq_exp_minus_1)
lemma [code]: ‹set_bit n k = k OR push_bit n 1›for k :: integer by (fact set_bit_def)
lemma [code]: ‹unset_bit n k = k AND NOT (push_bit n 1)›for k :: integer by (fact unset_bit_def)
lemma [code]: ‹flip_bit n k = k XOR push_bit n 1›for k :: integer by (fact flip_bit_def)
lemma [code]: ‹take_bit n k = k AND mask n›for k :: integer by (fact take_bit_eq_mask)
end
definition bit_cut_integer :: "integer ==> integer × bool" where"bit_cut_integer k = (k div 2, odd k)"
lemma bit_cut_integer_code [code]: "bit_cut_integer k = (if k = 0 then (0, False) else let (r, s) = Code_Numeral.divmod_abs k 2 in (if k > 0 then r else - r - s, s = 1))" proof - have"bit_cut_integer k = (let (r, s) = divmod_integer k 2 in (r, s = 1))" by (simp add: divmod_integer_def bit_cut_integer_def odd_iff_mod_2_eq_one) thenshow ?thesis by (simp add: divmod_integer_code) (auto simp add: split_def) qed
lemma equal_integer_refl [code nbe]: "HOL.equal (k::integer) k ⟷ True" by (fact equal_refl)
lemma less_eq_integer_code [code]: "0 ≤ (0::integer) ⟷ True" "0 ≤ Pos l ⟷ True" "0 ≤ Neg l ⟷ False" "Pos k ≤ 0 ⟷ False" "Pos k ≤ Pos l ⟷ k ≤ l" "Pos k ≤ Neg l ⟷ False" "Neg k ≤ 0 ⟷ True" "Neg k ≤ Pos l ⟷ True" "Neg k ≤ Neg l ⟷ l ≤ k" by simp_all
lemma less_integer_code [code]: "0 < (0::integer) ⟷ False" "0 < Pos l ⟷ True" "0 < Neg l ⟷ False" "Pos k < 0 ⟷ False" "Pos k < Pos l ⟷ k < l" "Pos k < Neg l ⟷ False" "Neg k < 0 ⟷ True" "Neg k < Pos l ⟷ True" "Neg k < Neg l ⟷ l < k" by simp_all
lemma num_of_integer_code [code]: "num_of_integer k = (if k ≤ 1 then Num.One else let (l, j) = divmod_integer k 2; l' = num_of_integer l; l'' = l' + l' in if j = 0 then l'' else l'' + Num.One)" proof -
{ assume"int_of_integer k mod 2 = 1" thenhave"nat (int_of_integer k mod 2) = nat 1"by simp moreoverassume *: "1 < int_of_integer k" ultimatelyhave **: "nat (int_of_integer k) mod 2 = 1"by (simp add: nat_mod_distrib) have"num_of_nat (nat (int_of_integer k)) = num_of_nat (2 * (nat (int_of_integer k) div 2) + nat (int_of_integer k) mod 2)" by simp thenhave"num_of_nat (nat (int_of_integer k)) = num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + nat (int_of_integer k) mod 2)" by (simp add: mult_2) with ** have"num_of_nat (nat (int_of_integer k)) = num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + 1)" by simp
} note aux = this show ?thesis by (auto simp add: num_of_integer_def nat_of_integer_def Let_def case_prod_beta
not_le integer_eq_iff less_eq_integer_def
nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib
mult_2 [where 'a=nat] aux add_One) qed
lemma nat_of_integer_code [code]: "nat_of_integer k = (if k ≤ 0 then 0 else let (l, j) = divmod_integer k 2; l' = nat_of_integer l; l'' = l' + l' in if j = 0 then l'' else l'' + 1)" proof - obtain j where k: "k = integer_of_int j" proof show"k = integer_of_int (int_of_integer k)"by simp qed have *: "nat j mod 2 = nat_of_integer (of_int j mod 2)"if"j ≥ 0" using that by transfer (simp add: nat_mod_distrib) from k show ?thesis by (auto simp add: split_def Let_def nat_of_integer_def nat_div_distrib mult_2 [symmetric]
minus_mod_eq_mult_div [symmetric] *) qed
lemma int_of_integer_code [code]: ‹int_of_integer k = ( if k = 0 then 0 else if k = - 1 then - 1 else let (l, j) = divmod_integer k 2; l' = 2 * int_of_integer l in if j = 0 then l' else l' + 1)› by (auto simp add: case_prod_unfold Let_def integer_eq_iff simp flip: minus_mod_eq_mult_div)
lemma integer_of_int_code [code]: ‹integer_of_int k = ( if k = 0 then 0 else if k = - 1 then - 1 else let l = 2 * integer_of_int (k div 2); j = k mod 2 in if j = 0 then l else l + 1)› by (simp add: integer_eq_iff Let_def flip: minus_mod_eq_mult_div)
hide_const (open) Pos Neg sub dup divmod_abs
context begin
qualified definition push_bit :: ‹integer ==> integer ==> integer› where‹push_bit i k = Bit_Operations.push_bit (nat_of_integer ∣i∣) k›
qualified lemma push_bit_code [code]: ‹push_bit i k = k * 2 ^ nat_of_integer ∣i∣› by (simp add: push_bit_def push_bit_eq_mult)
lemma push_bit_integer_code [code]: ‹Bit_Operations.push_bit n k = push_bit (of_nat n) k› by (simp add: push_bit_def)
qualified definition drop_bit :: ‹integer ==> integer ==> integer› where‹drop_bit i k = Bit_Operations.drop_bit (nat_of_integer ∣i∣) k›
qualified lemma drop_bit_code [code]: ‹drop_bit i k = k div 2 ^ nat_of_integer ∣i∣› by (simp add: drop_bit_def drop_bit_eq_div)
lemma drop_bit_integer_code [code]: ‹Bit_Operations.drop_bit n k = drop_bit (of_nat n) k› by (simp add: drop_bit_def)
end
subsection‹Serializer setup for target language integers›
code_printing
type_constructor integer ⇀
(SML) "IntInf.int" and (OCaml) "Z.t" and (Haskell) "Integer" and (Scala) "BigInt" and (Eval) "int"
| class_instance integer :: equal ⇀
(Haskell) -
code_reserved
(Eval) int Integer
code_printing
constant "0::integer"⇀
(SML) "!(0/ :/ IntInf.int)" and (OCaml) "Z.zero" and (Haskell) "!(0/ ::/ Integer)" and (Scala) "BigInt(0)"
code_printing
constant "plus :: integer ==> _ ==> _"⇀
(SML) "IntInf.+ ((_), (_))" and (OCaml) "Z.add" and (Haskell) infixl 6 "+" and (Scala) infixl 7 "+" and (Eval) infixl 8 "+"
| constant "uminus :: integer ==> _"⇀
(SML) "IntInf.~" and (OCaml) "Z.neg" and (Haskell) "negate" and (Scala) "!(- _)" and (Eval) "~/ _"
| constant "minus :: integer ==> _"⇀
(SML) "IntInf.- ((_), (_))" and (OCaml) "Z.sub" and (Haskell) infixl 6 "-" and (Scala) infixl 7 "-" and (Eval) infixl 8 "-"
| constant Code_Numeral.dup ⇀
(SML) "IntInf.*/ (2,/ (_))" and (OCaml) "Z.shift'_left/ _/ 1" and (Haskell) "!(2 * _)" and (Scala) "!(2 * _)" and (Eval) "!(2 * _)"
| constant Code_Numeral.sub ⇀
(SML) "!(raise/ Fail/ \"sub\")" and (OCaml) "failwith/ \"sub\"" and (Haskell) "error/ \"sub\"" and (Scala) "!sys.error(\"sub\")"
| constant "times :: integer ==> _ ==> _"⇀
(SML) "IntInf.* ((_), (_))" and (OCaml) "Z.mul" and (Haskell) infixl 7 "*" and (Scala) infixl 8 "*" and (Eval) infixl 9 "*"
| constant Code_Numeral.divmod_abs ⇀
(SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)" and (OCaml) "!(fun k l ->/ if Z.equal Z.zero l then/ (Z.zero, l) else/ Z.div'_rem/ (Z.abs k)/ (Z.abs l))" and (Haskell) "divMod/ (abs _)/ (abs _)" and (Scala) "!((k: BigInt) => (l: BigInt) =>/ l == 0 match { case true => (BigInt(0), k) case false => (k.abs '/% l.abs) })" and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)"
| constant "HOL.equal :: integer ==> _ ==> bool"⇀
(SML) "!((_ : IntInf.int) = _)" and (OCaml) "Z.equal" and (Haskell) infix 4 "==" and (Scala) infixl 5 "==" and (Eval) infixl 6 "="
| constant "less_eq :: integer ==> _ ==> bool"⇀
(SML) "IntInf.<= ((_), (_))" and (OCaml) "Z.leq" and (Haskell) infix 4 "<=" and (Scala) infixl 4 "<=" and (Eval) infixl 6 "<="
| constant "less :: integer ==> _ ==> bool"⇀
(SML) "IntInf.< ((_), (_))" and (OCaml) "Z.lt" and (Haskell) infix 4 "<" and (Scala) infixl 4 "<" and (Eval) infixl 6 "<"
| constant "abs :: integer ==> _"⇀
(SML) "IntInf.abs" and (OCaml) "Z.abs" and (Haskell) "Prelude.abs" and (Scala) "_.abs" and (Eval) "abs"
| constant "Bit_Operations.and :: integer ==> integer ==> integer"⇀
(SML) "IntInf.andb ((_),/ (_))" and (OCaml) "Z.logand" and (Haskell) infixl 7 ".&." and (Scala) infixl 3 "&"
| constant "Bit_Operations.or :: integer ==> integer ==> integer"⇀
(SML) "IntInf.orb ((_),/ (_))" and (OCaml) "Z.logor" and (Haskell) infixl 5 ".|." and (Scala) infixl 1 "|"
| constant "Bit_Operations.xor :: integer ==> integer ==> integer"⇀
(SML) "IntInf.xorb ((_),/ (_))" and (OCaml) "Z.logxor" and (Haskell) infixl 6 ".^." and (Scala) infixl 2 "^"
| constant "Bit_Operations.not :: integer ==> integer"⇀
(SML) "IntInf.notb" and (OCaml) "Z.lognot" and (Haskell) "Data.Bits.complement" and (Scala) "_.unary'_~"
code_reserved
(Eval) abs
code_printing code_module Bit_Shifts ⇀
(SML) ‹ structure Bit_Shifts : sig type int = IntInf.int val push : int -> int -> int val drop : int -> int -> int end = struct open IntInf; fun fold _ [] y = y | fold f (x :: xs) y = fold f xs (f x y); fun replicate n x = (if n 🚫0 then [] else x :: replicate (n - 1) x); val max_index = pow (fromInt 2, Word.wordSize) - fromInt 1; (*largest possible word*)
val word_of_int = Word.fromLargeInt o toLarge;
val word_max_index = word_of_int max_index;
fun words_of_int k = case divMod (k, max_index)
of (b, s) => word_of_int s :: replicate b word_max_index;
fun push' i k = << (k, i);
fun drop' i k = ~>> (k, i);
(* The implementations are formally total, though indices >~ max_index will produce heavy computation load *)
fun push i = fold push' (words_of_int (abs i));
fun drop i = fold drop' (words_of_int (abs i));
end;›for constant Code_Numeral.push_bit Code_Numeral.drop_bit and (OCaml) ‹ module Bit_Shifts : sig val push : Z.t -> Z.t -> Z.t val drop : Z.t -> Z.t -> Z.t end = struct let rec fold f xs y = match xs with [] -> y | (x :: xs) -> fold f xs (f x y);; let rec replicate n x = (if Z.leq n Z.zero then [] else x :: replicate (Z.pred n) x);; let max_index = Z.of_int max_int;; let splitIndex i = let (b, s) = Z.div_rem i max_index in Z.to_int s :: replicate b max_int;; let push' i k = Z.shift_left k i;; let drop' i k = Z.shift_right k i;; (* The implementations are formally total, though indices >~ max_index will produce heavy computation load *)
let push i = fold push' (splitIndex (Z.abs i));;
let drop i = fold drop' (splitIndex (Z.abs i));;
end;; ›for constant Code_Numeral.push_bit Code_Numeral.drop_bit and (Haskell) ‹ module Bit_Shifts (push, drop, push', drop') where import Prelude (Int, Integer, toInteger, fromInteger, maxBound, divMod, (-), (🚫, abs, flip) import GHC.Bits (Bits) import Data.Bits (shiftL, shiftR) fold :: (a -> b -> b) -> [a] -> b -> b fold _ [] y = y fold f (x : xs) y = fold f xs (f x y) replicate :: Integer -> a -> [a] replicate k x = if k 🚫0 then [] else x : replicate (k - 1) x maxIndex :: Integer maxIndex = toInteger (maxBound :: Int) splitIndex :: Integer -> [Int] splitIndex i = fromInteger s : replicate (fromInteger b) maxBound where (b, s) = i `divMod` maxIndex {- The implementations are formally total, though indices >~ maxIndex will produce heavy computation load -} push :: Integer -> Integer -> Integer push i = fold (flip shiftL) (splitIndex (abs i)) drop :: Integer -> Integer -> Integer drop i = fold (flip shiftR) (splitIndex (abs i)) push' :: Int -> Int -> Int push' i = flip shiftL (abs i) drop' :: Int -> Int -> Int drop' i = flip shiftR (abs i) › and (Scala) ‹ object Bit_Shifts { private val maxIndex : BigInt = BigInt(Int.MaxValue); private def replicate[A](i : BigInt, x : A) : List[A] = i 🚫0 match { case true => Nil case false => x :: replicate[A](i - 1, x) } private def splitIndex(i : BigInt) : List[Int] = { val (b, s) = i /% maxIndex return s.intValue :: replicate(b, Int.MaxValue) } /* The implementations are formally total, though indices >~ maxIndex will produce heavy computation load */ def push(i: BigInt, k: BigInt) : BigInt = splitIndex(i).foldLeft(k) { (l, j) => l 🚫j } def drop(i: BigInt, k: BigInt) : BigInt = splitIndex(i).foldLeft(k) { (l, j) => l >> j } } ›
code_reserved
(SML) Bit_Shifts and (Haskell) Bit_Shifts and (Scala) Bit_Shifts
code_printing
constant Code_Numeral.push_bit ⇀
(SML) "Bit'_Shifts.push" and (OCaml) "Bit'_Shifts.push" and (Haskell) "Bit'_Shifts.push" and (Scala) "Bit'_Shifts.push"
| constant Code_Numeral.drop_bit ⇀
(SML) "Bit'_Shifts.drop" and (OCaml) "Bit'_Shifts.drop" and (Haskell) "Bit'_Shifts.drop" and (Scala) "Bit'_Shifts.drop"
code_identifier code_module Code_Numeral ⇀ (SML) Arith and (OCaml) Arith and (Haskell) Arith
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
