covenant
Copyright(C) MLabs 2025
LicenseApache 2.0
Maintainerkoz@mlabs.city, sean@mlabs.city
Safe HaskellNone
LanguageHaskell2010

Covenant.Test

Description

Various utilities designed to help test Covenant.

Note

This is probably not that useful to end users of Covenant, but needs to be exposed so the tests can use this functionality.

Since: 1.0.0

Synopsis

QuickCheck data wrappers

newtype Concrete Source #

Wrapper for ValT to provide an Arbitrary instance to generate only value types without any type variables.

Since: 1.0.0

Constructors

Concrete (ValT AbstractTy) 

Instances

Instances details
Arbitrary Concrete Source #

Since: 1.0.0

Instance details

Defined in Covenant.Test

Methods

arbitrary :: Gen Concrete #

shrink :: Concrete -> [Concrete] #

Show Concrete Source #

Since: 1.0.0

Instance details

Defined in Covenant.Test

Methods

showsPrec :: Int -> Concrete -> ShowS #

show :: Concrete -> String #

showList :: [Concrete] -> ShowS #

Eq Concrete Source #

Since: 1.0.0

Instance details

Defined in Covenant.Test

Methods

(==) :: Concrete -> Concrete -> Bool #

(/=) :: Concrete -> Concrete -> Bool #

data DataDeclFlavor Source #

A 'description type' designed for use with DataDeclSet to describe what kind of types it contains.

Since: 1.1.0

Constructors

ConcreteDecl

All constructor arguments are concrete and the declaration is monomorphic.

Since: 1.1.0

ConcreteNestedDecl

As ConcreteDecl, but can re-use already generated concrete declarations in the context to make nested types.

Since: 1.1.0

SimpleRecursive

Recursive, monomorphic type (such as data IntList = End | More Int IntList).

Since: 1.1.0

Poly1

Polymorphic types in one variable, which may or may not be recursive.

Since: 1.1.0

Poly1PolyThunks

As Poly1, but may have further polymorphism via thunks.

Since: 1.1.0

newtype DataDeclSet (flavor :: DataDeclFlavor) Source #

Helper type to generate datatype definitions. Specifically, this stores already-generated datatype declarations for our (re)use when generating.

Since: 1.1.0

Constructors

DataDeclSet [DataDeclaration AbstractTy] 

Instances

