Skip to content

Commit

Permalink
commented and simplified TyProp
Browse files Browse the repository at this point in the history
  • Loading branch information
jmchapman committed Jul 9, 2020
1 parent a5eed06 commit a0fd503
Show file tree
Hide file tree
Showing 2 changed files with 12 additions and 12 deletions.
16 changes: 8 additions & 8 deletions language-plutus-core/prop-test/Language/PlutusCore/PropTest.hs
Original file line number Diff line number Diff line change
Expand Up @@ -31,14 +31,14 @@ import Text.Printf


-- |The type for properties with access to both representations.
type TyProp = Kind ()
-> ClosedTypeG
-> Kind ()
-> Quote (Type TyName DefaultUni ())
-> Cool

type TyProp = Kind () -- ^ kind for generated type
-> ClosedTypeG -- ^ generated type
-> Quote (Type TyName DefaultUni ()) -- ^ external rep. of gen. type
-> Cool -- ^ whether the property holds
-- |Internal version of type properties.
type TyPropG = Kind () -> ClosedTypeG -> Cool
type TyPropG = Kind () -- ^ kind of the generated type
-> ClosedTypeG -- ^ generated type
-> Cool -- ^ whether the property holds


-- |Test property on well-kinded types.
Expand Down Expand Up @@ -81,7 +81,7 @@ toTyPropG :: TyProp -> TyPropG
toTyPropG typrop kG tyG = tyG_ok Cool.!=> typrop_ok
where
tyG_ok = checkClosedTypeG kG tyG
typrop_ok = typrop kG tyG kG (toClosedType kG tyG)
typrop_ok = typrop kG tyG (toClosedType kG tyG)


-- |Stream of type names t0, t1, t2, ..
Expand Down
8 changes: 4 additions & 4 deletions language-plutus-core/prop-test/Spec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -40,22 +40,22 @@ tests = testGroup "all tests"

-- |Property: Kind checker for generated types is sound.
prop_checkKindSound :: TyProp
prop_checkKindSound _ _ k tyQ = isSafe $ do
prop_checkKindSound k _ tyQ = isSafe $ do
ty <- liftQuote tyQ
checkKind defConfig () ty k

-- |Property: Normalisation preserves kind.
prop_normalizePreservesKind :: TyProp
prop_normalizePreservesKind _ _ k tyQ = isSafe $ do
prop_normalizePreservesKind k _ tyQ = isSafe $ do
ty <- liftQuote tyQ
ty' <- unNormalized <$> normalizeType ty
checkKind defConfig () ty' k

-- |Property: Normalisation for generated types is sound.
prop_normalizeTypeSound :: TyProp
prop_normalizeTypeSound kG tyG _ tyQ = isSafe $ do
prop_normalizeTypeSound k tyG tyQ = isSafe $ do
ty1 <- unNormalized <$> (normalizeType =<< liftQuote tyQ)
ty2 <- toClosedType kG (normalizeTypeG tyG)
ty2 <- toClosedType k (normalizeTypeG tyG)
return (ty1 == ty2)

-- |Check if the type/kind checker threw any errors.
Expand Down

0 comments on commit a0fd503

Please sign in to comment.