Safe Haskell	Safe-Inferred
Language	Haskell2010

GHC.HsToCore.Pmc.Solver

Description

Model refinements type as per the Lower Your Guards paper. The main export of the module are the functions addPhiCtsNablas for adding facts to the oracle, isInhabited to check if a refinement type is inhabited and generateInhabitingPatterns to turn a Nabla into a concrete pattern for an equation.

In terms of the LYG paper, this module is concerned with Sections 3.4, 3.6 and 3.7. E.g., it represents refinement types directly as a bunch of normalised refinement types Nabla.

Synopsis

data Nabla
newtype Nablas = MkNablas (Bag Nabla)
initNablas :: Nablas
lookupRefuts :: Nabla -> Id -> [PmAltCon]
lookupSolution :: Nabla -> Id -> Maybe PmAltConApp
data PhiCt
- = PhiTyCt !PredType
- | PhiCoreCt !Id !CoreExpr
- | PhiConCt !Id !PmAltCon ![TyVar] ![PredType] ![Id]
- | PhiNotConCt !Id !PmAltCon
- | PhiBotCt !Id
- | PhiNotBotCt !Id
type PhiCts = Bag PhiCt
addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
isInhabited :: Nablas -> DsM Bool
generateInhabitingPatterns :: [Id] -> Int -> Nabla -> DsM [Nabla]

Documentation

data Nabla Source #

A normalised refinement type ∇ ("nabla"), comprised of an inert set of canonical (i.e. mutually compatible) term and type constraints that form the refinement type's predicate.

Instances

Instances details

Outputable Nabla Source #
Instance details Defined in GHC.HsToCore.Pmc.Solver.Types Methods ppr :: Nabla -> SDoc Source #

newtype Nablas Source #

A disjunctive bag of Nablas, representing a refinement type.

Constructors

MkNablas (Bag Nabla)

Instances

Instances details

Monoid Nablas Source #
Instance details Defined in GHC.HsToCore.Pmc.Solver.Types Methods mempty :: Nablas Source # mappend :: Nablas -> Nablas -> Nablas Source # mconcat :: [Nablas] -> Nablas Source #
Semigroup Nablas Source #
Instance details Defined in GHC.HsToCore.Pmc.Solver.Types Methods (<>) :: Nablas -> Nablas -> Nablas Source # sconcat :: NonEmpty Nablas -> Nablas Source # stimes :: Integral b => b -> Nablas -> Nablas Source #
Outputable Nablas Source #
Instance details Defined in GHC.HsToCore.Pmc.Solver.Types Methods ppr :: Nablas -> SDoc Source #

initNablas :: Nablas Source #

lookupRefuts :: Nabla -> Id -> [PmAltCon] Source #

lookupSolution :: Nabla -> Id -> Maybe PmAltConApp Source #

data PhiCt Source #

A high-level pattern-match constraint. Corresponds to φ from Figure 3 of the LYG paper.

Constructors

PhiTyCt !PredType	A type constraint "T ~ U".
PhiCoreCt !Id !CoreExpr	`PhiCoreCt x e` encodes "x ~ e", equating `x` with the `CoreExpr` `e`.
PhiConCt !Id !PmAltCon ![TyVar] ![PredType] ![Id]	`PhiConCt x K tvs dicts ys` encodes `K @tvs dicts ys <- x`, matching `x` against the `PmAltCon` application `K @tvs dicts ys`, binding `tvs`, `dicts` and possibly unlifted fields `ys` in the process. See Note [Strict fields and variables of unlifted type].
PhiNotConCt !Id !PmAltCon	`PhiNotConCt x K` encodes "x ≁ K", asserting that `x` can't be headed by `K`.
PhiBotCt !Id	`PhiBotCt x` encodes "x ~ ⊥", equating `x` to ⊥. by `K`.
PhiNotBotCt !Id	`PhiNotBotCt x y` encodes "x ≁ ⊥", asserting that `x` can't be ⊥.

Instances

Instances details

Outputable PhiCt Source #
Instance details Defined in GHC.HsToCore.Pmc.Solver Methods ppr :: PhiCt -> SDoc Source #

type PhiCts = Bag PhiCt Source #

addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas Source #

addPmCtsNablas for a single PmCt.

addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas Source #

Add a bunch of PhiCts to all the Nablas. Lifts addPhiCts over many Nablas.

isInhabited :: Nablas -> DsM Bool Source #

Test if any of the Nablas is inhabited. Currently this is pure, because we preserve the invariant that there are no uninhabited Nablas. But that could change in the future, for example by implementing this function in terms of notNull $ generateInhabitingPatterns 1 ds.

generateInhabitingPatterns :: [Id] -> Int -> Nabla -> DsM [Nabla] Source #

generateInhabitingPatterns vs n nabla returns a list of at most n (but perhaps empty) refinements of nabla that represent inhabited patterns. Negative information is only retained if literals are involved or for recursive GADTs.