ghc-9.2.0.20210821: The GHC API
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

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

Semigroup Nablas Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Outputable Nablas Source # 
Instance details

Defined in GHC.HsToCore.Pmc.Solver.Types

Methods

ppr :: Nablas -> SDoc 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 fields 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 #

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.