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

Jump to bottom

PDF cleanup 282: hide module syntax #370

Merged
merged 2 commits into from
Feb 16, 2024
Merged

PDF cleanup 282: hide module syntax #370

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
bcc8a5c
PDF cleanup 282: hide `module` syntax
williamdemeo Feb 15, 2024
d60c842
mod suggested in PR review
williamdemeo Feb 16, 2024
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
14 changes: 12 additions & 2 deletions src/Ledger/Script.lagda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,9 +81,19 @@ open import Data.List.Relation.Binary.Sublist.Ext
open import Data.List.Relation.Binary.Sublist.Propositional as S
import Data.Maybe.Relation.Unary.Any as M
\end{code}
\begin{code}[hide]
module _
\end{code}
\begin{code}
(khs : ℙ KeyHash) (I : Maybe Slot × Maybe Slot)
\end{code}
\begin{code}[hide]
where
data
\end{code}
\begin{code}
module _ (khs : ℙ KeyHash) (I : Maybe Slot × Maybe Slot) where
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since this module block contains only one thing, I think it'd be better to just add these as arguments to the datatype.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(done)

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh gosh, the repetition...

Also isn't it more confusing now to have the readers read "indexed constant types"?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there any repetition?

Generally I agree, but I think presenting evalTimelock as a datatype is a bad idea in the first place (why isn't it a function?). So when we have a spec that actually wants to present this there's a decent chance that we'll want to refactor this anyway.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The repetition comes from the "constant" indices, s/evalTimelock/(evalTimelock khs I), which is why I used module parameters as the best practice to avoid this, and results in much more readable constructors.

Having said that, I agree that using the "call-graph view" of the function as a datatype might be a bit too much here, I don't know why Ali initially did it this way. I agree you should investigate the alternative sooner rather than later to avoid maintenance overhead.

data evalTimelock : Timelock → Set where

evalTimelock : Timelock → Set where
evalAll : All evalTimelock ss
→ evalTimelock (RequireAllOf ss)
evalAny : Any evalTimelock ss
Expand Down
10 changes: 9 additions & 1 deletion src/Ledger/TokenAlgebra/ValueSet.lagda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,19 +61,27 @@ open CommutativeMonoid renaming (_∙_ to _⋆_) hiding (refl ; sym ; trans)

AssetId = PolicyId × AssetName
Quantity = ℕ

\end{code}
\begin{code}[hide]
module _
\end{code}
\begin{code}

{X : ℙ AssetId}
{⋁A : isMaximal X}
⦃ DecEq-PolicyId : DecEq PolicyId ⦄
⦃ DecEq-AssetName : DecEq AssetName ⦄
⦃ DecEq-Tot : DecEq (AssetId ⇒ ℕ) ⦄
(Dec-lookup≤ : ∀ {u v : AssetId ⇒ ℕ}
→ (∀ {a p q} → lookup u (a , p) ≤ lookup v (a , q)) ⁇)
\end{code}
\begin{code}[hide]
where

open ≡-Reasoning
open FunTot X ⋁A
\end{code}
\begin{code}

_⊕_ : Op₂ (AssetId ⇒ Quantity)
u ⊕ v = Fun⇒TotalMap λ aa → (lookup u) aa + (lookup v) aa
Expand Down
Loading