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
- 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
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
Outputable Nabla # | |
Defined in GHC.HsToCore.Pmc.Solver.Types |
A disjunctive bag of Nabla
s, representing a refinement type.
Instances
Monoid Nablas # | |
Semigroup Nablas # | |
Outputable Nablas # | |
Defined in GHC.HsToCore.Pmc.Solver.Types |
initNablas :: Nablas #
lookupRefuts :: Nabla -> Id -> [PmAltCon] #
lookupSolution :: Nabla -> Id -> Maybe PmAltConApp #
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 |
|
PhiConCt !Id !PmAltCon ![TyVar] ![PredType] ![Id] |
|
PhiNotConCt !Id !PmAltCon |
|
PhiBotCt !Id |
|
PhiNotBotCt !Id |
|
Instances
Outputable PhiCt # | |
Defined in GHC.HsToCore.Pmc.Solver |
isInhabited :: Nablas -> DsM Bool #