| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Unison.PatternMatchCoverage.Class
Synopsis
- class (Ord loc, Var vt, Var v, MonadFix m) => Pmc vt v loc (m :: Type -> Type) | m -> vt v loc where
- getConstructors :: Type vt loc -> m (EnumeratedConstructors vt v loc)
- getConstructorVarTypes :: Type vt loc -> ConstructorReference -> m [Type vt loc]
- getConstructorIndexRefinements :: Type vt loc -> ConstructorReference -> m [(vt, Type vt loc)]
- fresh :: m v
- getPrettyPrintEnv :: m PrettyPrintEnv
- data EnumeratedConstructors vt v loc
- = ConstructorType [(v, ConstructorReference, Type vt loc)]
- | AbilityType (Type vt loc) (Map ConstructorReference (v, Type vt loc))
- | SequenceType [(ListPat, [Type vt loc])]
- | RecordType (Map Text (Type vt loc))
- | BooleanType
- | OtherType
- traverseConstructorTypes :: Applicative f => (v -> ConstructorReference -> Type vt loc -> f (Type vt loc)) -> EnumeratedConstructors vt v loc -> f (EnumeratedConstructors vt v loc)
Documentation
class (Ord loc, Var vt, Var v, MonadFix m) => Pmc vt v loc (m :: Type -> Type) | m -> vt v loc where Source #
A typeclass for the queries required to perform pattern match coverage checking.
Methods
getConstructors :: Type vt loc -> m (EnumeratedConstructors vt v loc) Source #
Get the constructors of a type
getConstructorVarTypes :: Type vt loc -> ConstructorReference -> m [Type vt loc] Source #
Get the types of the arguments of a specific constructor
getConstructorIndexRefinements :: Type vt loc -> ConstructorReference -> m [(vt, Type vt loc)] Source #
The GADT type-index equations implied by matching the given constructor
against a value of the given type — the proposition the DK indexed-types
paper attaches to a constructor via the asserting type A ∧ P, recovered
here by unifying the constructor's result with the scrutinee's type. Each
pair maps a (rigid) index variable to the type the constructor pins it to.
Empty for ordinary (non-index-pinning) constructors.
Get a fresh variable
data EnumeratedConstructors vt v loc Source #
Constructors
| ConstructorType [(v, ConstructorReference, Type vt loc)] | |
| AbilityType (Type vt loc) (Map ConstructorReference (v, Type vt loc)) | |
| SequenceType [(ListPat, [Type vt loc])] | |
| RecordType (Map Text (Type vt loc)) | A record is a product with a single constructor, whose argument types are the field types. Carrying the field names lets us name the variables we introduce for them. |
| BooleanType | |
| OtherType |
Instances
| (Show v, Show vt) => Show (EnumeratedConstructors vt v loc) Source # | |
Defined in Unison.PatternMatchCoverage.Class Methods showsPrec :: Int -> EnumeratedConstructors vt v loc -> ShowS # show :: EnumeratedConstructors vt v loc -> String # showList :: [EnumeratedConstructors vt v loc] -> ShowS # | |
traverseConstructorTypes :: Applicative f => (v -> ConstructorReference -> Type vt loc -> f (Type vt loc)) -> EnumeratedConstructors vt v loc -> f (EnumeratedConstructors vt v loc) Source #