Skip to content

Commit 83cdef1

Browse files
authored
Merge pull request #3730 from Quviq/PR-typerep-show
Implement `Show` instance for `Rep` using `IsTypeable`
2 parents c3d0bea + 7a61b15 commit 83cdef1

File tree

9 files changed

+121
-234
lines changed

9 files changed

+121
-234
lines changed

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Ast.hs

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -160,21 +160,21 @@ infix 4 :⊆:
160160
pattern (:⊆:) :: forall era. (forall a. Ord a => Term era (Set a) -> Term era (Set a) -> Pred era)
161161
pattern x :⊆: y = Subset x y
162162

163-
pattern ExactSize :: Int -> Term era Size
163+
pattern ExactSize :: Era era => Int -> Term era Size
164164
pattern ExactSize x <- (sameRng -> Just x)
165165
where
166166
ExactSize x = Lit SizeR (SzRng x x)
167167

168-
pattern AtLeast :: Int -> Term era Size
168+
pattern AtLeast :: Era era => Int -> Term era Size
169169
pattern AtLeast n = Lit SizeR (SzLeast n)
170170

171-
pattern Size :: Size -> Term era Size
171+
pattern Size :: Era era => Size -> Term era Size
172172
pattern Size n = Lit SizeR n
173173

174-
pattern AtMost :: Int -> Term era Size
174+
pattern AtMost :: Era era => Int -> Term era Size
175175
pattern AtMost n = Lit SizeR (SzMost n)
176176

177-
pattern Range :: Int -> Int -> Term era Size
177+
pattern Range :: Era era => Int -> Int -> Term era Size
178178
pattern Range i j <- Lit SizeR (SzRng i j)
179179
where
180180
Range i j =
@@ -195,7 +195,7 @@ sameRng :: Term era Size -> Maybe Int
195195
sameRng (Lit SizeR (SzRng x y)) = if x == y then Just x else Nothing
196196
sameRng _ = Nothing
197197

198-
pattern Word64 :: Word64 -> Term era Word64
198+
pattern Word64 :: Era era => Word64 -> Term era Word64
199199
pattern Word64 x = Lit Word64R x
200200

201201
var :: Era era => String -> Rep era t -> Term era t
@@ -1009,7 +1009,7 @@ runComp _ t (AnyF (FConst r v _ l)) = do
10091009
With _ <- hasEq r r
10101010
pure $ t ^. l == v
10111011

1012-
termRep :: Term era t -> Rep era t
1012+
termRep :: Era era => Term era t -> Rep era t
10131013
termRep (Lit r _) = r
10141014
termRep (Var (V _ r _)) = r
10151015
termRep (Dom (termRep -> MapR r _)) = SetR r
@@ -1041,7 +1041,7 @@ makeTest env c = do
10411041
b <- runPred env c
10421042
pure (show c ++ " => " ++ show b, b, c)
10431043

1044-
displayTerm :: Env era -> Term era a -> IO ()
1044+
displayTerm :: Era era => Env era -> Term era a -> IO ()
10451045
displayTerm env (Var v@(V nm rep _)) = do
10461046
x <- monadTyped (findVar v env)
10471047
putStrLn (nm ++ "\n" ++ format rep x)

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Examples.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -727,7 +727,7 @@ test19 = do
727727

728728
-- ===================================================
729729

