src/Pure/General/sha1_polyml.ML
author wenzelm
Thu Mar 11 16:56:22 2010 +0100 (2010-03-11 ago)
changeset 35713 428284ee1465
parent 35628 f1456d045151
child 35935 32887cbfd62d
permissions -rw-r--r--
absolute lib_path relative to ML_HOME -- for improved robustness;
explicit warning if shared library failed to load;
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@35713
    18
val lib_path =
wenzelm@35713
    19
  ("$ML_HOME/" ^ (if String.isSuffix "cygwin" ml_system then "sha1.dll" else "libsha1.so"))
wenzelm@35713
    20
  |> Path.explode;
wenzelm@35713
    21
wenzelm@35628
    22
fun digest_external str =
wenzelm@35628
    23
  let
wenzelm@35628
    24
    val digest = CInterface.alloc 20 CInterface.Cchar;
wenzelm@35713
    25
    val _ =
wenzelm@35713
    26
      CInterface.call3 (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer")
wenzelm@35713
    27
        (CInterface.STRING, CInterface.INT, CInterface.POINTER)
wenzelm@35713
    28
        CInterface.POINTER (str, size str, CInterface.address digest);
wenzelm@35628
    29
  in fold (suffix o hex_string digest) (0 upto 19) "" end;
wenzelm@35628
    30
wenzelm@35628
    31
fun digest str = digest_external str
wenzelm@35713
    32
  handle CInterface.Foreign msg =>
wenzelm@35713
    33
    (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.digest str);
wenzelm@35628
    34
wenzelm@35628
    35
end;