author | wenzelm |
Sun, 13 Mar 2011 20:21:24 +0100 | |
changeset 41954 | fb94df4505a0 |
parent 35937 | d7b3190d8b4a |
child 43948 | 8f5add916a99 |
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 |
||
41954 | 12 |
(* digesting *) |
13 |
||
35628 | 14 |
fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10); |
15 |
||
16 |
fun hex_string arr i = |
|
17 |
let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr) |
|
18 |
in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end |
|
19 |
||
35713
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
20 |
val lib_path = |
35937
d7b3190d8b4a
use ml_platform instead of ml_system to distinguish library names
boehmes
parents:
35935
diff
changeset
|
21 |
("$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
|
22 |
|> Path.explode; |
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
23 |
|
35628 | 24 |
fun digest_external str = |
25 |
let |
|
26 |
val digest = CInterface.alloc 20 CInterface.Cchar; |
|
35713
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
27 |
val _ = |
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
28 |
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
|
29 |
(CInterface.STRING, CInterface.LONG, CInterface.POINTER) |
35713
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
30 |
CInterface.POINTER (str, size str, CInterface.address digest); |
35628 | 31 |
in fold (suffix o hex_string digest) (0 upto 19) "" end; |
32 |
||
41954 | 33 |
fun digest_string str = digest_external str |
35713
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
34 |
handle CInterface.Foreign msg => |
41954 | 35 |
(warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.rep (SHA1.digest str)); |
36 |
||
37 |
||
38 |
(* type digest *) |
|
39 |
||
40 |
datatype digest = Digest of string; |
|
41 |
||
42 |
val digest = Digest o digest_string; |
|
43 |
fun rep (Digest s) = s; |
|
35628 | 44 |
|
45 |
end; |