Instances details
Arbitrary (DataDeclSet 'ConcreteDecl) Source # 
Instance details

Defined in Covenant.Test

Methods

arbitrary :: Gen (DataDeclSet 'ConcreteDecl) #

shrink :: DataDeclSet 'ConcreteDecl -> [DataDeclSet 'ConcreteDecl] #

Arbitrary (DataDeclSet 'ConcreteNestedDecl) Source # 
Instance details

Defined in Covenant.Test

Methods

arbitrary :: Gen (DataDeclSet 'ConcreteNestedDecl) #

shrink :: DataDeclSet 'ConcreteNestedDecl -> [DataDeclSet 'ConcreteNestedDecl] #

Arbitrary (DataDeclSet 'Poly1) Source # 
Instance details

Defined in Covenant.Test

Methods

arbitrary :: Gen (DataDeclSet 'Poly1) #

shrink :: DataDeclSet 'Poly1 -> [DataDeclSet 'Poly1] #

Arbitrary (DataDeclSet 'Poly1PolyThunks) Source # 
Instance details

Defined in Covenant.Test

Methods

arbitrary :: Gen (DataDeclSet 'Poly1PolyThunks) #

shrink :: DataDeclSet 'Poly1PolyThunks -> [DataDeclSet 'Poly1PolyThunks] #

Arbitrary (DataDeclSet 'SimpleRecursive) Source # 
Instance details

Defined in Covenant.Test

Methods

arbitrary :: Gen (DataDeclSet 'SimpleRecursive) #

shrink :: DataDeclSet 'SimpleRecursive -> [DataDeclSet 'SimpleRecursive] #

Functions

Lifted QuickCheck functions

chooseInt :: MonadGen m => (Int, Int) -> m Int Source #

The same as chooseInt, but lifted to work in any MonadGen.

Since: 1.1.0

scale :: MonadGen m => (Int -> Int) -> m a -> m a Source #

The same as scale, but lifted to work in any MonadGen.

Since: 1.1.0

DataDeclSet functionality

prettyDeclSet :: forall (a :: DataDeclFlavor). DataDeclSet a -> String Source #

Prettyprinter for DataDeclSet.

Since: 1.1.0

Test helpers

checkApp :: Map TyName (DatatypeInfo AbstractTy) -> CompT Renamed -> [Maybe (ValT Renamed)] -> Either TypeAppError (ValT Renamed) Source #

Given information about in-scope datatypes, a computation type, and a list of arguments (some of which may be errors), try to construct the type of the result of the application of those arguments to the computation.

Since: 1.0.0

failLeft :: Show a => Either a b -> IO b Source #

If the argument is a Right, pass the assertion; otherwise, fail the assertion.

Since: 1.1.0

tyAppTestDatatypes :: Map TyName (DatatypeInfo AbstractTy) Source #

Small collection of datatypes needed to test type application logic.

Since: 1.1.0

list :: DataDeclaration AbstractTy Source #

The onchain list type.

Since: 1.1.0

tree :: DataDeclaration AbstractTy Source #

A datatype equivalent to

data Tree a = Bin (Tree a) (Tree a) | Tip a

Since: 1.1.0

weirderList :: DataDeclaration AbstractTy Source #

A datatype equivalent to

data WeirderList a = Uncons (Maybe (a, WeirderList a))

Since: 1.1.0

unsafeTyCon :: TyName -> [ValT a] -> ValT a Source #

Helper for tests to quickly construct Datatypes. This is unsafe, as it allows construction of nonsensical renamings.

Since: 1.1.0

Datatype checks

cycleCheck :: Ord a => Map TyName (DataDeclaration a) -> Maybe KindCheckError Source #

Verifies that no types in the argument are mutually recursive.

Since: 1.1.0

checkDataDecls :: Map TyName (DataDeclaration AbstractTy) -> Either KindCheckError () Source #

Checks that all the data declarations in the argument 'make sense'. Specifically:

  • The strategy declared for the datatype is valid for it
  • There are no mutually recursive datatype declarations
  • Constructor arguments are not thunks
  • The number of type variables in any constructor isn't greater than we expect

Since: 1.1.0

checkEncodingArgs :: forall a info. (info -> DataEncoding) -> Map TyName info -> ValT a -> Either (EncodingArgErr a) () Source #

Verifies that a datatype (third argument) is valid according to its stated encoding, as provided by the first two arguments (projection and metadata).

Note

If the datatype being validated refers to other datatypes, we assume that they exist in the metadata Map. Thus, we must ensure this holds or the check will fail.

Since: 1.1.0

Renaming

Types

data RenameError Source #

Ways in which the renamer can fail.

Since: 1.1.0

Constructors

InvalidAbstractionReference Int (Index "tyvar")

An attempt to reference an abstraction in a scope where this abstraction doesn't exist. First field is the true level, second is the index that was requested.

Since: 1.0.0

Instances

Instances details
Show RenameError Source # 
Instance details

Defined in Covenant.Internal.Rename

Methods

showsPrec :: Int -> RenameError -> ShowS #

show :: RenameError -> String #

showList :: [RenameError] -> ShowS #

Eq RenameError Source # 
Instance details

Defined in Covenant.Internal.Rename

Methods

(==) :: RenameError -> RenameError -> Bool #

(/=) :: RenameError -> RenameError -> Bool #

data RenameM a Source #

A 'renaming monad' which allows us to convert type representations from ones that use relative abstraction labelling to absolute abstraction labelling.

Why this is necessary

Consider the following AbstractTy: BoundAtScope 1 0. The meaning of this is relative to where in a type it is positioned: it could be bound by a scope higher than our own, or something we can unify with. Because its meaning (namely, what it refers to) is situational, type checking becomes more difficult, although it has other advantages.

This monad allows us to convert this relative form into an absolute one. More specifically, the renamer does two things:

  • Ensures that any given abstraction refers to one, and only one, thing; and
  • Indicates which abstractions are unifiable, and which are (effectively) constant or fixed.

Since: 1.0.0

Instances

Instances details
Applicative RenameM Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Rename

Methods

pure :: a -> RenameM a #

(<*>) :: RenameM (a -> b) -> RenameM a -> RenameM b #

liftA2 :: (a -> b -> c) -> RenameM a -> RenameM b -> RenameM c #

(*>) :: RenameM a -> RenameM b -> RenameM b #

(<*) :: RenameM a -> RenameM b -> RenameM a #

Functor RenameM Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Rename

Methods

fmap :: (a -> b) -> RenameM a -> RenameM b #

(<$) :: a -> RenameM b -> RenameM a #

Monad RenameM Source #

Since: 1.0.0

Instance details

Defined in Covenant.Internal.Rename

Methods

(>>=) :: RenameM a -> (a -> RenameM b) -> RenameM b #

(>>) :: RenameM a -> RenameM b -> RenameM b #

return :: a -> RenameM a #

Introduction

renameValT :: ValT AbstractTy -> RenameM (ValT Renamed) Source #

Rename a value type.

Since: 1.0.0

renameCompT :: CompT AbstractTy -> RenameM (CompT Renamed) Source #

Rename a computation type.

Since: 1.0.0

renameDataDecl :: DataDeclaration AbstractTy -> RenameM (DataDeclaration Renamed) Source #

Elimination

runRenameM :: RenameM a -> Either RenameError a Source #

Execute a renaming computation.

Since: 1.0.0