Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[ lint ] make auto implicits stand out #3

Merged
merged 1 commit into from
Mar 30, 2023
Merged

[ lint ] make auto implicits stand out #3

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 17 additions & 14 deletions src/Text/Crypt.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -188,10 +188,11 @@ refineHash = refineSalt
||| Implementation note: This fails on rare occasions for as of yet
||| unknown reasons. Rerunning seems to fix it, though.
export
gensalt : (cm : CryptMethod)
-> (cost : Bits32)
-> (0 prf : InRange cm cost)
=> IO String
gensalt :
(cm : CryptMethod)
-> (cost : Bits32)
-> {auto 0 prf : InRange cm cost}
-> IO String
gensalt cm cost = fromPrim (go 100)
where go : Nat -> PrimIO String
go Z w = prim__gensalt (cryptPrefix cm) cost w
Expand All @@ -213,11 +214,12 @@ cryptWithSalt (Element s _) (Element p _) = prim__crypt s p
||| cost. This will first generate a new random salt, therefore,
||| this runs in `IO`.
export
crypt : (cm : CryptMethod)
-> (cost : Bits32)
-> (phrase : Passphrase)
-> (0 p1 : InRange cm cost)
=> IO String
crypt :
(cm : CryptMethod)
-> (cost : Bits32)
-> (phrase : Passphrase)
-> {auto 0 p1 : InRange cm cost}
-> IO String
crypt cm cost (Element p _) = do
salt <- gensalt cm cost
pure $ prim__crypt salt p
Expand All @@ -228,11 +230,12 @@ crypt cm cost (Element p _) = do
||| fails to generate a valid salt (which is a highly unlikely thing
||| to happen).
export
cryptMaybe : (cm : CryptMethod)
-> (cost : Bits32)
-> (phrase : String)
-> (0 p1 : InRange cm cost)
=> IO (Maybe Hash)
cryptMaybe :
(cm : CryptMethod)
-> (cost : Bits32)
-> (phrase : String)
-> {auto 0 p1 : InRange cm cost}
-> IO (Maybe Hash)
cryptMaybe cm cost phrase = do
Just pp <- pure (refinePassphrase phrase) | Nothing => pure Nothing
hash <- crypt cm cost pp
Expand Down