Quelle Hex_Words.thy

Sprache: Isabelle

(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)

section "Print Words in Hex"

theory Hex_Words
imports
"HOL-Library.Word"
begin

text ‹Print words in hex.›

(* mostly clagged from Num.thy *)
typed_print_translation ‹

fun dest_num (Const (@{const_syntax Num.Bit0}, _) $ n) = 2 * dest_num n
| dest_num (Const (@{const_syntax Num.Bit1}, _) $ n) = 2 * dest_num n + 1
| dest_num (Const (@{const_syntax Num.One}, _)) = 1;

fun dest_bin_hex_str tm =
let
val num = dest_num tm;
val pre = if num < 10 then "" else "0x"
in
pre ^ (Int.fmt StringCvt.HEX num)
end;

fun num_tr' sign ctxt T [n] =
let
val k = dest_bin_hex_str n;
val t' = Syntax.const @{syntax_const "_Numeral"} $
Syntax.free (sign ^ k);
in
case T of
Type (@{type_name fun}, [_, T' as Type("Word.word",_)]) =>
if not (Config.get ctxt show_types) andalso can Term.dest_Type T'
then t'
else Syntax.const @{syntax_const "_constrain"} $ t' $
Syntax_Phases.term_of_typ ctxt T'
| T' => if T' = dummyT then t' else raise Match
end;
[(@{const_syntax numeral}, num_tr' "")] end
›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.1 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.