Disco.Exhaustiveness.Constraint

The heart of the Lower Your Guards algorithm. Functions for converting constraints detailing pattern matches into a normalized description of everything that is left uncovered.

Documentation

data Constraint where

Constructors

CMatch :: DataCon -> [TypedVar] -> Constraint

CNot :: DataCon -> Constraint

CWasOriginally :: TypedVar -> Constraint

Instances

Show Constraint

Defined in Disco.Exhaustiveness.Constraint

Methods

showsPrec :: Int -> Constraint -> ShowS

show :: Constraint -> String

showList :: [Constraint] -> ShowS

Eq Constraint

Defined in Disco.Exhaustiveness.Constraint

Methods

(==) :: Constraint -> Constraint -> Bool

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

Ord Constraint

Defined in Disco.Exhaustiveness.Constraint

Methods

compare :: Constraint -> Constraint -> Ordering

(<) :: Constraint -> Constraint -> Bool

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

(>) :: Constraint -> Constraint -> Bool

(>=) :: Constraint -> Constraint -> Bool

max :: Constraint -> Constraint -> Constraint

min :: Constraint -> Constraint -> Constraint

posMatch :: [Constraint] -> Maybe (DataCon, [TypedVar])

negMatches :: [Constraint] -> [DataCon]

type ConstraintFor = (TypedVar, Constraint)

lookupVar :: TypedVar -> [ConstraintFor] -> TypedVar

alistLookup :: Eq a => a -> [(a, b)] -> [b]

onVar :: TypedVar -> [ConstraintFor] -> [Constraint]

type NormRefType = [ConstraintFor]

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

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

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

breakIf :: Alternative f => Bool -> f ()

conflictsWith :: Constraint -> Constraint -> Bool

Returns a predicate that returns true if another constraint conflicts with the one given. This alone is not sufficient to test if a constraint can be added, but it filters out the easy negatives early on

getConstructorArgs :: DataCon -> [Constraint] -> Maybe [TypedVar]

Search for a MatchDataCon that is matching on k specifically (there should be at most one, see I4 in section 3.4) and if it exists, return the variable ids of its arguments

substituteVarIDs :: TypedVar -> TypedVar -> [ConstraintFor] -> [ConstraintFor]

substituting y *for* x ie replace the second with the first, replace x with y

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

Deals with I2 from section 3.4 if a variable in the context has a resolvable type, there must be at least one constructor which can be instantiated without contradiction of the refinement type This function tests if this is true

instantiate :: Members '[Fresh, Reader TyDefCtx] r => NormRefType -> TypedVar -> DataCon -> Sem r Bool

Attempts to "instantiate" a match of the dataconstructor k on x If we can add the MatchDataCon constraint to the normalized refinement type without contradiction (a Nothing value), then x is inhabited by k and we return true