| Copyright | disco team and contributors |
|---|---|
| License | BSD-3-Clause |
| Maintainer | byorgey@gmail.com |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Disco.Exhaustiveness.TypeInfo
Description
Utilities for converting Disco types into Constructors
that the exhaustiveness checker understands, and utilities
for working with TypedVars and their names.
Synopsis
- newtype TypedVar = TypedVar (Name ATerm, Type)
- getType :: TypedVar -> Type
- data DataCon = DataCon {}
- data Ident where
- data Constructors where
- Finite :: [DataCon] -> Constructors
- Infinite :: [DataCon] -> Constructors
- unknown :: DataCon
- unit :: DataCon
- bool :: Bool -> DataCon
- natural :: Integer -> DataCon
- integer :: Integer -> DataCon
- char :: Char -> DataCon
- cons :: Type -> Type -> DataCon
- nil :: DataCon
- pair :: Type -> Type -> DataCon
- left :: Type -> DataCon
- right :: Type -> DataCon
- tyDataCons :: Type -> TyDefCtx -> Constructors
- resolveAlias :: Type -> TyDefCtx -> Type
- tyDataConsHelper :: Type -> Constructors
- newName :: Member Fresh r => Sem r (Name ATerm)
- newVar :: Member Fresh r => Type -> Sem r TypedVar
- newNames :: Member Fresh r => Int -> Sem r [Name ATerm]
- newVars :: Member Fresh r => [Type] -> Sem r [TypedVar]
Documentation
Constructors
| KUnit :: Ident | |
| KBool :: Bool -> Ident | |
| KNat :: Integer -> Ident | |
| KInt :: Integer -> Ident | |
| KPair :: Ident | |
| KCons :: Ident | |
| KNil :: Ident | |
| KChar :: Char -> Ident | |
| KLeft :: Ident | |
| KRight :: Ident | |
| KUnknown :: Ident |
data Constructors where Source #
Finite constructors are used in the LYG checker
Infinite constructors are used when reporting
examples of uncovered patterns, we only pick out a few of them
Constructors
| Finite :: [DataCon] -> Constructors | |
| Infinite :: [DataCon] -> Constructors |
tyDataCons :: Type -> TyDefCtx -> Constructors Source #
tyDataConsHelper :: Type -> Constructors Source #
Assuming type aliases have been resolved, this function converts Disco types into lists of DataCons that are compatible with the LYG checker.
A list of constructors is Infinite if the only way to fully
match against the type is with a wildcard or variable pattern.
Otherwise, it is Finite.
The LYG checker only reads the list of constructors if
a type is Finite. From the point of view of the checker,
Infinite is a synonym for opaque, and the constructors are discarded.
The dataconstructors in an Infinite list are only
used when generating the 3 positive examples of what
you haven't matched against.
This will probably need to change a bit when bringing
exhaustiveness checking to the new arithmetic patterns.
Notice the last case of this function, which a wildcard handling the types: (_ Ty.:->: _) (Ty.TySet _) (Ty.TyBag _) (Ty.TyVar _) (Ty.TySkolem _) (Ty.TyProp) (Ty.TyMap _ _) (Ty.TyGraph _)
I believe all of these are impossible to pattern match against
with anything other than a wildcard (or variable pattern) in Disco, so they should always
be fully covered. But if they are in a pair, for example, Set(Int)*Int,
we still need to generate 3 examples of the pair if that Int part isn't covered.
So how do we fill the concrete part of Set(Int), (or a generic type "a", or a function, etc.)?
I'm calling that unknown, and printing an underscore.
(Also, I'm using Infinite for reasons metioned above).