author | blanchet |
Wed, 18 Sep 2013 16:44:19 +0200 | |
changeset 53697 | 221ec353bcc5 |
parent 53211 | 753b9fbe18be |
child 57638 | ed58e740a699 |
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 = |
43948 | 21 |
("$ML_HOME/" ^ (if ML_System.platform_is_cygwin 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 |
|
53211
753b9fbe18be
allow NUL characters in ML string passed to C library;
wenzelm
parents:
43948
diff
changeset
|
24 |
val STRING_INPUT_BYTES = |
753b9fbe18be
allow NUL characters in ML string passed to C library;
wenzelm
parents:
43948
diff
changeset
|
25 |
CInterface.mkConversion undefined (CInterface.toCbytes o Byte.stringToBytes) |
753b9fbe18be
allow NUL characters in ML string passed to C library;
wenzelm
parents:
43948
diff
changeset
|
26 |
(CInterface.Cpointer CInterface.Cchar); |
753b9fbe18be
allow NUL characters in ML string passed to C library;
wenzelm
parents:
43948
diff
changeset
|
27 |
|
35628 | 28 |
fun digest_external str = |
29 |
let |
|
30 |
val digest = CInterface.alloc 20 CInterface.Cchar; |
|
35713
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
31 |
val _ = |
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
32 |
CInterface.call3 (CInterface.get_sym (File.platform_path lib_path) "sha1_buffer") |
53211
753b9fbe18be
allow NUL characters in ML string passed to C library;
wenzelm
parents:
43948
diff
changeset
|
33 |
(STRING_INPUT_BYTES, CInterface.LONG, CInterface.POINTER) |
35713
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
34 |
CInterface.POINTER (str, size str, CInterface.address digest); |
35628 | 35 |
in fold (suffix o hex_string digest) (0 upto 19) "" end; |
36 |
||
41954 | 37 |
fun digest_string str = digest_external str |
35713
428284ee1465
absolute lib_path relative to ML_HOME -- for improved robustness;
wenzelm
parents:
35628
diff
changeset
|
38 |
handle CInterface.Foreign msg => |
41954 | 39 |
(warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); SHA1.rep (SHA1.digest str)); |
40 |
||
41 |
||
42 |
(* type digest *) |
|
43 |
||
44 |
datatype digest = Digest of string; |
|
45 |
||
46 |
val digest = Digest o digest_string; |
|
47 |
fun rep (Digest s) = s; |
|
35628 | 48 |
|
49 |
end; |