Disco.Exhaustiveness

Entry point into the exhaustiveness checker. Converts information into a format the checker understands, then pretty prints the results of running it.

Documentation

checkClauses :: Members '[Fresh, Reader TyDefCtx, Output (Message ann), Embed IO] r => Name ATerm -> [Type] -> NonEmpty [APattern] -> Sem r ()

This exhaustiveness checking algorithm is based on the paper "Lower Your Guards: A Compositional Pattern-Match Coverage Checker": https://www.microsoft.com/en-us/research/uploads/prod/2020/03/lyg.pdf

Some simplifications were made to adapt the algorithm to suit Disco. The most notable change is that here we always generate (at most) 3 concrete examples of uncovered patterns, instead of finding the most general complete description of every uncovered input.

prettyPrintExample :: ExamplePat -> Sem r (Doc ann)

prettyPrintPattern :: Members '[Reader PA, LFresh] r => Pattern -> Sem r (Doc ann)

exampleToDiscoPattern :: ExamplePat -> Pattern

resugarPair :: ExamplePat -> [ExamplePat]

resugarList :: ExamplePat -> [ExamplePat]

resugarString :: ExamplePat -> String

assumeExampleChar :: ExamplePat -> Char

desugarClause :: Members '[Fresh, Embed IO] r => [TypedVar] -> Int -> [APattern] -> Sem r Gdt

desugarTuplePats :: [APattern] -> APattern

desugarMatch :: Members '[Fresh, Embed IO] r => TypedVar -> APattern -> Sem r [Guard]

Convert a Disco APattern into a list of Guards which cover that pattern

These patterns are currently not handled: , APNeg --still need to handle rational case , APFrac --required for rationals? algebraic (probably will be eventually replaced anyway): , APAdd , APMul , APSub These (or some updated version of them) may be handled eventually, once updated arithmetic patterns are merged.

We treat unhandled patterns as if they are exhaustively matched against (aka, they are seen as wildcards by the checker). This necessarily results in some false negatives, but no false positives.

data Gdt where

Constructors

Grhs :: Int -> Gdt

Branch :: Gdt -> Gdt -> Gdt

Guarded :: Guard -> Gdt -> Gdt

Instances

Show Gdt

Defined in Disco.Exhaustiveness

Methods

showsPrec :: Int -> Gdt -> ShowS

show :: Gdt -> String

showList :: [Gdt] -> ShowS

Eq Gdt

Defined in Disco.Exhaustiveness

Methods

(==) :: Gdt -> Gdt -> Bool

(/=) :: Gdt -> Gdt -> Bool

type Guard = (TypedVar, GuardConstraint)

data GuardConstraint where

Constructors

GMatch :: DataCon -> [TypedVar] -> GuardConstraint

GWasOriginally :: TypedVar -> GuardConstraint

Instances

Show GuardConstraint

Defined in Disco.Exhaustiveness

Methods

showsPrec :: Int -> GuardConstraint -> ShowS

show :: GuardConstraint -> String

showList :: [GuardConstraint] -> ShowS

Eq GuardConstraint

Defined in Disco.Exhaustiveness

Methods

(==) :: GuardConstraint -> GuardConstraint -> Bool

(/=) :: GuardConstraint -> GuardConstraint -> Bool

newtype Literal

Constructors

Literal (TypedVar, LitCond)

data LitCond where

Constructors

LitMatch :: DataCon -> [TypedVar] -> LitCond

LitNot :: DataCon -> LitCond

LitWasOriginally :: TypedVar -> LitCond

Instances

Show LitCond

Defined in Disco.Exhaustiveness

Methods

showsPrec :: Int -> LitCond -> ShowS

show :: LitCond -> String

showList :: [LitCond] -> ShowS

Eq LitCond

Defined in Disco.Exhaustiveness

Methods

(==) :: LitCond -> LitCond -> Bool

(/=) :: LitCond -> LitCond -> Bool

Ord LitCond

Defined in Disco.Exhaustiveness

Methods

compare :: LitCond -> LitCond -> Ordering

(<) :: LitCond -> LitCond -> Bool

(<=) :: LitCond -> LitCond -> Bool

