Skip to content

Commit

Permalink
Added Constrained.SumList.hs to repo
Browse files Browse the repository at this point in the history
Defined pickAll the basis of sums with fixed length.
Added getSizedList as a method of the Foldy class
getSizeList cost is metered at 1000 calls. Typical calls are less than 10.
  • Loading branch information
TimSheard committed Jan 14, 2025
1 parent 7683b73 commit 1d97b29
Show file tree
Hide file tree
Showing 8 changed files with 806 additions and 85 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@ import Cardano.Ledger.Plutus.CostModels (CostModels)
import Cardano.Ledger.Plutus.ExUnits
import Cardano.Ledger.Shelley.PParams (ProposedPPUpdates (..))
import Constrained hiding (Value)
import Constrained.Base (genListWithSize)
import Constrained.Univ ()
import Control.Monad.Identity (Identity (..))
import Control.Monad.Trans.Fail.String
Expand Down Expand Up @@ -95,6 +96,10 @@ instance BaseUniverse fn => Foldy fn Coin where
genList s s' = map fromSimpleRep <$> genList @fn @Word64 (toSimpleRepSpec s) (toSimpleRepSpec s')
theAddFn = addFn
theZero = Coin 0
genSizedList sz elemSpec foldSpec =
map fromSimpleRep
<$> genListWithSize @fn @Word64 sz (toSimpleRepSpec elemSpec) (toSimpleRepSpec foldSpec)
nonNeg = True

-- TODO: This is hack to get around the need for `Num` in `NumLike`. We should possibly split
-- this up so that `NumLike` has its own addition etc. instead?
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,14 @@ import Cardano.Ledger.UTxO
import Cardano.Ledger.Val (Val)
import Constrained hiding (Sized, Value)
import Constrained qualified as C
import Constrained.Base (Binder (..), HasGenHint (..), Pred (..), Term (..), explainSpecOpt)
import Constrained.Base (
Binder (..),
HasGenHint (..),
Pred (..),
Term (..),
explainSpecOpt,
genListWithSize,
)
import Constrained.Spec.Map
import Control.DeepSeq (NFData)
import Crypto.Hash (Blake2b_224)
Expand Down Expand Up @@ -250,6 +257,10 @@ instance IsConwayUniv fn => Foldy fn DeltaCoin where
genList s s' = map fromSimpleRep <$> genList @fn @Integer (toSimpleRepSpec s) (toSimpleRepSpec s')
theAddFn = addFn
theZero = DeltaCoin 0
genSizedList sz elemSpec foldSpec =
map fromSimpleRep
<$> genListWithSize @fn @Integer sz (toSimpleRepSpec elemSpec) (toSimpleRepSpec foldSpec)
nonNeg = False

deriving via Integer instance Num DeltaCoin

Expand Down
2 changes: 2 additions & 0 deletions libs/constrained-generators/constrained-generators.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ library
Constrained.Examples.Basic
Constrained.Examples.CheatSheet
Constrained.Examples.Either
Constrained.Examples.Fold
Constrained.Examples.List
Constrained.Examples.Map
Constrained.Examples.Set
Expand All @@ -41,6 +42,7 @@ library
Constrained.Spec.Map
Constrained.Spec.Pairs
Constrained.Spec.Tree
Constrained.SumList
Constrained.Syntax
Constrained.Univ

Expand Down
Loading

0 comments on commit 1d97b29

Please sign in to comment.