hexadecimal representation of byte string;
authorwenzelm
Sat May 05 21:44:18 2018 +0200 (18 months ago ago)
changeset 68089dac267cd51fe
parent 68088 9e1c670301b8
child 68090 0763d4eb3ebc
hexadecimal representation of byte string;
src/Pure/General/bytes.scala
src/Pure/General/sha1.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/General/bytes.scala	Sat May 05 13:56:51 2018 +0200
     1.2 +++ b/src/Pure/General/bytes.scala	Sat May 05 21:44:18 2018 +0200
     1.3 @@ -39,6 +39,23 @@
     1.4      }
     1.5  
     1.6  
     1.7 +  def hex(s: String): Bytes =
     1.8 +  {
     1.9 +    def err(): Nothing = error("Malformed hexadecimal representation of bytes\n" + s)
    1.10 +    val len = s.length
    1.11 +    if (len % 2 != 0) err()
    1.12 +
    1.13 +    val n = len / 2
    1.14 +    val a = new Array[Byte](n)
    1.15 +    for (i <- 0 until n) {
    1.16 +      val j = 2 * i
    1.17 +      try { a(i) = Integer.parseInt(s.substring(j, j + 2), 16).toByte }
    1.18 +      catch { case _: NumberFormatException => err() }
    1.19 +    }
    1.20 +    new Bytes(a, 0, n)
    1.21 +  }
    1.22 +
    1.23 +
    1.24    /* read */
    1.25  
    1.26    def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes =
     2.1 --- a/src/Pure/General/sha1.ML	Sat May 05 13:56:51 2018 +0200
     2.2 +++ b/src/Pure/General/sha1.ML	Sat May 05 21:44:18 2018 +0200
     2.3 @@ -159,7 +159,6 @@
     2.4  
     2.5  (* digesting *)
     2.6  
     2.7 -fun hex_digit i = if i < 10 then chr (Char.ord #"0" + i) else chr (Char.ord #"a" + i - 10);
     2.8  fun hex_string byte = op ^ (apply2 hex_digit (Integer.div_mod (Word8.toInt byte) 16));
     2.9  
    2.10  in
     3.1 --- a/src/Pure/library.ML	Sat May 05 13:56:51 2018 +0200
     3.2 +++ b/src/Pure/library.ML	Sat May 05 21:44:18 2018 +0200
     3.3 @@ -116,6 +116,7 @@
     3.4    (*integers*)
     3.5    val upto: int * int -> int list
     3.6    val downto: int * int -> int list
     3.7 +  val hex_digit: int -> string
     3.8    val radixpand: int * int -> int list
     3.9    val radixstring: int * string * int -> string
    3.10    val string_of_int: int -> string
    3.11 @@ -154,6 +155,7 @@
    3.12    val translate_string: (string -> string) -> string -> string
    3.13    val encode_lines: string -> string
    3.14    val decode_lines: string -> string
    3.15 +  val hex_string: string -> string
    3.16    val align_right: string -> int -> string -> string
    3.17    val match_string: string -> string -> bool
    3.18  
    3.19 @@ -613,6 +615,10 @@
    3.20  
    3.21  (* convert integers to strings *)
    3.22  
    3.23 +(*hexadecimal*)
    3.24 +fun hex_digit i =
    3.25 +  if i < 10 then chr (Char.ord #"0" + i) else chr (Char.ord #"a" + i - 10);
    3.26 +
    3.27  (*expand the number in the given base;
    3.28    example: radixpand (2, 8) gives [1, 0, 0, 0]*)
    3.29  fun radixpand (base, num) : int list =
    3.30 @@ -771,6 +777,12 @@
    3.31  val encode_lines = translate_string (fn "\n" => "\v" | c => c);
    3.32  val decode_lines = translate_string (fn "\v" => "\n" | c => c);
    3.33  
    3.34 +fun hex_string s =
    3.35 +  fold_string (fn c =>
    3.36 +    let val (a, b) = IntInf.divMod (ord c, 16)
    3.37 +    in cons (hex_digit a) #> cons (hex_digit b) end) s []
    3.38 +  |> rev |> implode;
    3.39 +
    3.40  fun align_right c k s =
    3.41    let
    3.42      val _ = if size c <> 1 orelse size s > k