Skip to content

Commit

Permalink
Added Constrained.SumList.hs to repo (#4827)
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.
Gave HasSpec (optional) method 'typeSpecHasError' a better default value
  • Loading branch information
TimSheard authored Jan 20, 2025
1 parent 7683b73 commit 688430f
Show file tree
Hide file tree
Showing 8 changed files with 829 additions and 112 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)
noNegativeValues = 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)
noNegativeValues = 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 688430f

Please sign in to comment.