(>) :: LitCond -> LitCond -> Bool

(>=) :: LitCond -> LitCond -> Bool

max :: LitCond -> LitCond -> LitCond

min :: LitCond -> LitCond -> LitCond

data Ant where

Constructors

AGrhs :: [NormRefType] -> Int -> Ant

ABranch :: Ant -> Ant -> Ant

Instances

Show Ant

Defined in Disco.Exhaustiveness

Methods

showsPrec :: Int -> Ant -> ShowS

show :: Ant -> String

showList :: [Ant] -> ShowS

ua :: Members '[Fresh, Reader TyDefCtx] r => [NormRefType] -> Gdt -> Sem r ([NormRefType], Ant)

addLitMulti :: Members '[Fresh, Reader TyDefCtx] r => [NormRefType] -> Literal -> Sem r [NormRefType]

addLiteral :: Members '[Fresh, Reader TyDefCtx] r => NormRefType -> Literal -> MaybeT (Sem r) NormRefType

data InhabPat where

Constructors

IPIs :: DataCon -> [InhabPat] -> InhabPat

IPNot :: [DataCon] -> InhabPat

Instances

Show InhabPat

Defined in Disco.Exhaustiveness

Methods

showsPrec :: Int -> InhabPat -> ShowS

show :: InhabPat -> String

showList :: [InhabPat] -> ShowS

Eq InhabPat

Defined in Disco.Exhaustiveness

Methods

(==) :: InhabPat -> InhabPat -> Bool

(/=) :: InhabPat -> InhabPat -> Bool

Ord InhabPat

Defined in Disco.Exhaustiveness

Methods

compare :: InhabPat -> InhabPat -> Ordering

(<) :: InhabPat -> InhabPat -> Bool

(<=) :: InhabPat -> InhabPat -> Bool

(>) :: InhabPat -> InhabPat -> Bool

(>=) :: InhabPat -> InhabPat -> Bool

max :: InhabPat -> InhabPat -> InhabPat

min :: InhabPat -> InhabPat -> InhabPat

mkIPMatch :: DataCon -> [InhabPat] -> InhabPat

findInhabitants :: Members '[Fresh, Reader TyDefCtx] r => [NormRefType] -> [TypedVar] -> Sem r (Possibilities [InhabPat])

findAllForNref :: Members '[Fresh, Reader TyDefCtx] r => NormRefType -> [TypedVar] -> Sem r (Possibilities [InhabPat])

findVarInhabitants :: Members '[Fresh, Reader TyDefCtx] r => TypedVar -> NormRefType -> Sem r (Possibilities InhabPat)

findRedundant :: Members '[Fresh, Reader TyDefCtx] r => Ant -> [TypedVar] -> Sem r [Int]

data ExamplePat where

Constructors

ExamplePat :: DataCon -> [ExamplePat] -> ExamplePat

Instances

Show ExamplePat

Defined in Disco.Exhaustiveness

Methods

showsPrec :: Int -> ExamplePat -> ShowS

show :: ExamplePat -> String

showList :: [ExamplePat] -> ShowS

findPosExamples :: Members '[Fresh, Reader TyDefCtx] r => [NormRefType] -> [TypedVar] -> Sem r [[ExamplePat]]

Less general version of the above inhabitant finding function returns a maximum of 3 possible args lists that haven't been matched against, as to not overwhelm new users of the language. This is essentially a DFS, and it has a bad habit of trying to build infinite lists whenever it can, so we give it a max depth of 32 If we reach 32 levels of nested dataconstructors in this language, it is pretty safe to assume we were chasing after an infinite structure

findAllPosForNref :: Members '[Fresh, Reader TyDefCtx] r => Int -> NormRefType -> [TypedVar] -> Sem r (Possibilities [ExamplePat])

findVarPosExamples :: Members '[Fresh, Reader TyDefCtx] r => Int -> TypedVar -> NormRefType -> Sem r (Possibilities ExamplePat)

getPosFrom :: Type -> TyDefCtx -> [DataCon] -> [DataCon]

mkExampleMatch :: DataCon -> [ExamplePat] -> ExamplePat