Safe Haskell  None 

Language  GHC2021 
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 highlevel patternmatch 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]