-
Notifications
You must be signed in to change notification settings - Fork 15
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.
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
Eliminate Boolean properties #649
Conversation
cf59b69
to
f730932
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
feesOK
looks great! The other two still need a bit of work.
src/Ledger/Utxo.lagda
Outdated
(filterˢ (λ (a , _ ) → isTwoPhaseScriptAddress tx utxo a ≡ true) | ||
(range (utxo ∣ txins))) | ||
(filterˢ (λ (a , _ ) → isTwoPhaseScriptAddress tx utxo a) | ||
⦃ λ {(a , _)} → isTwoPhaseScriptAddress? {tx} {utxo} {a} ⦄ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here we have an interesting problem: this code belongs to the visible section of the PDF and we shouldn't show stuff like that because we'd have to explain what it means (and the meaning isn't particularly interesting). However, marking isTwoPhaseScriptAddress?
as an instance isn't a good idea and wouldn't even work anyway.
I think the only reasonable solution here is to turn isTwoPhaseScriptAddress
into a data
type and then provide a ⁇
instance for that type. As I see it, there are two options to do that:
- either completely replace the function with a type whose constructors contain the same logic, or
- provide a 'newtype' wrapper around
isTwoPhaseScriptAddress
, i.e. something of this form:data isTwoPhaseScriptAddress' : Tx → UTxO → Addr → Type where wrap : ∀ {tx utxo a} → isTwoPhaseScriptAddress tx utxo a → isTwoPhaseScriptAddress' tx utxo a
The second option has the upside that we can cheat a little and just hide this wrapper behind the curtain when rendering the PDF. We currently don't have the machinery to do that perfectly because we'd have to substitute isTwoPhaseScriptAddress'
with isTwoPhaseScriptAddress
in the line above when rendering the PDF, but we probably need a mechanism for that anyway. So I'm currently leaning more towards that option.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How would we go about substituting isTwoPhaseScriptAddress'
by its unprimed version in the pdf?
@carlostome I'd like to merge this, the only thing that's still open is the choice of |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks! I've renamed isAdaOnlyᵇ
to isAdaOnly
because the ᵇ
was just to indicate that it's a boolean. I've also removed a ˢ
that wasn't necessary anymore.
I don't want to investigate that right now, can be done some other time.
Whoa, apparently removing the |
Description
Addresses #342.
Original:
actionWellFormed
isP2Script
isAdaOnlyᵇ
feesOK
Other:
isTwoPhaseScriptAddress
Left:
isValid
Checklist
CHANGELOG.md