PDF cleanup 282: hide use of open for records in pdf
#364
Conversation
Only in `.lagda` files.
There was a problem hiding this comment.
open can't just be hidden from view, since it carries a lot of meaning. For example, in EPOCH it does some of the actual work. Rather, we should use techniques that avoid using open in the code, like for example pattern-matching on a state/environment when defining rules, instead of binding it to a single name and then writing open State s. Another option would be to use some kind of deep accessors to avoid nested opens and then applying those deep accessors to our variables. What's right needs to be decided on a case-by-case basis.
instead try using accessors; not as pretty, but avoids exposing some `open` declarations
|
Okay, I tried being less aggressive about hiding open statements, especially when applied to a private variable. I'm now hiding some open statements without naming the private variable, using accessors to make it more clear what's happening. |
...still more to fix... maybe have to revert
by reverting
williamdemeo
force-pushed
the
william/282-remove-open-for-records
branch
from
12c3635 to
751187e
Compare
| -- ^ this rolls over the future enact state into es | ||
| open LState ls; open UTxOState utxoSt; open CertState certState | ||
| open PState pState; open DState dState; open GState gState | ||
| open Acnt acnt | ||
|
|
There was a problem hiding this comment.
Removed a couple of instances of open for records here, at the expense of using accessors below.
| @@ -110,13 +111,13 @@ data _⊢_⇀⦇_,GOV'⦈_ where | |||
| (Γ , k) ⊢ s ⇀⦇ sig ,GOV'⦈ addVote s aid voter v | |||
|
|
|||
| GOV-Propose : ∀ {x} → let | |||
| open GovEnv Γ; open PParams pparams hiding (a) | |||
| open GovEnv Γ | |||
There was a problem hiding this comment.
Remove one instance of open for record pparams at the expense of having to write pparams a couple of times below.
| @@ -44,6 +44,8 @@ record LState : Set where | |||
|
|
|||
| txgov : TxBody → List (GovVote ⊎ GovProposal) | |||
| txgov txb = map inj₁ txvote ++ map inj₂ txprop | |||
| \end{code} | |||
| \begin{code}[hide] | |||
| where open TxBody txb | |||
There was a problem hiding this comment.
It doesn't seem necessary to show this open directive in the figure.
| open RwdAddr | ||
| open DState | ||
| open CertState | ||
| open CertState; open DState; open LEnv; open LState; open RwdAddr; open TxBody |
There was a problem hiding this comment.
Remove five instances of open for records from the figure at the expense of lots explicit use of accessors in the LEDGER transition rule below. Is it worth it? Is there a better way to avoid the open directives here?
| ⦃ DecEq-PolicyId : DecEq PolicyId ⦄ | ||
| ⦃ DecEq-AssetName : DecEq AssetName ⦄ | ||
| ⦃ DecEq-Tot : DecEq (AssetId ⇒ ℕ) ⦄ |
There was a problem hiding this comment.
Do these really need to appear in the figure?
Description
Hide use of
openfor records in pdf. This addresses one item of issue #282.Checklist