730-
preds20 :: Proof era -> [Pred era]
730+
preds20 :: Era era => Proof era -> [Pred era]
731731
preds20 proof =
732732
[ Sized (ExactSize 10) intUniv
733733
, Sized (AtMost 6) rewardsx

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Preds/Certs.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -480,5 +480,5 @@ maybeSL = lens foo bar
480480
poolMetaL :: Lens' (PoolParams era) (StrictMaybe PoolMetadata)
481481
poolMetaL = lens ppMetadata (\x r -> x {ppMetadata = r})
482482

483-
poolMetadata :: Proof era -> Term era (Maybe PoolMetadata)
483+
poolMetadata :: Era era => Proof era -> Term era (Maybe PoolMetadata)
484484
poolMetadata p = Var (pV p "poolMetadata" (MaybeR (PoolMetadataR p)) (Yes PoolParamsR (poolMetaL . sMaybeL)))

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Shrink.hs

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ module Test.Cardano.Ledger.Constrained.Shrink (
77
import Control.Monad
88
import Data.Maybe
99

10-
import Cardano.Ledger.Core (Era (..))
1110
import Test.Cardano.Ledger.Constrained.Ast
1211
import Test.Cardano.Ledger.Constrained.Env
1312
import Test.Cardano.Ledger.Constrained.Monad
@@ -29,7 +28,7 @@ justOneName xs = foldr accum [] xs -- FIXME throw away new style DependGraph ele
2928
-- Note that the DependGraph tells us the dependency order of the variables: a variable only
3029
-- depends on the variables before it in the graph, so when shrinking the value of a variable we
3130
-- only need to adjust the values of later variables.
32-
shrinkEnv :: Era era => DependGraph era -> Env era -> [Env era]
31+
shrinkEnv :: DependGraph era -> Env era -> [Env era]
3332
shrinkEnv (DependGraph vs) env =
3433
[ env'
3534
| (before, (x, cs), after) <- splits (justOneName vs)
@@ -40,7 +39,7 @@ shrinkEnv (DependGraph vs) env =
4039
splits [] = []
4140
splits (x : xs) = ([], x, xs) : [(x : ys, y, zs) | (ys, y, zs) <- splits xs]
4241

43-
shrinkOneVar :: Era era => Env era -> [Name era] -> Name era -> [Pred era] -> [(Name era, [Pred era])] -> [Env era]
42+
shrinkOneVar :: Env era -> [Name era] -> Name era -> [Pred era] -> [(Name era, [Pred era])] -> [Env era]
4443
shrinkOneVar originalEnv before x cs after =
4544
[ env'
4645
| val' <- shrinkVar x cs' val
@@ -56,15 +55,15 @@ shrinkOneVar originalEnv before x cs after =
5655
cs' = map (substPred beforeSubst) cs
5756
val = fromJust $ findName x originalEnv
5857

59-
shrinkVar :: Era era => Name era -> [Pred era] -> Payload era -> [Payload era]
58+
shrinkVar :: Name era -> [Pred era] -> Payload era -> [Payload era]
6059
shrinkVar v cs p = [p' | p' <- shrinkPayload p, validAssignment v p' cs]
6160

62-
shrinkPayload :: Era era => Payload era -> [Payload era]
61+
shrinkPayload :: Payload era -> [Payload era]
6362
shrinkPayload (Payload rep t acc) = [Payload rep t' acc | t' <- shrinkRep rep t]
6463

6564
-- | Compute something satisfying the constraints that's as "close" to the original value as
6665
-- possible. TODO: more cleverness
67-
fixupVar :: Era era => Name era -> [Pred era] -> Payload era -> Maybe (Payload era)
66+
fixupVar :: Name era -> [Pred era] -> Payload era -> Maybe (Payload era)
6867
fixupVar v cs p = listToMaybe [p' | p' <- [p | validAssignment v p cs] ++ reverse (shrinkVar v cs p)]
6968

7069
-- | Assumes the variable is the only free variable in the constraints.

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Solver.hs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,7 @@ isCountType rep = case hasCount rep rep of
130130
-- ==================================================
131131
-- Extras, simple helper functions
132132

133-
sameRep :: Era era => Rep era i -> Rep era j -> Typed (i :~: j)
133+
sameRep :: Rep era i -> Rep era j -> Typed (i :~: j)
134134
sameRep r1 r2 = case testEql r1 r2 of
135135
Just x -> pure x
136136
Nothing -> failT ["Type error in sameRep:\n " ++ show r1 ++ " =/=\n " ++ show r2]
@@ -167,7 +167,7 @@ exactlyOne pp xs = 1 == length (filter pp xs)
167167
-- This has been superceeded by the RelLens RelSpec
168168
projOnDom ::
169169
forall era a dom rng.
170-
(Era era, Ord dom) =>
170+
Ord dom =>
171171
Set a ->
172172
Lens' dom a ->
173173
Rep era dom ->
@@ -180,7 +180,7 @@ projOnDom setA lensDomA repDom repRng = do
180180
where
181181
genThenOverwriteA a = Lens.set lensDomA a <$> genRep repDom
182182

183-
atLeast :: (Era era, Adds c) => Rep era c -> c -> Gen c
183+
atLeast :: Adds c => Rep era c -> c -> Gen c
184184
atLeast rep c = add c <$> genRep rep
185185

186186
-- ================================================================
@@ -623,7 +623,7 @@ summandsAsInt (x : xs) = do
623623
m <- summandsAsInt xs
624624
pure (m + n)
625625

626-
sameV :: Era era => V era s -> V era t -> Typed (s :~: t)
626+
sameV :: V era s -> V era t -> Typed (s :~: t)
627627
sameV (V _ r1 _) (V _ r2 _) = sameRep r1 r2
628628

629629
unique2 :: Adds c => V era t -> (Int, Bool, [Name era]) -> Sum era c -> Typed (Int, Bool, [Name era])
@@ -689,7 +689,7 @@ solveLists v@(V nm (ListR _) _) cs =
689689
-- Helper functions for use in 'dispatch'
690690

691691
-- | Combine solving an generating for a variable with a 'Counts' instance
692-
genCount :: (Count t, Era era) => V era t -> [Pred era] -> Typed (Gen t)
692+
genCount :: Count t => V era t -> [Pred era] -> Typed (Gen t)
693693
genCount v1@(V _ rep _) [Random (Var v2)] | Name v1 == Name v2 = pure (genRep rep)
694694
genCount v1@(V _ r1 _) [Var v2@(V _ r2 _) :=: expr] | Name v1 == Name v2 = do
695695
Refl <- sameRep r1 r2
@@ -731,7 +731,7 @@ update :: t -> [Update t] -> t
731731
update t [] = t
732732
update t (Update s l : more) = update (Lens.set l s t) more
733733

734-
anyToUpdate :: Era era => Rep era t1 -> (AnyF era t2) -> Typed (Update t1)
734+
anyToUpdate :: Rep era t1 -> (AnyF era t2) -> Typed (Update t1)
735735
anyToUpdate rep1 (AnyF (FConst _ s rep2 l)) = do
736736
Refl <- sameRep rep1 rep2
737737
pure (Update s l)

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Spec.hs

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1546,7 +1546,7 @@ runElemSpec xs spec = case spec of
15461546

15471547
genElemSpec ::
15481548
forall w era.
1549-
(Adds w, Era era) =>
1549+
Adds w =>
15501550
Rep era w ->
15511551
-- Rep era c ->
15521552
SomeLens era w ->
@@ -1583,7 +1583,6 @@ genElemSpec repw (SomeLens (l :: Lens' w c)) siz = do
15831583

15841584
genFromElemSpec ::
15851585
forall era r.
1586-
Era era =>
15871586
[String] ->
15881587
Gen r ->
15891588
Int ->
@@ -1710,7 +1709,7 @@ runListSpec xs spec = case spec of
17101709

17111710
genListSpec ::
17121711
forall w era.
1713-
(Adds w, Era era) =>
1712+
Adds w =>
17141713
Rep era w ->
17151714
-- Rep era c ->
17161715
SomeLens era w ->
@@ -1722,7 +1721,6 @@ genListSpec repw l size = do
17221721

17231722
genFromListSpec ::
17241723
forall era r.
1725-
Era era =>
17261724
[String] ->
17271725
Gen r ->
17281726
ListSpec era r ->
@@ -1838,7 +1836,7 @@ someSet g = do
18381836
n <- pos @Int
18391837
Set.fromList <$> vectorOf n g
18401838

1841-
someMap :: forall era t d. (Ord d, TestAdd t, Era era) => Rep era d -> Gen (Map d t)
1839+
someMap :: forall era t d. (Ord d, TestAdd t) => Rep era d -> Gen (Map d t)
18421840
someMap r = do
18431841
n <- pos @Int
18441842
rs <- vectorOf n anyAdds
@@ -1857,7 +1855,7 @@ testm = do
18571855
b <- aMap
18581856
monadTyped (liftT (a <> b))
18591857

1860-
aList :: Era era => Gen (ListSpec era Word64)
1858+
aList :: Gen (ListSpec era Word64)
18611859
aList = genSize >>= genListSpec Word64R (SomeLens word64CoinL)
18621860

18631861
testl :: Gen (ListSpec TT Word64)
@@ -2174,7 +2172,7 @@ runPairSpec m1 (PairSpec _ _ VarOnRight m2) = Map.isSubmapOf m2 m1
21742172
-- and insist that when solving 'var' it contains the pairs from 'm2' and possibly more pairs
21752173
runPairSpec m1 (PairSpec _ _ VarOnLeft m2) = Map.isSubmapOf m1 m2
21762174

2177-
genPairSpec :: (Era era, Ord dom, Eq rng) => Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
2175+
genPairSpec :: forall era dom rng. (Ord dom, Eq rng) => Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
21782176
genPairSpec domr rngr =
21792177
frequency
21802178
[ (1, pure PairAny)
@@ -2202,7 +2200,7 @@ fixSide _ PairAny = PairAny
22022200
fixSide side (PairSpec d r _ m) = PairSpec d r side m
22032201

22042202
genConsistentPairSpec ::
2205-
(Ord dom, Era era, Eq rng) =>
2203+
(Ord dom, Eq rng) =>
22062204
Rep era dom ->
22072205
Rep era rng ->
22082206
PairSpec era dom rng ->
@@ -2236,7 +2234,7 @@ genConsistentPairSpec _ _ (PairSpec d r VarOnLeft m) =
22362234
)
22372235
]
22382236

2239-
genFromPairSpec :: (Era era, Ord dom) => [String] -> PairSpec era dom rng -> Gen (Map dom rng)
2237+
genFromPairSpec :: forall era dom rng. Ord dom => [String] -> PairSpec era dom rng -> Gen (Map dom rng)
22402238
genFromPairSpec msgs (PairNever xs) = errorMess "genFromPairSpec failed due to PairNever" (msgs ++ xs)
22412239
genFromPairSpec _msgs PairAny = pure $ Map.empty
22422240
genFromPairSpec msgs p@(PairSpec domr rngr VarOnRight mp) = do

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Trace/Actions.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ import Test.Cardano.Ledger.Generic.Proof hiding (lift)
1616
-- Some experiments with updating the state (Stored in the Env)
1717
-- Used as a means to track what applySTS does.
1818

19-
inputsAction :: Proof era -> Set (TxIn (EraCrypto era)) -> TraceM era ()
19+
inputsAction :: Era era => Proof era -> Set (TxIn (EraCrypto era)) -> TraceM era ()
2020
inputsAction proof is = updateVar (utxo proof) (\u -> Map.withoutKeys u is)
2121

2222
outputsAction :: Reflect era => Proof era -> TxBody era -> [TxOutF era] -> TraceM era ()

0 commit comments

Comments
 (0)