Theory Uint16
chapter ‹Unsigned words of 16 bits›
theory Uint16 imports
Word_Type_Copies
Code_Target_Integer_Bit
begin
text ‹
Restriction for ML code generation:
This theory assumes that the ML system provides a Word16
implementation (mlton does, but PolyML 5.5 does not).
Therefore, the code setup lives in the target ‹SML_word›
rather than ‹SML›. This ensures that code generation still
works as long as ‹uint16› is not involved.
For the target ‹SML› itself, no special code generation
for this type is set up. Nevertheless, it should work by emulation via \<^typ>‹16 word›
if the theory \<^text>‹Code_Target_Int_Bit› is imported.
Restriction for OCaml code generation:
OCaml does not provide an int16 type, so no special code generation
for this type is set up.
›
section ‹Type definition and primitive operations›
typedef uint16 = ‹UNIV :: 16 word set› ..
global_interpretation uint16: word_type_copy Abs_uint16 Rep_uint16
using type_definition_uint16 by (rule word_type_copy.intro)
setup_lifting type_definition_uint16
declare uint16.of_word_of [code abstype]
declare Quotient_uint16 [transfer_rule]
instantiation uint16 :: ‹{comm_ring_1, semiring_modulo, equal, linorder}›
begin
lift_definition zero_uint16 :: uint16 is 0 .
lift_definition one_uint16 :: uint16 is 1 .
lift_definition plus_uint16 :: ‹uint16 ⇒ uint16 ⇒ uint16› is ‹(+)› .
lift_definition uminus_uint16 :: ‹uint16 ⇒ uint16› is uminus .
lift_definition minus_uint16 :: ‹uint16 ⇒ uint16 ⇒ uint16› is ‹(-)› .
lift_definition times_uint16 :: ‹uint16 ⇒ uint16 ⇒ uint16› is ‹(*)› .
lift_definition divide_uint16 :: ‹uint16 ⇒ uint16 ⇒ uint16› is ‹(div)› .
lift_definition modulo_uint16 :: ‹uint16 ⇒ uint16 ⇒ uint16› is ‹(mod)› .
lift_definition equal_uint16 :: ‹uint16 ⇒ uint16 ⇒ bool› is ‹HOL.equal› .
lift_definition less_eq_uint16 :: ‹uint16 ⇒ uint16 ⇒ bool› is ‹(≤)› .
lift_definition less_uint16 :: ‹uint16 ⇒ uint16 ⇒ bool› is ‹(<)› .
global_interpretation uint16: word_type_copy_ring Abs_uint16 Rep_uint16
by standard (fact zero_uint16.rep_eq one_uint16.rep_eq
plus_uint16.rep_eq uminus_uint16.rep_eq minus_uint16.rep_eq
times_uint16.rep_eq divide_uint16.rep_eq modulo_uint16.rep_eq
equal_uint16.rep_eq less_eq_uint16.rep_eq less_uint16.rep_eq)+
instance proof -
show ‹OFCLASS(uint16, comm_ring_1_class)›
by (rule uint16.of_class_comm_ring_1)
show ‹OFCLASS(uint16, semiring_modulo_class)›
by (fact uint16.of_class_semiring_modulo)
show ‹OFCLASS(uint16, equal_class)›
by (fact uint16.of_class_equal)
show ‹OFCLASS(uint16, linorder_class)›
by (fact uint16.of_class_linorder)
qed
end
instantiation uint16 :: ring_bit_operations
begin
lift_definition bit_uint16 :: ‹uint16 ⇒ nat ⇒ bool› is bit .
lift_definition not_uint16 :: ‹uint16 ⇒ uint16› is ‹Bit_Operations.not› .
lift_definition and_uint16 :: ‹uint16 ⇒ uint16 ⇒ uint16› is ‹Bit_Operations.and› .
lift_definition or_uint16 :: ‹uint16 ⇒ uint16 ⇒ uint16› is ‹Bit_Operations.or› .
lift_definition xor_uint16 :: ‹uint16 ⇒ uint16 ⇒ uint16› is ‹Bit_Operations.xor› .
lift_definition mask_uint16 :: ‹nat ⇒ uint16› is mask .
lift_definition push_bit_uint16 :: ‹nat ⇒ uint16 ⇒ uint16› is push_bit .
lift_definition drop_bit_uint16 :: ‹nat ⇒ uint16 ⇒ uint16› is drop_bit .
lift_definition signed_drop_bit_uint16 :: ‹nat ⇒ uint16 ⇒ uint16› is signed_drop_bit .
lift_definition take_bit_uint16 :: ‹nat ⇒ uint16 ⇒ uint16› is take_bit .
lift_definition set_bit_uint16 :: ‹nat ⇒ uint16 ⇒ uint16› is Bit_Operations.set_bit .
lift_definition unset_bit_uint16 :: ‹nat ⇒ uint16 ⇒ uint16› is unset_bit .
lift_definition flip_bit_uint16 :: ‹nat ⇒ uint16 ⇒ uint16› is flip_bit .
global_interpretation uint16: word_type_copy_bits Abs_uint16 Rep_uint16 signed_drop_bit_uint16
by standard (fact bit_uint16.rep_eq not_uint16.rep_eq and_uint16.rep_eq or_uint16.rep_eq xor_uint16.rep_eq
mask_uint16.rep_eq push_bit_uint16.rep_eq drop_bit_uint16.rep_eq signed_drop_bit_uint16.rep_eq take_bit_uint16.rep_eq
set_bit_uint16.rep_eq unset_bit_uint16.rep_eq flip_bit_uint16.rep_eq)+
instance
by (fact uint16.of_class_ring_bit_operations)
end
lift_definition uint16_of_nat :: ‹nat ⇒ uint16›
is word_of_nat .
lift_definition nat_of_uint16 :: ‹uint16 ⇒ nat›
is unat .
lift_definition uint16_of_int :: ‹int ⇒ uint16›
is word_of_int .
lift_definition int_of_uint16 :: ‹uint16 ⇒ int›
is uint .
context
includes integer.lifting
begin
lift_definition Uint16 :: ‹integer ⇒ uint16›
is word_of_int .
lift_definition integer_of_uint16 :: ‹uint16 ⇒ integer›
is uint .
end
global_interpretation uint16: word_type_copy_more Abs_uint16 Rep_uint16 signed_drop_bit_uint16
uint16_of_nat nat_of_uint16 uint16_of_int int_of_uint16 Uint16 integer_of_uint16
apply standard
apply (simp_all add: uint16_of_nat.rep_eq nat_of_uint16.rep_eq
uint16_of_int.rep_eq int_of_uint16.rep_eq
Uint16.rep_eq integer_of_uint16.rep_eq integer_eq_iff)
done
instantiation uint16 :: "{size, msb, lsb, set_bit, bit_comprehension}"
begin
lift_definition size_uint16 :: ‹uint16 ⇒ nat› is size .
lift_definition msb_uint16 :: ‹uint16 ⇒ bool› is msb .
lift_definition lsb_uint16 :: ‹uint16 ⇒ bool› is lsb .
text ‹Workaround: avoid name space clash by spelling out \<^text>‹lift_definition› explicitly.›
definition set_bit_uint16 :: ‹uint16 ⇒ nat ⇒ bool ⇒ uint16›
where set_bit_uint16_eq: ‹set_bit_uint16 a n b = (if b then Bit_Operations.set_bit else unset_bit) n a›
context
includes lifting_syntax
begin
lemma set_bit_uint16_transfer [transfer_rule]:
‹(cr_uint16 ===> (=) ===> (⟷) ===> cr_uint16) Generic_set_bit.set_bit Generic_set_bit.set_bit›
by (simp only: set_bit_eq [abs_def] set_bit_uint16_eq [abs_def]) transfer_prover
end
lift_definition set_bits_uint16 :: ‹(nat ⇒ bool) ⇒ uint16› is set_bits .
lift_definition set_bits_aux_uint16 :: ‹(nat ⇒ bool) ⇒ nat ⇒ uint16 ⇒ uint16› is set_bits_aux .
global_interpretation uint16: word_type_copy_misc Abs_uint16 Rep_uint16 signed_drop_bit_uint16
uint16_of_nat nat_of_uint16 uint16_of_int int_of_uint16 Uint16 integer_of_uint16 16 set_bits_aux_uint16
by (standard; transfer) simp_all
instance using uint16.of_class_bit_comprehension
uint16.of_class_set_bit uint16.of_class_lsb
by simp_all standard
end
section ‹Code setup›
code_printing code_module Uint16 ⇀ (SML_word)
‹(* Test that words can handle numbers between 0 and 15 *)
val _ = if 4 <= Word.wordSize then () else raise (Fail ("wordSize less than 4"));
structure Uint16 : sig
val set_bit : Word16.word -> IntInf.int -> bool -> Word16.word
val shiftl : Word16.word -> IntInf.int -> Word16.word
val shiftr : Word16.word -> IntInf.int -> Word16.word
val shiftr_signed : Word16.word -> IntInf.int -> Word16.word
val test_bit : Word16.word -> IntInf.int -> bool
end = struct
fun set_bit x n b =
let val mask = Word16.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
in if b then Word16.orb (x, mask)
else Word16.andb (x, Word16.notb mask)
end
fun shiftl x n =
Word16.<< (x, Word.fromLargeInt (IntInf.toLarge n))
fun shiftr x n =
Word16.>> (x, Word.fromLargeInt (IntInf.toLarge n))
fun shiftr_signed x n =
Word16.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
fun test_bit x n =
Word16.andb (x, Word16.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word16.fromInt 0
end; (* struct Uint16 *)›
code_reserved SML_word Uint16
code_printing code_module Uint16 ⇀ (Haskell)
‹module Uint16(Int16, Word16) where
import Data.Int(Int16)
import Data.Word(Word16)›
code_reserved Haskell Uint16
text ‹Scala provides unsigned 16-bit numbers as Char.›
code_printing code_module Uint16 ⇀ (Scala)
‹object Uint16 {
def set_bit(x: scala.Char, n: BigInt, b: Boolean) : scala.Char =
b match {
case true => (x | (1.toChar << n.intValue)).toChar
case false => (x & (1.toChar << n.intValue).unary_~).toChar
}
def shiftl(x: scala.Char, n: BigInt) : scala.Char = (x << n.intValue).toChar
def shiftr(x: scala.Char, n: BigInt) : scala.Char = (x >>> n.intValue).toChar
def shiftr_signed(x: scala.Char, n: BigInt) : scala.Char = (x.toShort >> n.intValue).toChar
def test_bit(x: scala.Char, n: BigInt) : Boolean = (x & (1.toChar << n.intValue)) != 0
} /* object Uint16 */›
code_reserved Scala Uint16
text ‹
Avoid @{term Abs_uint16} in generated code, use @{term Rep_uint16'} instead.
The symbolic implementations for code\_simp use @{term Rep_uint16}.
The new destructor @{term Rep_uint16'} is executable.
As the simplifier is given the [code abstract] equations literally,
we cannot implement @{term Rep_uint16} directly, because that makes code\_simp loop.
If code generation raises Match, some equation probably contains @{term Rep_uint16}
([code abstract] equations for @{typ uint16} may use @{term Rep_uint16} because
these instances will be folded away.)
To convert @{typ "16 word"} values into @{typ uint16}, use @{term "Abs_uint16'"}.
›
definition Rep_uint16' where [simp]: "Rep_uint16' = Rep_uint16"
lemma Rep_uint16'_transfer [transfer_rule]:
"rel_fun cr_uint16 (=) (λx. x) Rep_uint16'"
unfolding Rep_uint16'_def by(rule uint16.rep_transfer)
lemma Rep_uint16'_code [code]: "Rep_uint16' x = (BITS n. bit x n)"
by transfer (simp add: set_bits_bit_eq)
lift_definition Abs_uint16' :: "16 word ⇒ uint16" is "λx :: 16 word. x" .
lemma Abs_uint16'_code [code]:
"Abs_uint16' x = Uint16 (integer_of_int (uint x))"
including integer.lifting by transfer simp
declare [[code drop: "term_of_class.term_of :: uint16 ⇒ _"]]
lemma term_of_uint16_code [code]:
defines "TR ≡ typerep.Typerep" and "bit0 ≡ STR ''Numeral_Type.bit0''" shows
"term_of_class.term_of x =
Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint16.uint16.Abs_uint16'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]], TR (STR ''Uint16.uint16'') []]))
(term_of_class.term_of (Rep_uint16' x))"
by(simp add: term_of_anything)
lemma Uint16_code [code]: "Rep_uint16 (Uint16 i) = word_of_int (int_of_integer_symbolic i)"
unfolding Uint16_def int_of_integer_symbolic_def by(simp add: Abs_uint16_inverse)
code_printing
type_constructor uint16 ⇀
(SML_word) "Word16.word" and
(Haskell) "Uint16.Word16" and
(Scala) "scala.Char"
| constant Uint16 ⇀
(SML_word) "Word16.fromLargeInt (IntInf.toLarge _)" and
(Haskell) "(Prelude.fromInteger _ :: Uint16.Word16)" and
(Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint16.Word16)" and
(Scala) "_.charValue"
| constant "0 :: uint16" ⇀
(SML_word) "(Word16.fromInt 0)" and
(Haskell) "(0 :: Uint16.Word16)" and
(Scala) "0"
| constant "1 :: uint16" ⇀
(SML_word) "(Word16.fromInt 1)" and
(Haskell) "(1 :: Uint16.Word16)" and
(Scala) "1"
| constant "plus :: uint16 ⇒ _ ⇒ _" ⇀
(SML_word) "Word16.+ ((_), (_))" and
(Haskell) infixl 6 "+" and
(Scala) "(_ +/ _).toChar"
| constant "uminus :: uint16 ⇒ _" ⇀
(SML_word) "Word16.~" and
(Haskell) "negate" and
(Scala) "(- _).toChar"
| constant "minus :: uint16 ⇒ _" ⇀
(SML_word) "Word16.- ((_), (_))" and
(Haskell) infixl 6 "-" and
(Scala) "(_ -/ _).toChar"
| constant "times :: uint16 ⇒ _ ⇒ _" ⇀
(SML_word) "Word16.* ((_), (_))" and
(Haskell) infixl 7 "*" and
(Scala) "(_ */ _).toChar"
| constant "HOL.equal :: uint16 ⇒ _ ⇒ bool" ⇀
(SML_word) "!((_ : Word16.word) = _)" and
(Haskell) infix 4 "==" and
(Scala) infixl 5 "=="
| class_instance uint16 :: equal ⇀ (Haskell) -
| constant "less_eq :: uint16 ⇒ _ ⇒ bool" ⇀
(SML_word) "Word16.<= ((_), (_))" and
(Haskell) infix 4 "<=" and
(Scala) infixl 4 "<="
| constant "less :: uint16 ⇒ _ ⇒ bool" ⇀
(SML_word) "Word16.< ((_), (_))" and
(Haskell) infix 4 "<" and
(Scala) infixl 4 "<"
| constant "Bit_Operations.not :: uint16 ⇒ _" ⇀
(SML_word) "Word16.notb" and
(Haskell) "Data'_Bits.complement" and
(Scala) "_.unary'_~.toChar"
| constant "Bit_Operations.and :: uint16 ⇒ _" ⇀
(SML_word) "Word16.andb ((_),/ (_))" and
(Haskell) infixl 7 "Data_Bits..&." and
(Scala) "(_ & _).toChar"
| constant "Bit_Operations.or :: uint16 ⇒ _" ⇀
(SML_word) "Word16.orb ((_),/ (_))" and
(Haskell) infixl 5 "Data_Bits..|." and
(Scala) "(_ | _).toChar"
| constant "Bit_Operations.xor :: uint16 ⇒ _" ⇀
(SML_word) "Word16.xorb ((_),/ (_))" and
(Haskell) "Data'_Bits.xor" and
(Scala) "(_ ^ _).toChar"
definition uint16_div :: "uint16 ⇒ uint16 ⇒ uint16"
where "uint16_div x y = (if y = 0 then undefined ((div) :: uint16 ⇒ _) x (0 :: uint16) else x div y)"
definition uint16_mod :: "uint16 ⇒ uint16 ⇒ uint16"
where "uint16_mod x y = (if y = 0 then undefined ((mod) :: uint16 ⇒ _) x (0 :: uint16) else x mod y)"
context includes undefined_transfer begin
lemma div_uint16_code [code]: "x div y = (if y = 0 then 0 else uint16_div x y)"
unfolding uint16_div_def by transfer (simp add: word_div_def)
lemma mod_uint16_code [code]: "x mod y = (if y = 0 then x else uint16_mod x y)"
unfolding uint16_mod_def by transfer (simp add: word_mod_def)
lemma uint16_div_code [code]:
"Rep_uint16 (uint16_div x y) =
(if y = 0 then Rep_uint16 (undefined ((div) :: uint16 ⇒ _) x (0 :: uint16)) else Rep_uint16 x div Rep_uint16 y)"
unfolding uint16_div_def by transfer simp
lemma uint16_mod_code [code]:
"Rep_uint16 (uint16_mod x y) =
(if y = 0 then Rep_uint16 (undefined ((mod) :: uint16 ⇒ _) x (0 :: uint16)) else Rep_uint16 x mod Rep_uint16 y)"
unfolding uint16_mod_def by transfer simp
end
code_printing constant uint16_div ⇀
(SML_word) "Word16.div ((_), (_))" and
(Haskell) "Prelude.div" and
(Scala) "(_ '/ _).toChar"
| constant uint16_mod ⇀
(SML_word) "Word16.mod ((_), (_))" and
(Haskell) "Prelude.mod" and
(Scala) "(_ % _).toChar"
definition uint16_test_bit :: "uint16 ⇒ integer ⇒ bool"
where [code del]:
"uint16_test_bit x n =
(if n < 0 ∨ 15 < n then undefined (bit :: uint16 ⇒ _) x n
else bit x (nat_of_integer n))"
lemma test_bit_uint16_code [code]:
"bit x n ⟷ n < 16 ∧ uint16_test_bit x (integer_of_nat n)"
including undefined_transfer integer.lifting unfolding uint16_test_bit_def
by (transfer, simp, transfer, simp)
lemma uint16_test_bit_code [code]:
"uint16_test_bit w n =
(if n < 0 ∨ 15 < n then undefined (bit :: uint16 ⇒ _) w n else bit (Rep_uint16 w) (nat_of_integer n))"
unfolding uint16_test_bit_def by (simp add: bit_uint16.rep_eq)
code_printing constant uint16_test_bit ⇀
(SML_word) "Uint16.test'_bit" and
(Haskell) "Data'_Bits.testBitBounded" and
(Scala) "Uint16.test'_bit"
definition uint16_set_bit :: "uint16 ⇒ integer ⇒ bool ⇒ uint16"
where [code del]:
"uint16_set_bit x n b =
(if n < 0 ∨ 15 < n then undefined (set_bit :: uint16 ⇒ _) x n b
else set_bit x (nat_of_integer n) b)"
lemma set_bit_uint16_code [code]:
"set_bit x n b = (if n < 16 then uint16_set_bit x (integer_of_nat n) b else x)"
including undefined_transfer integer.lifting unfolding uint16_set_bit_def
by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)
lemma uint16_set_bit_code [code]:
"Rep_uint16 (uint16_set_bit w n b) =
(if n < 0 ∨ 15 < n then Rep_uint16 (undefined (set_bit :: uint16 ⇒ _) w n b)
else set_bit (Rep_uint16 w) (nat_of_integer n) b)"
including undefined_transfer unfolding uint16_set_bit_def by transfer simp
code_printing constant uint16_set_bit ⇀
(SML_word) "Uint16.set'_bit" and
(Haskell) "Data'_Bits.setBitBounded" and
(Scala) "Uint16.set'_bit"
definition uint16_shiftl :: "uint16 ⇒ integer ⇒ uint16"
where [code del]:
"uint16_shiftl x n = (if n < 0 ∨ 16 ≤ n then undefined (push_bit :: nat ⇒ uint16 ⇒ _) x n else push_bit (nat_of_integer n) x)"
lemma shiftl_uint16_code [code]: "push_bit n x = (if n < 16 then uint16_shiftl x (integer_of_nat n) else 0)"
including undefined_transfer integer.lifting unfolding uint16_shiftl_def
by transfer simp
lemma uint16_shiftl_code [code]:
"Rep_uint16 (uint16_shiftl w n) =
(if n < 0 ∨ 16 ≤ n then Rep_uint16 (undefined (push_bit :: nat ⇒ uint16 ⇒ _) w n)
else push_bit (nat_of_integer n) (Rep_uint16 w))"
including undefined_transfer unfolding uint16_shiftl_def
by transfer simp
code_printing constant uint16_shiftl ⇀
(SML_word) "Uint16.shiftl" and
(Haskell) "Data'_Bits.shiftlBounded" and
(Scala) "Uint16.shiftl"
definition uint16_shiftr :: "uint16 ⇒ integer ⇒ uint16"
where [code del]:
"uint16_shiftr x n = (if n < 0 ∨ 16 ≤ n then undefined (drop_bit :: nat ⇒ uint16 ⇒ _) x n else drop_bit (nat_of_integer n) x)"
lemma shiftr_uint16_code [code]: "drop_bit n x = (if n < 16 then uint16_shiftr x (integer_of_nat n) else 0)"
including undefined_transfer integer.lifting unfolding uint16_shiftr_def
by transfer simp
lemma uint16_shiftr_code [code]:
"Rep_uint16 (uint16_shiftr w n) =
(if n < 0 ∨ 16 ≤ n then Rep_uint16 (undefined (drop_bit :: nat ⇒ uint16 ⇒ _) w n)
else drop_bit (nat_of_integer n) (Rep_uint16 w))"
including undefined_transfer unfolding uint16_shiftr_def by transfer simp
code_printing constant uint16_shiftr ⇀
(SML_word) "Uint16.shiftr" and
(Haskell) "Data'_Bits.shiftrBounded" and
(Scala) "Uint16.shiftr"
definition uint16_sshiftr :: "uint16 ⇒ integer ⇒ uint16"
where [code del]:
"uint16_sshiftr x n =
(if n < 0 ∨ 16 ≤ n then undefined signed_drop_bit_uint16 n x else signed_drop_bit_uint16 (nat_of_integer n) x)"
lemma sshiftr_uint16_code [code]:
"signed_drop_bit_uint16 n x =
(if n < 16 then uint16_sshiftr x (integer_of_nat n) else if bit x 15 then -1 else 0)"
including undefined_transfer integer.lifting unfolding uint16_sshiftr_def
by transfer (simp add: not_less signed_drop_bit_beyond word_size)
lemma uint16_sshiftr_code [code]:
"Rep_uint16 (uint16_sshiftr w n) =
(if n < 0 ∨ 16 ≤ n then Rep_uint16 (undefined signed_drop_bit_uint16 n w)
else signed_drop_bit (nat_of_integer n) (Rep_uint16 w))"
including undefined_transfer unfolding uint16_sshiftr_def
by transfer simp
code_printing constant uint16_sshiftr ⇀
(SML_word) "Uint16.shiftr'_signed" and
(Haskell)
"(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint16.Int16) _)) :: Uint16.Word16)" and
(Scala) "Uint16.shiftr'_signed"
lemma uint16_msb_test_bit: "msb x ⟷ bit (x :: uint16) 15"
by transfer (simp add: msb_word_iff_bit)
lemma msb_uint16_code [code]: "msb x ⟷ uint16_test_bit x 15"
by (simp add: uint16_test_bit_def uint16_msb_test_bit)
lemma uint16_of_int_code [code]: "uint16_of_int i = Uint16 (integer_of_int i)"
including integer.lifting by transfer simp
lemma int_of_uint16_code [code]:
"int_of_uint16 x = int_of_integer (integer_of_uint16 x)"
by (simp add: int_of_uint16.rep_eq integer_of_uint16_def)
lemma uint16_of_nat_code [code]:
"uint16_of_nat = uint16_of_int ∘ int"
by transfer (simp add: fun_eq_iff)
lemma nat_of_uint16_code [code]:
"nat_of_uint16 x = nat_of_integer (integer_of_uint16 x)"
unfolding integer_of_uint16_def including integer.lifting by transfer simp
lemma integer_of_uint16_code [code]:
"integer_of_uint16 n = integer_of_int (uint (Rep_uint16' n))"
unfolding integer_of_uint16_def by transfer auto
code_printing
constant "integer_of_uint16" ⇀
(SML_word) "Word16.toInt _ : IntInf.int" and
(Haskell) "Prelude.toInteger" and
(Scala) "BigInt"
section ‹Quickcheck setup›
definition uint16_of_natural :: "natural ⇒ uint16"
where "uint16_of_natural x ≡ Uint16 (integer_of_natural x)"
instantiation uint16 :: "{random, exhaustive, full_exhaustive}" begin
definition "random_uint16 ≡ qc_random_cnv uint16_of_natural"
definition "exhaustive_uint16 ≡ qc_exhaustive_cnv uint16_of_natural"
definition "full_exhaustive_uint16 ≡ qc_full_exhaustive_cnv uint16_of_natural"
instance ..
end
instantiation uint16 :: narrowing begin
interpretation quickcheck_narrowing_samples
"λi. let x = Uint16 i in (x, 0xFFFF - x)" "0"
"Typerep.Typerep (STR ''Uint16.uint16'') []" .
definition "narrowing_uint16 d = qc_narrowing_drawn_from (narrowing_samples d) d"
declare [[code drop: "partial_term_of :: uint16 itself ⇒ _"]]
lemmas partial_term_of_uint16 [code] = partial_term_of_code
instance ..
end
end