| 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 Nablas, 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 #