From 392582885500d8201bbe502943ca4b02c5c77ac0 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Wed, 8 Sep 2021 03:08:13 -0400 Subject: Normalized the syntax of "abstract:" and "actor:". --- stdlib/source/program/aedifex/hash.lux | 258 ++++++++++++++++----------------- 1 file changed, 128 insertions(+), 130 deletions(-) (limited to 'stdlib/source/program/aedifex/hash.lux') diff --git a/stdlib/source/program/aedifex/hash.lux b/stdlib/source/program/aedifex/hash.lux index eb00c2af5..996858e3e 100644 --- a/stdlib/source/program/aedifex/hash.lux +++ b/stdlib/source/program/aedifex/hash.lux @@ -31,138 +31,136 @@ ("static" getInstance [java/lang/String] java/security/MessageDigest) (digest [[byte]] [byte])]) -(abstract: .public SHA-1 {} Any) -(abstract: .public MD5 {} Any) +(abstract: .public SHA-1 Any []) +(abstract: .public MD5 Any []) (abstract: .public (Hash h) - {} - Binary - (def: .public data - (All (_ h) (-> (Hash h) Binary)) - (|>> :representation)) - - (template [ ] - [(def: .public ( value) - (-> Binary (Hash )) - (|> (java/security/MessageDigest::getInstance []) - (java/security/MessageDigest::digest [value]) - :abstraction))] - - [sha-1 ..SHA-1 "SHA-1"] - [md5 ..MD5 "MD5"] - ) - - (def: encoded - (Format Binary) - (binary.aggregate (function (_ byte representation) - (let [hex (\ n.hex encoded byte) - hex (case (text.size hex) - 1 (format "0" hex) - _ hex)] - (format representation hex))) - "")) - - (template [ ] - [(def: - Nat - )] - - [20 sha-1::size] - [16 md5::size] - ) - - (def: hex_per_byte - 2) - - (def: hex_per_chunk - (n.* hex_per_byte i64.bytes_per_i64)) - - (exception: .public (not_a_hash {size Nat} {value Text}) - (exception.report - ["Pseudo hash" (%.text value)] - ["Expected size" (%.nat size)] - ["Actual size" (%.nat (text.size value))])) - - (template [ ] - [(exception: .public ( {data Binary}) - (exception.report - ["Pseudo hash" (%.text (..encoded data))] - ["Expected size" (%.nat )] - ["Actual size" (%.nat (binary.size data))]))] - - [not_a_sha-1 ..sha-1::size] - [not_a_md5 ..md5::size] - ) - - (template [ ] - [(def: .public ( data) - (-> Binary (Try (Hash ))) - (if (n.= (binary.size data)) - (#try.Success (:abstraction data)) - (exception.except [data])))] - - [as_sha-1 SHA-1 ..sha-1::size ..not_a_sha-1] - [as_md5 MD5 ..md5::size ..not_a_md5] - ) - - (def: hash_size - (-> Text Nat) - (|>> text.size (n./ ..hex_per_byte))) - - (def: encoding_size - (-> Nat Nat) - (n.* ..hex_per_byte)) - - (def: (decoded size constructor encoded) - (All (_ h) - (-> Nat (-> Binary (Try (Hash h))) - (-> Text (Try (Hash h))))) - (let [hash_size (..hash_size encoded)] - (if (n.= size hash_size) - (loop [input encoded - chunk 0 - output (binary.empty hash_size)] - (let [index (n.* chunk i64.bytes_per_i64)] - (case (text.split_at ..hex_per_chunk input) - (#.Some [head tail]) - (do try.monad - [head (\ n.hex decoded head) - output (binary.write/64! index head output)] - (recur tail (++ chunk) output)) - - #.None - (case (..hash_size input) - 0 (constructor output) - (^template [ ] - [ - (do try.monad - [head (\ n.hex decoded input) - output ( index head output)] - (constructor output))]) - ([1 binary.write/8!] - [2 binary.write/16!] - [4 binary.write/32!]) - _ (exception.except ..not_a_hash [(..encoding_size size) encoded]))))) - (exception.except ..not_a_hash [(..encoding_size size) encoded])))) - - (template [ ] - [(implementation: .public - (Codec Text (Hash )) - - (def: encoded (|>> :representation ..encoded)) - (def: decoded (..decoded )))] - - [sha-1_codec SHA-1 ..sha-1::size ..as_sha-1] - [md5_codec MD5 ..md5::size ..as_md5] - ) - - (implementation: .public equivalence - (All (_ h) (Equivalence (Hash h))) - - (def: (= reference subject) - (\ binary.equivalence = - (:representation reference) - (:representation subject)))) + [(def: .public data + (All (_ h) (-> (Hash h) Binary)) + (|>> :representation)) + + (template [ ] + [(def: .public ( value) + (-> Binary (Hash )) + (|> (java/security/MessageDigest::getInstance []) + (java/security/MessageDigest::digest [value]) + :abstraction))] + + [sha-1 ..SHA-1 "SHA-1"] + [md5 ..MD5 "MD5"] + ) + + (def: encoded + (Format Binary) + (binary.aggregate (function (_ byte representation) + (let [hex (\ n.hex encoded byte) + hex (case (text.size hex) + 1 (format "0" hex) + _ hex)] + (format representation hex))) + "")) + + (template [ ] + [(def: + Nat + )] + + [20 sha-1::size] + [16 md5::size] + ) + + (def: hex_per_byte + 2) + + (def: hex_per_chunk + (n.* hex_per_byte i64.bytes_per_i64)) + + (exception: .public (not_a_hash {size Nat} {value Text}) + (exception.report + ["Pseudo hash" (%.text value)] + ["Expected size" (%.nat size)] + ["Actual size" (%.nat (text.size value))])) + + (template [ ] + [(exception: .public ( {data Binary}) + (exception.report + ["Pseudo hash" (%.text (..encoded data))] + ["Expected size" (%.nat )] + ["Actual size" (%.nat (binary.size data))]))] + + [not_a_sha-1 ..sha-1::size] + [not_a_md5 ..md5::size] + ) + + (template [ ] + [(def: .public ( data) + (-> Binary (Try (Hash ))) + (if (n.= (binary.size data)) + (#try.Success (:abstraction data)) + (exception.except [data])))] + + [as_sha-1 SHA-1 ..sha-1::size ..not_a_sha-1] + [as_md5 MD5 ..md5::size ..not_a_md5] + ) + + (def: hash_size + (-> Text Nat) + (|>> text.size (n./ ..hex_per_byte))) + + (def: encoding_size + (-> Nat Nat) + (n.* ..hex_per_byte)) + + (def: (decoded size constructor encoded) + (All (_ h) + (-> Nat (-> Binary (Try (Hash h))) + (-> Text (Try (Hash h))))) + (let [hash_size (..hash_size encoded)] + (if (n.= size hash_size) + (loop [input encoded + chunk 0 + output (binary.empty hash_size)] + (let [index (n.* chunk i64.bytes_per_i64)] + (case (text.split_at ..hex_per_chunk input) + (#.Some [head tail]) + (do try.monad + [head (\ n.hex decoded head) + output (binary.write/64! index head output)] + (recur tail (++ chunk) output)) + + #.None + (case (..hash_size input) + 0 (constructor output) + (^template [ ] + [ + (do try.monad + [head (\ n.hex decoded input) + output ( index head output)] + (constructor output))]) + ([1 binary.write/8!] + [2 binary.write/16!] + [4 binary.write/32!]) + _ (exception.except ..not_a_hash [(..encoding_size size) encoded]))))) + (exception.except ..not_a_hash [(..encoding_size size) encoded])))) + + (template [ ] + [(implementation: .public + (Codec Text (Hash )) + + (def: encoded (|>> :representation ..encoded)) + (def: decoded (..decoded )))] + + [sha-1_codec SHA-1 ..sha-1::size ..as_sha-1] + [md5_codec MD5 ..md5::size ..as_md5] + ) + + (implementation: .public equivalence + (All (_ h) (Equivalence (Hash h))) + + (def: (= reference subject) + (\ binary.equivalence = + (:representation reference) + (:representation subject))))] ) -- cgit v1.2.3