Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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
- data PhiCt
- type PhiCts = Bag PhiCt
- addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
- addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
- isInhabited :: Nablas -> DsM Bool
- generateInhabitingPatterns :: GenerateInhabitingPatternsMode -> [Id] -> Int -> Nabla -> DsM [Nabla]
- data GenerateInhabitingPatternsMode
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
A disjunctive bag of Nabla
s, representing a refinement type.
initNablas :: Nablas Source #
A high-level pattern-match constraint. Corresponds to φ from Figure 3 of the LYG paper.
PhiTyCt !PredType | A type constraint "T ~ U". |
PhiCoreCt !Id !CoreExpr |
|
PhiConCt !Id !PmAltCon ![TyVar] ![PredType] ![Id] |
|
PhiNotConCt !Id !PmAltCon |
|
PhiBotCt !Id |
|
PhiNotBotCt !Id |
|
Instances
generateInhabitingPatterns :: GenerateInhabitingPatternsMode -> [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.
data GenerateInhabitingPatternsMode Source #
See Note [Case split inhabiting patterns]