src/Pure/General/sha1_polyml.ML
author wenzelm
Sun Mar 07 15:51:29 2010 +0100 (2010-03-07 ago)
changeset 35628 f1456d045151
child 35713 428284ee1465
permissions -rw-r--r--
Digesting strings according to SHA-1.
wenzelm@35628
     1
(*  Title:      Pure/General/sha1_polyml.ML
wenzelm@35628
     2
    Author:     Sascha Boehme, TU Muenchen
wenzelm@35628
     3
wenzelm@35628
     4
Digesting strings according to SHA-1 (see RFC 3174) -- based on an
wenzelm@35628
     5
external implementation in C with a fallback to an internal
wenzelm@35628
     6
implementation.
wenzelm@35628
     7
*)
wenzelm@35628
     8
wenzelm@35628
     9
structure SHA1: SHA1 =
wenzelm@35628
    10
struct
wenzelm@35628
    11
wenzelm@35628
    12
fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10);
wenzelm@35628
    13
wenzelm@35628
    14
fun hex_string arr i =
wenzelm@35628
    15
  let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)
wenzelm@35628
    16
  in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end
wenzelm@35628
    17
wenzelm@35628
    18
fun digest_external str =
wenzelm@35628
    19
  let
wenzelm@35628
    20
    val digest = CInterface.alloc 20 CInterface.Cchar;
wenzelm@35628
    21
    val _ = CInterface.call3 (CInterface.get_sym "sha1" "sha1_buffer")
wenzelm@35628
    22
      (CInterface.STRING, CInterface.INT, CInterface.POINTER)
wenzelm@35628
    23
      CInterface.POINTER (str, size str, CInterface.address digest);
wenzelm@35628
    24
  in fold (suffix o hex_string digest) (0 upto 19) "" end;
wenzelm@35628
    25
wenzelm@35628
    26
fun digest str = digest_external str
wenzelm@35628
    27
  handle CInterface.Foreign _ => SHA1.digest str;
wenzelm@35628
    28
wenzelm@35628
    29
end;