author | wenzelm |
Fri, 17 Dec 2010 20:21:35 +0100 | |
changeset 41253 | 42f24340ae53 |
parent 35937 | d7b3190d8b4a |
child 41954 | fb94df4505a0 |
permissions | -rw-r--r-- |
35628 | 1 |
(* Title: Pure/General/sha1_polyml.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
4 |
Digesting strings according to SHA-1 (see RFC 3174) -- based on an |
|
5 |
external implementation in C with a fallback to an internal |
|
6 |
implementation. |
|
7 |
*) |
|
8 |
||
9 |
structure SHA1: SHA1 = |
|
10 |
struct |
|
11 |
||
12 |
fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10); |
|
13 |
||
14 |
fun hex_string arr i = |
|
15 |
let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr) |
|
16 |
in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end |
|
17 |
||
35713
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
18 |
val lib_path = |
35937
d7b3190d8b4a
use ml_platform instead of ml_system to distinguish library names
boehmes
parents:
35935
diff
changeset
|
19 |
("$ML_HOME/" ^ (if String.isSuffix "cygwin" ml_platform then "sha1.dll" else "libsha1.so")) |
35713
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
20 |
|> Path.explode; |
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
21 |
|
35628 | 22 |
fun digest_external str = |
23 |
let |
|
24 |
val digest = CInterface.alloc 20 CInterface.Cchar; |
|
35713
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
25 |
val _ = |
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
26 |
CInterface.call3 (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer") |
35935
32887cbfd62d
use LONG rather than INT to represent the C datatype size_t
boehmes
parents:
35713
diff
changeset
|
27 |
(CInterface.STRING, CInterface.LONG, CInterface.POINTER) |
35713
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
28 |
CInterface.POINTER (str, size str, CInterface.address digest); |
35628 | 29 |
in fold (suffix o hex_string digest) (0 upto 19) "" end; |
30 |
||
31 |
fun digest str = digest_external str |
|
35713
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
32 |
handle CInterface.Foreign msg => |
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
33 |
(warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.digest str); |
35628 | 34 |
|
35 |
end; |