src/Pure/General/sha1_polyml.ML
author wenzelm
Sat Jul 23 17:22:28 2011 +0200 (2011-07-23 ago)
changeset 43948 8f5add916a99
parent 41954 fb94df4505a0
child 53211 753b9fbe18be
permissions -rw-r--r--
explicit structure ML_System;
tunned ML bootstrap;
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@41954
    12
(* digesting *)
wenzelm@41954
    13
wenzelm@35628
    14
fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10);
wenzelm@35628
    15
wenzelm@35628
    16
fun hex_string arr i =
wenzelm@35628
    17
  let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)
wenzelm@35628
    18
  in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end
wenzelm@35628
    19
wenzelm@35713
    20
val lib_path =
wenzelm@43948
    21
  ("$ML_HOME/" ^ (if ML_System.platform_is_cygwin then "sha1.dll" else "libsha1.so"))
wenzelm@35713
    22
  |> Path.explode;
wenzelm@35713
    23
wenzelm@35628
    24
fun digest_external str =
wenzelm@35628
    25
  let
wenzelm@35628
    26
    val digest = CInterface.alloc 20 CInterface.Cchar;
wenzelm@35713
    27
    val _ =
wenzelm@35713
    28
      CInterface.call3 (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer")
boehmes@35935
    29
        (CInterface.STRING, CInterface.LONG, CInterface.POINTER)
wenzelm@35713
    30
        CInterface.POINTER (str, size str, CInterface.address digest);
wenzelm@35628
    31
  in fold (suffix o hex_string digest) (0 upto 19) "" end;
wenzelm@35628
    32
wenzelm@41954
    33
fun digest_string str = digest_external str
wenzelm@35713
    34
  handle CInterface.Foreign msg =>
wenzelm@41954
    35
    (warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.rep (SHA1.digest str));
wenzelm@41954
    36
wenzelm@41954
    37
wenzelm@41954
    38
(* type digest *)
wenzelm@41954
    39
wenzelm@41954
    40
datatype digest = Digest of string;
wenzelm@41954
    41
wenzelm@41954
    42
val digest = Digest o digest_string;
wenzelm@41954
    43
fun rep (Digest s) = s;
wenzelm@35628
    44
wenzelm@35628
    45
end;